From ab9e0988286dc744a18e384901e15c2c4b2ecddb Mon Sep 17 00:00:00 2001
From: Bouillaguet Quentin <quentin.bouillaguet@cea.fr>
Date: Wed, 23 Jan 2019 16:38:05 +0100
Subject: [PATCH] [Eva] No default for after in Abstract Domains
---
src/kernel_services/plugin_entry_points/db.ml | 38 ++++++++++++++-----
.../plugin_entry_points/db.mli | 6 +--
src/plugins/from/functionwise.ml | 2 +-
src/plugins/inout/operational_inputs.ml | 2 +-
src/plugins/value/domains/abstract_domain.mli | 2 +-
.../value/domains/cvalue/cvalue_domain.ml | 4 +-
src/plugins/value/domains/domain_product.ml | 6 +--
src/plugins/value/domains/domain_store.ml | 2 +-
src/plugins/value/engine/analysis.ml | 12 +++---
src/plugins/value/engine/analysis.mli | 4 +-
src/plugins/value/gui_files/register_gui.ml | 2 +-
11 files changed, 50 insertions(+), 30 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index baad021381a..7a20c487788 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -316,6 +316,13 @@ module Value = struct
let size = size
let dependencies = [ Table_By_Callstack.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 ]
+ end)
let self = Table_By_Callstack.self
@@ -519,13 +526,21 @@ module Value = struct
let add_formals_to_state = mk_fun "add_formals_to_state"
- let noassert_get_stmt_state s =
+ let noassert_get_stmt_state ~after s =
if !no_results (Kernel_function.(get_definition (find_englobing_kf s)))
then Cvalue.Model.top
else
- try Table.find s
+ let tbl : (module State_builder.Hashtbl with type key = Cil_types.stmt
+ and type data = Cvalue.Model.t) =
+ if after then (module AfterTable) else (module Table) in
+ let module Tbl = (val tbl) in
+ try Tbl.find s
with Not_found ->
- let ho = try Some (Table_By_Callstack.find s) with Not_found -> None in
+ let ho =
+ try
+ Some (if after then AfterTable_By_Callstack.find s else
+ Table_By_Callstack.find s)
+ with Not_found -> None in
let state =
match ho with
| None -> Cvalue.Model.bottom
@@ -534,21 +549,24 @@ module Value = struct
Cvalue.Model.join acc state
) h Cvalue.Model.bottom
in
- Table.add s state;
+ Tbl.add s state;
state
- let noassert_get_state k =
+ let noassert_get_state ?(after=false) k =
match k with
| Kglobal -> globals_state ()
- | Kstmt s -> noassert_get_stmt_state s
+ | Kstmt s ->
+ noassert_get_stmt_state ~after s
- let get_stmt_state s =
+ let get_stmt_state ?(after=false) s =
+ (* [QB]: false was previous default. *)
assert (is_computed ()); (* this assertion fails during value analysis *)
- noassert_get_stmt_state s
+ noassert_get_stmt_state ~after s
- let get_state k =
+ let get_state ?(after=false) k =
+ (* [QB]: false was previous default. *)
assert (is_computed ()); (* this assertion fails during value analysis *)
- noassert_get_state k
+ noassert_get_state ~after k
let get_stmt_state_callstack ~after stmt =
assert (is_computed ()); (* this assertion fails during value analysis *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index cd627fbe685..74f81d20817 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -265,13 +265,13 @@ module Value : sig
val get_initial_state : kernel_function -> state
val get_initial_state_callstack :
kernel_function -> state Value_types.Callstack.Hashtbl.t option
- val get_state : kinstr -> state
+ val get_state : ?after:bool -> kinstr -> state
val get_stmt_state_callstack:
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t option
- val get_stmt_state : stmt -> state
+ val get_stmt_state : ?after:bool -> stmt -> state
(** @plugin development guide *)
val fold_stmt_state_callstack :
@@ -519,7 +519,7 @@ module Value : sig
(**/**)
(** {3 Internal use only} *)
- val noassert_get_state : kinstr -> state
+ val noassert_get_state : ?after:bool -> kinstr -> state
(** To be used during the value analysis itself (instead of
{!get_state}). *)
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index 66d83674fe4..3233b733bfc 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -37,7 +37,7 @@ let () = From_parameters.ForceDeps.set_output_dependencies [Tbl.self]
let force_compute = ref (fun _ -> assert false)
module To_Use = struct
- let get_value_state = Db.Value.get_stmt_state
+ let get_value_state s = Db.Value.get_stmt_state s
let memo kf =
Tbl.memo
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 1c070d2ddf9..3df4c008632 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -699,7 +699,7 @@ module FunctionWise = struct
let module Computer = Computer(Fenv)(struct
let _version = "functionwise"
let _kf = kf
- let stmt_state = Db.Value.get_stmt_state
+ let stmt_state s = Db.Value.get_stmt_state s
let at_call stmt kf = get_external_aux ~stmt kf
end) in
Stack.iter
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 4a1da6a9352..ca999ade675 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -481,7 +481,7 @@ module type Store = sig
val get_initial_state_by_callstack:
kernel_function -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
- val get_stmt_state: ?after:bool -> stmt -> state or_bottom
+ val get_stmt_state: after:bool -> stmt -> state or_bottom
val get_stmt_state_by_callstack:
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
end
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index f3b0fe3d1c8..841850c4fef 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -473,7 +473,9 @@ module State = struct
| None -> `Bottom
else `Top
- let get_stmt_state ?(after=false) stmt = assert (not after); return (Db.Value.get_stmt_state stmt)
+ let get_stmt_state ~after stmt =
+ return (Db.Value.get_stmt_state ~after stmt)
+
let get_stmt_state_by_callstack ~after stmt =
if Storage.get ()
then
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index d75ccc84f22..e596deec5d4 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -366,9 +366,9 @@ module Make
and right_tbl = Right.Store.get_initial_state_by_callstack kf in
merge_callstack_tbl left_tbl right_tbl
- let get_stmt_state ?after stmt =
- Left.Store.get_stmt_state ?after stmt >>- fun left ->
- Right.Store.get_stmt_state ?after stmt >>-: fun right ->
+ let get_stmt_state ~after stmt =
+ Left.Store.get_stmt_state ~after stmt >>- fun left ->
+ Right.Store.get_stmt_state ~after stmt >>-: fun right ->
left, right
let get_stmt_state_by_callstack ~after stmt =
let left_tbl = Left.Store.get_stmt_state_by_callstack ~after stmt
diff --git a/src/plugins/value/domains/domain_store.ml b/src/plugins/value/domains/domain_store.ml
index 2341f4e22a0..150129f159c 100644
--- a/src/plugins/value/domains/domain_store.ml
+++ b/src/plugins/value/domains/domain_store.ml
@@ -208,7 +208,7 @@ module Make (Domain: InputDomain) = struct
try `Value (Called_Functions_By_Callstack.find kf)
with Not_found -> `Bottom
- let get_stmt_state ?(after=false) s =
+ let get_stmt_state ~after s =
if not (Storage.get ())
then `Value Domain.top
else
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 14728aa4d7e..fd3cf68003b 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -28,8 +28,8 @@ module type Results = sig
type value
type location
- val get_stmt_state : stmt -> state or_bottom
- val get_kinstr_state: kinstr -> state or_bottom
+ val get_stmt_state : after:bool -> stmt -> state or_bottom
+ val get_kinstr_state: after:bool -> kinstr -> state or_bottom
val get_stmt_state_by_callstack:
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
val get_initial_state_by_callstack:
@@ -67,15 +67,15 @@ module Make (Abstract: Abstractions.S) = struct
include Abstract
include Compute_functions.Make (Abstract)
- let get_stmt_state stmt =
+ let get_stmt_state ~after stmt =
let fundec = Kernel_function.(get_definition (find_englobing_kf stmt)) in
if Mark_noresults.should_memorize_function fundec && Db.Value.is_computed ()
- then Abstract.Dom.Store.get_stmt_state stmt
+ then Abstract.Dom.Store.get_stmt_state ~after stmt
else `Value Abstract.Dom.top
- let get_kinstr_state = function
+ let get_kinstr_state ~after = function
| Kglobal -> Abstract.Dom.Store.get_global_state ()
- | Kstmt stmt -> get_stmt_state stmt
+ | Kstmt stmt -> get_stmt_state ~after stmt
let get_stmt_state_by_callstack =
Abstract.Dom.Store.get_stmt_state_by_callstack
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index 4ecfde378fd..89316e76c4c 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -28,8 +28,8 @@ module type Results = sig
type value
type location
- val get_stmt_state : stmt -> state or_bottom
- val get_kinstr_state: kinstr -> state or_bottom
+ val get_stmt_state : after:bool -> stmt -> state or_bottom
+ val get_kinstr_state: after:bool -> kinstr -> state or_bottom
val get_stmt_state_by_callstack:
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
val get_initial_state_by_callstack:
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index d455fab0fdc..7892476419f 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -519,7 +519,7 @@ module Select (Eval: Eval) = struct
(* Function pointers *)
(* get the list of functions in the values *)
let e = Value_util.lval_to_exp lv in
- match Eval.Analysis.get_kinstr_state ki with
+ match Eval.Analysis.get_kinstr_state ~after:false ki with
| `Bottom -> ()
| `Value state ->
let funs, _ = Eval.Analysis.eval_function_exp state e in
--
GitLab