From 7056b92d0bc54971f7ce50a65038a23a0ead6b60 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 29 Sep 2023 10:27:26 +0200
Subject: [PATCH] [Hptmap] Simplifies functor use: merges two argument modules
into one.
Merges the two argument modules `Initial_values` and `Datatype_deps` into one
module `Info` containing two values "initial_values" and "dependencies".
---
src/kernel_services/abstract_interp/base.ml | 12 ++++--
src/kernel_services/abstract_interp/lmap.ml | 23 +++++------
.../abstract_interp/lmap_bitwise.ml | 6 ++-
.../abstract_interp/locations.ml | 35 ++++++++--------
src/kernel_services/analysis/stmts_graph.ml | 6 ++-
.../ast_data/kernel_function.ml | 6 ++-
.../ast_queries/cil_datatype.ml | 21 ++++------
src/libraries/utils/hptmap.ml | 25 ++++++-----
src/libraries/utils/hptmap.mli | 20 ++++-----
src/libraries/utils/hptset.ml | 41 ++++++++++---------
src/libraries/utils/hptset.mli | 29 +++++++------
.../eva/domains/cvalue/builtins_malloc.ml | 14 ++++---
src/plugins/eva/domains/equality/equality.ml | 10 ++---
.../eva/domains/gauges/gauges_domain.ml | 13 +++---
src/plugins/eva/domains/hcexprs.ml | 14 ++++---
.../domains/multidim/abstract_structure.ml | 9 ++--
.../eva/domains/multidim/multidim_domain.ml | 13 +++---
src/plugins/eva/domains/octagons.ml | 31 +++++---------
src/plugins/eva/domains/simple_memory.ml | 9 ++--
src/plugins/eva/domains/symbolic_locs.ml | 8 +++-
src/plugins/eva/domains/traces_domain.ml | 9 ++--
src/plugins/from/from_compute.ml | 11 +++--
src/plugins/impact/pdg_aux.ml | 8 +++-
src/plugins/pdg/pdg_types/pdgTypes.ml | 16 +++++---
24 files changed, 208 insertions(+), 181 deletions(-)
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 9e78618b6bd..b5f98f4b825 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -461,8 +461,10 @@ module Hptshape = Hptmap.Shape (Base)
module Hptset = Hptset.Make
(Base)
- (struct let v = [ [ ]; [Null] ] end)
- (struct let l = [ Ast.self ] end)
+ (struct
+ let initial_values = [ [Null] ]
+ let dependencies = [ Ast.self ]
+ end)
let () = Ast.add_monotonic_state Hptset.self
let () = Ast.add_hook_on_update Hptset.clear_caches
@@ -554,8 +556,10 @@ module SetLattice = Make_Hashconsed_Lattice_Set(Base)(Hptset)
module BMap =
Hptmap.Make (Base) (Base) (Hptmap.Comp_unused)
- (struct let v = [ [] ] end)
- (struct let l = [ Ast.self ] end)
+ (struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end)
type substitution = base Hptshape.map
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 7c4689e11b9..8c8b3f3c20e 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -82,24 +82,23 @@ struct
module M = struct
- module Comp =
- struct
+ module Offsetmap = struct
+ include Offsetmap
+ let name = Offsetmap.name ^ " " ^ Default_offsetmap.name
+ end
+
+ module Comp = struct
let f _base offsetmap = Offsetmap.cardinal_zero_or_one offsetmap
let compose a b = a && b
let e = true
end
- module Initial_Values = struct let v = [ [] ] end
+ module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end
- module M = Hptmap.Make
- (Base.Base)
- (struct
- include Offsetmap
- let name = Offsetmap.name ^ " " ^ Default_offsetmap.name
- end)
- (Comp)
- (Initial_Values)
- (struct let l = [ Ast.self ] end)
+ module M = Hptmap.Make (Base.Base) (Offsetmap) (Comp) (Hptmap_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 bb23f971096..ffc2bafe92e 100644
--- a/src/kernel_services/abstract_interp/lmap_bitwise.ml
+++ b/src/kernel_services/abstract_interp/lmap_bitwise.ml
@@ -141,7 +141,11 @@ struct
let default_offsetmap b = default_offsetmap_aux b (Base.validity b)
module LBase = struct
- include Hptmap.Make(Base.Base)(LOffset)(Hptmap.Comp_unused)(struct let v = [[]] end)(struct let l = [ Ast.self ] end)
+ module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end
+ include Hptmap.Make (Base.Base) (LOffset) (Hptmap.Comp_unused) (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 56d9349940e..af174d7cd4d 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -24,15 +24,17 @@ open Cil_types
open Cil
open Abstract_interp
-module Initial_Values = struct
- let v = [ [Base.null,Ival.zero];
- [Base.null,Ival.one];
- [Base.null,Ival.zero_or_one];
- [Base.null,Ival.top];
- [Base.null,Ival.top_float];
- [Base.null,Ival.top_single_precision_float];
- [Base.null,Ival.float_zeros];
- ]
+module Hptmap_Info = struct
+ let initial_values = [ [Base.null,Ival.zero];
+ [Base.null,Ival.one];
+ [Base.null,Ival.zero_or_one];
+ [Base.null,Ival.top];
+ [Base.null,Ival.top_float];
+ [Base.null,Ival.top_single_precision_float];
+ [Base.null,Ival.float_zeros];
+ ]
+
+ let dependencies = [ Ast.self ]
end
(* Store the information that the location has at most cardinal 1, ignoring
@@ -55,13 +57,10 @@ module Comp_exact = struct
end
-
module Location_Bytes = struct
module M = struct
- include Hptmap.Make
- (Base.Base) (Ival) (Comp_exact) (Initial_Values)
- (struct let l = [ Ast.self ] end)
+ include Hptmap.Make (Base.Base) (Ival) (Comp_exact) (Hptmap_Info)
let shape x = x
end
let () = Ast.add_monotonic_state M.self
@@ -372,12 +371,12 @@ module Location_Bits = Location_Bytes
module Zone = struct
- module Initial_Values = struct let v = [ ] end
+ module Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end
- module M =
- Hptmap.Make
- (Base.Base) (Int_Intervals) (Hptmap.Comp_unused) (Initial_Values)
- (struct let l = [ Ast.self ] end)
+ module M = Hptmap.Make (Base.Base) (Int_Intervals) (Hptmap.Comp_unused) (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 3b8beac54f3..bd7e0df01be 100644
--- a/src/kernel_services/analysis/stmts_graph.ml
+++ b/src/kernel_services/analysis/stmts_graph.ml
@@ -36,8 +36,10 @@ struct
(Cil_datatype.Stmt_Id)
(struct include Datatype.Bool let pretty_debug = pretty end)
(Hptmap.Comp_unused)
- (struct let v = [ [] ] end)
- (struct let l = [ Ast.self ] end)
+ (struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end)
(* Clear the (non-project compliant) internal caches each time the ast
changes, which includes every time we switch project. *)
let () = Ast.add_hook_on_update (fun _ -> HptmapStmtBool.clear_caches ())
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index d2b9e4638a3..b76527a49a7 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -628,8 +628,10 @@ module Make_Table = State_builder.Hashtbl(Cil_datatype.Kf.Hashtbl)
module Hptset = struct
include Hptset.Make
(Cil_datatype.Kf)
- (struct let v = [ [ ] ] end)
- (struct let l = [ Ast.self ] end)
+ (struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end)
let () = Ast.add_monotonic_state self
let () = Ast.add_hook_on_update clear_caches
end
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 15182c27463..ba258b3485f 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -307,18 +307,18 @@ module Stmt_Id = struct
end)
let id stmt = stmt.sid
end
+
+module Hptset_Info = struct
+ let initial_values = []
+ let dependencies = [] (* This should be [Ast.self], but cannot be done here *)
+end
+
module Stmt = struct
include Stmt_Id
let pretty_sid fmt s = Format.pp_print_int fmt s.sid
- module Hptset = struct
- include Hptset.Make
- (Stmt_Id)
- (struct let v = [ [ ] ] end)
- (struct let l = [ ] (* This should be [Ast.self], but cannot be done
- here *) end)
- end
+ module Hptset = Hptset.Make (Stmt_Id) (Hptset_Info)
let () = clear_caches := Hptset.clear_caches :: !clear_caches
let rec loc_skind = function
@@ -760,12 +760,7 @@ end
module Varinfo = struct
include Varinfo_Id
- module Hptset = struct
- include Hptset.Make
- (Varinfo_Id)
- (struct let v = [ [ ] ] end)
- (struct let l = [ ] (* Should morally be [Ast.self] *) end)
- end
+ module Hptset = Hptset.Make (Varinfo_Id) (Hptset_Info)
let () = clear_caches := Hptset.clear_caches :: !clear_caches
end
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index 462a08c1d08..9bc3422c355 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -597,14 +597,11 @@ module type Compositional_bool = sig
val compose : bool -> bool -> bool
end
-module type Initial_values = sig
+module type Info = sig
type key
type v
- val v : (key*v) list list
-end
-
-module type Datatype_deps = sig
- val l : State.t list
+ val initial_values : (key * v) list list
+ val dependencies : State.t list
end
module Make
@@ -612,9 +609,8 @@ module Make
(V : V)
(Compositional_bool : Compositional_bool with type key := Key.t
and type v := V.t)
- (Initial_Values: Initial_values with type key := Key.t
- and type v := V.t)
- (Datatype_deps: Datatype_deps)
+ (Info: Info with type key := Key.t
+ and type v := V.t)
=
struct
@@ -668,11 +664,18 @@ struct
incr current_tag;
Tag_comp.encode tag b
in
+ (* If required, add the empty map to the initial values, as it is always
+ exported by the functor at Caml link-time. *)
+ let initial_values =
+ if List.mem [] Info.initial_values
+ then Info.initial_values
+ else [] :: Info.initial_values
+ in
List.map
(function [k,v] -> Leaf (k, v, tc k v)
| [] -> Empty
| _ -> assert false)
- Initial_Values.v
+ initial_values
let rehash_ref = ref (fun _ -> assert false)
@@ -741,7 +744,7 @@ struct
end)
(struct
let name = Type.name ty ^ " hashconsing table"
- let dependencies = Datatype_deps.l
+ let dependencies = Info.dependencies
let size = 137
end)
diff --git a/src/libraries/utils/hptmap.mli b/src/libraries/utils/hptmap.mli
index 18d2595e377..2c80736a6b6 100644
--- a/src/libraries/utils/hptmap.mli
+++ b/src/libraries/utils/hptmap.mli
@@ -45,7 +45,7 @@ module Shape (Key : Id_Datatype): sig
type 'a t = 'a map
end
-(** A boolean information is maintained for each tree, by composing the
+(** 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
@@ -62,19 +62,18 @@ module type Compositional_bool = sig
(** Composition of the values of two subtrees *)
end
-module type Initial_values = sig
+(** Required information for the correctness of the hptmaps. *)
+module type Info = sig
type key
type v
- val v : (key*v) list list
+
+ val initial_values : (key * v) list list
(** List of the maps that must be shared between all instances of Frama-C
(the maps being described by the list of their elements).
Must include all maps that are exported at Caml link-time when the
- functor is applied. This usually includes at least the empty map, hence
- [v] nearly always contains [[]]. *)
-end
+ functor is applied. *)
-module type Datatype_deps = sig
- val l : State.t list
+ val dependencies : State.t list
(** Dependencies of the hash-consing table. The table will be cleared
whenever one of those dependencies is cleared. *)
end
@@ -86,9 +85,8 @@ module Make
(V : V)
(_ : Compositional_bool with type key := Key.t
and type v := V.t)
- (_ : Initial_values with type key := Key.t
- and type v := V.t)
- (_ : Datatype_deps)
+ (_ : 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
diff --git a/src/libraries/utils/hptset.ml b/src/libraries/utils/hptset.ml
index a0f560b2480..59a1dd0955c 100644
--- a/src/libraries/utils/hptset.ml
+++ b/src/libraries/utils/hptset.ml
@@ -92,34 +92,35 @@ module type S = sig
val pretty_debug: t Pretty_utils.formatter
end
-module type Initial_values = sig
+module type Info = sig
type elt
- val v : elt list list
+ val initial_values : elt list list
+ val dependencies : State.t list
end
-module type Datatype_deps = sig
- val l : State.t list
-end
-
-module Make(X: Hptmap.Id_Datatype)
- (Initial_values : Initial_values with type elt := X.t)
- (Datatype_deps : Datatype_deps) : sig
- include S with type elt = X.t
- and type 'a map = 'a Hptmap.Shape(X).t
- val self : State.t
-end
+module Make
+ (X: Hptmap.Id_Datatype)
+ (Info : Info with type elt := X.t)
+ : sig
+ include S with type elt = X.t
+ and type 'a map = 'a Hptmap.Shape(X).t
+ val self : State.t
+ end
= struct
type elt = X.t
- module M =
- Hptmap.Make
- (X)
- (struct include Datatype.Unit let pretty_debug = pretty end)
- (Hptmap.Comp_unused)
- (struct let v = List.map (List.map (fun k -> k, ())) Initial_values.v end)
- (Datatype_deps)
+ module Unit = struct
+ include Datatype.Unit
+ let pretty_debug = pretty
+ end
+
+ module Hptmap_Info = struct
+ let initial_values = List.map (List.map (fun k -> k, ())) Info.initial_values
+ let dependencies = Info.dependencies
+ end
+ module M = Hptmap.Make (X) (Unit) (Hptmap.Comp_unused) (Hptmap_Info)
include M
let add k s = add k () s
diff --git a/src/libraries/utils/hptset.mli b/src/libraries/utils/hptset.mli
index 5a0422db5fc..3729c08177a 100644
--- a/src/libraries/utils/hptset.mli
+++ b/src/libraries/utils/hptset.mli
@@ -105,30 +105,29 @@ module type S = sig
val pretty_debug: t Pretty_utils.formatter
end
-module type Initial_values = sig
+(** Required information for the correctness of the hptsets. *)
+module type Info = sig
type elt
- val v : elt list list
+
+ val initial_values : elt list list
(** List of the sets that must be shared between all instances of Frama-C
(the sets being described by the list of their elements).
Must include all sets that are exported at Caml link-time when the
- functor is applied. This usually includes at least the empty set, hence
- [v] nearly always contains [[]]. *)
-end
+ functor is applied. *)
-module type Datatype_deps = sig
- val l : State.t list
+ val dependencies : State.t list
(** Dependencies of the hash-consing table. The table will be cleared
whenever one of those dependencies is cleared. *)
end
-module Make(X: Hptmap.Id_Datatype)
- (_ : Initial_values with type elt := X.t)
- (_ : Datatype_deps) :
-sig
- include S with type elt = X.t
- and type 'a map = 'a Hptmap.Shape(X).map
- val self : State.t
-end
+module Make
+ (X: Hptmap.Id_Datatype)
+ (_ : Info with type elt := X.t)
+ : sig
+ include S with type elt = X.t
+ and type 'a map = 'a Hptmap.Shape(X).map
+ val self : State.t
+ end
(*
Local Variables:
diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.ml b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
index 270e6a1afa0..8c6155ad86b 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
@@ -36,12 +36,14 @@ let wkey_imprecise_alloc = Self.register_warn_category
(* ---------------------- Dynamically allocated bases ----------------------- *)
-module Base_hptmap = Hptmap.Make
- (Base.Base)
- (Callstack)
- (Hptmap.Comp_unused)
- (struct let v = [ [ ] ] end)
- (struct let l = [ Ast.self ] end)
+
+module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+end
+
+module Base_hptmap =
+ Hptmap.Make (Base.Base) (Callstack) (Hptmap.Comp_unused) (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 0683f1f9a5d..6f1de9bfc41 100644
--- a/src/plugins/eva/domains/equality/equality.ml
+++ b/src/plugins/eva/domains/equality/equality.ml
@@ -63,9 +63,6 @@ type equality = Equality.t
module Set = struct
- module Initial_Values = struct let v = [[]] end
- module Dependencies = struct let l = [ HCE.self ] end
-
(* A set of equalities between lvalues and expressions is encoded as a map
from each lvalue or expression to:
- the equality in which it is involved;
@@ -97,8 +94,11 @@ module Set = struct
HCESet.union left_set' right_set'
end
- include Hptmap.Make (HCE) (Data)
- (Hptmap.Comp_unused) (Initial_Values) (Dependencies)
+ module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end
+ include Hptmap.Make (HCE) (Data) (Hptmap.Comp_unused) (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 ea16b89bfc9..fc759a3f6e6 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -272,6 +272,11 @@ module G = struct
end
+ module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end
+
(* A MV contains (usual) values for the different bases that are incremented
in a loop.
1. for missing bases, no information is stored (i.e. Top)
@@ -280,9 +285,7 @@ module G = struct
*)
module MV = struct
- include Hptmap.Make(Base)(Cvalue.V)(Hptmap.Comp_unused)
- (struct let v = [] end)
- (struct let l = [Ast.self] end)
+ include Hptmap.Make (Base) (Cvalue.V) (Hptmap.Comp_unused) (Hptmap_Info)
(* This function computes a pointwise union on two MVs assumed to have
disjoint set of keys. *)
@@ -319,9 +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)
- (struct let v = [] end)
- (struct let l = [Ast.self] end)
+ include Hptmap.Make (Base) (Bounds) (Hptmap.Comp_unused) (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 b67b7b20813..d34f7bdfa6d 100644
--- a/src/plugins/eva/domains/hcexprs.ml
+++ b/src/plugins/eva/domains/hcexprs.ml
@@ -130,8 +130,12 @@ module HCE = struct
| LV lval -> if Lval.equal lval late then of_exp heir else h
end
-module HCESet =
- Hptset.Make (HCE) (struct let v = [] end) (struct let l = [Ast.self] end)
+module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+end
+
+module HCESet = Hptset.Make (HCE) (Hptmap_Info)
type lvalues = {
read : HCESet.t;
@@ -158,8 +162,7 @@ module HCEToZone = struct
let cache_prefix = "Value.Symbolic_exprs.K2Z"
- include Hptmap.Make(HCE)(Locations.Zone)(Hptmap.Comp_unused)
- (struct let v = [] end)(struct let l = [Ast.self] end)
+ include Hptmap.Make (HCE) (Locations.Zone) (Hptmap.Comp_unused) (Hptmap_Info)
let is_included =
let cache_name = cache_prefix ^ ".is_included" in
@@ -199,8 +202,7 @@ end
module BaseToHCESet = struct
- include Hptmap.Make (Base.Base) (HCESet) (Hptmap.Comp_unused)
- (struct let v = [] end)(struct let l = [Ast.self] end)
+ include Hptmap.Make (Base.Base) (HCESet) (Hptmap.Comp_unused) (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 e53381f0cb4..3b00b1ddb72 100644
--- a/src/plugins/eva/domains/multidim/abstract_structure.ml
+++ b/src/plugins/eva/domains/multidim/abstract_structure.ml
@@ -77,11 +77,14 @@ struct
end)
let pretty_debug = pretty
end
- module Initial_Values = struct let v = [[]] end
- module Deps = struct let l = Config.deps end
+
+ module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end
module FieldMap =
- Hptmap.Make (Field) (Values) (Hptmap.Comp_unused) (Initial_Values) (Deps)
+ Hptmap.Make (Field) (Values) (Hptmap.Comp_unused) (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 4a047f6d3d2..5a27426cb27 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -330,8 +330,6 @@ struct
module Tracking = Base.Hptset
(* The domain is essentially a map from bases to individual memory abstractions *)
- module Initial_Values = struct let v = [[]] end
- module Deps = struct let l = [Ast.self] end
module V =
struct
include Datatype.Pair (Memory) (Referers)
@@ -340,12 +338,15 @@ struct
let is_top (m,r) = Memory.is_top m && Referers.is_empty r
end
+ module Hptmap_Info =
+ struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end
+
module BaseMap =
struct
- include
- Hptmap.Make
- (Base.Base) (V)
- (Hptmap.Comp_unused) (Initial_Values) (Deps)
+ include Hptmap.Make (Base.Base) (V) (Hptmap.Comp_unused) (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 3859cea67a4..30367800d64 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -44,6 +44,11 @@ let saturate_octagons = true
the caller either. *)
let intraprocedural () = not (Parameters.OctagonCall.get ())
+module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+end
+
(* -------------------------------------------------------------------------- *)
(* Basic types: pair of variables and Ival.t *)
(* -------------------------------------------------------------------------- *)
@@ -158,11 +163,7 @@ module Variable : Variable = struct
Eva_ast.deps_of_lval eval_loc (Option.get (HCE.to_lval lval))
end
-module VarSet =
- Hptset.Make
- (Variable)
- (struct let v = [ [ ] ] end)
- (struct let l = [ Ast.self ] end)
+module VarSet = Hptset.Make (Variable) (Hptmap_Info)
(* Pairs of related variables in an octagon.
This module imposes an order between the two variables X and Y in a pair
@@ -615,11 +616,8 @@ end
(* Maps linking pairs of variables (X, Y) to intervals for X+Y and X-Y. *)
module Octagons = struct
- module Initial_Values = struct let v = [[]] end
- module Dependencies = struct let l = [ Ast.self ] end
- include Hptmap.Make (Pair) (Diamond)
- (Hptmap.Comp_unused) (Initial_Values) (Dependencies)
+ include Hptmap.Make (Pair) (Diamond) (Hptmap.Comp_unused) (Hptmap_Info)
let internal_join = join
@@ -737,12 +735,10 @@ end
(* Keep track of related variables in an octagon state. *)
module Relations = struct
- module Initial_Values = struct let v = [[]] end
- module Dependencies = struct let l = [ Ast.self ] end
include Hptmap.Make (Variable)
(struct include VarSet let pretty_debug = pretty end)
- (Hptmap.Comp_unused) (Initial_Values) (Dependencies)
+ (Hptmap.Comp_unused) (Hptmap_Info)
let inter =
let cache = Hptmap_sig.PersistentCache "Octagons.Relations.inter" in
@@ -782,11 +778,8 @@ end
(* -------------------------------------------------------------------------- *)
module Intervals = struct
- module Initial_Values = struct let v = [[]] end
- module Dependencies = struct let l = [ Ast.self ] end
- include Hptmap.Make (Variable) (Ival)
- (Hptmap.Comp_unused) (Initial_Values) (Dependencies)
+ include Hptmap.Make (Variable) (Ival) (Hptmap.Comp_unused) (Hptmap_Info)
let internal_join = join
@@ -839,8 +832,7 @@ module VariableToDeps =
struct
let cache_prefix = "Eva.Octagons.VariableToDeps"
- include Hptmap.Make (Variable) (Deps) (Hptmap.Comp_unused)
- (struct let v = [[]] end) (struct let l = [Ast.self] end)
+ include Hptmap.Make (Variable) (Deps) (Hptmap.Comp_unused) (Hptmap_Info)
let is_included: t -> t -> bool =
let cache_name = cache_prefix ^ ".is_included" in
@@ -909,8 +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)
- (struct let v = [[]] end) (struct let l = [Ast.self] end)
+ include Hptmap.Make (Base.Base) (VSetPair) (Hptmap.Comp_unused) (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 39aef1ca1f1..3dcd4d525a0 100644
--- a/src/plugins/eva/domains/simple_memory.ml
+++ b/src/plugins/eva/domains/simple_memory.ml
@@ -44,11 +44,12 @@ end
module Make_Memory (Info: sig val name: string end) (Value: Value) = struct
- module Initial_Values = struct let v = [] end
- module Deps = struct let l = [Ast.self] end
+ module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end
- include Hptmap.Make
- (Base.Base) (Value) (Hptmap.Comp_unused) (Initial_Values) (Deps)
+ include Hptmap.Make (Base.Base) (Value) (Hptmap.Comp_unused) (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 e2a72839350..cfb81b31b08 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -32,8 +32,12 @@ module V = Cvalue.V (* TODO: functorize (with locations too ?) *)
(* Map from expressions/lvalues to abstract values *)
module K2V = struct
- module M = Hptmap.Make(K.HCE)(V)(Hptmap.Comp_unused)
- (struct let v = [] end)(struct let l = [Ast.self] end)
+
+ module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end
+ module M = Hptmap.Make (K.HCE) (V) (Hptmap.Comp_unused) (Hptmap_Info)
include M
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index b6113457eab..8d71f8881d0 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -227,9 +227,12 @@ module EdgeList = struct
end
module Graph = struct
- include Hptmap.Make(Node)(EdgeList)(Hptmap.Comp_unused)
- (struct let v = [[]] end)
- (struct let l = [Ast.self] end)
+
+ module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end
+ include Hptmap.Make (Node) (EdgeList) (Hptmap.Comp_unused) (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 466dfd85c36..dd4fec14857 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -142,10 +142,13 @@ let compute_using_prototype_for_state state kf assigns =
Eva.Assigns.{ return = return_deps; memory = deps }
module ZoneStmtMap = struct
- include
- Hptmap.Make(Stmt_Id)(Zone)(Hptmap.Comp_unused)
- (struct let v = [[]] end)
- (struct let l = [Ast.self] end)
+
+ module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end
+
+ include Hptmap.Make (Stmt_Id) (Zone) (Hptmap.Comp_unused) (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 df335158b96..d9ea3006d88 100644
--- a/src/plugins/impact/pdg_aux.ml
+++ b/src/plugins/impact/pdg_aux.ml
@@ -26,13 +26,17 @@ open Locations
type node = PdgTypes.Node.t * Zone.t
+module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+end
+
module NS = struct
include Hptmap.Make
(PdgTypes.Node)
(Locations.Zone)
(Hptmap.Comp_unused)
- (struct let v = [[]] end)
- (struct let l = [Ast.self] end)
+ (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 63d4d75fa4a..e3e19dfd24c 100644
--- a/src/plugins/pdg/pdg_types/pdgTypes.ml
+++ b/src/plugins/pdg/pdg_types/pdgTypes.ml
@@ -99,9 +99,11 @@ end
end
-module NodeSet = Hptset.Make(Node)
- (struct let v = [ [ ] ] end)
- (struct let l = [ Ast.self ] end)
+module Hptset_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+end
+module NodeSet = Hptset.Make(Node) (Hptset_Info)
(* Clear the (non-project compliant) internal caches each time the ast
is updated, which includes every time we switch project. *)
let () = Ast.add_hook_on_update NodeSet.clear_caches
@@ -274,8 +276,12 @@ module G = struct
let label (_, l, _) = l
end
- module To = Hptmap.Make(Node)(DpdZone)(Hptmap.Comp_unused)
- (struct let v = [[]] end)(struct let l = [Ast.self] end)
+ module Hptmap_Info = struct
+ let initial_values = []
+ let dependencies = [ Ast.self ]
+ end
+
+ module To = Hptmap.Make (Node) (DpdZone) (Hptmap.Comp_unused) (Hptmap_Info)
let () = Ast.add_hook_on_update (fun _ -> To.clear_caches ())
(* See comment on previous call to Ast.add_hook_on_update *)
--
GitLab