From 691a9d59a6c2451fa58447f4db406205ec41d33b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 25 Sep 2020 15:00:41 +0200
Subject: [PATCH] [Eva] In abstract values, adds a new function [replace_base].
This function substitutes variables in pointer values.
---
src/plugins/value/values/abstract_value.mli | 3 +++
src/plugins/value/values/main_values.ml | 3 +++
src/plugins/value/values/numerors/numerors_value.ml | 1 +
src/plugins/value/values/offsm_value.ml | 5 +++++
src/plugins/value/values/sign_value.ml | 2 ++
src/plugins/value/values/value_product.ml | 4 ++++
6 files changed, 18 insertions(+)
diff --git a/src/plugins/value/values/abstract_value.mli b/src/plugins/value/values/abstract_value.mli
index 05e465434ff..ac8ddecc5dc 100644
--- a/src/plugins/value/values/abstract_value.mli
+++ b/src/plugins/value/values/abstract_value.mli
@@ -182,12 +182,15 @@ module type S = sig
dst_val: t ->
t option or_bottom
+ (** {3 Misc } *)
+
val resolve_functions : t -> Kernel_function.t list or_top * bool
(** [resolve_functions v] returns the list of functions that may be pointed to
by the abstract value [v] (representing a function pointer). The returned
boolean must be [true] if some of the values represented by [v] do not
correspond to functions. It is always safe to return [`Top, true]. *)
+ val replace_base: Base.substitution -> t -> t
end
type 'v key = 'v Structure.Key_Value.key
diff --git a/src/plugins/value/values/main_values.ml b/src/plugins/value/values/main_values.ml
index b21f868739e..b38d4fcaf3a 100644
--- a/src/plugins/value/values/main_values.ml
+++ b/src/plugins/value/values/main_values.ml
@@ -132,6 +132,8 @@ module CVal = struct
let kfs, alarm = Locations.Location_Bytes.fold_topset_ok aux v init in
`Value kfs, alarm
with Abstract_interp.Error_Top -> `Top, true
+
+ let replace_base substitution t = snd (Cvalue.V.replace_base substitution t)
end
module Interval = struct
@@ -175,6 +177,7 @@ module Interval = struct
let forward_cast ~src_type:_ ~dst_type:_ _ = `Value top
let resolve_functions _ = `Top, true
+ let replace_base _substitution t = t
let rewrap_integer range value =
match value with
diff --git a/src/plugins/value/values/numerors/numerors_value.ml b/src/plugins/value/values/numerors/numerors_value.ml
index 2832d06cb35..5381969a55f 100644
--- a/src/plugins/value/values/numerors/numerors_value.ml
+++ b/src/plugins/value/values/numerors/numerors_value.ml
@@ -318,6 +318,7 @@ let assume_comparable _cmp v1 v2 = `Unknown (v1, v2)
let rewrap_integer _ _ = top
let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ = `Value None
let resolve_functions _ = `Top, true
+let replace_base _substitution t = t
(*-----------------------------------------------------------------------------
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index b46b11002e8..f6fd8d3fd66 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -434,6 +434,11 @@ module Offsm : Abstract_value.Leaf with type t = offsm_or_top = struct
else Top
let resolve_functions _ = `Top, true (* TODO: extract value *)
+ let replace_base substitution = function
+ | Top -> Top
+ | O offsm ->
+ let f v = snd (Cvalue.V_Or_Uninitialized.replace_base substitution v) in
+ O (Cvalue.V_Offsetmap.map_on_values f offsm)
let forward_unop _typ op o =
let o' = match o, op with
diff --git a/src/plugins/value/values/sign_value.ml b/src/plugins/value/values/sign_value.ml
index b9f59f90e27..08334941537 100644
--- a/src/plugins/value/values/sign_value.ml
+++ b/src/plugins/value/values/sign_value.ml
@@ -107,6 +107,8 @@ let constant _ = function
precisely *)
let resolve_functions _ = `Top, true
+let replace_base _substitution t = t
+
(** {2 Alarms} *)
let assume_non_zero v =
diff --git a/src/plugins/value/values/value_product.ml b/src/plugins/value/values/value_product.ml
index 7e89f1fc751..03ec02d71f2 100644
--- a/src/plugins/value/values/value_product.ml
+++ b/src/plugins/value/values/value_product.ml
@@ -125,6 +125,10 @@ module Make
in
list, b1 && b2
+ let replace_base substitution (left, right) =
+ Left.replace_base substitution left,
+ Right.replace_base substitution right
+
let reduce (orig_left, orig_right) left right = match left, right with
| None, None -> None
| Some left, None -> Some (left, orig_right)
--
GitLab