From e86fc9974755c162e9a53b67806dd529ba555d3b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 3 Aug 2023 10:31:58 +0200
Subject: [PATCH] [Eva] Db.Value.globals_state returns the initial state
supplied externally.
And no longer the cvalue initial state normally computed by the analysis,
when no initial state is supplied externally.
The initial cvalue state can always be accessed from Cvalue_results.
Removes [initial_state_only_globals] from Db.Value.
---
src/kernel_services/plugin_entry_points/db.ml | 7 +------
.../plugin_entry_points/db.mli | 7 ++-----
src/plugins/eva/engine/analysis.ml | 9 ---------
src/plugins/eva/engine/compute_functions.ml | 2 --
src/plugins/eva/engine/compute_functions.mli | 3 ---
src/plugins/eva/engine/initialization.ml | 19 +++++--------------
src/plugins/eva/engine/initialization.mli | 5 -----
src/plugins/eva/legacy/eval_terms.ml | 6 ++++--
src/plugins/eva/utils/eva_results.ml | 10 ++++++----
9 files changed, 18 insertions(+), 50 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 960480c8c22..469c3aed3c6 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -219,12 +219,7 @@ module Value = struct
if VGlobals.get_option () <> None then
(!initial_state_changed (); VGlobals.clear ())
- let initial_state_only_globals = mk_fun "Value.initial_state_only_globals"
-
- let globals_state () =
- match VGlobals.get_option () with
- | Some v -> v
- | None -> !initial_state_only_globals ()
+ let globals_state () = VGlobals.get_option ()
let globals_use_supplied_state () = not (VGlobals.get_option () = None)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index d664470b29d..9344f5d1c24 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -161,8 +161,8 @@ module Value : sig
val globals_use_default_initial_state : unit -> unit
- (** Initial state used by the analysis *)
- val globals_state : unit -> state
+ (** Initial state provided by [globals_set_initial_state], if any. *)
+ val globals_state : unit -> state option
(** @return [true] if the initial state for globals used by the value
@@ -174,9 +174,6 @@ module Value : sig
(**/**)
(** {3 Internal use only} *)
-
- val initial_state_only_globals : (unit -> state) ref
-
val initial_state_changed: (unit -> unit) ref
end
[@@alert db_deprecated
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index 6bbfef27ba4..06aa0bce44b 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -88,7 +88,6 @@ module type Analyzer = sig
include S
val compute_from_entry_point : kernel_function -> lib_entry:bool -> unit
(* val compute_from_init_state: kernel_function -> Dom.t -> unit *)
- val initial_state: lib_entry:bool -> Dom.t or_bottom
end
@@ -181,14 +180,6 @@ let set_current_analyzer config (analyzer: (module Analyzer)) =
Analyzer_Hook.apply (module (val analyzer): S);
ref_analyzer := (config, analyzer)
-let cvalue_initial_state () =
- let module A = (val snd !ref_analyzer) in
- let module G = (Cvalue_domain.Getters (A.Dom)) in
- let _, lib_entry = Globals.entry_point () in
- G.get_cvalue_or_bottom (A.initial_state ~lib_entry)
-
-let () = Db.Value.initial_state_only_globals := cvalue_initial_state
-
(* Builds the Analyzer module corresponding to a given configuration,
and sets it as the current analyzer. *)
let make_analyzer config =
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index d46426ab057..59f8a8d9a4e 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -167,8 +167,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
include Cvalue_domain.Getters (Abstract.Dom)
- let initial_state = Init.initial_state
-
let get_cval =
match Abstract.Val.get Main_values.CVal.key with
| None -> fun _ -> assert false
diff --git a/src/plugins/eva/engine/compute_functions.mli b/src/plugins/eva/engine/compute_functions.mli
index 28f78965dbb..b582766632a 100644
--- a/src/plugins/eva/engine/compute_functions.mli
+++ b/src/plugins/eva/engine/compute_functions.mli
@@ -23,7 +23,6 @@
(** Value analysis of entire functions, using Eva engine. *)
open Cil_types
-open Eval
module Make (Abstract: Abstractions.S_with_evaluation)
: sig
@@ -33,6 +32,4 @@ module Make (Abstract: Abstractions.S_with_evaluation)
(** Compute a call to the main function from the given initial state. *)
val compute_from_init_state: kernel_function -> Abstract.Dom.t -> unit
-
- val initial_state: lib_entry:bool -> Abstract.Dom.t or_bottom
end
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index da1ac7627c2..572cbf09e68 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -27,7 +27,6 @@ open Eval
module type S = sig
type state
- val initial_state : lib_entry:bool -> state or_bottom
val initial_state_with_formals :
lib_entry:bool -> kernel_function -> state or_bottom
val initialize_local_variable:
@@ -357,19 +356,13 @@ module Make
InitialState.memo (compute_global_state ~lib_entry)
(* The global cvalue state may be supplied by the user. *)
- let supplied_state () =
- let cvalue_state = Db.Value.globals_state () in
+ let supplied_state cvalue_state =
if Cvalue.Model.is_reachable cvalue_state
then
let cvalue_state = cvalue_state, Locals_scoping.bottom () in
`Value (Domain.set Cvalue_domain.State.key cvalue_state Domain.top)
else `Bottom
- let initial_state ~lib_entry =
- if Db.Value.globals_use_supplied_state ()
- then supplied_state ()
- else global_state ~lib_entry
-
let print_initial_cvalue_state state =
let cvalue_state = get_cvalue_or_bottom state in
(* Do not show variables from the frama-c libc specifications. *)
@@ -391,18 +384,16 @@ module Make
let initial_state_with_formals ~lib_entry kf =
let init_state =
- if Db.Value.globals_use_supplied_state ()
- then begin
+ match Db.Value.globals_state () with
+ | Some state ->
Self.feedback "Initial state supplied by user";
- supplied_state ()
- end
- else begin
+ supplied_state state
+ | None ->
let pp = Parameters.ValShowProgress.get () in
if pp then Self.feedback "Computing initial state";
let state = global_state ~lib_entry in
if pp then Self.feedback "Initial state computed";
state
- end
in
let b = Parameters.ResultsAll.get () in
Domain.Store.register_global_state b init_state;
diff --git a/src/plugins/eva/engine/initialization.mli b/src/plugins/eva/engine/initialization.mli
index 872206abe61..e669a8df56c 100644
--- a/src/plugins/eva/engine/initialization.mli
+++ b/src/plugins/eva/engine/initialization.mli
@@ -28,11 +28,6 @@ open Lattice_bounds
module type S = sig
type state
- (** Compute the initial state for an analysis. The initial state is generated
- according to the options of Value governing the shape of this state.
- All global variables are bound in the resulting abstract state. *)
- val initial_state : lib_entry:bool -> state or_bottom
-
(** Compute the initial state for an analysis (as in {!initial_state}),
but also bind the formal parameters of the function given as argument. *)
val initial_state_with_formals :
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 72e58f5421a..0eceb70bf48 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -238,8 +238,10 @@ let add_pre = add_logic Logic_const.pre_label
let add_post = add_logic Logic_const.post_label
let add_old = add_logic Logic_const.old_label
(* Init is a bit special, it is constant and always added to the initial state*)
-let add_init state =
- add_logic Logic_const.init_label (Db.Value.globals_state ()) state
+let add_init states =
+ match Cvalue_results.get_global_state () with
+ | `Bottom -> states
+ | `Value state -> add_logic Logic_const.init_label state states
let add_logic_var env lv cvalue =
{ env with logic_vars = LogicVarEnv.add lv cvalue env.logic_vars }
diff --git a/src/plugins/eva/utils/eva_results.ml b/src/plugins/eva/utils/eva_results.ml
index 606158151f6..c3fb17411b7 100644
--- a/src/plugins/eva/utils/eva_results.ml
+++ b/src/plugins/eva/utils/eva_results.ml
@@ -57,7 +57,7 @@ type results = {
after_states: stmt_by_callstack Stmt.Hashtbl.t;
kf_initial_states: stmt_by_callstack Kernel_function.Hashtbl.t;
kf_callers: Function_calls.t;
- initial_state: Cvalue.Model.t;
+ initial_state: Cvalue.Model.t Lattice_bounds.or_bottom;
initial_args: Cvalue.V.t list option;
alarms: Property_status.emitted_status AlarmsStmt.Hashtbl.t;
statuses: Property_status.emitted_status Property.Hashtbl.t
@@ -93,7 +93,7 @@ let get_results () =
in
Globals.Functions.iter copy_kf;
let kf_callers = Function_calls.get_results () in
- let initial_state = Db.Value.globals_state () in
+ let initial_state = Cvalue_results.get_global_state () in
let initial_args = Db.Value.fun_get_args () in
let aux_statuses f_status ip =
let aux_any_status e status =
@@ -133,7 +133,7 @@ let set_results results =
Project.clear ~selection ();
(* Those two functions may clear Self.state. Start by them *)
(* Initial state *)
- Db.Value.globals_set_initial_state results.initial_state;
+ Cvalue_results.register_global_state true results.initial_state;
(* Initial args *)
begin match results.initial_args with
| None -> Db.Value.fun_use_default_args ()
@@ -254,7 +254,9 @@ let merge r1 r2 =
let kf_callers = Function_calls.merge_results r1.kf_callers r2.kf_callers in
let alarms = AlarmsStmtH.merge merge_statuses r1.alarms r2.alarms in
let statuses = PropertyH.merge merge_statuses r1.statuses r2.statuses in
- let initial_state = Cvalue.Model.join r1.initial_state r2.initial_state in
+ let initial_state =
+ Lattice_bounds.Bottom.join Cvalue.Model.join r1.initial_state r2.initial_state
+ in
let initial_args =
match main, r1.initial_args, r2.initial_args with
| None, _, _ | _, None, _ | _, _, None -> None
--
GitLab