diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 62f4e168dc79228f58b3c8650cec68a6b6f12a1a..0c5e09da764e81ee6ed1bd33f195255a9ed31e96 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/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)
diff --git a/src/plugins/value/domains/simpler_domains.mli b/src/plugins/value/domains/simpler_domains.mli
index 37a1209a79b929a90d05f63ff1c3afd2adf57773..ba32d0d3d2e0fd94a2c579e668e52ec73563e775 100644
--- a/src/plugins/value/domains/simpler_domains.mli
+++ b/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
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 8eaabed066410ff3309ad58a961f42d4faafd31f..4a438739080c1c4b727319ce9c5efbb0c5a3b8db 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/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 ();
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index 83133b6a202d3be19b18d13144971ec5c664b475..ea0471737a5b6efb8eabab0d7b40d181edf6369d 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/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; }
diff --git a/src/plugins/value/engine/recursion.mli b/src/plugins/value/engine/recursion.mli
index a446573aca8c6858c701f14993c1beef7baaae3f..3a83fbd0023ba10437f65d193719b4cb8730741e 100644
--- a/src/plugins/value/engine/recursion.mli
+++ b/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
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 10fd7aad07a7a8f2bad9703f492797dc77d931e3..eaaaca8f6733d99e76d54f3c5fae6dada4135fa8 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/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 ------------------- *)
diff --git a/src/plugins/value/engine/transfer_stmt.mli b/src/plugins/value/engine/transfer_stmt.mli
index af7e5fa3e7383125abfbb9101e64a23d5b8f9baf..87c505e24111ca06f51ce4a9cb5ee3fe9178c788 100644
--- a/src/plugins/value/engine/transfer_stmt.mli
+++ b/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:
diff --git a/src/plugins/value/eval.ml b/src/plugins/value/eval.ml
index ab4e77305f48391e739b76186615836e4bda4c36..74eb76353824f011548ccc8fe7727b42262cda2e 100644
--- a/src/plugins/value/eval.ml
+++ b/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 = {
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index ef1a1937757b26c68da7c2857e2bf350e902f857..c64f692b7bd70ac3b95eee342519317c3e0cb11a 100644
--- a/src/plugins/value/eval.mli
+++ b/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.