From 9c3a4505f0c9d839cbfc5d9972a59107f368b41f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 4 Apr 2022 11:33:16 +0200
Subject: [PATCH] [Eva] In [call] type, the callstack includes the current
call.
---
src/plugins/value/engine/compute_functions.ml | 5 ++---
src/plugins/value/engine/recursion.ml | 2 +-
src/plugins/value/engine/transfer_stmt.ml | 10 +++++-----
src/plugins/value/eval.mli | 2 +-
4 files changed, 9 insertions(+), 10 deletions(-)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index ac17b268d15..c4288155ea6 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -352,9 +352,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute () =
Eva_utils.push_call_stack kf Kglobal;
store_initial_state kf init_state;
- let call =
- { kf; callstack = []; arguments = []; rest = []; return = None; }
- in
+ let callstack = [kf, Kglobal] in
+ let call = { kf; callstack; arguments = []; rest = []; return = None; } in
let final_result = compute_call Kglobal call None init_state in
let final_states = List.map snd (final_result.Transfer.states) in
let final_state = PowersetDomain.(final_states |> of_list |> join) in
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index 9134b02da04..fb0da4b9b93 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -179,7 +179,7 @@ let make_recursion call depth =
let make call =
let is_same_kf (f, _) = Kernel_function.equal f call.kf in
let previous_calls = List.filter is_same_kf call.callstack in
- let depth = List.length previous_calls in
+ let depth = List.length previous_calls - 1 in
if depth > 0
then Some (make_recursion call depth)
else None
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 303e69ee16d..34ec661ec42 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -531,9 +531,9 @@ module Make (Abstract: Abstractions.Eva) = struct
(* ------------------------- Make an Eval.call ---------------------------- *)
(* Create an Eval.call *)
- let create_call kf args =
+ let create_call stmt kf args =
let return = Library_functions.get_retres_vi kf in
- let callstack = Eva_utils.call_stack () in
+ let callstack = (kf, Kstmt stmt) :: Eva_utils.call_stack () in
let arguments, rest =
let formals = Kernel_function.get_formals kf in
let rec format_arguments acc args formals = match args, formals with
@@ -572,12 +572,12 @@ module Make (Abstract: Abstractions.Eva) = struct
let arguments = List.map replace_arg call.arguments in
{ call with arguments; }
- let make_call ~subdivnb kf arguments valuation state =
+ let make_call ~subdivnb stmt kf arguments valuation state =
(* Evaluate the arguments of the call. *)
let determinate = is_determinate kf in
compute_actuals ~subdivnb ~determinate valuation state arguments
>>=: fun (args, valuation) ->
- let call = create_call kf args in
+ let call = create_call stmt kf args in
let recursion = Recursion.make call in
let call = Extlib.opt_fold replace_recursive_call recursion call in
call, recursion, valuation
@@ -756,7 +756,7 @@ module Make (Abstract: Abstractions.Eva) = struct
[(Partition.Key.empty, state)]
else
(* Create the call. *)
- let eval, alarms = make_call ~subdivnb kf args valuation state in
+ let eval, alarms = make_call ~subdivnb stmt kf args valuation state in
Alarmset.emit ki_call alarms;
let states =
let+ call, recursion, valuation = eval in
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index 76f96cf20bc..c0335e7761b 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -238,7 +238,7 @@ type callstack = call_site list
type ('loc, 'value) call = {
kf: kernel_function; (** The called function. *)
callstack: callstack; (** The current callstack
- (without this call). *)
+ (with this call on top). *)
arguments: ('loc, 'value) argument list; (** The arguments of the call. *)
rest: (exp * ('loc, 'value) assigned) list; (** Extra-arguments. *)
return: varinfo option; (** Fake varinfo to store the
--
GitLab