From 835eaf3fb065677567d66ae520686b7fe943e896 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 6 Sep 2019 13:35:47 +0200
Subject: [PATCH] [Eva] Minor simplification of Db.Value and domain_store.
---
src/kernel_services/plugin_entry_points/db.ml | 21 +++++++------------
.../plugin_entry_points/db.mli | 7 ++++---
src/plugins/value/domains/domain_store.ml | 12 +++++++----
3 files changed, 20 insertions(+), 20 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 7a20c487788..e88014be4f9 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -530,17 +530,14 @@ module Value = struct
if !no_results (Kernel_function.(get_definition (find_englobing_kf s)))
then Cvalue.Model.top
else
- 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
+ let (find, add), find_by_callstack =
+ if after
+ then AfterTable.(find, add), AfterTable_By_Callstack.find
+ else Table.(find, add), Table_By_Callstack.find
+ in
+ try find s
with Not_found ->
- let ho =
- try
- Some (if after then AfterTable_By_Callstack.find s else
- Table_By_Callstack.find s)
- with Not_found -> None in
+ let ho = try Some (find_by_callstack s) with Not_found -> None in
let state =
match ho with
| None -> Cvalue.Model.bottom
@@ -549,7 +546,7 @@ module Value = struct
Cvalue.Model.join acc state
) h Cvalue.Model.bottom
in
- Tbl.add s state;
+ add s state;
state
let noassert_get_state ?(after=false) k =
@@ -559,12 +556,10 @@ module Value = struct
noassert_get_stmt_state ~after 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 ~after s
let get_state ?(after=false) k =
- (* [QB]: false was previous default. *)
assert (is_computed ()); (* this assertion fails during value analysis *)
noassert_get_state ~after k
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 74f81d20817..fe390a2c327 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -266,13 +266,14 @@ module Value : sig
val get_initial_state_callstack :
kernel_function -> state Value_types.Callstack.Hashtbl.t option
val get_state : ?after:bool -> kinstr -> state
-
+ (** [after] is false by default. *)
val get_stmt_state_callstack:
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t option
val get_stmt_state : ?after:bool -> stmt -> state
- (** @plugin development guide *)
+ (** [after] is false by default.
+ @plugin development guide *)
val fold_stmt_state_callstack :
(state -> 'a -> 'a) -> 'a -> after:bool -> stmt -> 'a
@@ -521,7 +522,7 @@ module Value : sig
val noassert_get_state : ?after:bool -> kinstr -> state
(** To be used during the value analysis itself (instead of
- {!get_state}). *)
+ {!get_state}). [after] is false by default. *)
val recursive_call_occurred: kernel_function -> unit
diff --git a/src/plugins/value/domains/domain_store.ml b/src/plugins/value/domains/domain_store.ml
index 150129f159c..592b14ca41d 100644
--- a/src/plugins/value/domains/domain_store.ml
+++ b/src/plugins/value/domains/domain_store.ml
@@ -212,10 +212,14 @@ module Make (Domain: InputDomain) = struct
if not (Storage.get ())
then `Value Domain.top
else
- try `Value ((if after then AfterTable.find else Table.find) s)
+ let (find, add), find_by_callstack =
+ if after
+ then AfterTable.(find, add), AfterTable_By_Callstack.find
+ else Table.(find, add), Table_By_Callstack.find
+ in
+ try `Value (find s)
with Not_found ->
- let ho = try Some ((if after then AfterTable_By_Callstack.find
- else Table_By_Callstack.find) s) with Not_found -> None in
+ let ho = try Some (find_by_callstack s) with Not_found -> None in
let state =
match ho with
| None -> `Bottom
@@ -224,7 +228,7 @@ module Make (Domain: InputDomain) = struct
(fun _cs state acc -> Bottom.join Domain.join acc (`Value state))
h `Bottom
in
- ignore (state >>-: (if after then AfterTable.add else Table.add) s);
+ ignore (state >>-: add s);
state
let get_stmt_state_by_callstack ~after stmt =
--
GitLab