Merge pull request #479 from smackers/cvc4_support

CVC4 support

Author: zvonimir

bin/build.sh

@@ -23,6 +23,7 @@
 # Set these flags to control various installation options
 INSTALL_DEPENDENCIES=1
 INSTALL_Z3=1
+INSTALL_CVC4=1
 BUILD_BOOGIE=1
 BUILD_CORRAL=1
 BUILD_SYMBOOGLIX=1
@@ -40,6 +41,7 @@ INSTALL_RUST=0
 SMACK_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && cd .. && pwd )"
 ROOT="$( cd "${SMACK_DIR}" && cd .. && pwd )"
 Z3_DIR="${ROOT}/z3"
+CVC4_DIR="${ROOT}/cvc4"
 BOOGIE_DIR="${ROOT}/boogie"
 CORRAL_DIR="${ROOT}/corral"
 SYMBOOGLIX_DIR="${ROOT}/symbooglix"
@@ -405,6 +407,18 @@ if [ ${INSTALL_Z3} -eq 1 ] ; then
   fi
 fi
 
+if [ ${INSTALL_CVC4} -eq 1 ] ; then
+  if [ ! -d "$CVC4_DIR" ] ; then
+    puts "Installing CVC4"
+    mkdir -p ${CVC4_DIR}
+    ${WGET} https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt -O cvc4
+    chmod +x cvc4
+    mv cvc4 ${CVC4_DIR}
+    puts "Installed CVC4"
+  else
+    puts "CVC4 already installed"
+  fi
+fi
 
 if [ ${BUILD_BOOGIE} -eq 1 ] ; then
   if ! upToDate $BOOGIE_DIR $BOOGIE_COMMIT ; then
@@ -420,6 +434,7 @@ if [ ${BUILD_BOOGIE} -eq 1 ] ; then
     rm -rf /tmp/nuget/
     msbuild Boogie.sln /p:Configuration=Release
     ln -sf ${Z3_DIR}/bin/z3 ${BOOGIE_DIR}/Binaries/z3.exe
+    ln -sf ${CVC4_DIR}/cvc4 ${BOOGIE_DIR}/Binaries/cvc4.exe
     puts "Built Boogie"
   else
     puts "Boogie already built"
@@ -439,6 +454,7 @@ if [ ${BUILD_CORRAL} -eq 1 ] ; then
     git submodule update
     msbuild cba.sln /p:Configuration=Release
     ln -sf ${Z3_DIR}/bin/z3 ${CORRAL_DIR}/bin/Release/z3.exe
+    ln -sf ${CVC4_DIR}/cvc4 ${CORRAL_DIR}/bin/Release/cvc4.exe
     puts "Built Corral"
   else
     puts "Corral already built"

lib/smack/Prelude.cpp

@@ -381,9 +381,9 @@ void IntOpGen::generateArithOps(std::stringstream &s) const {
        bvBuiltinOp, true},
       {"sdiv", 2, intBuiltinOp, bvBuiltinOp, false},
       {"smod", 2, intBuiltinOp, bvBuiltinOp, false},
-      {"srem", 2, intBuiltinOp, bvBuiltinOp, false},
       {"udiv", 2, intBuiltinOp, bvBuiltinOp, false},
-      {"urem", 2, intBuiltinOp, bvBuiltinOp, false},
+      {"srem", 2, uninterpretedOp, bvBuiltinOp, false},
+      {"urem", 2, uninterpretedOp, bvBuiltinOp, false},
       {"shl", 2, uninterpretedOp, bvBuiltinOp, false},
       {"lshr", 2, uninterpretedOp, bvBuiltinOp, false},
       {"ashr", 2, uninterpretedOp, bvBuiltinOp, false},
@@ -731,7 +731,7 @@ void IntOpGen::generateBvIntConvs(std::stringstream &s) const {
     << "\n";
   if (SmackOptions::BitPrecise && !SmackOptions::BitPrecisePointers) {
     s << Decl::function(indexedName("$bv2uint", {ptrSize}), {{"i", bt}}, it,
-                        nullptr, {makeBuiltinAttr("bv2int")})
+                        nullptr, {makeBuiltinAttr("bv2nat")})
       << "\n";
     const Expr *arg = Expr::id("i");
     const Expr *uint = Expr::fn(indexedName("$bv2uint", {ptrSize}), arg);
@@ -753,7 +753,7 @@ void IntOpGen::generateBvIntConvs(std::stringstream &s) const {
       << "\n";
   } else
     s << Decl::function(indexedName("$bv2int", {ptrSize}), {{"i", bt}}, it,
-                        nullptr, {makeBuiltinAttr("bv2int")})
+                        nullptr, {makeBuiltinAttr("bv2nat")})
       << "\n";
   s << "\n";
 }

share/smack/top.py

@@ -208,6 +208,10 @@ def arguments():
     choices=['boogie', 'corral', 'symbooglix', 'svcomp'], default='corral',
     help='back-end verification engine')
 
+  verifier_group.add_argument('--solver',
+    choices=['z3', 'cvc4'], default='z3',
+    help='back-end SMT solver')
+
   verifier_group.add_argument('--unroll', metavar='N', default='1',
     type = lambda x: int(x) if int(x) > 0 else parser.error('Unroll bound has to be positive.'),
     help='loop/recursion unroll bound [default: %(default)s]')
@@ -460,6 +464,8 @@ def verify_bpl(args):
     command += ["/errorLimit:%s" % args.max_violations]
     if not args.modular:
       command += ["/loopUnroll:%d" % args.unroll]
+    if args.solver == 'cvc4':
+      command += ["/proverOpt:SOLVER=cvc4"]
 
   elif args.verifier == 'corral':
     command = ["corral"]
@@ -471,7 +477,9 @@ def verify_bpl(args):
     command += ["/cex:%s" % args.max_violations]
     command += ["/maxStaticLoopBound:%d" % args.loop_limit]
     command += ["/recursionBound:%d" % args.unroll]
-	
+    if args.solver == 'cvc4':
+      command += ["/bopt:proverOpt:SOLVER=cvc4"]
+
   elif args.verifier == 'symbooglix':
     command = ['symbooglix']
     command += [args.bpl_file]