AddressSet.meet: Convert offsets to intdomain values to check overlap

src/analyses/base.ml

@@ -344,15 +344,18 @@ struct
           if AD.is_definite x && AD.is_definite y then
             let ax = AD.choose x in
             let ay = AD.choose y in
-            if AD.Addr.equal ax ay then
-              match AD.Addr.to_var ax with
+            let handle_address_is_multiple addr = begin match AD.Addr.to_var addr with
               | Some v when a.f (Q.IsMultiple v) ->
                 None
               | _ ->
                 Some true
-            else
-              (* If they are unequal, it does not matter if the underlying var represents multiple concrete vars or not *)
-              Some false
+              end
+            in
+            match AD.Addr.semantic_equal ax ay with
+            | Some true ->
+              handle_address_is_multiple ax
+            | Some false -> Some false
+            | None -> None
           else
             None
         in

src/cdomains/addressDomain.ml

@@ -20,12 +20,19 @@ end
 
 module AddressSet (Idx: IntDomain.Z) =
 struct
+  module BaseAddr = Lval.BaseAddrRepr (Idx)
   module Addr = Lval.NormalLatRepr (Idx)
-  module J = SetDomain.Joined (Addr)
+  module J = (struct
+    include SetDomain.Joined (Addr)
+    let may_be_equal a b = Option.value (Addr.semantic_equal a b) ~default:true
+  end)
+  module OffsetSplit = DisjointDomain.ProjectiveSetPairwiseMeet (Addr) (J) (Addr.R)
+
   (* module H = HoareDomain.SetEM (Addr) *)
   (* Hoare set for bucket doesn't play well with StrPtr limiting:
      https://github.com/goblint/analyzer/pull/808 *)
-  include DisjointDomain.ProjectiveSet (Addr) (J) (Addr.R)
+  module AddressSet : SetDomain.S with type elt = Addr.t = DisjointDomain.ProjectiveSet (BaseAddr) (OffsetSplit) (BaseAddr.R)
+  include AddressSet
 
   (* short-circuit with physical equality,
      makes a difference at long-scale: https://github.com/goblint/analyzer/pull/809#issuecomment-1206174751 *)

src/cdomains/lval.ml

@@ -18,16 +18,10 @@ sig
   val to_int: t -> IntOps.BigIntOps.t option
 end
 
-module type IdxDomain =
-sig
-  include IdxPrintable
-  include Lattice.S with type t := t
-end
-
-module OffsetPrintable (Idx: IdxPrintable) =
+module Offset (Idx: IdxPrintable) =
 struct
   type t = (fieldinfo, Idx.t) offs
-  include Printable.Std
+  include Printable.StdLeaf
 
   let name () = "offset"
 
@@ -113,9 +107,9 @@ struct
     | `Index(i,o) -> NoOffset (* array domain can not deal with this -> leads to being handeled as access to unknown part *)
 end
 
-module Offset (Idx: IdxDomain) =
+module OffsetLat (Idx: IntDomain.Z) =
 struct
-  include OffsetPrintable (Idx)
+  include Offset (Idx)
 
   let rec leq x y =
     match x, y with
@@ -150,6 +144,43 @@ struct
     | `NoOffset -> `NoOffset
 end
 
+module OffsetLatWithSemanticEqual (Idx: IntDomain.Z) =
+struct
+  include OffsetLat (Idx)
+
+  let ikind () = Cilfacade.ptrdiff_ikind ()
+
+  let offset_to_index_offset typ offs =
+    let idx_of_int x =
+      Idx.of_int (ikind ()) (Z.of_int x)
+    in
+    let rec offset_to_index_offset ?typ offs = match offs with
+      | `NoOffset -> idx_of_int 0
+      | `Field (field, o) ->
+        let field_as_offset = Field (field, NoOffset) in
+        let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset  in
+        let bits_offset = idx_of_int bits_offset in
+        let remaining_offset = offset_to_index_offset ~typ:field.ftype o in
+        Idx.add bits_offset remaining_offset
+      | `Index (x, o) ->
+        match Option.map unrollType typ with
+        | Some TArray(item_typ, _, _) ->
+          let item_size_in_bits = bitsSizeOf item_typ in
+          let item_size_in_bits = idx_of_int item_size_in_bits in
+          let bits_offset = Idx.mul item_size_in_bits x in
+          let remaining_offset = offset_to_index_offset ~typ:item_typ o in
+          Idx.add bits_offset remaining_offset
+        | _ -> Idx.top ()
+    in
+    offset_to_index_offset ~typ offs
+
+  let semantic_equal ~xtyp ~xoffs ~ytyp ~yoffs =
+    let x_index = offset_to_index_offset xtyp xoffs in
+    let y_index = offset_to_index_offset ytyp yoffs in
+    Idx.to_bool (Idx.eq x_index y_index)
+
+end
+
 module type S =
 sig
   type field
@@ -181,14 +212,10 @@ sig
   (** Finds the type of the address location. *)
 end
 
-module Normal (Idx: IdxPrintable) =
+module PreNormal (Offset: Printable.S) =
 struct
-  type field = fieldinfo
-  type idx = Idx.t
-  module Offs = OffsetPrintable (Idx)
-
   type t =
-    | Addr of CilType.Varinfo.t * Offs.t (** Pointer to offset of a variable. *)
+    | Addr of CilType.Varinfo.t * Offset.t (** Pointer to offset of a variable. *)
     | NullPtr (** NULL pointer. *)
     | UnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *)
     | StrPtr of string option (** String literal pointer. [StrPtr None] abstracts any string pointer *)
@@ -202,6 +229,24 @@ struct
         hash x
     | _ -> hash x
 
+  let relift x = x
+
+  let show_str_ptr = function
+    | Some s -> "\"" ^ s ^ "\""
+    | None -> "(unknown string)"
+
+  let show_unknown_ptr = "?"
+
+  let show_null_ptr = "NULL"
+end
+
+module Normal (Idx: IdxPrintable) =
+struct
+  type field = fieldinfo
+  type idx = Idx.t
+  module Offs = Offset (Idx)
+  include PreNormal (Offs)
+
   include Printable.StdLeaf
   let name () = "Normal Lvals"
 
@@ -246,10 +291,9 @@ struct
 
   let show = function
     | Addr (x, o)-> short_addr (x, o)
-    | StrPtr (Some x)   -> "\"" ^ x ^ "\""
-    | StrPtr None -> "(unknown string)"
-    | UnknownPtr -> "?"
-    | NullPtr    -> "NULL"
+    | StrPtr s -> show_str_ptr s
+    | UnknownPtr -> show_unknown_ptr
+    | NullPtr    -> show_null_ptr
 
   include Printable.SimpleShow (
     struct
@@ -258,6 +302,7 @@ struct
     end
     )
 
+
   (* exception if the offset can't be followed completely *)
   exception Type_offset of typ * string
   (* tries to follow o in t *)
@@ -326,10 +371,30 @@ end
     - {!NullPtr} is a singleton sublattice.
     - {!UnknownPtr} is a singleton sublattice.
     - If [ana.base.limit-string-addresses] is enabled, then all {!StrPtr} are together in one sublattice with flat ordering. If [ana.base.limit-string-addresses] is disabled, then each {!StrPtr} is a singleton sublattice. *)
-module NormalLat (Idx: IdxDomain) =
+module NormalLat (Idx: IntDomain.Z) =
 struct
   include Normal (Idx)
-  module Offs = Offset (Idx)
+  module Offs = OffsetLatWithSemanticEqual (Idx)
+
+  (** Semantic equal. [Some true] if definitely equal,  [Some false] if definitely not equal, [None] otherwise *)
+  let semantic_equal x y = match x, y with
+    | Addr (x, xoffs), Addr (y, yoffs) ->
+      if CilType.Varinfo.equal x y then
+        let xtyp = x.vtype in
+        let ytyp = y.vtype in
+        Offs.semantic_equal ~xtyp ~xoffs ~ytyp ~yoffs
+      else
+        Some false
+    | StrPtr None, StrPtr _
+    | StrPtr _, StrPtr None -> Some true
+    | StrPtr (Some a), StrPtr (Some b) -> if a = b then None else Some false
+    | NullPtr, NullPtr -> Some true
+    | UnknownPtr, UnknownPtr
+    | UnknownPtr, Addr _
+    | Addr _, UnknownPtr
+    | UnknownPtr, StrPtr _
+    | StrPtr _, UnknownPtr -> None
+    | _, _ -> Some false
 
   let is_definite = function
     | NullPtr -> true
@@ -390,7 +455,46 @@ struct
 end
 
 (** Lvalue lattice with sublattice representatives for {!DisjointDomain}. *)
-module NormalLatRepr (Idx: IdxDomain) =
+module BaseAddrRepr (Idx: IntDomain.Z) =
+struct
+  include NormalLat (Idx)
+
+  module R: DisjointDomain.Representative with type elt = t =
+  struct
+    type elt = t
+
+    module AnyOffset = Printable.Unit
+    module Address = PreNormal (AnyOffset)
+
+    include Printable.Std
+    include Address
+
+    let name () = "BaseAddrRepr.R"
+
+    let show = function
+      | Addr (v, ()) -> "&" ^ CilType.Varinfo.show v
+      | StrPtr s -> show_str_ptr s
+      | NullPtr -> show_null_ptr
+      | UnknownPtr -> show_unknown_ptr
+
+    include Printable.SimpleShow (
+      struct
+        type nonrec t = t
+        let show = show
+      end
+      )
+
+    let of_elt (x: elt): t = match x with
+      | Addr (v, o) -> Addr (v, ())
+      | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> StrPtr None (* all strings together if limited *)
+      | StrPtr x -> StrPtr x (* everything else is kept separate, including strings if not limited *)
+      | NullPtr -> NullPtr
+      | UnknownPtr -> UnknownPtr
+  end
+end
+
+(** Lvalue lattice with sublattice representatives for {!DisjointDomain}. *)
+module NormalLatRepr (Idx: IntDomain.Z) =
 struct
   include NormalLat (Idx)
 

src/cdomains/valueDomain.ml

@@ -3,7 +3,7 @@ open Pretty
 open PrecisionUtil
 
 include PreValueDomain
-module Offs = Lval.Offset (IndexDomain)
+module Offs = Lval.OffsetLat (IndexDomain)
 module M = Messages
 module GU = Goblintutil
 module Q = Queries

src/domains/disjointDomain.ml

@@ -27,7 +27,9 @@ end
     Common choices for [B] are {!SetDomain.Joined} and {!HoareDomain.SetEM}.
 
     Handles {!Lattice.BotValue} from [B]. *)
-module ProjectiveSet (E: Printable.S) (B: SetDomain.S with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t =
+module ProjectiveSet (E: Printable.S) (B: SetDomain.S with type elt = E.t) (R: Representative with type elt = E.t)
+(* : SetDomain.S with type elt = E.t *)
+=
 struct
   type elt = E.t
 
@@ -176,6 +178,51 @@ struct
   let disjoint m1 m2 = is_empty (inter m1 m2) (* TODO: optimize? *)
 end
 
+module type MayEqualSetDomain =
+sig
+  include SetDomain.S
+  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
+  include ProjectiveSet (E) (B) (R)
+
+  let fold_buckets a b f s =
+    B.fold (fun e1 acc ->
+      B.fold (fun e2 acc ->
+          f e1 e2 acc
+        ) b acc
+      ) a s
+
+  module S = BatSet.Make(E)
+  let meet m1 m2 =
+    let collect_equal a b =
+      let add_equal e1 e2 (s1, s2) =
+        if B.may_be_equal e1 e2 then
+          S.add e1 s1, S.add e2 s2
+        else
+          s1, s2
+      in
+      fold_buckets a b add_equal (S.empty, S.empty)
+    in
+    let inner_fold key b key2 b2 acc =
+      let s1, s2 = collect_equal b b2 in
+      let add_entries key s m =
+        S.fold (fun e macc ->
+          M.add key (B.singleton e) m
+        ) s m
+      in
+      acc
+        |> add_entries key s1
+        |> add_entries key2 s2
+    in
+    let outer_fold key b acc =
+      M.fold (inner_fold key b) m2 acc
+    in
+    M.fold outer_fold m1 (M.empty ())
+
+end
+
 (** {2 By congruence} *)
 
 (** Buckets defined by congruence. *)