diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml index 6e661036c0cc91facfb7fc2c1d62a1e384b8146e..8fb7cf1b226f052663ef9f58979897e86792d1da 100644 --- a/src/kernel_services/abstract_interp/int_val.ml +++ b/src/kernel_services/abstract_interp/int_val.ml @@ -613,18 +613,6 @@ let extract_bits ~start ~stop = function Lattice_messages.emit_imprecision emitter "Ival.extract_bits"; top -let overlaps ~partial ~size t1 t2 = - let diff = add t1 (neg t2) in - match diff with - | Set array -> - not (Int_set.for_all - (fun i -> Int.ge (Int.abs i) size || (partial && Int.is_zero i)) - array) - | Itv i -> - let min, max = Int_interval.min_and_max i in - let pred_size = Int.pred size in - min_le_elt min pred_size && max_ge_elt max (Int.neg pred_size) - let make = check_make (* ------------------------------------------------------------------------ *) diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli index 86b7f208542a3b944d820a41f48a214d18ddba55..807fab7bfdd27d49926ef5c030bf4f1a14f88af3 100644 --- a/src/kernel_services/abstract_interp/int_val.mli +++ b/src/kernel_services/abstract_interp/int_val.mli @@ -181,8 +181,6 @@ val create_all_values: signed:bool -> size:int -> t representable in [size] bits. *) val all_values: size:Integer.t -> t -> bool -val overlaps: partial:bool -> size:Integer.t -> t -> t -> bool - val complement_under: size:int -> signed:bool -> t -> t or_bottom (** Returns an under-approximation of the integers of the given size and signedness that are *not* represented by the given value. *) diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml index ef21fe8eec6802213945ee09f9302148da42031d..2384610cb9f8af4512699f51a1cbc2421bf6f758 100644 --- a/src/kernel_services/abstract_interp/ival.ml +++ b/src/kernel_services/abstract_interp/ival.ml @@ -1056,11 +1056,6 @@ let reinterpret_as_float kind i = (* currently always imprecise *) top_float -let overlaps ~partial ~size t1 t2 = - match t1, t2 with - | Int i1, Int i2 -> Int_val.overlaps ~partial ~size i1 i2 - | _, _ -> assert false - let bitwise_int f_int v1 v2 = match v1, v2 with diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli index 82740fff771c53814b332b5658c12f92214bba01..4323fd006c445e69ab7770f5aa2699219d473dfe 100644 --- a/src/kernel_services/abstract_interp/ival.mli +++ b/src/kernel_services/abstract_interp/ival.mli @@ -49,7 +49,6 @@ include Lattice_type.Full_AI_Lattice_with_cardinality and type widen_hint = size_widen_hint * numerical_widen_hint val is_bottom : t -> bool -val overlaps: partial:bool -> size:Integer.t -> t -> t -> bool val is_float: t -> bool val is_int: t -> bool diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml index 448510a0aded1aefe4b5a26b2e7f98a336c5cd8b..d330023067eb7aa336fad8020cabdb397368f45c 100644 --- a/src/kernel_services/abstract_interp/locations.ml +++ b/src/kernel_services/abstract_interp/locations.ml @@ -377,11 +377,20 @@ module Location_Bytes = struct match mm1, mm2 with | Top _, _ | _, Top _ -> intersects mm1 mm2 | Map m1, Map m2 -> + (* The two locations may overlap if there are two offsets i1 and i2 such + that |i1-i2| < size (and |i1-i2| > 0 when partial is true). *) + let pred_size = Int.pred size in + let min = if partial then Int.one else Int.zero in + let size_itv = Ival.inject_range (Some min) (Some pred_size) in + let decide_both _ x y = + let abs_diff = Ival.abs_int (Ival.sub_int x y) in + Ival.intersects abs_diff size_itv + in M.symmetric_binary_predicate Hptmap_sig.NoCache M.ExistentialPredicate ~decide_fast:(fun _ _ -> M.PUnknown) ~decide_one:(fun _ _ -> false) - ~decide_both:(fun _ x y -> Ival.overlaps ~partial ~size x y) + ~decide_both m1 m2 type size_widen_hint = Ival.size_widen_hint