diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index b622130d6e7c272654cfa450ebc47e2f5d7232d1..6a721abfab960aee57ecf241fbf28041f6e335cd 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -329,7 +329,8 @@ module Make (Abstract: Abstractions.Eva) = struct
Value_util.push_call_stack kf Kglobal;
store_initial_state kf init_state;
let call =
- {kf; arguments = []; rest = []; return = None; recursive = false}
+ {kf; arguments = []; rest = []; return = None;
+ recursive = false; }
in
let final_result = compute_using_spec_or_body Kglobal call init_state in
let final_states = final_result.Transfer.states in
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index 99d150435c7d019f1cb0bd1a88f5ecb76e347f02..c7a7dfe117ad6edd8637d8f7a29659aba9fcb6b9 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -32,7 +32,7 @@ open Cil_types
let check_formals_non_referenced kf =
let formals = Kernel_function.get_formals kf in
if List.exists (fun vi -> vi.vaddrof) formals then
- Value_parameters.error ~current:true ~once:true
+ Value_parameters.warning ~current:true ~once:true
"function '%a' (involved in a recursive call) has a formal parameter \
whose address is taken. Analysis may be unsound."
Kernel_function.pretty kf
@@ -104,3 +104,73 @@ let empty_spec_for_recursive_call kf =
let bhv = Cil.mk_behavior ~assigns ~name:Cil.default_behavior_name () in
empty.spec_behavior <- [bhv];
empty
+
+
+(* -------------------------------------------------------------------------- *)
+
+module CallDepth =
+ Datatype.Pair_with_collections (Kernel_function) (Datatype.Int)
+ (struct let module_name = "RecDepth" end)
+
+module VarCopies =
+ Datatype.List (Datatype.Pair (Cil_datatype.Varinfo) (Cil_datatype.Varinfo))
+
+module Vars = Datatype.Pair (VarCopies) (Datatype.List (Cil_datatype.Varinfo))
+
+module VarStack =
+ State_builder.Hashtbl
+ (CallDepth.Hashtbl)
+ (Vars)
+ (struct
+ let name = "Eva.Recursion.VarStack"
+ let dependencies = [ Ast.self ]
+ let size = 9
+ end)
+
+let copy_variable depth varinfo =
+ let name = Format.asprintf "\\copy<%s>[%i]" varinfo.vname depth
+ and typ = varinfo.vtype
+ and source = true
+ and temp = varinfo.vtemp
+ and referenced = varinfo.vreferenced
+ and ghost = varinfo.vghost
+ and loc = varinfo.vdecl in
+ Cil.makeVarinfo ~source ~temp ~referenced ~ghost ~loc false false name typ
+
+let copy_fresh_variable fundec depth varinfo =
+ let v = copy_variable depth varinfo in
+ Cil.refresh_local_name fundec v;
+ v
+
+let make_stack (kf, depth) =
+ let fundec =
+ try Kernel_function.get_definition kf
+ with Kernel_function.No_Definition -> assert false
+ in
+ let vars = Kernel_function.(get_formals kf @ get_locals kf) in
+ let reachable, withdrawal = List.partition (fun vi -> vi.vaddrof) vars in
+ let copy v = v, copy_fresh_variable fundec depth v in
+ let substitution = List.map copy reachable in
+ substitution, withdrawal
+
+let get_stack kf depth = VarStack.memo make_stack (kf, depth)
+
+let make_recursive_call kf =
+ let call_stack = Value_util.call_stack () in
+ let previous_calls = List.filter (fun (f, _) -> f == kf) call_stack in
+ let depth = List.length previous_calls in
+ let substitution, withdrawal = get_stack kf depth in
+ let base_of_varinfo (v1, v2) = Base.of_varinfo v1, Base.of_varinfo v2 in
+ let list_substitution = List.map base_of_varinfo substitution in
+ let base_substitution = Base.substitution_from_list list_substitution in
+ let list_withdrawal = List.map Base.of_varinfo withdrawal in
+ let base_withdrawal = Base.Hptset.of_list list_withdrawal in
+ Eval.{ depth; substitution; base_substitution; withdrawal; base_withdrawal; }
+
+let revert_recursion recursion =
+ let revert (v1, v2) = v2, v1 in
+ let substitution = List.map revert recursion.Eval.substitution in
+ let base_of_varinfo (v1, v2) = Base.of_varinfo v1, Base.of_varinfo v2 in
+ let list = List.map base_of_varinfo substitution in
+ let base_substitution = Base.substitution_from_list list in
+ Eval.{ recursion with substitution; base_substitution; }
diff --git a/src/plugins/value/engine/recursion.mli b/src/plugins/value/engine/recursion.mli
index 3a3255c47d1b22827ef20c36d711d349c5cd1492..80c28c1cd88641aa45a2fe58c1f20d139e1cb9a4 100644
--- a/src/plugins/value/engine/recursion.mli
+++ b/src/plugins/value/engine/recursion.mli
@@ -32,3 +32,8 @@ val empty_spec_for_recursive_call: kernel_function -> spec
(** Generate an empty spec [assigns \nothing] or
[assigns \result \from \nothing], to be used to "approximate" the
results of a recursive call. *)
+
+(** TODO *)
+val make_recursive_call: kernel_function -> Eval.recursion
+
+val revert_recursion: Eval.recursion -> Eval.recursion
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 040629aa88699be86afd064e0775d464398b4e34..8e574e39a482a0c6a0e822e2873e04af132ade4e 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -556,7 +556,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let arguments = List.rev arguments in
arguments, rest
in
- {kf; arguments; rest; return; recursive}
+ {kf; arguments; rest; return; recursive; }
let make_call ~subdivnb kf arguments valuation state =
(* Evaluate the arguments of the call. *)
diff --git a/src/plugins/value/eval.ml b/src/plugins/value/eval.ml
index 8aab315162a3557beba3835d1b3c821ded536474..ab4e77305f48391e739b76186615836e4bda4c36 100644
--- a/src/plugins/value/eval.ml
+++ b/src/plugins/value/eval.ml
@@ -248,6 +248,14 @@ type ('loc, 'value) call = {
recursive: bool;
}
+type recursion = {
+ depth: int;
+ substitution: (varinfo * varinfo) list;
+ base_substitution: Base.substitution;
+ withdrawal: varinfo list;
+ base_withdrawal: Base.Hptset.t;
+}
+
type cacheable = Cacheable | NoCache | NoCacheCallers
(*
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index e050aae784876740fd329e70493c9876495131ef..ef1a1937757b26c68da7c2857e2bf350e902f857 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -215,7 +215,6 @@ type 'location logic_assign =
(** {2 Interprocedural Analysis } *)
(* -------------------------------------------------------------------------- *)
-
(** Argument of a function call. *)
type ('loc, 'value) argument = {
formal: varinfo; (** The formal argument of the called function. *)
@@ -235,7 +234,19 @@ type ('loc, 'value) call = {
recursive: bool;
}
-(* Can the results of a function call be cached with memexec? *)
+(** Information needed to interpret a recursive call.
+ The local variables and formal parameters of different recursive calls
+ should not be mixed up. Those of the current call must be temporary withdraw
+ or replaced from the domain states before starting the new recursive call. *)
+type recursion = {
+ depth: int;
+ substitution: (varinfo * varinfo) list;
+ base_substitution: Base.substitution;
+ withdrawal: varinfo list;
+ base_withdrawal: Base.Hptset.t;
+}
+
+(** Can the results of a function call be cached with memexec? *)
type cacheable =
| Cacheable (** Functions whose result can be safely cached *)
| NoCache (** Functions whose result should not be cached, but for