From 3b8a9bef5379cd458b2a083baabbdbf11e4a7dfc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 22 Jul 2024 11:16:24 +0200
Subject: [PATCH] [Hptmap] Simplifies functor use: no compositional bool by
default.
Complete functor Make_with_compositional_bool takes an additional module
for the compositional boolean.
Functor Make simply uses Comp_unused by default.
---
src/kernel_services/abstract_interp/base.ml | 2 +-
src/kernel_services/abstract_interp/lmap.ml | 9 +--
.../abstract_interp/lmap_bitwise.ml | 2 +-
.../abstract_interp/locations.ml | 9 +--
src/kernel_services/analysis/stmts_graph.ml | 1 -
src/libraries/utils/hptmap.ml | 28 +++++----
src/libraries/utils/hptmap.mli | 60 ++++++++++---------
src/libraries/utils/hptset.ml | 2 +-
.../eva/domains/cvalue/builtins_malloc.ml | 3 +-
src/plugins/eva/domains/equality/equality.ml | 2 +-
.../eva/domains/gauges/gauges_domain.ml | 4 +-
src/plugins/eva/domains/hcexprs.ml | 4 +-
.../domains/multidim/abstract_structure.ml | 3 +-
.../eva/domains/multidim/multidim_domain.ml | 2 +-
src/plugins/eva/domains/octagons.ml | 10 ++--
src/plugins/eva/domains/simple_memory.ml | 2 +-
src/plugins/eva/domains/symbolic_locs.ml | 2 +-
src/plugins/eva/domains/traces_domain.ml | 2 +-
src/plugins/from/from_compute.ml | 2 +-
src/plugins/impact/pdg_aux.ml | 6 +-
src/plugins/pdg/pdg_types/pdgTypes.ml | 2 +-
21 files changed, 79 insertions(+), 78 deletions(-)
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index b5f98f4b825..0a87aa8f1fd 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -555,7 +555,7 @@ let of_string_exp e =
module SetLattice = Make_Hashconsed_Lattice_Set(Base)(Hptset)
module BMap =
- Hptmap.Make (Base) (Base) (Hptmap.Comp_unused)
+ Hptmap.Make (Base) (Base)
(struct
let initial_values = []
let dependencies = [ Ast.self ]
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 8c8b3f3c20e..54240aad4fa 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -88,17 +88,18 @@ struct
end
module Comp = struct
- let f _base offsetmap = Offsetmap.cardinal_zero_or_one offsetmap
+ let empty = true
+ let leaf _base offsetmap = Offsetmap.cardinal_zero_or_one offsetmap
let compose a b = a && b
- let e = true
end
- module Hptmap_Info = struct
+ module Info = struct
let initial_values = []
let dependencies = [ Ast.self ]
end
- module M = Hptmap.Make (Base.Base) (Offsetmap) (Comp) (Hptmap_Info)
+ module M =
+ Hptmap.Make_with_compositional_bool (Base.Base) (Offsetmap) (Comp) (Info)
let () = Ast.add_monotonic_state M.self
include M
diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.ml b/src/kernel_services/abstract_interp/lmap_bitwise.ml
index ffc2bafe92e..04ca90b91a1 100644
--- a/src/kernel_services/abstract_interp/lmap_bitwise.ml
+++ b/src/kernel_services/abstract_interp/lmap_bitwise.ml
@@ -145,7 +145,7 @@ struct
let initial_values = []
let dependencies = [ Ast.self ]
end
- include Hptmap.Make (Base.Base) (LOffset) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (Base.Base) (LOffset) (Hptmap_Info)
let () = Ast.add_monotonic_state self
(* We override [add] so that the map is canonical: no key should be
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index af174d7cd4d..a47a5d2cbee 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -46,9 +46,9 @@ end
are included in it. Said otherwise, we do not consider the cardinality
of the concretization, but instead the one of the Ocaml datastructure. *)
module Comp_exact = struct
- let e = true (* corresponds to bottom *)
+ let empty = true (* corresponds to bottom *)
- let f _b v = Ival.cardinal_zero_or_one v
+ let leaf _b v = Ival.cardinal_zero_or_one v
(* on Ival, both forms of cardinal coincide *)
let compose _ _ = false
@@ -60,7 +60,8 @@ end
module Location_Bytes = struct
module M = struct
- include Hptmap.Make (Base.Base) (Ival) (Comp_exact) (Hptmap_Info)
+ include Hptmap.Make_with_compositional_bool
+ (Base.Base) (Ival) (Comp_exact) (Hptmap_Info)
let shape x = x
end
let () = Ast.add_monotonic_state M.self
@@ -376,7 +377,7 @@ module Zone = struct
let dependencies = [ Ast.self ]
end
- module M = Hptmap.Make (Base.Base) (Int_Intervals) (Hptmap.Comp_unused) (Info)
+ module M = Hptmap.Make (Base.Base) (Int_Intervals) (Info)
let () = Ast.add_monotonic_state M.self
let clear_caches = M.clear_caches
diff --git a/src/kernel_services/analysis/stmts_graph.ml b/src/kernel_services/analysis/stmts_graph.ml
index bd7e0df01be..f93858ebf92 100644
--- a/src/kernel_services/analysis/stmts_graph.ml
+++ b/src/kernel_services/analysis/stmts_graph.ml
@@ -35,7 +35,6 @@ struct
module HptmapStmtBool = Hptmap.Make
(Cil_datatype.Stmt_Id)
(struct include Datatype.Bool let pretty_debug = pretty end)
- (Hptmap.Comp_unused)
(struct
let initial_values = []
let dependencies = [ Ast.self ]
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index 9bc3422c355..a4678edd33b 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -93,13 +93,6 @@ struct
end
type tag = Tag_comp.t
-module Comp_unused =
-struct
- let e = false
- let f _ _ = false
- let compose _ _ = false
-end
-
(* A tree is either empty, or a leaf node, containing both
the integer key and a piece of data, or a binary node.
Each binary node carries two integers. The first one is
@@ -592,8 +585,8 @@ module type Compositional_bool = sig
type key
type v
- val e : bool
- val f : key -> v -> bool
+ val empty : bool
+ val leaf : key -> v -> bool
val compose : bool -> bool -> bool
end
@@ -604,7 +597,7 @@ module type Info = sig
val dependencies : State.t list
end
-module Make
+module Make_with_compositional_bool
(Key: Id_Datatype)
(V : V)
(Compositional_bool : Compositional_bool with type key := Key.t
@@ -649,7 +642,7 @@ struct
let compositional_bool t =
match t with
- | Empty -> Compositional_bool.e
+ | Empty -> Compositional_bool.empty
| Leaf (_,_,tc)
| Branch (_,_,_,_,tc) -> Tag_comp.get_comp tc
@@ -659,7 +652,7 @@ struct
let initial_values =
let tc k v =
- let b = Compositional_bool.f k v in
+ let b = Compositional_bool.leaf k v in
let tag = !current_tag in
incr current_tag;
Tag_comp.encode tag b
@@ -754,7 +747,7 @@ struct
(* The test k < p+m and the implementation of [highest_bit] do not work
with negative keys. *)
assert (Key.id k >= 0);
- let b = Compositional_bool.f k v in
+ let b = Compositional_bool.leaf k v in
let tag = !current_tag in
let new_tr = Leaf (k, v, Tag_comp.encode tag b) in
let result = PatriciaHashconsTbl.merge new_tr in
@@ -1438,6 +1431,15 @@ struct
let equal_subtree = equal
end
+module Comp_unused = struct
+ let empty = false
+ let leaf _ _ = false
+ let compose _ _ = false
+end
+
+module Make (Key: Id_Datatype) (V : V) (Info: Info with type key := Key.t
+ and type v := V.t)
+ = Make_with_compositional_bool (Key) (V) (Comp_unused) (Info)
(*
Local Variables:
diff --git a/src/libraries/utils/hptmap.mli b/src/libraries/utils/hptmap.mli
index 2c80736a6b6..725c205712d 100644
--- a/src/libraries/utils/hptmap.mli
+++ b/src/libraries/utils/hptmap.mli
@@ -32,12 +32,6 @@ module type Id_Datatype = sig
[equal k1 k2 ==> id k1 = id k2] *)
end
-(** Values stored in the map *)
-module type V = sig
- include Datatype.S
- val pretty_debug: t Pretty_utils.formatter
-end
-
(** This functor builds {!Hptmap_sig.Shape} for maps indexed by keys [Key],
which contains all functions on hptmap that do not create or modify maps. *)
module Shape (Key : Id_Datatype): sig
@@ -45,21 +39,10 @@ module Shape (Key : Id_Datatype): sig
type 'a t = 'a map
end
-(** A optional boolean information is maintained for each tree, by composing the
- boolean on the subtrees and the value information present on each leaf.
- Use {!Comp_unused} for a default implementation. *)
-module type Compositional_bool = sig
- type key
- type v
-
- val e : bool
- (** Value for the empty tree *)
-
- val f : key -> v -> bool
- (** Value for a leaf *)
-
- val compose : bool -> bool -> bool
- (** Composition of the values of two subtrees *)
+(** Values stored in the map *)
+module type V = sig
+ include Datatype.S
+ val pretty_debug: t Pretty_utils.formatter
end
(** Required information for the correctness of the hptmaps. *)
@@ -83,8 +66,6 @@ end
module Make
(Key : Id_Datatype)
(V : V)
- (_ : Compositional_bool with type key := Key.t
- and type v := V.t)
(_ : Info with type key := Key.t
and type v := V.t)
: Hptmap_sig.S with type key = Key.t
@@ -92,14 +73,37 @@ module Make
and type 'v map = 'v Shape(Key).map
and type prefix = prefix
-(** Default implementation for the [Compositional_bool] argument of the functor
- {!Make}. To be used when no interesting compositional bit can be computed. *)
-module Comp_unused : sig
- val e : bool
- val f : 'a -> 'b -> bool
+(** An additional boolean information is computed for each tree, by composing
+ the boolean on the subtrees and the value information on each leaf. *)
+module type Compositional_bool = sig
+ type key
+ type v
+
+ val empty : bool
+ (** Value for the empty tree *)
+
+ val leaf : key -> v -> bool
+ (** Value for a leaf *)
+
val compose : bool -> bool -> bool
+ (** Composition of the values of two subtrees *)
end
+(** This functor builds the complete module of maps indexed by keys [Key]
+ to values [V], with an additional boolean information maintained for
+ each tree. *)
+module Make_with_compositional_bool
+ (Key : Id_Datatype)
+ (V : V)
+ (_ : Compositional_bool with type key := Key.t
+ and type v := V.t)
+ (_ : Info with type key := Key.t
+ and type v := V.t)
+ : Hptmap_sig.S with type key = Key.t
+ and type v = V.t
+ and type 'v map = 'v Shape(Key).map
+ and type prefix = prefix
+
(*
Local Variables:
compile-command: "make -C .."
diff --git a/src/libraries/utils/hptset.ml b/src/libraries/utils/hptset.ml
index 59a1dd0955c..28c3164935d 100644
--- a/src/libraries/utils/hptset.ml
+++ b/src/libraries/utils/hptset.ml
@@ -120,7 +120,7 @@ module Make
let dependencies = Info.dependencies
end
- module M = Hptmap.Make (X) (Unit) (Hptmap.Comp_unused) (Hptmap_Info)
+ module M = Hptmap.Make (X) (Unit) (Hptmap_Info)
include M
let add k s = add k () s
diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.ml b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
index 8c6155ad86b..b3be407a16d 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
@@ -42,8 +42,7 @@ module Hptmap_Info = struct
let dependencies = [ Ast.self ]
end
-module Base_hptmap =
- Hptmap.Make (Base.Base) (Callstack) (Hptmap.Comp_unused) (Hptmap_Info)
+module Base_hptmap = Hptmap.Make (Base.Base) (Callstack) (Hptmap_Info)
module Dynamic_Alloc_Bases =
State_builder.Ref
diff --git a/src/plugins/eva/domains/equality/equality.ml b/src/plugins/eva/domains/equality/equality.ml
index 6f1de9bfc41..7d85984fcb2 100644
--- a/src/plugins/eva/domains/equality/equality.ml
+++ b/src/plugins/eva/domains/equality/equality.ml
@@ -98,7 +98,7 @@ module Set = struct
let initial_values = []
let dependencies = [ Ast.self ]
end
- include Hptmap.Make (HCE) (Data) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (HCE) (Data) (Hptmap_Info)
let find_option elt map =
try
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index fc759a3f6e6..a082f405044 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -285,7 +285,7 @@ module G = struct
*)
module MV = struct
- include Hptmap.Make (Base) (Cvalue.V) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (Base) (Cvalue.V) (Hptmap_Info)
(* This function computes a pointwise union on two MVs assumed to have
disjoint set of keys. *)
@@ -322,7 +322,7 @@ module G = struct
are not incremented in one inner, but only in outemost one. *)
module MC = struct
- include Hptmap.Make (Base) (Bounds) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (Base) (Bounds) (Hptmap_Info)
(* This function computes a pointwise union on two MCs assumed to have
disjoint set of keys. *)
diff --git a/src/plugins/eva/domains/hcexprs.ml b/src/plugins/eva/domains/hcexprs.ml
index d34f7bdfa6d..951d897535f 100644
--- a/src/plugins/eva/domains/hcexprs.ml
+++ b/src/plugins/eva/domains/hcexprs.ml
@@ -162,7 +162,7 @@ module HCEToZone = struct
let cache_prefix = "Value.Symbolic_exprs.K2Z"
- include Hptmap.Make (HCE) (Locations.Zone) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (HCE) (Locations.Zone) (Hptmap_Info)
let is_included =
let cache_name = cache_prefix ^ ".is_included" in
@@ -202,7 +202,7 @@ end
module BaseToHCESet = struct
- include Hptmap.Make (Base.Base) (HCESet) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (Base.Base) (HCESet) (Hptmap_Info)
let cache_prefix = "Value.Symbolic_exprs.B2K"
diff --git a/src/plugins/eva/domains/multidim/abstract_structure.ml b/src/plugins/eva/domains/multidim/abstract_structure.ml
index 3b00b1ddb72..eac548f2d77 100644
--- a/src/plugins/eva/domains/multidim/abstract_structure.ml
+++ b/src/plugins/eva/domains/multidim/abstract_structure.ml
@@ -83,8 +83,7 @@ struct
let initial_values = []
let dependencies = [ Ast.self ]
end
- module FieldMap =
- Hptmap.Make (Field) (Values) (Hptmap.Comp_unused) (Hptmap_Info)
+ module FieldMap = Hptmap.Make (Field) (Values) (Hptmap_Info)
type t = {
padding: Bit.t;
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 5a27426cb27..63db3c5dc72 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -346,7 +346,7 @@ struct
module BaseMap =
struct
- include Hptmap.Make (Base.Base) (V) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (Base.Base) (V) (Hptmap_Info)
let find_or_top (state : t) (b : Base.t) =
try find b state with Not_found -> V.top
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index 30367800d64..bd82bcbad8a 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -617,7 +617,7 @@ end
(* Maps linking pairs of variables (X, Y) to intervals for X+Y and X-Y. *)
module Octagons = struct
- include Hptmap.Make (Pair) (Diamond) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (Pair) (Diamond) (Hptmap_Info)
let internal_join = join
@@ -738,7 +738,7 @@ module Relations = struct
include Hptmap.Make (Variable)
(struct include VarSet let pretty_debug = pretty end)
- (Hptmap.Comp_unused) (Hptmap_Info)
+ (Hptmap_Info)
let inter =
let cache = Hptmap_sig.PersistentCache "Octagons.Relations.inter" in
@@ -779,7 +779,7 @@ end
module Intervals = struct
- include Hptmap.Make (Variable) (Ival) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (Variable) (Ival) (Hptmap_Info)
let internal_join = join
@@ -832,7 +832,7 @@ module VariableToDeps =
struct
let cache_prefix = "Eva.Octagons.VariableToDeps"
- include Hptmap.Make (Variable) (Deps) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (Variable) (Deps) (Hptmap_Info)
let is_included: t -> t -> bool =
let cache_name = cache_prefix ^ ".is_included" in
@@ -901,7 +901,7 @@ module BaseToVariables = struct
let is_empty (s, t) = VSet.is_empty s && VSet.is_empty t
end
- include Hptmap.Make (Base.Base) (VSetPair) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (Base.Base) (VSetPair) (Hptmap_Info)
let cache_prefix = "Eva.Octagons.BaseToVariables"
diff --git a/src/plugins/eva/domains/simple_memory.ml b/src/plugins/eva/domains/simple_memory.ml
index 3dcd4d525a0..e8a9140134e 100644
--- a/src/plugins/eva/domains/simple_memory.ml
+++ b/src/plugins/eva/domains/simple_memory.ml
@@ -49,7 +49,7 @@ module Make_Memory (Info: sig val name: string end) (Value: Value) = struct
let dependencies = [ Ast.self ]
end
- include Hptmap.Make (Base.Base) (Value) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (Base.Base) (Value) (Hptmap_Info)
let name = Info.name
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index cfb81b31b08..b7e3cf5ecc7 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -37,7 +37,7 @@ module K2V = struct
let initial_values = []
let dependencies = [ Ast.self ]
end
- module M = Hptmap.Make (K.HCE) (V) (Hptmap.Comp_unused) (Hptmap_Info)
+ module M = Hptmap.Make (K.HCE) (V) (Hptmap_Info)
include M
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index 8d71f8881d0..e45a1cbba8a 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -232,7 +232,7 @@ module Graph = struct
let initial_values = []
let dependencies = [ Ast.self ]
end
- include Hptmap.Make (Node) (EdgeList) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (Node) (EdgeList) (Hptmap_Info)
let is_included =
let cache = Hptmap_sig.NoCache in
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index dd4fec14857..14c0cc2acda 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -148,7 +148,7 @@ module ZoneStmtMap = struct
let dependencies = [ Ast.self ]
end
- include Hptmap.Make (Stmt_Id) (Zone) (Hptmap.Comp_unused) (Hptmap_Info)
+ include Hptmap.Make (Stmt_Id) (Zone) (Hptmap_Info)
let join =
let decide _k z1 z2 = Zone.join z1 z2 in
diff --git a/src/plugins/impact/pdg_aux.ml b/src/plugins/impact/pdg_aux.ml
index d9ea3006d88..0163c1bf7d0 100644
--- a/src/plugins/impact/pdg_aux.ml
+++ b/src/plugins/impact/pdg_aux.ml
@@ -32,11 +32,7 @@ module Hptmap_Info = struct
end
module NS = struct
- include Hptmap.Make
- (PdgTypes.Node)
- (Locations.Zone)
- (Hptmap.Comp_unused)
- (Hptmap_Info)
+ include Hptmap.Make (PdgTypes.Node) (Locations.Zone) (Hptmap_Info)
let intersects =
let name = "Impact.Pdg_aux.NS.intersects" in
diff --git a/src/plugins/pdg/pdg_types/pdgTypes.ml b/src/plugins/pdg/pdg_types/pdgTypes.ml
index e3e19dfd24c..e4af154aef0 100644
--- a/src/plugins/pdg/pdg_types/pdgTypes.ml
+++ b/src/plugins/pdg/pdg_types/pdgTypes.ml
@@ -281,7 +281,7 @@ module G = struct
let dependencies = [ Ast.self ]
end
- module To = Hptmap.Make (Node) (DpdZone) (Hptmap.Comp_unused) (Hptmap_Info)
+ module To = Hptmap.Make (Node) (DpdZone) (Hptmap_Info)
let () = Ast.add_hook_on_update (fun _ -> To.clear_caches ())
(* See comment on previous call to Ast.add_hook_on_update *)
--
GitLab