From 41f129a2a66fc09c1e0b7bb8056231aa6310a565 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 9 Oct 2024 10:55:16 +0200
Subject: [PATCH] [Eva] In offsetmaps, rewrites some functions to share more
code.
Uses [fold_between] and [Base.range_validity]; removes [clip_by_validity].
---
.../abstract_interp/offsetmap.ml | 94 ++++++++-----------
1 file changed, 40 insertions(+), 54 deletions(-)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 2c3099a0fe..a04bb8fabe 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -510,11 +510,11 @@ module Make
/ \ iter f t = f n1; fn0; f n2;
n1 n2
*)
- let fold_offset f o t acc =
+ let fold_offset f ~offset t acc =
if t = Empty then
acc
else
- let o, n, z = leftmost_child o End t in
+ let o, n, z = leftmost_child offset End t in
let rec aux_fold o t z pre =
match t with
| Empty -> pre
@@ -528,7 +528,7 @@ module Make
aux_fold o n z acc
;;
- let fold f t = fold_offset f Integer.zero t
+ let fold = fold_offset ~offset:Integer.zero
;;
let iter_offset f o t =
@@ -1722,47 +1722,6 @@ module Make
let update_itv = update_itv_with_rem ~rem:Rel.zero ~once:false
- (* This should be in Int_Intervals, but is currently needed here.
- Returns an interval with reversed bounds when the intersection is empty. *)
- let clip_by_validity = function
- | Base.Empty | Base.Invalid ->
- (fun _-> Int.one, Int.zero (* reversed interval -> no intersection*))
- | Base.Known (min, max)
- | Base.Unknown (min, _, max) ->
- (fun (min', max') -> Integer.max min min', Integer.min max max')
- | Base.Variable variable_v ->
- (fun (min', max') -> Integer.max Int.zero min',
- Integer.min variable_v.Base.max_alloc max')
-
- (** This function does a weak update of the entire [offsm], by adding the
- topification of [v]. The parameter [validity] is respected, and so is the
- current size of [offsm]: each interval already present in [offsm] and valid
- is overwritten. Interval already present but not valid are bound to
- [V.bottom].
- This function used to write bottom on non-valid locations, but this was
- unnecessary as values on non-valid locations should never be accessed
- anyway. *)
- (* TODO: this function should also be written as a call to fold_between *)
- let update_imprecise_everywhere ~validity o v offsm =
- let v = V.topify_with_origin o v in
- if Base.Validity.equal validity Base.Invalid then
- `Bottom
- else
- let clip = clip_by_validity validity in
- let r = fold
- (fun itv (bound_v, _, _) acc ->
- let new_v = V.topify_with_origin o (V.join bound_v v) in
- let new_min, new_max = clip itv in
- if new_min <=~ new_max then (* [min..max] and validity intersect *)
- append_basic_itv ~min:new_min ~max:new_max ~v:new_v acc
- else
- acc
- ) offsm m_empty
- in
- `Value r
- ;;
-
-
(** Update a set of intervals in a given rangemap all offsets starting from
mn ending in mx must be updated with value v, every period *)
let update_itvs ~exact ~mn ~mx ~period ~size v curr_off tree =
@@ -1961,7 +1920,7 @@ module Make
| Node(_, _, Empty, _, Empty, _, _, v', _) -> V.equal v v'
| _ -> false
- let fold_between ?(direction=`LTR) ~entire (imin, imax) f t acc =
+ let fold_between_offset ?(direction=`LTR) ~entire (imin, imax) f ~offset t acc =
let rec aux curr_off t acc = match t with
| Empty -> acc
| Node (max, offl, subl, offr, subr, rem, modu, v, _) ->
@@ -1998,8 +1957,10 @@ module Make
| `LTR -> acc_right (acc_middle (acc_left acc))
| `RTL -> acc_left (acc_middle (acc_right acc))
in
- aux Integer.zero t acc
- ;;
+ aux offset t acc
+
+ let fold_between = fold_between_offset ~offset:Integer.zero
+
(* weak validity should be handled caller *)
let paste_slice_itv ~exact from stop start_dest to_ =
@@ -2189,6 +2150,26 @@ module Make
let bounds = bounds_offset Int.zero m in
find_imprecise_between bounds m
+ (** This function does a weak update of the entire [offsm], by adding the
+ topification of [v]. The parameter [validity] is respected, and so is the
+ current size of [offsm]: each interval already present in [offsm] and valid
+ is overwritten. Interval already present but not valid are bound to
+ [V.bottom].
+ This function used to write bottom on non-valid locations, but this was
+ unnecessary as values on non-valid locations should never be accessed
+ anyway. *)
+ let update_imprecise_everywhere ~validity o v offsm =
+ match Base.valid_range validity with
+ | Invalid_range -> `Bottom
+ | Valid_range None -> `Value offsm
+ | Valid_range (Some itv) ->
+ let v = V.topify_with_origin o v in
+ let topify (min, max) (bound_v, _, _) acc =
+ let new_v = V.topify_with_origin o (V.join bound_v v) in
+ append_basic_itv ~min ~max ~v:new_v acc
+ in
+ `Value (fold_between ~entire:false itv topify offsm m_empty)
+
let clear_caches () = List.iter (fun f -> f ()) !clear_caches_ref
end
@@ -2624,7 +2605,7 @@ module Int_Intervals = struct
let co, i = Int_Intervals_Map.diff (co1, i1) coi2' in
normalize_itv co i
- let fold f m acc =
+ let generic_fold ~fold_offset f m acc =
match m with
| Bottom -> acc
| Top -> raise Error_Top
@@ -2632,7 +2613,14 @@ module Int_Intervals = struct
let aux_itv itv (v, _, _) acc =
if v then f itv acc else acc
in
- Int_Intervals_Map.fold_offset aux_itv curr_off i acc
+ fold_offset aux_itv ~offset:curr_off i acc
+
+ let fold f m acc =
+ generic_fold ~fold_offset:Int_Intervals_Map.fold_offset f m acc
+
+ let fold_between ~entire itv f m acc =
+ let fold_offset = Int_Intervals_Map.fold_between_offset ~entire itv in
+ generic_fold ~fold_offset f m acc
(* Could be slightly improved *)
let inject l =
@@ -2810,16 +2798,14 @@ module Make_bitwise(V: sig
try
match Base.valid_range validity with
| Base.Invalid_range -> `Bottom
- | Base.Valid_range None -> (* empty validity *) `Value m
- | Base.Valid_range (Some _) ->
- let clip = clip_by_validity validity in
+ | Base.Valid_range None -> `Value m (* empty validity *)
+ | Base.Valid_range (Some itv) ->
let aux_itv itv m =
- let itv = clip itv in
if Int.le (fst itv) (snd itv) then
add ~exact itv (v_size_mod v) m
else m
in
- `Value (Int_Intervals.fold aux_itv itvs m)
+ `Value (Int_Intervals.fold_between ~entire:false itv aux_itv itvs m)
with Error_Top ->
update_imprecise_everywhere ~validity Origin.(current Misalign_write) v m
--
GitLab