From dbdee5395c459722d0fb8187f9cb241ee10c4da4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 20 Apr 2021 13:51:01 +0200
Subject: [PATCH] [Eva] Adds the [callstack] in the [Eval.call] record built by
transfer_stmt.
---
src/plugins/value/engine/compute_functions.ml | 4 +++-
src/plugins/value/engine/recursion.ml | 4 ++--
src/plugins/value/engine/transfer_stmt.ml | 3 ++-
src/plugins/value/eval.ml | 5 +++++
src/plugins/value/eval.mli | 13 +++++++++++++
src/plugins/value/utils/value_util.ml | 6 +-----
src/plugins/value/utils/value_util.mli | 7 +------
7 files changed, 27 insertions(+), 15 deletions(-)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 50b0d1084fd..ece699c60df 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -331,7 +331,9 @@ module Make (Abstract: Abstractions.Eva) = struct
try
Value_util.push_call_stack kf Kglobal;
store_initial_state kf init_state;
- let call = { kf; arguments = []; rest = []; return = None; } in
+ let call =
+ { kf; callstack = []; arguments = []; rest = []; return = None; }
+ in
let final_result =
compute_using_spec_or_body Kglobal call None init_state
in
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index 634204a9452..a5abcb4b90e 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -167,8 +167,8 @@ let make_recursion call depth =
{ depth; substitution; base_substitution; withdrawal; base_withdrawal; }
let make call =
- let call_stack = Value_util.call_stack () in
- let previous_calls = List.filter (fun (f, _) -> f == call.kf) call_stack in
+ 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
if depth > 0
then Some (make_recursion call depth)
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 68c94c2fa24..7ba3de0d199 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -538,6 +538,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Create an Eval.call *)
let create_call kf args =
let return = Library_functions.get_retres_vi kf in
+ let callstack = Value_util.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
@@ -551,7 +552,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let arguments = List.rev arguments in
arguments, rest
in
- {kf; arguments; rest; return; }
+ {kf; callstack; arguments; rest; return; }
let replace_value visitor substitution = function
| Assign value -> Assign (Value.replace_base substitution value)
diff --git a/src/plugins/value/eval.ml b/src/plugins/value/eval.ml
index 74eb7635382..7a12a168d66 100644
--- a/src/plugins/value/eval.ml
+++ b/src/plugins/value/eval.ml
@@ -240,8 +240,13 @@ type ('loc, 'value) argument = {
avalue: ('loc, 'value) assigned;
}
+
+type call_site = kernel_function * kinstr
+type callstack = call_site list
+
type ('loc, 'value) call = {
kf: kernel_function;
+ callstack: callstack;
arguments: ('loc, 'value) argument list;
rest: (exp * ('loc, 'value) assigned) list;
return: varinfo option;
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index c68cebbd998..5714172358f 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -222,9 +222,22 @@ type ('loc, 'value) argument = {
avalue: ('loc, 'value) assigned; (** The value of the concrete argument. *)
}
+(** A call_stack is a list, telling which function was called at which
+ site. The head of the list tells about the latest call. *)
+
+(** A call site: the function called, and the call statement
+ (or [Kglobal] for the main function. *)
+type call_site = kernel_function * kinstr
+
+(* A call stack is a list of call sites. The head is the latest call.
+ The last element is the main function. *)
+type callstack = call_site list
+
(** A function call. *)
type ('loc, 'value) call = {
kf: kernel_function; (** The called function. *)
+ callstack: callstack; (** The current callstack
+ (without this call). *)
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
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index 00f2871518e..13a005dd2af 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -24,11 +24,7 @@ open Cil_types
(* Callstacks related types and functions *)
-(* Function called, and calling instruction. *)
-type call_site = (kernel_function * kinstr)
-type callstack = call_site list
-
-let call_stack : callstack ref = ref []
+let call_stack : Value_types.callstack ref = ref []
(* let call_stack_for_callbacks : (kernel_function * kinstr) list ref = ref [] *)
let clear_call_stack () =
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/value_util.mli
index 61df6ce5331..0bfe89cbe91 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/value_util.mli
@@ -24,11 +24,6 @@ open Cil_types
(** {2 Callstacks related types and functions} *)
-(** A call_stack is a list, telling which function was called at which
- site. The head of the list tells about the latest call. *)
-type call_site = (kernel_function * kinstr)
-type callstack = call_site list
-
(** Functions dealing with call stacks. *)
val clear_call_stack : unit -> unit
val pop_call_stack : unit -> unit
@@ -36,7 +31,7 @@ val push_call_stack : kernel_function -> kinstr -> unit
(** The current function is the one on top of the call stack. *)
val current_kf : unit -> kernel_function
-val call_stack : unit -> callstack
+val call_stack : unit -> Value_types.callstack
(** Prints the current callstack. *)
val pp_callstack : Format.formatter -> unit
--
GitLab