From 84cae8a80b23f4532572599e62588cc7e9d75fe7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 29 Mar 2024 16:34:04 +0100 Subject: [PATCH] feat(BV, CP): Add propagators for bvudiv and bvurem These are interval propagators only and respect the SMT-LIB semantics for division by 0. This requires custom operators in the `Intervals` module that update the bounds appropriately, sincethe existing `div` operator is undefined on `0`. --- src/lib/reasoners/bitv.ml | 4 +-- src/lib/reasoners/bitv_rel.ml | 44 ++++++++++++++++++++++++++++++++- src/lib/reasoners/intervals.ml | 30 ++++++++++++++++++++++ src/lib/reasoners/intervals.mli | 14 +++++++++++ src/lib/structures/expr.ml | 12 ++------- src/lib/structures/symbols.ml | 8 ++++-- src/lib/structures/symbols.mli | 2 +- tests/bitvec_tests.ml | 38 ++++++++++++++++++++++++++++ 8 files changed, 136 insertions(+), 16 deletions(-) diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index b28ef6d165..0ffa395ac0 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -353,7 +353,7 @@ module Shostak(X : ALIEN) = struct | Op ( Concat | Extract _ | BV2Nat | BVnot | BVand | BVor | BVxor - | BVadd | BVsub | BVmul) + | BVadd | BVsub | BVmul | BVudiv | BVurem) -> true | _ -> false @@ -411,7 +411,7 @@ module Shostak(X : ALIEN) = struct match E.term_view t with | { f = Op ( BVand | BVor | BVxor - | BVadd | BVsub | BVmul + | BVadd | BVsub | BVmul | BVudiv | BVurem ); _ } -> X.term_embed t, [] | _ -> X.make t diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index b220fcbd7a..beaa80f3e8 100644 --- a/src/lib/reasoners/bitv_rel.ml +++ b/src/lib/reasoners/bitv_rel.ml @@ -243,6 +243,17 @@ module Constraint : sig val bvmul : X.r -> X.r -> X.r -> t (** [bvmul r x y] is the constraint [r = x * y] *) + val bvudiv : X.r -> X.r -> X.r -> t + (** [bvudir r x y] is the constraint [r = x / y] + + This uses the convention that [x / 0] is [-1]. *) + + val bvurem : X.r -> X.r -> X.r -> t + (** [bvurem r x y] is the constraint [r = x % y], where [x % y] is the + remainder of euclidean division. + + This uses the convention that [x % 0] is [x]. *) + val bvule : X.r -> X.r -> t val bvugt : X.r -> X.r -> t @@ -259,7 +270,7 @@ end = struct (* Bitwise operations *) | Band | Bor | Bxor (* Arithmetic operations *) - | Badd | Bmul + | Badd | Bmul | Budiv | Burem let pp_binop ppf = function | Band -> Fmt.pf ppf "bvand" @@ -267,6 +278,8 @@ end = struct | Bxor -> Fmt.pf ppf "bvxor" | Badd -> Fmt.pf ppf "bvadd" | Bmul -> Fmt.pf ppf "bvmul" + | Budiv -> Fmt.pf ppf "bvudiv" + | Burem -> Fmt.pf ppf "bvurem" let equal_binop : binop -> binop -> bool = Stdlib.(=) @@ -274,6 +287,7 @@ end = struct let is_commutative = function | Band | Bor | Bxor | Badd | Bmul -> true + | Budiv | Burem -> false let propagate_binop ~ex dx op dy dz = let open Domains.Ephemeral in @@ -310,6 +324,12 @@ end = struct | Bmul -> (* Only forward propagation for now *) update ~ex dx (Bitlist.mul !!dy !!dz) + | Budiv -> (* No bitlist propagation for now *) + () + + | Burem -> (* No bitlist propagation for now *) + () + let propagate_interval_binop ~ex sz dr op dx dy = let open Interval_domains.Ephemeral in let norm i = Intervals.Int.extract i ~ofs:0 ~len:sz in @@ -322,6 +342,12 @@ end = struct | Bmul -> (* Only forward propagation for now *) update ~ex dr @@ norm @@ Intervals.Int.mul !!dx !!dy + | Budiv -> (* Only forward propagation for now *) + update ~ex dr @@ Intervals.Int.bvudiv ~size:sz !!dx !!dy + + | Burem -> (* Only forward propagation for now *) + update ~ex dr @@ Intervals.Int.bvurem !!dx !!dy + | Band | Bor | Bxor -> (* No interval propagation for bitwise operators yet *) () @@ -524,6 +550,8 @@ end = struct (* r = x - y <-> x = r + y *) bvadd x r y let bvmul = cbinop Bmul + let bvudiv = cbinop Budiv + let bvurem = cbinop Burem let crel r = hcons @@ Crel r @@ -687,6 +715,16 @@ end = struct | Bxor -> cast ty @@ Z.logxor x y | Badd -> cast ty @@ Z.add x y | Bmul -> cast ty @@ Z.mul x y + | Budiv -> + if Z.equal y Z.zero then + cast ty Z.minus_one + else + cast ty @@ Z.div x y + | Burem -> + if Z.equal y Z.zero then + cast ty x + else + cast ty @@ Z.rem x y (* Constant simplification rules for binary operators. @@ -731,6 +769,8 @@ end = struct add_mul_const acts r x (value y) | Bmul -> false + | Budiv | Burem -> false + (* Algebraic rewrite rules for binary operators. Rules based on constant simplifications are in [rw_binop_const]. *) @@ -800,6 +840,8 @@ let extract_binop = | BVadd -> Some bvadd | BVsub -> Some bvsub | BVmul -> Some bvmul + | BVudiv -> Some bvudiv + | BVurem -> Some bvurem | _ -> None let extract_constraints bcs uf r t = diff --git a/src/lib/reasoners/intervals.ml b/src/lib/reasoners/intervals.ml index acbc866efe..573c62d004 100644 --- a/src/lib/reasoners/intervals.ml +++ b/src/lib/reasoners/intervals.ml @@ -633,6 +633,36 @@ module Int = struct let lognot u = 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 *) + 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 = + 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 + map_to_set (fun i1 -> + if ZEuclideanType.compare i1.ub i2.lb < 0 then + (* x < y : bvurem is the identity *) + interval_set i1 + else if ( + ZEuclideanType.equal i2.lb ZEuclideanType.zero || + ZEuclideanType.compare i1.ub i2.ub < 0 + ) then + (* The range [0, i1.ub] is always valid; it is also the best we can + do if [y] can be either [0] or bigger than [x]. *) + interval_set @@ { i1 with lb = ZEuclideanType.zero } + else + (* y is non-zero and smaller than x; use [0, i2.ub[ *) + interval_set @@ + { lb = ZEuclideanType.zero ; ub = ZEuclideanType.pred i2.ub } + ) u1 + ) u2 end module Legacy = struct diff --git a/src/lib/reasoners/intervals.mli b/src/lib/reasoners/intervals.mli index d22c96a23a..65d7fa3250 100644 --- a/src/lib/reasoners/intervals.mli +++ b/src/lib/reasoners/intervals.mli @@ -74,6 +74,20 @@ module Int : sig {b Note}: The interval [s] must be an integer interval, but is allowed to be unbounded (in which case [extract s i j] returns the full interval [[0, 2^(j - i + 1) - 1]]). *) + + val bvudiv : size:int -> t -> t -> t + (** [bvudiv sz s t] computes an overapproximation of integer division for + bit-vectors of width [sz] as defined in the FixedSizeBitVectors SMT-LIB + theory, i.e. where [bvudiv n 0] is [2^sz - 1]. + + [s] and [t] must be within the [0, 2^sz - 1] range. *) + + val bvurem : t -> t -> t + (** [bvurem sz s t] computes an overapproximation of integer remainder for + bit-vectors of width [sz] as defined in the FixedSizeBitVectors SMT-LIB + theory, i.e. where [bvurem n 0] is [n]. + + [s] and [t] must be within the [0, 2^sz - 1] range. *) end module Legacy : sig diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index eca4c0ebd1..26885ad325 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -3060,16 +3060,8 @@ module BV = struct let bvsub s t = mk_term (Op BVsub) [s; t] (type_info s) let bvneg s = bvsub (of_bigint_like s Z.zero) s let bvmul s t = mk_term (Op BVmul) [s; t] (type_info s) - let bvudiv s t = - let m = size2 s t in - ite (eq (bv2nat t) Ints.(~$0)) - (bvones m) - (int2bv m Ints.(bv2nat s / bv2nat t)) - let bvurem s t = - let m = size2 s t in - ite (eq (bv2nat t) Ints.(~$0)) - s - (int2bv m Ints.(bv2nat s mod bv2nat t)) + let bvudiv s t = mk_term (Op BVudiv) [s; t] (type_info s) + let bvurem s t = mk_term (Op BVurem) [s; t] (type_info s) let bvsdiv s t = let m = size2 s t in let msb_s = extract (m - 1) (m - 1) s in diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 4560e5d2e9..8cec9761d6 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -47,7 +47,7 @@ type operator = | Concat | Extract of int * int (* lower bound * upper bound *) | BVnot | BVand | BVor | BVxor - | BVadd | BVsub | BVmul + | BVadd | BVsub | BVmul | BVudiv | BVurem | Int2BV of int | BV2Nat (* FP *) | Float @@ -198,7 +198,7 @@ let compare_operators op1 op2 = | Sqrt_real_excess | Min_real | Min_int | Max_real | Max_int | Integer_log2 | Pow | Integer_round | BVnot | BVand | BVor | BVxor - | BVadd | BVsub | BVmul + | BVadd | BVsub | BVmul | BVudiv | BVurem | Int2BV _ | BV2Nat | Not_theory_constant | Is_theory_constant | Linear_dependency | Constr _ | Destruct _ | Tite) -> assert false @@ -361,6 +361,8 @@ module AEPrinter = struct | BVadd -> Fmt.pf ppf "bvadd" | BVsub -> Fmt.pf ppf "bvsub" | BVmul -> Fmt.pf ppf "bvmul" + | BVudiv -> Fmt.pf ppf "bvudiv" + | BVurem -> Fmt.pf ppf "bvurem" (* ArraysEx theory *) | Get -> Fmt.pf ppf "get" @@ -465,6 +467,8 @@ module SmtPrinter = struct | BVadd -> Fmt.pf ppf "bvadd" | BVsub -> Fmt.pf ppf "bvsub" | BVmul -> Fmt.pf ppf "bvmul" + | BVudiv -> Fmt.pf ppf "bvudiv" + | BVurem -> Fmt.pf ppf "bvurem" (* ArraysEx theory *) | Get -> Fmt.pf ppf "select" diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index 20a7305e8f..2a533d24ec 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -47,7 +47,7 @@ type operator = | Concat | Extract of int * int (* lower bound * upper bound *) | BVnot | BVand | BVor | BVxor - | BVadd | BVsub | BVmul + | BVadd | BVsub | BVmul | BVudiv | BVurem | Int2BV of int | BV2Nat (* FP *) | Float diff --git a/tests/bitvec_tests.ml b/tests/bitvec_tests.ml index c0ae96fd24..013f6ac184 100644 --- a/tests/bitvec_tests.ml +++ b/tests/bitvec_tests.ml @@ -254,6 +254,18 @@ let test_bitlist_binop ~count sz zop bop = (IntSet.map2 zop (of_bitlist s) (of_bitlist t)) (of_bitlist u)) +let test_interval_binop ~count sz zop iop = + Test.make ~count + ~print:Print.( + pair + (Fmt.to_to_string Intervals.Int.pp) + (Fmt.to_to_string Intervals.Int.pp)) + Gen.(pair (intervals sz) (intervals sz)) + (fun (s, t) -> + IntSet.subset + (IntSet.map2 zop (of_interval s) (of_interval t)) + (of_interval (iop s t))) + let zmul sz a b = Z.extract (Z.mul a b) 0 sz @@ -263,3 +275,29 @@ let test_bitlist_mul sz = let () = Test.check_exn (test_bitlist_mul 3) + +let zudiv sz a b = + if Z.equal b Z.zero then + Z.extract Z.minus_one 0 sz + else + Z.div a b + +let test_interval_bvudiv sz = + test_interval_binop ~count:1_000 + sz (zudiv sz) (Intervals.Int.bvudiv ~size:sz) + +let () = + Test.check_exn (test_interval_bvudiv 3) + +let zurem a b = + if Z.equal b Z.zero then + a + else + Z.rem a b + +let test_interval_bvurem sz = + test_interval_binop ~count:1_000 + sz zurem Intervals.Int.bvurem + +let () = + Test.check_exn (test_interval_bvurem 3)