From d4431f8f117857115527f9e28a17ea49f15e03a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 29 Mar 2024 18:06:18 +0100 Subject: [PATCH] feat(BV, CP): Propagators for addition and multiplication MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This patch adds constraints to represent bit-vector addition and multiplication, with propagators in the interval domain and a simple propagator for multiplication that only considers the factors-of-two multiples in the bit-vector domain (this information cannot be captured by the interval domain due to imprecise handling of overflow). No propagator for addition in the bit-vector domain is provided yet, although the plan is to add a full-adder propagator to provide a limited form of *local* bit-blasting, as suggested in S. Bardin, P. Herrmann, and F. Perroud. “An Alternative to SAT-Based Approaches for Bit-Vectors”. In: TACAS. 2010. --- src/lib/reasoners/bitlist.ml | 38 ++- src/lib/reasoners/bitlist.mli | 3 + src/lib/reasoners/bitv.ml | 10 +- src/lib/reasoners/bitv_rel.ml | 307 ++++++++++++++++-- src/lib/reasoners/intervals.ml | 6 +- src/lib/reasoners/intervals_intf.ml | 4 + src/lib/structures/expr.ml | 25 +- src/lib/structures/symbols.ml | 18 +- src/lib/structures/symbols.mli | 4 +- tests/bitvec_tests.ml | 34 ++ .../dolmen/bitv/bv2nat_bvneg.dolmen.expected | 2 +- tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2 | 2 + 12 files changed, 408 insertions(+), 45 deletions(-) diff --git a/src/lib/reasoners/bitlist.ml b/src/lib/reasoners/bitlist.ml index c45535fc8..091537fdf 100644 --- a/src/lib/reasoners/bitlist.ml +++ b/src/lib/reasoners/bitlist.ml @@ -49,7 +49,7 @@ let explanation { ex; _ } = ex let exact width value ex = { width - ; bits_set = value + ; bits_set = Z.extract value 0 width ; bits_clr = Z.extract (Z.lognot value) 0 width ; ex } @@ -264,3 +264,39 @@ let fold_domain f b acc = (ofs + 1) { b with bits_set = Z.logor b.bits_set mask } acc in fold_domain_aux 0 b acc + +(* simple propagator: only compute known low bits *) +let mul a b = + let sz = width a in + assert (width b = sz); + + let ex = Ex.union (explanation a) (explanation b) in + + (* (a * 2^n) * (b * 2^m) = (a * b) * 2^(n + m) *) + let zeroes_a = Z.trailing_zeros @@ Z.lognot a.bits_clr in + let zeroes_b = Z.trailing_zeros @@ Z.lognot b.bits_clr in + if zeroes_a + zeroes_b >= sz then + exact sz Z.zero ex + else + let low_bits = + if zeroes_a + zeroes_b = 0 then empty + else exact (zeroes_a + zeroes_b) Z.zero ex + in + let a = extract a zeroes_a (zeroes_a + sz - width low_bits - 1) in + assert (width a + width low_bits = sz); + let b = extract b zeroes_b (zeroes_b + sz - width low_bits - 1) in + assert (width b + width low_bits = sz); + (* ((ah * 2^n) + al) * ((bh * 2^m) + bl) = + al * bl (mod 2^(min n m)) *) + let low_a_known = Z.trailing_zeros @@ Z.lognot @@ bits_known a in + let low_b_known = Z.trailing_zeros @@ Z.lognot @@ bits_known b in + let low_known = min low_a_known low_b_known in + let mid_bits = + if low_known = 0 then empty + else exact + low_known + Z.(extract (value a) 0 low_known * extract (value b) 0 low_known) + ex + in + concat (unknown (sz - width mid_bits - width low_bits) Ex.empty) @@ + concat mid_bits low_bits diff --git a/src/lib/reasoners/bitlist.mli b/src/lib/reasoners/bitlist.mli index 66c73aa70..cc1e753f8 100644 --- a/src/lib/reasoners/bitlist.mli +++ b/src/lib/reasoners/bitlist.mli @@ -118,6 +118,9 @@ val logor : t -> t -> t val logxor : t -> t -> t (** Bitwise xor. *) +val mul : t -> t -> t +(** Multiplication. *) + val concat : t -> t -> t (** Bit-vector concatenation. *) diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 39080aad2..cf558974b 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -347,7 +347,10 @@ module Shostak(X : ALIEN) = struct let is_mine_symb sy _ = match sy with | Sy.Bitv _ - | Op (Concat | Extract _ | BV2Nat | BVnot | BVand | BVor | BVxor) + | Op ( + Concat | Extract _ | BV2Nat + | BVnot | BVand | BVor | BVxor + | BVadd | BVsub | BVmul) -> true | _ -> false @@ -403,7 +406,10 @@ module Shostak(X : ALIEN) = struct let other ~neg t _sz ctx = let r, ctx' = match E.term_view t with - | { f = Op (BVand | BVor | BVxor); _ } -> + | { f = Op ( + BVand | BVor | BVxor + | BVadd | BVsub | BVmul + ); _ } -> X.term_embed t, [] | _ -> X.make t in diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index 0eec89e3a..d28958db7 100644 --- a/src/lib/reasoners/bitv_rel.ml +++ b/src/lib/reasoners/bitv_rel.ml @@ -75,7 +75,7 @@ let is_bv_ty = function let is_bv_r r = is_bv_ty @@ X.type_info r -module Interval_domain : Rel_utils.Domain with type t = Intervals.Int.t = struct +module Interval_domain = struct type t = Intervals.Int.t let equal = Intervals.Int.equal @@ -236,6 +236,15 @@ module Constraint : sig val bvxor : X.r -> X.r -> X.r -> t (** [bvxor x y z] is the constraint [x ^ y ^ z = 0] *) + val bvadd : X.r -> X.r -> X.r -> t + (** [bvadd r x y] is the constraint [r = x + y] *) + + val bvsub : X.r -> X.r -> X.r -> t + (** [bvsub r x y] is the constraint [r = x - y] *) + + val bvmul : X.r -> X.r -> X.r -> t + (** [bvmul r x y] is the constraint [r = x * y] *) + val bvule : X.r -> X.r -> t val bvugt : X.r -> X.r -> t @@ -251,22 +260,36 @@ end = struct type binop = (* Bitwise operations *) | Band | Bor | Bxor + (* Arithmetic operations *) + | Badd | Bmul let pp_binop ppf = function | Band -> Fmt.pf ppf "bvand" | Bor -> Fmt.pf ppf "bvor" | Bxor -> Fmt.pf ppf "bvxor" + | Badd -> Fmt.pf ppf "bvadd" + | Bmul -> Fmt.pf ppf "bvmul" let equal_binop op1 op2 = match op1, op2 with - | Band, Band | Bor, Bor | Bxor, Bxor -> true + | Band, Band -> true | Band, _ | _, Band -> false - | Bor, Bxor | Bxor, Bor -> false + + | Bor, Bor -> true + | Bor, _ | _, Bor -> false + + | Bxor, Bxor -> true + | Bxor, _ | _, Bxor -> false + + | Badd, Badd -> true + | Badd, _ | _, Badd -> false + + | Bmul, Bmul -> true let hash_binop : binop -> int = Hashtbl.hash let is_commutative = function - | Band | Bor | Bxor -> true + | Band | Bor | Bxor | Badd | Bmul -> true let propagate_binop ~ex dx op dy dz = let open Domains.Ephemeral in @@ -296,10 +319,28 @@ end = struct (* x = y ^ z <-> y = x ^ z *) update ~ex dy (Bitlist.logxor !!dx !!dz); update ~ex dz (Bitlist.logxor !!dx !!dy) + | Badd -> + (* TODO: full adder propagation *) + () - let propagate_interval_binop ~ex:_ _r _op _y _z = - (* No interval propagation for binops yet *) - () + | Bmul -> (* Only forward propagation for now *) + update ~ex dx (Bitlist.mul !!dy !!dz) + + 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 + match op with + | Badd -> + update ~ex dr @@ norm @@ Intervals.Int.add !!dx !!dy; + update ~ex dy @@ norm @@ Intervals.Int.sub !!dr !!dx; + update ~ex dx @@ norm @@ Intervals.Int.sub !!dr !!dy + + | Bmul -> (* Only forward propagation for now *) + update ~ex dr @@ norm @@ Intervals.Int.mul !!dx !!dy + + | Band | Bor | Bxor -> + (* No interval propagation for bitwise operators yet *) + () type fun_t = | Fbinop of binop * X.r * X.r @@ -339,7 +380,8 @@ end = struct let get r = Interval_domains.Ephemeral.handle dom r in match f with | Fbinop (op, x, y) -> - propagate_interval_binop ~ex (get r) op (get x) (get y) + let sz = match X.type_info r with Tbitv n -> n | _ -> assert false in + propagate_interval_binop ~ex sz (get r) op (get x) (get y) type binrel = Rule | Rugt @@ -355,20 +397,22 @@ end = struct (* No bitlist propagation for relations yet *) () - let less_than_sup ~strict iv = - let sup, ex = Intervals.Int.upper_bound iv in + let less_than_sup ~ex ~strict iv = + let sup, ex' = Intervals.Int.upper_bound iv in let sup = if strict then Intervals.map_bound Z.pred sup else sup in - Intervals.Int.of_bounds ~ex Unbounded sup + Intervals.Int.of_bounds ~ex:(Ex.union ex ex') Unbounded sup - let greater_than_inf ~strict iv = - let inf, ex = Intervals.Int.lower_bound iv in + let greater_than_inf ~ex ~strict iv = + let inf, ex' = Intervals.Int.lower_bound iv in let inf = if strict then Intervals.map_bound Z.succ inf else inf in - Intervals.Int.of_bounds ~ex inf Unbounded + Intervals.Int.of_bounds ~ex:(Ex.union ex ex') inf Unbounded let propagate_less_than ~ex ~strict dx dy = let open Interval_domains.Ephemeral in - update ~ex dx (less_than_sup ~strict !!dy); - update ~ex dy (greater_than_inf ~strict !!dx) + (* Do not use [update] to make sure that the justification is only stored on + the upper/lower bound. *) + update ~ex:Ex.empty dx (less_than_sup ~ex ~strict !!dy); + update ~ex:Ex.empty dy (greater_than_inf ~ex ~strict !!dx) let propagate_interval_binrel ~ex op dx dy = match op with @@ -491,6 +535,11 @@ end = struct let bvand = cbinop Band let bvor = cbinop Bor let bvxor = cbinop Bxor + let bvadd = cbinop Badd + let bvsub r x y = + (* r = x - y <-> x = r + y *) + bvadd x r y + let bvmul = cbinop Bmul let crel r = hcons @@ Crel r @@ -516,26 +565,226 @@ end = struct let propagate_interval ~ex c dom = propagate_interval_repr ~ex dom c.repr - let simplify_binop acts op r x y = - let acts_add_zero r = - let sz = match X.type_info r with Tbitv n -> n | _ -> assert false in - acts.Rel_utils.acts_add_eq r - (Shostak.Bitv.is_mine [ { bv = Cte Z.zero ; sz }]) - in + let bitwidth r = + match X.type_info r with Tbitv n -> n | _ -> assert false + + let const sz n = + Shostak.Bitv.is_mine [ { bv = Cte (Z.extract n 0 sz); sz } ] + + let cast ty n = + match ty with + | Ty.Tbitv sz -> const sz n + | _ -> invalid_arg "cast" + + let value x = + match Shostak.Bitv.embed x with + | [ { bv = Cte n; _ } ] -> n + | _ -> invalid_arg "const_value" + + (* Add the constraint: r = x *) + let add_eq acts r x = + acts.Rel_utils.acts_add_eq r x + + (* Add the constraint: r = c *) + let add_eq_const acts r c = + add_eq acts r @@ const (bitwidth r) c + + (* Add the constraint: r = x & c *) + let add_and_const acts r x c = + (* TODO: apply to extractions for any [c]? Could be expensive for Shostak *) + if Z.equal c Z.zero then ( + add_eq_const acts r Z.zero; + true + ) else if Z.equal c (Z.extract Z.minus_one 0 (bitwidth r)) then ( + add_eq acts r x; + true + ) else + false + + (* Add the constraint: r = x | c *) + let add_or_const acts r x c = + (* TODO: apply to extractions for any [c]? Could be expensive for Shostak *) + if Z.equal c Z.zero then ( + add_eq acts r x; + true + ) else if Z.equal c (Z.extract Z.minus_one 0 (bitwidth r)) then ( + add_eq_const acts r Z.minus_one; + true + ) else + false + + (* Add the constraint: r = x ^ c *) + let add_xor_const acts r x c = + (* TODO: apply to extractions for any [c]? Could be expensive for Shostak *) + if Z.equal c Z.zero then ( + add_eq acts r x; + true + ) else if Z.equal c (Z.extract Z.minus_one 0 (bitwidth r)) then ( + add_eq acts r + (Shostak.Bitv.is_mine @@ Bitv.lognot @@ Shostak.Bitv.embed x); + true + ) else + false + + (* Add the constraint: r = x + c *) + let add_add_const acts r x c = + let sz = bitwidth r in + if Z.equal c Z.zero then ( + add_eq acts r x; + true + ) else if X.is_constant r then ( + (* c1 = x + c2 -> x = c1 - c2 *) + add_eq_const acts x Z.(value r - c); + true + ) else if Z.testbit c (sz - 1) then + (* Due to the modular nature of arithmetic on bit-vectors, [y = x + c] + and [y = x + (2^sz - c)] are actually equivalent. + + We normalize to the version that uses a smaller constant. *) + if Z.popcount c = 1 then + (* INT_MIN (2^(sz - 1)) is special because -INT_MIN = INT_MIN and so + r = x + INT_MIN + and + x = r + INT_MIN + are actually equivalent, so we just pick a normalized order between x + and r. *) + if X.hash_cmp r x > 0 then ( + acts.acts_add_constraint (bvadd x r (const (bitwidth r) c)); + true + ) else + false + else + (* r = x - c -> x = r + c (mod 2^sz) *) + let c = Z.neg @@ Z.signed_extract c 0 sz in + assert (Z.sign c > 0 && not (Z.testbit c sz)); + acts.acts_add_constraint (bvadd x r (const sz c)); + true + else + false + + (* Add the constraint: r = x << c *) + let add_shl_const acts r x c = + let sz = bitwidth r in + match Z.to_int c with + | 0 -> add_eq acts r x + | n when n < sz -> + assert (n > 0); + let r_bitv = Shostak.Bitv.embed r in + let high_bits = + Shostak.Bitv.is_mine @@ + Bitv.extract sz 0 (sz - 1 - n) (Shostak.Bitv.embed x) + in + add_eq acts + (Shostak.Bitv.is_mine @@ Bitv.extract sz n (sz - 1) r_bitv) + high_bits; + add_eq_const acts + (Shostak.Bitv.is_mine @@ Bitv.extract sz 0 (n - 1) r_bitv) + Z.zero + | _ | exception Z.Overflow -> + add_eq_const acts r Z.zero + + (* Add the constraint: r = x * c *) + let add_mul_const acts r x c = + if Z.equal c Z.zero then ( + add_eq_const acts r Z.zero; + true + ) else if Z.popcount c = 1 then ( + let ofs = Z.numbits c - 1 in + add_shl_const acts r x (Z.of_int ofs); + true + ) else + false + + (* Ground evaluation rules for binary operators. *) + let eval_binop op ty x y = match op with + | Band -> cast ty @@ Z.logand x y + | Bor -> cast ty @@ Z.logor x y + | Bxor -> cast ty @@ Z.logxor x y + | Badd -> cast ty @@ Z.add x y + | Bmul -> cast ty @@ Z.mul x y + + (* Constant simplification rules for binary operators. + + The case where all arguments are constant and the function can be fully + evaluated is assumed to be dealt with prior to calling this function. + + Algebraic rules (e.g. x & x = x) are in [rw_binop_algebraic].*) + let rw_binop_const acts op r x y = + (* NB: for commutative operators, arguments are sorted, so the second + argument can only be constant if the first argument also is constant. *) + match op with + | Band when X.is_constant x -> + add_and_const acts r y (value x) + | Band when X.is_constant y -> + add_and_const acts r x (value y) + | Band -> false + + | Bor when X.is_constant x -> + add_or_const acts r y (value x) + | Bor when X.is_constant y -> + add_or_const acts r x (value y) + | Bor -> false + + | Bxor when X.is_constant x -> + add_xor_const acts r y (value x) + | Bxor when X.is_constant y -> + add_xor_const acts r x (value y) + | Bxor when X.is_constant r -> + add_xor_const acts x y (value r) + | Bxor -> false + + | Badd when X.is_constant x -> + add_add_const acts r y (value x) + | Badd when X.is_constant y -> + add_add_const acts r x (value y) + | Badd -> + false + + | Bmul when X.is_constant x -> + add_mul_const acts r y (value x) + | Bmul when X.is_constant y -> + add_mul_const acts r x (value y) + | Bmul -> false + + (* Algebraic rewrite rules for binary operators. + + Rules based on constant simplifications are in [rw_binop_const]. *) + let rw_binop_algebraic acts op r x y = + match op with + (* x & x = x ; x | x = x *) | Band | Bor when X.equal x y -> - acts.acts_add_eq r x; true + add_eq acts r x; true (* r ^ x ^ x = 0 <-> r = 0 *) | Bxor when X.equal x y -> - acts_add_zero r; true + add_eq_const acts r Z.zero; true | Bxor when X.equal r x -> - acts_add_zero y; true + add_eq_const acts y Z.zero; true | Bxor when X.equal r y -> - acts_add_zero x; true + add_eq_const acts x Z.zero; true + + | Badd when X.equal x y -> + (* r = x + x -> r = 2x -> r = x << 1 *) + add_shl_const acts r x Z.one; true + | Badd when X.equal r x -> + (* x = x + y -> y = 0 *) + add_eq_const acts y Z.zero; true + | Badd when X.equal r y -> + (* y = x + y -> x = 0 *) + add_eq_const acts x Z.zero; true | _ -> false + let simplify_binop acts op r x y = + if X.is_constant x && X.is_constant y then ( + add_eq acts r @@ + eval_binop op (X.type_info r) (value x) (value y); + true + ) else + rw_binop_const acts op r x y || + rw_binop_algebraic acts op r x y + let simplify_fun_t acts r = function | Fbinop (op, x, y) -> simplify_binop acts op r x y @@ -564,6 +813,9 @@ let extract_binop = | Sy.BVand -> Some bvand | BVor -> Some bvor | BVxor -> Some bvxor + | BVadd -> Some bvadd + | BVsub -> Some bvsub + | BVmul -> Some bvmul | _ -> None let extract_constraints bcs uf r t = @@ -594,7 +846,7 @@ let rec mk_eq ex lhs w z = if Options.get_debug_bitv () then Printer.print_dbg ~module_name:"Bitv_rel" ~function_name:"mk_eq" - "bitlist propagated: %a = %a" X.print lhs X.print rhs; + "bitlist propagated: %a = %a%a" X.print lhs X.print rhs Ex.print ex; (Uf.LX.mkv_eq lhs rhs , ex) :: if sz = w then [] else mk_eq ex rest (w - sz) (Z.extract z 0 (w - sz)) @@ -644,6 +896,7 @@ module Any_constraint = struct | Structural r -> 2 * X.hash r + 1 let propagate constraint_propagate structural_propagation c d = + Steps.incr CP; match c with | Constraint { value; explanation = ex } -> constraint_propagate ~ex value d diff --git a/src/lib/reasoners/intervals.ml b/src/lib/reasoners/intervals.ml index 933466109..28e92834e 100644 --- a/src/lib/reasoners/intervals.ml +++ b/src/lib/reasoners/intervals.ml @@ -86,10 +86,14 @@ module Ring(C : Core)(RT : RingType) = struct ); u + let neg u = trace1 "neg" u @@ map_strict_dec RT.neg u + let add u1 u2 = trace2 "add" u1 u2 @@ of_set_nonempty @@ map2_mon_to_set RT.add Inc u1 Inc u2 + let sub u1 u2 = add u1 (neg u2) + let scale alpha u = let alpha = RT.finite alpha in let c = RT.compare alpha RT.zero in @@ -125,8 +129,6 @@ module Ring(C : Core)(RT : RingType) = struct (map_inc_to_set (RT.pow n)) else map_strict_inc (RT.pow n) u - - let neg u = trace1 "neg" u @@ map_strict_dec RT.neg u end module Field(C : Core)(FT : FieldType) = struct diff --git a/src/lib/reasoners/intervals_intf.ml b/src/lib/reasoners/intervals_intf.ml index 0bec8ea03..9c9aba536 100644 --- a/src/lib/reasoners/intervals_intf.ml +++ b/src/lib/reasoners/intervals_intf.ml @@ -639,6 +639,10 @@ module type Ring = sig (** [add u1 u2] evaluates to {m \{ x + y \mid x \in S_1, y \in S_2 \}} when [u1] evaluates to {m S_1} and [u2] evaluates to {m S_2}. *) + val sub : t -> t -> t + (** [sub u1 u2] evaluates to {m \{ x - y \mid x \in S_1, y \in S_2 \}} when + [u1] evaluates to {m S_1} and [u2] evaluates to {m S_2}. *) + val scale : value -> t -> t (** [scale v u] evaluates to {m \{ v \times x \mid x \in S \}} when [u] evaluates to {m S}. *) diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 924ee7054..5e5c41841 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -3001,9 +3001,18 @@ end module BV = struct open Core + let of_bigint sz n = + assert (sz > 0); + mk_term (Sy.Bitv (sz, Z.extract n 0 sz)) [] (Tbitv sz) + + let of_bigint_like s n = + match type_info s with + | Tbitv sz -> of_bigint sz n + | _ -> invalid_arg "of_bigint_like" + (* Constant symbols for all zeros and all ones *) - let bvzero m = bitv (String.make m '0') (Tbitv m) - let bvones m = bitv (String.make m '1') (Tbitv m) + let bvzero m = of_bigint m Z.zero + let bvones m = of_bigint m Z.minus_one (* Helpers *) let b = function @@ -3101,12 +3110,10 @@ module BV = struct bvcomp (size2 s t) s t (* Arithmetic operations *) - let bvneg s = - let m = size s in - int2bv m Ints.(~$$Z.(~$1 lsl m) - bv2nat s) - let bvadd s t = int2bv (size s) Ints.(bv2nat s + bv2nat t) - let bvsub s t = bvadd s (bvneg t) - let bvmul s t = int2bv (size s) Ints.(bv2nat s * bv2nat t) + let bvadd s t = mk_term (Op BVadd) [s; t] (type_info s) + 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)) @@ -3146,7 +3153,7 @@ module BV = struct let abs_s = ite (is msb_s 0) s (bvneg s) in let abs_t = ite (is msb_t 0) t (bvneg t) in let u = bvurem abs_s abs_t in - ite (eq (bv2nat u) Ints.(~$0)) + ite (eq u (of_bigint_like u Z.zero)) u @@ ite (and_ (is msb_s 0) (is msb_t 0)) u diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index ebe318db3..5e8681a6f 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -43,7 +43,9 @@ type operator = (* BV *) | Concat | Extract of int * int (* lower bound * upper bound *) - | BVnot | BVand | BVor | BVxor | Int2BV of int | BV2Nat + | BVnot | BVand | BVor | BVxor + | BVadd | BVsub | BVmul + | Int2BV of int | BV2Nat (* FP *) | Float | Integer_round @@ -190,7 +192,9 @@ let compare_operators op1 op2 = | Real_of_int | Int_floor | Int_ceil | Sqrt_real_default | Sqrt_real_excess | Min_real | Min_int | Max_real | Max_int | Integer_log2 | Pow | Integer_round - | BVnot | BVand | BVor | BVxor | Int2BV _ | BV2Nat + | BVnot | BVand | BVor | BVxor + | BVadd | BVsub | BVmul + | Int2BV _ | BV2Nat | Not_theory_constant | Is_theory_constant | Linear_dependency | Constr _ | Destruct _ | Tite) -> assert false ) @@ -348,6 +352,11 @@ module AEPrinter = struct | BVor -> Fmt.pf ppf "bvor" | BVxor -> Fmt.pf ppf "bvxor" + (* BV logic *) + | BVadd -> Fmt.pf ppf "bvadd" + | BVsub -> Fmt.pf ppf "bvsub" + | BVmul -> Fmt.pf ppf "bvmul" + (* ArraysEx theory *) | Get -> Fmt.pf ppf "get" | Set -> Fmt.pf ppf "set" @@ -447,6 +456,11 @@ module SmtPrinter = struct | BVor -> Fmt.pf ppf "bvor" | BVxor -> Fmt.pf ppf "bvxor" + (* BV logic *) + | BVadd -> Fmt.pf ppf "bvadd" + | BVsub -> Fmt.pf ppf "bvsub" + | BVmul -> Fmt.pf ppf "bvmul" + (* ArraysEx theory *) | Get -> Fmt.pf ppf "select" | Set -> Fmt.pf ppf "store" diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index fe0c1f13e..8c9c894aa 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -43,7 +43,9 @@ type operator = (* BV *) | Concat | Extract of int * int (* lower bound * upper bound *) - | BVnot | BVand | BVor | BVxor | Int2BV of int | BV2Nat + | BVnot | BVand | BVor | BVxor + | BVadd | BVsub | BVmul + | Int2BV of int | BV2Nat (* FP *) | Float | Integer_round diff --git a/tests/bitvec_tests.ml b/tests/bitvec_tests.ml index e5b7c1b6d..6ce54389f 100644 --- a/tests/bitvec_tests.ml +++ b/tests/bitvec_tests.ml @@ -10,6 +10,8 @@ module IntSet : sig val map : (Z.t -> Z.t) -> t -> t + val map2 : (Z.t -> Z.t -> Z.t) -> t -> t -> t + val mem : Z.t -> t -> bool end = struct type t = Z.t @@ -51,6 +53,13 @@ end = struct let map f t = fold (fun n -> add (f n)) t empty + + let map2 f s t = + fold (fun n -> + fold (fun m -> + add (f n m) + ) t + ) s empty end let finite_bound = function @@ -229,3 +238,28 @@ let test_decrease_upper_bound sz = let () = Test.check_exn (test_decrease_upper_bound 3) + +let test_bitlist_binop ~count sz zop bop = + Test.make ~count + ~print:Print.( + pair + (Fmt.to_to_string Bitlist.pp) + (Fmt.to_to_string Bitlist.pp)) + Gen.(pair (bitlist sz) (bitlist sz)) + (fun (s, t) -> + let u = bop s t in + Bitlist.width u = Bitlist.width s && + Bitlist.width u = Bitlist.width t && + IntSet.subset + (IntSet.map2 zop (of_bitlist s) (of_bitlist t)) + (of_bitlist u)) + +let zmul sz a b = + Z.extract (Z.mul a b) 0 sz + +let test_bitlist_mul sz = + test_bitlist_binop ~count:1_000 + sz (zmul sz) Bitlist.mul + +let () = + Test.check_exn (test_bitlist_mul 3) diff --git a/tests/dolmen/bitv/bv2nat_bvneg.dolmen.expected b/tests/dolmen/bitv/bv2nat_bvneg.dolmen.expected index 6f99ff0f4..a6e005255 100644 --- a/tests/dolmen/bitv/bv2nat_bvneg.dolmen.expected +++ b/tests/dolmen/bitv/bv2nat_bvneg.dolmen.expected @@ -1,2 +1,2 @@ -unsat +unknown diff --git a/tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2 b/tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2 index 5b850ecc6..86632001a 100644 --- a/tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2 +++ b/tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2 @@ -1,5 +1,7 @@ (set-logic ALL) +; This is true, but we are not able to prove it for now due to lack of +; algebraic reasoning on bit-vectors (declare-const x (_ BitVec 64)) (assert (distinct (bv2nat (bvneg x)) (mod (+ (bv2nat (bvnot x)) 1) 18446744073709551616))) (check-sat)