Optimize and refactor "Hoare" domains

src/cdomains/addressDomain.ml

@@ -24,13 +24,79 @@ struct
   include Printable.Std (* for default invariant, tag, ... *)
 
   module Addr = Lval.NormalLat (Idx)
-  include HoareDomain.HoarePO (Addr)
+  module R =
+  struct
+    include Addr
+    type elt = Addr.t
+
+    let rec of_elt_offset: Offs.t -> Offs.t =
+      function
+      | `NoOffset -> `NoOffset
+      | `Field (f,o) when not (Offs.is_first_field f) -> `Field (f, of_elt_offset o)
+      | `Field (_,o) (* zero offsets need to yield the same hash as `NoOffset! *)
+      | `Index (_,o) -> of_elt_offset o (* index might become top during fp -> might be zero offset *)
+      (* function
+      | `NoOffset -> `NoOffset
+      | `Index (_, o') as o when Offs.cmp_zero_offset o <> `MustNonzero ->
+        of_elt_offset o'
+      | `Index (i, o') -> `Index (Idx.top (), of_elt_offset o')
+      | `Field (_, o') as o when Offs.cmp_zero_offset o <> `MustNonzero ->
+        of_elt_offset o'
+      | `Field (f, o') -> `Field (f, of_elt_offset o') (* incorrect *) *)
+      (* function _ -> `NoOffset (* very crude *) *)
+    let of_elt = function
+      | Addr (v, o) -> Addr (v, of_elt_offset o)
+      | a -> a
+  end
+  module R2 =
+  struct
+    include IntDomain.Integers (IntOps.NIntOps)
+    type elt = Addr.t
+    let of_elt = Addr.hash
+  end
+  module C =
+  struct
+    type t = Addr.t
+    let cong x y =
+      (* ignore (Pretty.eprintf "cong %a %a\n" Addr.pretty x Addr.pretty y); *)
+      if M.tracing then M.tracei "ad" "cong %a %a\n" Addr.pretty x Addr.pretty y;
+      (* begin match Addr.to_var_offset y with
+        | Some (_, `Index (i, `NoOffset)) when Idx.to_int i = Some (Z.of_int 2) -> failwith "THIS"
+        | _ -> ()
+      end; *)
+      let r = match Addr.join x y with
+      | exception Lattice.Uncomparable -> false
+      | _ -> true
+      in
+      if M.tracing then M.traceu "ad" "-> %B\n" r;
+      r
+  end
+  module RC =
+  struct
+    include R
+    include C
+  end
+  module J = SetDomain.Joined (Addr)
+  module H = HoareDomain.Set2 (Addr)
+  (* include SensitiveDomain.Pairwise (Addr) (H) (C) *)
+  include SensitiveDomain.Combined (Addr) (H) (RC)
+  (* include HoareDomain.HoarePO (Addr) *)
 
   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 = leq x y in
+    if M.tracing then M.traceu "ad" "-> %B\n" r;
+    r
 
   type field = Addr.field
   type idx = Idx.t
@@ -41,6 +107,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
@@ -140,4 +207,10 @@ 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 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

@@ -112,8 +112,7 @@ 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 -> true
     | `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,10 +122,9 @@ struct
     match x, y with
     | `NoOffset, `NoOffset -> `NoOffset
     | `NoOffset, x
-    | x, `NoOffset -> (match cop, cmp_zero_offset x with
-      | (`Join | `Widen), (`MustZero | `MayZero) -> x
-      | (`Meet | `Narrow), (`MustZero | `MayZero) -> `NoOffset
-      | _ -> raise Lattice.Uncomparable)
+    | x, `NoOffset -> (match cop with
+      | `Join | `Widen -> x
+      | `Meet | `Narrow -> `NoOffset)
     | `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
@@ -329,6 +327,8 @@ 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
 

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

src/domains/hoareDomain.ml

@@ -119,8 +119,6 @@ struct
   let union x y = join x y
   let iter f m = Map.iter (fun _ -> List.iter f) m
 
-  let is_element e m = Map.cardinal m = 1 && snd (Map.choose m) = [e]
-
   (* Lattice *)
   let bot () = Map.empty
   let is_bot = Map.is_empty
@@ -167,6 +165,7 @@ struct
     List.iter (E.printXml f) (elements x);
     BatPrintf.fprintf f "</set>\n</value>\n"
 end
+[@@deprecated]
 
 
 module type SetS =
@@ -194,7 +193,7 @@ struct
   let narrow = product_bot (fun x y -> if B.leq y x then B.narrow x y else x)
 
   let add x a = if mem x a then a else add x a (* special mem! *)
-  let remove x a = unsupported "Set.remove"
+  let remove x a = filter (fun y -> not (B.leq y x)) a
   let join a b = union a b |> reduce
   let union _ _ = unsupported "Set.union"
   let inter _ _ = unsupported "Set.inter"
@@ -338,3 +337,36 @@ struct
         (cardinal s2)
     end
 end
+
+
+module Set2 (E: Lattice.S): SetDomain.S with type elt = E.t =
+struct
+  module H = Set (E)
+  include H
+
+
+  (* version of widen which doesn't use E.bot *)
+  let product_widen (op: elt -> elt -> elt option) a b = (* assumes b to be bigger than a *)
+  let xs,ys = elements a, elements b in
+  List.concat_map (fun x -> List.filter_map (fun y -> op x y) ys) xs |> fun x -> join b (of_list x)
+  let widen = product_widen (fun x y -> if E.leq x y then Some (E.widen x y) else None)
+
+  (* widen is actually extrapolation operator, so define connector-based widening instead *)
+  let leq_em s1 s2 =
+    is_bot s1 || leq s1 s2 && for_all (fun e2 -> exists (fun e1 -> E.leq e1 e2) s1) s2
+  let join_em s1 s2 =
+    join s1 s2
+    |> elements
+    |> BatList.reduce E.join
+    |> singleton
+
+  let widen s1 s2 =
+    assert (leq s1 s2);
+    let s2' =
+      if leq_em s1 s2 then
+        s2
+      else
+        join_em s1 s2
+    in
+    widen s1 s2'
+end

src/domains/lattice.ml

@@ -60,6 +60,15 @@ end
 module Unit = UnitConf (struct let name = "()" end)
 
 
+module NoBotTop =
+struct
+  let top () = raise TopValue
+  let is_top _ = false
+  let bot () = raise BotValue
+  let is_bot _ = false
+end
+
+
 module Fake (Base: Printable.S) =
 struct
   include Base
@@ -70,10 +79,7 @@ struct
   let meet x y =
     if equal x y then x else raise (Unsupported "fake meet")
   let narrow = meet
-  let top () = raise (Unsupported "fake top")
-  let is_top _ = false
-  let bot () = raise (Unsupported "fake bot")
-  let is_bot _ = false
+  include NoBotTop
 
   let pretty_diff () (x,y) =
     Pretty.dprintf "%s: %a not equal %a" (Base.name ()) pretty x pretty y