From 9a434b7a566281d1036974068d51fb466d03904b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 27 Mar 2023 14:11:09 +0200
Subject: [PATCH] [Eva] Requests: fixes evaluation of \result in
post-conditions.
---
src/plugins/eva/api/general_requests.ml | 14 ++++++++------
src/plugins/eva/api/general_requests.mli | 4 ++++
src/plugins/eva/api/values_request.ml | 22 ++++++++++++----------
src/plugins/eva/utils/eva_utils.ml | 5 +++++
src/plugins/eva/utils/eva_utils.mli | 4 ++++
5 files changed, 33 insertions(+), 16 deletions(-)
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 1247eda023d..ca9395f89d1 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -226,8 +226,10 @@ let marker_evaluation_point = function
| PTermLval (_, _, prop, _) | PIP prop -> property_evaluation_point prop
| PType _ -> raise Not_found
-let term_lval_to_lval tlval =
- try Logic_to_c.term_lval_to_lval tlval
+let term_lval_to_lval kf tlval =
+ try
+ let result = Option.bind kf Eva_utils.find_return_var in
+ Logic_to_c.term_lval_to_lval ?result tlval
with Logic_to_c.No_conversion -> raise Not_found
let print_value fmt loc =
@@ -242,8 +244,8 @@ let print_value fmt loc =
Results.eval_exp expr
| PVDecl (_, _, vi) when is_scalar vi.vtype ->
Results.eval_var vi
- | PTermLval (_, _, _ip, tlval) ->
- let lval = term_lval_to_lval tlval in
+ | PTermLval (kf, _, _ip, tlval) ->
+ let lval = term_lval_to_lval kf tlval in
if is_scalar (Cil.typeOfLval lval)
then Results.eval_lval lval
else raise Not_found
@@ -288,8 +290,8 @@ module EvaTaints = struct
| PLval (_, Kstmt stmt, lval) -> Some (expr_of_lval lval, stmt)
| PExp (_, Kstmt stmt, expr) -> Some (expr, stmt)
| PVDecl (_, Kstmt stmt, vi) -> Some (expr_of_lval (Var vi, NoOffset), stmt)
- | PTermLval (_, Kstmt stmt, _, tlval) ->
- Some (term_lval_to_lval tlval |> expr_of_lval, stmt)
+ | PTermLval (kf, Kstmt stmt, _, tlval) ->
+ Some (term_lval_to_lval kf tlval |> expr_of_lval, stmt)
| _ -> None
let of_marker marker =
diff --git a/src/plugins/eva/api/general_requests.mli b/src/plugins/eva/api/general_requests.mli
index 57502fa634b..9a1c8699b3d 100644
--- a/src/plugins/eva/api/general_requests.mli
+++ b/src/plugins/eva/api/general_requests.mli
@@ -32,3 +32,7 @@ type evaluation_point =
(* Returns the evaluation point of a marker.
@raises Not_found if the marker cannot be evaluated. *)
val marker_evaluation_point: Printer_tag.localizable -> evaluation_point
+
+(* Converts an ACSL lval into a C lval.
+ @raises Not_found if the conversion fails. *)
+val term_lval_to_lval: kernel_function option -> term_lval -> lval
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 2796bb32d74..4fe3f15d5e4 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -114,12 +114,6 @@ let probe_property = function
Ppred (Logic_const.pred_of_id_pred pred)
| _ -> raise Not_found
-let probe_term_lval kf tlval =
- try
- let result = Option.bind kf Library_functions.get_retres_vi in
- Plval (Logic_to_c.term_lval_to_lval ?result tlval)
- with Logic_to_c.No_conversion -> raise Not_found
-
let probe_marker = function
| Printer_tag.PLval (_, _, (Var vi, NoOffset))
| PVDecl (_, _, vi) when Cil.isFunctionType vi.vtype -> raise Not_found
@@ -127,7 +121,8 @@ let probe_marker = function
| PExp (_, _, e) -> Pexpr e
| PStmt (_, s) | PStmtStart (_, s) -> probe_stmt s
| PVDecl (_, _, v) -> Plval (Var v, NoOffset)
- | PTermLval (kf, _, _, tlval) -> probe_term_lval kf tlval
+ | PTermLval (kf, _, _, tlval) ->
+ Plval (General_requests.term_lval_to_lval kf tlval)
| PIP property -> probe_property property
| _ -> raise Not_found
@@ -475,9 +470,16 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let eval_expr expr state =
A.eval_expr state expr >>=: fun value -> Value value
- let eval_pred predicate state =
+ let eval_pred eval_point predicate state =
+ let result =
+ match eval_point with
+ | Initial | Pre _ -> None
+ | Stmt stmt ->
+ let kf = Kernel_function.find_englobing_kf stmt in
+ Eva_utils.find_return_var kf
+ in
let env =
- Abstract_domain.{ states = (function _ -> A.Dom.top) ; result = None }
+ Abstract_domain.{ states = (function _ -> A.Dom.top) ; result }
in
let truth = A.Dom.evaluate_predicate env state predicate in
`Value (Status truth), Alarmset.none
@@ -518,7 +520,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
| Pexpr expr ->
eval_steps (Cil.typeOf expr) (eval_expr expr) eval_point callstack
| Ppred pred ->
- eval_steps Cil.intType (eval_pred pred) eval_point callstack
+ eval_steps Cil.intType (eval_pred eval_point pred) eval_point callstack
end
let proxy =
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 75d902623d8..7dbc948a1e0 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -138,6 +138,11 @@ let create_new_var name typ =
let is_const_write_invalid typ = Cil.typeHasQualifier "const" typ
+let find_return_var kf =
+ match (Kernel_function.find_return kf).skind with
+ | Return (Some ({enode = Lval ((Var vi, NoOffset))}), _) -> Some vi
+ | _ | exception Kernel_function.No_Statement -> None
+
(* Find if a postcondition contains [\result] *)
class postconditions_mention_result = object
inherit Visitor.frama_c_inplace
diff --git a/src/plugins/eva/utils/eva_utils.mli b/src/plugins/eva/utils/eva_utils.mli
index 0903cdabad1..9297eee8543 100644
--- a/src/plugins/eva/utils/eva_utils.mli
+++ b/src/plugins/eva/utils/eva_utils.mli
@@ -72,6 +72,10 @@ val is_const_write_invalid: typ -> bool
(** Detect that the type is const, and that option [-global-const] is set. In
this case, we forbid writing in a l-value that has this type. *)
+val find_return_var: kernel_function -> varinfo option
+(** Returns the varinfo returned by the given function.
+ Returns None if the function returns void or has no return statement. *)
+
val postconditions_mention_result: Cil_types.funspec -> bool
(** Does the post-conditions of this specification mention [\result]? *)
--
GitLab