Add amenable_to_meet and test for it

Author: michael-schwarz

src/cdomain/value/cdomains/addressDomain.ml

@@ -110,6 +110,10 @@ struct
     | StrPtr _, UnknownPtr -> None
     | _, _ -> Some false
 
+  let amenable_to_meet x y = match x,y with
+    | StrPtr _, StrPtr _ -> 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 +182,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

@@ -80,8 +80,11 @@ sig
 
     val semantic_equal: t -> t -> bool option
     (** 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;
+}