Merge pull request #1690 from arkocal/hashcachedcontextlifter

HashCachedContextLifter: Introduce the lifter and the option

Author: sim642

src/common/domains/printable.ml

@@ -26,7 +26,7 @@ sig
   (* For hashconsing together with incremental we need to re-hashcons old values.
    * For HashconsLifter.D this is done on any lattice operation, so we can replace x with `join bot x` to hashcons it again and get a new tag for it.
    * For HashconsLifter.C we call hashcons only in `context` which is in Analyses.Spec but not in Analyses.GlobConstrSys, i.e. not visible to the solver. *)
-  (* The default for this should be identity, except for HConsed below where we want to have the side-effect and return a value with the updated tag. *)
+  (* The default for functors should pass the call to their argument modules, except for HConsed below where we want to have the side-effect and return a value with the updated tag. *)
   val relift: t -> t
 end
 
@@ -162,39 +162,40 @@ struct
   let arbitrary () = QCheck.map ~rev:unlift lift (Base.arbitrary ())
 end
 
-module HashCached (M: S) =
+module HashCached (Base: S) =
 struct
-  module LazyHash = LazyEval.Make (struct type t = M.t type result = int let eval = M.hash end)
+  module LazyHash = LazyEval.Make (struct type t = Base.t type result = int let eval = Base.hash end)
 
-  let name () = "HashCached " ^ M.name ()
+  let name () = "HashCached " ^ Base.name ()
 
   type t =
     {
-      m: M.t;
+      m: Base.t;
       lazy_hash: LazyHash.t;
     }
 
   let lift m = {m; lazy_hash = LazyHash.make m}
   let unlift {m; _} = m
+  let relift x = lift @@ Base.relift x.m
 
   let lift_f f x = f (unlift x)
   let lift_f' f x = lift @@ lift_f f x
   let lift_f2 f x y = f (unlift x) (unlift y)
   let lift_f2' f x y = lift @@ lift_f2 f x y
 
-  let equal = lift_f2 M.equal
-  let compare = lift_f2 M.compare
+  let equal = lift_f2 Base.equal
+  let compare = lift_f2 Base.compare
   let hash x = LazyHash.force x.lazy_hash
-  let show = lift_f M.show
+  let show = lift_f Base.show
 
-  let pretty () = lift_f (M.pretty ())
+  let pretty () = lift_f (Base.pretty ())
 
-  let printXml f = lift_f (M.printXml f)
-  let to_yojson = lift_f (M.to_yojson)
+  let printXml f = lift_f (Base.printXml f)
+  let to_yojson = lift_f (Base.to_yojson)
 
-  let arbitrary () = QCheck.map ~rev:unlift lift (M.arbitrary ())
+  let arbitrary () = QCheck.map ~rev:unlift lift (Base.arbitrary ())
 
-  let tag = lift_f M.tag
+  let tag = lift_f Base.tag
 end
 
 

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