From df7de13be89bb8349e04c903c4bcdbe2fb97f907 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 14 Sep 2020 16:50:40 +0200
Subject: [PATCH] [Eva] New type Eval.recursion to support recursion in
abstract domains.
---
src/plugins/value/engine/compute_functions.ml | 3 +-
src/plugins/value/engine/recursion.ml | 72 ++++++++++++++++++-
src/plugins/value/engine/recursion.mli | 5 ++
src/plugins/value/engine/transfer_stmt.ml | 2 +-
src/plugins/value/eval.ml | 8 +++
src/plugins/value/eval.mli | 15 +++-
6 files changed, 100 insertions(+), 5 deletions(-)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index b622130d6e7..6a721abfab9 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 99d150435c7..c7a7dfe117a 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 3a3255c47d1..80c28c1cd88 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 040629aa886..8e574e39a48 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 8aab315162a..ab4e77305f4 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 e050aae7848..ef1a1937757 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
--
GitLab