Merge pull request #1468 from goblint/issue_1467

Make meet in AddressDomain more precise

Author: michael-schwarz

src/analyses/base.ml

@@ -1613,7 +1613,7 @@ struct
   let set ~(man: _ man) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store =
     let update_variable x t y z =
       if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a" x.vname VD.pretty y CPA.pretty z;
-      let r = update_variable x t y z in (* refers to defintion that is outside of set *)
+      let r = update_variable x t y z in (* refers to definition that is outside of set *)
       if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\nresults in\n%a" x.vname VD.pretty y CPA.pretty z CPA.pretty r;
       r
     in

src/domain/disjointDomain.ml

@@ -184,14 +184,25 @@ sig
   val may_be_equal: elt -> elt -> bool
 end
 
-module ProjectiveSetPairwiseMeet (E: Printable.S) (B: MayEqualSetDomain with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t = struct
+module ProjectiveSetPairwiseMeet (E: Lattice.S) (B: MayEqualSetDomain with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t = struct
   include ProjectiveSet (E) (B) (R)
 
   let meet m1 m2 =
     let meet_buckets b1 b2 acc =
       B.fold (fun e1 acc ->
+          let r1 = R.of_elt e1 in
           B.fold (fun e2 acc ->
-              if B.may_be_equal e1 e2 then
+              (* If they have the same representative, we use the normal meet within this bucket *)
+              if R.equal r1 (R.of_elt e2) then
+                try
+                  let m = E.meet e1 e2 in
+                  if not (E.is_bot m) then
+                    add m acc
+                  else
+                    acc
+                with Lattice.Uncomparable ->
+                  failwith (GobPretty.sprintf "Elements %a and %a are in same bucket, but meet throws!" E.pretty e1 E.pretty e2)
+              else if B.may_be_equal e1 e2 then
                 add e1 (add e2 acc)
               else
                 acc

tests/regression/13-privatized/89-write-lacking-precision.c

@@ -0,0 +1,31 @@
+// PARAM: --set ana.base.privatization write
+#include<pthread.h>
+struct a {
+  char* b;
+};
+
+struct a *c;
+struct a h = {""};
+struct a i = {"string"};
+
+void* d(void* args) {
+  if (c->b) {
+    // Handled by privatization as a write
+    // Without fix (#1468) causes both h.b and i.b to become unknown string
+    __goblint_check(strlen(h.b) == 0); // Check h.b is still known
+  }
+}
+
+int main() {
+  int top;
+
+  if(top) {
+    c = &h;
+  } else {
+    c = &i;
+  }
+
+  pthread_t t;
+  pthread_create(&t, 0, d, 0);
+  return 0;
+}

tests/regression/27-inv_invariants/23-meet-ptrs.c

@@ -0,0 +1,51 @@
+//PARAM:  --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <time.h>
+
+int more_intricate() {
+   int arr[20];
+
+   int top;
+
+   int i = 2;
+   int j = 8;
+   if(top) {
+      i = 8;
+      j = 9;
+   }
+
+   int* imprecise1 = &arr[i]; // &arr[2..8]
+   int* imprecise2 = &arr[j]; // &arr[8..9]
+
+   if(imprecise1 == imprecise2) {
+      __goblint_check(imprecise1 == &arr[8]);
+      __goblint_check(imprecise2 == &arr[8]); //TODO (Refinement should happen in both directions!)
+   }
+
+   if(imprecise1 == &arr[j]) {
+      __goblint_check(imprecise1 == &arr[8]);
+   }
+
+}
+
+
+int main() {
+   int arr[20];
+
+   int top;
+
+   int i = 2;
+   if(top) {
+      i = 8;
+   }
+
+   int* imprecise = &arr[i];
+
+   if(imprecise == &arr[2]) {
+      __goblint_check(imprecise == &arr[2]);
+   }
+
+   more_intricate();
+   return 0;
+}