From 66a6668ae70d02b44426492629b985bedde653f7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 28 May 2024 19:13:54 +0200
Subject: [PATCH] [Eva] Domain_builder.Complete functor builds unit context for
domains.
Removes NoContext from domain_builder.
Removes Context argument from other Complete_* functors: they all build
a unit context.
---
src/plugins/eva/domains/apron/apron_domain.ml | 1 -
.../eva/domains/cvalue/cvalue_domain.ml | 5 +++-
src/plugins/eva/domains/domain_builder.ml | 23 ++++++-------------
src/plugins/eva/domains/domain_builder.mli | 16 +++++--------
.../eva/domains/gauges/gauges_domain.ml | 1 -
src/plugins/eva/domains/inout_domain.ml | 1 -
.../eva/domains/multidim/multidim_domain.ml | 1 -
src/plugins/eva/domains/octagons.ml | 1 -
src/plugins/eva/domains/offsm_domain.ml | 1 -
src/plugins/eva/domains/simple_memory.ml | 1 -
src/plugins/eva/domains/symbolic_locs.ml | 1 -
src/plugins/eva/domains/taint_domain.ml | 1 -
src/plugins/eva/domains/traces_domain.ml | 1 -
src/plugins/eva/domains/unit_domain.ml | 1 -
14 files changed, 17 insertions(+), 38 deletions(-)
diff --git a/src/plugins/eva/domains/apron/apron_domain.ml b/src/plugins/eva/domains/apron/apron_domain.ml
index 691980d0ed5..ec320503fdf 100644
--- a/src/plugins/eva/domains/apron/apron_domain.ml
+++ b/src/plugins/eva/domains/apron/apron_domain.ml
@@ -428,7 +428,6 @@ module Make (Man : Input) = struct
let s = Abstract1.meet man s1 s2 in
if Abstract1.is_bottom man s then `Bottom else `Value s
- include Domain_builder.No_context
include Domain_builder.Complete
(struct
include D
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 888a0d0cafe..1fd21a94a0c 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -32,7 +32,10 @@ module State = struct
let value_dependencies = Main_values.cval
let location_dependencies = Main_locations.ploc
- include Domain_builder.No_context
+
+ type context = unit
+ let context_dependencies = Abstract_context.Leaf (module Unit_context)
+ let return_context _ = `Value ()
let log_category = Self.dkey_cvalue_domain
diff --git a/src/plugins/eva/domains/domain_builder.ml b/src/plugins/eva/domains/domain_builder.ml
index c67308531fe..c7324a89dbc 100644
--- a/src/plugins/eva/domains/domain_builder.ml
+++ b/src/plugins/eva/domains/domain_builder.ml
@@ -36,6 +36,10 @@ end
module type LeafDomain = sig
type t
+ type context = unit
+ val context_dependencies: context Abstract_context.dependencies
+ val return_context: t -> context or_bottom
+
val backward_location: t -> lval -> typ -> 'loc -> 'v -> ('loc * 'v) or_bottom
val reduce_further: t -> exp -> 'v -> (exp * 'v) list
@@ -66,16 +70,11 @@ module type LeafDomain = sig
end
+module Complete (Domain: InputDomain) = struct
-module No_context = struct
type context = unit
let context_dependencies = Abstract_context.Leaf (module Unit_context)
let return_context _ = `Value ()
-end
-
-
-
-module Complete (Domain: InputDomain) = struct
let backward_location _state _lval _typ loc value = `Value (loc, value)
let reduce_further _state _expr _value = []
@@ -119,7 +118,6 @@ let simplify_call call =
module Make_Minimal
- (Context : Abstract_context.Leaf)
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
(Domain: Simpler_domains.Minimal)
@@ -129,14 +127,11 @@ module Make_Minimal
let log_category = Self.register_category ("d-" ^ name)
- type context = Context.t
type value = Value.t
type location = Location.location
type state = Domain.t
type origin
- let return_context _ = `Value Context.top
- let context_dependencies = Abstract_context.Leaf (module Context)
let value_dependencies = Abstract_value.Leaf (module Value)
let location_dependencies = Abstract_location.Leaf (module Location)
@@ -181,14 +176,13 @@ end
module Complete_Minimal
- (Context : Abstract_context.Leaf)
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
(Domain: Simpler_domains.Minimal)
= struct
module D = struct
- include Make_Minimal (Context) (Value) (Location) (Domain)
+ include Make_Minimal (Value) (Location) (Domain)
include
(Datatype.Make_with_collections
@@ -213,7 +207,6 @@ end
module Complete_Minimal_with_datatype
- (Context : Abstract_context.Leaf)
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
(Domain: Minimal_with_datatype)
@@ -221,7 +214,7 @@ module Complete_Minimal_with_datatype
module D = struct
- include Make_Minimal (Context) (Value) (Location) (Domain)
+ include Make_Minimal (Value) (Location) (Domain)
include
(Datatype.With_collections
@@ -254,8 +247,6 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
type state = Domain.t
type origin
- include No_context
-
let value_dependencies = Abstract_value.Leaf (module Main_values.CVal)
let location_dependencies = Abstract_location.Leaf (module Main_locations.PLoc)
diff --git a/src/plugins/eva/domains/domain_builder.mli b/src/plugins/eva/domains/domain_builder.mli
index 568c5509ec2..7f24bb4a8c9 100644
--- a/src/plugins/eva/domains/domain_builder.mli
+++ b/src/plugins/eva/domains/domain_builder.mli
@@ -40,6 +40,10 @@ end
module type LeafDomain = sig
type t
+ type context = unit
+ val context_dependencies: context Abstract_context.dependencies
+ val return_context: t -> context or_bottom
+
val backward_location: t -> lval -> typ -> 'loc -> 'v -> ('loc * 'v) or_bottom
val reduce_further: t -> exp -> 'v -> (exp * 'v) list
@@ -69,31 +73,23 @@ module type LeafDomain = sig
val key: t Abstract_domain.key
end
-module No_context : sig
- type context = unit
- val context_dependencies : context Abstract_context.dependencies
- val return_context : 'a -> context Eval.or_bottom
-end
-
(** Automatically builds some functions of an abstract domain. *)
module Complete (Domain: InputDomain) : LeafDomain with type t := Domain.t
module Complete_Minimal
- (Context : Abstract_context.Leaf)
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
(Domain: Simpler_domains.Minimal)
- : Abstract_domain.Leaf with type context = Context.t
+ : Abstract_domain.Leaf with type context = unit
and type value = Value.t
and type location = Location.location
and type state = Domain.t
module Complete_Minimal_with_datatype
- (Context : Abstract_context.Leaf)
(Value: Abstract_value.Leaf)
(Location: Abstract_location.Leaf)
(Domain: Simpler_domains.Minimal_with_datatype)
- : Abstract_domain.Leaf with type context = Context.t
+ : Abstract_domain.Leaf with type context = unit
and type value = Value.t
and type location = Location.location
and type state = Domain.t
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index a1e82cd863a..4fc078eb9d2 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -1125,7 +1125,6 @@ module D : Abstract_domain.Leaf
include G
include Domain_builder.Complete (struct include G let top = empty end)
- include Domain_builder.No_context
let log_category = dkey
diff --git a/src/plugins/eva/domains/inout_domain.ml b/src/plugins/eva/domains/inout_domain.ml
index 728c892b7d4..db4680480a4 100644
--- a/src/plugins/eva/domains/inout_domain.ml
+++ b/src/plugins/eva/domains/inout_domain.ml
@@ -220,7 +220,6 @@ module Domain = struct
end)
include Domain_builder.Complete (LatticeInout)
- include Domain_builder.No_context
let log_category = Self.register_category "d-inout"
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 92f546a13bf..c34c84acc99 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -664,7 +664,6 @@ module Domain =
struct
include DomainLattice
include Domain_builder.Complete (DomainLattice)
- include Domain_builder.No_context
(* Eva Queries *)
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index eab6d98444a..33be2920a29 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -1600,7 +1600,6 @@ module Domain = struct
include State
include Domain_builder.Complete (State)
- include Domain_builder.No_context
type value = Cvalue.V.t
type location = Precise_locs.precise_location
diff --git a/src/plugins/eva/domains/offsm_domain.ml b/src/plugins/eva/domains/offsm_domain.ml
index 652cca15035..806d306d6f7 100644
--- a/src/plugins/eva/domains/offsm_domain.ml
+++ b/src/plugins/eva/domains/offsm_domain.ml
@@ -110,7 +110,6 @@ module D : Abstract_domain.Leaf
end)
include Domain_builder.Complete (Memory)
- include Domain_builder.No_context
let log_category = dkey
diff --git a/src/plugins/eva/domains/simple_memory.ml b/src/plugins/eva/domains/simple_memory.ml
index d0356313438..d2c81be458b 100644
--- a/src/plugins/eva/domains/simple_memory.ml
+++ b/src/plugins/eva/domains/simple_memory.ml
@@ -188,7 +188,6 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
include M
include Domain_builder.Complete (M)
- include Domain_builder.No_context
type state = t
type value = Value.t
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index 1a5ebf09887..0719ce81c89 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -472,7 +472,6 @@ module D : Abstract_domain.Leaf
end)
include Domain_builder.Complete (Memory)
- include Domain_builder.No_context
let log_category = dkey
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index e0b0d4f3c07..d20a13adf8a 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -310,7 +310,6 @@ module Domain = struct
end)
include Domain_builder.Complete (LatticeTaint)
- include Domain_builder.No_context
include QueriesTaint
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index d631c13e358..53eb03a0032 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -1089,7 +1089,6 @@ module D = struct
type location = Precise_locs.precise_location
type origin
- include Domain_builder.No_context
let value_dependencies = Main_values.cval
let location_dependencies = Main_locations.ploc
diff --git a/src/plugins/eva/domains/unit_domain.ml b/src/plugins/eva/domains/unit_domain.ml
index 378f0437b30..0d05955f190 100644
--- a/src/plugins/eva/domains/unit_domain.ml
+++ b/src/plugins/eva/domains/unit_domain.ml
@@ -25,7 +25,6 @@ let log_key = Self.register_category "unit-domain"
module Static = struct
module D = struct
include Datatype.Unit
- include Domain_builder.No_context
type state = t
let name = "unit"
--
GitLab