Merge pull request #1879 from diffblue/smt2-frontend

An SMT2 frontend plus solver binary

Author: Daniel Kroening

.gitignore

@@ -104,6 +104,8 @@ src/goto-instrument/goto-instrument.exe
 src/jbmc/jbmc
 src/musketeer/musketeer
 src/musketeer/musketeer.exe
+src/solvers/smt2/smt2_solver
+src/solvers/smt2/smt2_solver.exe
 src/symex/symex
 src/symex/symex.exe
 src/goto-diff/goto-diff

regression/Makefile

@@ -11,6 +11,7 @@ DIRS = cbmc \
        strings-smoke-tests \
        cbmc-cover \
        goto-instrument-typedef \
+       smt2_solver \
        strings \
        invariants \
        goto-diff \

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

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)

regression/smt2_solver/basic-bv1/test.desc

@@ -0,0 +1,7 @@
+CORE
+basic-bv1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

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)

regression/smt2_solver/let-with-bv1/test.desc

@@ -0,0 +1,7 @@
+CORE
+let-with-bv1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

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)

regression/smt2_solver/let1/test.desc

@@ -0,0 +1,7 @@
+CORE
+let1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

src/ansi-c/expr2c.cpp

@@ -944,6 +944,26 @@ std::string expr2ct::convert_with(
   return dest;
 }
 
+std::string expr2ct::convert_let(
+  const let_exprt &src,
+  unsigned precedence)
+{
+  if(src.operands().size()<3)
+    return convert_norep(src, precedence);
+
+  unsigned p0;
+  std::string op0=convert_with_precedence(src.op0(), p0);
+
+  std::string dest="LET ";
+  dest+=convert(src.symbol());
+  dest+='=';
+  dest+=convert(src.value());
+  dest+=" IN ";
+  dest+=convert(src.where());
+
+  return dest;
+}
+
 std::string expr2ct::convert_update(
   const exprt &src,
   unsigned precedence)
@@ -3936,6 +3956,9 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_sizeof)
     return convert_sizeof(src, precedence);
 
+  else if(src.id()==ID_let)
+    return convert_let(to_let_expr(src), precedence=16);
+
   else if(src.id()==ID_type)
     return convert(src.type());