From 3d6dbaa1e4458b0dba5da13b934380d32615f48d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 17 Jan 2022 22:24:14 +0100
Subject: [PATCH] [Eva] New Frama-C state Self.state to replace Db.Value.self.
---
src/kernel_services/plugin_entry_points/db.ml | 25 ++++++-------------
.../plugin_entry_points/db.mli | 2 ++
src/plugins/value/parameters.ml | 5 ++--
src/plugins/value/self.ml | 14 +++++++++++
src/plugins/value/self.mli | 3 +++
5 files changed, 29 insertions(+), 20 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index b63abe98dc9..950e5d6150e 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -266,14 +266,10 @@ module Value = struct
let globals_use_supplied_state () = not (VGlobals.get_option () = None)
- (* Do NOT add dependencies to Kernel parameters here, but at the top of
- Value/Value_parameters *)
- let dependencies =
- [ Ast.self;
- Alarms.self;
- Annotations.code_annot_state;
- FunArgs.self;
- VGlobals.self ]
+ let dependencies = [ FunArgs.self; VGlobals.self ]
+ let proxy = State_builder.Proxy.(create "eva_db" Forward dependencies)
+ let self = State_builder.Proxy.get proxy
+ let only_self = [ self ]
let size = 256
@@ -285,14 +281,14 @@ module Value = struct
(struct
let name = "Db.Value.Table_By_Callstack"
let size = size
- let dependencies = dependencies
+ let dependencies = [ self ]
end)
module Table =
Cil_state_builder.Stmt_hashtbl(Cvalue.Model)
(struct
let name = "Db.Value.Table"
let size = size
- let dependencies = [ Table_By_Callstack.self ]
+ let dependencies = [ self ]
end)
(* Clear Value's various caches each time [Db.Value.is_computed] is updated,
including when it is set, reset, or during project change. Some operations
@@ -308,26 +304,21 @@ module Value = struct
Function_Froms.Memory.clear_caches ();
)
-
module AfterTable_By_Callstack =
Cil_state_builder.Stmt_hashtbl(States_by_callstack)
(struct
let name = "Db.Value.AfterTable_By_Callstack"
let size = size
- let dependencies = [ Table_By_Callstack.self ]
+ let dependencies = [ self ]
end)
module AfterTable =
Cil_state_builder.Stmt_hashtbl(Cvalue.Model)
(struct
let name = "Db.Value.AfterTable"
let size = size
- let dependencies = [ AfterTable_By_Callstack.self ]
+ let dependencies = [ self ]
end)
-
- let self = Table_By_Callstack.self
- let only_self = [ self ]
-
let mark_as_computed =
Journal.register "Db.Value.mark_as_computed"
(Datatype.func Datatype.unit Datatype.unit)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 636ec1d8bd5..d944d48b154 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -129,6 +129,8 @@ module Value : sig
val emitter: Emitter.t ref
(** Emitter used by Value to emit statuses *)
+ val proxy: State_builder.Proxy.t
+
val self : State.t
(** Internal state of the value analysis from projects viewpoint.
@plugin development guide *)
diff --git a/src/plugins/value/parameters.ml b/src/plugins/value/parameters.ml
index 0b994b78bd7..c03116c950d 100644
--- a/src/plugins/value/parameters.ml
+++ b/src/plugins/value/parameters.ml
@@ -45,9 +45,8 @@ let kernel_parameters_correctness = [
let parameters_correctness = ref Typed_parameter.Set.empty
let parameters_tuning = ref Typed_parameter.Set.empty
let add_dep p =
- State_dependency_graph.add_codependencies
- ~onto:Db.Value.self
- [State.get p.Typed_parameter.name]
+ let state = State.get p.Typed_parameter.name in
+ State_builder.Proxy.extend [state] Self.proxy
let add_correctness_dep p =
if Typed_parameter.Set.mem p !parameters_correctness then
Kernel.abort "adding correctness parameter %a twice"
diff --git a/src/plugins/value/self.ml b/src/plugins/value/self.ml
index 69af425301a..660ac61d9a5 100644
--- a/src/plugins/value/self.ml
+++ b/src/plugins/value/self.ml
@@ -28,6 +28,20 @@ include Plugin.Register
"automatically computes variation domains for the variables of the program"
end)
+(* Do not add dependencies to Kernel parameters here, but at the top of
+ Parameters. *)
+let kernel_dependencies =
+ [ Ast.self;
+ Alarms.self;
+ Annotations.code_annot_state; ]
+
+let dependencies = Db.Value.self :: kernel_dependencies
+
+let proxy = State_builder.Proxy.(create "eva" Forward dependencies)
+let state = State_builder.Proxy.get proxy
+
+let () = State_builder.Proxy.extend [state] Db.Value.proxy
+
let () = Help.add_aliases ~visible:false [ "-value-h"; "-val-h" ]
let () = add_plugin_output_aliases ~visible:false ~deprecated:true [ "value" ]
diff --git a/src/plugins/value/self.mli b/src/plugins/value/self.mli
index 94cd9910a27..cd4de22ea76 100644
--- a/src/plugins/value/self.mli
+++ b/src/plugins/value/self.mli
@@ -22,6 +22,9 @@
include Plugin.General_services
+val proxy: State_builder.Proxy.t
+val state: State.t
+
(** Debug categories responsible for printing initial and final states of Value.
Enabled by default, but can be disabled via the command-line:
-value-msg-key="-initial_state,-final_state" *)
--
GitLab