For elements in the same bucket, perform meet

Author: michael-schwarz

src/cdomain/value/cdomains/addressDomain.ml

@@ -110,11 +110,6 @@ 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
@@ -183,7 +178,6 @@ 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,10 +82,6 @@ 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,7 +182,6 @@ 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: Lattice.S) (B: MayEqualSetDomain with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t = struct
@@ -192,15 +191,16 @@ module ProjectiveSetPairwiseMeet (E: Lattice.S) (B: MayEqualSetDomain with type
     let meet_buckets b1 b2 acc =
       B.fold (fun e1 acc ->
           B.fold (fun e2 acc ->
-              if B.amenable_to_meet e1 e2 then
+              (* If they have the same representative, we use the normal meet within this bucket *)
+              if R.equal (R.of_elt e1) (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 "amenable_to_meet %a %a returned true, but meet throws!" E.pretty e1 E.pretty e2)
+                  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