[WIP] Optionally model the LLVM assume statement in Boogie

.travis.yml

@@ -36,6 +36,7 @@ env:
     - TRAVIS_ENV="--exhaustive --folder=memory-safety"
     - TRAVIS_ENV="--exhaustive --folder=pthread"
     - TRAVIS_ENV="--exhaustive --folder=strings"
+    - TRAVIS_ENV="--exhaustive --folder=special"
 
 before_install:
   - sudo rm -rf /usr/local/clang-7.0.0

include/smack/SmackOptions.h

@@ -10,6 +10,8 @@
 #include "smack/SmackWarnings.h"
 
 namespace smack {
+enum class LLVMAssumeType { none, use, check };
+
 class SmackOptions {
 public:
   static const llvm::cl::list<std::string> EntryPoints;
@@ -28,6 +30,7 @@ class SmackOptions {
   static const llvm::cl::opt<bool> FloatEnabled;
   static const llvm::cl::opt<bool> MemorySafety;
   static const llvm::cl::opt<bool> IntegerOverflow;
+  static const llvm::cl::opt<LLVMAssumeType> LLVMAssumes;
   static const llvm::cl::opt<bool> AddTiming;
 
   static bool isEntryPoint(std::string);

lib/smack/SmackInstGenerator.cpp

@@ -902,6 +902,28 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) {
         };
       };
 
+  // Optionally generate a boogie assume statement from assume statements in
+  // LLVM. Currently this behavior is experimental and must be enabled by
+  // passing the -llvm-assumes flag. The default behavior of this
+  // function is to ignore the assume statement, specified by the "none"
+  // argument. If the check argument is given, an additional assertion is
+  // generated to check the validity of the assumption.
+  static const auto assume = [this](CallInst *ci) {
+    if (SmackOptions::LLVMAssumes != LLVMAssumeType::none) {
+      auto arg = rep->expr(ci->getArgOperand(0));
+      auto llvmTrue =
+          SmackOptions::BitPrecise ? Expr::lit(1, 1) : Expr::lit(1LL);
+      auto chkStmt = Expr::eq(arg, llvmTrue);
+      if (SmackOptions::LLVMAssumes == LLVMAssumeType::check)
+        emit(Stmt::assert_(chkStmt));
+      else
+        emit(Stmt::assume(chkStmt));
+    } else {
+      // Skip assume statements
+      return;
+    }
+  };
+
   static const auto f16UpCast = conditionalModel(
       [this](CallInst *ci) {
         // translation: $f := $fpext.bvhalf.*($rmode, $bitcast.bv16.bvhalf($i));
@@ -1130,6 +1152,7 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) {
 
   static const std::map<llvm::Intrinsic::ID, std::function<void(CallInst *)>>
       stmtMap{
+          {llvm::Intrinsic::assume, assume},
           {llvm::Intrinsic::bitreverse, assignBvExpr(bitreverse)},
           {llvm::Intrinsic::bswap, assignBvExpr(bswap)},
           {llvm::Intrinsic::convert_from_fp16, f16UpCast},

lib/smack/SmackOptions.cpp

@@ -66,6 +66,17 @@ const llvm::cl::opt<bool>
 const llvm::cl::opt<bool> SmackOptions::IntegerOverflow(
     "integer-overflow", llvm::cl::desc("Enable integer overflow checks"));
 
+const llvm::cl::opt<LLVMAssumeType> SmackOptions::LLVMAssumes(
+    "llvm-assumes",
+    llvm::cl::desc(
+        "Optionally enable generation of Boogie assumes from LLVM assumes"),
+    llvm::cl::values(clEnumValN(LLVMAssumeType::none, "none",
+                                "disable generation of assume statements"),
+                     clEnumValN(LLVMAssumeType::use, "use",
+                                "enable generation of assume statements"),
+                     clEnumValN(LLVMAssumeType::check, "check",
+                                "enable checking of assume statements")));
+
 bool SmackOptions::isEntryPoint(std::string name) {
   for (auto EP : EntryPoints)
     if (name == EP)

share/smack/top.py

@@ -197,6 +197,10 @@ def arguments():
   translate_group.add_argument('--integer-overflow', action='store_true', default=False,
     help='enable integer overflow checks')
 
+  translate_group.add_argument('--llvm-assumes', choices=['none', 'use', 'check'], default='none',
+    help='optionally enable generation of Boogie assume statements from LLVM assume statements ' +
+         '(none=no generation [default], use=generate assume statements, check=check assume statements)')
+
   translate_group.add_argument('--float', action="store_true", default=False,
     help='enable bit-precise floating-point functions')
 
@@ -347,6 +351,7 @@ def llvm_to_bpl(args):
   if args.no_memory_splitting: cmd += ['-no-memory-splitting']
   if args.memory_safety: cmd += ['-memory-safety']
   if args.integer_overflow: cmd += ['-integer-overflow']
+  if args.llvm_assumes: cmd += ['-llvm-assumes=' + args.llvm_assumes]
   if args.float: cmd += ['-float']
   if args.modular: cmd += ['-modular']
   try_command(cmd, console=True)

test/special/assume.c

@@ -0,0 +1,12 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --llvm-assumes=use
+
+int main(void) {
+  unsigned int y = 2 * (unsigned int)__VERIFIER_nondet_unsigned_short();
+  // This assumption is used for verification, even though bit-precise
+  // is not enabled, the assertion will pass.
+  __builtin_assume((y & 1) == 0);
+  __VERIFIER_assert((y & 1) == 0);
+}

test/special/assume2.c

@@ -0,0 +1,12 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --llvm-assumes=use
+
+int main(void) {
+  unsigned int y = (2 * (unsigned int)__VERIFIER_nondet_unsigned_short()) + 1;
+  // This assumption is used for verification, even though the assumption
+  // is false, the assertion will pass.
+  __builtin_assume((y & 1) == 0);
+  __VERIFIER_assert((y & 1) == 0);
+}

test/special/assume_check.c

@@ -0,0 +1,12 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --llvm-assumes=check
+// @flag --bit-precise
+
+int main(void) {
+  unsigned int y = 2 * (unsigned int)__VERIFIER_nondet_unsigned_short();
+  // This assumption is checked under bit-precise and is verified.
+  __builtin_assume((y & 1) == 0);
+  __VERIFIER_assert((y & 1) == 0);
+}

test/special/assume_check2.c

@@ -0,0 +1,13 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --llvm-assumes=check
+// @flag --bit-precise
+
+int main(void) {
+  unsigned int y = (2 * (unsigned int)__VERIFIER_nondet_unsigned_short()) + 1;
+  // This assumption is checked at verification time, and since bit-precise
+  // is enabled, and y is clearly odd, the check will pass.
+  __builtin_assume((y & 1) == 1);
+  __VERIFIER_assert((y & 1) == 1);
+}

test/special/assume_check_fail.c

@@ -0,0 +1,13 @@
+#include "smack.h"
+
+// @expect error
+// @flag --llvm-assumes=check
+// @flag --bit-precise
+
+int main(void) {
+  unsigned int y = (2 * (unsigned int)__VERIFIER_nondet_unsigned_short()) + 1;
+  // This assumption is checked at verification time, and since bit-precise
+  // is enabled, and y is clearly odd, the assumption should be shown false.
+  __builtin_assume((y & 1) == 0);
+  __VERIFIER_assert((y & 1) == 0);
+}

test/special/assume_fail.c

@@ -0,0 +1,12 @@
+#include "smack.h"
+
+// @expect error
+// @flag --llvm-assumes=none
+
+int main(void) {
+  unsigned int y = 2 * (unsigned int)__VERIFIER_nondet_unsigned_short();
+  // This assumption is not used, and since bit-precise is not enabled,
+  // verification will fail.
+  __builtin_assume((y & 1) == 0);
+  __VERIFIER_assert((y & 1) == 0);
+}