HashCachedContextLifter: Introduce the lifter and the option

Using hashcache on contexes makes a big difference in memory usage (churn) and a reasonable improvement on runtime when HashConsing is disabled. This is particularly important for the upcoming parallel solvers

Author: arkocal

src/common/domains/printable.ml

@@ -176,6 +176,7 @@ struct
 
   let lift m = {m; lazy_hash = LazyHash.make m}
   let unlift {m; _} = m
+  let relift x = x
 
   let lift_f f x = f (unlift x)
   let lift_f' f x = lift @@ lift_f f x

src/config/options.schema.json

@@ -513,6 +513,13 @@
               "type": "boolean",
               "default": true
             },
+            "hashcached": {
+              "title": "ana.opt.hashcached",
+              "description":
+                "Should we try to save memory and speed up equality by caching hashes of contexts? This is useful when hashconsing is off",
+              "type": "boolean",
+              "default": false
+            },
             "equal": {
               "title": "ana.opt.equal",
               "description":

src/framework/control.ml

@@ -28,6 +28,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
+      |> lift (get_bool "ana.opt.hashcached") (module HashCachedContextLifter)
       |> lift arg_enabled (module HashconsLifter)
       |> lift arg_enabled (module WitnessConstraints.PathSensitive3)
       |> lift (not arg_enabled) (module PathSensitive2)

src/lifters/specLifters.ml

@@ -180,6 +180,88 @@ struct
   let event man e oman = S.event (conv man) e (conv oman)
 end
 
+(** Lifts a [Spec] so that the context is [HashCached]. *)
+module HashCachedContextLifter (S:Spec)
+  : Spec with module D = S.D
+          and module G = S.G
+          and module C = Printable.HashCached (S.C)
+=
+struct
+  module D = S.D
+  module G = S.G
+  module C = Printable.HashCached (S.C)
+  module V = S.V
+  module P = S.P
+
+  let name () = S.name () ^" context hashcached"
+
+  type marshal = S.marshal 
+  let init = S.init
+  let finalize = S.finalize
+
+  let startstate = S.startstate
+  let exitstate  = S.exitstate
+  let morphstate = S.morphstate
+
+  let conv man =
+    { man with context = (fun () -> C.unlift (man.context ())) }
+
+  let context man fd = C.lift % S.context (conv man) fd
+  let startcontext () = C.lift @@ S.startcontext ()
+
+  let sync man reason =
+    S.sync (conv man) reason
+
+  let query man (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | Queries.IterPrevVars f ->
+      let g i (n, c, j) e = f i (n, Obj.repr (C.lift (Obj.obj c)), j) e in
+      S.query (conv man) (Queries.IterPrevVars g)
+    | _ -> S.query (conv man) q
+
+  let assign man lv e =
+    S.assign (conv man) lv e
+
+  let vdecl man v =
+    S.vdecl (conv man) v
+
+  let branch man e tv =
+    S.branch (conv man) e tv
+
+  let body man f =
+    S.body (conv man) f
+
+  let return man r f =
+    S.return (conv man) r f
+
+  let asm man =
+    S.asm (conv man)
+
+  let skip man =
+    S.skip (conv man)
+
+  let enter man r f args =
+    S.enter (conv man) r f args
+
+  let special man r f args =
+    S.special (conv man) r f args
+
+  let combine_env man r fe f args fc es f_ask =
+    S.combine_env (conv man) r fe f args (Option.map C.unlift fc) es f_ask
+
+  let combine_assign man r fe f args fc es f_ask =
+    S.combine_assign (conv man) r fe f args (Option.map C.unlift fc) es f_ask
+
+  let threadenter man ~multiple lval f args =
+    S.threadenter (conv man) ~multiple lval f args
+
+  let threadspawn man ~multiple lval f args fman =
+    S.threadspawn (conv man) ~multiple lval f args (conv fman)
+
+  let paths_as_set man = S.paths_as_set (conv man)
+  let event man e oman = S.event (conv man) e (conv oman)
+end
+
 (* see option ana.opt.equal *)
 module OptEqual (S: Spec) = struct
   module D = struct include S.D let equal x y = x == y || equal x y end