From b424e89fe8e9b64c8f0415be237611c5b6d3b6dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 20 Jun 2024 10:46:02 +0200 Subject: [PATCH] feat(CP): Add bitlist propagators for add/sub This patch adds propagators on the bitlist domain for addition and subtraction. These propagators are able to compute low bits independently of high bits; in particular, we now know that the sum of two even (or two odd) numbers is even. If there is a bit pattern that prevents carry propagation (e.g. two [0]s for addition), we are also able to compute the following bits precisely. Note that we do not currently decompose addition/subtraction according to these propagators -- for instance, we do not know that `(bvadd (concat x #b0) (concat y #b0))` is `(concat (bvadd x y) #b0)`. --- src/lib/reasoners/bitlist.ml | 67 +++++++++++++++ src/lib/reasoners/bitlist.mli | 6 ++ src/lib/reasoners/bitv_rel.ml | 5 +- tests/bitv/testfile-bvadd-001.dolmen.expected | 2 + tests/bitv/testfile-bvadd-001.dolmen.smt2 | 6 ++ tests/bitv/testfile-bvadd-002.dolmen.expected | 2 + tests/bitv/testfile-bvadd-002.dolmen.smt2 | 8 ++ tests/bitv/testfile-bvsub-001.dolmen.expected | 2 + tests/bitv/testfile-bvsub-001.dolmen.smt2 | 6 ++ tests/bitv/testfile-bvsub-002.dolmen.expected | 2 + tests/bitv/testfile-bvsub-002.dolmen.smt2 | 8 ++ tests/dune.inc | 84 +++++++++++++++++++ 12 files changed, 196 insertions(+), 2 deletions(-) create mode 100644 tests/bitv/testfile-bvadd-001.dolmen.expected create mode 100644 tests/bitv/testfile-bvadd-001.dolmen.smt2 create mode 100644 tests/bitv/testfile-bvadd-002.dolmen.expected create mode 100644 tests/bitv/testfile-bvadd-002.dolmen.smt2 create mode 100644 tests/bitv/testfile-bvsub-001.dolmen.expected create mode 100644 tests/bitv/testfile-bvsub-001.dolmen.smt2 create mode 100644 tests/bitv/testfile-bvsub-002.dolmen.expected create mode 100644 tests/bitv/testfile-bvsub-002.dolmen.smt2 diff --git a/src/lib/reasoners/bitlist.ml b/src/lib/reasoners/bitlist.ml index 32e5ace37..68731a275 100644 --- a/src/lib/reasoners/bitlist.ml +++ b/src/lib/reasoners/bitlist.ml @@ -389,3 +389,70 @@ let bvlshr ~size:sz a b = extract unknown 0 sz | _ | exception Z.Overflow -> constant Z.zero (explanation b) + +let add a b = + (* A binary addition [x + y] has a carry at bit position [i] iff the addition + of the lower bits of [x] and [y] overflows, i.e. if: + + {math x \bmod 2^i + y \bmod 2^i > 2^i}. + + Consider two integers [x] and [k] with no common bits set ([x & k = 0]), + then there are no carries in [x + k = x | k = x ^ k]: we can compute the + addition bitwise, and for any bit position [i]: + + {math (x + k) \bmod 2^i = x \bmod 2^i + k \bmod 2^i} + + + In particular, for an arbitrary integer [y] and bit position [i], we have: + + {math (x + k) \bmod 2^i + y \bmod 2^i \geq x \bmod 2^i + y \bmod 2^i} + + This implies that any carry position in [x + y] is also a carry position + in [(x | k) + y]; in other words, switching bits from [0] to [1] can only + introduce new carry positions -- never remove existing ones. + + Now, let us prove that this addition function is correct. For any integers + [x] and [y] in the sets represented by bitlists [a] and [b], let us + consider a bit position [i] where [x + y] and [a.bits_set + b.bits_set] + disagree (i.e. have different values for that bit). Let us furthermore + assume that [i] is known in both [a] and [b] (i.e. it is set in both + [a.bits_unk] and [b.bits_unk]). + + Since bit [i] is known in both [a] and [b], it has the same value in [x] + and [a.bits_set] (resp. [y] and [b.bits_set]): there must be a carry in + exactly one of the two additions. Since [x] is obtained by flipping some + (unknown in [a]) bits of [a.bits_set] from [0] to [1], and [y] is obtained + by flipping some (unknown in [b]) bits of [b.bits_set] from [0] to [1], it + must be [x + y] that has a carry at position [i]. If we set all remaining + unknown bits in [x] (resp. [y]) to [1], we get [a.bits_set + a.bits_unk] + (resp. [b.bits_set + b.bits_unk]) while preserving the carry at position + [i]. + + Hence, unknown bits in [a + b] are the bits that are either unknown in + [a], unknown in [b], or differ in [a.bits_set + b.bits_set] and in + [a.bits_set + a.bits_unk + b.bits_set + b.bits_unk]. *) + let x = Z.add a.bits_set b.bits_set in + let bits_unk = + Z.(a.bits_unk lor b.bits_unk lor (x lxor (x + a.bits_unk + b.bits_unk))) + in + let bits_set = Z.(x land ~!bits_unk) in + { bits_unk ; bits_set ; ex = Ex.union a.ex b.ex } + +let sub a b = + (* Recall that [x - y] is [x + ~y + 1] and remark that: + + {math x + y + 1 = ((2x + 1) + (2y + 1)) / 2} + + From this last remark, we can apply the same reasoning for [a + b + 1] as + for [a + b], and get that the unknown bits in [a + b + 1] are either + unknown in [a], unknown in [b], or differ in [a.bits_set + b.bits_set + 1] + and in [a.bits_set + a.bits_unk + b.bits_set + b.bits_unk + 1]. + + Recalling [(~b).bits_set = ~(b.bits_set | b.bits_unk)], we get the formula + below. *) + let x = Z.sub a.bits_set b.bits_set in + let bits_unk = + Z.(a.bits_unk lor b.bits_unk lor ((x + a.bits_unk) lxor (x - b.bits_unk))) + in + let bits_set = Z.(x land ~!bits_unk) in + { bits_unk ; bits_set ; ex = Ex.union a.ex b.ex } diff --git a/src/lib/reasoners/bitlist.mli b/src/lib/reasoners/bitlist.mli index 5d7779dff..c6cf4b3d1 100644 --- a/src/lib/reasoners/bitlist.mli +++ b/src/lib/reasoners/bitlist.mli @@ -112,6 +112,12 @@ val logor : t -> t -> t val logxor : t -> t -> t (** Bit-wise xor. *) +val add : t -> t -> t +(** Addition. *) + +val sub : t -> t -> t +(** Subtraction. *) + val mul : t -> t -> t (** Multiplication. *) diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index a6b8bc01b..147f88618 100644 --- a/src/lib/reasoners/bitv_rel.ml +++ b/src/lib/reasoners/bitv_rel.ml @@ -364,8 +364,9 @@ end = struct update ~ex dy @@ norm @@ Bitlist.logxor !!dx !!dz; update ~ex dz @@ norm @@ Bitlist.logxor !!dx !!dy | Badd -> - (* TODO: full adder propagation *) - () + update ~ex dx @@ norm @@ Bitlist.add !!dy !!dz; + update ~ex dz @@ norm @@ Bitlist.sub !!dx !!dy; + update ~ex dy @@ norm @@ Bitlist.sub !!dx !!dz | Bshl -> (* Only forward propagation for now *) update ~ex dx (Bitlist.bvshl ~size:sz !!dy !!dz) diff --git a/tests/bitv/testfile-bvadd-001.dolmen.expected b/tests/bitv/testfile-bvadd-001.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bvadd-001.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bvadd-001.dolmen.smt2 b/tests/bitv/testfile-bvadd-001.dolmen.smt2 new file mode 100644 index 000000000..6a5a3b878 --- /dev/null +++ b/tests/bitv/testfile-bvadd-001.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(declare-const x (_ BitVec 1024)) +(declare-const y (_ BitVec 1024)) +; Addition of low bits is independent from high bits +(assert (distinct ((_ extract 3 0) (bvadd (concat x #b0101) (concat y #b1100))) #b0001)) +(check-sat) diff --git a/tests/bitv/testfile-bvadd-002.dolmen.expected b/tests/bitv/testfile-bvadd-002.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bvadd-002.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bvadd-002.dolmen.smt2 b/tests/bitv/testfile-bvadd-002.dolmen.smt2 new file mode 100644 index 000000000..7438211f6 --- /dev/null +++ b/tests/bitv/testfile-bvadd-002.dolmen.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(declare-const x (_ BitVec 1024)) +(declare-const y (_ BitVec 1024)) +(declare-const z (_ BitVec 1024)) +(declare-const w (_ BitVec 1024)) +; Double zero stops carries +(assert (distinct ((_ extract 1027 1025) (bvadd (concat x (concat #b0100 y)) (concat y (concat #b1100 z)))) #b000)) +(check-sat) diff --git a/tests/bitv/testfile-bvsub-001.dolmen.expected b/tests/bitv/testfile-bvsub-001.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bvsub-001.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bvsub-001.dolmen.smt2 b/tests/bitv/testfile-bvsub-001.dolmen.smt2 new file mode 100644 index 000000000..4848ce195 --- /dev/null +++ b/tests/bitv/testfile-bvsub-001.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(declare-const x (_ BitVec 1024)) +(declare-const y (_ BitVec 1024)) +; Subtraction of low bits is independent of high bits +(assert (distinct ((_ extract 3 0) (bvsub (concat x #b0101) (concat y #b0111))) #b1110)) +(check-sat) diff --git a/tests/bitv/testfile-bvsub-002.dolmen.expected b/tests/bitv/testfile-bvsub-002.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bvsub-002.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bvsub-002.dolmen.smt2 b/tests/bitv/testfile-bvsub-002.dolmen.smt2 new file mode 100644 index 000000000..a6636eae2 --- /dev/null +++ b/tests/bitv/testfile-bvsub-002.dolmen.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(declare-const x (_ BitVec 1024)) +(declare-const y (_ BitVec 1024)) +(declare-const z (_ BitVec 1024)) +(declare-const w (_ BitVec 1024)) +; Double zero stops carries +(assert (distinct ((_ extract 1027 1025) (bvsub (concat x (concat #b0101 y)) (concat y (concat #b0100 z)))) #b000)) +(check-sat) diff --git a/tests/dune.inc b/tests/dune.inc index 99478732c..638a7228e 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -121342,6 +121342,48 @@ (package alt-ergo) (action (diff testfile-bvxor-001.dolmen.expected testfile-bvxor-001.dolmen_dolmen.output))) + (rule + (target testfile-bvsub-002.dolmen_dolmen.output) + (deps (:input testfile-bvsub-002.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-bvsub-002.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bvsub-002.dolmen.expected testfile-bvsub-002.dolmen_dolmen.output))) + (rule + (target testfile-bvsub-001.dolmen_dolmen.output) + (deps (:input testfile-bvsub-001.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-bvsub-001.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bvsub-001.dolmen.expected testfile-bvsub-001.dolmen_dolmen.output))) (rule (target testfile-bvor-001.dolmen_dolmen.output) (deps (:input testfile-bvor-001.dolmen.smt2)) @@ -121426,6 +121468,48 @@ (package alt-ergo) (action (diff testfile-bvand-001.dolmen.expected testfile-bvand-001.dolmen_dolmen.output))) + (rule + (target testfile-bvadd-002.dolmen_dolmen.output) + (deps (:input testfile-bvadd-002.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-bvadd-002.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bvadd-002.dolmen.expected testfile-bvadd-002.dolmen_dolmen.output))) + (rule + (target testfile-bvadd-001.dolmen_dolmen.output) + (deps (:input testfile-bvadd-001.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-bvadd-001.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bvadd-001.dolmen.expected testfile-bvadd-001.dolmen_dolmen.output))) (rule (target testfile-bv2nat-models.dolmen_dolmen.output) (deps (:input testfile-bv2nat-models.dolmen.smt2))