From cb9a91334500d8ae8ba101f85e1d60aa2f9dbc70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 30 Nov 2020 10:26:32 +0100
Subject: [PATCH] [Eva] Adds [replace_base] in abstract locations.
Applies the substitution of local and formal variables to the copy of variables
in recursive calls.
---
src/plugins/value/engine/transfer_stmt.ml | 9 ++++++---
.../value/values/abstract_location.mli | 2 ++
src/plugins/value/values/main_locations.ml | 2 ++
src/plugins/value_types/precise_locs.ml | 19 +++++++++++++++++++
src/plugins/value_types/precise_locs.mli | 2 ++
5 files changed, 31 insertions(+), 3 deletions(-)
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index eaaaca8f673..8cdbc6d4dff 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -553,21 +553,24 @@ module Make (Abstract: Abstractions.Eva) = struct
in
{kf; arguments; rest; return; }
- let replace_value substitution = function
+ let replace_value visitor substitution = function
| Assign value -> Assign (Value.replace_base substitution value)
| Copy (loc, flagged) ->
let v = flagged.v >>-: Value.replace_base substitution in
let flagged = { flagged with v } in
- (* TODO: replace base in [loc] *)
+ let lloc = Location.replace_base substitution loc.lloc in
+ let lval = Visitor.visitFramacLval visitor loc.lval in
+ let loc = { loc with lval; lloc } in
Copy (loc, flagged)
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 base_substitution = recursion.base_substitution in
let replace_arg argument =
let concrete = Visitor.visitFramacExpr visitor argument.concrete in
- let avalue = replace_value recursion.base_substitution argument.avalue in
+ let avalue = replace_value visitor base_substitution argument.avalue in
{ argument with concrete; avalue }
in
let arguments = List.map replace_arg call.arguments in
diff --git a/src/plugins/value/values/abstract_location.mli b/src/plugins/value/values/abstract_location.mli
index df2247048be..00d64bc5f32 100644
--- a/src/plugins/value/values/abstract_location.mli
+++ b/src/plugins/value/values/abstract_location.mli
@@ -44,6 +44,8 @@ module type S = sig
val to_value : location -> value
val size : location -> Int_Base.t
+ val replace_base: Base.substitution -> location -> location
+
(** {3 Alarms } *)
(** These functions are used to create the alarms that report undesirable
diff --git a/src/plugins/value/values/main_locations.ml b/src/plugins/value/values/main_locations.ml
index 7aab78471df..7dd75133117 100644
--- a/src/plugins/value/values/main_locations.ml
+++ b/src/plugins/value/values/main_locations.ml
@@ -62,6 +62,8 @@ module PLoc = struct
else `Unknown (l1, l2)
else `True
+ let replace_base = Precise_locs.replace_base
+
(* ------------------------------------------------------------------------ *)
(* Offsets *)
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/value_types/precise_locs.ml b/src/plugins/value_types/precise_locs.ml
index 63faec349a5..905339d0fd2 100644
--- a/src/plugins/value_types/precise_locs.ml
+++ b/src/plugins/value_types/precise_locs.ml
@@ -263,6 +263,25 @@ let loc_top = {
}
let is_top_loc pl = equal_loc loc_top pl
+let replace_base substitution po =
+ match po.loc with
+ | PLBottom -> po
+ | PLLoc loc ->
+ let modified, loc = Location_Bits.replace_base substitution loc in
+ if modified then { po with loc = PLLoc loc } else po
+ | PLVarOffset (base, offset) ->
+ let set = Base.Hptset.singleton base in
+ let modified, set = Base.Hptset.replace substitution set in
+ if modified then
+ let base = Option.get (Base.Hptset.contains_single_elt set) in
+ { po with loc = PLVarOffset (base, offset) }
+ else po
+ | PLLocOffset (loc, offset) ->
+ let modified, loc = Location_Bits.replace_base substitution loc in
+ if modified
+ then { po with loc = PLLocOffset (loc, offset) }
+ else po
+
let rec fold_offset f po acc =
match po with
| POBottom -> f Ival.bottom acc
diff --git a/src/plugins/value_types/precise_locs.mli b/src/plugins/value_types/precise_locs.mli
index ba93233b11a..cdff5d94de1 100644
--- a/src/plugins/value_types/precise_locs.mli
+++ b/src/plugins/value_types/precise_locs.mli
@@ -84,6 +84,8 @@ val is_bottom_loc: precise_location -> bool
val loc_top : precise_location
val is_top_loc: precise_location -> bool
+val replace_base: Base.substitution -> precise_location -> precise_location
+
val fold:
(Locations.location -> 'a -> 'a) -> precise_location -> 'a -> 'a
--
GitLab