Merge branch 'goblint:master' into master

src/cdomain/value/cdomains/intDomain.ml

@@ -1910,7 +1910,6 @@ struct
     | `Definite x -> if i = x then `Eq else `Neq
     | `Excluded (s,r) -> if S.mem i s then `Neq else `Top
 
-  let top_of ik = `Excluded (S.empty (), size ik)
   let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov ik = function
     | `Excluded (s,r) ->
       let r' = size ik in
@@ -2419,10 +2418,13 @@ module Enums : S with type int_t = Z.t = struct
   type int_t = Z.t
   let name () = "enums"
   let bot () = failwith "bot () not implemented for Enums"
-  let top_of ik = Exc (BISet.empty (), size ik)
   let top () = failwith "top () not implemented for Enums"
   let bot_of ik = Inc (BISet.empty ())
   let top_bool = Inc (BISet.of_list [Z.zero; Z.one])
+  let top_of ik =
+    match ik with
+    | IBool -> top_bool
+    | _ -> Exc (BISet.empty (), size ik)
 
   let range ik = Size.range ik
 
@@ -2722,20 +2724,32 @@ module Enums : S with type int_t = Z.t = struct
   let ne ik x y = c_lognot ik (eq ik x y)
 
   let invariant_ikind e ik x =
+    let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
     match x with
+    | Inc ps when not inexact_type_bounds && ik = IBool && is_top_of ik x ->
+      Invariant.none
     | Inc ps ->
       if BISet.cardinal ps > 1 || get_bool "witness.invariant.exact" then
-        List.fold_left (fun a x ->
+        BISet.fold (fun x a ->
             let i = Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x, intType)) in
             Invariant.(a || i) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
-          ) (Invariant.bot ()) (BISet.elements ps)
+          ) ps (Invariant.bot ())
       else
         Invariant.top ()
-    | Exc (ns, _) ->
-      List.fold_left (fun a x ->
+    | Exc (ns, r) ->
+      (* Emit range invariant if tighter than ikind bounds.
+         This can be more precise than interval, which has been widened. *)
+      let (rmin, rmax) = (Exclusion.min_of_range r, Exclusion.max_of_range r) in
+      let (ikmin, ikmax) =
+        let ikr = size ik in
+        (Exclusion.min_of_range ikr, Exclusion.max_of_range ikr)
+      in
+      let imin = if inexact_type_bounds || Z.compare ikmin rmin <> 0 then Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik rmin, e, intType)) else Invariant.none in
+      let imax = if inexact_type_bounds || Z.compare rmax ikmax <> 0 then Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik rmax, intType)) else Invariant.none in
+      BISet.fold (fun x a ->
           let i = Invariant.of_exp Cil.(BinOp (Ne, e, kintegerCilint ik x, intType)) in
           Invariant.(a && i)
-        ) (Invariant.top ()) (BISet.elements ns)
+        ) ns Invariant.(imin && imax)
 
 
   let arbitrary ik =

tests/regression/04-mutex/58-pthread-lock-return.c

@@ -68,9 +68,10 @@ void *t_fun(void *arg) {
     __goblint_check(1); // reachable
   }
 
+  int reach1 = 0, reach2 = 0, reach3 = 0;
 #ifndef __APPLE__
   if (!pthread_spin_lock(&spin)) {
-    __goblint_check(1); // TODO reachable (TODO for OSX)
+    reach1 = 1;
     g_spin++; // NORACE
     pthread_spin_unlock(&spin);
   }
@@ -79,14 +80,25 @@ void *t_fun(void *arg) {
   }
 
   if (!pthread_spin_trylock(&spin)) {
-    __goblint_check(1); // TODO reachable (TODO for OSX)
+    reach2 = 1;
     g_spin++; // NORACE
     pthread_spin_unlock(&spin);
   }
   else {
-    __goblint_check(1); // TODO reachable (TODO for OSX)
-  }
+    reach3 = 1;
+  }
+#else
+  // fake values so test passes on OSX
+  reach1 = 1;
+  int r;
+  if (r)
+    reach2 = 1;
+  else
+    reach3 = 1;
 #endif
+  __goblint_check(reach1); // always reached
+  __goblint_check(reach2); // UNKNOWN! (sometimes reached)
+  __goblint_check(reach3); // UNKNOWN! (sometimes reached)
 
   return NULL;
 }

tests/regression/36-apron/21-traces-cluster-based.c

@@ -1,6 +1,7 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions --set ana.relation.privatization mutex-meet
 extern int __VERIFIER_nondet_int();
-
+// Normal mutex-meet is enough here, this doesn't require mutex-meet-tid-cluster* (despite the name).
+// The name is "cluster-based" for historical reasons to match the example name in more-traces paper repository.
 #include <pthread.h>
 #include <goblint.h>
 
@@ -45,7 +46,7 @@ void *t3_fun(void *arg) {
   y = h;
   pthread_mutex_unlock(&A);
   pthread_mutex_unlock(&B);
-  __goblint_check(y == x); // TODO (mutex-meet succeeds, protection unknown)
+  __goblint_check(y == x); // mutex-meet succeeds, protection unknown
   return NULL;
 }
 
@@ -63,9 +64,9 @@ int main(void) {
   x = g;
   y = h;
   pthread_mutex_lock(&B);
-  __goblint_check(y == x); // TODO (mutex-meet succeeds, protection unknown)
+  __goblint_check(y == x); // mutex-meet succeeds, protection unknown
   pthread_mutex_unlock(&B);
   pthread_mutex_unlock(&A);
-  __goblint_check(y == x); // TODO (mutex-meet succeeds, protection unknown)
+  __goblint_check(y == x); // mutex-meet succeeds, protection unknown
   return 0;
 }

tests/regression/36-apron/22-traces-write-centered-vs-meet-mutex.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions --set ana.relation.privatization mutex-meet
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
@@ -22,11 +22,11 @@ void *t_fun(void *arg) {
     y = h;
     __goblint_check(y <= x);
     pthread_mutex_lock(&B);
-    __goblint_check(x == y); // TODO (mutex-meet succeeds, write unknown)
+    __goblint_check(x == y); // mutex-meet succeeds, (now-defunct) write unknown
     pthread_mutex_unlock(&B);
     i = x + 31;
     z = i;
-    __goblint_check(z >= x); // TODO (write succeeds, mutex-meet unknown)
+    __goblint_check(z >= x); // TODO ((now-defunct) write succeeds, mutex-meet unknown)
     pthread_mutex_unlock(&A);
     pthread_mutex_unlock(&C);
   }

tests/regression/36-apron/34-large-bigint.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[-] expRelation
 #include <goblint.h>
 
 void main() {
@@ -9,14 +9,15 @@ void main() {
     __goblint_check(y < z);
     __goblint_check(x < z);
 
-    if (18446744073709551612ull <= x && z <= 18446744073709551615ull) {
-      __goblint_check(18446744073709551612ull <= x); // TODO (unknown with D, success with MPQ)
-      __goblint_check(x <= 18446744073709551613ull); // TODO (unknown with D, success with MPQ)
-      __goblint_check(18446744073709551613ull <= y); // TODO (unknown with D, success with MPQ)
-      __goblint_check(y <= 18446744073709551614ull); // TODO (unknown with D, success with MPQ)
-      __goblint_check(18446744073709551614ull <= z); // TODO (unknown with D, success with MPQ)
-      __goblint_check(z <= 18446744073709551615ull); // TODO (unknown with D, success with MPQ)
+    if (18446744073709551611ull <= x && z <= 18446744073709551614ull) {
+      __goblint_check(18446744073709551611ull <= x); // TODO (unknown with D, success with MPQ)
+      __goblint_check(x <= 18446744073709551612ull); // TODO (unknown with D, success with MPQ)
+      __goblint_check(18446744073709551612ull <= y); // TODO (unknown with D, success with MPQ)
+      __goblint_check(y <= 18446744073709551613ull); // TODO (unknown with D, success with MPQ)
+      __goblint_check(18446744073709551613ull <= z); // TODO (unknown with D, success with MPQ)
+      __goblint_check(z <= 18446744073709551614ull); // TODO (unknown with D, success with MPQ)
 
+      // disable expRelation to prevent base from simplifying x - x to 0
       __goblint_check(x >= x - x); // avoid base from answering to check if apron doesn't say x == -3
       __goblint_check(y >= y - y); // avoid base from answering to check if apron doesn't say y == -3
       __goblint_check(z >= z - z); // avoid base from answering to check if apron doesn't say z == -3

tests/regression/36-apron/38-branch-global.c

@@ -10,6 +10,6 @@ int main() {
         __goblint_check(count < ARR_SIZE);
         count++;
     }
-    __goblint_check(count == ARR_SIZE); // TODO (requires threshold)
+    __goblint_check(count == ARR_SIZE); // requires narrowing
     return 0 ;
 }

tests/regression/36-apron/42-threadenter-arg.c

@@ -2,8 +2,8 @@
 #include <pthread.h>
 #include <goblint.h>
 
-void *t_fun(int arg) {
-  __goblint_check(arg == 3); // TODO (cast through void*)
+void *t_fun(int arg) { // check that apron doesn't crash with tracked thread argument
+  __goblint_check(arg == 3); // cast through void*, passes by base
   return NULL;
 }
 

tests/regression/36-apron/90-mine14-5b.c

@@ -46,6 +46,10 @@ int main(void) {
   pthread_create(&id2, NULL, t_fun2, NULL);
   pthread_mutex_lock(&mutex);
   __goblint_check(x==y);
+  __goblint_check(0 <= x);
+  __goblint_check(x <= 10);
+  __goblint_check(0 <= y);
+  __goblint_check(y <= 10);
   pthread_mutex_unlock(&mutex);
   return 0;
 }

tests/regression/36-apron/91-mine14-5b-no-threshhold.c

@@ -46,7 +46,11 @@ int main(void) {
   pthread_create(&id, NULL, t_fun, NULL);
   pthread_create(&id2, NULL, t_fun2, NULL);
   pthread_mutex_lock(&mutex);
-  __goblint_check(x==y); //TODO
+  __goblint_check(x==y);
+  __goblint_check(0 <= x);
+  __goblint_check(x <= 10); // TODO
+  __goblint_check(0 <= y);
+  __goblint_check(y <= 10); // TODO
   pthread_mutex_unlock(&mutex);
   return 0;
 }

tests/regression/46-apron2/75-mutex_with_ghosts.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none --set ana.base.privatization protection-atomic
 /*-----------------------------------------------------------------------------
  * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
  *                       witness validation using locking to access a shared
@@ -53,6 +53,7 @@ int main()
   pthread_mutex_lock(&m);
   __VERIFIER_atomic_end();
 
+  // TODO: works with base protection privatization but not protection-atomic
   __goblint_check(used == 0); // TODO (read/refine? of used above makes used write-unprotected)
 
   __VERIFIER_atomic_begin();

tests/regression/56-witness/46-top-bool-invariant.c

@@ -0,0 +1,6 @@
+// PARAM: --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set --disable witness.invariant.inexact-type-bounds
+
+int main() {
+  _Bool x;
+  return 0;
+}