From cde12158a17c120e4d9d965a11f006c078fb12c9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 27 Feb 2020 13:33:12 +0100
Subject: [PATCH] [Eva] Abstract values: new function assume_pointer.
---
src/plugins/value/values/abstract_value.mli | 9 ++++++
src/plugins/value/values/cvalue_forward.ml | 29 +++++++++++++++++++
src/plugins/value/values/cvalue_forward.mli | 1 +
src/plugins/value/values/main_values.ml | 2 ++
.../value/values/numerors/numerors_value.ml | 1 +
src/plugins/value/values/offsm_value.ml | 1 +
src/plugins/value/values/sign_value.ml | 1 +
src/plugins/value/values/value_product.ml | 5 ++++
8 files changed, 49 insertions(+)
diff --git a/src/plugins/value/values/abstract_value.mli b/src/plugins/value/values/abstract_value.mli
index 378c06407ac..bd42be08f83 100644
--- a/src/plugins/value/values/abstract_value.mli
+++ b/src/plugins/value/values/abstract_value.mli
@@ -92,6 +92,15 @@ module type S = sig
floating-point values. *)
val assume_not_nan: assume_finite:bool -> fkind -> t -> t truth
+ (** Assumes that the abstract value only represents well-formed pointer values:
+ pointers either to an element of an array object or one past the last
+ element of an array object. (A pointer to an object that is not an element
+ of an array is viewed as a pointer to the first element of an array of
+ length one with the type of the object as its element type.)
+ The NULL pointer is always a valid pointer value. Function pointers are
+ also considered as valid pointer values for now. *)
+ val assume_pointer: t -> t truth
+
(* [assume_comparable cmp v1 v2] assumes that the integer or pointer values
[v1] and [v2] are comparable for [cmp]. Integers are always comparable.
If one value is a pointer, then both values should be pointers, and:
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index ad45ab9ddb8..6822e5f5a5c 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -220,6 +220,35 @@ let assume_not_nan ~assume_finite fkind v =
let res = Bottom.non_bottom (backward_propagate kind res) in
`Unknown (V.inject_float res)
+let nearly_valid_bits = function
+ | Base.Empty
+ | Base.Invalid -> Integer.zero, Integer.zero
+ | Base.Known (min, max) | Base.Unknown (min, _, max) -> min, Integer.succ max
+ | Base.Variable variable -> Integer.zero, Integer.succ variable.Base.max_alloc
+
+let nearly_valid_offset base =
+ let min, max = nearly_valid_bits base in
+ let to_byte bound = Some (Integer.e_div bound (Bit_utils.sizeofchar ())) in
+ Ival.inject_range (to_byte min) (to_byte max)
+
+let assume_pointer loc =
+ let aux base ival (acc_v, acc_ok) =
+ let validity = Base.validity base in
+ let nearly_valid_ival = nearly_valid_offset validity in
+ let new_ival = Ival.narrow ival nearly_valid_ival in
+ let ival, ok =
+ if Base.is_null base && Ival.contains_zero ival
+ then Ival.(join zero new_ival), acc_ok && Ival.is_zero ival
+ else new_ival, acc_ok && Ival.equal ival new_ival
+ in
+ Locations.Location_Bytes.add base ival acc_v, ok
+ in
+ try
+ let loc, ok = Cvalue.V.(fold_topset_ok aux loc (bottom, true)) in
+ if Cvalue.V.is_bottom loc then `False
+ else if ok then `True else `Unknown loc
+ with Abstract_interp.Error_Top -> `Unknown loc
+
(* --------------------------------------------------------------------------
Integer overflow
-------------------------------------------------------------------------- *)
diff --git a/src/plugins/value/values/cvalue_forward.mli b/src/plugins/value/values/cvalue_forward.mli
index 77b587c28e4..07fb2ef7591 100644
--- a/src/plugins/value/values/cvalue_forward.mli
+++ b/src/plugins/value/values/cvalue_forward.mli
@@ -31,6 +31,7 @@ val are_comparable: Abstract_interp.Comp.t -> V.t -> V.t -> bool
val assume_non_zero: V.t -> V.t truth
val assume_bounded: bound_kind -> bound -> V.t -> V.t truth
val assume_not_nan: assume_finite:bool -> fkind -> V.t -> V.t truth
+val assume_pointer: V.t -> V.t truth
val assume_comparable: pointer_comparison -> V.t -> V.t -> (V.t * V.t) truth
val forward_binop_int: typ: typ -> V.t -> binop -> V.t -> V.t
diff --git a/src/plugins/value/values/main_values.ml b/src/plugins/value/values/main_values.ml
index ebd8d3b0989..9218b0a03a3 100644
--- a/src/plugins/value/values/main_values.ml
+++ b/src/plugins/value/values/main_values.ml
@@ -46,6 +46,7 @@ module CVal = struct
let assume_non_zero = Cvalue_forward.assume_non_zero
let assume_bounded = Cvalue_forward.assume_bounded
let assume_not_nan = Cvalue_forward.assume_not_nan
+ let assume_pointer = Cvalue_forward.assume_pointer
let assume_comparable = Cvalue_forward.assume_comparable
let constant exp = function
@@ -165,6 +166,7 @@ module Interval = struct
let assume_non_zero v = `Unknown v
let assume_bounded _ _ v = `Unknown v
let assume_not_nan ~assume_finite:_ _ v = `Unknown v
+ let assume_pointer v = `Unknown v
let assume_comparable _ v1 v2 = `Unknown (v1, v2)
let constant _ _ = top
diff --git a/src/plugins/value/values/numerors/numerors_value.ml b/src/plugins/value/values/numerors/numerors_value.ml
index da6a115444b..443a2dd4434 100644
--- a/src/plugins/value/values/numerors/numerors_value.ml
+++ b/src/plugins/value/values/numerors/numerors_value.ml
@@ -312,6 +312,7 @@ let backward_binop ~input_type:_ ~resulting_type:_ op ~left ~right ~result =
let assume_non_zero v = `Unknown v
let assume_bounded _kind _bound v = `Unknown v
let assume_not_nan ~assume_finite:_ _fkind v = `Unknown v
+let assume_pointer v = `Unknown v
let assume_comparable _cmp v1 v2 = `Unknown (v1, v2)
let rewrap_integer _ _ = top
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index 672025219b7..d6d7995ae35 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -423,6 +423,7 @@ module Offsm : Abstract_value.Leaf with type t = offsm_or_top = struct
let assume_non_zero v = `Unknown v
let assume_bounded _ _ v = `Unknown v
let assume_not_nan ~assume_finite:_ _ v = `Unknown v
+ let assume_pointer v = `Unknown v
let assume_comparable _ v1 v2 = `Unknown (v1, v2)
let constant e _c =
diff --git a/src/plugins/value/values/sign_value.ml b/src/plugins/value/values/sign_value.ml
index 58f961a324d..74c45a2c268 100644
--- a/src/plugins/value/values/sign_value.ml
+++ b/src/plugins/value/values/sign_value.ml
@@ -120,6 +120,7 @@ let assume_non_zero v =
let assume_bounded _ _ v = `Unknown v
let assume_not_nan ~assume_finite:_ _ v = `Unknown v
+let assume_pointer v = `Unknown v
let assume_comparable _ v1 v2 = `Unknown (v1, v2)
(** {2 Forward transfer functions} *)
diff --git a/src/plugins/value/values/value_product.ml b/src/plugins/value/values/value_product.ml
index 5b612953614..99d6ff34751 100644
--- a/src/plugins/value/values/value_product.ml
+++ b/src/plugins/value/values/value_product.ml
@@ -81,6 +81,11 @@ module Make
and right_truth = Right.assume_not_nan ~assume_finite fkind right in
narrow_truth (left, left_truth) (right, right_truth)
+ let assume_pointer (left, right) =
+ let left_truth = Left.assume_pointer left
+ and right_truth = Right.assume_pointer right in
+ narrow_truth (left, left_truth) (right, right_truth)
+
let assume_comparable op (l1, r1) (l2, r2) =
let left_truth = Left.assume_comparable op l1 l2
and right_truth = Right.assume_comparable op r1 r2 in
--
GitLab