Optimize and refactor "Hoare" domains

src/analyses/base.ml

@@ -2446,7 +2446,11 @@ struct
         in
         List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
       end
-    | _, _ ->
+    | _, _ when get_bool "sem.unknown_function.spawn" ->
+      (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
+         But here we consider all non-ThreadCrate functions also unknown, so old-style LibraryFunctions access
+         definitions using `Write would still spawn because they are not truly unknown functions (missing from LibraryFunctions).
+         Need this to not have memmove spawn in SV-COMP. *)
       let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in
       let deep_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = true } args in
       let shallow_flist = collect_invalidate ~deep:false (Analyses.ask_of_ctx ctx) ctx.global ctx.local shallow_args in
@@ -2455,6 +2459,7 @@ struct
       let addrs = List.concat_map AD.to_var_may flist in
       if addrs <> [] then M.debug ~category:Analyzer "Spawning functions from unknown function: %a" (d_list ", " d_varinfo) addrs;
       List.filter_map (create_thread None None) addrs
+    | _, _ -> []
 
   let assert_fn ctx e refine =
     (* make the state meet the assertion in the rest of the code *)

src/cdomains/addressDomain.ml

@@ -21,16 +21,32 @@ end
 
 module AddressSet (Idx: IntDomain.Z) =
 struct
-  include Printable.Std (* for default invariant, tag, ... *)
+  module Addr = Lval.NormalLatRepr (Idx)
+  module J = SetDomain.Joined (Addr)
+  (* 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 Addr = Lval.NormalLat (Idx)
-  include HoareDomain.HoarePO (Addr)
+  (* short-circuit with physical equality,
+     makes a difference at long-scale: https://github.com/goblint/analyzer/pull/809#issuecomment-1206174751 *)
+  let equal x y = x == y || equal x y
 
   let widen x y =
     if M.tracing then M.traceli "ad" "widen %a %a\n" pretty x pretty y;
     let r = widen x y in
     if M.tracing then M.traceu "ad" "-> %a\n" pretty r;
     r
+  let join x y =
+    if M.tracing then M.traceli "ad" "join %a %a\n" pretty x pretty y;
+    let r = join x y in
+    if M.tracing then M.traceu "ad" "-> %a\n" pretty r;
+    r
+  let leq x y =
+    if M.tracing then M.traceli "ad" "leq %a %a\n" pretty x pretty y;
+    let r = x == y || leq x y in (* short-circuit with physical equality, not benchmarked *)
+    if M.tracing then M.traceu "ad" "-> %B\n" r;
+    r
 
   type field = Addr.field
   type idx = Idx.t
@@ -41,6 +57,7 @@ struct
   let not_null       = unknown_ptr
   let top_ptr        = of_list Addr.([UnknownPtr; NullPtr])
   let may_be_unknown x = exists (fun e -> e = Addr.UnknownPtr) x
+  let is_element a x = cardinal x = 1 && Addr.equal (choose x) a
   let is_null x      = is_element Addr.NullPtr x
   let is_not_null x  = for_all (fun e -> e <> Addr.NullPtr) x
   let may_be_null x = exists (fun e -> e = Addr.NullPtr) x
@@ -83,30 +100,26 @@ struct
   let to_string x = List.filter_map Addr.to_string (elements x)
 
   (* add an & in front of real addresses *)
-  let short_addr a =
-    match Addr.to_var a with
-    | Some _ -> "&" ^ Addr.show a
-    | None -> Addr.show a
-
-  let pretty () x =
-    try
-      let content = List.map (fun a -> text (short_addr a)) (elements x) in
-      let rec separate x =
-        match x with
-        | [] -> []
-        | [x] -> [x]
-        | (x::xs) -> x ++ (text ", ") :: separate xs
-      in
-      let separated = separate content in
-      let content = List.fold_left (++) nil separated in
-      (text "{") ++ content ++ (text "}")
-    with SetDomain.Unsupported _ -> pretty () x
-
-  let show x : string =
-    try
-      let all_elems : string list = List.map short_addr (elements x) in
-      Printable.get_short_list "{" "}" all_elems
-    with SetDomain.Unsupported _ -> show x
+  module ShortAddr =
+  struct
+    include Addr
+
+    let show a =
+      match Addr.to_var a with
+      | Some _ -> "&" ^ Addr.show a
+      | None -> Addr.show a
+
+    let pretty () a = Pretty.text (show a)
+  end
+
+  include SetDomain.Print (ShortAddr) (
+    struct
+      type nonrec t = t
+      type nonrec elt = elt
+      let elements = elements
+      let iter = iter
+    end
+    )
 
   (*
   let leq = if not fast_addr_sets then leq else fun x y ->
@@ -140,4 +153,16 @@ struct
 
   let meet x y   = merge join meet x y
   let narrow x y = merge (fun x y -> widen x (join x y)) narrow x y
+
+  let meet x y =
+    if M.tracing then M.traceli "ad" "meet %a %a\n" pretty x pretty y;
+    let r = meet x y in
+    if M.tracing then M.traceu "ad" "-> %a\n" pretty r;
+    r
+
+  let narrow x y =
+    if M.tracing then M.traceli "ad" "narrow %a %a\n" pretty x pretty y;
+    let r = narrow x y in
+    if M.tracing then M.traceu "ad" "-> %a\n" pretty r;
+    r
 end

src/cdomains/lval.ml

@@ -41,7 +41,7 @@ struct
     match x, y with
     | `NoOffset , `NoOffset -> true
     | `NoOffset, x
-    | x, `NoOffset -> cmp_zero_offset x = `MustZero (* cannot derive due to this special case *)
+    | x, `NoOffset -> cmp_zero_offset x = `MustZero (* cannot derive due to this special case, special cases not used for AddressDomain any more due to splitting *)
     | `Field (f1,o1), `Field (f2,o2) when CilType.Fieldinfo.equal f1 f2 -> equal o1 o2
     | `Index (i1,o1), `Index (i2,o2) when Idx.equal i1 i2 -> equal o1 o2
     | _ -> false
@@ -61,7 +61,7 @@ struct
   let pretty_diff () (x,y) =
     dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
 
-  let rec hash = function
+  let rec hash = function (* special cases not used for AddressDomain any more due to splitting *)
     | `NoOffset -> 1
     | `Field (f,o) when not (is_first_field f) -> Hashtbl.hash f.fname * hash o + 13
     | `Field (_,o) (* zero offsets need to yield the same hash as `NoOffset! *)
@@ -86,7 +86,7 @@ struct
   let rec compare o1 o2 = match o1, o2 with
     | `NoOffset, `NoOffset -> 0
     | `NoOffset, x
-    | x, `NoOffset when cmp_zero_offset x = `MustZero -> 0 (* cannot derive due to this special case *)
+    | x, `NoOffset when cmp_zero_offset x = `MustZero -> 0 (* cannot derive due to this special case, special cases not used for AddressDomain any more due to splitting *)
     | `Field (f1,o1), `Field (f2,o2) ->
       let c = CilType.Fieldinfo.compare f1 f2 in
       if c=0 then compare o1 o2 else c
@@ -112,8 +112,8 @@ struct
   let rec leq x y =
     match x, y with
     | `NoOffset, `NoOffset -> true
-    | `NoOffset, x -> cmp_zero_offset x <> `MustNonzero
-    | x, `NoOffset -> cmp_zero_offset x = `MustZero
+    | `NoOffset, x -> cmp_zero_offset x <> `MustNonzero (* special case not used for AddressDomain any more due to splitting *)
+    | x, `NoOffset -> cmp_zero_offset x = `MustZero (* special case not used for AddressDomain any more due to splitting *)
     | `Index (i1,o1), `Index (i2,o2) when Idx.leq i1 i2 -> leq o1 o2
     | `Field (f1,o1), `Field (f2,o2) when CilType.Fieldinfo.equal f1 f2 -> leq o1 o2
     | _ -> false
@@ -123,13 +123,13 @@ struct
     match x, y with
     | `NoOffset, `NoOffset -> `NoOffset
     | `NoOffset, x
-    | x, `NoOffset -> (match cop, cmp_zero_offset x with
+    | x, `NoOffset -> (match cop, cmp_zero_offset x with (* special cases not used for AddressDomain any more due to splitting *)
       | (`Join | `Widen), (`MustZero | `MayZero) -> x
       | (`Meet | `Narrow), (`MustZero | `MayZero) -> `NoOffset
       | _ -> raise Lattice.Uncomparable)
     | `Field (x1,y1), `Field (x2,y2) when CilType.Fieldinfo.equal x1 x2 -> `Field (x1, merge cop y1 y2)
     | `Index (x1,y1), `Index (x2,y2) -> `Index (op x1 x2, merge cop y1 y2)
-    | _ -> raise Lattice.Uncomparable
+    | _ -> raise Lattice.Uncomparable (* special case not used for AddressDomain any more due to splitting *)
 
   let join x y = merge `Join x y
   let meet x y = merge `Meet x y
@@ -178,7 +178,7 @@ 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. *)
     | NullPtr (** NULL pointer. *)
@@ -309,6 +309,15 @@ struct
   let arbitrary () = QCheck.always UnknownPtr (* S TODO: non-unknown *)
 end
 
+(** Lvalue lattice.
+
+    Actually a disjoint union of lattices without top or bottom.
+    Lvalues are grouped as follows:
+
+    - Each {!Addr}, modulo precise index expressions in offset, is a sublattice with ordering induced by {!Offset}.
+    - {!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: IntDomain.Z) =
 struct
   include Normal (Idx)
@@ -343,7 +352,11 @@ struct
     | None, a
     | a, None -> a
     | Some a, Some b when a = b -> Some a
-    | Some a, Some b (* when a <> b *) -> raise Lattice.Uncomparable
+    | Some a, Some b (* when a <> b *) ->
+      if GobConfig.get_bool "ana.base.limit-string-addresses" then
+        raise Lattice.BotValue
+      else
+        raise Lattice.Uncomparable
 
   let merge cop x y =
     match x, y with
@@ -363,9 +376,34 @@ struct
   let meet = merge `Meet
   let narrow = merge `Narrow
 
+  include Lattice.NoBotTop
+
   let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
 end
 
+(** Lvalue lattice with sublattice representatives for {!DisjointDomain}. *)
+module NormalLatRepr (Idx: IntDomain.Z) =
+struct
+  include NormalLat (Idx)
+
+  (** Representatives for lvalue sublattices as defined by {!NormalLat}. *)
+  module R: DisjointDomain.Representative with type elt = t =
+  struct
+    include Normal (Idx)
+    type elt = t
+
+    let rec of_elt_offset: Offs.t -> Offs.t =
+      function
+      | `NoOffset -> `NoOffset
+      | `Field (f,o) -> `Field (f, of_elt_offset o)
+      | `Index (_,o) -> `Index (Idx.top (), of_elt_offset o) (* all indices to same bucket *)
+    let of_elt = function
+      | Addr (v, o) -> Addr (v, of_elt_offset o) (* addrs grouped by var and part of offset *)
+      | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> StrPtr None (* all strings together if limited *)
+      | a -> a (* everything else is kept separate, including strings if not limited *)
+  end
+end
+
 module Fields =
 struct
   module F = CilType.Fieldinfo

src/cdomains/valueDomain.ml

@@ -562,11 +562,12 @@ struct
     | (x, `Bot) -> x
     | (`Int x, `Int y) -> (try `Int (ID.widen x y) with IntDomain.IncompatibleIKinds m -> Messages.warn ~category:Analyzer "%s" m; `Top)
     | (`Float x, `Float y) -> `Float (FD.widen x y)
+    (* TODO: symmetric widen, wtf? *)
     | (`Int x, `Address y)
     | (`Address y, `Int x) -> `Address (match ID.to_int x with
-        | Some x when BI.equal BI.zero x -> AD.widen AD.null_ptr y
-        | Some x -> AD.(widen y not_null)
-        | None -> AD.widen y AD.top_ptr)
+        | Some x when BI.equal BI.zero x -> AD.widen AD.null_ptr (AD.join AD.null_ptr y)
+        | Some x -> AD.(widen y (join y not_null))
+        | None -> AD.widen y (AD.join y AD.top_ptr))
     | (`Address x, `Address y) -> `Address (AD.widen x y)
     | (`Struct x, `Struct y) -> `Struct (Structs.widen_with_fct widen_elem x y)
     | (`Union (f,x), `Union (g,y)) -> `Union (match UnionDomain.Field.widen f g with
@@ -647,11 +648,12 @@ struct
     | (x, `Bot) -> x
     | (`Int x, `Int y) -> (try `Int (ID.widen x y) with IntDomain.IncompatibleIKinds m -> Messages.warn ~category:Analyzer "%s" m; `Top)
     | (`Float x, `Float y) -> `Float (FD.widen x y)
+    (* TODO: symmetric widen, wtf? *)
     | (`Int x, `Address y)
     | (`Address y, `Int x) -> `Address (match ID.to_int x with
-        | Some x when BI.equal x BI.zero -> AD.widen AD.null_ptr y
-        | Some x -> AD.(widen y not_null)
-        | None -> AD.widen y AD.top_ptr)
+        | Some x when BI.equal x BI.zero -> AD.widen AD.null_ptr (AD.join AD.null_ptr y)
+        | Some x -> AD.(widen y (join y not_null))
+        | None -> AD.widen y (AD.join y AD.top_ptr))
     | (`Address x, `Address y) -> `Address (AD.widen x y)
     | (`Struct x, `Struct y) -> `Struct (Structs.widen x y)
     | (`Union (f,x), `Union (g,y)) -> `Union (match UnionDomain.Field.widen f g with