From 44014604fd949ff354345b3974761f33df19a7fa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 11 Jul 2023 22:37:57 +0200
Subject: [PATCH] [Eva] Removes Conditions_table from the deprecated module
Db.Value.
Records the truth value of conditions in a hashtbl in iterator.ml.
---
src/kernel_services/plugin_entry_points/db.ml | 29 --------
.../plugin_entry_points/db.mli | 7 --
src/plugins/eva/engine/iterator.ml | 71 +++++++++----------
src/plugins/eva/engine/iterator.mli | 5 ++
src/plugins/eva/utils/results.ml | 2 +-
5 files changed, 41 insertions(+), 73 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 4266f7dd127..960480c8c22 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -231,35 +231,6 @@ module Value = struct
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 ]
-
- module Conditions_table =
- Cil_state_builder.Stmt_hashtbl
- (Datatype.Int)
- (struct
- let name = "Db.Value.Conditions_table"
- let size = 101
- let dependencies = only_self
- end)
-
- let merge_conditions h =
- Cil_datatype.Stmt.Hashtbl.iter
- (fun stmt v ->
- try
- let old = Conditions_table.find stmt in
- Conditions_table.replace stmt (old lor v)
- with Not_found ->
- Conditions_table.add stmt v)
- h
-
- let mask_then = 1
- let mask_else = 2
-
- let condition_truth_value s =
- try
- let i = Conditions_table.find s in
- ((i land mask_then) <> 0, (i land mask_else) <> 0)
- with Not_found -> false, false
let compute = mk_fun "Value.compute"
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 7867a74f246..d664470b29d 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -124,10 +124,6 @@ module Value : sig
an incorrect number of them is given.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- val condition_truth_value: stmt -> bool * bool
- (** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
- (resp. snd) is true if and only if the condition of the 'if' has been
- evaluated to true (resp. false) at least once during the analysis. *)
(** {4 Arguments of the main function} *)
@@ -178,9 +174,6 @@ module Value : sig
(**/**)
(** {3 Internal use only} *)
- val merge_conditions: int Cil_datatype.Stmt.Hashtbl.t -> unit
- val mask_then: int
- val mask_else: int
val initial_state_only_globals : (unit -> state) ref
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index 28a09aefb91..899fb601299 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -43,6 +43,33 @@ let blocks_share_locals b1 b2 =
| v1 :: _, v2 :: _ -> v1.vid = v2.vid
| _, _ -> false
+
+module Conditions_table =
+ Cil_state_builder.Stmt_hashtbl
+ (Datatype.Pair (Datatype.Bool) (Datatype.Bool))
+ (struct
+ let name = "Eva.Iterator.Conditions_table"
+ let size = 101
+ let dependencies = [ Self.state ]
+ end)
+
+let condition_truth_value s =
+ try Conditions_table.find s
+ with Not_found -> false, false
+
+let record_fireable edge =
+ match edge.edge_transition with
+ | Guard (_exp, kind, stmt) ->
+ let b_then, b_else = condition_truth_value stmt in
+ let new_status =
+ match kind with
+ | Then -> true, b_else
+ | Else -> b_then, true
+ in
+ Conditions_table.replace stmt new_status
+ | _ -> ()
+
+
module Make_Dataflow
(Abstract : Abstractions.S_with_evaluation)
(States : Powerset.S with type state = Abstract.Dom.t)
@@ -104,10 +131,6 @@ module Make_Dataflow
type tank = Partitioning.tank
type widening = Partitioning.widening
- type edge_info = {
- mutable fireable : bool (* Does any states survive the transition ? *)
- }
-
(* --- Interpreted automata --- *)
@@ -171,7 +194,7 @@ module Make_Dataflow
VertexTable.create control_point_count
let w_table : widening VertexTable.t =
VertexTable.create 7
- let e_table : (tank * edge_info) EdgeTable.t =
+ let e_table : tank EdgeTable.t =
EdgeTable.create transition_count
(* Default (Initial) stores on vertex and edges *)
@@ -179,18 +202,18 @@ module Make_Dataflow
Partitioning.empty_store ~stmt:v.vertex_start_of
let default_vertex_widening (v : vertex) () : widening =
Partitioning.empty_widening ~stmt:v.vertex_start_of
- let default_edge_tank () : tank * edge_info =
- Partitioning.empty_tank (), { fireable = false }
+ let default_edge_tank () : tank =
+ Partitioning.empty_tank ()
(* Get the stores associated to a control point or edge *)
let get_vertex_store (v : vertex) : store =
VertexTable.find_or_add v_table v ~default:(default_vertex_store v)
let get_vertex_widening (v : vertex) : widening =
VertexTable.find_or_add w_table v ~default:(default_vertex_widening v)
- let get_edge_data (e : vertex edge) : tank * edge_info =
+ let get_edge_data (e : vertex edge) : tank =
EdgeTable.find_or_add e_table e ~default:default_edge_tank
let get_succ_tanks (v : vertex) : tank list =
- List.map (fun (_,e,_) -> fst (get_edge_data e)) (G.succ_e graph v)
+ List.map (fun (_,e,_) -> get_edge_data e) (G.succ_e graph v)
module StmtTable = struct
include Cil_datatype.Stmt.Hashtbl
@@ -422,7 +445,7 @@ module Make_Dataflow
let process_edge (v1,e,v2 : G.edge) : flow =
let {edge_transition=transition; edge_kinstr=kinstr} = e in
- let tank,edge_info = get_edge_data e in
+ let tank = get_edge_data e in
let flow = Partitioning.drain tank in
Db.yield ();
check_signals ();
@@ -431,7 +454,7 @@ module Make_Dataflow
let flow = Partitioning.transfer (transfer_transition transition) flow in
let flow = process_partitioning_transitions v1 v2 transition flow in
if not (Partitioning.is_empty_flow flow) then
- edge_info.fireable <- true;
+ record_fireable e;
flow
let gather_cvalues states = match get_cvalue with
@@ -526,7 +549,7 @@ module Make_Dataflow
let reset_component (vertex_list : vertex list) : unit =
let reset_edge (_,e,_) =
- let t,_ = get_edge_data e in
+ let t = get_edge_data e in
Partitioning.reset_tank t
in
let reset_vertex v =
@@ -611,29 +634,6 @@ module Make_Dataflow
(* --- Results conversion --- *)
- let merge_conditions () =
- let table = StmtTable.create 5 in
- let fill (_,e,_) =
- match e.edge_transition with
- | Guard (_exp,kind,stmt) ->
- let mask = match kind with
- | Then -> Db.Value.mask_then
- | Else -> Db.Value.mask_else
- in
- let edge_info = snd (get_edge_data e) in
- let old_status =
- try StmtTable.find table stmt
- with Not_found -> 0
- and status =
- if edge_info.fireable then mask else 0
- in
- let new_status = old_status lor status in
- StmtTable.replace table stmt new_status;
- | _ -> ()
- in
- G.iter_edges_e fill graph;
- Db.Value.merge_conditions table
-
let is_instr s = match s.skind with Instr _ -> true | _ -> false
let states_after_stmt states_before states_after =
@@ -693,7 +693,6 @@ module Make_Dataflow
and register_post = Domain.Store.register_state_after_stmt callstack in
StmtTable.iter register_pre (Lazy.force merged_pre_states);
StmtTable.iter register_post (Lazy.force merged_post_states);
- merge_conditions ();
end;
let states =
Cvalue_callbacks.{ before_stmts = merged_pre_cvalues;
diff --git a/src/plugins/eva/engine/iterator.mli b/src/plugins/eva/engine/iterator.mli
index 0d1f9944063..4c8d02c16bb 100644
--- a/src/plugins/eva/engine/iterator.mli
+++ b/src/plugins/eva/engine/iterator.mli
@@ -25,6 +25,11 @@ open Cil_types
(** Mark the analysis as aborted. It will be stopped at the next safe point *)
val signal_abort: unit -> unit
+(** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
+ (resp. snd) is true if and only if the condition of the 'if' has been
+ evaluated to true (resp. false) at least once during the analysis. *)
+val condition_truth_value: stmt -> bool * bool
+
module Computer
(* Abstractions with the evaluator. *)
(Abstract: Abstractions.S_with_evaluation)
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index bc78a896d00..297a2b22d2e 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -774,7 +774,7 @@ let is_reachable_kinstr kinstr =
let module M = Make () in
M.is_reachable (before_kinstr kinstr)
-let condition_truth_value = Db.Value.condition_truth_value
+let condition_truth_value = Iterator.condition_truth_value
(* Callers / callsites *)
--
GitLab