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]