From 96785f1794827e72d8e81a2ca21b6a27790edf81 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 1 Jul 2019 20:02:35 +0000 Subject: [PATCH] Improved SMACK's warning system MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This commit changes SMACK's warning system as follows, 1. Added a class (SmackWarnings) to provide APIs that print warning messages to both the Boogie program and the console. 2. The warning messages are layered: there are three levels, silent (no messages), unsound (messages about unsoundness such as using uninterpreted functions to model bitwise operations), and info (messages about unsoundness as well as translation information such as collapsing DSA nodes). Their relation is silent ⊂ unsound ⊂ info. 3. The warning messages can be colored, which is controlled by the llvm2bpl option, `-colored-warnings`. Co-authored-by: Mark Stanislaw Baranowski Co-authored-by: Shaobo He --- CMakeLists.txt | 2 + include/smack/SmackOptions.h | 5 +- include/smack/SmackRep.h | 4 + include/smack/SmackWarnings.h | 46 ++++++ lib/DSA/DSMonitor.cpp | 29 ++-- lib/smack/SmackInstGenerator.cpp | 256 +++++++++++++++---------------- lib/smack/SmackOptions.cpp | 16 +- lib/smack/SmackRep.cpp | 31 ++-- lib/smack/SmackWarnings.cpp | 81 ++++++++++ share/smack/top.py | 10 +- 10 files changed, 318 insertions(+), 162 deletions(-) create mode 100644 include/smack/SmackWarnings.h create mode 100644 lib/smack/SmackWarnings.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 2256efa6a..9c39d3fce 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -180,6 +180,7 @@ add_library(smackTranslator STATIC include/smack/NormalizeLoops.h include/smack/SplitAggregateValue.h include/smack/Prelude.h + include/smack/SmackWarnings.h lib/smack/AddTiming.cpp lib/smack/BoogieAst.cpp lib/smack/BplFilePrinter.cpp @@ -203,6 +204,7 @@ add_library(smackTranslator STATIC lib/smack/NormalizeLoops.cpp lib/smack/SplitAggregateValue.cpp lib/smack/Prelude.cpp + lib/smack/SmackWarnings.cpp ) add_executable(llvm2bpl diff --git a/include/smack/SmackOptions.h b/include/smack/SmackOptions.h index 4fbd23747..3c27642d8 100644 --- a/include/smack/SmackOptions.h +++ b/include/smack/SmackOptions.h @@ -7,12 +7,15 @@ #include "llvm/Support/CommandLine.h" +#include "smack/SmackWarnings.h" + namespace smack { class SmackOptions { public: static const llvm::cl::list EntryPoints; - static const llvm::cl::opt Warnings; + static const llvm::cl::opt WarningLevel; + static const llvm::cl::opt ColoredWarnings; static const llvm::cl::opt MemoryModelDebug; static const llvm::cl::opt MemoryModelImpls; diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index c41318bb1..dfe660cc4 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -80,6 +80,7 @@ class SmackRep { const Stmt* store(unsigned R, const llvm::Type* T, const Expr* P, const Expr* V); const Expr* cast(unsigned opcode, const llvm::Value* v, const llvm::Type* t); + bool isFpArithOp(unsigned opcode); const Expr* bop(unsigned opcode, const llvm::Value* lhs, const llvm::Value* rhs, const llvm::Type* t); const Expr* cmp(unsigned predicate, const llvm::Value* lhs, const llvm::Value* rhs, bool isUnsigned); @@ -127,6 +128,9 @@ class SmackRep { const Expr* cast(const llvm::Instruction* I); const Expr* cast(const llvm::ConstantExpr* CE); + bool isBitwiseOp(llvm::Instruction* I); + bool isFpArithOp(llvm::Instruction* I); + const Expr* bop(const llvm::BinaryOperator* BO); const Expr* bop(const llvm::ConstantExpr* CE); diff --git a/include/smack/SmackWarnings.h b/include/smack/SmackWarnings.h new file mode 100644 index 000000000..6ab6a7d41 --- /dev/null +++ b/include/smack/SmackWarnings.h @@ -0,0 +1,46 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// + +#ifndef SMACKWARNINGS_H +#define SMACKWARNINGS_H + +#include "llvm/Support/CommandLine.h" +#include "llvm/IR/Instruction.h" +#include "smack/BoogieAst.h" + +#include +#include + +namespace smack { + +class SmackWarnings { + typedef const llvm::cl::opt FlagT; + typedef std::initializer_list RequiredFlagsT; + typedef std::list UnsetFlagsT; + +public: + enum class WarningLevel: unsigned { + Silent=0, + Unsound=10, // Unhandled intrinsics, asm, etc + Info=20 // Memory length, etc. + }; + + static UnsetFlagsT getUnsetFlags(RequiredFlagsT flags); + + // generate warnings about unsoundness + static void warnUnsound(std::string unmodeledOpName, Block* currBlock, const llvm::Instruction* i, bool ignore=false); + static void warnUnsound(std::string name, UnsetFlagsT unsetFlags, Block* currBlock, const llvm::Instruction* i, bool ignore=false); + static void warnIfUnsound(std::string name, RequiredFlagsT requiredFlags, Block* currBlock, const llvm::Instruction* i, bool ignore=false); + static void warnIfUnsound(std::string name, FlagT& requiredFlag, Block* currBlock, const llvm::Instruction* i); + static void warnIfUnsound(std::string name, FlagT& requiredFlag1, FlagT& requiredFlag2, Block* currBlock, const llvm::Instruction* i); + + // generate warnings about memcpy/memset length/DSA + static void warnInfo(std::string info); +private: + static bool isSufficientWarningLevel(WarningLevel level); + static std::string getFlagStr(UnsetFlagsT flags); +}; +} + +#endif // SMACKWARNINGS_H diff --git a/lib/DSA/DSMonitor.cpp b/lib/DSA/DSMonitor.cpp index e961cb27e..733d68db3 100644 --- a/lib/DSA/DSMonitor.cpp +++ b/lib/DSA/DSMonitor.cpp @@ -2,7 +2,8 @@ #include "dsa/DSMonitor.h" #include "dsa/DSGraph.h" #include "llvm/IR/DebugInfo.h" -#include "smack/SmackOptions.h" +#include "llvm/Support/raw_ostream.h" +#include "smack/SmackWarnings.h" #include @@ -156,40 +157,42 @@ void DSMonitor::watch(DSNodeHandle N, std::vector VS, std::string M) { } void DSMonitor::warn() { - if (!smack::SmackOptions::Warnings) - return; + std::string msg; + raw_string_ostream ss(msg); if (location != "") - errs() << location << ": "; + ss << location << ": "; - errs() << "warning: collapsing DSA node\n"; + ss << "warning: collapsing DSA node\n"; if (message != "") - errs() << message << "\n"; + ss << message << "\n"; if (VS.empty()) { - errs() << "(unknown value)" << "\n"; + ss << "(unknown value)" << "\n"; } else { if (Instruction *I = getInstruction(VS[0])) { if (BasicBlock *B = I->getParent()) { if (Function *F = B->getParent()) { if (F->hasName()) - errs() << "in function:\n " << F->getName() << "\n"; + ss << "in function:\n " << F->getName() << "\n"; } if (B->hasName()) - errs() << "in block:\n " << I->getParent()->getName() << "\n"; + ss << "in block:\n " << I->getParent()->getName() << "\n"; } - errs() << "at instruction:\n" << *I << "\n"; + ss << "at instruction:\n" << *I << "\n"; } for (auto V : VS) - errs() << "at value:\n" << *V << "\n"; + ss << "at value:\n" << *V << "\n"; if (caption != "") - errs() << "node:\n " << caption << "\n"; + ss << "node:\n " << caption << "\n"; } - errs() << "\n"; + ss << "\n"; + + smack::SmackWarnings::warnInfo(ss.str()); } void DSMonitor::witness(DSNodeHandle N, std::vector VS, std::string M) { diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index 04845ef73..d4462c8fa 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -20,16 +20,15 @@ #include "llvm/Support/raw_ostream.h" #include "dsa/DSNode.h" +#include "smack/SmackWarnings.h" + namespace smack { using llvm::errs; using namespace llvm; -const bool CODE_WARN = true; const bool SHOW_ORIG = false; -#define WARN(str) \ - if (CODE_WARN) emit(Stmt::comment(std::string("WARNING: ") + str)) #define ORIG(ins) \ if (SHOW_ORIG) emit(Stmt::comment(i2s(ins))) @@ -304,7 +303,8 @@ void SmackInstGenerator::visitInvokeInst(llvm::InvokeInst& ii) { emit(rep->call(f, ii)); } else { // llvm_unreachable("Unexpected invoke instruction."); - WARN("unsoundly ignoring invoke instruction... "); + SmackWarnings::warnUnsound("invoke instruction", currBlock, &ii, + ii.getType()->isVoidTy()); } std::vector > targets; targets.push_back({ @@ -337,6 +337,13 @@ void SmackInstGenerator::visitUnreachableInst(llvm::UnreachableInst& ii) { void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator& I) { processInstruction(I); + if (rep->isBitwiseOp(&I)) + SmackWarnings::warnIfUnsound(std::string("bitwise operation ")+I.getOpcodeName(), + SmackOptions::BitPrecise, currBlock, &I); + if (rep->isFpArithOp(&I)) + SmackWarnings::warnIfUnsound(std::string("floating-point arithmetic ")+I.getOpcodeName(), + SmackOptions::FloatEnabled, currBlock, &I); + const Expr *E; if (isa(I.getType())) { auto X = I.getOperand(0); @@ -610,7 +617,8 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { std::string name = f->hasName() ? f->getName() : ""; if (ci.isInlineAsm()) { - WARN("unsoundly ignoring inline asm call: " + i2s(ci)); + SmackWarnings::warnUnsound("inline asm call " + i2s(ci), currBlock, &ci, + ci.getType()->isVoidTy()); emit(Stmt::skip()); } else if (name.find(Naming::RUST_ENTRY) != std::string::npos) { @@ -793,7 +801,6 @@ void SmackInstGenerator::visitDbgValueInst(llvm::DbgValueInst& dvi) { if (currInst != dvi.getParent()->begin()) { const Instruction& pi = *std::prev(currInst); V = V->stripPointerCasts(); - WARN(i2s(pi)); if (!llvm::isa(&pi) && V == llvm::dyn_cast(&pi)) emit(recordProcedureCall(V, {Attr::attr("cexpr", var->getName().str())})); } @@ -814,7 +821,7 @@ void SmackInstGenerator::visitLandingPadInst(llvm::LandingPadInst& lpi) { emit(Stmt::assign(rep->expr(&lpi),Expr::id(Naming::EXN_VAL_VAR))); if (lpi.isCleanup()) emit(Stmt::assign(Expr::id(Naming::EXN_VAR), Expr::lit(false))); - WARN("unsoundly ignoring landingpad clauses..."); + SmackWarnings::warnUnsound("landingpad clauses", currBlock, &lpi, true); } /******************************************************************************/ @@ -834,61 +841,62 @@ void SmackInstGenerator::visitMemSetInst(llvm::MemSetInst& msi) { } void SmackInstGenerator::generateUnModeledCall(llvm::CallInst* ci) { - if (ci->getFunctionType()->getReturnType()->isVoidTy()) { - WARN("ignoring call to "+ci->getCalledFunction()->getName().str()); - emit(Stmt::skip()); - } else { - errs() << "warning: over-approximate call to : " - << ci->getCalledFunction()->getName() << "\n"; - emit(rep->call(ci->getCalledFunction(), *ci)); - } + SmackWarnings::warnUnsound(ci->getCalledFunction()->getName(), + currBlock, ci, ci->getType()->isVoidTy()); + emit(rep->call(ci->getCalledFunction(), *ci)); } void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst& ii) { processInstruction(ii); - static const auto f16UpCast = [this] (CallInst* ci) { + //(CallInst -> Void) -> [Flags] -> (CallInst -> Void) + static const auto conditionalModel = [this] (std::function modelGenFunc, + std::initializer_list*> requiredFlags) { + return [this, requiredFlags, modelGenFunc] (CallInst* ci) { + auto unsetFlags = SmackWarnings::getUnsetFlags(requiredFlags); + if (unsetFlags.empty()) + modelGenFunc(ci); + else { + SmackWarnings::warnUnsound("call to " + ci->getCalledFunction()->getName().str(), + unsetFlags, currBlock, ci); + emit(rep->call(ci->getCalledFunction(), *ci)); + } + }; + }; + + static const auto f16UpCast = conditionalModel([this] (CallInst* ci) { // translation: $f := $fpext.bvhalf.*($rmode, $bitcast.bv16.bvhalf($i)); auto argT = rep->type(ci->getArgOperand(0)->getType()); auto retT = rep->type(ci->getFunctionType()->getReturnType()); - if (SmackOptions::FloatEnabled && SmackOptions::BitPrecise) - emit(Stmt::assign( - rep->expr(ci), - Expr::fn(indexedName("$fpext", {Naming::HALF_TYPE, retT}), - {Expr::id(Naming::RMODE_VAR), - Expr::fn(indexedName("$bitcast", {argT, Naming::HALF_TYPE}), - rep->expr(ci->getArgOperand(0)))}))); - else - generateUnModeledCall(ci); - }; - - static const auto f16DownCast = [this] (CallInst* ci){ + emit(Stmt::assign( + rep->expr(ci), + Expr::fn(indexedName("$fpext", {Naming::HALF_TYPE, retT}), + {Expr::id(Naming::RMODE_VAR), + Expr::fn(indexedName("$bitcast", {argT, Naming::HALF_TYPE}), + rep->expr(ci->getArgOperand(0)))}))); + }, {&SmackOptions::FloatEnabled, &SmackOptions::BitPrecise}); + + static const auto f16DownCast = conditionalModel([this] (CallInst* ci) { // translation: assume($bitcast.bv16.bvhalf($i) == $fptrunc.bvfloat.bvhalf($rmode, $f)); auto argT = rep->type(ci->getArgOperand(0)->getType()); auto retT = rep->type(ci->getFunctionType()->getReturnType()); - if (SmackOptions::FloatEnabled && SmackOptions::BitPrecise) { - emit(Stmt::assume( - Expr::eq( - Expr::fn(indexedName("$fptrunc", {argT, Naming::HALF_TYPE}), - Expr::id(Naming::RMODE_VAR), - rep->expr(ci->getArgOperand(0))), - Expr::fn(indexedName("$bitcast", {retT, Naming::HALF_TYPE}), - rep->expr(ci))))); - } else - generateUnModeledCall(ci); - }; - - static const auto fma = [this](CallInst* ci) { - if (SmackOptions::FloatEnabled) - emit(Stmt::assign(rep->expr(ci), - Expr::fn(indexedName("$fma", - {rep->type(ci->getFunctionType()->getReturnType())}), - rep->expr(ci->getArgOperand(0)), - rep->expr(ci->getArgOperand(1)), - rep->expr(ci->getArgOperand(2))))); - else - generateUnModeledCall(ci); - }; + emit(Stmt::assume( + Expr::eq( + Expr::fn(indexedName("$fptrunc", {argT, Naming::HALF_TYPE}), + Expr::id(Naming::RMODE_VAR), + rep->expr(ci->getArgOperand(0))), + Expr::fn(indexedName("$bitcast", {retT, Naming::HALF_TYPE}), + rep->expr(ci))))); + }, {&SmackOptions::FloatEnabled, &SmackOptions::BitPrecise}); + + static const auto fma = conditionalModel([this] (CallInst* ci) { + emit(Stmt::assign(rep->expr(ci), + Expr::fn(indexedName("$fma", + {rep->type(ci->getFunctionType()->getReturnType())}), + rep->expr(ci->getArgOperand(0)), + rep->expr(ci->getArgOperand(1)), + rep->expr(ci->getArgOperand(2))))); + }, {&SmackOptions::FloatEnabled}); static const auto bitreverse = [this](Value* arg){ auto width = arg->getType()->getIntegerBitWidth(); @@ -931,64 +939,54 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst& ii) { }; // Count leading zeros - static const auto ctlz = [this](CallInst* ci) { - if (SmackOptions::BitPrecise) { - auto width = ci->getArgOperand(0)->getType()->getIntegerBitWidth(); - auto var = rep->expr(ci->getArgOperand(0)); - - // e.g., if v[32:31] == 1 then 0bv32 else if v[31:30] == 1 then 1bv32 else - // ... else if v[1:0] == 1 then 31bv32 else 32bv32 - const Expr* body = Expr::lit(width, width); - for (unsigned i = 0; i < width; ++i) { - body = Expr::if_then_else(Expr::eq(Expr::bvExtract(var, i+1, i), - Expr::lit(1,1)), - Expr::lit(width-i-1, width), - body); - } + static const auto ctlz = conditionalModel([this] (CallInst* ci) { + auto width = ci->getArgOperand(0)->getType()->getIntegerBitWidth(); + auto var = rep->expr(ci->getArgOperand(0)); - // Handle the is_zero_undef case, i.e. if the flag is set and the argument - // is zero, then the result is undefined. - auto isZeroUndef = rep->expr(ci->getArgOperand(1)); - body = Expr::if_then_else(Expr::and_(Expr::eq(isZeroUndef, Expr::lit(1, 1)), - Expr::eq(var, Expr::lit(0,width))), - rep->expr(ci), // The result is undefined + // e.g., if v[32:31] == 1 then 0bv32 else if v[31:30] == 1 then 1bv32 else + // ... else if v[1:0] == 1 then 31bv32 else 32bv32 + const Expr* body = Expr::lit(width, width); + for (unsigned i = 0; i < width; ++i) { + body = Expr::if_then_else(Expr::eq(Expr::bvExtract(var, i+1, i), + Expr::lit(1,1)), + Expr::lit(width-i-1, width), body); - emit(Stmt::havoc(rep->expr(ci))); - emit(Stmt::assign(rep->expr(ci), body)); } - else - generateUnModeledCall(ci); - }; - // Count trailing zeros - static const auto cttz = [this](CallInst* ci) { - if (SmackOptions::BitPrecise) { - auto width = ci->getArgOperand(0)->getType()->getIntegerBitWidth(); - auto arg = rep->expr(ci->getArgOperand(0)); - - // e.g., if v[1:0] == 1 then 0bv32 else if v[2:1] == 1 then 1bv32 else - // ... else if v[32:31] == 1 then 31bv32 else 32bv32 - const Expr* body = Expr::lit(width, width); - for (unsigned i = width; i > 0; --i) { - body = Expr::if_then_else(Expr::eq(Expr::bvExtract(arg, i, i-1), - Expr::lit(1,1)), - Expr::lit(i-1, width), - body); - } + // Handle the is_zero_undef case, i.e. if the flag is set and the argument + // is zero, then the result is undefined. + auto isZeroUndef = rep->expr(ci->getArgOperand(1)); + body = Expr::if_then_else(Expr::and_(Expr::eq(isZeroUndef, Expr::lit(1, 1)), + Expr::eq(var, Expr::lit(0,width))), + rep->expr(ci), // The result is undefined + body); + emit(Stmt::havoc(rep->expr(ci))); + emit(Stmt::assign(rep->expr(ci), body));}, {&SmackOptions::BitPrecise}); - // Handle the is_zero_undef case, i.e. if the flag is set and the argument - // is zero, then the result is undefined. - auto isZeroUndef = rep->expr(ci->getArgOperand(1)); - body = Expr::if_then_else(Expr::and_(Expr::eq(isZeroUndef, Expr::lit(1, 1)), - Expr::eq(arg, Expr::lit(0,width))), - rep->expr(ci), // The result is undefined + // Count trailing zeros + static const auto cttz = conditionalModel([this] (CallInst* ci) { + auto width = ci->getArgOperand(0)->getType()->getIntegerBitWidth(); + auto arg = rep->expr(ci->getArgOperand(0)); + + // e.g., if v[1:0] == 1 then 0bv32 else if v[2:1] == 1 then 1bv32 else + // ... else if v[32:31] == 1 then 31bv32 else 32bv32 + const Expr* body = Expr::lit(width, width); + for (unsigned i = width; i > 0; --i) { + body = Expr::if_then_else(Expr::eq(Expr::bvExtract(arg, i, i-1), + Expr::lit(1,1)), + Expr::lit(i-1, width), body); - emit(Stmt::havoc(rep->expr(ci))); - emit(Stmt::assign(rep->expr(ci), body)); } - else - generateUnModeledCall(ci); - }; + + // Handle the is_zero_undef case, i.e. if the flag is set and the argument + // is zero, then the result is undefined. + auto isZeroUndef = rep->expr(ci->getArgOperand(1)); + body = Expr::if_then_else(Expr::and_(Expr::eq(isZeroUndef, Expr::lit(1, 1)), + Expr::eq(arg, Expr::lit(0,width))), + rep->expr(ci), // The result is undefined + body); + emit(Stmt::havoc(rep->expr(ci))); + emit(Stmt::assign(rep->expr(ci), body));}, {&SmackOptions::BitPrecise}); // Count the population of 1s in a bv static const auto ctpop = [this](Value* arg) { @@ -1007,56 +1005,41 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst& ii) { }; static const auto assignBvExpr = [this] (std::function exprGenFunc) { - return [this, exprGenFunc] (CallInst* ci) { - if (SmackOptions::BitPrecise) - emit(Stmt::assign(rep->expr(ci), - exprGenFunc(ci->getArgOperand(0)))); - else - generateUnModeledCall(ci); - }; - }; + return conditionalModel([this, exprGenFunc] (CallInst* ci) { + emit(Stmt::assign(rep->expr(ci), + exprGenFunc(ci->getArgOperand(0)))); + }, {&SmackOptions::BitPrecise}); }; static const auto assignUnFPFuncApp = [this] (std::string fnBase) { - return [this, fnBase] (CallInst* ci) { + return conditionalModel([this, fnBase] (CallInst* ci) { // translation: $res := $.bv*($arg1); - if (SmackOptions::FloatEnabled) - emit(Stmt::assign( - rep->expr(ci), - Expr::fn(indexedName(fnBase, - {rep->type(ci->getArgOperand(0)->getType())}), - rep->expr(ci->getArgOperand(0))))); - else - generateUnModeledCall(ci); - }; - }; + emit(Stmt::assign( + rep->expr(ci), + Expr::fn(indexedName(fnBase, + {rep->type(ci->getArgOperand(0)->getType())}), + rep->expr(ci->getArgOperand(0))))); + }, {&SmackOptions::FloatEnabled}); }; static const auto assignBinFPFuncApp = [this] (std::string fnBase) { - return [this, fnBase] (CallInst* ci) { + return conditionalModel([this, fnBase] (CallInst* ci) { // translation: $res := $.bv*($arg1, $arg2); - if (SmackOptions::FloatEnabled) emit(Stmt::assign( rep->expr(ci), Expr::fn(indexedName(fnBase, {rep->type(ci->getFunctionType()->getReturnType())}), {rep->expr(ci->getArgOperand(0)), rep->expr(ci->getArgOperand(1))}))); - else - generateUnModeledCall(ci); - }; - }; + }, {&SmackOptions::FloatEnabled}); }; + + //Expr* -> (CallInst -> Void) static const auto assignRoundFPFuncApp = [this] (const Expr* rMode) { - return [this, rMode] (CallInst* ci) { - // translation: $res := $round.bv*(rmode, $arg1); - if (SmackOptions::FloatEnabled) + return conditionalModel([this, rMode] (CallInst* ci) { emit(Stmt::assign( rep->expr(ci), Expr::fn(indexedName("$round", {rep->type(ci->getFunctionType()->getReturnType())}), {rMode, rep->expr(ci->getArgOperand(0))}))); - else - generateUnModeledCall(ci); - }; - }; + }, {&SmackOptions::FloatEnabled}); }; static const auto identity = [this] (CallInst* ci) { // translation: $res := $arg1 @@ -1064,6 +1047,10 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst& ii) { emit(Stmt::assign(rep->expr(ci), rep->expr(val))); }; + static const auto ignore = [this] (CallInst* ci) { + emit(Stmt::skip()); + }; + // TODO: these functions is consistent with the implementations in math.c, // meaning we can use __builtin_* to implement math.c which is mostly // modeled using __SMACK_code. @@ -1076,6 +1063,7 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst& ii) { {llvm::Intrinsic::ctlz, ctlz}, {llvm::Intrinsic::ctpop, assignBvExpr(ctpop)}, {llvm::Intrinsic::cttz, cttz}, + {llvm::Intrinsic::dbg_declare, ignore}, {llvm::Intrinsic::expect, identity}, {llvm::Intrinsic::fabs, assignUnFPFuncApp("$abs")}, {llvm::Intrinsic::fma, fma}, diff --git a/lib/smack/SmackOptions.cpp b/lib/smack/SmackOptions.cpp index 29f173b33..55e3164d7 100644 --- a/lib/smack/SmackOptions.cpp +++ b/lib/smack/SmackOptions.cpp @@ -14,8 +14,20 @@ const llvm::cl::list SmackOptions::EntryPoints( llvm::cl::value_desc("PROCS") ); -const llvm::cl::opt SmackOptions::Warnings( - "warnings", llvm::cl::desc("Enable warnings.") +const llvm::cl::opt SmackOptions::WarningLevel( + "warn-type", + llvm::cl::desc("Enable certain type of warning messages."), + llvm::cl::values( + clEnumValN(SmackWarnings::WarningLevel::Silent, + "silent", "No warning messages"), + clEnumValN(SmackWarnings::WarningLevel::Unsound, + "unsound", "Enable warnings about unsoundness"), + clEnumValN(SmackWarnings::WarningLevel::Info, + "info", "Enable warnings about unsoundness and translation information")) +); + +const llvm::cl::opt SmackOptions::ColoredWarnings( + "colored-warnings", llvm::cl::desc("Enable colored warning messages.") ); const llvm::cl::opt SmackOptions::MemoryModelDebug( diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 39438c304..02e909ddb 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -11,6 +11,7 @@ #include "smack/Naming.h" #include "smack/Regions.h" #include "smack/Debug.h" +#include "smack/SmackWarnings.h" #include #include @@ -839,7 +840,7 @@ const Expr* SmackRep::expr(const llvm::Value* v, bool isConstIntUnsigned) { } } else if (isa(v)) { - errs() << "warning: ignoring inline asm passed as argument.\n"; + SmackWarnings::warnUnsound("inline asm passed as argument", nullptr, nullptr); return pointerLit(0ULL); } else { @@ -875,6 +876,19 @@ const Expr* SmackRep::cast(unsigned opcode, const llvm::Value* v, const llvm::Ty return Expr::fn(opName(fn, {v->getType(), t}), expr(v)); } +bool SmackRep::isBitwiseOp(llvm::Instruction* I) { + return I->isShift() || I->isBitwiseLogicOp(); +} + +bool SmackRep::isFpArithOp(llvm::Instruction* I) { + return isFpArithOp(I->getOpcode()); +} + +bool SmackRep::isFpArithOp(unsigned opcode) { + return opcode == Instruction::FAdd || opcode == Instruction::FSub + || opcode == Instruction::FMul || opcode == Instruction::FDiv; +} + const Expr* SmackRep::bop(const llvm::ConstantExpr* CE) { return bop(CE->getOpcode(), CE->getOperand(0), CE->getOperand(1), CE->getType()); } @@ -885,8 +899,7 @@ const Expr* SmackRep::bop(const llvm::BinaryOperator* BO) { const Expr* SmackRep::bop(unsigned opcode, const llvm::Value* lhs, const llvm::Value* rhs, const llvm::Type* t) { std::string fn = Naming::INSTRUCTION_TABLE.at(opcode); - if (opcode == Instruction::FAdd || opcode == Instruction::FSub - || opcode == Instruction::FMul || opcode == Instruction::FDiv) { + if (isFpArithOp(opcode)) { if (SmackOptions::FloatEnabled) { return Expr::fn(opName(fn, {t}), Expr::id(Naming::RMODE_VAR), expr(lhs), expr(rhs)); } else { @@ -1242,10 +1255,8 @@ Decl* SmackRep::memcpyProc(std::string type, unsigned length) { if (no_quantifiers) name = name + "." + std::to_string(length); - else if (SmackOptions::Warnings) - errs() << "warning: memory intrinsic length exceeds threshold (" - << MEMORY_INTRINSIC_THRESHOLD << "); " - << "adding quantifiers.\n"; + SmackWarnings::warnInfo("warning: memory intrinsic length exceeds threshold (" + + std::to_string(MEMORY_INTRINSIC_THRESHOLD) + "adding quantifiers."); s << "procedure " << name << "(" << "M.dst: [ref] " << type << ", " @@ -1305,10 +1316,8 @@ Decl* SmackRep::memsetProc(std::string type, unsigned length) { if (no_quantifiers) name = name + "." + std::to_string(length); - else if (SmackOptions::Warnings) - errs() << "warning: memory intrinsic length exceeds threshold (" - << MEMORY_INTRINSIC_THRESHOLD << "); " - << "adding quantifiers.\n"; + SmackWarnings::warnInfo("warning: memory intrinsic length exceeds threshold (" + + std::to_string(MEMORY_INTRINSIC_THRESHOLD) + "adding quantifiers."); s << "procedure " << name << "(" << "M: [ref] " << type << ", " diff --git a/lib/smack/SmackWarnings.cpp b/lib/smack/SmackWarnings.cpp new file mode 100644 index 000000000..2d360d948 --- /dev/null +++ b/lib/smack/SmackWarnings.cpp @@ -0,0 +1,81 @@ +#include "llvm/Support/raw_ostream.h" +#include "llvm/IR/DebugLoc.h" +#include "llvm/IR/DebugInfoMetadata.h" + +#include "smack/SmackWarnings.h" +#include "smack/SmackOptions.h" + +#include +#include + +namespace smack { +using namespace llvm; + +std::string buildDebugInfo(const Instruction* i) { + std::stringstream ss; + if (i && i->getMetadata("dbg")) { + const DebugLoc DL = i->getDebugLoc(); + auto* scope = cast(DL.getScope()); + + ss << scope->getFilename().str() << ":" << DL.getLine() << ":" << DL.getCol() << ": "; + } + return ss.str(); +} + +bool SmackWarnings::isSufficientWarningLevel(WarningLevel level) { + return SmackOptions::WarningLevel >= level; +} + +SmackWarnings::UnsetFlagsT SmackWarnings::getUnsetFlags(RequiredFlagsT requiredFlags) { + UnsetFlagsT ret; + std::copy_if(requiredFlags.begin(), requiredFlags.end(), std::inserter(ret, ret.begin()), + [](FlagT* flag) {return !*flag;}); + return ret; +} + +std::string SmackWarnings::getFlagStr(UnsetFlagsT flags) { + std::string ret = ""; + for (auto f : flags) + ret += ("--" + f->ArgStr.str() + " "); + return ret; +} + +void SmackWarnings::warnIfUnsound(std::string name, RequiredFlagsT requiredFlags, Block* currBlock, const Instruction* i, bool ignore) { + auto unsetFlags = getUnsetFlags(requiredFlags); + if (unsetFlags.size()) + warnUnsound(name, unsetFlags, currBlock, i, ignore); +} + +void SmackWarnings::warnUnsound(std::string unmodeledOpName, Block* currBlock, const Instruction* i, bool ignore) { + warnUnsound("unmodeled operation " + unmodeledOpName, UnsetFlagsT(), currBlock, i, ignore); +} + +void SmackWarnings::warnUnsound(std::string name, UnsetFlagsT unsetFlags, Block* currBlock, const Instruction* i, bool ignore) { + if (!isSufficientWarningLevel(WarningLevel::Unsound)) + return; + std::string beginning = std::string("llvm2bpl: ") + buildDebugInfo(i); + std::string end = (ignore? "unsoundly ignoring " : "over-approximating ") + name + ";"; + if (currBlock) + currBlock->addStmt(Stmt::comment(beginning + "warning: " + end)); + std::string hint = ""; + if (unsetFlags.size()) + hint = (" try adding flag(s): " + getFlagStr(unsetFlags)); + errs() << beginning; + (SmackOptions::ColoredWarnings? errs().changeColor(raw_ostream::MAGENTA) : errs()) << "warning: "; + (SmackOptions::ColoredWarnings? errs().resetColor() : errs()) << end << hint << "\n"; +} + +void SmackWarnings::warnIfUnsound(std::string name, FlagT& requiredFlag, Block* currBlock, const Instruction* i) { + warnIfUnsound(name, {&requiredFlag}, currBlock, i); +} + +void SmackWarnings::warnIfUnsound(std::string name, FlagT& requiredFlag1, FlagT& requiredFlag2, Block* currBlock, const Instruction* i) { + warnIfUnsound(name, {&requiredFlag1, &requiredFlag2}, currBlock, i); +} + +void SmackWarnings::warnInfo(std::string info) { + if (!isSufficientWarningLevel(WarningLevel::Info)) + return; + errs() << "warning: " << info << "\n"; +} +} diff --git a/share/smack/top.py b/share/smack/top.py index 8c2e19c72..d00ca7e32 100755 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -110,6 +110,13 @@ def arguments(): noise_group.add_argument('--debug-only', metavar='MODULES', default=None, type=str, help='limit debugging output to given MODULES') + noise_group.add_argument('--warn', default="unsound", + choices=['silent', 'unsound', 'info'], + help='''enable certain type of warning messages + (silent: no warning messages; + unsound: warnings about unsoundness; + info: warnings about unsoundness and translation information) [default: %(default)s]''') + parser.add_argument('-t', '--no-verify', action="store_true", default=False, help='perform only translation, without verification.') @@ -322,7 +329,8 @@ def llvm_to_bpl(args): """Translate the LLVM bitcode file to a Boogie source file.""" cmd = ['llvm2bpl', args.linked_bc_file, '-bpl', args.bpl_file] - cmd += ['-warnings'] + cmd += ['-warn-type', args.warn] + if sys.stdout.isatty(): cmd += ['-colored-warnings'] cmd += ['-source-loc-syms'] for ep in args.entry_points: cmd += ['-entry-points', ep]