From c5da56df0dc16f27d31cbf0b4a2f75d627edc8e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 21 Jun 2024 16:33:13 +0200 Subject: [PATCH] Address review --- src/lib/reasoners/intervals.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/lib/reasoners/intervals.ml b/src/lib/reasoners/intervals.ml index ff362d3fb..9bb33527f 100644 --- a/src/lib/reasoners/intervals.ml +++ b/src/lib/reasoners/intervals.ml @@ -632,16 +632,22 @@ module Int = struct trace1 "lognot" u @@ map_strict_dec ZEuclideanType.lognot u let bvudiv ~size:sz u1 u2 = - (* [bvudiv] is euclidean division where division by zero is -1 *) + (* [bvudiv] is euclidean division where division by zero is -1 (as an + integer of width [sz], so 2^sz - 1) *) let mone = Z.extract Z.minus_one 0 sz in ediv ~div0:(Interval.of_bounds (Closed mone) (Closed mone)) u1 u2 let bvurem u1 u2 = + (* In the following, [x] is the implicit variable associated with [u1] and + [y] the implicit variable associated with [u2]. *) of_set_nonempty @@ map_to_set (fun i2 -> if ZEuclideanType.equal i2.ub ZEuclideanType.zero then (* [y] is always zero -> identity *) map_to_set interval_set u1 + else if ZEuclideanType.compare i2.ub ZEuclideanType.zero < 0 then + (* Safety check -- bvurem only makes sense if [u2] is nonnegative. *) + invalid_arg "bvurem" else map_to_set (fun i1 -> if ZEuclideanType.compare i1.ub i2.lb < 0 then