Higher radix multiplier encoding

bench-multiplication/assoc.c

@@ -0,0 +1,8 @@
+#ifndef BW
+#define BW 9
+#endif
+int main() {
+  __CPROVER_bitvector[BW] a, b, c;
+  __CPROVER_bitvector[BW] ab = a * b, bc = b * c;
+  __CPROVER_assert(ab * c == a * bc, "associativity");
+}

bench-multiplication/comm.c

@@ -0,0 +1,8 @@
+#ifndef BW
+#define BW 9
+#endif
+int main() {
+  __CPROVER_bitvector[BW] a, b;
+  __CPROVER_bitvector[BW] c = a * b, d = b * a;
+  __CPROVER_assert(c == d, "commutativity");
+}

bench-multiplication/const3.c

@@ -0,0 +1,7 @@
+#ifndef BW
+#define BW 9
+#endif
+int main() {
+  __CPROVER_bitvector[BW] a;
+  __CPROVER_assert(a * 3 == a + a + a, "multiply by 3");
+}

bench-multiplication/distrib.c

@@ -0,0 +1,8 @@
+#ifndef BW
+#define BW 9
+#endif
+int main() {
+  __CPROVER_bitvector[BW] a, b, c;
+  __CPROVER_bitvector[BW] lhs = a * (b + c), rhs = a * b + a * c;
+  __CPROVER_assert(lhs == rhs, "distributivity");
+}

bench-multiplication/factor.c

@@ -0,0 +1,8 @@
+#ifndef BW
+#define BW 9
+#endif
+int main() {
+  __CPROVER_bitvector[BW] p, q;
+  __CPROVER_assume(p > 1 && q > 1);
+  __CPROVER_assert(p * q != 143, "not factorable");
+}

bench-multiplication/mul_bounds.c

@@ -0,0 +1,9 @@
+#ifndef BW
+#define BW 16
+#endif
+int main() {
+  __CPROVER_bitvector[BW/2] a, b;
+  __CPROVER_bitvector[BW] wide = (__CPROVER_bitvector[BW])a * (__CPROVER_bitvector[BW])b;
+  __CPROVER_bitvector[BW*2] wider = (__CPROVER_bitvector[BW*2])a * (__CPROVER_bitvector[BW*2])b;
+  __CPROVER_assert(wide == (__CPROVER_bitvector[BW])wider, "no overflow");
+}

bench-multiplication/mul_double.c

@@ -0,0 +1,8 @@
+#ifndef BW
+#define BW 16
+#endif
+int main() {
+  __CPROVER_bitvector[BW] a, b;
+  __CPROVER_bitvector[BW/2] a_lo = a, b_lo = b, prod_lo = a * b;
+  __CPROVER_assert(prod_lo == (__CPROVER_bitvector[BW/2])(a_lo * b_lo), "low half");
+}

bench-multiplication/mul_negation.c

@@ -0,0 +1,7 @@
+#ifndef BW
+#define BW 16
+#endif
+int main() {
+  __CPROVER_bitvector[BW] a;
+  __CPROVER_assert(a * (__CPROVER_bitvector[BW])(-1) == -a, "mul by -1");
+}

bench-multiplication/mul_overflow.c

@@ -0,0 +1,9 @@
+#ifndef BW
+#define BW 16
+#endif
+int main() {
+  __CPROVER_bitvector[BW] a, b;
+  __CPROVER_bitvector[BW*2] wide = (__CPROVER_bitvector[BW*2])a * (__CPROVER_bitvector[BW*2])b;
+  __CPROVER_bitvector[BW] narrow = a * b;
+  __CPROVER_assert(narrow == (__CPROVER_bitvector[BW])wide, "truncated matches wide");
+}

bench-multiplication/mul_shift.c

@@ -0,0 +1,8 @@
+#ifndef BW
+#define BW 16
+#endif
+int main() {
+  __CPROVER_bitvector[BW] a;
+  __CPROVER_assert(a * 4 == a << 2, "mul4 == shl2");
+  __CPROVER_assert(a * 8 == a << 3, "mul8 == shl3");
+}

bench-multiplication/mul_square_nonneg.c

@@ -0,0 +1,8 @@
+#ifndef BW
+#define BW 9
+#endif
+int main() {
+  __CPROVER_bitvector[BW] a;
+  __CPROVER_bitvector[BW*2] wide = (__CPROVER_bitvector[BW*2])a * (__CPROVER_bitvector[BW*2])a;
+  __CPROVER_assert(wide >= a, "square >= original");
+}

bench-multiplication/mul_zero_factor.c

@@ -0,0 +1,11 @@
+#ifndef BW
+#define BW 8
+#endif
+int main() {
+  __CPROVER_bitvector[BW] a, b, r;
+  r = a * b;
+  __CPROVER_assume(r == 0);
+  __CPROVER_assume(a != 0);
+  __CPROVER_assume(b != 0);
+  __CPROVER_assert(0, "found zero divisors");
+}

bench-multiplication/smt-comp/assoc_8.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(declare-fun c () (_ BitVec 8))
+(assert (not (= (bvmul (bvmul a b) c) (bvmul a (bvmul b c)))))
+(check-sat)
+(exit)

bench-multiplication/smt-comp/comm_16.smt2

@@ -0,0 +1,6 @@
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 16))
+(declare-fun b () (_ BitVec 16))
+(assert (not (= (bvmul a b) (bvmul b a))))
+(check-sat)
+(exit)

bench-multiplication/smt-comp/comm_32.smt2

@@ -0,0 +1,6 @@
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 32))
+(declare-fun b () (_ BitVec 32))
+(assert (not (= (bvmul a b) (bvmul b a))))
+(check-sat)
+(exit)

bench-multiplication/smt-comp/comm_8.smt2

@@ -0,0 +1,6 @@
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (not (= (bvmul a b) (bvmul b a))))
+(check-sat)
+(exit)

bench-multiplication/smt-comp/distrib_16.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 16))
+(declare-fun b () (_ BitVec 16))
+(declare-fun c () (_ BitVec 16))
+(assert (not (= (bvmul a (bvadd b c)) (bvadd (bvmul a b) (bvmul a c)))))
+(check-sat)
+(exit)

bench-multiplication/smt-comp/distrib_8.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(declare-fun c () (_ BitVec 8))
+(assert (not (= (bvmul a (bvadd b c)) (bvadd (bvmul a b) (bvmul a c)))))
+(check-sat)
+(exit)

bench-multiplication/smt-comp/factor_12.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_BV)
+(declare-fun p () (_ BitVec 12))
+(declare-fun q () (_ BitVec 12))
+(assert (bvugt p (_ bv1 12)))
+(assert (bvugt q (_ bv1 12)))
+(assert (= (bvmul p q) (_ bv143 12)))
+(check-sat)
+(exit)

bench-multiplication/smt-comp/factor_16.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_BV)
+(declare-fun p () (_ BitVec 16))
+(declare-fun q () (_ BitVec 16))
+(assert (bvugt p (_ bv1 16)))
+(assert (bvugt q (_ bv1 16)))
+(assert (= (bvmul p q) (_ bv10403 16)))
+(check-sat)
+(exit)

bench-multiplication/smt-comp/factor_20.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_BV)
+(declare-fun p () (_ BitVec 20))
+(declare-fun q () (_ BitVec 20))
+(assert (bvugt p (_ bv1 20)))
+(assert (bvugt q (_ bv1 20)))
+(assert (= (bvmul p q) (_ bv101101 20)))
+(check-sat)
+(exit)

bench-multiplication/smt-comp/mixed_arith_8.smt2

@@ -0,0 +1,9 @@
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(declare-fun c () (_ BitVec 8))
+(declare-fun d () (_ BitVec 8))
+(assert (not (= (bvadd (bvmul a b) (bvmul c d))
+                (bvsub (bvsub (bvmul (bvadd a c) (bvadd b d)) (bvmul a d)) (bvmul c b)))))
+(check-sat)
+(exit)

bench-multiplication/smt-comp/mul_no_overflow_16.smt2

@@ -0,0 +1,11 @@
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 16))
+(declare-fun b () (_ BitVec 16))
+(declare-fun r () (_ BitVec 16))
+(assert (= r (bvmul a b)))
+; Check: if a != 0 then r/a == b (no overflow case)
+(assert (not (= a (_ bv0 16))))
+(assert (not (= (bvudiv r a) b)))
+; This is SAT when overflow occurs
+(check-sat)
+(exit)

bench-multiplication/square.c

@@ -0,0 +1,9 @@
+#ifndef BW
+#define BW 9
+#endif
+int main() {
+  __CPROVER_bitvector[BW] a, b, s = a + b;
+  __CPROVER_bitvector[BW] lhs = s * s;
+  __CPROVER_bitvector[BW] rhs = a*a + (__CPROVER_bitvector[BW])2*a*b + b*b;
+  __CPROVER_assert(lhs == rhs, "square identity");
+}