Merge branch 'master' into generic-spec-lifters

Author: sim642

src/cdomain/value/cdomains/int/defExcDomain.ml

@@ -299,15 +299,15 @@ struct
       let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else  S.empty () in
       norm ik @@ (`Excluded (ex, r))
 
-  let to_bitfield ik x = 
-    match x with 
-    | `Definite c -> (Z.lognot c, c) 
-    | _ when Cil.isSigned ik -> 
-      let one_mask = Z.lognot Z.zero in 
+  let to_bitfield ik x =
+    match x with
+    | `Definite c -> (Z.lognot c, c)
+    | _ when Cil.isSigned ik ->
+      let one_mask = Z.lognot Z.zero in
       (one_mask, one_mask)
-    | _ -> 
-      let one_mask = Z.lognot Z.zero in 
-      let ik_mask = snd (Size.range ik) in 
+    | _ ->
+      let one_mask = Z.lognot Z.zero in
+      let ik_mask = snd (Size.range ik) in
       (one_mask, ik_mask)
 
   let starting ?(suppress_ovwarn=false) ikind x =
@@ -333,12 +333,9 @@ struct
     | `Bot -> None
 
   let apply_range f r = (* apply f to the min/max of the old range r to get a new range *)
-    (* If the Int64 might overflow on us during computation, we instead go to top_range *)
-    match R.minimal r, R.maximal r with
-    | _ ->
-      let rf m = (size % Size.min_for % f) (m r) in
-      let r1, r2 = rf Exclusion.min_of_range, rf Exclusion.max_of_range in
-      R.join r1 r2
+    let rf m = (size % Size.min_for % f) (m r) in
+    let r1, r2 = rf Exclusion.min_of_range, rf Exclusion.max_of_range in
+    R.join r1 r2
 
   (* Default behaviour for unary operators, simply maps the function to the
    * DefExc data structure. *)
@@ -542,8 +539,8 @@ struct
 
   let refine_with_congruence ik a b = a
 
-  let refine_with_bitfield ik x (z,o) = 
-    match BitfieldDomain.Bitfield.to_int (z,o) with 
+  let refine_with_bitfield ik x (z,o) =
+    match BitfieldDomain.Bitfield.to_int (z,o) with
     | Some y ->
       meet ik x (`Definite y)
     | _ ->

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

@@ -206,6 +206,9 @@ end
 (** Lifts a [Spec] so that the context is [Hashcons]d. *)
 module HashconsContextLifter = ContextLifter (Printable.HConsed)
 
+(** Lifts a [Spec] so that the context is [HashCached]. *)
+module HashCachedContextLifter = ContextLifter (Printable.HashCached)
+
 (* 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