From a7d9d161c36931defaf1cddcf2d1fee12efe9e88 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 15 Mar 2019 11:30:58 +0100
Subject: [PATCH] [Eva] Offsetmap: removes the unused alarm boolean returned by
some functions.
If needed, this boolean could be computed by the callers of these functions via
Base.is_valid_offset.
In Base, do not export offset_is_in_validity, that was only used to compute
this boolean.
---
src/kernel_services/abstract_interp/base.mli | 4 -
src/kernel_services/abstract_interp/lmap.ml | 14 ++--
.../abstract_interp/offsetmap.ml | 75 ++++++++-----------
.../abstract_interp/offsetmap_sig.mli | 19 ++---
.../abstract_interp/tr_offset.ml | 4 +-
.../abstract_interp/tr_offset.mli | 13 +---
.../value/domains/cvalue/builtins_memory.ml | 8 +-
.../value/domains/cvalue/builtins_string.ml | 2 +-
src/plugins/value/legacy/eval_op.ml | 9 +--
src/plugins/value/values/offsm_value.ml | 14 ++--
10 files changed, 63 insertions(+), 99 deletions(-)
diff --git a/src/kernel_services/abstract_interp/base.mli b/src/kernel_services/abstract_interp/base.mli
index 0c4cefd1949..ce45249b747 100644
--- a/src/kernel_services/abstract_interp/base.mli
+++ b/src/kernel_services/abstract_interp/base.mli
@@ -177,10 +177,6 @@ val max_valid_absolute_address: unit -> Int.t
val bits_sizeof : t -> Int_Base.t
-val offset_is_in_validity : Int.t -> validity -> Ival.t -> bool
-(** [is_offset_in_validity size validity ival] checks that [ival] is a valid
- offset for an access of size [size] according to [validity]. *)
-
val is_valid_offset : for_writing:bool -> Int.t -> t -> Ival.t -> bool
(** [is_valid_offset ~for_writing size b offset] checks that [offset]
(expressed in bits) plus [size] bits is valid in [b]. *)
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 28caf337006..825aa7b0b74 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -183,10 +183,7 @@ struct
Offsetmap.update_imprecise_everywhere ~validity orig v offm
| Int_Base.Value size ->
assert (Int.ge size Int.zero);
- let _, r =
- Offsetmap.update ?origin ~validity ~exact ~offsets ~size v offm
- in
- r
+ Offsetmap.update ?origin ~validity ~exact ~offsets ~size v offm
in
match offm' with
| `Bottom -> ()
@@ -230,7 +227,7 @@ struct
match find_or_default base mem with
| `Bottom -> acc_v
| `Value offsetmap ->
- let _alarm_o, new_v =
+ let new_v =
Offsetmap.find
~conflate_bottom ~validity ~offsets ~size offsetmap
in
@@ -475,7 +472,7 @@ struct
match offsetmap_dst with
| `Bottom -> acc
| `Value offsetmap_dst ->
- let _this_alarm, new_offsetmap =
+ let new_offsetmap =
Offsetmap.paste_slice ~validity ~exact
~from ~size ~offsets:i_dst offsetmap_dst
in
@@ -512,9 +509,8 @@ struct
match find_or_default k_src m with
| `Bottom -> acc
| `Value offsetmap_src ->
- let _alarm_copy, copy =
- Offsetmap.copy_slice ~validity
- ~offsets:i_src ~size offsetmap_src
+ let copy =
+ Offsetmap.copy_slice ~validity~offsets:i_src ~size offsetmap_src
in
Bottom.join Offsetmap.join acc copy
in
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 507f88fe4c8..bd89eb563c1 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -109,7 +109,6 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
type v = V.t
type widen_hint = V.generic_widen_hint
- type alarm = bool
let empty = Empty
(** All high-level functions of this module must handle a size of 0, in which
@@ -1531,7 +1530,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
(* Finds the value associated to some offsets represented as an ival. *)
let find ~validity ?(conflate_bottom=true) ~offsets ~size tree =
- let alarm, offsets = Tr_offset.trim_by_validity offsets size validity in
+ let offsets = Tr_offset.trim_by_validity offsets size validity in
let topify = Origin.K_Misalign_read in
let read_one_node ~offset node ~start ~size acc =
extract_bits_and_stitch ~topify ~conflate_bottom
@@ -1543,8 +1542,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
let read_nodes = read_successive_nodes ~read_one_node neutral in
let read_value v _size = v in
let join = V.join in
- let v = read ~offsets ~size tree ~read_value ~read_nodes ~join V.bottom in
- alarm, v
+ read ~offsets ~size tree ~read_value ~read_nodes ~join V.bottom
(* Copies the node [node] at the end of the offsetmap [acc], as part of the
larger copy of the interval [start..start+size-1] from the englobing
@@ -1575,10 +1573,10 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
t
let copy_slice ~validity ~offsets ~size tree =
- let alarm, offsets = Tr_offset.trim_by_validity offsets size validity in
- if Int.(equal size zero) then alarm, `Value Empty
+ let offsets = Tr_offset.trim_by_validity offsets size validity in
+ if Int.(equal size zero) then `Value Empty
else match offsets with
- | Tr_offset.Invalid -> alarm, `Bottom
+ | Tr_offset.Invalid -> `Bottom
| _ ->
let read_one_node = copy_one_node in
let neutral = m_empty in
@@ -1586,7 +1584,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
let read_value v size = interval_aux (pred size) Rel.zero size v in
let init = isotropic_interval size V.bottom in
let t = read ~offsets ~size tree ~read_value ~read_nodes ~join init in
- alarm, `Value t
+ `Value t
(* Keep the part of the tree strictly under (i.e. strictly on the left) of a
given offset. *)
@@ -1907,37 +1905,34 @@ let update_aux_tr_offsets ~exact ~offsets ~size v curr_off t =
the memory zones written. *)
let update_aux ?origin ~validity ~exact ~offsets ~size v curr_off t =
let v = V.anisotropic_cast ~size v in
- let alarm, reduced =
- Tr_offset.trim_by_validity ?origin offsets size validity
- in
+ let reduced = Tr_offset.trim_by_validity ?origin offsets size validity in
let exact = exact && not (Base.is_weak_validity validity) in
- let r = update_aux_tr_offsets ~exact ~offsets:reduced ~size v curr_off t in
- alarm, r
+ update_aux_tr_offsets ~exact ~offsets:reduced ~size v curr_off t
(* Same as update_aux, but on zero-rooted offsetmaps. *)
let update ?origin ~validity ~exact ~offsets ~size v t =
try
- let alarm, (_curr_off, r) =
+ let _curr_off, r =
update_aux ?origin ~validity ~exact ~offsets ~size v Int.zero t
in
- alarm, `Value r
- with Update_Result_is_bottom -> true, `Bottom
+ `Value r
+ with Update_Result_is_bottom -> `Bottom
(* High-level update function (roughly of type [Ival.t -> v -> offsetmap ->
offsetmap]) that *under*-approximate the set of written locations, when
there are too many of them. *)
let update_under ~validity ~exact ~offsets ~size v t =
let v = V.anisotropic_cast ~size v in
- let alarm, offsets = Tr_offset.trim_by_validity offsets size validity in
+ let offsets = Tr_offset.trim_by_validity offsets size validity in
if Base.is_weak_validity validity ||
update_aux_tr_offsets_approximates offsets size
then
- alarm, `Value t
+ `Value t
else
try
let _, t = update_aux_tr_offsets ~exact ~offsets ~size v Int.zero t in
- alarm, `Value t
- with Update_Result_is_bottom -> true, `Bottom
+ `Value t
+ with Update_Result_is_bottom -> `Bottom
let is_single_interval o =
match o with
@@ -2016,33 +2011,26 @@ let update_under ~validity ~exact ~offsets ~size v t =
let stop_src = Int.pred size in
ignore (Ival.cardinal_less_than offsets plevel);
(* See explanations at the end of [Tr_offset] for what is computed here.*)
- let min_valid, max_sure_valid, max_maybe_valid = match validity with
- | Base.Invalid | Base.Empty (* size > 0 *) ->
- Int.zero, Int.minus_one, Int.minus_one
- | Base.Known (b,e) ->
- b, e, e
- | Base.Unknown (b, k, e) ->
- let max_sure = Extlib.opt_conv Int.minus_one k in
- b, max_sure, e
- | Base.Variable { Base.min_alloc; Base.max_alloc } ->
- Int.zero, min_alloc, max_alloc
+ let min_valid, max_maybe_valid = match validity with
+ | Base.Invalid | Base.Empty (* size > 0 *) -> Int.zero, Int.minus_one
+ | Base.Known (b, e) | Base.Unknown (b, _, e) -> b, e
+ | Base.Variable { Base.max_alloc } -> Int.zero, max_alloc
in
- let aux start_to (acc_offsm, acc_alarm, acc_success) =
+ let aux start_to (acc_offsm, acc_success) =
let stop_to = Int.pred (Int.add start_to size) in
(* check if at least one access is possibly valid *)
if Int.lt start_to min_valid || Int.gt stop_to max_maybe_valid then
(* at least one bit cannot be written => invalid access *)
- acc_offsm, true, acc_success
+ acc_offsm, acc_success
else
let exact = exact && not (Base.is_weak_validity validity) in
- let alarm = acc_alarm || Int.gt stop_to max_sure_valid in
- paste_slice_itv ~exact src stop_src start_to acc_offsm, alarm, true
+ paste_slice_itv ~exact src stop_src start_to acc_offsm, true
in
(* TODO: this should be improved if offsets if of the form [a..b]c%d
with d >= size. In this case, the write do not overlap, and
could be done in one run in the offsetmap itself, using a zipper *)
- let res, alarm, success = Ival.fold_int aux offsets (dst, false, false) in
- if success then alarm, `Value res else true, `Bottom
+ let res, success = Ival.fold_int aux offsets (dst, false) in
+ if success then `Value res else `Bottom
with Not_less_than ->
(* Value to paste, since we cannot be precise *)
let v =
@@ -2050,11 +2038,8 @@ let update_under ~validity ~exact ~offsets ~size v t =
when doing 'find' *)
if size <=~ Integer.of_int 128 then
let validity_src = Base.validity_from_size size in
- let _, v =
- find ~validity:validity_src ~conflate_bottom:false
- ~offsets:Ival.zero ~size src
- in
- v
+ find ~validity:validity_src ~conflate_bottom:false
+ ~offsets:Ival.zero ~size src
else
(* This is a struct or an array. Either the result will be imprecise
because catenating semi-imprecise values through merge_bits
@@ -2074,7 +2059,7 @@ let update_under ~validity ~exact ~offsets ~size v t =
(** pastes [from] (of size [size]) at all [offsets] in [dst] *)
let paste_slice ~validity ~exact ~from:src ~size ~offsets dst =
- if Int.(equal size zero) then (* nothing to do *) false, `Value dst
+ if Int.(equal size zero) then (* nothing to do *) `Value dst
else
match offsets, src with
(*Special case: [from] contains a single (aligned) binding [v], and [size]
@@ -2714,7 +2699,7 @@ module Int_Intervals = struct
let max = pred (start_max +~ size) in
let curr_off, ifalse = aux_create_interval ~min ~max false in
let validity = Base.Known (min, max) in
- let _alarm, (curr_off', i) =
+ let curr_off', i =
try
Int_Intervals_Map.update_aux
~validity ~exact:true ~offsets:ival ~size true curr_off ifalse
@@ -2758,7 +2743,7 @@ module Int_Intervals = struct
(* See if using [from_ival_size] would cause an approximation *)
let max = pred (start_max +~ size) in
let validity = Base.Known (min, max) in
- let _, offsets = Tr_offset.trim_by_validity ival size validity in
+ let offsets = Tr_offset.trim_by_validity ival size validity in
if Int_Intervals_Map.update_aux_tr_offsets_approximates offsets size
then bottom (* imprecise *)
else from_ival_size_over_cached ival size (* precise *)
@@ -2836,7 +2821,7 @@ end) = struct
let add_binding_ival ~validity ~exact offsets ~size v m =
match size with
| Int_Base.Value size ->
- snd (update ~validity ~exact ~offsets ~size v m)
+ update ~validity ~exact ~offsets ~size v m
| Int_Base.Top ->
update_imprecise_everywhere ~validity Origin.top v m
diff --git a/src/kernel_services/abstract_interp/offsetmap_sig.mli b/src/kernel_services/abstract_interp/offsetmap_sig.mli
index 87ee6349e91..54f47dbbd53 100644
--- a/src/kernel_services/abstract_interp/offsetmap_sig.mli
+++ b/src/kernel_services/abstract_interp/offsetmap_sig.mli
@@ -29,7 +29,6 @@ open Abstract_interp
type v (** Type of the values stored in the offsetmap *)
type widen_hint
-type alarm = bool (** [true] indicates that an alarm may have occurred *)
include Datatype.S (** Datatype for the offsetmaps *)
@@ -182,10 +181,9 @@ val find :
validity:Base.validity ->
?conflate_bottom:bool ->
offsets:Ival.t -> size:Integer.t ->
- t -> bool * v
+ t -> v
(** Find the value bound to a set of intervals, expressed as an ival, in the
- given rangemap. The returned boolean (alarm) indicates that at least one
- of the offsets does not comply with [validity]. *)
+ given rangemap. *)
val find_imprecise: validity:Base.validity-> t -> v
(** [find_imprecise ~validity m] returns an imprecise join of the values bound
@@ -197,9 +195,9 @@ val find_imprecise_everywhere: t -> v
val copy_slice:
validity:Base.validity ->
offsets:Ival.t -> size:Integer.t ->
- t -> alarm * t Bottom.or_bottom
+ t -> t Bottom.or_bottom
(** [copy_slice ~validity ~offsets ~size m] copies and merges the slices of
- [m] starting at offsets [offsets] and of size [size]. Offsets invalid
+ [m] starting at offsets [offsets] and of size [size]. Offsets invalid
according to [validity] are removed. [size] must be strictly greater
than zero. *)
@@ -221,15 +219,14 @@ val update :
offsets:Ival.t ->
size:Int.t ->
v ->
- t -> alarm * t Bottom.or_bottom
+ t -> t Bottom.or_bottom
(** [update ?origin ~validity ~exact ~offsets ~size v m] writes [v],
of size [size], each [offsets] in [m]; [m] must be of the size implied by
[validity]. [~exact=true] results in a strong update, while
[~exact=false] performs a weak update. If [offsets] contains too many
offsets, or if [offsets] and [size] are not compatible, [offsets] and/or
[v] are over-approximated. In this case, [origin] is used as the source of
- the resulting imprecision. Returns [`Bottom] when all offsets are invalid.
- The boolean returned indicates a potential alarm. *)
+ the resulting imprecision. Returns [`Bottom] when all offsets are invalid. *)
val update_under :
validity:Base.validity ->
@@ -237,7 +234,7 @@ val update_under :
offsets:Ival.t ->
size:Int.t ->
v ->
- t -> alarm * t Bottom.or_bottom
+ t -> t Bottom.or_bottom
(** Same as {!update}, except that no over-approximation on the set
of offsets or on the value written occurs. In case of imprecision,
[m] is not updated. *)
@@ -258,7 +255,7 @@ val paste_slice:
from:t ->
size:Int.t ->
offsets:Ival.t ->
- t -> alarm * t Bottom.or_bottom
+ t -> t Bottom.or_bottom
(** {2 Shape} *)
diff --git a/src/kernel_services/abstract_interp/tr_offset.ml b/src/kernel_services/abstract_interp/tr_offset.ml
index 190317dfd3f..1dff8c7d48b 100644
--- a/src/kernel_services/abstract_interp/tr_offset.ml
+++ b/src/kernel_services/abstract_interp/tr_offset.ml
@@ -65,9 +65,7 @@ let reduce_offset_by_validity origin ival size validity =
| Base.Variable v -> reduce_for_bounds Int.zero v.Base.max_alloc
let trim_by_validity ?(origin=Origin.Unknown) ival size validity =
- let alarm = not (Base.offset_is_in_validity size validity ival) in
- let offset = reduce_offset_by_validity origin ival size validity in
- alarm, offset
+ reduce_offset_by_validity origin ival size validity
(*
Local Variables:
diff --git a/src/kernel_services/abstract_interp/tr_offset.mli b/src/kernel_services/abstract_interp/tr_offset.mli
index d59336ec349..a64e29a1612 100644
--- a/src/kernel_services/abstract_interp/tr_offset.mli
+++ b/src/kernel_services/abstract_interp/tr_offset.mli
@@ -40,16 +40,11 @@ val pretty: t Pretty_utils.formatter
(** [trim_by_validity ?origin offsets size validity] reduces [offsets] so that
all accesses to [offsets+(0..size-1)] are valid according to [validity].
For a size of 0, consider the offsets up to the validity past-one valid.
- The returned boolean indicates that at least one of the offsets does not
- comply with [validity]. If the valid offsets cannot be represented
- precisely, the [Overlap] constructor is returned. When specified,
- the [origin] argument is used as the source of this imprecision . *)
+ If the valid offsets cannot be represented precisely, the [Overlap]
+ constructor is returned. When specified, the [origin] argument is used as
+ the source of this imprecision . *)
val trim_by_validity :
- ?origin:Origin.t ->
- Ival.t ->
- Integer.t ->
- Base.validity ->
- bool (** alarm *) * t
+ ?origin:Origin.t -> Ival.t -> Integer.t -> Base.validity -> t
(** This is a more complete specification of this function, for a single offset
[o]. We want to write [size>0 bits], on a base possibly valid between
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index e413f5d9ac2..497a32936a5 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -444,8 +444,8 @@ let memset_typ_offsm_int full_typ i =
(* Read [full_offsm] between [offset] and [offset+size-1], and return
the value stored there. *)
let find size =
- snd (V_Offsetmap.find ~validity
- ~offsets:(Ival.inject_singleton offset) ~size full_offsm)
+ V_Offsetmap.find ~validity
+ ~offsets:(Ival.inject_singleton offset) ~size full_offsm
in
(* Update [full_offsm] between [offset] and [offset+size-1], and store
exactly [v] there *)
@@ -490,7 +490,7 @@ let memset_typ_offsm_int full_typ i =
if Integer.(gt nb one) then begin
(* Copy the result *)
let src = Ival.inject_singleton offset in
- let _alarm_access, copy =
+ let copy =
V_Offsetmap.copy_slice
~validity ~offsets:src ~size:sizeelt offsm'
in
@@ -505,7 +505,7 @@ let memset_typ_offsm_int full_typ i =
match copy with
| `Bottom -> assert false (* the copy is within bounds *)
| `Value copy ->
- let _alarm_access, r =
+ let r =
V_Offsetmap.paste_slice ~validity
~exact:true ~from:copy ~size:sizeelt ~offsets:dst offsm'
in
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index 343dffefba4..00a56357172 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -149,7 +149,7 @@ let read_char kind offset cvalue acc =
let rec search_each_index kind ~validity ~index ~max offsetmap acc =
let offsets = Ival.inject_singleton index in
let size = kind.size in
- let _, cvalue = Cvalue.V_Offsetmap.find ~validity ~offsets ~size offsetmap in
+ let cvalue = Cvalue.V_Offsetmap.find ~validity ~offsets ~size offsetmap in
let acc = read_char kind offsets cvalue acc in
let index = Integer.add index size in
if acc.stop || Integer.gt index max
diff --git a/src/plugins/value/legacy/eval_op.ml b/src/plugins/value/legacy/eval_op.ml
index 7e919716a71..9db5315a07a 100644
--- a/src/plugins/value/legacy/eval_op.ml
+++ b/src/plugins/value/legacy/eval_op.ml
@@ -54,10 +54,7 @@ let v_uninit_of_offsetmap ~typ offsm =
| Int_Base.Value size ->
let validity = Base.validity_from_size size in
let offsets = Ival.zero in
- let _alarm, r =
- V_Offsetmap.find ~validity ~conflate_bottom:false ~offsets ~size offsm
- in
- r
+ V_Offsetmap.find ~validity ~conflate_bottom:false ~offsets ~size offsm
let backward_comp_int_left positive comp l r =
if (Value_parameters.UndefinedPointerComparisonPropagateAll.get())
@@ -221,13 +218,13 @@ let add_if_singleton value acc =
else acc
let find_offsm_under validity ival size offsm acc =
- let _alarm, offsets = Tr_offset.trim_by_validity ival size validity in
+ let offsets = Tr_offset.trim_by_validity ival size validity in
match offsets with
| Tr_offset.Invalid | Tr_offset.Overlap _ -> acc
| Tr_offset.Set list ->
let find acc offset =
let offsets = Ival.inject_singleton offset in
- let _, value = Cvalue.V_Offsetmap.find ~validity ~offsets ~size offsm in
+ let value = Cvalue.V_Offsetmap.find ~validity ~offsets ~size offsm in
add_if_singleton value acc
in
List.fold_left find acc list
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index ad5cffc13e1..db062fd131d 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -44,8 +44,8 @@ let basic_copy ?(start=Int.zero) ~size o =
let validity = enough_validity ~start ~size in
let offsets = Ival.inject_singleton start in
match V_Offsetmap.copy_slice ~validity ~offsets ~size o with
- | _, `Bottom -> assert false
- | _, `Value r -> r
+ | `Bottom -> assert false
+ | `Value r -> r
(* paste [src] of size [size_src] starting at [start] in [r]. If [r] has size
[size_r], [size+start <= size_r] must hold. *)
@@ -56,14 +56,14 @@ let basic_paste ?(start=Int.zero) ~src ~size_src dst =
let offsets = Ival.inject_singleton start in
let from = src in
match V_Offsetmap.paste_slice ~validity ~exact ~from ~size ~offsets dst with
- | _, `Bottom -> assert false
- | _, `Value r -> r
+ | `Bottom -> assert false
+ | `Value r -> r
(* Reads [size] bits starting at [start] in [o], as a single value *)
let basic_find ?(start=Int.zero) ~size o =
let validity = enough_validity ~start ~size in
let offsets = Ival.inject_singleton start in
- let _, v = V_Offsetmap.find ~validity ~offsets ~size o in
+ let v = V_Offsetmap.find ~validity ~offsets ~size o in
V_Or_Uninitialized.map (fun v -> V.reinterpret_as_int ~signed:false ~size v) v
(* Paste [v] of size [size] at position [start] in [o] *)
@@ -72,8 +72,8 @@ let basic_add ?(start=Int.zero) ~size v o =
let offsets = Ival.inject_singleton start in
let v = V_Or_Uninitialized.initialized v in
match V_Offsetmap.update ~validity ~exact:true ~offsets ~size v o with
- | _, `Value m -> m
- | _ -> assert false
+ | `Value m -> m
+ | `Bottom -> assert false
let inject ~size v =
V_Offsetmap.create ~size ~size_v:size (V_Or_Uninitialized.initialized v)
--
GitLab