diff --git a/.travis.yml b/.travis.yml index 70f6ce234..6bb28f7e1 100644 --- a/.travis.yml +++ b/.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 diff --git a/include/smack/SmackOptions.h b/include/smack/SmackOptions.h index 66c0f34dc..a6c210311 100644 --- a/include/smack/SmackOptions.h +++ b/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 EntryPoints; @@ -28,6 +30,7 @@ class SmackOptions { static const llvm::cl::opt FloatEnabled; static const llvm::cl::opt MemorySafety; static const llvm::cl::opt IntegerOverflow; + static const llvm::cl::opt LLVMAssumes; static const llvm::cl::opt AddTiming; static bool isEntryPoint(std::string); diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index 55fcd4807..a7663d812 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/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> stmtMap{ + {llvm::Intrinsic::assume, assume}, {llvm::Intrinsic::bitreverse, assignBvExpr(bitreverse)}, {llvm::Intrinsic::bswap, assignBvExpr(bswap)}, {llvm::Intrinsic::convert_from_fp16, f16UpCast}, diff --git a/lib/smack/SmackOptions.cpp b/lib/smack/SmackOptions.cpp index 6c835170c..1376bede0 100644 --- a/lib/smack/SmackOptions.cpp +++ b/lib/smack/SmackOptions.cpp @@ -66,6 +66,17 @@ const llvm::cl::opt const llvm::cl::opt SmackOptions::IntegerOverflow( "integer-overflow", llvm::cl::desc("Enable integer overflow checks")); +const llvm::cl::opt 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) diff --git a/share/smack/top.py b/share/smack/top.py index 97cb68db2..6211e2ad6 100755 --- a/share/smack/top.py +++ b/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) diff --git a/test/special/assume.c b/test/special/assume.c new file mode 100644 index 000000000..6e66bdbd8 --- /dev/null +++ b/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); +} diff --git a/test/special/assume2.c b/test/special/assume2.c new file mode 100644 index 000000000..e4c47314a --- /dev/null +++ b/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); +} diff --git a/test/special/assume_check.c b/test/special/assume_check.c new file mode 100644 index 000000000..54d460e86 --- /dev/null +++ b/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); +} diff --git a/test/special/assume_check2.c b/test/special/assume_check2.c new file mode 100644 index 000000000..979369b33 --- /dev/null +++ b/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); +} diff --git a/test/special/assume_check_fail.c b/test/special/assume_check_fail.c new file mode 100644 index 000000000..1faa46507 --- /dev/null +++ b/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); +} diff --git a/test/special/assume_fail.c b/test/special/assume_fail.c new file mode 100644 index 000000000..b0a803faa --- /dev/null +++ b/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); +}