diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 6a721abfab960aee57ecf241fbf28041f6e335cd..8eaabed066410ff3309ad58a961f42d4faafd31f 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -154,6 +154,14 @@ module Make (Abstract: Abstractions.Eva) = struct
| None -> fun _ -> assert false
| Some get -> fun location -> get location
+ let unroll_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
+ assert (depth > 0);
+ let limit = Value_parameters.RecursiveUnroll.get () in
+ depth <= limit
+
(* Compute a call to [kf] in the state [state]. The evaluation will
be done either using the body of [kf] or its specification, depending
on whether the body exists and on option [-eva-use-spec]. [call_kinstr]
@@ -172,8 +180,8 @@ module Make (Abstract: Abstractions.Eva) = struct
Value_types.Callstack.pretty_short call_stack
Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc call_kinstr);
let use_spec =
- if call.recursive then
- `Spec (Recursion.empty_spec_for_recursive_call kf)
+ if call.recursive && not (unroll_recursive_call kf) then
+ `Spec (Recursion.recursive_spec kf)
else
match kf.fundec with
| Declaration (_,_,_,_) -> `Spec (Annotations.funspec kf)
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index af9cefc4579e3cdb435eec9429d30581c92236f6..83133b6a202d3be19b18d13144971ec5c664b475 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -37,18 +37,29 @@ let check_formals_non_referenced kf =
whose address is taken. Analysis may be unsound."
Kernel_function.pretty kf
-let warn_recursive_call kf call_stack =
+let warn_recursive_call kf =
Value_parameters.feedback ~once:true ~current:true
- "@[@[detected@ recursive@ call@ (%a <- %a)@]@;@]"
- Kernel_function.pretty kf Value_types.Callstack.pretty call_stack;
+ "@[detected recursive call@ of function %a.@]"
+ Kernel_function.pretty kf;
check_formals_non_referenced kf
+let recursive_spec kf =
+ let funspec = Annotations.funspec ~populate:false kf in
+ if Cil.is_empty_funspec funspec then
+ Value_parameters.abort ~current:true
+ "@[Recursive call to %a@ without a specification.@ Try to increase@ \
+ the %s parameter@ or write a specification@ for function %a.@]"
+ Kernel_function.pretty kf
+ Value_parameters.RecursiveUnroll.name
+ Kernel_function.pretty kf
+ else funspec
+
(* Check whether the function at the top of the call-stack starts a
recursive call. *)
let is_recursive_call kf =
let call_stack = Value_util.call_stack () in
if List.exists (fun (f, _) -> f == kf) call_stack
- then (warn_recursive_call kf call_stack; true)
+ then (warn_recursive_call kf; true)
else false
(* Find a spec for a function [kf] that begins a recursive call. If [kf]
@@ -74,7 +85,7 @@ let _spec_for_recursive_call kf =
~silent_about_merging_behav:true spec initial_spec;
spec
-let empty_spec_for_recursive_call kf =
+let _empty_spec_for_recursive_call kf =
let typ_res = Kernel_function.get_return_type kf in
let empty = Cil.empty_funspec () in
let assigns =
diff --git a/src/plugins/value/engine/recursion.mli b/src/plugins/value/engine/recursion.mli
index 80c28c1cd88641aa45a2fe58c1f20d139e1cb9a4..a446573aca8c6858c701f14993c1beef7baaae3f 100644
--- a/src/plugins/value/engine/recursion.mli
+++ b/src/plugins/value/engine/recursion.mli
@@ -24,15 +24,12 @@
open Cil_types
+val recursive_spec: kernel_function -> funspec
+
val is_recursive_call: kernel_function -> bool
(** Given the current state of the call stack, detect whether the
given given function would start a recursive cycle. *)
-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
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 853705200e9832fcaa6a9fef87253f1784be3b08..8580e99fc2d08ea9d98ecea0600adbdf91adda72 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -472,22 +472,15 @@ module Make (Abstract: Abstractions.Eva) = struct
>>- fun reductions ->
(* The formals (and the locals) of the called function leave scope. *)
let post = Domain.leave_scope kf_callee leaving_vars state in
+ let recursion = Option.map Recursion.revert_recursion recursion in
(* Computes the state after the call, from the post state at the end of
the called function, and the pre state at the call site. *)
Domain.finalize_call stmt call recursion ~pre ~post >>- fun state ->
(* Backward propagates the [reductions] on the concrete arguments. *)
reduce_arguments reductions state >>- fun state ->
treat_return ~kf_callee lv call.return stmt state
- and process_recursive state =
- (* When the call is recursive, formals have not been added to the
- domains. Do not reduce them, and more importantly, do not remove
- them from the scope. (Because the instance from the initial,
- non-recursive, call are still present.) *)
- Domain.finalize_call stmt call recursion ~pre ~post:state >>- fun state ->
- treat_return ~kf_callee lv call.return stmt state
in
let states =
- let process = if call.recursive then process_recursive else process in
List.fold_left
(fun acc return -> Bottom.add_to_list (process return) acc)
[] result
@@ -536,25 +529,17 @@ module Make (Abstract: Abstractions.Eva) = struct
let recursive = Recursion.is_recursive_call kf in
let return = Library_functions.get_retres_vi kf in
let arguments, rest =
- if recursive then
- (* For recursive calls, we evaluate 'assigns \result \from \nothing'
- using a specification. We generate a dummy [call] object in which
- formals are not present. This way, domains will not overwrite
- the formals of the recursive function (which would be present
- in scope twice). *)
- [], []
- else
- let formals = Kernel_function.get_formals kf in
- let rec format_arguments acc args formals = match args, formals with
- | _, [] -> acc, args
- | [], _ -> assert false
- | (concrete, avalue) :: args, formal :: formals ->
- let argument = { formal ; concrete; avalue } in
- format_arguments (argument :: acc) args formals
- in
- let arguments, rest = format_arguments [] args formals in
- let arguments = List.rev arguments in
- arguments, rest
+ let formals = Kernel_function.get_formals kf in
+ let rec format_arguments acc args formals = match args, formals with
+ | _, [] -> acc, args
+ | [], _ -> assert false
+ | (concrete, avalue) :: args, formal :: formals ->
+ let argument = { formal ; concrete; avalue } in
+ format_arguments (argument :: acc) args formals
+ in
+ let arguments, rest = format_arguments [] args formals in
+ let arguments = List.rev arguments in
+ arguments, rest
in
{kf; arguments; rest; return; recursive; }