Make meet in AddressDomain more precise

src/analyses/base.ml

@@ -1579,7 +1579,7 @@ struct
   let set ~(ctx: _ ctx) ?(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/cdomain/value/cdomains/addressDomain.ml

@@ -110,6 +110,11 @@ struct
     | StrPtr _, UnknownPtr -> None
     | _, _ -> Some false
 
+  let amenable_to_meet x y = match x,y with
+    | StrPtr _, StrPtr _ -> true
+    | Addr x, Addr y when Mval.equal (Mval.top_indices x) (Mval.top_indices y) -> true
+    | _ -> false
+
   let leq x y = match x, y with
     | StrPtr s1, StrPtr s2   -> SD.leq s1 s2
     | Addr x, Addr y -> Mval.leq x y
@@ -178,6 +183,7 @@ struct
   struct
     include SetDomain.Joined (Addr)
     let may_be_equal a b = Option.value (Addr.semantic_equal a b) ~default:true
+    let amenable_to_meet = Addr.amenable_to_meet
   end
   module OffsetSplit = DisjointDomain.ProjectiveSetPairwiseMeet (Addr) (J) (Addr.UnitOffsetRepr)
 

src/cdomain/value/cdomains/addressDomain_intf.ml

@@ -82,6 +82,10 @@ sig
     (** Check semantic equality of two addresses.
 
         @return [Some true] if definitely equal, [Some false] if definitely not equal, [None] if unknown. *)
+
+    val amenable_to_meet: t -> t -> bool
+    (** Whether two addresses are amenable to meet operation, i.e., their lattice meet overapproximates the intersection
+        of concretizations. If true, meet is used instead of semantic_equal *)
   end
 
   (** Address lattice with sublattice representatives for {!DisjointDomain}. *)

src/domain/disjointDomain.ml

@@ -182,16 +182,26 @@ module type MayEqualSetDomain =
 sig
   include SetDomain.S
   val may_be_equal: elt -> elt -> bool
+  val amenable_to_meet: 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 ->
           B.fold (fun e2 acc ->
-              if B.may_be_equal e1 e2 then
+              if B.amenable_to_meet e1 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 "amenable_to_meet %a %a returned true, 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,30 @@
+// 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) {
+  struct a r;
+  if (c->b) {
+    __goblint_check(strlen(h.b) == 0); // Should also work for write!
+  }
+}
+
+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/22-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;
+}