[Eva] New type Eval.recursion to support recursion in abstract domains.

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

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

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

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. *)

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
 
 (*

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