From 2d9c7320f0a79e76798938c102f3b67e3feb9c66 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:33:09 +0200
Subject: [PATCH] [Hptmap] Simplifies functor use: V.pretty_debug is no longer
required.
Values are simply modules of type Datatype.S.
The pretty_debug of hptmap simply uses V.pretty instead of V.pretty_debug.
Removes all previous definitions "let pretty_debug = pretty" in modules
using Hptmap.
---
src/kernel_services/abstract_interp/base.ml | 1 -
src/kernel_services/abstract_interp/ival.ml | 1 -
src/kernel_services/abstract_interp/ival.mli | 2 --
src/kernel_services/analysis/stmts_graph.ml | 2 +-
src/libraries/utils/hptmap.ml | 16 +++++++---------
src/libraries/utils/hptmap.mli | 10 ++--------
src/libraries/utils/hptset.ml | 7 +------
src/plugins/eva/Eva.mli | 1 -
src/plugins/eva/domains/equality/equality.ml | 1 -
src/plugins/eva/domains/gauges/gauges_domain.ml | 1 -
src/plugins/eva/domains/hcexprs.ml | 2 --
src/plugins/eva/domains/hcexprs.mli | 1 -
.../eva/domains/multidim/abstract_structure.ml | 1 -
.../eva/domains/multidim/multidim_domain.ml | 2 --
.../eva/domains/numerors/numerors_value.ml | 1 -
.../eva/domains/numerors/numerors_value.mli | 2 --
src/plugins/eva/domains/octagons.ml | 6 +-----
src/plugins/eva/domains/simple_memory.ml | 1 -
src/plugins/eva/domains/simple_memory.mli | 3 ---
src/plugins/eva/domains/traces_domain.ml | 1 -
src/plugins/eva/types/callstack.ml | 2 --
src/plugins/eva/types/callstack.mli | 2 --
src/plugins/eva/types/deps.ml | 2 --
src/plugins/eva/types/deps.mli | 1 -
src/plugins/eva/values/sign_value.ml | 1 -
src/plugins/eva/values/sign_value.mli | 1 -
src/plugins/pdg/pdg_types/pdgTypes.ml | 3 ---
27 files changed, 12 insertions(+), 62 deletions(-)
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 0a87aa8f1fd..87b585b9c48 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -452,7 +452,6 @@ module Base = struct
let copy = Datatype.undefined
end)
let id = id
- let pretty_debug = pretty
end
include Base
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 7d64c801fb9..9bc8df0beb2 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -1024,7 +1024,6 @@ let bitwise_not ~size ~signed v =
else
bitwise_unsigned_not ~size v
-let pretty_debug = pretty
let name = "ival"
(*
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index aadd4ff0759..0ef0bbfb577 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -330,8 +330,6 @@ val complement_int_under: size:int -> signed:bool -> t -> t Lattice_bounds.or_bo
(** Returns an under-approximation of the integers of the given size and
signedness that are *not* represented by the given ival. *)
-val pretty_debug : Format.formatter -> t -> unit
-
(**/**)
val rehash: t -> t (* Low-level operation for demarshalling *)
diff --git a/src/kernel_services/analysis/stmts_graph.ml b/src/kernel_services/analysis/stmts_graph.ml
index f93858ebf92..342f5ba62ce 100644
--- a/src/kernel_services/analysis/stmts_graph.ml
+++ b/src/kernel_services/analysis/stmts_graph.ml
@@ -34,7 +34,7 @@ struct
module HV = Hashtbl.Make(Stmt)
module HptmapStmtBool = Hptmap.Make
(Cil_datatype.Stmt_Id)
- (struct include Datatype.Bool let pretty_debug = pretty end)
+ (Datatype.Bool)
(struct
let initial_values = []
let dependencies = [ Ast.self ]
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index a4678edd33b..7766433682c 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -130,11 +130,6 @@ module type Id_Datatype = sig
val id: t -> int
end
-module type V = sig
- include Datatype.S
- val pretty_debug: t Pretty_utils.formatter
-end
-
module Shape(Key: Id_Datatype) = struct
type key = Key.t
type 'b map = (Key.t, 'b) tree
@@ -599,7 +594,7 @@ end
module Make_with_compositional_bool
(Key: Id_Datatype)
- (V : V)
+ (V : Datatype.S)
(Compositional_bool : Compositional_bool with type key := Key.t
and type v := V.t)
(Info: Info with type key := Key.t
@@ -621,7 +616,7 @@ struct
"L@[<v>@[(A %x, T %a)@]@ @[(AK %x)%a@]@ @[ -> (AV %x)@]@ @[%a@]@]"
(Extlib.address_of_value t) Tag_comp.pretty comp
(Extlib.address_of_value k) Key.pretty k
- (Extlib.address_of_value v) V.pretty_debug v
+ (Extlib.address_of_value v) V.pretty v
| Branch (prefix, mask, t1, t2, tag) as t ->
Format.fprintf fmt
"B@[<v>@[(A %x, T %a, P %x, M %x)@]@ @[%a@]@ @[ %a@]@]"
@@ -1437,8 +1432,11 @@ module Comp_unused = struct
let compose _ _ = false
end
-module Make (Key: Id_Datatype) (V : V) (Info: Info with type key := Key.t
- and type v := V.t)
+module Make
+ (Key: Id_Datatype)
+ (V : Datatype.S)
+ (Info: Info with type key := Key.t
+ and type v := V.t)
= Make_with_compositional_bool (Key) (V) (Comp_unused) (Info)
(*
diff --git a/src/libraries/utils/hptmap.mli b/src/libraries/utils/hptmap.mli
index 725c205712d..cd2b5c0c3ae 100644
--- a/src/libraries/utils/hptmap.mli
+++ b/src/libraries/utils/hptmap.mli
@@ -39,12 +39,6 @@ module Shape (Key : Id_Datatype): sig
type 'a t = 'a map
end
-(** 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. *)
module type Info = sig
type key
@@ -65,7 +59,7 @@ end
to values [V]. *)
module Make
(Key : Id_Datatype)
- (V : V)
+ (V : Datatype.S)
(_ : Info with type key := Key.t
and type v := V.t)
: Hptmap_sig.S with type key = Key.t
@@ -94,7 +88,7 @@ end
each tree. *)
module Make_with_compositional_bool
(Key : Id_Datatype)
- (V : V)
+ (V : Datatype.S)
(_ : Compositional_bool with type key := Key.t
and type v := V.t)
(_ : Info with type key := Key.t
diff --git a/src/libraries/utils/hptset.ml b/src/libraries/utils/hptset.ml
index 28c3164935d..11e88615617 100644
--- a/src/libraries/utils/hptset.ml
+++ b/src/libraries/utils/hptset.ml
@@ -110,17 +110,12 @@ module Make
type elt = X.t
- 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_Info)
+ module M = Hptmap.Make (X) (Datatype.Unit) (Hptmap_Info)
include M
let add k s = add k () s
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index aa4bb6a684b..a317fca1878 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -188,7 +188,6 @@ module Deps: sig
include Datatype.S with type t := t
val pretty_precise: Format.formatter -> t -> unit
- val pretty_debug: Format.formatter -> t -> unit
(* Constructors *)
diff --git a/src/plugins/eva/domains/equality/equality.ml b/src/plugins/eva/domains/equality/equality.ml
index 7d85984fcb2..ab2e0c45457 100644
--- a/src/plugins/eva/domains/equality/equality.ml
+++ b/src/plugins/eva/domains/equality/equality.ml
@@ -75,7 +75,6 @@ module Set = struct
the value of [lv], and the second set gathers the expressions that
contains [&lv]. *)
include Datatype.Triple (Equality) (HCESet) (HCESet)
- let pretty_debug = pretty
let inter (left_eq, left_set, left_set') (right_eq, right_set, right_set') =
let equality = Equality.inter left_eq right_eq
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index a082f405044..49416c570c0 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -65,7 +65,6 @@ module G = struct
| Some i -> Abstract_interp.Int.pretty fmt i
in
Format.fprintf fmt "[%a .. %a]" (pp_bound '-') min (pp_bound '+') max
- let pretty_debug = pretty
let inject_range n1 n2 : t =
Some (Integer.of_int (min n1 n2)), Some (Integer.of_int (max n1 n2))
diff --git a/src/plugins/eva/domains/hcexprs.ml b/src/plugins/eva/domains/hcexprs.ml
index 951d897535f..b0fd18a76ac 100644
--- a/src/plugins/eva/domains/hcexprs.ml
+++ b/src/plugins/eva/domains/hcexprs.ml
@@ -96,8 +96,6 @@ module HCE = struct
include S
- let pretty_debug = pretty
-
let of_lval lv = hashcons (LV lv)
let of_exp (exp : Eva_ast.exp) =
diff --git a/src/plugins/eva/domains/hcexprs.mli b/src/plugins/eva/domains/hcexprs.mli
index 0b65e6e224e..72cc5f976e1 100644
--- a/src/plugins/eva/domains/hcexprs.mli
+++ b/src/plugins/eva/domains/hcexprs.mli
@@ -40,7 +40,6 @@ module E: Datatype.S with type t = unhashconsed_exprs
module HCE: sig
include Datatype.S_with_collections
val self: State.t
- val pretty_debug: t Pretty_utils.formatter
val id: t -> int
diff --git a/src/plugins/eva/domains/multidim/abstract_structure.ml b/src/plugins/eva/domains/multidim/abstract_structure.ml
index eac548f2d77..d8301b01b21 100644
--- a/src/plugins/eva/domains/multidim/abstract_structure.ml
+++ b/src/plugins/eva/domains/multidim/abstract_structure.ml
@@ -75,7 +75,6 @@ struct
let name = "Abstract_Memory.Structure.Values"
let reprs = [ of_raw Bit.zero ]
end)
- let pretty_debug = pretty
end
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 63db3c5dc72..ed430145d4c 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -265,7 +265,6 @@ struct
include Datatype.Make (Prototype)
let pretty = Memory.pretty
- let _pretty_debug = Memory.pretty
let top = Memory.top
let is_top = Memory.is_top
let is_included = Memory.is_included
@@ -333,7 +332,6 @@ struct
module V =
struct
include Datatype.Pair (Memory) (Referers)
- let pretty_debug = pretty
let top = Memory.top, Referers.empty
let is_top (m,r) = Memory.is_top m && Referers.is_empty r
end
diff --git a/src/plugins/eva/domains/numerors/numerors_value.ml b/src/plugins/eva/domains/numerors/numerors_value.ml
index 85485626c68..ee85f4a742c 100644
--- a/src/plugins/eva/domains/numerors/numerors_value.ml
+++ b/src/plugins/eva/domains/numerors/numerors_value.ml
@@ -113,7 +113,6 @@ module T = struct
let pretty = pp_print
end
include Datatype.Make(T)
-let pretty_debug = pretty
let pretty_typ _ = pretty
type context = unit
diff --git a/src/plugins/eva/domains/numerors/numerors_value.mli b/src/plugins/eva/domains/numerors/numerors_value.mli
index 4814acb57a0..721ef891ec3 100644
--- a/src/plugins/eva/domains/numerors/numerors_value.mli
+++ b/src/plugins/eva/domains/numerors/numerors_value.mli
@@ -22,8 +22,6 @@
include Abstract_value.Leaf with type context = unit
-val pretty_debug : t Pretty_utils.formatter
-
(** Reduction of an error value according to a floating-point interval. *)
val reduce: Fval.t -> t -> t Eval.or_bottom
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index bd82bcbad8a..e4a757b1b39 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -588,7 +588,6 @@ end
module Diamond = struct
include Datatype.Make (DiamondDatatype)
- let pretty_debug = pretty
let top = { add = Ival.top; sub = Ival.top }
@@ -736,9 +735,7 @@ end
(* Keep track of related variables in an octagon state. *)
module Relations = struct
- include Hptmap.Make (Variable)
- (struct include VarSet let pretty_debug = pretty end)
- (Hptmap_Info)
+ include Hptmap.Make (Variable) (VarSet) (Hptmap_Info)
let inter =
let cache = Hptmap_sig.PersistentCache "Octagons.Relations.inter" in
@@ -895,7 +892,6 @@ module BaseToVariables = struct
include Datatype.Pair
(VSet) (* Directly dependent variables *)
(VSet) (* Indirectly dependent variables *)
- let pretty_debug = pretty
let inter (s1,t1) (s2,t2) = VSet.inter s1 s2, VSet.inter t1 t2
let union (s1,t1) (s2,t2) = VSet.union s1 s2, VSet.union t1 t2
let is_empty (s, t) = VSet.is_empty s && VSet.is_empty t
diff --git a/src/plugins/eva/domains/simple_memory.ml b/src/plugins/eva/domains/simple_memory.ml
index e8a9140134e..b935f55c6a9 100644
--- a/src/plugins/eva/domains/simple_memory.ml
+++ b/src/plugins/eva/domains/simple_memory.ml
@@ -28,7 +28,6 @@ module type Value = sig
include Abstract_value.Leaf
val widen : t -> t -> t
val track_variable: Cil_types.varinfo -> bool
- val pretty_debug: t Pretty_utils.formatter
val builtins: (string * t builtin) list
end
diff --git a/src/plugins/eva/domains/simple_memory.mli b/src/plugins/eva/domains/simple_memory.mli
index f70f75d573b..ae1cbfd0f87 100644
--- a/src/plugins/eva/domains/simple_memory.mli
+++ b/src/plugins/eva/domains/simple_memory.mli
@@ -40,9 +40,6 @@ module type Value = sig
mapped to [V.top]. *)
val track_variable: Cil_types.varinfo -> bool
- (** Can be equal to {!pretty} *)
- val pretty_debug: t Pretty_utils.formatter
-
(** A list of builtins for the domain: each builtin is associated with the
name of the C function it interprets. *)
val builtins: (string * t builtin) list
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index e45a1cbba8a..5ca13666ef8 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -223,7 +223,6 @@ module EdgeList = struct
include Datatype.List_with_collections(Edge)
(struct let module_name = "Value.Traces_domain.EdgeList" end)
let pretty = Edge.pretty_list
- let pretty_debug = pretty
end
module Graph = struct
diff --git a/src/plugins/eva/types/callstack.ml b/src/plugins/eva/types/callstack.ml
index fec3d186842..922edd69df4 100644
--- a/src/plugins/eva/types/callstack.ml
+++ b/src/plugins/eva/types/callstack.ml
@@ -78,8 +78,6 @@ type call = Call.t
include Datatype.Make_with_collections (Prototype)
-let pretty_debug = pretty
-
let compare_lex cs1 cs2 =
if cs1 == cs2 then 0 else
let c = Thread.compare cs1.thread cs2.thread in
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
index 0340490e58e..494df93cf70 100644
--- a/src/plugins/eva/types/callstack.mli
+++ b/src/plugins/eva/types/callstack.mli
@@ -85,5 +85,3 @@ val to_stmt_list : t -> Cil_types.stmt list
val to_call_list : t -> (Cil_types.kernel_function * Cil_types.kinstr) list
[@@@ api_end]
-
-val pretty_debug : Format.formatter -> t -> unit
diff --git a/src/plugins/eva/types/deps.ml b/src/plugins/eva/types/deps.ml
index 9ac28758519..31a37bf66a6 100644
--- a/src/plugins/eva/types/deps.ml
+++ b/src/plugins/eva/types/deps.ml
@@ -45,8 +45,6 @@ let pretty_precise fmt {data; indirect} =
Zone.pretty indirect
Zone.pretty data
-let pretty_debug = pretty_precise
-
(* Conversion to zone, used by default pretty printing *)
let to_zone d = Locations.Zone.join d.data d.indirect
diff --git a/src/plugins/eva/types/deps.mli b/src/plugins/eva/types/deps.mli
index 4dbd0ea9935..9edd34e5ba2 100644
--- a/src/plugins/eva/types/deps.mli
+++ b/src/plugins/eva/types/deps.mli
@@ -33,7 +33,6 @@ type t = {
include Datatype.S with type t := t
val pretty_precise: Format.formatter -> t -> unit
-val pretty_debug: Format.formatter -> t -> unit
(* Constructors *)
diff --git a/src/plugins/eva/values/sign_value.ml b/src/plugins/eva/values/sign_value.ml
index 04ab54aa224..4e779b62672 100644
--- a/src/plugins/eva/values/sign_value.ml
+++ b/src/plugins/eva/values/sign_value.ml
@@ -65,7 +65,6 @@ include Datatype.Make(struct
(if v.zero then "0" else "")
(if v.pos then "+" else "")
end)
-let pretty_debug = pretty
let pretty_typ _ = pretty
type context = unit
diff --git a/src/plugins/eva/values/sign_value.mli b/src/plugins/eva/values/sign_value.mli
index 7fadfe56970..b1419e132b2 100644
--- a/src/plugins/eva/values/sign_value.mli
+++ b/src/plugins/eva/values/sign_value.mli
@@ -29,4 +29,3 @@ type signs = {
}
include Abstract_value.Leaf with type t = signs and type context = unit
-val pretty_debug: t Pretty_utils.formatter
diff --git a/src/plugins/pdg/pdg_types/pdgTypes.ml b/src/plugins/pdg/pdg_types/pdgTypes.ml
index e4af154aef0..7a8215b18c4 100644
--- a/src/plugins/pdg/pdg_types/pdgTypes.ml
+++ b/src/plugins/pdg/pdg_types/pdgTypes.ml
@@ -224,14 +224,11 @@ module DpdZone : sig
val dpd_zone : t -> Locations.Zone.t option
val pretty : Format.formatter -> t -> unit
- val pretty_debug: Format.formatter -> t -> unit
end = struct
include Datatype.Pair(Dpd)(Datatype.Option(Locations.Zone))
(* None == Locations.Zone.Top *)
- let pretty_debug = pretty
-
let dpd_kind dpd = fst dpd
let dpd_zone dpd = snd dpd
let kind_and_zone dpd = dpd
--
GitLab