From ab688488e3b699f8fe6b6320a44dc0a875e6a6a8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 6 Mar 2018 17:55:34 +0000 Subject: [PATCH] tests for smt2_solver --- regression/Makefile | 1 + regression/smt2_solver/Makefile | 18 ++++++ .../smt2_solver/basic-bv1/basic-bv1.smt2 | 64 +++++++++++++++++++ regression/smt2_solver/basic-bv1/test.desc | 7 ++ .../let-with-bv1/let-with-bv1.smt2 | 32 ++++++++++ regression/smt2_solver/let-with-bv1/test.desc | 7 ++ regression/smt2_solver/let1/let1.smt2 | 30 +++++++++ regression/smt2_solver/let1/test.desc | 7 ++ 8 files changed, 166 insertions(+) create mode 100644 regression/smt2_solver/Makefile create mode 100644 regression/smt2_solver/basic-bv1/basic-bv1.smt2 create mode 100644 regression/smt2_solver/basic-bv1/test.desc create mode 100644 regression/smt2_solver/let-with-bv1/let-with-bv1.smt2 create mode 100644 regression/smt2_solver/let-with-bv1/test.desc create mode 100644 regression/smt2_solver/let1/let1.smt2 create mode 100644 regression/smt2_solver/let1/test.desc diff --git a/regression/Makefile b/regression/Makefile index c5f7c41764..eefb1f9e04 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -11,6 +11,7 @@ DIRS = cbmc \ strings-smoke-tests \ cbmc-cover \ goto-instrument-typedef \ + smt2_solver \ strings \ invariants \ goto-diff \ diff --git a/regression/smt2_solver/Makefile b/regression/smt2_solver/Makefile new file mode 100644 index 0000000000..3be14ea765 --- /dev/null +++ b/regression/smt2_solver/Makefile @@ -0,0 +1,18 @@ +default: tests.log + +test: + @../test.pl -p -c ../../../src/solvers/smt2_solver + +tests.log: ../test.pl + @../test.pl -p -c ../../../src/solvers/smt2_solver + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + $(RM) tests.log diff --git a/regression/smt2_solver/basic-bv1/basic-bv1.smt2 b/regression/smt2_solver/basic-bv1/basic-bv1.smt2 new file mode 100644 index 0000000000..13c3a739dc --- /dev/null +++ b/regression/smt2_solver/basic-bv1/basic-bv1.smt2 @@ -0,0 +1,64 @@ +(set-logic QF_BV) + +; From https://rise4fun.com/z3/tutorialcontent/guide + +; Basic Bitvector Arithmetic +(define-fun b01 () Bool (= (bvadd #x07 #x03) #x0a)) ; addition +(define-fun b02 () Bool (= (bvsub #x07 #x03) #x04)) ; subtraction +(define-fun b03 () Bool (= (bvneg #x07) #xf9)) ; unary minus +(define-fun b04 () Bool (= (bvmul #x07 #x03) #x15)) ; multiplication +(define-fun b05 () Bool (= (bvurem #x07 #x03) #x01)) ; unsigned remainder +(define-fun b06 () Bool (= (bvsrem #x07 #x03) #x01)) ; signed remainder +(define-fun b07 () Bool (= (bvsmod #x07 #x03) #x01)) ; signed modulo +(define-fun b08 () Bool (= (bvshl #x07 #x03) #x38)) ; shift left +(define-fun b09 () Bool (= (bvlshr #xf0 #x03) #x1e)) ; unsigned (logical) shift right +(define-fun b10 () Bool (= (bvashr #xf0 #x03) #xfe)) ; signed (arithmetical) shift right#x0a + +; Bitwise Operations + +(define-fun w1 () Bool (= (bvor #x6 #x3) #x7)) ; bitwise or +(define-fun w2 () Bool (= (bvand #x6 #x3) #x2)) ; bitwise and +(define-fun w3 () Bool (= (bvnot #x6) #x9)) ; bitwise not +(define-fun w4 () Bool (= (bvnand #x6 #x3) #xd)) ; bitwise nand +(define-fun w5 () Bool (= (bvnor #x6 #x3) #x8)) ; bitwise nor +(define-fun w6 () Bool (= (bvxnor #x6 #x3) #xa)) ; bitwise xnor + +; We can prove a bitwise version of deMorgan's law + +(declare-const x (_ BitVec 64)) +(declare-const y (_ BitVec 64)) +(define-fun d01 () Bool (= (bvand (bvnot x) (bvnot y)) (bvnot (bvor x y)))) + +; There is a fast way to check that fixed size numbers are powers of two + +(define-fun is-power-of-two ((x (_ BitVec 4))) Bool + (= #x0 (bvand x (bvsub x #x1)))) +(declare-const a (_ BitVec 4)) +(define-fun power-test () Bool + (= (is-power-of-two a) + (or (= a #x0) + (= a #x1) + (= a #x2) + (= a #x4) + (= a #x8)))) + +; Predicates over Bitvectors + +(define-fun p1 () Bool (= (bvule #x0a #xf0) true)) ; unsigned less or equal +(define-fun p2 () Bool (= (bvult #x0a #xf0) true)) ; unsigned less than +(define-fun p3 () Bool (= (bvuge #x0a #xf0) false)) ; unsigned greater or equal +(define-fun p4 () Bool (= (bvugt #x0a #xf0) false)) ; unsigned greater than +(define-fun p5 () Bool (= (bvsle #x0a #xf0) false)) ; signed less or equal +(define-fun p6 () Bool (= (bvslt #x0a #xf0) false)) ; signed less than +(define-fun p7 () Bool (= (bvsge #x0a #xf0) true)) ; signed greater or equal +(define-fun p8 () Bool (= (bvsgt #x0a #xf0) true)) ; signed greater than + +; all must be true + +(assert (not (and + b01 b02 b03 b04 b05 b06 b07 b08 b09 b10 + d01 + power-test + p1 p2 p3 p4 p5 p6 p7 p8))) + +(check-sat) diff --git a/regression/smt2_solver/basic-bv1/test.desc b/regression/smt2_solver/basic-bv1/test.desc new file mode 100644 index 0000000000..aee65a85d4 --- /dev/null +++ b/regression/smt2_solver/basic-bv1/test.desc @@ -0,0 +1,7 @@ +CORE +basic-bv1.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- diff --git a/regression/smt2_solver/let-with-bv1/let-with-bv1.smt2 b/regression/smt2_solver/let-with-bv1/let-with-bv1.smt2 new file mode 100644 index 0000000000..baea8cee9a --- /dev/null +++ b/regression/smt2_solver/let-with-bv1/let-with-bv1.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_BV) + +; try 'let' on bitvectors + +(define-fun x () (_ BitVec 4) #x0) + +; very simple +(define-fun let0 () Bool (= (let ((x #x0)) #x1) #x1)) + +; let hides the function 'x' +(define-fun let1 () Bool (= (let ((x #x1)) x) #x1)) + +; the binding isn't visible immediately +(define-fun let2 () Bool (= (let ((x x)) x) #x0)) + +; parallel let +(define-fun let3 () Bool (= (let ((x #x1) (y x)) y) #x0)) + +; limited scope +(define-fun let4 () Bool (and (= (let ((x #x1)) x) #x1) (= x #x0))) + +; all must be true + +(assert (not (and + let0 + let1 + let2 + let3 + let4 + ))) + +(check-sat) diff --git a/regression/smt2_solver/let-with-bv1/test.desc b/regression/smt2_solver/let-with-bv1/test.desc new file mode 100644 index 0000000000..6fc7556943 --- /dev/null +++ b/regression/smt2_solver/let-with-bv1/test.desc @@ -0,0 +1,7 @@ +CORE +let-with-bv1.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- diff --git a/regression/smt2_solver/let1/let1.smt2 b/regression/smt2_solver/let1/let1.smt2 new file mode 100644 index 0000000000..543c993b2c --- /dev/null +++ b/regression/smt2_solver/let1/let1.smt2 @@ -0,0 +1,30 @@ +(set-logic QF_BV) + +(define-fun x () Bool false) + +; very simple +(define-fun let0 () Bool (let ((x false)) true)) + +; let hides the function 'x' +(define-fun let1 () Bool (let ((x true)) x)) + +; the binding isn't visible immediately +(define-fun let2 () Bool (not (let ((x x)) x))) + +; parallel let +(define-fun let3 () Bool (let ((x true) (y x)) (not y))) + +; limited scope +(define-fun let4 () Bool (and (let ((x true)) x) (not x))) + +; all must be true + +(assert (not (and + let0 + let1 + let2 + let3 + let4 + ))) + +(check-sat) diff --git a/regression/smt2_solver/let1/test.desc b/regression/smt2_solver/let1/test.desc new file mode 100644 index 0000000000..834542aa89 --- /dev/null +++ b/regression/smt2_solver/let1/test.desc @@ -0,0 +1,7 @@ +CORE +let1.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +--