diff --git a/.gitmodules b/.gitmodules index fe7950bd7..32ba47b83 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,4 +1,3 @@ [submodule "sea-dsa"] path = sea-dsa url = https://github.com/seahorn/sea-dsa.git - branch = llvm-8.0 diff --git a/.travis.yml b/.travis.yml index 3791b47ce..0ffdfd721 100644 --- a/.travis.yml +++ b/.travis.yml @@ -73,6 +73,6 @@ before_script: - llvm-config --version script: - - ./format/run-clang-format.py -e test/c/basic/transform-out.c -r lib/smack include/smack share/smack/include share/smack/lib test examples + - ./format/run-clang-format.py -r lib/smack include/smack tools share/smack/include share/smack/lib test examples - flake8 test/regtest.py share/smack/ --extend-exclude share/smack/svcomp/,share/smack/reach.py - INSTALL_RUST=1 ./bin/build.sh diff --git a/Doxyfile b/Doxyfile index a23d248f2..9bc8b160c 100644 --- a/Doxyfile +++ b/Doxyfile @@ -5,7 +5,7 @@ #--------------------------------------------------------------------------- DOXYFILE_ENCODING = UTF-8 PROJECT_NAME = smack -PROJECT_NUMBER = 2.5.0 +PROJECT_NUMBER = 2.6.0 PROJECT_BRIEF = "A bounded software verifier." PROJECT_LOGO = OUTPUT_DIRECTORY = docs diff --git a/bin/versions b/bin/versions index 6be059a2c..c71e9e983 100644 --- a/bin/versions +++ b/bin/versions @@ -1,10 +1,10 @@ Z3_VERSION=4.8.8 -CVC4_VERSION=1.7 +CVC4_VERSION=1.8 YICES2_VERSION=2.6.2 -BOOGIE_VERSION=2.6.15 +BOOGIE_VERSION=2.7.15 CORRAL_VERSION=1.0.12 SYMBOOGLIX_COMMIT=ccb2e7f2b3 LOCKPWN_COMMIT=12ba58f1ec -LLVM_SHORT_VERSION=9 -LLVM_FULL_VERSION=9.0.1 -RUST_VERSION=2020-05-21 +LLVM_SHORT_VERSION=10 +LLVM_FULL_VERSION=10.0.1 +RUST_VERSION=2020-08-23 diff --git a/docs/installation.md b/docs/installation.md index 7a7745d00..183e158dd 100644 --- a/docs/installation.md +++ b/docs/installation.md @@ -80,8 +80,8 @@ to Docker's official documentation. SMACK depends on the following projects: -* [LLVM][] version [9.0.1][LLVM-9.0.1] -* [Clang][] version [9.0.1][Clang-9.0.1] +* [LLVM][] version [10.0.1][LLVM-10.0.1] +* [Clang][] version [10.0.1][Clang-10.0.1] * [Boost][] version 1.55 or greater * [Python][] version 3.6.8 or greater * [Ninja][] version 1.5.1 or greater @@ -210,9 +210,9 @@ shell in the `test` directory by executing [CMake]: http://www.cmake.org [Python]: http://www.python.org [LLVM]: http://llvm.org -[LLVM-9.0.1]: http://llvm.org/releases/download.html#9.0.1 +[LLVM-10.0.1]: http://llvm.org/releases/download.html#10.0.1 [Clang]: http://clang.llvm.org -[Clang-9.0.1]: http://llvm.org/releases/download.html#9.0.1 +[Clang-10.0.1]: http://llvm.org/releases/download.html#10.0.1 [Boogie]: https://github.com/boogie-org/boogie [Corral]: https://github.com/boogie-org/corral [Z3]: https://github.com/Z3Prover/z3/ diff --git a/include/smack/Regions.h b/include/smack/Regions.h index d2c1ad0ea..8e783050e 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -6,6 +6,7 @@ #include "seadsa/Graph.hh" #include "llvm/IR/InstVisitor.h" +#include "llvm/Pass.h" using namespace llvm; diff --git a/include/smack/SimplifyLibCalls.h b/include/smack/SimplifyLibCalls.h index 227f7eed3..139d3b242 100644 --- a/include/smack/SimplifyLibCalls.h +++ b/include/smack/SimplifyLibCalls.h @@ -12,7 +12,7 @@ namespace smack { using namespace llvm; -class SimplifyLibCalls : public ModulePass, +class SimplifyLibCalls : public FunctionPass, public InstVisitor { private: bool modified; @@ -20,9 +20,9 @@ class SimplifyLibCalls : public ModulePass, public: static char ID; - SimplifyLibCalls() : ModulePass(ID) {} + SimplifyLibCalls() : FunctionPass(ID) {} virtual void getAnalysisUsage(AnalysisUsage &AU) const; - virtual bool runOnModule(Module &M); + virtual bool runOnFunction(Function &F); void visitCallInst(CallInst &); }; } // namespace smack diff --git a/include/smack/SmackInstGenerator.h b/include/smack/SmackInstGenerator.h index e65db1f5e..f5c137830 100644 --- a/include/smack/SmackInstGenerator.h +++ b/include/smack/SmackInstGenerator.h @@ -68,6 +68,7 @@ class SmackInstGenerator : public llvm::InstVisitor { void visitUnreachableInst(llvm::UnreachableInst &i); void visitBinaryOperator(llvm::BinaryOperator &I); + void visitUnaryOperator(llvm::UnaryOperator &I); void visitExtractElementInst(llvm::ExtractElementInst &I); void visitInsertElementInst(llvm::InsertElementInst &I); diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index 875a6ad90..53043330f 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -85,6 +85,7 @@ class SmackRep { bool isFpArithOp(unsigned opcode); const Expr *bop(unsigned opcode, const llvm::Value *lhs, const llvm::Value *rhs, const llvm::Type *t); + const Expr *uop(const llvm::Value *op); const Expr *cmp(unsigned predicate, const llvm::Value *lhs, const llvm::Value *rhs, bool isUnsigned); const Expr *select(const llvm::Value *condVal, const llvm::Value *trueVal, @@ -147,6 +148,9 @@ class SmackRep { const Expr *bop(const llvm::BinaryOperator *BO); const Expr *bop(const llvm::ConstantExpr *CE); + const Expr *uop(const llvm::UnaryOperator *UO); + const Expr *uop(const llvm::ConstantExpr *CE); + const Expr *cmp(const llvm::CmpInst *I); const Expr *cmp(const llvm::ConstantExpr *CE); diff --git a/include/smack/SplitAggregateValue.h b/include/smack/SplitAggregateValue.h index 98a06362a..b09b1642a 100644 --- a/include/smack/SplitAggregateValue.h +++ b/include/smack/SplitAggregateValue.h @@ -14,13 +14,13 @@ namespace smack { -class SplitAggregateValue : public llvm::BasicBlockPass { +class SplitAggregateValue : public llvm::FunctionPass { public: typedef std::vector> IndexT; typedef std::pair InfoT; static char ID; - SplitAggregateValue() : llvm::BasicBlockPass(ID) {} - virtual bool runOnBasicBlock(llvm::BasicBlock &BB); + SplitAggregateValue() : llvm::FunctionPass(ID) {} + virtual bool runOnFunction(llvm::Function &F); private: llvm::Value *splitAggregateLoad(llvm::LoadInst *li, std::vector &info, diff --git a/include/utils/InitializePasses.h b/include/utils/InitializePasses.h new file mode 100644 index 000000000..faf799910 --- /dev/null +++ b/include/utils/InitializePasses.h @@ -0,0 +1,13 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// +#ifndef UTILS_INITIALIZEPASSES_H +#define UTILS_INITIALIZEPASSES_H + +#include "llvm/InitializePasses.h" + +namespace llvm { +void initializeDevirtualizePass(PassRegistry &Registry); +} // end namespace llvm + +#endif // UTILS_INITIALIZEPASSES_H diff --git a/lib/smack/AddTiming.cpp b/lib/smack/AddTiming.cpp index ad1eb2a40..7cc074857 100644 --- a/lib/smack/AddTiming.cpp +++ b/lib/smack/AddTiming.cpp @@ -28,6 +28,7 @@ #include "llvm/IR/IntrinsicInst.h" #include "llvm/IR/Value.h" #include "llvm/Pass.h" +#include "llvm/Support/Alignment.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" @@ -186,7 +187,8 @@ unsigned AddTiming::getInstructionCost(const Instruction *I) const { Type *ValTy = SI->getValueOperand()->getType(); assert(!ValTy->isStructTy() && "Timing annotations do not currently work for struct sized stores"); - return TTI->getMemoryOpCost(I->getOpcode(), ValTy, SI->getAlignment(), + return TTI->getMemoryOpCost(I->getOpcode(), ValTy, + MaybeAlign(SI->getAlignment()), SI->getPointerAddressSpace()); } case Instruction::Load: { @@ -194,7 +196,7 @@ unsigned AddTiming::getInstructionCost(const Instruction *I) const { assert(!I->getType()->isStructTy() && "Timing annotations do not currently work for struct sized loads"); return TTI->getMemoryOpCost(I->getOpcode(), I->getType(), - LI->getAlignment(), + MaybeAlign(LI->getAlignment()), LI->getPointerAddressSpace()); } case Instruction::ZExt: diff --git a/lib/smack/Debug.cpp b/lib/smack/Debug.cpp index 1d12f49bd..4a3c3d06d 100644 --- a/lib/smack/Debug.cpp +++ b/lib/smack/Debug.cpp @@ -42,7 +42,8 @@ void setCurrentDebugTypes(const char **Types, unsigned Count) { static ::llvm::cl::opt Debug("debug", cl::desc("Enable debug output"), - cl::Hidden, cl::location(DebugFlag)); + cl::Hidden, + cl::location(smack::DebugFlag)); namespace { @@ -50,7 +51,7 @@ struct DebugOnlyOpt { void operator=(const std::string &Val) const { if (Val.empty()) return; - DebugFlag = true; + smack::DebugFlag = true; SmallVector dbgTypes; StringRef(Val).split(dbgTypes, ',', -1, false); for (auto dbgType : dbgTypes) diff --git a/lib/smack/ExtractContracts.cpp b/lib/smack/ExtractContracts.cpp index f0cc0b00c..4d8b81b63 100644 --- a/lib/smack/ExtractContracts.cpp +++ b/lib/smack/ExtractContracts.cpp @@ -229,7 +229,8 @@ bool ExtractContracts::runOnModule(Module &M) { } if (!contractBlocks.empty()) { - auto *newF = CodeExtractor(contractBlocks).extractCodeRegion(); + auto *newF = CodeExtractor(contractBlocks) + .extractCodeRegion(CodeExtractorAnalysisCache(*F)); std::vector Is; for (auto V : newF->users()) @@ -258,7 +259,8 @@ bool ExtractContracts::runOnModule(Module &M) { for (auto const &entry : invariantBlocks) { auto BBs = entry.second; - auto *newF = CodeExtractor(BBs).extractCodeRegion(); + auto *newF = + CodeExtractor(BBs).extractCodeRegion(CodeExtractorAnalysisCache(*F)); std::vector Is; for (auto V : newF->users()) diff --git a/lib/smack/Naming.cpp b/lib/smack/Naming.cpp index 18d437e23..f4dd71358 100644 --- a/lib/smack/Naming.cpp +++ b/lib/smack/Naming.cpp @@ -121,6 +121,7 @@ const std::map Naming::INSTRUCTION_TABLE{ {Instruction::FMul, "$fmul"}, {Instruction::FDiv, "$fdiv"}, {Instruction::FRem, "$frem"}, + {Instruction::FNeg, "$fneg"}, {Instruction::ShuffleVector, "$shufflevector"}, {Instruction::InsertElement, "$insertelement"}, {Instruction::ExtractElement, "$extractelement"}}; diff --git a/lib/smack/Prelude.cpp b/lib/smack/Prelude.cpp index bcb867aed..b72839886 100644 --- a/lib/smack/Prelude.cpp +++ b/lib/smack/Prelude.cpp @@ -980,7 +980,7 @@ void IntOpGen::generateMemOps(std::stringstream &s) const { } else { auto loadBody = prelude.mapSelExpr(0); auto storeBody = prelude.mapUpdExpr(0, Expr::bvExtract(valExpr, 8, 0)); - for (unsigned i = 1; i> 3; ++i) { + for (unsigned i = 1; i < (size >> 3); ++i) { unsigned lowerIdx = i << 3; unsigned upperIdx = lowerIdx + 8; loadBody = Expr::bvConcat(prelude.mapSelExpr(i), loadBody); @@ -1333,6 +1333,7 @@ const Attr *FpOp::fpAttrFunc(std::string opName) { {"fdiv", "fp.div"}, {"frem", "fp.rem"}, {"fma", "fp.fma"}, + {"fneg", "fp.neg"}, {"isnormal", "fp.isNormal"}, {"issubnormal", "fp.isSubnormal"}, {"iszero", "fp.isZero"}, @@ -1388,7 +1389,7 @@ void FpOpGen::generateArithOps(std::stringstream &s) const { {"abs", 1, false}, {"round", 1, true}, {"sqrt", 1, true}, {"fadd", 2, true}, {"fsub", 2, true}, {"fmul", 2, true}, {"fdiv", 2, true}, {"frem", 2, false}, {"min", 2, false}, - {"max", 2, false}, {"fma", 3, true}}; + {"max", 2, false}, {"fma", 3, true}, {"fneg", 1, false}}; for (auto &f : fpArithOps) { if (SmackOptions::FloatEnabled) diff --git a/lib/smack/SimplifyLibCalls.cpp b/lib/smack/SimplifyLibCalls.cpp index 605f161f6..8400fc13e 100644 --- a/lib/smack/SimplifyLibCalls.cpp +++ b/lib/smack/SimplifyLibCalls.cpp @@ -28,15 +28,16 @@ void SimplifyLibCalls::getAnalysisUsage(AnalysisUsage &AU) const { AU.addRequired(); } -bool SimplifyLibCalls::runOnModule(Module &M) { +bool SimplifyLibCalls::runOnFunction(Function &F) { modified = false; simplifier = new LibCallSimplifier( - M.getDataLayout(), &getAnalysis().getTLI(), + F.getParent()->getDataLayout(), + &getAnalysis().getTLI(F), getAnalysis().getORE(), &getAnalysis().getBFI(), &getAnalysis().getPSI()); if (simplifier) - visit(M); + visit(F); return modified; } diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index f8ca4c702..e3d147a55 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -200,7 +200,7 @@ void SmackInstGenerator::generatePhiAssigns(llvm::Instruction &ti) { llvm::PHINode *phi = llvm::cast(s); if (llvm::Value *v = phi->getIncomingValueForBlock(block)) { - v = v->stripPointerCasts(); + v = v->stripPointerCastsAndAliases(); lhs.push_back(rep->expr(phi)); rhs.push_back(rep->expr(v)); } @@ -372,6 +372,20 @@ void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator &I) { emit(Stmt::assign(rep->expr(&I), E)); } +/******************************************************************************/ +/* UNARY OPERATIONS */ +/******************************************************************************/ + +void SmackInstGenerator::visitUnaryOperator(llvm::UnaryOperator &I) { + assert(I.getOpcode() == Instruction::FNeg && !isa(I.getType()) && + "Unsupported unary operation!"); + processInstruction(I); + SmackWarnings::warnIfUnsound(std::string("floating-point arithmetic ") + + I.getOpcodeName(), + SmackOptions::FloatEnabled, currBlock, &I); + emit(Stmt::assign(rep->expr(&I), rep->uop(&I))); +} + /******************************************************************************/ /* VECTOR OPERATIONS */ /******************************************************************************/ @@ -505,7 +519,7 @@ void SmackInstGenerator::visitLoadInst(llvm::LoadInst &li) { void SmackInstGenerator::visitStoreInst(llvm::StoreInst &si) { processInstruction(si); const llvm::Value *P = si.getPointerOperand(); - const llvm::Value *V = si.getValueOperand()->stripPointerCasts(); + const llvm::Value *V = si.getValueOperand()->stripPointerCastsAndAliases(); assert(!V->getType()->isAggregateType() && "Unexpected store value."); if (isa(V->getType())) { @@ -635,7 +649,7 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) { Function *f = ci.getCalledFunction(); if (!f) { assert(ci.getCalledValue() && "Called value is null"); - f = cast(ci.getCalledValue()->stripPointerCasts()); + f = cast(ci.getCalledValue()->stripPointerCastsAndAliases()); } std::string name = f->hasName() ? f->getName() : ""; @@ -834,7 +848,7 @@ void SmackInstGenerator::visitDbgValueInst(llvm::DbgValueInst &dvi) { auto currInst = std::prev(nextInst); if (currInst != dvi.getParent()->begin()) { const Instruction &pi = *std::prev(currInst); - V = V->stripPointerCasts(); + V = V->stripPointerCastsAndAliases(); if (!llvm::isa(&pi) && V == llvm::dyn_cast(&pi)) emit(recordProcedureCall( diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 40dfe0bef..e78b5513b 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -355,7 +355,7 @@ const Stmt *SmackRep::valueAnnotation(const CallInst &CI) { assert(CI.getNumArgOperands() > 0 && "Expected at least one argument."); assert(CI.getNumArgOperands() <= 2 && "Expected at most two arguments."); - const Value *V = CI.getArgOperand(0)->stripPointerCasts(); + const Value *V = CI.getArgOperand(0)->stripPointerCastsAndAliases(); if (CI.getNumArgOperands() == 1) { name = indexedName(Naming::VALUE_PROC, {type(V->getType())}); @@ -788,7 +788,7 @@ const Expr *SmackRep::expr(const llvm::Value *v, bool isConstIntUnsigned) { using namespace llvm; if (isa(v)) { - v = v->stripPointerCasts(); + v = v->stripPointerCastsAndAliases(); } if (isa(v)) { @@ -924,6 +924,19 @@ const Expr *SmackRep::bop(unsigned opcode, const llvm::Value *lhs, return Expr::fn(opName(fn, {t}), expr(lhs), expr(rhs)); } +const Expr *SmackRep::uop(const llvm::ConstantExpr *CE) { + return uop(CE->getOperand(0)); +} + +const Expr *SmackRep::uop(const llvm::UnaryOperator *UO) { + return uop(UO->getOperand(0)); +} + +const Expr *SmackRep::uop(const llvm::Value *op) { + std::string fn = Naming::INSTRUCTION_TABLE.at(Instruction::FNeg); + return Expr::fn(opName(fn, {op->getType()}), expr(op)); +} + const Expr *SmackRep::cmp(const llvm::CmpInst *I) { return cmp(I->getPredicate(), I->getOperand(0), I->getOperand(1), I->isUnsigned()); diff --git a/lib/smack/SmackWarnings.cpp b/lib/smack/SmackWarnings.cpp index 8746c10e3..b7bc2b1cd 100644 --- a/lib/smack/SmackWarnings.cpp +++ b/lib/smack/SmackWarnings.cpp @@ -38,8 +38,12 @@ SmackWarnings::getUnsetFlags(RequiredFlagsT requiredFlags) { std::string SmackWarnings::getFlagStr(UnsetFlagsT flags) { std::string ret = ""; - for (auto f : flags) - ret += ("--" + f->ArgStr.str() + " "); + for (auto f : flags) { + if (f->ArgStr.str() == "bit-precise") + ret += ("--integer-encoding=bit-vector "); + else + ret += ("--" + f->ArgStr.str() + " "); + } return ret; } diff --git a/lib/smack/SplitAggregateValue.cpp b/lib/smack/SplitAggregateValue.cpp index bd9243901..0c27514f9 100644 --- a/lib/smack/SplitAggregateValue.cpp +++ b/lib/smack/SplitAggregateValue.cpp @@ -22,50 +22,52 @@ std::vector getSeconds(SplitAggregateValue::IndexT lst) { return ret; } -bool SplitAggregateValue::runOnBasicBlock(BasicBlock &BB) { - std::vector toRemove; - LLVMContext &C = BB.getContext(); - for (Instruction &I : BB) { - IndexT idx; - std::vector info; - if (LoadInst *li = dyn_cast(&I)) { - if (li->getType()->isAggregateType()) { - visitAggregateValue(nullptr, li->getType(), idx, info, C); - IRBuilder<> irb(li); - li->replaceAllUsesWith(splitAggregateLoad(li, info, irb)); - toRemove.push_back(li); - } - } else if (StoreInst *si = dyn_cast(&I)) { - Value *V = si->getValueOperand(); - if (V->getType()->isAggregateType()) { - visitAggregateValue(dyn_cast_or_null(V), V->getType(), idx, - info, C); - IRBuilder<> irb(si); - splitAggregateStore(si, info, irb); - toRemove.push_back(si); - } - } else if (ReturnInst *ri = dyn_cast(&I)) { - Value *V = ri->getReturnValue(); - if (isConstantAggregate(V)) { - visitAggregateValue(cast(V), V->getType(), idx, info, C); - splitConstantReturn(ri, info); - } - } else if (CallInst *ci = dyn_cast(&I)) { - for (unsigned i = 0; i < ci->getNumArgOperands(); ++i) { - Value *arg = ci->getArgOperand(i); - if (isConstantAggregate(arg)) { - info.clear(); - idx.clear(); - visitAggregateValue(cast(arg), arg->getType(), idx, info, - C); - splitConstantArg(ci, i, info); +bool SplitAggregateValue::runOnFunction(Function &F) { + for (auto &BB : F) { + std::vector toRemove; + LLVMContext &C = BB.getContext(); + for (Instruction &I : BB) { + IndexT idx; + std::vector info; + if (LoadInst *li = dyn_cast(&I)) { + if (li->getType()->isAggregateType()) { + visitAggregateValue(nullptr, li->getType(), idx, info, C); + IRBuilder<> irb(li); + li->replaceAllUsesWith(splitAggregateLoad(li, info, irb)); + toRemove.push_back(li); + } + } else if (StoreInst *si = dyn_cast(&I)) { + Value *V = si->getValueOperand(); + if (V->getType()->isAggregateType()) { + visitAggregateValue(dyn_cast_or_null(V), V->getType(), idx, + info, C); + IRBuilder<> irb(si); + splitAggregateStore(si, info, irb); + toRemove.push_back(si); + } + } else if (ReturnInst *ri = dyn_cast(&I)) { + Value *V = ri->getReturnValue(); + if (isConstantAggregate(V)) { + visitAggregateValue(cast(V), V->getType(), idx, info, C); + splitConstantReturn(ri, info); + } + } else if (CallInst *ci = dyn_cast(&I)) { + for (unsigned i = 0; i < ci->getNumArgOperands(); ++i) { + Value *arg = ci->getArgOperand(i); + if (isConstantAggregate(arg)) { + info.clear(); + idx.clear(); + visitAggregateValue(cast(arg), arg->getType(), idx, info, + C); + splitConstantArg(ci, i, info); + } } } } - } - for (auto &i : toRemove) - i->eraseFromParent(); + for (auto &i : toRemove) + i->eraseFromParent(); + } return true; } diff --git a/lib/utils/Devirt.cpp b/lib/utils/Devirt.cpp index 5722830db..ecb281a10 100644 --- a/lib/utils/Devirt.cpp +++ b/lib/utils/Devirt.cpp @@ -12,6 +12,8 @@ #include "utils/Devirt.h" #include "smack/Debug.h" +#include "seadsa/InitializePasses.hh" +#include "utils/InitializePasses.h" #include "llvm/Support/CommandLine.h" #include "llvm/ADT/Statistic.h" @@ -21,17 +23,10 @@ using namespace llvm; -// Pass ID variable -char Devirtualize::ID = 0; - // Pass statistics STATISTIC(FuncAdded, "Number of bounce functions added"); STATISTIC(CSConvert, "Number of call sites converted"); -// Pass registration -RegisterPass -Z ("devirt", "Devirtualize indirect function calls"); - const bool SKIP_INCOMPLETE_NODES = false; // @@ -173,7 +168,7 @@ Devirtualize::findInCache (const CallSite & CS, // Check the type of the function pointer and the argumentsa PointerType* PT = dyn_cast(bounceFunc->arg_begin()->getType()); assert(PT); - if (CS.getCalledValue()->stripPointerCasts()->getType() != PT) + if (CS.getCalledValue()->stripPointerCastsAndAliases()->getType() != PT) continue; FunctionType* FT = dyn_cast(PT->getElementType()); @@ -461,7 +456,7 @@ Devirtualize::processCallSite (CallSite &CS) { // First, determine if this is a direct call. If so, then just ignore it. // Value * CalledValue = CS.getCalledValue(); - if (isa(CalledValue->stripPointerCasts())) + if (isa(CalledValue->stripPointerCastsAndAliases())) return; // @@ -519,3 +514,12 @@ Devirtualize::runOnModule (Module & M) { // return true; } + +// Pass ID variable +char Devirtualize::ID = 0; + +using namespace seadsa; +// Pass registration +INITIALIZE_PASS_BEGIN(Devirtualize, "devirt", "Devirtualize indirect function calls", false, false) +INITIALIZE_PASS_DEPENDENCY(CompleteCallGraph) +INITIALIZE_PASS_END(Devirtualize, "devirt", "Devirtualize indirect function calls", false, false) diff --git a/sea-dsa b/sea-dsa index 39ddfbfcb..77fa9ef09 160000 --- a/sea-dsa +++ b/sea-dsa @@ -1 +1 @@ -Subproject commit 39ddfbfcbc58287bca76bc7ff2539f7e97635eac +Subproject commit 77fa9ef0935aee4085a5ecdf52f67fcf2f87513b diff --git a/share/smack/reach.py b/share/smack/reach.py index 3aef8c852..b06b7462a 100755 --- a/share/smack/reach.py +++ b/share/smack/reach.py @@ -11,7 +11,7 @@ from smackgen import * from smackverify import * -VERSION = '2.5.0' +VERSION = '2.6.0' def reachParser(): diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py index c520e6bca..2272df8e0 100644 --- a/share/smack/svcomp/utils.py +++ b/share/smack/svcomp/utils.py @@ -25,13 +25,13 @@ def svcomp_frontend(input_file, args): svcomp_check_property(args) # fix: disable float filter for memory safety benchmarks - if not (args.memory_safety or args.only_check_memcleanup): + if not ('memory-safety' in args.check or 'memleak' in args.check): # test bv and executable benchmarks file_type, executable = filters.svcomp_filter(args.input_files[0]) if file_type == 'bitvector': args.integer_encoding = 'bit-vector' args.pointer_encoding = 'bit-vector' - if file_type == 'float' and not args.integer_overflow: + if file_type == 'float' and not 'integer-overflow' in args.check: args.float = True args.integer_encoding = 'bit-vector' with open(input_file, "r") as sf: @@ -46,6 +46,9 @@ def svcomp_frontend(input_file, args): args.integer_encoding = 'bit-vector' #args.pointer_encoding = 'bit-vector' + if 'memory-safety' in args.check or 'memleak' in args.check or 'integer-overflow' in args.check: + args.strings = True + name, ext = os.path.splitext(os.path.basename(args.input_files[0])) svcomp_process_file(args, name, ext) @@ -66,24 +69,21 @@ def svcomp_frontend(input_file, args): libs = set() smack.top.link_bc_files([bc],libs,args) - if args.only_check_memcleanup: - args.memory_safety = False def svcomp_check_property(args): - args.only_check_memcleanup = False # Check if property is vanilla reachability, and return unknown otherwise if args.svcomp_property: with open(args.svcomp_property, "r") as f: prop = f.read() if "valid-deref" in prop: - args.memory_safety = True + args.check = ['memory-safety'] elif "valid-memcleanup" in prop: - args.memory_safety = True - args.only_check_memcleanup = True + args.check = ['memleak'] elif "overflow" in prop: - args.integer_overflow = True + args.check = ['integer-overflow'] elif not "reach_error" in prop: - sys.exit(smack.top.results(args)['unknown']) + print(smack.top.results(args)['unknown'][0]) + sys.exit(smack.top.results(args)['unknown'][1]) def svcomp_process_file(args, name, ext): args.orig_files = list(args.input_files) @@ -98,14 +98,14 @@ def svcomp_process_file(args, name, ext): s = re.sub(r'static\s+char\s+dir\[42\];\s+for\(int\s+i=0;\s+i<42;\s+\+\+i\)\s+dir\[i\]\s+=\s+__VERIFIER_nondet_char\(\);\s+dir\[41\]\s+=\s+\'\\0\';', r'static char dir[3];\n dir[0] = __VERIFIER_nondet_char();\n dir[1] = __VERIFIER_nondet_char();\n dir[2] = 0;', s) s = re.sub(r'__VERIFIER_assume\(i < 16\);', r'__VERIFIER_assume(i >= 0 && i < 16);', s) - if args.memory_safety and not 'argv=malloc' in s: + if 'memory-safety' in args.check and not 'argv=malloc' in s: s = re.sub(r'typedef long unsigned int size_t', r'typedef unsigned int size_t', s) - elif args.memory_safety and re.search(r'getopt32\([^,)]+,[^,)]+,[^.)]+\);', s): + elif 'memory-safety' in args.check and re.search(r'getopt32\([^,)]+,[^,)]+,[^.)]+\);', s): if not args.quiet: print("Stumbled upon a benchmark that requires precise handling of vararg\n") while (True): pass - elif args.memory_safety and ('count is too big' in s or 'pdRfilsLHarPv' in s or 'rnugG' in s): + elif 'memory-safety' in args.check and ('count is too big' in s or 'pdRfilsLHarPv' in s or 'rnugG' in s): if not args.quiet: print("Stumbled upon a benchmark that contains undefined behavior\n") while (True): @@ -113,7 +113,7 @@ def svcomp_process_file(args, name, ext): if 'argv=malloc' in s: # args.integer_encoding = 'bit-vector' - if args.integer_overflow and ('unsigned int d = (unsigned int)((signed int)(unsigned char)((signed int)*q | (signed int)(char)32) - 48);' in s or 'bb_ascii_isalnum' in s or 'ptm=localtime' in s or '0123456789.' in s): + if 'integer-overflow' in args.check and ('unsigned int d = (unsigned int)((signed int)(unsigned char)((signed int)*q | (signed int)(char)32) - 48);' in s or 'bb_ascii_isalnum' in s or 'ptm=localtime' in s or '0123456789.' in s): args.integer_encoding = 'bit-vector' args.pointer_encoding = 'bit-vector' @@ -167,7 +167,8 @@ def is_stack_benchmark(args, csource): "arr[194]" in csource or "if(1)" in csource or "alloca(10" in csource or "p[0] = 2;" in csource): if not args.quiet: print("Stumbled upon a stack-based memory safety benchmark\n") - sys.exit(smack.top.results(args)['unknown']) + print(smack.top.results(args)['unknown'][0]) + sys.exit(smack.top.results(args)['unknown'][1]) def inject_assert_false(args): with open(args.bpl_file, 'r') as bf: @@ -180,38 +181,42 @@ def verify_bpl_svcomp(args): """Verify the Boogie source file using SVCOMP-tuned heuristics.""" heurTrace = "\n\nHeuristics Info:\n" - if not args.memory_safety and not args.only_check_memcleanup and not args.integer_overflow: + if not 'memory-safety' in args.check and not 'memleak' in args.check and not 'integer-overflow' in args.check: inject_assert_false(args) - if args.memory_safety: - if not (args.only_check_valid_deref or args.only_check_valid_free or args.only_check_memleak): + if 'memory-safety' in args.check: + if len(args.check) == 1: heurTrace = "engage valid deference checks.\n" - args.only_check_valid_deref = True + args.check.pop() + args.check.append('valid-deref') args.prop_to_check = 'valid-deref' args.bpl_with_all_props = smack.top.temporary_file(os.path.splitext(os.path.basename(args.bpl_file))[0], '.bpl', args) copyfile(args.bpl_file, args.bpl_with_all_props) - smack.top.property_selection(args) - elif args.only_check_valid_deref: + smack.top.memsafety_subproperty_selection(args) + args.check.append('memory-safety') + elif 'valid-deref' in args.check: heurTrace = "engage valid free checks.\n" - args.only_check_valid_free = True + args.check.pop() + args.check.pop() args.prop_to_check = 'valid-free' - args.only_check_valid_deref = False + args.check.append('valid-free') args.bpl_file = smack.top.temporary_file(os.path.splitext(os.path.basename(args.bpl_file))[0], '.bpl', args) copyfile(args.bpl_with_all_props, args.bpl_file) - smack.top.property_selection(args) - elif args.only_check_valid_free: + smack.top.memsafety_subproperty_selection(args) + args.check.append('memory-safety') + elif 'valid-free' in args.check: heurTrace = "engage memleak checks.\n" - args.only_check_memleak = True + args.check.pop() + args.check.pop() args.prop_to_check = 'memleak' - args.only_check_valid_free = False + args.check.append('memleak') args.bpl_file = smack.top.temporary_file(os.path.splitext(os.path.basename(args.bpl_file))[0], '.bpl', args) copyfile(args.bpl_with_all_props, args.bpl_file) - smack.top.property_selection(args) - elif args.only_check_memcleanup: + smack.top.memsafety_subproperty_selection(args) + args.check.append('memory-safety') + elif 'memleak' in args.check: heurTrace = "engage memcleanup checks.\n" - args.only_check_memleak = True - smack.top.property_selection(args) - args.only_check_memleak = False + smack.top.memsafety_subproperty_selection(args) # If pthreads found, perform lock set analysis if args.pthread: @@ -234,17 +239,19 @@ def verify_bpl_svcomp(args): with open(args.input_files[0], "r") as f: csource = f.read() - if args.memory_safety: + if 'memory-safety' in args.check: is_stack_benchmark(args, csource) else: if "angleInRadian" in csource: if not args.quiet: print("Stumbled upon trigonometric function is float benchmark\n") - sys.exit(smack.top.results(args)['unknown']) + print(smack.top.results(args)['unknown'][0]) + sys.exit(smack.top.results(args)['unknown'][1]) elif "copysign(1" in csource: if not args.quiet: print("Stumbled upon tricky float benchmark\n") - sys.exit(smack.top.results(args)['unknown']) + print(smack.top.results(args)['unknown'][0]) + sys.exit(smack.top.results(args)['unknown'][1]) is_buggy_driver_benchmark(args, bpl) if args.pthread: @@ -257,7 +264,7 @@ def verify_bpl_svcomp(args): corral_command += ["/cooperative"] else: corral_command += ["/k:1"] - if not (args.memory_safety or args.integer_encoding == 'bit-vector' or args.only_check_memcleanup): + if not ('memory-safety' in args.check or args.integer_encoding == 'bit-vector' or 'memleak' in args.check): if not ("dll_create" in csource or "sll_create" in csource or "changeMethaneLevel" in csource): corral_command += ["/di"] @@ -266,7 +273,8 @@ def verify_bpl_svcomp(args): heurTrace += "We are not modeling strcpy - aborting\n" if not args.quiet: print((heurTrace + "\n")) - sys.exit(smack.top.results(args)['unknown']) + print(smack.top.results(args)['unknown'][0]) + sys.exit(smack.top.results(args)['unknown'][1]) # Setting good loop unroll bound based on benchmark class loopUnrollBar = 8 @@ -309,16 +317,16 @@ def verify_bpl_svcomp(args): elif "printf_false-unreach-call" in bpl or "echo_true-no-overflow" in bpl: heurTrace += "BusyBox benchmark detected. Setting loop unroll bar to 11.\n" loopUnrollBar = 11 - elif args.memory_safety and "__main($i0" in bpl: + elif 'memory-safety' in args.check and "__main($i0" in bpl: heurTrace += "BusyBox memory safety benchmark detected. Setting loop unroll bar to 4.\n" loopUnrollBar = 4 - elif args.integer_overflow and "__main($i0" in bpl: + elif 'integer-overflow' in args.check and "__main($i0" in bpl: heurTrace += "BusyBox overflows benchmark detected. Setting loop unroll bar to 40.\n" loopUnrollBar = 40 - elif args.integer_overflow and ("jain" in bpl or "TerminatorRec02" in bpl or "NonTerminationSimple" in bpl): + elif 'integer-overflow' in args.check and ("jain" in bpl or "TerminatorRec02" in bpl or "NonTerminationSimple" in bpl): heurTrace += "Infinite loop in overflow benchmark. Setting loop unroll bar to INT_MAX.\n" loopUnrollBar = 2**31 - 1 - elif args.integer_overflow and ("(x != 0)" in csource or "(z > 0)" in csource or "(max > 0)" in csource or + elif 'integer-overflow' in args.check and ("(x != 0)" in csource or "(z > 0)" in csource or "(max > 0)" in csource or "(k < N)" in csource or "partial_sum" in csource): heurTrace += "Large overflow benchmark. Setting loop unroll bar to INT_MAX.\n" loopUnrollBar = 2**31 - 1 @@ -333,7 +341,7 @@ def verify_bpl_svcomp(args): heurTrace += "No quantifiers detected. Setting z3 relevancy to 0.\n" corral_command += ["/bopt:proverOpt:O:smt.relevancy=0"] - if args.memory_safety: + if 'memory-safety' in args.check: if args.prop_to_check == 'valid-deref': if "memleaks_test12_false-valid-free" in bpl: time_limit = 10 @@ -363,7 +371,7 @@ def verify_bpl_svcomp(args): if not args.quiet: error = smack.top.error_trace(verifier_output, args) print(error) - if args.memory_safety: + if 'memory-safety' in args.check: heurTrace += (args.prop_to_check + "has errors\n") if args.prop_to_check == 'valid-free': if args.valid_deref_check_result != 'verified': @@ -399,16 +407,18 @@ def verify_bpl_svcomp(args): heurTrace += "Oops, execution result says {0}.\n".format(execution_result) if not args.quiet: print((heurTrace + "\n")) - sys.exit(smack.top.results(args)['unknown']) + print(smack.top.results(args)['unknown'][0]) + sys.exit(smack.top.results(args)['unknown'][1]) random_test_result = random_test(args, result) if random_test_result == 'false' or random_test_result == 'unknown': heurTrace += "Oops, random testing says {0}.\n".format(random_test_result) if not args.quiet: print((heurTrace + "\n")) - sys.exit(smack.top.results(args)['unknown']) + print(smack.top.results(args)['unknown'][0]) + sys.exit(smack.top.results(args)['unknown'][1]) if not args.quiet: print((heurTrace + "\n")) - if args.memory_safety: + if 'memory-safety' in args.check: heurTrace += (args.prop_to_check + "is verified\n") if args.prop_to_check == 'valid-deref': args.valid_deref_check_result = 'verified' @@ -418,11 +428,13 @@ def verify_bpl_svcomp(args): if args.valid_deref_check_result == 'timeout': force_timeout() else: - sys.exit(smack.top.results(args)[args.valid_deref_check_result]) + print(smack.top.results(args)[args.valid_deref_check_result][0]) + sys.exit(smack.top.results(args)[args.valid_deref_check_result][1]) verify_bpl_svcomp(args) else: write_error_file(args, 'verified', verifier_output) - sys.exit(smack.top.results(args)['verified']) + print(smack.top.results(args)['verified'][0]) + sys.exit(smack.top.results(args)['verified'][1]) else: heurTrace += "Only unrolled " + str(unrollMax) + " times.\n" heurTrace += "Insufficient unrolls to consider 'verified'. " @@ -430,7 +442,7 @@ def verify_bpl_svcomp(args): if not args.quiet: print((heurTrace + "\n")) sys.stdout.flush() - if args.memory_safety: + if 'memory-safety' in args.check: heurTrace += (args.prop_to_check + " times out\n") if args.prop_to_check == 'valid-deref': args.valid_deref_check_result = 'timeout' @@ -441,7 +453,8 @@ def verify_bpl_svcomp(args): if args.valid_deref_check_result == 'timeout': force_timeout() else: - sys.exit(smack.top.results(args)[args.valid_deref_check_result]) + print(smack.top.results(args)[args.valid_deref_check_result][0]) + sys.exit(smack.top.results(args)[args.valid_deref_check_result][1]) verify_bpl_svcomp(args) else: force_timeout() @@ -451,7 +464,7 @@ def verify_bpl_svcomp(args): heurTrace += "Normal inlining returned 'unknown'. See errors above.\n" if not args.quiet: print((heurTrace + "\n")) - if args.memory_safety and result == 'verified': + if 'memory-safety' in args.check and result == 'verified': heurTrace += (args.prop_to_check + " is verified\n") if args.prop_to_check == 'valid-deref': args.valid_deref_check_result = 'verified' @@ -461,14 +474,16 @@ def verify_bpl_svcomp(args): if args.valid_deref_check_result == 'timeout': force_timeout() else: - sys.exit(smack.top.results(args)[args.valid_deref_check_result]) + print(smack.top.results(args)[args.valid_deref_check_result][0]) + sys.exit(smack.top.results(args)[args.valid_deref_check_result][1]) verify_bpl_svcomp(args) else: write_error_file(args, result, verifier_output) - if args.only_check_memcleanup and result == 'invalid-memtrack': + if 'memleak' in args.check and result == 'invalid-memtrack': sys.exit('SMACK found an error: memory cleanup.') else: - sys.exit(smack.top.results(args)[result]) + print(smack.top.results(args)[result][0]) + sys.exit(smack.top.results(args)[result][1]) def write_error_file(args, status, verifier_output): #return diff --git a/share/smack/top.py b/share/smack/top.py index 49ddef237..06343c8be 100755 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -13,7 +13,7 @@ from .replay import replay_error_trace from .frontend import link_bc_files, frontends, languages, extra_libs -VERSION = '2.5.0' +VERSION = '2.6.0' def results(args): @@ -600,7 +600,7 @@ def annotate_bpl(args): def memsafety_subproperty_selection(args): - selected_props = {} + selected_props = set() if 'memory-safety' in args.check: return if 'valid-deref' in args.check: diff --git a/test/c/basic/transform-out.c b/test/c/basic/transform-out.c index d56756fc9..dad17ff34 100644 --- a/test/c/basic/transform-out.c +++ b/test/c/basic/transform-out.c @@ -3,7 +3,9 @@ #include // @expect verified +// clang-format off // @flag --transform-out "sed -e 's/[[:digit:]]* verified, [[:digit:]]* error/1 verified, 0 errors/' -e 's/can fail/no bugs/'" +// clang-format on int main(void) { assert(0); diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp index 0a71fdf65..61427c5c9 100644 --- a/tools/llvm2bpl/llvm2bpl.cpp +++ b/tools/llvm2bpl/llvm2bpl.cpp @@ -24,10 +24,8 @@ #include "llvm/Support/raw_ostream.h" #include "llvm/Target/TargetMachine.h" -#include "utils/Devirt.h" -#include "utils/MergeGEP.h" -#include "utils/SimplifyExtractValue.h" -#include "utils/SimplifyInsertValue.h" +#include "seadsa/InitializePasses.hh" +#include "seadsa/support/RemovePtrToInt.hh" #include "smack/AddTiming.h" #include "smack/BplFilePrinter.h" #include "smack/CodifyStaticInits.h" @@ -42,6 +40,11 @@ #include "smack/SmackOptions.h" #include "smack/SplitAggregateValue.h" #include "smack/VerifierCodeMetadata.h" +#include "utils/Devirt.h" +#include "utils/InitializePasses.h" +#include "utils/MergeGEP.h" +#include "utils/SimplifyExtractValue.h" +#include "utils/SimplifyInsertValue.h" static llvm::cl::opt InputFilename(llvm::cl::Positional, @@ -108,9 +111,9 @@ static TargetMachine *GetTargetMachine(Triple TheTriple, StringRef CPUStr, Reloc::Static, /* was getRelocModel(),*/ None, /* Use default CodeModel */ CodeGenOpt::None /*GetCodeGenOptLevel())*/ - ); -} + ); } +} // namespace int main(int argc, char **argv) { llvm::llvm_shutdown_obj shutdown; // calls llvm_shutdown() on exit @@ -146,13 +149,16 @@ int main(int argc, char **argv) { llvm::initializeAnalysis(Registry); llvm::initializeCodifyStaticInitsPass(Registry); + llvm::initializeDevirtualizePass(Registry); + llvm::initializeRemovePtrToIntPass(Registry); llvm::legacy::PassManager pass_manager; + pass_manager.add(seadsa::createRemovePtrToIntPass()); pass_manager.add(llvm::createLowerSwitchPass()); // pass_manager.add(llvm::createCFGSimplificationPass()); // Shaobo: sea-dsa is inconsistent with the pass below. - //pass_manager.add(llvm::createInternalizePass()); + // pass_manager.add(llvm::createInternalizePass()); pass_manager.add(llvm::createPromoteMemoryToRegisterPass()); if (StaticUnroll) {