[Eva] Engine: rework the handling of recursive calls.

- Removes the [recursion] boolean field from [call] type.
- Functions in [compute_function] takes a [recursion option] in argument.

src/plugins/value/domains/domain_builder.ml

@@ -48,8 +48,7 @@ let simplify_call call =
   { kf = call.Eval.kf;
     arguments = List.map simplify_argument call.Eval.arguments;
     rest = List.map fst call.Eval.rest;
-    return = call.Eval.return;
-    recursive = call.Eval.recursive }
+    return = call.Eval.return; }
 
 module Make_Minimal
     (Value: Abstract_value.S)

src/plugins/value/domains/simpler_domains.mli

@@ -42,7 +42,6 @@ type simple_call = {
   rest: exp list;                     (* Extra arguments. *)
   return: varinfo option;             (* Fake varinfo where the result of the
                                          call is stored. *)
-  recursive: bool;                    (* Is the call recursive? *)
 }
 
 (** Simplest interface for an abstract domain. No exchange of information with

src/plugins/value/engine/compute_functions.ml

@@ -154,21 +154,13 @@ 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]
      is the instruction at which the call takes place, and is used to update
      the statuses of the preconditions of [kf]. If [show_progress] is true,
      the callstack and additional information are printed. *)
-  let compute_using_spec_or_body call_kinstr call state =
+  let compute_using_spec_or_body call_kinstr call recursion state =
     let kf = call.kf in
     Value_results.mark_kf_as_called kf;
     let global = match call_kinstr with Kglobal -> true | _ -> false in
@@ -180,9 +172,10 @@ 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 && not (unroll_recursive_call kf) then
+      match recursion with
+      | Some { depth } when depth >= Value_parameters.RecursiveUnroll.get () ->
         `Spec (Recursion.recursive_spec kf)
-      else
+      | _ ->
         match kf.fundec with
         | Declaration (_,_,_,_) -> `Spec (Annotations.funspec kf)
         | Definition (def, _) ->
@@ -218,8 +211,10 @@ module Make (Abstract: Abstractions.Eva) = struct
 
   module MemExec = Mem_exec.Make (Abstract.Val) (Abstract.Dom)
 
-  let compute_and_cache_call stmt call init_state =
-    let default () = compute_using_spec_or_body (Kstmt stmt) call init_state in
+  let compute_and_cache_call stmt call recursion init_state =
+    let default () =
+      compute_using_spec_or_body (Kstmt stmt) call recursion init_state
+    in
     if Value_parameters.MemExecAll.get () then
       let args =
         List.map (fun {avalue} -> Eval.value_assigned avalue) call.arguments
@@ -280,9 +275,9 @@ module Make (Abstract: Abstractions.Eva) = struct
     | [state] -> `Value state
     | s :: l  -> `Value (List.fold_left Abstract.Dom.join s l)
 
-  let compute_call_or_builtin stmt call state =
+  let compute_call_or_builtin stmt call recursion state =
     match Builtins.find_builtin_override call.kf with
-    | None -> compute_and_cache_call stmt call state
+    | None -> compute_and_cache_call stmt call recursion state
     | Some (name, builtin, cacheable, spec) ->
       Value_results.mark_kf_as_called call.kf;
       let kinstr = Kstmt stmt in
@@ -336,11 +331,10 @@ 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;
-         recursive = false; }
+      let call = { kf; arguments = []; rest = []; return = None; } in
+      let final_result =
+        compute_using_spec_or_body Kglobal call None init_state
       in
-      let final_result = compute_using_spec_or_body Kglobal call init_state in
       let final_states = final_result.Transfer.states in
       let final_state = PowersetDomain.(final_states >>-: of_list >>- join) in
       Value_util.pop_call_stack ();

src/plugins/value/engine/recursion.ml

@@ -21,6 +21,7 @@
 (**************************************************************************)
 
 open Cil_types
+open Eval
 
 (** Recursion *)
 
@@ -54,14 +55,6 @@ let recursive_spec kf =
       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; true)
-  else false
-
 (* Find a spec for a function [kf] that begins a recursive call. If [kf]
    has no existing specification, generate (an incorrect) one, and warn
    loudly. *)
@@ -106,7 +99,7 @@ let _empty_spec_for_recursive_call kf =
 
 module CallDepth =
   Datatype.Pair_with_collections (Kernel_function) (Datatype.Int)
-    (struct let module_name = "RecDepth" end)
+    (struct let module_name = "CallDepth" end)
 
 module VarCopies =
   Datatype.List (Datatype.Pair (Cil_datatype.Varinfo) (Cil_datatype.Varinfo))
@@ -151,22 +144,28 @@ let make_stack (kf, depth) =
 
 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 make_recursion kf depth =
+  warn_recursive_call kf;
   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; }
+  { depth; substitution; base_substitution; withdrawal; base_withdrawal; }
+
+let get_recursion 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
+  if depth > 0
+  then Some (make_recursion kf depth)
+  else None
 
 let revert_recursion recursion =
   let revert (v1, v2) = v2, v1 in
-  let substitution = List.map revert recursion.Eval.substitution in
+  let substitution = List.map revert recursion.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; }
+  { recursion with substitution; base_substitution; }

src/plugins/value/engine/recursion.mli

@@ -23,14 +23,11 @@
 (** Handling of recursion cycles in the callgraph *)
 
 open Cil_types
+open Eval
 
 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. *)
-
 (** TODO *)
-val make_recursive_call: kernel_function -> Eval.recursion
+val get_recursion: kernel_function -> recursion option
 
-val revert_recursion: Eval.recursion -> Eval.recursion
+val revert_recursion: recursion -> recursion

src/plugins/value/engine/transfer_stmt.ml

@@ -27,7 +27,7 @@ open Eval
 module type S = sig
   type state
   type value
-  type location
+  type loc
   val assign: state -> kinstr -> lval -> exp -> state or_bottom
   val assume: state -> stmt -> exp -> bool -> state or_bottom
   val call:
@@ -44,7 +44,7 @@ module type S = sig
     builtin: bool;
   }
   val compute_call_ref:
-    (stmt -> (location, value) call -> state -> call_result) ref
+    (stmt -> (loc, value) call -> recursion option ->state -> call_result) ref
 end
 
 (* Reference filled in by the callwise-inout callback *)
@@ -105,6 +105,17 @@ module DumpFileCounters =
       let name = "Transfer_stmt.DumpFileCounters"
     end)
 
+module VarHashtbl = Cil_datatype.Varinfo.Hashtbl
+
+let substitution_visitor table = object
+  inherit Visitor.frama_c_copy (Project.current ())
+
+  method! vvrbl varinfo =
+    match VarHashtbl.find_opt table varinfo with
+    | None -> Cil.JustCopy
+    | Some lval -> Cil.ChangeTo lval
+end
+
 module Make (Abstract: Abstractions.Eva) = struct
 
   module Value = Abstract.Val
@@ -114,7 +125,7 @@ module Make (Abstract: Abstractions.Eva) = struct
 
   type state = Domain.t
   type value = Value.t
-  type location = Location.location
+  type loc = Location.location
 
   (* When using a product of domains, a product of states may have no
      concretization (if the domains have inferred incompatible properties)
@@ -295,8 +306,8 @@ module Make (Abstract: Abstractions.Eva) = struct
   }
 
   (* Forward reference to [Eval_funs.compute_call] *)
-  let compute_call_ref
-    : (stmt -> (location, value) call -> Domain.state -> call_result) ref
+  let compute_call_ref :
+    (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
     = ref (fun _ -> assert false)
 
   (* Returns the result of a call, and a boolean that indicates whether a
@@ -315,7 +326,7 @@ module Make (Abstract: Abstractions.Eva) = struct
         match Domain.start_call stmt call recursion domain_valuation state with
         | `Value state ->
           Domain.Store.register_initial_state (Value_util.call_stack ()) state;
-          !compute_call_ref stmt call state
+          !compute_call_ref stmt call recursion state
         | `Bottom ->
           { states = `Bottom; cacheable = Cacheable; builtin=false }
       in
@@ -526,7 +537,6 @@ module Make (Abstract: Abstractions.Eva) = struct
 
   (* Create an Eval.call *)
   let create_call kf args =
-    let recursive = Recursion.is_recursive_call kf in
     let return = Library_functions.get_retres_vi kf in
     let arguments, rest =
       let formals = Kernel_function.get_formals kf in
@@ -541,9 +551,9 @@ module Make (Abstract: Abstractions.Eva) = struct
       let arguments = List.rev arguments in
       arguments, rest
     in
-    {kf; arguments; rest; return; recursive; }
+    {kf; arguments; rest; return; }
 
-  let substitute_assigned_value substitution = function
+  let replace_value substitution = function
     | Assign value -> Assign (Value.replace_base substitution value)
     | Copy (loc, flagged) ->
       let v = flagged.v >>-: Value.replace_base substitution in
@@ -551,13 +561,17 @@ module Make (Abstract: Abstractions.Eva) = struct
       (* TODO: replace base in [loc] *)
       Copy (loc, flagged)
 
-  let substitute_argument substitution argument =
-    let avalue = substitute_assigned_value substitution argument.avalue in
-    { argument with avalue }
-
-  let substitute_call substitution call =
-    let arguments = List.map (substitute_argument substitution) call.arguments in
-    { call with arguments }
+  let replace_recursive_call recursion call =
+    let tbl = VarHashtbl.create 9 in
+    List.iter (fun (v1, v2) -> VarHashtbl.add tbl v1 v2) recursion.substitution;
+    let visitor = substitution_visitor tbl in
+    let replace_arg argument =
+      let concrete = Visitor.visitFramacExpr visitor argument.concrete in
+      let avalue = replace_value recursion.base_substitution argument.avalue in
+      { argument with concrete; avalue }
+    in
+    let arguments = List.map replace_arg call.arguments in
+    { call with arguments; }
 
   let make_call ~subdivnb kf arguments valuation state =
     (* Evaluate the arguments of the call. *)
@@ -565,16 +579,8 @@ module Make (Abstract: Abstractions.Eva) = struct
     compute_actuals ~subdivnb ~determinate valuation state arguments
     >>=: fun (args, valuation) ->
     let call = create_call kf args in
-    let recursion =
-      if call.recursive
-      then Some (Recursion.make_recursive_call call.kf)
-      else None
-    in
-    let call =
-      match recursion with
-      | None -> call
-      | Some recursion -> substitute_call recursion.base_substitution call
-    in
+    let recursion = Recursion.get_recursion kf in
+    let call = Extlib.opt_fold replace_recursive_call recursion call in
     call, recursion, valuation
 
   (* ----------------- show_each and dump_each directives ------------------- *)

src/plugins/value/engine/transfer_stmt.mli

@@ -29,7 +29,7 @@ module type S = sig
 
   type state
   type value
-  type location
+  type loc
 
   val assign: state -> kinstr -> lval -> exp -> state or_bottom
 
@@ -55,13 +55,13 @@ module type S = sig
   }
 
   val compute_call_ref:
-    (stmt -> (location, value) call -> state -> call_result) ref
+    (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
 end
 
 module Make (Abstract: Abstractions.Eva)
   : S with type state = Abstract.Dom.t
        and type value = Abstract.Val.t
-       and type location = Abstract.Loc.location
+       and type loc = Abstract.Loc.location
 
 (*
 Local Variables:

src/plugins/value/eval.ml

@@ -245,7 +245,6 @@ type ('loc, 'value) call = {
   arguments: ('loc, 'value) argument list;
   rest: (exp * ('loc, 'value) assigned) list;
   return: varinfo option;
-  recursive: bool;
 }
 
 type recursion = {

src/plugins/value/eval.mli

@@ -231,7 +231,6 @@ type ('loc, 'value) call = {
                                                   return value of the call.
                                                   Same varinfo for every
                                                   call to a given function. *)
-  recursive: bool;
 }
 
 (** Information needed to interpret a recursive call.