From e711d912b7800e25e0e8bb28e9fc693be1c6740e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 22 Feb 2022 09:43:12 +0100
Subject: [PATCH] [Eva] Implements [use_spec_instead_of_definition] in
function_calls.
Must be consistent with [define_analysis_target].
---
Makefile | 4 ++--
src/plugins/value/engine/function_calls.ml | 8 ++++++++
src/plugins/value/engine/function_calls.mli | 5 +++++
src/plugins/value/engine/transfer_logic.ml | 2 +-
src/plugins/value/engine/transfer_stmt.ml | 2 +-
src/plugins/value/gui_files/gui_eval.ml | 5 +++--
src/plugins/value/legacy/eval_annots.ml | 2 +-
src/plugins/value/register.ml | 11 ++---------
8 files changed, 23 insertions(+), 16 deletions(-)
diff --git a/Makefile b/Makefile
index 531ba1bf1fa..8a1d9897659 100644
--- a/Makefile
+++ b/Makefile
@@ -899,7 +899,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
domains/cvalue/builtins_watchpoint \
domains/cvalue/builtins_float domains/cvalue/builtins_split \
domains/inout_domain \
- legacy/eval_terms legacy/eval_annots \
+ legacy/eval_terms \
domains/cvalue/cvalue_transfer domains/cvalue/cvalue_init \
domains/cvalue/cvalue_specification \
domains/cvalue/cvalue_domain \
@@ -908,7 +908,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
partitioning/auto_loop_unroll \
partitioning/partition partitioning/partitioning_parameters \
partitioning/partitioning_index partitioning/trace_partitioning \
- engine/recursion engine/function_calls \
+ engine/recursion engine/function_calls legacy/eval_annots \
engine/subdivided_evaluation engine/evaluation engine/abstractions \
engine/transfer_logic engine/transfer_stmt engine/transfer_specification \
engine/mem_exec engine/iterator engine/initialization \
diff --git a/src/plugins/value/engine/function_calls.ml b/src/plugins/value/engine/function_calls.ml
index eff7dbc77a5..7c368ffcbae 100644
--- a/src/plugins/value/engine/function_calls.ml
+++ b/src/plugins/value/engine/function_calls.ml
@@ -123,6 +123,14 @@ let analysis_status kf =
with Not_found -> Unreachable
+(* Must be consistent with the choice made by [analysis_target] below. *)
+let use_spec_instead_of_definition ?(recursion_depth = -1) kf =
+ Ast_info.is_frama_c_builtin (Kernel_function.get_name kf) ||
+ Builtins.is_builtin_overridden kf ||
+ recursion_depth >= Parameters.RecursiveUnroll.get () ||
+ not (Kernel_function.is_definition kf) ||
+ Kernel_function.Set.mem kf (Parameters.UsePrototype.get ())
+
let analysis_target ~recursion_depth callsite kf =
match Builtins.find_builtin_override kf with
| Some (name, builtin, cache, spec) ->
diff --git a/src/plugins/value/engine/function_calls.mli b/src/plugins/value/engine/function_calls.mli
index 698b62406e5..c7efe940d88 100644
--- a/src/plugins/value/engine/function_calls.mli
+++ b/src/plugins/value/engine/function_calls.mli
@@ -40,6 +40,11 @@ type analysis_target =
val define_analysis_target:
?recursion_depth:int -> kinstr -> kernel_function -> analysis_target
+(** Returns true if the Eva analysis use the specification of the given
+ function instead of its body to interpret its calls. *)
+val use_spec_instead_of_definition:
+ ?recursion_depth:int -> kernel_function -> bool
+
(** Returns true if the function has been analyzed. *)
val is_called: kernel_function -> bool
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index d56f52ae0bb..634021c6ecc 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -54,7 +54,7 @@ let pp_p_kind fmt = function
let post_kind kf =
if Builtins.is_builtin_overridden kf
then PostBuiltin
- else if !Db.Value.use_spec_instead_of_definition kf then
+ else if Function_calls.use_spec_instead_of_definition kf then
if Kernel_function.is_definition kf
then PostUseSpec
else PostLeaf
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 8e3c04f6d31..205ad005015 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -85,7 +85,7 @@ let do_copy_at = function
on functions whose body is analyzed. *)
let is_determinate kf =
let name = Kernel_function.get_name kf in
- (warn_indeterminate kf || !Db.Value.use_spec_instead_of_definition kf)
+ (warn_indeterminate kf || Function_calls.use_spec_instead_of_definition kf)
&& not (Ast_info.is_frama_c_builtin name)
let subdivide_stmt = Eva_utils.get_subdivision
diff --git a/src/plugins/value/gui_files/gui_eval.ml b/src/plugins/value/gui_files/gui_eval.ml
index 05ca7822f59..691ec61e3e2 100644
--- a/src/plugins/value/gui_files/gui_eval.ml
+++ b/src/plugins/value/gui_files/gui_eval.ml
@@ -343,7 +343,7 @@ module Make (X: Analysis.S) = struct
let pre = pre_kf kf callstack in
let post = X.Dom.get_cvalue_or_top post in
let result =
- if !Db.Value.use_spec_instead_of_definition kf then
+ if Function_calls.use_spec_instead_of_definition kf then
None
else
let ret_stmt = Kernel_function.find_return kf in
@@ -395,7 +395,8 @@ module Make (X: Analysis.S) = struct
normal termination, and only when the function is called.
After states are not available. *)
let callstacks_at_post kf =
- if not (!Db.Value.use_spec_instead_of_definition kf) && results_kf_computed kf
+ if not (Function_calls.use_spec_instead_of_definition kf)
+ && results_kf_computed kf
then
let ret = Kernel_function.find_return kf in
let states_before = X.get_stmt_state_by_callstack ~after:true ret in
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index 8c83557fd2a..4bf41555291 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -109,7 +109,7 @@ let mark_unreachable () =
Visitor.visitFramacFileFunctions unreach (Ast.get ())
let c_labels kf cs =
- if !Db.Value.use_spec_instead_of_definition kf then
+ if Function_calls.use_spec_instead_of_definition kf then
Cil_datatype.Logic_label.Map.empty
else
let fdec = Kernel_function.get_definition kf in
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index c1e1695ae85..8732d620e1a 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -124,14 +124,6 @@ let find_deps_term_no_transitivity_state state t =
r.Eval_terms.ldeps
with Eval_terms.LogicEvalError _ -> raise Db.From.Not_lval
-(* If the function is a builtin, or if the user has requested it, use
- \assigns and \from clauses, that give an approximation of the result *)
-let use_spec_instead_of_definition kf =
- not (Kernel_function.is_definition kf) ||
- Ast_info.is_frama_c_builtin (Kernel_function.get_name kf) ||
- Builtins.is_builtin_overridden kf ||
- Kernel_function.Set.mem kf (Parameters.UsePrototype.get ())
-
let eval_predicate ~pre ~here p =
let open Eval_terms in
let env = env_annot ~pre ~here () in
@@ -153,7 +145,8 @@ let valid_behaviors kf state =
let () =
(* Pretty-printing *)
- Db.Value.use_spec_instead_of_definition := use_spec_instead_of_definition;
+ Db.Value.use_spec_instead_of_definition :=
+ Function_calls.use_spec_instead_of_definition;
Db.Value.assigns_outputs_to_zone := assigns_outputs_to_zone;
Db.Value.assigns_outputs_to_locations := assigns_outputs_to_locations;
Db.Value.assigns_inputs_to_zone := assigns_inputs_to_zone;
--
GitLab