From db7526e879f480adc0d7b29e7c781340c2b5e7e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 5 Mar 2021 14:56:03 +0100
Subject: [PATCH] [Eva] Fixes the cvalue domain on recursive calls.
---
.../value/domains/cvalue/cvalue_domain.ml | 51 ++++++++-----------
.../value/domains/cvalue/locals_scoping.ml | 13 +++--
.../value/domains/cvalue/locals_scoping.mli | 5 +-
3 files changed, 31 insertions(+), 38 deletions(-)
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index aa7f27b0021..e31a140be37 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -230,21 +230,19 @@ module State = struct
Cvalue_transfer.assume stmt expr positive valuation s >>-: fun s ->
s, clob
+ let is_direct_recursion stmt call =
+ try
+ let kf = Kernel_function.find_englobing_kf stmt in
+ Kernel_function.equal kf call.kf
+ with Not_found -> false (* Should not happen *)
+
let start_recursive_call stmt call recursion (state, clob) =
- let direct =
- try
- let kf = Kernel_function.find_englobing_kf stmt in
- Kernel_function.equal kf call.kf
- with Not_found -> false (* Should not happen *)
- in
+ let direct = is_direct_recursion stmt call in
let state = Model.remove_variables recursion.withdrawal state in
- let state = Model.replace_base recursion.base_substitution state in
+ let substitution = recursion.base_substitution in
let clob = if direct then clob else Locals_scoping.top () in
- let state, set =
- Locals_scoping.substitute recursion.base_substitution clob state
- in
- Locals_scoping.remember_bases_with_locals clob (Base.SetLattice.inject set);
- state
+ let state = Locals_scoping.substitute substitution clob state in
+ Model.replace_base substitution state
let start_call stmt call recursion valuation (state, clob) =
let state =
@@ -256,31 +254,26 @@ module State = struct
>>-: fun state -> state, Locals_scoping.bottom ()
let finalize_recursive_call stmt call ~pre recursion state =
- let direct =
- try
- let kf = Kernel_function.find_englobing_kf stmt in
- Kernel_function.equal kf call.kf
- with Not_found -> false (* Should not happen *)
- in
+ let direct = is_direct_recursion stmt call in
let pre, clob = pre in
+ let substitution = recursion.base_substitution in
+ let state = Model.replace_base substitution state in
+ let clob = if direct then clob else Locals_scoping.top () in
+ let state = Locals_scoping.substitute substitution clob state in
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
- let clob = if direct then clob else Locals_scoping.top () in
- let state, _set =
- Locals_scoping.substitute recursion.base_substitution clob state
- in
- state
+ Cvalue.Model.merge ~into:state inter
let finalize_call stmt call recursion ~pre ~post =
+ let (pre, clob) = pre in
let (post, post_clob) = post in
+ Locals_scoping.(remember_bases_with_locals clob post_clob.clob);
let post =
- Extlib.opt_fold (finalize_recursive_call stmt call ~pre) recursion post
+ Extlib.opt_fold
+ (finalize_recursive_call stmt call ~pre:(pre, clob))
+ recursion post
in
- let (pre, clob) = pre in
- Locals_scoping.(remember_bases_with_locals clob post_clob.clob);
- Cvalue_transfer.finalize_call stmt call recursion ~pre ~post
+ Cvalue_transfer.finalize_call stmt call recursion ~pre ~post
>>-: fun state ->
state, clob
diff --git a/src/plugins/value/domains/cvalue/locals_scoping.ml b/src/plugins/value/domains/cvalue/locals_scoping.ml
index d8eea04d82b..9fc5b4d5dee 100644
--- a/src/plugins/value/domains/cvalue/locals_scoping.ml
+++ b/src/plugins/value/domains/cvalue/locals_scoping.ml
@@ -130,12 +130,12 @@ let make_escaping_fundec fundec clob vars state =
let substitute substitution clob state =
(* Apply the [substitution] to [offsm]. If it is modified, bind the new
offsetmap to [base] in [state], and add the [base] to [set]. *)
- let replace_offsm base offsm (state, set) =
+ let replace_offsm base offsm state =
let f v = snd (Cvalue.V_Or_Uninitialized.replace_base substitution v) in
let offsm' = Cvalue.V_Offsetmap.map_on_values f offsm in
if Cvalue.V_Offsetmap.equal offsm' offsm
- then state, set
- else Cvalue.Model.add_base base offsm' state, Base.Hptset.add base set
+ then state
+ else Cvalue.Model.add_base base offsm' state
in
(* Apply the substitution to the offsetmap bound to [base] in [state] *)
let replace_base base acc =
@@ -144,15 +144,14 @@ let substitute substitution clob state =
| `Top | `Bottom -> acc
| exception Not_found -> acc
in
- let acc = state, Base.Hptset.empty in
(* Iterate on all the bases that might contain a variable to substitute *)
- try Base.SetLattice.fold replace_base clob.clob (replace_base Base.null acc)
+ try Base.SetLattice.fold replace_base clob.clob (replace_base Base.null state)
with Abstract_interp.Error_Top ->
(* [clob] is too imprecise. Iterate on the entire memory state instead,
which is much slower. *)
match state with
- | Cvalue.Model.Top | Cvalue.Model.Bottom -> acc
- | Cvalue.Model.Map map -> Cvalue.Model.fold replace_offsm map acc
+ | Cvalue.Model.Top | Cvalue.Model.Bottom -> state
+ | Cvalue.Model.Map map -> Cvalue.Model.fold replace_offsm map state
(*
Local Variables:
diff --git a/src/plugins/value/domains/cvalue/locals_scoping.mli b/src/plugins/value/domains/cvalue/locals_scoping.mli
index 9da04c27dad..64cdf339a39 100644
--- a/src/plugins/value/domains/cvalue/locals_scoping.mli
+++ b/src/plugins/value/domains/cvalue/locals_scoping.mli
@@ -71,8 +71,9 @@ val make_escaping_fundec:
function, in which case a different warning is emitted. *)
val substitute:
- Base.substitution -> clobbered_set -> Cvalue.Model.t ->
- Cvalue.Model.t * Base.Hptset.t
+ Base.substitution -> clobbered_set -> Cvalue.Model.t -> Cvalue.Model.t
+(** [substitute substitution clob state] applies [substitution] to all pointer
+ values in the offsetmaps bound to variables in [clob] in [state]. *)
(*
Local Variables:
--
GitLab