From 1d40be1aefbdfa1680787739ca759c14535d4c44 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 11 Sep 2023 09:15:19 +0200
Subject: [PATCH] [Eva] Fixes the generation of assigns clauses required for
Eva.
- Only generates assigns clauses when required:
- when the analysis uses the specification to analyze a function
(decided in function_calls.ml)
- for Frama_C_* builtins, such as Frama_C_assert. Others builtins should
already have a specification.
- when interpreting a Frama_C_show_each directive, so other plugins known
these functions have no effect.
- in [Logic_inout.valid_behaviors], used by inout and from plugins to
interpret a function specification.
- Also generates assigns clauses for functions with a body: this is required
for the analysis of recursive functions and of functions specified in the
-eva-use-spec parameter (in both case, a specific Eva warning is emitted).
- In recursion.ml, renames get_spec to check_spec.
The generation of assigns clauses is now uniformly done in function_calls.
---
src/plugins/eva/domains/cvalue/builtins.ml | 6 ++-
src/plugins/eva/engine/compute_functions.ml | 5 +--
src/plugins/eva/engine/function_calls.ml | 18 ++++++---
src/plugins/eva/engine/recursion.ml | 43 ++++++---------------
src/plugins/eva/engine/recursion.mli | 2 +-
src/plugins/eva/engine/transfer_logic.ml | 3 --
src/plugins/eva/engine/transfer_stmt.ml | 3 ++
src/plugins/eva/legacy/logic_inout.ml | 4 +-
8 files changed, 35 insertions(+), 49 deletions(-)
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index 3eec1afe396..4dc7cb838a7 100644
--- a/src/plugins/eva/domains/cvalue/builtins.ml
+++ b/src/plugins/eva/domains/cvalue/builtins.ml
@@ -118,7 +118,11 @@ let () =
(* Returns the specification of a builtin, used to evaluate preconditions
and to transfer the states of other domains. *)
let find_builtin_specification kf =
- Populate_spec.(populate_funspec kf [`Assigns]);
+ (* Functions for which a builtin is used should have a specification, except
+ Frama_C_* builtins such as Frama_C_assert, for which we generate an empty
+ specification with assigns clauses. *)
+ if String.starts_with ~prefix:"Frama_C" (Kernel_function.get_name kf)
+ then Populate_spec.populate_funspec kf [`Assigns];
let spec = Annotations.funspec kf in
(* The specification can be empty if [kf] has a body but no specification,
in which case [Annotations.funspec] does not generate a specification.
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index cee61d66501..bc9d3599351 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -79,13 +79,12 @@ let plugins_ok () =
let generate_specs () =
let aux kf =
if need_assigns kf then begin
- let funspec = Annotations.funspec kf in
Self.warning "Generating potentially incorrect assigns \
for function '%a' for which option %s is set"
Kernel_function.pretty kf Parameters.UsePrototype.option_name;
- (* The function populate_spec may emit a warning. Position a loc. *)
+ (* The function populate_funspec may emit a warning. Position a loc. *)
Cil.CurrentLoc.set (Kernel_function.get_location kf);
- Populate_spec.(populate_funspec ~funspec kf [`Assigns]);
+ Populate_spec.(populate_funspec ~do_body:true kf [`Assigns]);
end
in
Parameters.UsePrototype.iter aux
diff --git a/src/plugins/eva/engine/function_calls.ml b/src/plugins/eva/engine/function_calls.ml
index 6a3dc5e207c..24dd64d6ef9 100644
--- a/src/plugins/eva/engine/function_calls.ml
+++ b/src/plugins/eva/engine/function_calls.ml
@@ -152,22 +152,28 @@ let use_spec_instead_of_definition ?(recursion_depth = -1) kf =
not (Kernel_function.is_definition kf) ||
Kernel_function.Set.mem kf (Parameters.UsePrototype.get ())
+(* Returns the function specification of [kf], with generated assigns clauses
+ if they are missing. *)
+let get_funspec kf =
+ Populate_spec.populate_funspec ~do_body:true kf [`Assigns];
+ Annotations.funspec kf
+
let analysis_target ~recursion_depth callsite kf =
match Builtins.find_builtin_override kf with
| Some (name, builtin, cache, spec) ->
`Builtin (name, builtin, cache, spec)
| None ->
if recursion_depth >= Parameters.RecursiveUnroll.get ()
- then `Spec (Recursion.get_spec callsite kf)
+ then begin
+ Recursion.check_spec callsite kf;
+ `Spec (get_funspec kf)
+ end
else
match kf.fundec with
- | Declaration (_,_,_,_) -> `Spec (Annotations.funspec kf)
+ | Declaration _ -> `Spec (get_funspec kf)
| Definition (def, _) ->
if Kernel_function.Set.mem kf (Parameters.UsePrototype.get ())
- then begin
- Populate_spec.(populate_funspec kf [`Assigns]);
- `Spec (Annotations.funspec kf)
- end
+ then `Spec (get_funspec kf)
else `Body (def, save_results def)
let define_analysis_target ?(recursion_depth = -1) callsite kf =
diff --git a/src/plugins/eva/engine/recursion.ml b/src/plugins/eva/engine/recursion.ml
index 918905f490f..6feec3ffad0 100644
--- a/src/plugins/eva/engine/recursion.ml
+++ b/src/plugins/eva/engine/recursion.ml
@@ -44,15 +44,10 @@ let mark_unknown_requires kinstr kf funspec =
in
List.iter emit_behavior funspec.spec_behavior
-let need_assigns funspec =
- match Cil.find_default_behavior funspec with
- | None -> true
- | Some bhv -> bhv.b_assigns = WritesAny
-
-let get_spec kinstr kf =
+let check_spec kinstr kf =
let funspec = Annotations.funspec kf in
if List.for_all (fun b -> b.b_assigns = WritesAny) funspec.spec_behavior
- then begin
+ then
Self.error ~current:true
"@[Recursive call to %a@ without assigns clause.@ \
Generating probably incomplete assigns to interpret the call.@ \
@@ -64,33 +59,17 @@ let get_spec kinstr kf =
Kernel_function.pretty kf
Parameters.RecursiveUnroll.name
Kernel_function.pretty kf
- Eva_utils.pp_callstack;
- Cil.CurrentLoc.set (Kernel_function.get_location kf);
- Populate_spec.(populate_funspec ~funspec kf [`Assigns]);
- Annotations.funspec kf
- end
+ Eva_utils.pp_callstack
else
let depth = Parameters.RecursiveUnroll.get () in
- let () =
- Self.warning ~once:true ~current:true
- "@[Using specification of function %a@ for recursive calls%s.@ \
- Analysis of function %a@ is thus incomplete@ and its soundness@ \
- relies on the written specification.@]"
- Kernel_function.pretty kf
- (if depth > 0 then Format.asprintf " of depth %i" depth else "")
- Kernel_function.pretty kf
- in
- let funspec =
- if need_assigns funspec
- then
- begin
- Populate_spec.(populate_funspec ~funspec kf [`Assigns]);
- Annotations.funspec kf
- end
- else funspec
- in
- mark_unknown_requires kinstr kf funspec;
- funspec
+ Self.warning ~once:true ~current:true
+ "@[Using specification of function %a@ for recursive calls%s.@ \
+ Analysis of function %a@ is thus incomplete@ and its soundness@ \
+ relies on the written specification.@]"
+ Kernel_function.pretty kf
+ (if depth > 0 then Format.asprintf " of depth %i" depth else "")
+ Kernel_function.pretty kf;
+ mark_unknown_requires kinstr kf funspec
(* Find a spec for a function [kf] that begins a recursive call. If [kf]
has no existing specification, generate (an incorrect) one, and warn
diff --git a/src/plugins/eva/engine/recursion.mli b/src/plugins/eva/engine/recursion.mli
index 575a220ebfd..dac29974c7d 100644
--- a/src/plugins/eva/engine/recursion.mli
+++ b/src/plugins/eva/engine/recursion.mli
@@ -28,7 +28,7 @@ open Eval
(* Returns the specification for a recursive call to the given function. Fails
if the function has no specification. Marks the preconditions of the call
as unknowns. *)
-val get_spec: kinstr -> kernel_function -> funspec
+val check_spec: kinstr -> kernel_function -> unit
(** Creates the information about a recursive call. *)
val make: ('v, 'loc) call -> recursion option
diff --git a/src/plugins/eva/engine/transfer_logic.ml b/src/plugins/eva/engine/transfer_logic.ml
index 7de051e0183..319e14323b7 100644
--- a/src/plugins/eva/engine/transfer_logic.ml
+++ b/src/plugins/eva/engine/transfer_logic.ml
@@ -285,7 +285,6 @@ module Make
Active_behaviors.create eval_predicate funspec
let create init_state kf =
- Populate_spec.(populate_funspec kf [`Assigns]);
let funspec = Annotations.funspec kf in
create_from_spec init_state funspec
@@ -475,7 +474,6 @@ module Make
The postcondition of the global behavior is applied for each behavior,
to help reduce the final state. *)
let check_fct_postconditions kf ab kind ~pre_state ~post_states ~result =
- Populate_spec.(populate_funspec kf [`Assigns]);
let behaviors = Annotations.behaviors kf in
let is_active = Active_behaviors.is_active ab in
let states =
@@ -522,7 +520,6 @@ module Make
into multiple states if the precondition contains disjunctions. *)
let check_fct_preconditions call_ki kf ab init_state =
let init_states = States.singleton init_state in
- Populate_spec.(populate_funspec kf [`Assigns]);
let behaviors = Annotations.behaviors kf in
let is_active = Active_behaviors.is_active ab in
let states =
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 3ff6e2ac1d4..165dbf57cdd 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -729,6 +729,9 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Legacy callbacks for the cvalue domain, usually called by
{Cvalue_transfer.start_call}. *)
let apply_cvalue_callback kf stmt state =
+ (* Generates assigns clauses for other plugins, as they may use
+ the directive specification. *)
+ Populate_spec.populate_funspec kf [`Assigns];
let call_stack = Eva_utils.current_call_stack () in
let stack_with_call = Callstack.push kf stmt call_stack in
let cvalue_state = get_cvalue_or_top state in
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index 8992d326150..03c6ee235ba 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -46,7 +46,7 @@ let compute_term_deps stmt t =
let () = Logic_deps.compute_term_deps := compute_term_deps
let valid_behaviors kf state =
- Populate_spec.(populate_funspec kf [`Assigns]);
+ Populate_spec.populate_funspec kf [`Assigns];
let funspec = Annotations.funspec kf in
let eval_predicate pred =
match Eval_terms.(eval_predicate (env_pre_f ~pre:state ()) pred) with
@@ -211,7 +211,6 @@ let conv_status = function
let check_fct_assigns kf ab ~pre_state found_froms =
let open Locations in
let open Alarmset in
- Populate_spec.(populate_funspec kf [`Assigns]);
let behaviors = Annotations.behaviors kf in
(* Under-approximation of the union. *)
let link zones = List.fold_left Zone.link Zone.bottom zones in
@@ -282,7 +281,6 @@ let check_fct_assigns kf ab ~pre_state found_froms =
in List.iter check_for_behavior behaviors
let verify_assigns kf ~pre froms =
- Populate_spec.(populate_funspec kf [`Assigns]);
let funspec = Annotations.funspec kf in
let env = Eval_terms.env_pre_f ~pre () in
let eval_predicate pred =
--
GitLab