Allow optional generation of Boogie assumes from llvm.assume intrinsics

LLVM has the llvm.assume intrinsic which is intended to allow a
compiler to communicate facts about a program to LLVM's
optimizers. These facts may be useful for verification, so this allows
them to be used. Additionally, checking of assumptions is possible in
order to diagnose faulty assumptions arising from source code or
compiler bugs.

Specifically, a new flag "--llvm-assumes" is added with three modes:
- "none": This ignores the llvm.assume intrinsic and is the default
  mode.
- "use": This enables generation of Boogie assumes from llvm.assume
  instructions.
- "check": This enables assertion checking of the validity of assumed
  statements.

Author: keram88

.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, y is clearly odd.
+  __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, y is clearly odd.
+  __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);
+}