[Eva] Engine: unroll the n first recursive calls, and then use the specification.

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)

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 =

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
 

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; }