From 5b8582a16edfb3f064d36e3756fc7542aebb36e7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 22 Mar 2024 22:46:11 +0100
Subject: [PATCH] [Eva] Backward propagates reduction of builtins arguments.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
During the interpretation of a function call, the possible values of formal
parameters can be reduced — especially by the evaluation of the function
preconditions.
At the end of a function call, Eva backward propagates these reductions to the
concrete arguments of the call.
This commit also does this backward-propagation when a builtin is used to
interpret the call.
Also removes unused [builtin] field from call results (it was only used to
avoid the backward propagation of argument reductions when a builtin was used).
---
src/plugins/eva/engine/compute_functions.ml | 9 ++++-----
src/plugins/eva/engine/transfer_stmt.ml | 13 ++-----------
src/plugins/eva/engine/transfer_stmt.mli | 1 -
3 files changed, 6 insertions(+), 17 deletions(-)
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 90a70b081ad..63265847a27 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -220,7 +220,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
end;
apply_call_results_hooks call init_state (`Reuse i);
(* call can be cached since it was cached once *)
- Transfer.{states; cacheable = Cacheable; builtin=false}
+ Transfer.{ states; cacheable = Cacheable; }
(* ----- Body or specification analysis ----------------------------------- *)
@@ -273,7 +273,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
if Parameters.ValShowProgress.get () then
Self.feedback
"Done for function %a" Kernel_function.pretty call.kf;
- Transfer.{ states = resulting_states; cacheable; builtin=false }
+ Transfer.{ states = resulting_states; cacheable; }
(* ----- Use of cvalue builtins ------------------------------------------- *)
@@ -310,8 +310,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
match final_state with
| `Bottom ->
apply_call_results_hooks call state (`Builtin ([], None));
- let cacheable = Eval.Cacheable in
- Transfer.{states; cacheable; builtin=true}
+ Transfer.{ states; cacheable = Eval.Cacheable; }
| `Value final_state ->
let cvalue_call = get_cvalue_call call in
let post = get_cvalue_or_top final_state in
@@ -324,7 +323,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
in
let states = List.map insert cvalue_states in
- Transfer.{states; cacheable; builtin=true}
+ Transfer.{ states; cacheable; }
(* Uses cvalue builtin only if the cvalue domain is available. Otherwise, only
use the called function specification. *)
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 2579ca24f8a..bc4fc022505 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -41,7 +41,6 @@ module type S = sig
type call_result = {
states: (Partition.key * state) list;
cacheable: Eval.cacheable;
- builtin: bool;
}
val compute_call_ref:
(stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
@@ -295,7 +294,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
type call_result = {
states: (Partition.key * state) list;
cacheable: cacheable;
- builtin: bool;
}
(* Forward reference to [Eval_funs.compute_call] *)
@@ -304,8 +302,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
call_result) ref
= ref (fun _ -> assert false)
- (* Returns the result of a call, and a boolean that indicates whether a
- builtin has been used to interpret the call. *)
+ (* Returns the result of a call. *)
let process_call stmt call recursion valuation state =
Eva_utils.push_call_stack call.kf stmt;
let cleanup () =
@@ -323,7 +320,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
Domain.Store.register_initial_state callstack call.kf state;
!compute_call_ref stmt call recursion state
| `Bottom ->
- { states = []; cacheable = Cacheable; builtin=false }
+ { states = []; cacheable = Cacheable; }
in
cleanup ();
res
@@ -460,12 +457,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Process the call according to the domain decision. *)
let call_result = process_call stmt call recursion valuation state in
let leaving_vars = leaving_vars kf_callee in
- (* Do not try to reduce concrete arguments if a builtin was used. *)
- let gather_reduced_arguments =
- if call_result.builtin
- then fun _ _ _ -> `Value []
- else gather_reduced_arguments
- in
(* Treat each result one by one. *)
let process state =
(* Gathers the possible reductions on the value of the concrete arguments
diff --git a/src/plugins/eva/engine/transfer_stmt.mli b/src/plugins/eva/engine/transfer_stmt.mli
index 7da3e2be794..8f5c2527e0c 100644
--- a/src/plugins/eva/engine/transfer_stmt.mli
+++ b/src/plugins/eva/engine/transfer_stmt.mli
@@ -51,7 +51,6 @@ module type S = sig
type call_result = {
states: (Partition.key * state) list;
cacheable: Eval.cacheable;
- builtin: bool;
}
val compute_call_ref:
--
GitLab