Fix var_eq from keeping equalities with pointers to globals

src/analyses/varEq.ml

@@ -353,6 +353,29 @@ struct
       | _ -> D.top ()
     *)
 
+  let rec is_global_var (ask: Queries.ask) x =
+    match x with
+    | SizeOf _
+    | SizeOfE _
+    | SizeOfStr _
+    | AlignOf _
+    | AlignOfE _
+    | UnOp _
+    | BinOp _ -> None
+    | Const _ -> Some false
+    | Lval (Var v,_) -> Some v.vglob
+    | Lval (Mem e, _) ->
+      begin match ask (Queries.MayPointTo e) with
+        | `LvalSet ls when not (Queries.LS.is_top ls) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) ls) ->
+          Some (Queries.LS.exists (fun (v, _) -> is_global_var ask (Lval (var v)) = Some true) ls)
+        | _ -> Some true
+      end
+    | CastE (t,e) -> is_global_var ask e
+    | AddrOf lval -> Some false
+    | StartOf lval -> Some false
+    | Question _ -> failwith "Logical operations should be compiled away by CIL."
+    | _ -> failwith "Unmatched pattern."
+
   (* Set given lval equal to the result of given expression. On doubt do nothing. *)
   let add_eq ask (lv:lval) (rv:Exp.t) st =
     (*    let is_local x =
@@ -361,9 +384,9 @@ struct
           let st =
     *)  let lvt = unrollType @@ typeOf (Lval lv) in
     (*     Messages.report (sprint 80 (d_type () lvt)); *)
-    if Exp.is_global_var (Lval lv) = Some false
+    if is_global_var ask (Lval lv) = Some false
     && Exp.interesting rv
-    && Exp.is_global_var rv = Some false
+    && is_global_var ask rv = Some false
     && ((isArithmeticType lvt && match lvt with | TFloat _ -> false | _ -> true ) || isPointerType lvt)
     then D.add_eq (rv,Lval lv) (remove ask lv st)
     else remove ask lv st

src/cdomains/exp.ml

@@ -98,24 +98,6 @@ struct
     in
     cv e
 
-  let rec is_global_var x =
-    match x with
-    | SizeOf _
-    | SizeOfE _
-    | SizeOfStr _
-    | AlignOf _
-    | AlignOfE _
-    | UnOp _
-    | BinOp _ -> None
-    | Const _ -> Some false
-    | Lval (Var v,_) -> Some v.vglob
-    | Lval (Mem e,_) -> is_global_var e
-    | CastE (t,e) -> is_global_var e
-    | AddrOf lval -> Some false
-    | StartOf lval -> Some false
-    | Question _ -> failwith "Logical operations should be compiled away by CIL."
-    | _ -> failwith "Unmatched pattern."
-
   let rec conv_offs (offs:(fieldinfo,exp) Lval.offs) : offset =
     match offs with
     | `NoOffset -> NoOffset

src/util/goblintutil.ml

@@ -118,7 +118,8 @@ let escape (x:string):string =
   Str.global_replace (Str.regexp ">") ">" |>
   Str.global_replace (Str.regexp "\"") """ |>
   Str.global_replace (Str.regexp "'") "'" |>
-  Str.global_replace (Str.regexp "\x0b") "" (* g2html just cannot handle \v from some kernel benchmarks, even when escaped... *)
+  Str.global_replace (Str.regexp "\x0b") "" |> (* g2html just cannot handle \v from some kernel benchmarks, even when escaped... *)
+  Str.global_replace (Str.regexp "\001") "" (* g2html just cannot handle \v from some kernel benchmarks, even when escaped... *)
 
 let trim (x:string): string =
   let len = String.length x in

tests/regression/06-symbeq/22-var_eq_types.c

@@ -1,4 +1,4 @@
-// PARAM: --disable ana.mutex.disjoint_types --set ana.activated[+] "'var_eq'" 
+// PARAM: --disable ana.mutex.disjoint_types --set ana.activated[+] "'var_eq'"
 #include <stdio.h>
 
 extern short * anShortPlease();
@@ -38,7 +38,7 @@ extern void f(int *);
 extern struct s ** get_s();
 
 int t17(){
-	int i = i % 6;
+	int i = i % 6; // WTF?
 	struct s ss[6], *ps;
 
 	ps = &ss[i];
@@ -54,9 +54,9 @@ int t16(){
 	int i;
 	struct t tt, *pt, tt2;
 	struct s ss,ss2;
-
+	// UB: deref uninit ptr pt
 	pt->ss->i = i;
-	assert(pt->ss->i == i);
+	assert(pt->ss->i == i); // UNKNOWN?
 
 	tt = tt2;
 	assert(pt->ss->i == i); // UNKNOWN
@@ -71,9 +71,9 @@ int t15(){
 
 //	pt = &tt;
 	tt.ss = &ss;
-
+	// UB: deref uninit ptr pt
 	pt->ss->i = i;
-	assert(pt->ss->i == i);
+	assert(pt->ss->i == i); // UNKNOWN?
 
 	ss = ss2;
 	assert(pt->ss->i == i); // UNKNOWN
@@ -88,9 +88,9 @@ int t14(){
 
 //	pt = &tt;
 //	tt.ss = &ss;
-
+	// UB: deref uninit ptr pt
 	pt->ss->i = i;
-	assert(pt->ss->i == i);
+	assert(pt->ss->i == i); // UNKNOWN?
 	ss.i = 1;
 	assert(pt->ss->i == i); // UNKNOWN
 

tests/regression/06-symbeq/25-ptr_global.c

@@ -0,0 +1,28 @@
+// PARAM: --set ana.activated[+] "'var_eq'"
+// Own version of 29/20
+#include <pthread.h>
+#include <stdlib.h>
+#include <assert.h>
+
+int *global;
+
+void *t_fun(void *arg) {
+  int *p = global;
+  *p = 2;
+  assert(*p == 2); // UNKNOWN!
+  return NULL;
+}
+
+int main(void) {
+  global = malloc(sizeof(int));
+  int *p = global;
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  *p = 1;
+  assert(*p == 1); // UNKNOWN!
+
+  pthread_join (id, NULL);
+  return 0;
+}

tests/regression/29-svcomp/20-char_generic_nvram.c

@@ -0,0 +1,41 @@
+// PARAM: --set ana.activated[+] "'var_eq'"
+// Minimized from pthread-driver-races/char_generic_nvram_read_nvram_write_nvram.i
+#include <pthread.h>
+#include <stdlib.h>
+#include <assert.h>
+
+typedef long long loff_t;
+
+void read_nvram(loff_t *ppos)
+{
+ unsigned int i;
+ *ppos = i;
+ assert(*ppos == i); // UNKNOWN!
+}
+void write_nvram(loff_t *ppos)
+{
+ unsigned int i;
+ *ppos = i;
+ assert(*ppos == i); // UNKNOWN!
+}
+loff_t *whoop_loff_t;
+void *whoop_wrapper_write_nvram(void* args)
+{
+ write_nvram(whoop_loff_t);
+ return ((void *)0);
+}
+void *whoop_wrapper_read_nvram(void* args)
+{
+ read_nvram(whoop_loff_t);
+ return ((void *)0);
+}
+int main(void)
+{
+ whoop_loff_t = (loff_t *) malloc(sizeof(loff_t));
+ pthread_t pthread_t_write_nvram;
+ pthread_t pthread_t_read_nvram;
+ pthread_create(&pthread_t_write_nvram, ((void *)0), whoop_wrapper_write_nvram, ((void *)0));
+ pthread_create(&pthread_t_read_nvram, ((void *)0), whoop_wrapper_read_nvram, ((void *)0));
+ pthread_join(pthread_t_write_nvram, ((void *)0));
+ pthread_join(pthread_t_read_nvram, ((void *)0));
+}