An SMT2 frontend plus solver binary

.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());
 

src/ansi-c/expr2c_class.h

@@ -253,6 +253,7 @@ class expr2ct
   std::string convert_designated_initializer(const exprt &src, unsigned &precedence);
   std::string convert_concatenation(const exprt &src, unsigned &precedence);
   std::string convert_sizeof(const exprt &src, unsigned &precedence);
+  std::string convert_let(const let_exprt &, unsigned precedence);
 
   std::string convert_struct(
     const exprt &src,

src/solvers/CMakeLists.txt

@@ -1,3 +1,6 @@
+set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD_REQUIRED true)
+
 #   We may use one of several different solver libraries.
 #   The following files wrap the chosen solver library.
 #   We remove them all from the solver-library sources list, and then add the
@@ -104,6 +107,10 @@ elseif("${sat_impl}" STREQUAL "glucose")
     target_link_libraries(solvers glucose-condensed)
 endif()
 
-target_link_libraries(solvers java_bytecode util)
+target_link_libraries(solvers util)
+
+# Executable
+add_executable(smt2_solver smt2/smt2_solver.cpp)
+target_link_libraries(smt2_solver solvers)
 
 generic_includes(solvers)

src/solvers/Makefile

@@ -125,6 +125,7 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/boolbv_ieee_float_rel.cpp \
       flattening/boolbv_if.cpp \
       flattening/boolbv_index.cpp \
+      flattening/boolbv_let.cpp \
       flattening/boolbv_map.cpp \
       flattening/boolbv_member.cpp \
       flattening/boolbv_mod.cpp \
@@ -215,9 +216,9 @@ INCLUDES += -I .. \
   $(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
 	$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
 
-CLEANFILES = solvers$(LIBEXT)
+CLEANFILES = solvers$(LIBEXT) smt2_solver$(EXEEXT)
 
-all: solvers$(LIBEXT)
+all: solvers$(LIBEXT) smt2_solver$(EXEEXT)
 
 ifneq ($(SQUOLEM2),)
   CP_CXXFLAGS += -DHAVE_QBF_CORE
@@ -231,9 +232,15 @@ endif
 
 -include $(SRC:.cpp=.d)
 
-###############################################################################
-
-solvers$(LIBEXT): $(OBJ) $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
+SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
         $(MINISAT2_LIB) $(SMVSAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
 	$(PRECOSAT_LIB) $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)
+
+###############################################################################
+
+solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB)
 	$(LINKLIB) $(LIBSOLVER)
+
+smt2_solver$(EXEEXT): $(OBJ) smt2/smt2_solver$(OBJEXT) \
+	../util/util$(LIBEXT) ../langapi/langapi$(LIBEXT) ../big-int/big-int$(LIBEXT) $(SOLVER_LIB)
+	$(LINKBIN) $(LIBSOLVER)

src/solvers/flattening/boolbv.cpp

@@ -278,14 +278,10 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_array_of)
     return convert_array_of(to_array_of_expr(expr));
   else if(expr.id()==ID_let)
-  {
-    // const let_exprt &let_expr=to_let_expr(expr);
-    throw "let is todo";
-  }
+    return convert_let(to_let_expr(expr));
   else if(expr.id()==ID_function_application)
-  {
-    return convert_function_application(to_function_application_expr(expr));
-  }
+    return convert_function_application(
+      to_function_application_expr(expr));
   else if(expr.id()==ID_reduction_or  || expr.id()==ID_reduction_and  ||
           expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
           expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
@@ -463,6 +459,15 @@ literalt boolbvt::convert_rest(const exprt &expr)
     return convert_quantifier(expr);
   else if(expr.id()==ID_exists)
     return convert_quantifier(expr);
+  else if(expr.id()==ID_let)
+  {
+    bvt bv=convert_let(to_let_expr(expr));
+
+    DATA_INVARIANT(bv.size()==1,
+      "convert_let must return 1-bit vector for boolean let");
+
+    return bv[0];
+  }
   else if(expr.id()==ID_index)
   {
     bvt bv=convert_index(to_index_expr(expr));

src/solvers/flattening/boolbv.h

@@ -145,6 +145,7 @@ class boolbvt:public arrayst
   virtual bvt convert_complex_real(const exprt &expr);
   virtual bvt convert_complex_imag(const exprt &expr);
   virtual bvt convert_lambda(const exprt &expr);
+  virtual bvt convert_let(const let_exprt &);
   virtual bvt convert_array_of(const array_of_exprt &expr);
   virtual bvt convert_union(const union_exprt &expr);
   virtual bvt convert_bv_typecast(const typecast_exprt &expr);

src/solvers/flattening/boolbv_let.cpp

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "boolbv.h"
+
+#include <util/std_expr.h>
+#include <util/std_types.h>
+
+bvt boolbvt::convert_let(const let_exprt &expr)
+{
+  const bvt value_bv=convert_bv(expr.value());
+
+  // We expect the identifiers of the bound symbols to be unique,
+  // and thus, these can go straight into the symbol to literal map.
+  // This property also allows us to cache any subexpressions.
+  const irep_idt &id=expr.symbol().get_identifier();
+
+  // the symbol shall be visible during the recursive call
+  // to convert_bv
+  map.set_literals(id, expr.symbol().type(), value_bv);
+  bvt result_bv=convert_bv(expr.where());
+
+  // now remove, no longer needed
+  map.erase_literals(id, expr.symbol().type());
+
+  return result_bv;
+}

src/solvers/flattening/boolbv_map.cpp

@@ -146,3 +146,10 @@ void boolbv_mapt::set_literals(
     mb.l=literal;
   }
 }
+
+void boolbv_mapt::erase_literals(
+  const irep_idt &identifier,
+  const typet &)
+{
+  mapping.erase(identifier);
+}

src/solvers/flattening/boolbv_map.h

@@ -75,6 +75,10 @@ class boolbv_mapt
     const typet &type,
     const bvt &literals);
 
+  void erase_literals(
+    const irep_idt &identifier,
+    const typet &type);
+
 protected:
   propt ∝
   const namespacet &ns;