From e642e4bd420896522919f4984f40be7928693760 Mon Sep 17 00:00:00 2001 From: "Mark S. Baranowski" Date: Wed, 31 Jul 2019 23:09:52 -0600 Subject: [PATCH] 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. --- .travis.yml | 1 + include/smack/SmackOptions.h | 3 +++ lib/smack/SmackInstGenerator.cpp | 23 +++++++++++++++++++++++ lib/smack/SmackOptions.cpp | 11 +++++++++++ share/smack/top.py | 5 +++++ test/special/assume.c | 12 ++++++++++++ test/special/assume2.c | 12 ++++++++++++ test/special/assume_check.c | 12 ++++++++++++ test/special/assume_check2.c | 13 +++++++++++++ test/special/assume_check_fail.c | 13 +++++++++++++ test/special/assume_fail.c | 12 ++++++++++++ 11 files changed, 117 insertions(+) create mode 100644 test/special/assume.c create mode 100644 test/special/assume2.c create mode 100644 test/special/assume_check.c create mode 100644 test/special/assume_check2.c create mode 100644 test/special/assume_check_fail.c create mode 100644 test/special/assume_fail.c 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); +}