From 7e15d177ce577ac4ba479713a1c4ce69c30df513 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 18 Sep 2020 10:12:12 +0200
Subject: [PATCH] [Eva] Abstract domains support recursion in [start_call] and
[finalize_call].
Through a new argument [recursion].
---
src/plugins/value/domains/abstract_domain.mli | 5 ++-
.../value/domains/apron/apron_domain.ml | 8 +++-
.../value/domains/cvalue/cvalue_domain.ml | 34 +++++++++++++----
.../value/domains/cvalue/cvalue_transfer.ml | 4 +-
src/plugins/value/domains/domain_builder.ml | 37 +++++++++++++------
src/plugins/value/domains/domain_lift.ml | 9 +++--
src/plugins/value/domains/domain_product.ml | 14 ++++---
.../value/domains/equality/equality_domain.ml | 9 ++++-
.../value/domains/gauges/gauges_domain.ml | 12 ++++--
src/plugins/value/domains/inout_domain.ml | 5 ++-
src/plugins/value/domains/octagons.ml | 9 ++++-
src/plugins/value/domains/offsm_domain.ml | 10 ++++-
src/plugins/value/domains/simple_memory.ml | 28 ++++++++++++--
src/plugins/value/domains/symbolic_locs.ml | 10 ++++-
src/plugins/value/domains/traces_domain.ml | 4 +-
src/plugins/value/domains/unit_domain.ml | 4 +-
src/plugins/value/engine/transfer_stmt.ml | 21 +++++++----
17 files changed, 161 insertions(+), 62 deletions(-)
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index a667687b8c6..472f056cf79 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -260,7 +260,7 @@ module type Transfer = sig
- [valuation] is a cache for all values and locations computed during
the evaluation of the function and its arguments. *)
val start_call:
- stmt -> (location, value) call ->
+ stmt -> (location, value) call -> recursion option ->
(value, location, origin) valuation -> state -> state or_bottom
(** [finalize_call stmt call ~pre ~post] computes the state after a function
@@ -271,7 +271,8 @@ module type Transfer = sig
- [pre] and [post] are the states before and at the end of the call
respectively. *)
val finalize_call:
- stmt -> (location, value) call -> pre:state -> post:state -> state or_bottom
+ stmt -> (location, value) call -> recursion option ->
+ pre:state -> post:state -> state or_bottom
(** Called on the Frama_C_show_each directives. Prints the internal properties
inferred by the domain in the [state] about the expression [exp]. Can use
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 9c2d3e85184..9bfd7edafd3 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -634,7 +634,11 @@ module Make (Man : Input) = struct
with
| Out_of_Scope _ -> `Value state
- let start_call _stmt call valuation state =
+ let start_call _stmt call recursion valuation state =
+ if recursion <> None
+ then
+ Value_parameters.abort ~current:true
+ "The binding to APRON domains does not support recursive calls.";
update valuation state >>- fun state ->
let eval = make_eval state in
let oracle = make_oracle valuation in
@@ -669,7 +673,7 @@ module Make (Man : Input) = struct
then `Bottom
else `Value state
- let finalize_call _stmt _call ~pre:_ ~post = `Value post
+ let finalize_call _stmt _call _recursion ~pre:_ ~post = `Value post
let show_expr _valuation _state _fmt _expr = ()
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 661b972b1ad..c7e2889e3df 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -230,15 +230,33 @@ module State = struct
Cvalue_transfer.assume stmt expr positive valuation s >>-: fun s ->
s, clob
- let start_call stmt call valuation (s, _clob) =
- Cvalue_transfer.start_call stmt call valuation s >>-: fun state ->
- state, Locals_scoping.bottom ()
-
- let finalize_call stmt call ~pre ~post =
- let (post_state, post_clob) = post
- and pre_state, clob = pre in
+ let start_recursive_call recursion (state, clob) =
+ let state = Model.remove_variables recursion.withdrawal state in
+ let state = Model.replace_base recursion.base_substitution state in
+ Locals_scoping.substitute recursion.base_substitution clob state
+
+ let start_call stmt call recursion valuation (state, clob) =
+ let state =
+ match recursion with
+ | None -> state
+ | Some recursion -> start_recursive_call recursion (state, clob)
+ in
+ Cvalue_transfer.start_call stmt call recursion valuation state
+ >>-: fun state -> state, Locals_scoping.bottom ()
+
+ let finalize_recursive_call ~pre recursion (state, clob) =
+ let shape = Base.Hptset.shape recursion.base_withdrawal in
+ let inter = Cvalue.Model.filter_by_shape shape pre in
+ let state = Cvalue.Model.merge ~into:state inter in
+ let state = Model.replace_base recursion.base_substitution state in
+ Locals_scoping.substitute recursion.base_substitution clob state, clob
+
+ let finalize_call stmt call recursion ~pre ~post =
+ let pre, clob = pre in
+ let post = Extlib.opt_fold (finalize_recursive_call ~pre) recursion post in
+ let (post, post_clob) = post in
Locals_scoping.(remember_bases_with_locals clob post_clob.clob);
- Cvalue_transfer.finalize_call stmt call ~pre:pre_state ~post:post_state
+ Cvalue_transfer.finalize_call stmt call recursion ~pre ~post
>>-: fun state ->
state, clob
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index 1f2c6672623..1e7bedefe0b 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -204,14 +204,14 @@ let actualize_formals state arguments =
in
List.fold_left treat_one_formal state arguments
-let start_call _stmt call valuation state =
+let start_call _stmt call _recursion valuation state =
let state = update valuation state in
let with_formals = actualize_formals state call.arguments in
let stack_with_call = Value_util.call_stack () in
Db.Value.Call_Value_Callbacks.apply (with_formals, stack_with_call);
`Value with_formals
-let finalize_call stmt call ~pre:_ ~post:state =
+let finalize_call stmt call _recursion ~pre:_ ~post:state =
(* Deallocate memory allocated via alloca().
To minimize computations, only do it for function definitions. *)
let state' =
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index f19b48efa12..62f4e168dc7 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -82,10 +82,16 @@ module Make_Minimal
let assume stmt expr positive _valuation state =
Domain.assume stmt expr positive state
- let start_call stmt call _valuation state =
- `Value (Domain.start_call stmt (simplify_call call) state)
-
- let finalize_call stmt call ~pre ~post =
+ let start_call stmt call recursion _valuation state =
+ match recursion with
+ | None -> `Value (Domain.start_call stmt (simplify_call call) state)
+ | Some _ ->
+ (* TODO *)
+ Value_parameters.abort
+ "The domain %s does not support recursive call." Domain.name
+
+ let finalize_call stmt call recursion ~pre ~post =
+ assert (recursion = None);
Domain.finalize_call stmt (simplify_call call) ~pre ~post
let show_expr _valuation = Domain.show_expr
@@ -218,9 +224,18 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
Domain.assign kinstr lv expr value (record valuation) state
let assume stmt expr positive valuation state =
Domain.assume stmt expr positive (record valuation) state
- let start_call stmt call valuation state =
- `Value (Domain.start_call stmt call (record valuation) state)
- let finalize_call = Domain.finalize_call
+
+ let start_call stmt call recursion valuation state =
+ match recursion with
+ | None -> `Value (Domain.start_call stmt call (record valuation) state)
+ | Some _ ->
+ (* TODO *)
+ Value_parameters.abort
+ "The domain %s does not support recursive call." Domain.name
+
+ let finalize_call stmt call recursion =
+ assert (recursion = None);
+ Domain.finalize_call stmt call
let show_expr _valuation = Domain.show_expr
@@ -436,7 +451,7 @@ module Restrict
- otherwise, only propagate the state from the call site to kill the
properties that depend on locations written in the called functions. *)
- let start_call stmt call valuation state =
+ let start_call stmt call recursion valuation state =
(* Starts the call with mode [new_mode]. [previous_mode] is the current mode
of the caller. *)
let start_call_with_mode ?previous_mode ~new_mode state =
@@ -444,7 +459,7 @@ module Restrict
then
match previous_mode with
| Some mode when mode.current.write ->
- Domain.start_call stmt call valuation state >>-: fun state ->
+ Domain.start_call stmt call recursion valuation state >>-: fun state ->
Some (state, new_mode)
| _ ->
`Value (Some (start_analysis call state, new_mode))
@@ -465,13 +480,13 @@ module Restrict
| None, None ->
`Value None
- let finalize_call stmt call ~pre ~post =
+ let finalize_call stmt call recursion ~pre ~post =
match pre, post with
| None, _ | _, None -> `Value None
| Some (pre, pre_mode), Some (post, post_mode) ->
if post_mode.current.write
then
- Domain.finalize_call stmt call ~pre ~post >>-: fun state ->
+ Domain.finalize_call stmt call recursion ~pre ~post >>-: fun state ->
Some (state, pre_mode)
else
`Value (Some (post, pre_mode))
diff --git a/src/plugins/value/domains/domain_lift.ml b/src/plugins/value/domains/domain_lift.ml
index 0ff4608c1cd..63fe0d3bdf2 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -116,11 +116,12 @@ module Make
let assume stmt expr positive valuation state =
Domain.assume stmt expr positive (lift_valuation valuation) state
- let start_call stmt call valuation state =
- Domain.start_call stmt (lift_call call) (lift_valuation valuation) state
+ let start_call stmt call recursion valuation state =
+ Domain.start_call
+ stmt (lift_call call) recursion (lift_valuation valuation) state
- let finalize_call stmt call ~pre ~post =
- Domain.finalize_call stmt (lift_call call) ~pre ~post
+ let finalize_call stmt call recursion ~pre ~post =
+ Domain.finalize_call stmt (lift_call call) recursion ~pre ~post
let show_expr valuation = Domain.show_expr (lift_valuation valuation)
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 683892ef2dc..4ea88b8b41f 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -155,18 +155,20 @@ module Make
Right.assume stmt expr positive (right_val valuation) right >>-: fun right ->
left, right
- let finalize_call stmt call ~pre ~post =
+ let finalize_call stmt call recursion ~pre ~post =
let pre_left, pre_right = pre
and left_state, right_state = post in
- Left.finalize_call stmt call ~pre:pre_left ~post:left_state
+ Left.finalize_call stmt call recursion ~pre:pre_left ~post:left_state
>>- fun left ->
- Right.finalize_call stmt call ~pre:pre_right ~post:right_state
+ Right.finalize_call stmt call recursion ~pre:pre_right ~post:right_state
>>-: fun right ->
left, right
- let start_call stmt call valuation (left, right) =
- Left.start_call stmt call (left_val valuation) left >>- fun left ->
- Right.start_call stmt call (right_val valuation) right >>-: fun right ->
+ let start_call stmt call recursion valuation (left, right) =
+ Left.start_call stmt call recursion (left_val valuation) left
+ >>- fun left ->
+ Right.start_call stmt call recursion (right_val valuation) right
+ >>-: fun right ->
left, right
let show_expr =
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 2849ec1f6f3..4bc2213fcca 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -473,16 +473,21 @@ module Make
end
| _ -> `Value state
- let start_call _stmt call valuation state =
+ let start_recursive_call recursion state =
+ let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+ unscope state vars
+
+ let start_call _stmt call recursion valuation state =
let state =
match call_init_state call.kf with
| ISCaller -> assign_formals valuation call state
| ISFormals -> assign_formals valuation call empty
| ISEmpty -> empty
in
+ let state = Extlib.opt_fold start_recursive_call recursion state in
`Value state
- let finalize_call _stmt call ~pre ~post =
+ let finalize_call _stmt call _recursion ~pre ~post =
if call_init_state call.kf = ISCaller then
`Value post (* [pre] was the state inferred in the caller, and it
has been updated during the analysis of [kf] into
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 00641adb100..8b45d1c11ff 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1208,7 +1208,7 @@ module D_Impl : Abstract_domain.S
try `Value (G.assign to_loc to_val lv.lval e state)
with Unassignable -> `Value (kill lv.lloc state)
- let finalize_call _stmt _call ~pre ~post =
+ let finalize_call _stmt _call _recursion ~pre ~post =
let state =
match function_calls_handling with
| FullInterprocedural -> post
@@ -1217,10 +1217,16 @@ module D_Impl : Abstract_domain.S
in
`Value state
- let start_call _stmt call valuation state =
+ let start_recursive_call recursion state =
+ let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+ remove_variables vars state
+
+ let start_call _stmt call recursion valuation state =
let state =
match function_calls_handling with
- | FullInterprocedural -> update valuation state
+ | FullInterprocedural ->
+ let state = Extlib.opt_fold start_recursive_call recursion state in
+ update valuation state
| IntraproceduralAll
| IntraproceduralNonReferenced -> `Value G.empty
in
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index a51098e16eb..bda7c81868a 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -241,9 +241,10 @@ module Internal
let effects = Transfer.effects_assume to_z e in
`Value (Transfer.catenate state effects)
- let start_call _stmt _call _valuation _state = `Value LatticeInout.empty
+ let start_call _stmt _call _recursion _valuation _state =
+ `Value LatticeInout.empty
- let finalize_call _stmt _call ~pre ~post =
+ let finalize_call _stmt _call _recursion ~pre ~post =
`Value (Transfer.catenate pre post)
let update _valuation state = `Value state
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 2be0ff0dfa9..b63cce8fc72 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -1216,17 +1216,22 @@ module Domain = struct
let assume _stmt _exp _bool = update
- let start_call _stmt call valuation state =
+ let start_recursive_call recursion state =
+ let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+ List.fold_left State.remove state vars
+
+ let start_call _stmt call recursion valuation state =
if intraprocedural ()
then `Value (empty ())
else
+ let state = Extlib.opt_fold start_recursive_call recursion state in
let state = { state with modified = Locations.Zone.bottom } in
let assign_formal state { formal; concrete; avalue } =
state >>- assign_variable formal concrete avalue valuation
in
List.fold_left assign_formal (`Value state) call.arguments
- let finalize_call _stmt _call ~pre ~post =
+ let finalize_call _stmt _call _recursion ~pre ~post =
if intraprocedural ()
then `Value (kill post.modified pre)
else
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index a2d8355c3e2..07872c80f08 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -157,9 +157,15 @@ module Internal : Domain_builder.InputDomain
let assume _ _ _ _ state = `Value state
- let finalize_call _stmt _call ~pre:_ ~post = `Value post
+ let finalize_call _stmt _call _recursion ~pre:_ ~post = `Value post
- let start_call _stmt _call valuation state = update valuation state
+ let start_recursive_call recursion state =
+ let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+ Memory.remove_variables vars state
+
+ let start_call _stmt _call recursion valuation state =
+ let state = Extlib.opt_fold start_recursive_call recursion state in
+ update valuation state
let show_expr _valuation _state _fmt _expr = ()
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 94a2f4c5f6c..1c5d96355de 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -52,11 +52,17 @@ module Make_Memory (Value: Value) = struct
module Initial_Values = struct let v = [] end
module Deps = struct let l = [Ast.self] end
- include Hptmap.Make (Base) (Value)(Hptmap.Comp_unused) (Initial_Values) (Deps)
+ include Hptmap.Make
+ (Base.Base) (Value)(Hptmap.Comp_unused) (Initial_Values) (Deps)
let cache_name s =
Hptmap_sig.PersistentCache ("Value." ^ Value.name ^ "." ^ s)
+ let disjoint_union =
+ let cache = cache_name "union" in
+ let decide _key _v1 _v2 = assert false in
+ join ~cache ~symmetric:true ~idempotent:true ~decide
+
let narrow =
let module E = struct exception Bottom end in
let cache = cache_name "narrow" in
@@ -259,7 +265,14 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
abstraction of the domain itself. *)
let assume _stmt _expr _pos = update
- let start_call _stmt call _valuation state =
+ let start_recusive_call recursion state =
+ let state = remove_variables recursion.withdrawal state in
+ (* No collision should occur in the substitution. *)
+ let decide _key _v1 _v2 = assert false in
+ snd (replace_key ~decide recursion.base_substitution state)
+
+ let start_call _stmt call recursion _valuation state =
+ let state = Extlib.opt_fold start_recusive_call recursion state in
let bind_argument state argument =
let typ = argument.formal.vtype in
let loc = Main_locations.PLoc.eval_varinfo argument.formal in
@@ -269,8 +282,17 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
let state = List.fold_left bind_argument state call.arguments in
`Value state
- let finalize_call _stmt call ~pre:_ ~post =
+ let finalize_recursive_call ~pre recursion state =
+ let shape = Base.Hptset.shape recursion.base_withdrawal in
+ let inter = inter_with_shape shape pre in
+ let state = disjoint_union state inter in
+ (* No collision should occur in the substitution. *)
+ let decide _key _v1 _v2 = assert false in
+ snd (replace_key ~decide recursion.base_substitution state)
+
+ let finalize_call _stmt call recursion ~pre ~post =
let kf_name = Kernel_function.get_name call.kf in
+ let post = Extlib.opt_fold (finalize_recursive_call ~pre) recursion post in
match find_builtin kf_name, call.return with
| None, _ | _, None -> `Value post
| Some f, Some return ->
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 2c2f51d88a2..03f5bb73961 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -563,9 +563,15 @@ module Internal : Domain_builder.InputDomain
let assume _stmt _exp _pos valuation state = update valuation state
- let start_call _stmt _call valuation state = update valuation state
+ let start_recursive_call recursion state =
+ let vars = List.map fst recursion.substitution @ recursion.withdrawal in
+ Memory.remove_variables vars state
+
+ let start_call _stmt _call recursion valuation state =
+ let state = Extlib.opt_fold start_recursive_call recursion state in
+ update valuation state
- let finalize_call _stmt _call ~pre:_ ~post = `Value post
+ let finalize_call _stmt _call _recursion ~pre:_ ~post = `Value post
let show_expr _valuation _state _fmt _expr = ()
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 408114d1568..5f566f15944 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -865,7 +865,7 @@ module Internal = struct
let trans = Assume (stmt, e, pos) in
`Value (Traces.add_trans state trans)
- let start_call stmt call _valuation state =
+ let start_call stmt call _recursion _valuation state =
let kf = call.Eval.kf in
if Kernel_function.is_definition kf then
let msg = Format.asprintf "start_call: %s (%b)" (Kernel_function.get_name call.Eval.kf)
@@ -890,7 +890,7 @@ module Internal = struct
(CallDeclared (call.Eval.kf, exps, Option.map Cil.var var))
in `Value {state with call_declared_function = true}
- let finalize_call _stmt call ~pre:_ ~post =
+ let finalize_call _stmt call _recursion ~pre:_ ~post =
if post.call_declared_function
then `Value {post with call_declared_function = false}
else
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 5633d599dd5..0c90f11a488 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -63,8 +63,8 @@ module Make
let update _ _ = `Value ()
let assign _ _ _ _ _ _ = `Value ()
let assume _ _ _ _ _ = `Value ()
- let start_call _ _ _ _ = `Value ()
- let finalize_call _ _ ~pre:_ ~post:_ = `Value ()
+ let start_call _ _ _ _ _ = `Value ()
+ let finalize_call _ _ _ ~pre:_ ~post:_ = `Value ()
let show_expr _ _ _ _ = ()
let logic_assign _ _ _ = ()
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 8e574e39a48..853705200e9 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -301,7 +301,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Returns the result of a call, and a boolean that indicates whether a
builtin has been used to interpret the call. *)
- let process_call stmt call valuation state =
+ let process_call stmt call recursion valuation state =
Value_util.push_call_stack call.kf (Kstmt stmt);
let cleanup () =
Value_util.pop_call_stack ();
@@ -312,7 +312,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let domain_valuation = Eval.to_domain_valuation valuation in
let res =
(* Process the call according to the domain decision. *)
- match Domain.start_call stmt call domain_valuation state with
+ 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
@@ -449,11 +449,11 @@ module Make (Abstract: Abstractions.Eva) = struct
Kernel_function.get_formals kf @ locals
(* Do the call to one function. *)
- let do_one_call valuation stmt lv call state =
+ let do_one_call valuation stmt lv call recursion state =
let kf_callee = call.kf in
let pre = state in
(* Process the call according to the domain decision. *)
- let call_result = process_call stmt call valuation state in
+ let call_result = process_call stmt call recursion valuation state in
call_result.cacheable,
call_result.states >>- fun result ->
let leaving_vars = leaving_vars kf_callee in
@@ -474,7 +474,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let post = Domain.leave_scope kf_callee leaving_vars state 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 ~pre ~post >>- fun state ->
+ 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
@@ -483,7 +483,7 @@ module Make (Abstract: Abstractions.Eva) = struct
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 ~pre ~post:state >>- fun state ->
+ Domain.finalize_call stmt call recursion ~pre ~post:state >>- fun state ->
treat_return ~kf_callee lv call.return stmt state
in
let states =
@@ -745,10 +745,17 @@ module Make (Abstract: Abstractions.Eva) = struct
let eval, alarms = make_call ~subdivnb kf args valuation state in
Alarmset.emit ki_call alarms;
eval >>- fun (call, valuation) ->
+ let recursion =
+ if call.recursive
+ then Some (Recursion.make_recursive_call call.kf)
+ else None
+ in
(* Register the call. *)
Value_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
(* Do the call. *)
- let c, states = do_one_call valuation stmt lval_option call state in
+ let c, states =
+ do_one_call valuation stmt lval_option call recursion state
+ in
(* If needed, propagate that callers cannot be cached. *)
if c = NoCacheCallers then
cacheable := NoCacheCallers;
--
GitLab