From f72ddfad6391f1a95c14fd06a4703f7bf6e3f50e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 9 Oct 2024 14:27:09 +0200
Subject: [PATCH] [Eva] In offsetmap and lmap, removes bottom from the argument
value.
Returns `Bottom when needed, instead of using V.bottom.
---
src/kernel_services/abstract_interp/cvalue.ml | 6 ++-
.../abstract_interp/cvalue.mli | 2 +
src/kernel_services/abstract_interp/lmap.ml | 29 +++++-----
.../abstract_interp/lmap_bitwise.ml | 1 +
.../abstract_interp/lmap_sig.ml | 9 ++--
.../abstract_interp/offsetmap.ml | 54 ++++++++++---------
.../abstract_interp/offsetmap_bitwise_sig.ml | 4 +-
.../abstract_interp/offsetmap_sig.ml | 6 +--
.../eva/domains/cvalue/builtins_memory.ml | 1 +
.../eva/domains/cvalue/builtins_string.ml | 1 +
.../eva/domains/cvalue/cvalue_queries.ml | 5 +-
src/plugins/eva/legacy/eval_op.ml | 7 +--
src/plugins/eva/values/offsm_value.ml | 1 +
13 files changed, 73 insertions(+), 53 deletions(-)
diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index 31d72c55b6c..965f16257ed 100644
--- a/src/kernel_services/abstract_interp/cvalue.ml
+++ b/src/kernel_services/abstract_interp/cvalue.ml
@@ -768,6 +768,10 @@ module V_Or_Uninitialized = struct
let uninitialized = C_uninit_noesc V.bottom
let initialized v = C_init_noesc v
+ let inject_or_bottom = function
+ | `Bottom -> bottom
+ | `Value v -> v
+
let is_included t1 t2 =
(* (t2.initialized ==> t1.initialized) &&
(t2.no_escaping_adr ==> t1.no_escaping_adr) &&
@@ -1052,7 +1056,7 @@ module Model = struct
include Make_Narrow(V_Or_Uninitialized)
let find_indeterminate ?(conflate_bottom=true) state loc =
- find ~conflate_bottom state loc
+ find ~conflate_bottom state loc |> V_Or_Uninitialized.inject_or_bottom
let find ?(conflate_bottom=true) state loc =
let v = find_indeterminate ~conflate_bottom state loc in
diff --git a/src/kernel_services/abstract_interp/cvalue.mli b/src/kernel_services/abstract_interp/cvalue.mli
index c29a49c14ed..8147ae8675a 100644
--- a/src/kernel_services/abstract_interp/cvalue.mli
+++ b/src/kernel_services/abstract_interp/cvalue.mli
@@ -179,6 +179,8 @@ module V_Or_Uninitialized : sig
val get_v : t -> V.t
val make : initialized: bool -> escaping: bool -> V.t -> t
+ val inject_or_bottom: t Lattice_bounds.or_bottom -> t
+
val is_bottom: t -> bool
(** [is_initialized v = true] implies [v] is definitely initialized.
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 55a15a5e78e..ef80f24dc12 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -180,21 +180,23 @@ struct
(* may raise Error_Top in the case Top Top. Make sure to annotate callers *)
let find ?(conflate_bottom=true) mem {loc ; size} =
+ let open Bottom.Operators in
let handle_imprecise_base base acc =
- match find_or_default base mem with
- | `Bottom -> acc
- | `Value offsetmap ->
- V.join (Offsetmap.find_imprecise_everywhere offsetmap) acc
+ let v =
+ let* offsetmap = find_or_default base mem in
+ Offsetmap.find_imprecise_everywhere offsetmap
+ in
+ Bottom.join V.join v acc
in
match loc with
- | Location_Bits.Top (Base.SetLattice.Top, _) -> vtop ()
+ | Location_Bits.Top (Base.SetLattice.Top, _) -> `Value (vtop ())
| Location_Bits.Top (Base.SetLattice.Set s, _) ->
- Base.SetLattice.O.fold handle_imprecise_base s V.bottom
+ Base.SetLattice.O.fold handle_imprecise_base s `Bottom
| Location_Bits.Map loc_map -> begin
match size with
| Int_Base.Top ->
let aux base _ acc = handle_imprecise_base base acc in
- Location_Bits.M.fold aux loc_map V.bottom
+ Location_Bits.M.fold aux loc_map `Bottom
| Int_Base.Value size ->
let aux_base base offsets acc_v =
let validity = Base.validity base in
@@ -205,9 +207,9 @@ struct
Offsetmap.find
~conflate_bottom ~validity ~offsets ~size offsetmap
in
- V.join new_v acc_v
+ Bottom.join V.join new_v acc_v
in
- Location_Bits.M.fold aux_base loc_map V.bottom
+ Location_Bits.M.fold aux_base loc_map `Bottom
end
(* Internal function for join and widen, that handles efficiently the
@@ -497,8 +499,9 @@ struct
Base.SetLattice.pretty top
Origin.pretty_as_reason orig;
let validity = Base.validity_from_size size in
- let v = Offsetmap.find_imprecise ~validity from in
- add_binding ~exact:false m loc_dst v
+ match Offsetmap.find_imprecise ~validity from with
+ | `Bottom -> false, m
+ | `Value v -> add_binding ~exact:false m loc_dst v
let top_offsetmap size =
let top = vtop () in
@@ -667,8 +670,8 @@ struct
let find ?(conflate_bottom=true) m loc =
match m with
- | Bottom -> V.bottom
- | Top -> vtop ()
+ | Bottom -> `Bottom
+ | Top -> `Value (vtop ())
| Map m -> M.find ~conflate_bottom m loc
let join mm1 mm2 = match mm1, mm2 with
diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.ml b/src/kernel_services/abstract_interp/lmap_bitwise.ml
index af05661e44a..3e000177075 100644
--- a/src/kernel_services/abstract_interp/lmap_bitwise.ml
+++ b/src/kernel_services/abstract_interp/lmap_bitwise.ml
@@ -394,6 +394,7 @@ struct
else
let offsetmap = find_or_default base m in
let v = LOffset.find_iset ~validity itvs offsetmap in
+ let v = Lattice_bounds.Bottom.value ~bottom:V.bottom v in
V.join acc v
in
Zone.fold_i treat_offset loc V.bottom
diff --git a/src/kernel_services/abstract_interp/lmap_sig.ml b/src/kernel_services/abstract_interp/lmap_sig.ml
index 4198bc34a17..fca0253cebe 100644
--- a/src/kernel_services/abstract_interp/lmap_sig.ml
+++ b/src/kernel_services/abstract_interp/lmap_sig.ml
@@ -24,6 +24,7 @@
to be those of the [Offsetmap] module. *)
open Locations
+open Lattice_bounds
module type S = sig
@@ -92,12 +93,12 @@ module type S = sig
(** {2 Finding values} *)
- val find: ?conflate_bottom:bool -> t -> location -> v
+ val find: ?conflate_bottom:bool -> t -> location -> v or_bottom
(** @raise Error_Top when the location or the state are Top, and there
is no Top value in the type {!v}. *)
val copy_offsetmap :
- Location_Bits.t -> Integer.t -> t -> offsetmap Lattice_bounds.or_bottom
+ Location_Bits.t -> Integer.t -> t -> offsetmap or_bottom
(** [copy_offsetmap alarms loc size m] returns the superposition of the
ranges of [size] bits starting at [loc] within [m]. [size] must be
strictly greater than zero. Return [None] if all pointed addresses are
@@ -106,11 +107,11 @@ module type S = sig
@raise Error_Top when the location or the state are Top, and there
is no Top value in the type {!v}. *)
- val find_base : Base.t -> t -> offsetmap Lattice_bounds.or_top_bottom
+ val find_base : Base.t -> t -> offsetmap or_top_bottom
(** @raise Not_found if the varid is not present in the map. *)
val find_base_or_default :
- Base.t -> t -> offsetmap Lattice_bounds.or_top_bottom
+ Base.t -> t -> offsetmap or_top_bottom
(** Same as [find_base], but return the default values for bases
that are not currently present in the map. Prefer the use of this function
to [find_base], unless you explicitly want to see if the base is bound. *)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index a04bb8fabe7..d6ebfd61503 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Abstract_interp
+module Bottom = Lattice_bounds.Bottom
(* This module uses Bigints everywhere. Set up some notations *)
let pretty_int = Int.pretty
@@ -1368,32 +1369,33 @@ module Make
let find_imprecise_between (first_bit, last_bit) tree =
let rec aux tree_offset tree =
match tree with
- | Empty -> V.bottom
+ | Empty -> `Bottom
| Node (max, offl, subl, offr, subr, _rem, _m, v, _) ->
let abs_max = max +~ tree_offset in
let subl_value =
if first_bit <~ tree_offset then
let subl_abs_offset = tree_offset +~ offl in
aux subl_abs_offset subl
- else V.bottom
+ else `Bottom
in
let subr_value =
if last_bit >~ abs_max then
let subr_abs_offset = tree_offset +~ offr in
aux subr_abs_offset subr
- else V.bottom
+ else `Bottom
in
let current_node_value =
if last_bit <~ tree_offset || first_bit >~ abs_max
- then V.bottom
+ then `Bottom
else
if V.is_isotropic v
- then v
+ then `Value v
else
let origin = Origin.(current Misalign_read) in
- V.topify_with_origin origin v
+ `Value (V.topify_with_origin origin v)
in
- V.join subl_value (V.join subr_value current_node_value)
+ let join = Bottom.join V.join in
+ join subl_value (join subr_value current_node_value)
in
aux Integer.zero tree
@@ -1460,14 +1462,14 @@ module Make
whose period is [period]. [size] is the size of each read. [read_value] and
[read_nodes] are used to read the offsetmap (see read_itv for details).
[join] is used to merge the result of each read, starting with [acc]. *)
- let read_series_itv ~min ~max ~period ~size tree ~read_value ~read_nodes ~join acc =
+ let read_series_itv ~min ~max ~period ~size tree ~read_value ~read_nodes ~join =
let r = min %~ period in
let since_and_period = min, period in
let rec read_series start acc =
let read_ahead, v =
read_itv ~since_and_period ~start ~size tree ~read_value ~read_nodes
in
- let acc = join v acc in
+ let acc = Bottom.join join (`Value v) acc in
(* Compute the offset of the next read. By default, add the [period] to the
current [start], unless we can jump to the end of the current node. *)
let next = match read_ahead with
@@ -1488,26 +1490,27 @@ module Make
then read_series next acc
else acc
in
- read_series min acc
+ read_series min `Bottom
(* Reads [tree] at each offset of [offsets]. [size] is the size of each read.
[read_value] and [read_nodes] perform the reads; [join] merges the result
of each read, starting with [acc]. *)
- let read ~offsets ~size tree ~read_value ~read_nodes ~join acc =
+ let read ~offsets ~size tree ~read_value ~read_nodes ~join =
match offsets with
| Tr_offset.Interval (min, max, period) ->
read_series_itv
- ~min ~max ~period ~size tree ~read_value ~read_nodes ~join acc
+ ~min ~max ~period ~size tree ~read_value ~read_nodes ~join
| Tr_offset.Set s ->
List.fold_left
(fun acc start ->
let t = read_one_itv ~start ~size tree ~read_value ~read_nodes in
- join acc t)
- acc s
+ Bottom.join join acc (`Value t))
+ `Bottom s
| Tr_offset.Overlap(min, max, _origin) ->
- let v = find_imprecise_between (min, max) tree in
- read_value v size
- | Tr_offset.Invalid -> acc
+ let open Bottom.Operators in
+ let* v = find_imprecise_between (min, max) tree in
+ `Value (read_value v size)
+ | Tr_offset.Invalid -> `Bottom
(* Transforms a function reading one node into a function reading successive
nodes. The resulting function can be supplied to the [read_itv] function.
@@ -1544,7 +1547,7 @@ module Make
let read_nodes = read_successive_nodes ~read_one_node neutral in
let read_value v _size = v in
let join = V.join in
- read ~offsets ~size tree ~read_value ~read_nodes ~join V.bottom
+ read ~offsets ~size tree ~read_value ~read_nodes ~join
(* 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
@@ -1584,9 +1587,7 @@ module Make
let neutral = m_empty in
let read_nodes = read_successive_nodes ~read_one_node neutral in
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
- `Value t
+ read ~offsets ~size tree ~read_value ~read_nodes ~join
(* Keep the part of the tree strictly under (i.e. strictly on the left) of a
given offset. *)
@@ -2004,8 +2005,9 @@ module Make
let res, success = Ival.fold_int aux offsets (dst, false) in
if success then `Value res else `Bottom
with Not_less_than ->
+ let open Bottom.Operators in
(* Value to paste, since we cannot be precise *)
- let v =
+ let* v =
(* Under this size, this may be an integer. Try to be a bit precise
when doing 'find' *)
if size <=~ Integer.of_int 128 then
@@ -2141,11 +2143,11 @@ module Make
find_imprecise_between (min, max) m
| Base.Variable variable_v ->
find_imprecise_between (Int.zero, variable_v.Base.max_alloc) m
- | Base.Invalid | Base.Empty -> V.bottom
+ | Base.Invalid | Base.Empty -> `Bottom
let find_imprecise_everywhere m =
match m with
- | Empty -> V.bottom
+ | Empty -> `Bottom
| Node _ ->
let bounds = bounds_offset Int.zero m in
find_imprecise_between bounds m
@@ -2824,8 +2826,8 @@ module Make_bitwise(V: sig
let find_iset ~validity itvs m =
try
- let aux_itv i acc = V.join acc (find i m) in
- Int_Intervals.fold aux_itv itvs V.bottom
+ let aux_itv i acc = Bottom.join V.join acc (find i m) in
+ Int_Intervals.fold aux_itv itvs `Bottom
with Error_Top -> find_imprecise ~validity m
module V_Hashtbl = FCHashtbl.Make(V)
diff --git a/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml b/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml
index d736be4315f..b744b14981c 100644
--- a/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml
+++ b/src/kernel_services/abstract_interp/offsetmap_bitwise_sig.ml
@@ -60,8 +60,8 @@ module type S = sig
(** {2 Finding values} *)
- val find : Int_Intervals_sig.itv -> t -> v
- val find_iset : validity:Base.validity -> intervals -> t -> v
+ val find : Int_Intervals_sig.itv -> t -> v Lattice_bounds.or_bottom
+ val find_iset : validity:Base.validity -> intervals -> t -> v Lattice_bounds.or_bottom
(** {2 Adding values} *)
diff --git a/src/kernel_services/abstract_interp/offsetmap_sig.ml b/src/kernel_services/abstract_interp/offsetmap_sig.ml
index 3e05e3cd024..80a860a44cc 100644
--- a/src/kernel_services/abstract_interp/offsetmap_sig.ml
+++ b/src/kernel_services/abstract_interp/offsetmap_sig.ml
@@ -186,15 +186,15 @@ module type S = sig
validity:Base.validity ->
?conflate_bottom:bool ->
offsets:Ival.t -> size:Integer.t ->
- t -> v
+ t -> v Lattice_bounds.or_bottom
(** Find the value bound to a set of intervals, expressed as an ival, in the
given rangemap. *)
- val find_imprecise: validity:Base.validity-> t -> v
+ val find_imprecise: validity:Base.validity-> t -> v Lattice_bounds.or_bottom
(** [find_imprecise ~validity m] returns an imprecise join of the values bound
in [m], in the range described by [validity]. *)
- val find_imprecise_everywhere: t -> v
+ val find_imprecise_everywhere: t -> v Lattice_bounds.or_bottom
(** Returns an imprecise join of all the values bound in the offsetmap. *)
val copy_slice:
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index 0e2e94ac1ce..eb30b6d4f65 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -379,6 +379,7 @@ let memset_typ_offsm_int full_typ i =
let find size =
V_Offsetmap.find ~validity
~offsets:(Ival.inject_singleton offset) ~size full_offsm
+ |> V_Or_Uninitialized.inject_or_bottom
in
(* Update [full_offsm] between [offset] and [offset+size-1], and store
exactly [v] there *)
diff --git a/src/plugins/eva/domains/cvalue/builtins_string.ml b/src/plugins/eva/domains/cvalue/builtins_string.ml
index 3de4a2bc5f7..2bacde37446 100644
--- a/src/plugins/eva/domains/cvalue/builtins_string.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_string.ml
@@ -162,6 +162,7 @@ let search_offsetmap_range kind offsetmap validity ~min ~max ~v_size acc =
let rem = Integer.e_rem min modu in
let offsets = make_interval ~min ~max ~rem ~modu in
let cvalue = Cvalue.V_Offsetmap.find ~validity ~offsets ~size offsetmap in
+ let cvalue = Cvalue.V_Or_Uninitialized.inject_or_bottom cvalue in
(* Be careful to not use this result [t] for the reads of the next
characters, as the reduction of [acc.from] assumes that the reads at
[offset] are consecutive, which is not the case here. Thus, we always
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
index c11f27519b9..5b4dc984d32 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -110,7 +110,10 @@ module Queries = struct
match offsm with
| `Bottom -> `Bottom, Alarmset.none
| `Value offsm ->
- let value = Cvalue.V_Offsetmap.find_imprecise_everywhere offsm in
+ let open Eval.Evaluated.Operators in
+ let* value =
+ Cvalue.V_Offsetmap.find_imprecise_everywhere offsm, Alarmset.none
+ in
let alarms = indeterminate_alarms lval value in
let v = Cvalue.V_Or_Uninitialized.get_v value in
read_garbled_mix v;
diff --git a/src/plugins/eva/legacy/eval_op.ml b/src/plugins/eva/legacy/eval_op.ml
index 5b5ed54e071..2bddd8f4a99 100644
--- a/src/plugins/eva/legacy/eval_op.ml
+++ b/src/plugins/eva/legacy/eval_op.ml
@@ -194,11 +194,11 @@ let pretty_stitched_offsetmap fmt typ o =
if Cil.isScalarType typ &&
not (Cvalue.V_Offsetmap.is_single_interval o)
then
- let v = v_uninit_of_offsetmap ~typ o in
- if not (Cvalue.V_Or_Uninitialized.is_isotropic v)
- then
+ match v_uninit_of_offsetmap ~typ o with
+ | `Value v when not (Cvalue.V_Or_Uninitialized.is_isotropic v) ->
Format.fprintf fmt "@\nThis amounts to: %a"
Cvalue.V_Or_Uninitialized.pretty v
+ | _ -> ()
let pretty_offsetmap typ fmt offsm =
(* YYY: catch pointers to arrays, and print the contents of the array *)
@@ -229,6 +229,7 @@ let find_offsm_under validity ival size offsm acc =
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_Or_Uninitialized.inject_or_bottom value in
add_if_singleton value acc
in
List.fold_left find acc list
diff --git a/src/plugins/eva/values/offsm_value.ml b/src/plugins/eva/values/offsm_value.ml
index 9118e16727e..59e65996a63 100644
--- a/src/plugins/eva/values/offsm_value.ml
+++ b/src/plugins/eva/values/offsm_value.ml
@@ -63,6 +63,7 @@ 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_Or_Uninitialized.inject_or_bottom v 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] *)
--
GitLab