From b424b8975e12225cdb445b827a7ce728738e546f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 19 Apr 2021 12:05:24 +0200
Subject: [PATCH] [Eva] Fixes abstract domains uses of the valuation for
recursive calls.
On recursive calls, the substitution to be applied to the domain states is not
applied to the valuation given as argument to [start_call].
This commit:
- adds comment in the abstract domain signature to reflect this fact;
- fixes the domains to properly use the valuation in recursive calls.
The equality and octagon domains are now intra-procedural on recursive calls:
they always start the analysis of a recursive call with an empty state.
---
src/plugins/value/domains/abstract_domain.mli | 11 ++++++++++-
.../value/domains/cvalue/cvalue_domain.ml | 3 +++
.../value/domains/cvalue/cvalue_transfer.ml | 3 +--
.../value/domains/equality/equality_domain.ml | 17 ++++++++++++-----
.../value/domains/gauges/gauges_domain.ml | 4 ++--
src/plugins/value/domains/octagons.ml | 17 ++++++++++++-----
src/plugins/value/domains/offsm_domain.ml | 4 ++--
src/plugins/value/domains/symbolic_locs.ml | 4 ++--
8 files changed, 44 insertions(+), 19 deletions(-)
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 318a78d9638..7c5861aa942 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -260,7 +260,16 @@ module type Transfer = sig
It is None if the call is not recursive.
- [state] is the abstract state at the call site, before the call;
- [valuation] is a cache for all values and locations computed during
- the evaluation of the function and its arguments. *)
+ the evaluation of the function and its arguments.
+
+ On recursive calls, [recursion] contains some substitution of variables
+ to be applied on the domain state to prevent mixing up local variables
+ and formal parameters of different recursive calls.
+ See {!Eval.recursion} for more details.
+ This substitution has been applied on values and expressions in [call],
+ but not in the [valuation] given as argument. If the domain uses some
+ information from the [valuation] on a recursive call, it must apply the
+ substitution on it. *)
val start_call:
stmt -> (location, value) call -> recursion option ->
(value, location, origin) valuation -> state -> state or_bottom
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index e31a140be37..80f885d5936 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -245,6 +245,9 @@ module State = struct
Model.replace_base substitution state
let start_call stmt call recursion valuation (state, clob) =
+ (* Uses the [valuation] to update the [state] before the substitution
+ for recursive calls. *)
+ Cvalue_transfer.update valuation state >>- fun state ->
let state =
match recursion with
| None -> state
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index 1e7bedefe0b..26518aa8d7c 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -204,8 +204,7 @@ let actualize_formals state arguments =
in
List.fold_left treat_one_formal state arguments
-let start_call _stmt call _recursion valuation state =
- let state = update valuation state in
+let start_call _stmt call _recursion _valuation state =
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);
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 4bc2213fcca..74925890fdc 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -479,12 +479,19 @@ module Make
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
+ match recursion with
+ | Some recursion ->
+ (* No relation inferred from the assignment of formal parameters
+ for recursive calls, because the valuation cannot be used safely
+ as the substitution of local and formals variables has not been
+ applied to it. *)
+ start_recursive_call recursion state
+ | None ->
+ 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 _recursion ~pre ~post =
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 8b45d1c11ff..23cef9f01a2 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1225,8 +1225,8 @@ module D_Impl : Abstract_domain.S
let state =
match function_calls_handling with
| FullInterprocedural ->
- let state = Extlib.opt_fold start_recursive_call recursion state in
- update valuation state
+ update valuation state >>-: fun state ->
+ Extlib.opt_fold start_recursive_call recursion state
| IntraproceduralAll
| IntraproceduralNonReferenced -> `Value G.empty
in
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index b63cce8fc72..e45b1c875de 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -1224,12 +1224,19 @@ module Domain = struct
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
+ match recursion with
+ | Some recursion ->
+ (* No relation inferred from the assignment of formal parameters
+ for recursive calls, because the valuation cannot be used safely
+ as the substitution of local and formals variables has not been
+ applied to it. *)
+ `Value (start_recursive_call recursion state)
+ | None ->
+ 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 _recursion ~pre ~post =
if intraprocedural ()
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 07872c80f08..70f2f43ccca 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -164,8 +164,8 @@ module Internal : Domain_builder.InputDomain
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
+ update valuation state >>-: fun state ->
+ Extlib.opt_fold start_recursive_call recursion state
let show_expr _valuation _state _fmt _expr = ()
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 03f5bb73961..bd2fab8b55a 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -568,8 +568,8 @@ module Internal : Domain_builder.InputDomain
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
+ update valuation state >>-: fun state ->
+ Extlib.opt_fold start_recursive_call recursion state
let finalize_call _stmt _call _recursion ~pre:_ ~post = `Value post
--
GitLab