diff --git a/CMakeLists.txt b/CMakeLists.txt index db78c104d..80ad325c0 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -159,6 +159,7 @@ add_library(smackTranslator STATIC include/smack/SmackRep.h include/smack/SmackRepFlatMem.h include/smack/MemorySafetyChecker.h + include/smack/SignedIntegerOverflowChecker.h lib/smack/BoogieAst.cpp lib/smack/BplFilePrinter.cpp lib/smack/BplPrinter.cpp @@ -175,6 +176,7 @@ add_library(smackTranslator STATIC lib/smack/SmackRep.cpp lib/smack/SmackRepFlatMem.cpp lib/smack/MemorySafetyChecker.cpp + lib/smack/SignedIntegerOverflowChecker.cpp ) add_executable(llvm2bpl diff --git a/Doxyfile b/Doxyfile index b9a3ca2b7..8097ba76d 100644 --- a/Doxyfile +++ b/Doxyfile @@ -5,7 +5,7 @@ #--------------------------------------------------------------------------- DOXYFILE_ENCODING = UTF-8 PROJECT_NAME = smack -PROJECT_NUMBER = 1.7.0 +PROJECT_NUMBER = 1.7.1 PROJECT_BRIEF = "A bounded software verifier." PROJECT_LOGO = OUTPUT_DIRECTORY = docs diff --git a/bin/build.sh b/bin/build.sh index 8748b27c7..5920c2d98 100755 --- a/bin/build.sh +++ b/bin/build.sh @@ -24,7 +24,7 @@ INSTALL_DEPENDENCIES=1 BUILD_Z3=1 BUILD_BOOGIE=1 BUILD_CORRAL=1 -BUILD_LOCKPWN=0 +BUILD_LOCKPWN=1 BUILD_SMACK=1 TEST_SMACK=1 BUILD_LLVM=0 # LLVM is typically installed from packages (see below) @@ -369,6 +369,7 @@ then cd ${ROOT} git clone https://github.com/smackers/lockpwn.git cd ${LOCKPWN_DIR} + git reset --hard ${LOCKPWN_COMMIT} xbuild lockpwn.sln /p:Configuration=Release ln -s ${Z3_DIR}/bin/z3 ${LOCKPWN_DIR}/Binaries/z3.exe diff --git a/bin/package-smack.sh b/bin/package-smack.sh index a25f132aa..519568e00 100755 --- a/bin/package-smack.sh +++ b/bin/package-smack.sh @@ -6,7 +6,7 @@ # Note: this script requires CDE to be downloaded from # http://www.pgbovine.net/cde.html -VERSION=1.7.0 +VERSION=1.7.1 PACKAGE=smack-$VERSION-64 # Create folder to export diff --git a/bin/smack-svcomp-wrapper.sh b/bin/smack-svcomp-wrapper.sh index 24ddf364c..2db7b289b 100755 --- a/bin/smack-svcomp-wrapper.sh +++ b/bin/smack-svcomp-wrapper.sh @@ -4,16 +4,20 @@ ROOT="$( cd "$(dirname "$(readlink -f "${0}")")" && pwd )" SMACK_BIN="${ROOT}/smack/bin" +BOOGIE_BIN="${ROOT}/boogie" CORRAL_BIN="${ROOT}/corral" LOCKPWN_BIN="${ROOT}/lockpwn" LLVM_BIN="${ROOT}/llvm/bin" +LLVM_LIB="${ROOT}/llvm/lib" -# Setting mono heap size to 9GB -export MONO_GC_PARAMS=max-heap-size=9g +# Setting mono heap size to 13GB +export MONO_GC_PARAMS=max-heap-size=13g export PATH=${LLVM_BIN}:$SMACK_BIN:$PATH +export BOOGIE="mono ${BOOGIE_BIN}/Boogie.exe" export CORRAL="mono ${CORRAL_BIN}/corral.exe" export LOCKPWN="mono ${LOCKPWN_BIN}/lockpwn.exe" +export LD_LIBRARY_PATH=${LLVM_LIB}:$LD_LIBRARY_PATH smack -x=svcomp --verifier=svcomp -q $@ diff --git a/bin/versions b/bin/versions index f0a1db5ba..a486ead0c 100644 --- a/bin/versions +++ b/bin/versions @@ -1,3 +1,4 @@ MONO_VERSION=3.8.0 BOOGIE_COMMIT=4e4c3a5252 CORRAL_COMMIT=874a078e39 +LOCKPWN_COMMIT=a4d802a1cb diff --git a/include/smack/BoogieAst.h b/include/smack/BoogieAst.h index 837fd9f1d..9c76685c1 100644 --- a/include/smack/BoogieAst.h +++ b/include/smack/BoogieAst.h @@ -194,6 +194,7 @@ class Attr { public: Attr(std::string n, std::initializer_list vs) : name(n), vals(vs) {} void print(std::ostream& os) const; + std::string getName() const { return name; } static const Attr* attr(std::string s); static const Attr* attr(std::string s, std::string v); @@ -268,6 +269,13 @@ class AssumeStmt : public Stmt { void add(const Attr* a) { attrs.push_back(a); } + bool hasAttr(std::string name) const { + for (auto a = attrs.begin(); a != attrs.end(); ++a) { + if ((*a)->getName() == name) + return true; + } + return false; + } void print(std::ostream& os) const; static bool classof(const Stmt* S) { return S->getKind() == ASSUME; } }; diff --git a/include/smack/SignedIntegerOverflowChecker.h b/include/smack/SignedIntegerOverflowChecker.h new file mode 100644 index 000000000..5a502fcc2 --- /dev/null +++ b/include/smack/SignedIntegerOverflowChecker.h @@ -0,0 +1,27 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// +#ifndef SIGNEDINTEGEROVERFLOWCHECKER_H +#define SIGNEDINTEGEROVERFLOWCHECKER_H + +#include "llvm/Pass.h" +#include "llvm/IR/Module.h" +#include + +namespace smack { + +class SignedIntegerOverflowChecker: public llvm::ModulePass { +public: + static char ID; // Pass identification, replacement for typeid + SignedIntegerOverflowChecker() : llvm::ModulePass(ID) {} + virtual bool runOnModule(llvm::Module& m); +private: + static std::map INSTRUCTION_TABLE; + static std::map INT_MAX_TABLE; + static std::map INT_MIN_TABLE; + void replaceValue(llvm::Value* ee, llvm::Value* er); +}; + +} + +#endif //SIGNEDINTEGEROVERFLOWCHECKER_H diff --git a/include/smack/SmackInstGenerator.h b/include/smack/SmackInstGenerator.h index 3569cfe47..bb4a0162e 100644 --- a/include/smack/SmackInstGenerator.h +++ b/include/smack/SmackInstGenerator.h @@ -23,6 +23,7 @@ class SmackInstGenerator : public llvm::InstVisitor { Naming& naming; Block* currBlock; + llvm::BasicBlock::const_iterator nextInst; std::map blockMap; std::map sourceNames; diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index 8468f4920..680738711 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -68,7 +68,7 @@ class SmackRep { const Expr* cast(unsigned opcode, const llvm::Value* v, const llvm::Type* t); 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); + const Expr* cmp(unsigned predicate, const llvm::Value* lhs, const llvm::Value* rhs, bool isUnsigned); std::string procName(const llvm::User& U); std::string procName(llvm::Function* F, const llvm::User& U); @@ -99,14 +99,14 @@ class SmackRep { std::string type(const llvm::Type* t); std::string type(const llvm::Value* v); - const Expr* lit(const llvm::Value* v); + const Expr* lit(const llvm::Value* v, bool isUnsigned=false); const Expr* lit(const llvm::Value* v, unsigned flag); const Expr* ptrArith(const llvm::GetElementPtrInst* I); const Expr* ptrArith(const llvm::ConstantExpr* CE); const Expr* ptrArith(const llvm::Value* p, std::vector< std::pair > args); - const Expr* expr(const llvm::Value* v); + const Expr* expr(const llvm::Value* v, bool isConstIntUnsigned=false); const Expr* cast(const llvm::Instruction* I); const Expr* cast(const llvm::ConstantExpr* CE); diff --git a/lib/smack/SignedIntegerOverflowChecker.cpp b/lib/smack/SignedIntegerOverflowChecker.cpp new file mode 100644 index 000000000..65d02f9de --- /dev/null +++ b/lib/smack/SignedIntegerOverflowChecker.cpp @@ -0,0 +1,125 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// +#include "smack/SignedIntegerOverflowChecker.h" +#include "smack/Naming.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/InstIterator.h" +#include "llvm/IR/Constants.h" +#include "llvm/Support/Debug.h" +#include "llvm/IR/ValueSymbolTable.h" +#include "llvm/IR/IRBuilder.h" +#include "llvm/Support/Regex.h" +#include + +namespace smack { + +using namespace llvm; + +Regex OVERFLOW_INTRINSICS("^llvm.s(add|sub|mul).with.overflow.i(32|64)$"); + +std::map SignedIntegerOverflowChecker::INSTRUCTION_TABLE { + {"add", Instruction::Add}, + {"sub", Instruction::Sub}, + {"mul", Instruction::Mul} +}; + +std::map SignedIntegerOverflowChecker::INT_MAX_TABLE { + {32, "2147483647"}, + {64, "9223372036854775807"} +}; + +std::map SignedIntegerOverflowChecker::INT_MIN_TABLE { + {32, "-2147483648"}, + {64, "-9223372036854775808"} +}; + +void SignedIntegerOverflowChecker::replaceValue(Value* ee, Value* er) { + for (auto u : ee->users()) { + if (auto inst = dyn_cast(u)) { + if (inst != cast(ee)) { + for (unsigned i = 0; i < inst->getNumOperands(); ++i) { + if (inst->getOperand(i) == ee) + inst->setOperand(i, er); + } + } + } + } +} + +bool SignedIntegerOverflowChecker::runOnModule(Module& m) { + DataLayout* dataLayout = new DataLayout(&m); + Function* va = m.getFunction("__SMACK_overflow_false"); + Function* co = m.getFunction("__SMACK_check_overflow"); + + for (auto& F : m) { + if (!Naming::isSmackName(F.getName())) { + for (inst_iterator I = inst_begin(F), E = inst_end(F); I != E; ++I) { + if (auto ci = dyn_cast(&*I)) { + Function* f = ci->getCalledFunction(); + if (f && f->hasName() && f->getName() == "llvm.trap") { + ci->setCalledFunction(va); + } + } + if (auto ei = dyn_cast(&*I)) { + if (auto ci = dyn_cast(ei->getAggregateOperand())) { + Function* f = ci->getCalledFunction(); + SmallVectorImpl *ar = new SmallVector; + if (f && f->hasName() && OVERFLOW_INTRINSICS.match(f->getName().str(), ar)) { + std::string op = ar->begin()[1].str(); + std::string len = ar->begin()[2].str(); + int bits = std::stoi(len); + if (ei->getIndices()[0] == 0) { + Value* o1 = ci->getArgOperand(0); + Value* o2 = ci->getArgOperand(1); + CastInst* so1 = CastInst::CreateSExtOrBitCast(o1, IntegerType::get(F.getContext(), bits*2), "", &*I); + CastInst* so2 = CastInst::CreateSExtOrBitCast(o2, IntegerType::get(F.getContext(), bits*2), "", &*I); + BinaryOperator* ai = BinaryOperator::Create(INSTRUCTION_TABLE.at(op), so1, so2, "", &*I); + CastInst* tr = CastInst::CreateTruncOrBitCast(ai, IntegerType::get(F.getContext(), bits), "", &*I); + //replaceValue(&*I, tr); + (*I).replaceAllUsesWith(tr); + //I->eraseFromParent(); + } + if (ei->getIndices()[0] == 1) { + auto ai = std::prev(std::prev(std::prev(I))); + ConstantInt* max = ConstantInt::get(IntegerType::get(F.getContext(), bits*2), INT_MAX_TABLE.at(bits), 10); + ConstantInt* min = ConstantInt::get(IntegerType::get(F.getContext(), bits*2), INT_MIN_TABLE.at(bits), 10); + ICmpInst* gt = new ICmpInst(&*I, CmpInst::ICMP_SGT, &*ai, max, ""); + ICmpInst* lt = new ICmpInst(&*I, CmpInst::ICMP_SLT, &*ai, min, ""); + BinaryOperator* flag = BinaryOperator::Create(Instruction::Or, gt, lt, "", &*I); + //replaceValue(&*I, flag); + (*I).replaceAllUsesWith(flag); + } + } + } + } + if (auto sdi = dyn_cast(&*I)) { + if (sdi->getOpcode() == Instruction::SDiv) { + int bits = sdi->getType()->getIntegerBitWidth(); + Value* o1 = sdi->getOperand(0); + Value* o2 = sdi->getOperand(1); + CastInst* so1 = CastInst::CreateSExtOrBitCast(o1, IntegerType::get(F.getContext(), bits*2), "", &*I); + CastInst* so2 = CastInst::CreateSExtOrBitCast(o2, IntegerType::get(F.getContext(), bits*2), "", &*I); + BinaryOperator* lsdi = BinaryOperator::Create(Instruction::SDiv, so1, so2, "", &*I); + ConstantInt* max = ConstantInt::get(IntegerType::get(F.getContext(), bits*2), INT_MAX_TABLE.at(bits), 10); + ConstantInt* min = ConstantInt::get(IntegerType::get(F.getContext(), bits*2), INT_MIN_TABLE.at(bits), 10); + ICmpInst* gt = new ICmpInst(&*I, CmpInst::ICMP_SGT, lsdi, max, ""); + ICmpInst* lt = new ICmpInst(&*I, CmpInst::ICMP_SLT, lsdi, min, ""); + BinaryOperator* flag = BinaryOperator::Create(Instruction::Or, gt, lt, "", &*I); + CastInst* tf = CastInst::CreateSExtOrBitCast(flag, co->getArgumentList().begin()->getType(), "", &*I); + CallInst* ci = CallInst::Create(co, {tf}, "", &*I); + CastInst* tv = CastInst::CreateTruncOrBitCast(lsdi, sdi->getType(), "", &*I); + //replaceValue(&*I, tv); + (*I).replaceAllUsesWith(tv); + } + } + } + } + } + return true; +} + +// Pass ID variable +char SignedIntegerOverflowChecker::ID = 0; +} diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index a2f6e3faa..c854aced4 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -34,7 +34,7 @@ Regex VAR_DECL("^[[:space:]]*var[[:space:]]+([[:alpha:]_.$#'`~^\\?][[:alnum:]_.$ // Procedures whose return value should not be marked as external Regex EXTERNAL_PROC_IGNORE("^(malloc|__VERIFIER_nondet)$"); -std::string i2s(llvm::Instruction& i) { +std::string i2s(const llvm::Instruction& i) { std::string s; llvm::raw_string_ostream ss(s); ss << i; @@ -87,9 +87,11 @@ void SmackInstGenerator::processInstruction(llvm::Instruction& inst) { annotate(inst, currBlock); ORIG(inst); nameInstruction(inst); + nextInst++; } void SmackInstGenerator::visitBasicBlock(llvm::BasicBlock& bb) { + nextInst = bb.begin(); currBlock = getBlock(&bb); } @@ -278,10 +280,14 @@ void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator& I) { void SmackInstGenerator::visitExtractValueInst(llvm::ExtractValueInst& evi) { processInstruction(evi); - const Expr* e = rep.expr(evi.getAggregateOperand()); - for (unsigned i = 0; i < evi.getNumIndices(); i++) - e = Expr::fn(Naming::EXTRACT_VALUE, e, Expr::lit((unsigned long) evi.getIndices()[i])); - emit(Stmt::assign(rep.expr(&evi),e)); + if (!SmackOptions::BitPrecise) { + const Expr* e = rep.expr(evi.getAggregateOperand()); + for (unsigned i = 0; i < evi.getNumIndices(); i++) + e = Expr::fn(Naming::EXTRACT_VALUE, e, Expr::lit((unsigned long) evi.getIndices()[i])); + emit(Stmt::assign(rep.expr(&evi),e)); + } else { + WARN("Ignoring extract instruction under bit vector mode."); + } } void SmackInstGenerator::visitInsertValueInst(llvm::InsertValueInst& ivi) { @@ -353,8 +359,12 @@ void SmackInstGenerator::visitStoreInst(llvm::StoreInst& si) { if (SmackOptions::SourceLocSymbols) { if (const llvm::GlobalVariable* G = llvm::dyn_cast(P)) { - assert(G->hasName() && "Expected named global variable."); - emit(Stmt::call("boogie_si_record_" + rep.type(V), {rep.expr(V)}, {}, {Attr::attr("cexpr", G->getName().str())})); + if (const llvm::PointerType* t = llvm::dyn_cast(G->getType())) { + if (!t->getElementType()->isPointerTy()) { + assert(G->hasName() && "Expected named global variable."); + emit(Stmt::call("boogie_si_record_" + rep.type(V), {rep.expr(V)}, {}, {Attr::attr("cexpr", G->getName().str())})); + } + } } } @@ -589,17 +599,35 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { } } +bool isSourceLoc(const Stmt* stmt) { + return (stmt->getKind() == Stmt::ASSUME + && (llvm::cast(stmt))->hasAttr("sourceloc")) + || (stmt->getKind() == Stmt::CALL); +} + void SmackInstGenerator::visitDbgValueInst(llvm::DbgValueInst& dvi) { processInstruction(dvi); if (SmackOptions::SourceLocSymbols) { const Value* V = dvi.getValue(); const llvm::DILocalVariable *var = dvi.getVariable(); - if (V) { - V = V->stripPointerCasts(); - std::stringstream recordProc; - recordProc << "boogie_si_record_" << rep.type(V); - emit(Stmt::call(recordProc.str(), {rep.expr(V)}, {}, {Attr::attr("cexpr", var->getName().str())})); + //if (V && !V->getType()->isPointerTy() && !llvm::isa(V)) { + if (V && !V->getType()->isPointerTy()) { + //if (currBlock->begin() != currBlock->end() + //&& currBlock->getStatements().back()->getKind() == Stmt::ASSUME) { + // && isSourceLoc(currBlock->getStatements().back())) { + //assert(&*currInst == &dvi && "Current Instruction mismatch!"); + auto currInst = std::prev(nextInst); + 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)) { + std::stringstream recordProc; + recordProc << "boogie_si_record_" << rep.type(V); + emit(Stmt::call(recordProc.str(), {rep.expr(V)}, {}, {Attr::attr("cexpr", var->getName().str())})); + } + } } } } diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 5531e7ccf..00c4afc7b 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -586,13 +586,13 @@ const Expr* SmackRep::integerLit(long v, unsigned width) { } } -const Expr* SmackRep::lit(const llvm::Value* v) { +const Expr* SmackRep::lit(const llvm::Value* v, bool isUnsigned) { using namespace llvm; if (const ConstantInt* ci = llvm::dyn_cast(v)) { const APInt& API = ci->getValue(); unsigned width = ci->getBitWidth(); - bool neg = width > 1 && ci->isNegative(); + bool neg = isUnsigned? false : width > 1 && ci->isNegative(); std::string str = (neg ? API.abs() : API).toString(10,false); const Expr* e = SmackOptions::BitPrecise ? Expr::lit(str,width) : Expr::lit(str,0); std::stringstream op; @@ -696,7 +696,7 @@ const Expr* SmackRep::ptrArith(const llvm::Value* p, return e; } -const Expr* SmackRep::expr(const llvm::Value* v) { +const Expr* SmackRep::expr(const llvm::Value* v, bool isConstIntUnsigned) { using namespace llvm; if (isa(v)) { @@ -737,7 +737,7 @@ const Expr* SmackRep::expr(const llvm::Value* v) { } } else if (const ConstantInt* ci = dyn_cast(constant)) { - return lit(ci); + return lit(ci, isConstIntUnsigned); } else if (const ConstantFP* cf = dyn_cast(constant)) { return lit(cf); @@ -786,16 +786,17 @@ const Expr* SmackRep::bop(unsigned opcode, const llvm::Value* lhs, const llvm::V } const Expr* SmackRep::cmp(const llvm::CmpInst* I) { - return cmp(I->getPredicate(), I->getOperand(0), I->getOperand(1)); + bool isUnsigned = I->isUnsigned(); + return cmp(I->getPredicate(), I->getOperand(0), I->getOperand(1), isUnsigned); } const Expr* SmackRep::cmp(const llvm::ConstantExpr* CE) { - return cmp(CE->getPredicate(), CE->getOperand(0), CE->getOperand(1)); + return cmp(CE->getPredicate(), CE->getOperand(0), CE->getOperand(1), false); } -const Expr* SmackRep::cmp(unsigned predicate, const llvm::Value* lhs, const llvm::Value* rhs) { +const Expr* SmackRep::cmp(unsigned predicate, const llvm::Value* lhs, const llvm::Value* rhs, bool isUnsigned) { std::string fn = Naming::CMPINST_TABLE.at(predicate); - return Expr::fn(opName(fn, {lhs->getType()}), expr(lhs), expr(rhs)); + return Expr::fn(opName(fn, {lhs->getType()}), expr(lhs, isUnsigned), expr(rhs, isUnsigned)); } ProcDecl* SmackRep::procedure(Function* F, CallInst* CI) { diff --git a/share/smack/include/smack.h b/share/smack/include/smack.h index 14c7a5da7..93a767bb5 100644 --- a/share/smack/include/smack.h +++ b/share/smack/include/smack.h @@ -3,6 +3,7 @@ // #ifndef SMACK_H_ #define SMACK_H_ +#include /** * The SMACK "prelude" declarations @@ -72,45 +73,62 @@ void exit(int); #define S(...) TY(__VA_ARGS__, S4, S3, S2, S1)(__VA_ARGS__) #define U(...) TY(__VA_ARGS__, U4, U3, U2, U1)(__VA_ARGS__) -#define NONDET_DECL(ty...) S(ty) U(__VERIFIER_nondet,U(ty)) () +#define NONDET_DECL(P, ty...) S(ty) U(P,U(ty)) () void* __VERIFIER_nondet(void); -NONDET_DECL(char); -NONDET_DECL(signed,char); -NONDET_DECL(unsigned,char); -NONDET_DECL(short); -NONDET_DECL(short,int); -NONDET_DECL(signed,short); -NONDET_DECL(signed,short,int); -NONDET_DECL(unsigned,short); -NONDET_DECL(unsigned,short,int); -NONDET_DECL(int); -NONDET_DECL(signed,int); -NONDET_DECL(unsigned); -NONDET_DECL(unsigned,int); -NONDET_DECL(long); -NONDET_DECL(long,int); -NONDET_DECL(signed,long); -NONDET_DECL(signed,long,int); -NONDET_DECL(unsigned,long); -NONDET_DECL(unsigned,long,int); -NONDET_DECL(long,long); -NONDET_DECL(long,long,int); -NONDET_DECL(signed,long,long); -NONDET_DECL(signed,long,long,int); -NONDET_DECL(unsigned,long,long); -NONDET_DECL(unsigned,long,long,int); -NONDET_DECL(float); -NONDET_DECL(double); -NONDET_DECL(long,double); - -// Apparently used in SVCOMP benchmarks -_Bool __VERIFIER_nondet_bool(void); -unsigned char __VERIFIER_nondet_uchar(void); -unsigned short __VERIFIER_nondet_ushort(void); -unsigned __VERIFIER_nondet_uint(void); -unsigned long __VERIFIER_nondet_ulong(void); -void* __VERIFIER_nondet_pointer(void); +NONDET_DECL(__SMACK_nondet,char); +NONDET_DECL(__SMACK_nondet,signed,char); +NONDET_DECL(__SMACK_nondet,unsigned,char); +NONDET_DECL(__SMACK_nondet,short); +NONDET_DECL(__SMACK_nondet,short,int); +NONDET_DECL(__SMACK_nondet,signed,short); +NONDET_DECL(__SMACK_nondet,signed,short,int); +NONDET_DECL(__SMACK_nondet,unsigned,short); +NONDET_DECL(__SMACK_nondet,unsigned,short,int); +NONDET_DECL(__SMACK_nondet,int); +NONDET_DECL(__SMACK_nondet,signed,int); +NONDET_DECL(__SMACK_nondet,unsigned); +NONDET_DECL(__SMACK_nondet,unsigned,int); +NONDET_DECL(__SMACK_nondet,long); +NONDET_DECL(__SMACK_nondet,long,int); +NONDET_DECL(__SMACK_nondet,signed,long); +NONDET_DECL(__SMACK_nondet,signed,long,int); +NONDET_DECL(__SMACK_nondet,unsigned,long); +NONDET_DECL(__SMACK_nondet,unsigned,long,int); +NONDET_DECL(__SMACK_nondet,long,long); +NONDET_DECL(__SMACK_nondet,long,long,int); +NONDET_DECL(__SMACK_nondet,signed,long,long); +NONDET_DECL(__SMACK_nondet,signed,long,long,int); +NONDET_DECL(__SMACK_nondet,unsigned,long,long); +NONDET_DECL(__SMACK_nondet,unsigned,long,long,int); +NONDET_DECL(__VERIFIER_nondet,char); +NONDET_DECL(__VERIFIER_nondet,signed,char); +NONDET_DECL(__VERIFIER_nondet,unsigned,char); +NONDET_DECL(__VERIFIER_nondet,short); +NONDET_DECL(__VERIFIER_nondet,short,int); +NONDET_DECL(__VERIFIER_nondet,signed,short); +NONDET_DECL(__VERIFIER_nondet,signed,short,int); +NONDET_DECL(__VERIFIER_nondet,unsigned,short); +NONDET_DECL(__VERIFIER_nondet,unsigned,short,int); +NONDET_DECL(__VERIFIER_nondet,int); +NONDET_DECL(__VERIFIER_nondet,signed,int); +NONDET_DECL(__VERIFIER_nondet,unsigned); +NONDET_DECL(__VERIFIER_nondet,unsigned,int); +NONDET_DECL(__VERIFIER_nondet,long); +NONDET_DECL(__VERIFIER_nondet,long,int); +NONDET_DECL(__VERIFIER_nondet,signed,long); +NONDET_DECL(__VERIFIER_nondet,signed,long,int); +NONDET_DECL(__VERIFIER_nondet,unsigned,long); +NONDET_DECL(__VERIFIER_nondet,unsigned,long,int); +NONDET_DECL(__VERIFIER_nondet,long,long); +NONDET_DECL(__VERIFIER_nondet,long,long,int); +NONDET_DECL(__VERIFIER_nondet,signed,long,long); +NONDET_DECL(__VERIFIER_nondet,signed,long,long,int); +NONDET_DECL(__VERIFIER_nondet,unsigned,long,long); +NONDET_DECL(__VERIFIER_nondet,unsigned,long,long,int); +NONDET_DECL(__VERIFIER_nondet,float); +NONDET_DECL(__VERIFIER_nondet,double); +NONDET_DECL(__VERIFIER_nondet,long,double); #if FLOAT_ENABLED //floats @@ -193,6 +211,15 @@ int __finite(double x); #undef U #undef NONDET_DECL +// Apparently used in SVCOMP benchmarks +_Bool __VERIFIER_nondet_bool(void); +unsigned char __VERIFIER_nondet_uchar(void); +unsigned short __VERIFIER_nondet_ushort(void); +unsigned __VERIFIER_nondet_uint(void); +unsigned long __VERIFIER_nondet_ulong(void); +void* __VERIFIER_nondet_pointer(void); + + void __SMACK_decls(); #ifdef __cplusplus diff --git a/share/smack/include/spinlock.h b/share/smack/include/spinlock.h deleted file mode 100644 index 90c161ff5..000000000 --- a/share/smack/include/spinlock.h +++ /dev/null @@ -1,30 +0,0 @@ -// -// Copyright (c) 2013 Zvonimir Rakamaric (zvonimir@cs.utah.edu), -// Michael Emmi (michael.emmi@gmail.com) -// This file is distributed under the MIT License. See LICENSE for details. -// -#ifndef SPINLOCK_H -#define SPINLOCK_H - - -// Begin:: A bunch of stuff to support multiple methods to init locks: -typedef unsigned int spinlock_t; - -#define __SPIN_LOCK_UNLOCKED() (spinlock_t)0 - -#define SPIN_LOCK_UNLOCKED __SPIN_LOCK_UNLOCKED() -#define DEFINE_SPINLOCK(x) spinlock_t x = __SPIN_LOCK_UNLOCKED() - -#define spin_lock_init(lock) \ - do { *(lock) = SPIN_LOCK_UNLOCKED; } while (0) -// End:: a bunch of stuff to init locks - -//model spinlock: -// 0 = unlocked, -// else = locked by thread with matching id - -void spin_lock(spinlock_t *__lock); - -void spin_unlock(spinlock_t *__lock); - -#endif // SPINLOCK_H diff --git a/share/smack/lib/Makefile b/share/smack/lib/Makefile index 7925f6aaa..58db6376d 100644 --- a/share/smack/lib/Makefile +++ b/share/smack/lib/Makefile @@ -2,7 +2,7 @@ CC = clang INC = ../include CFLAGS = -c -Wall -emit-llvm -O0 -g -I$(INC) -SOURCES = smack.c pthread.c spinlock.c +SOURCES = smack.c pthread.c BITCODE = $(SOURCES:.c=.bc) diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c index d8826f7ea..7e4ebcc6a 100644 --- a/share/smack/lib/smack.c +++ b/share/smack/lib/smack.c @@ -2,6 +2,7 @@ // This file is distributed under the MIT License. See LICENSE for details. #include +#include /** * The SMACK "prelude" definitions @@ -33,14 +34,30 @@ void __VERIFIER_assume(int x) { #ifndef CUSTOM_VERIFIER_ASSERT void __VERIFIER_assert(int x) { +#if !MEMORY_SAFETY && !SIGNED_INTEGER_OVERFLOW_CHECK __SMACK_dummy(x); __SMACK_code("assert @ != $0;", x); +#endif } #endif void __VERIFIER_error(void) { +#if !MEMORY_SAFETY && !SIGNED_INTEGER_OVERFLOW_CHECK __SMACK_code("assert false;"); +#else + __SMACK_code("assume false;"); +#endif +} + +#if SIGNED_INTEGER_OVERFLOW_CHECK +void __SMACK_overflow_false(void) { + __SMACK_code("assert {:overflow} false;"); } +void __SMACK_check_overflow(int flag) { + __SMACK_dummy(flag); __SMACK_code("assert {:overflow} @ == $0;", flag); +} +#endif + void exit(int x) { #if MEMORY_SAFETY __SMACK_code("assert $allocatedCounter == 0;"); @@ -49,33 +66,174 @@ void exit(int x) { while(1); } +char __VERIFIER_nondet_char() { + char x = __SMACK_nondet_char(); + __VERIFIER_assume(x >= SCHAR_MIN && x <= SCHAR_MAX); + return x; +} + +signed char __VERIFIER_nondet_signed_char() { + signed char x = __SMACK_nondet_signed_char(); + __VERIFIER_assume(x >= SCHAR_MIN && x <= SCHAR_MAX); + return x; +} + +unsigned char __VERIFIER_nondet_unsigned_char() { + unsigned char x = __SMACK_nondet_unsigned_char(); + __VERIFIER_assume(x >= 0 && x <= UCHAR_MAX); + return x; +} + +short __VERIFIER_nondet_short() { + short x = __SMACK_nondet_short(); + __VERIFIER_assume(x >= SHRT_MIN && x <= SHRT_MAX); + return x; +} + +signed short __VERIFIER_nondet_signed_short() { + signed short x = __SMACK_nondet_signed_short(); + __VERIFIER_assume(x >= SHRT_MIN && x <= SHRT_MAX); + return x; +} + +signed short int __VERIFIER_nondet_signed_short_int() { + signed short int x = __SMACK_nondet_signed_short_int(); + __VERIFIER_assume(x >= SHRT_MIN && x <= SHRT_MAX); + return x; +} + +unsigned short __VERIFIER_nondet_unsigned_short() { + unsigned short x = __SMACK_nondet_unsigned_short(); + __VERIFIER_assume(x >= 0 && x <= USHRT_MAX); + return x; +} + +unsigned short int __VERIFIER_nondet_unsigned_short_int() { + unsigned short int x = __SMACK_nondet_unsigned_short_int(); + __VERIFIER_assume(x >= 0 && x <= USHRT_MAX); + return x; +} + +int __VERIFIER_nondet_int() { + int x = __SMACK_nondet_int(); + __VERIFIER_assume(x >= INT_MIN && x <= INT_MAX); + return x; +} + +signed int __VERIFIER_nondet_signed_int() { + signed int x = __SMACK_nondet_signed_int(); + __VERIFIER_assume(x >= INT_MIN && x <= INT_MAX); + return x; +} + +unsigned __VERIFIER_nondet_unsigned() { + unsigned x = __SMACK_nondet_unsigned(); + __VERIFIER_assume(x >= 0 && x <= UINT_MAX); + return x; +} + +unsigned int __VERIFIER_nondet_unsigned_int() { + unsigned int x = __SMACK_nondet_unsigned_int(); + __VERIFIER_assume(x >= 0 && x <= UINT_MAX); + return x; +} + +long __VERIFIER_nondet_long() { + long x = __SMACK_nondet_long(); + __VERIFIER_assume(x >= LONG_MIN && x <= LONG_MAX); + return x; +} + +long int __VERIFIER_nondet_long_int() { + long int x = __SMACK_nondet_long_int(); + __VERIFIER_assume(x >= LONG_MIN && x <= LONG_MAX); + return x; +} + +signed long __VERIFIER_nondet_signed_long() { + signed long x = __SMACK_nondet_signed_long(); + __VERIFIER_assume(x >= LONG_MIN && x <= LONG_MAX); + return x; +} + +signed long int __VERIFIER_nondet_signed_long_int() { + signed long int x = __SMACK_nondet_signed_long_int(); + __VERIFIER_assume(x >= LONG_MIN && x <= LONG_MAX); + return x; +} + +unsigned long __VERIFIER_nondet_unsigned_long() { + unsigned long x = __SMACK_nondet_unsigned_long(); + __VERIFIER_assume(x >= 0 && x <= ULONG_MAX); + return x; +} + +unsigned long int __VERIFIER_nondet_unsigned_long_int() { + unsigned long int x = __SMACK_nondet_unsigned_long_int(); + __VERIFIER_assume(x >= 0 && x <= ULONG_MAX); + return x; +} + +long long __VERIFIER_nondet_long_long() { + long long x = __SMACK_nondet_long_long(); + __VERIFIER_assume(x >= LLONG_MIN && x <= LLONG_MAX); + return x; +} + +long long int __VERIFIER_nondet_long_long_int() { + long long int x = __SMACK_nondet_long_long_int(); + __VERIFIER_assume(x >= LLONG_MIN && x <= LLONG_MAX); + return x; +} + +signed long long __VERIFIER_nondet_signed_long_long() { + signed long long x = __SMACK_nondet_signed_long_long(); + __VERIFIER_assume(x >= LLONG_MIN && x <= LLONG_MAX); + return x; +} + +signed long long int __VERIFIER_nondet_signed_long_long_int() { + signed long long int x = __SMACK_nondet_signed_long_long_int(); + __VERIFIER_assume(x >= LLONG_MIN && x <= LLONG_MAX); + return x; +} + +unsigned long long __VERIFIER_nondet_unsigned_long_long() { + unsigned long long x = __SMACK_nondet_unsigned_long_long(); + __VERIFIER_assume(x >= 0 && x <= ULLONG_MAX); + return x; +} + +unsigned long long int __VERIFIER_nondet_unsigned_long_long_int() { + unsigned long long int x = __SMACK_nondet_unsigned_long_long_int(); + __VERIFIER_assume(x >= 0 && x <= ULLONG_MAX); + return x; +} + // Apparently used in SVCCOMP benchmarks _Bool __VERIFIER_nondet_bool(void) { _Bool x = (_Bool)__VERIFIER_nondet_int(); + __VERIFIER_assume(x == 0 || x == 1); return x; } unsigned char __VERIFIER_nondet_uchar(void) { unsigned char x = __VERIFIER_nondet_unsigned_char(); - __VERIFIER_assume(x >= 0); return x; } unsigned short __VERIFIER_nondet_ushort(void) { unsigned short x = __VERIFIER_nondet_unsigned_short(); - __VERIFIER_assume(x >= 0); return x; } unsigned int __VERIFIER_nondet_uint(void) { unsigned int x = __VERIFIER_nondet_unsigned_int(); - __VERIFIER_assume(x >= 0); return x; } unsigned long __VERIFIER_nondet_ulong(void) { unsigned long x = __VERIFIER_nondet_unsigned_long(); - __VERIFIER_assume(x >= 0); return x; } @@ -123,13 +281,13 @@ float roundf(float x) { __SMACK_code("@ := sbv32td($float.round.rne(@));", rete, x); __SMACK_code("@ := sbv32td($float.round.rna(@));", reta, x); if (x > 0) - return fmax(rete, reta); + return fmax(rete, reta); return fmin(rete, reta); } long lroundf(float x) { long ret = __VERIFIER_nondet_long(); - __SMACK_code("@ := $float.lround(dtf(@));", ret, x); + __SMACK_code("@ := $float.lround.rne(dtf(@));", ret, x); return ret; } @@ -179,7 +337,7 @@ float sqrtf(float x) { float remainderf(float x, float y) { double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := $float.rem(dtf(@), dtf(@));", ret, x, y); + __SMACK_code("@ := ftd($float.rem(dtf(@), dtf(@)));", ret, x, y); return ret; } @@ -309,13 +467,13 @@ double round(double x) { __SMACK_code("@ := sbv64td($double.round.rne(@));", rete, x); __SMACK_code("@ := sbv64td($double.round.rna(@));", reta, x); if (x > 0) - return fmax(rete, reta); + return fmax(rete, reta); return fmin(rete, reta); } long lround(double x) { long ret = __VERIFIER_nondet_long(); - __SMACK_code("@ := $double.lround(@);", ret, x); + __SMACK_code("@ := $double.lround.rne(@);", ret, x); return ret; } @@ -894,6 +1052,7 @@ void __SMACK_decls() { D("axiom $xor.i1(0,1) == 1;"); D("axiom $xor.i1(1,0) == 1;"); D("axiom $xor.i1(1,1) == 0;"); + D("axiom($and.i32(32, 16) == 0);"); DECLARE(INLINE_CONVERSION,i128,i96,$trunc,{i}); DECLARE(INLINE_CONVERSION,i128,i88,$trunc,{i}); @@ -1447,7 +1606,7 @@ void __SMACK_decls() { #if BUILD_64 D("function {:builtin \"(_ fp.to_sbv 64) RNA\"} $float.lround(bvfloat) returns (bv64);"); - + #else D("function {:builtin \"(_ fp.to_sbv 32) RNA\"} $float.lround(bvfloat) returns (bv32);"); @@ -1571,7 +1730,7 @@ void __SMACK_decls() { #if BUILD_64 D("function {:builtin \"(_ fp.to_sbv 64) RNA\"} $double.lround.rne(bvdouble) returns (bv64);"); - + #else D("function {:builtin \"(_ fp.to_sbv 32) RNA\"} $double.lround.rna(bvdouble) returns (bv32);"); diff --git a/share/smack/lib/spinlock.c b/share/smack/lib/spinlock.c deleted file mode 100644 index 253766d8a..000000000 --- a/share/smack/lib/spinlock.c +++ /dev/null @@ -1,21 +0,0 @@ -#include "spinlock.h" -#include "smack.h" - -void spin_lock(spinlock_t *__lock) { - int ctid = __VERIFIER_nondet_int(); - __SMACK_code("call @ := corral_getThreadID();", ctid); - assert(ctid != (unsigned int)(*__lock)); - __SMACK_code("call corral_atomic_begin();"); - assume(*__lock == SPIN_LOCK_UNLOCKED); - *__lock = (spinlock_t)ctid; - __SMACK_code("call corral_atomic_end();"); -} - -void spin_unlock(spinlock_t *__lock) { - int ctid = __VERIFIER_nondet_int(); - __SMACK_code("call @ := corral_getThreadID();", ctid); - assert((unsigned int)ctid == (unsigned int)(*__lock)); - __SMACK_code("call corral_atomic_begin();"); - *__lock = SPIN_LOCK_UNLOCKED; - __SMACK_code("call corral_atomic_end();"); -} diff --git a/share/smack/reach.py b/share/smack/reach.py index 1a717972c..d6fffac15 100755 --- a/share/smack/reach.py +++ b/share/smack/reach.py @@ -11,7 +11,7 @@ from smackgen import * from smackverify import * -VERSION = '1.7.0' +VERSION = '1.7.1' def reachParser(): parser = argparse.ArgumentParser(add_help=False, parents=[verifyParser()]) diff --git a/share/smack/svcomp/filters.py b/share/smack/svcomp/filters.py index 25af0f6ea..049c6d5d5 100644 --- a/share/smack/svcomp/filters.py +++ b/share/smack/svcomp/filters.py @@ -35,8 +35,8 @@ def svcomp_filter(f): raw_lines = len(lines.split('\n')) executable = False - if len(linecount(r'__VERIFIER_nondet', r'void|extern', lines)) == 0: - executable = True + if raw_lines < 50 and len(linecount(r'__VERIFIER_nondet|fopen', r'void\s+|extern', lines)) == 0 and not ('while(1)' in lines): + executable = True if bv_filter(lines, raw_lines, pruned_lines): return 'bitvector', executable @@ -47,9 +47,15 @@ def svcomp_filter(f): return 'normal', executable def bv_filter(lines, raw_line_count, pruned_line_count): + if ("bugBrokenOut" in lines or "returnsStructure" in lines or "__VERIFIER_nondet_double" in lines or + "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines): + return 0 if raw_line_count > 1500: - return 0 + if 'ldv_usb_gadget' in lines or "SyncPush" in lines or "kaweth_set_receive_filter" in lines: + return 1 + else: + return 0 #line_count = raw_file_line_count(lines) if pruned_line_count > 650: @@ -61,6 +67,10 @@ def bv_filter(lines, raw_line_count, pruned_line_count): #cast patterns if pruned_line_count <= 210: + + if pruned_line_count < 25 and 'while(1)' in lines: + return 1 + casts = re.compile(r'''4294967295|plus_one|minus_one|\(x % 2\) == \(y % 2\)|linear_search|while \(\('0' <= c\) && \(c <= '9'\)\)''') if casts.search(lines): return 1 @@ -68,7 +78,7 @@ def bv_filter(lines, raw_line_count, pruned_line_count): bwops = re.compile(r'''[=|\(][^,]*[^\&|\(|{]\&\s|[^\|]\|\s|\^|>>|<<''') #bwops = re.compile(r'''\s\&\s|\s\|\s|\^|>>|<<''') #dv = re.compile(r'''1\s+<<\s+[1|5]|cil''') - dv = re.compile(r'''1.*<<.*\"|cil|found''') + dv = re.compile(r'''1.*<<.*\"|cil|found|node''') for line in lines.split('\n'): if bwops.search(line): @@ -82,6 +92,10 @@ def float_filter(lines, raw_line_count, pruned_line_count): fliteral = 0 ddecl = 0 + if ("bugBrokenOut" in lines or "returnsStructure" in lines or "__VERIFIER_nondet_double" in lines or + "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines): + return 1 + #heuristic #-1: don't do test on too large programs if raw_line_count >= 2000: return 0 @@ -113,6 +127,11 @@ def float_filter(lines, raw_line_count, pruned_line_count): for valid_line in valid_lines: if regex_special.search(valid_line) is not None and count <= 4: return 0 + if valid_line == '1.' or valid_line == '2.': + if 'double' not in lines: + return 0 + else: + return 1 return 1 @@ -143,6 +162,7 @@ def scrub_pthreads(s): fltrs.append(r'typedef\s+union\s+{\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_mutexattr_t;') #pthread_mutex_t fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_mutex_s\s+{\s+int\s+__lock;\s+unsigned\s+int\s+__count;\s+int\s+__owner;\s+unsigned\s+int\s+__nusers;\s+int\s+__kind;\s+int\s+__spins;\s+__pthread_list_t\s+__list;\s+}\s+__data;\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_mutex_t;') + fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_mutex_s\s+{\s+int\s+__lock;\s+unsigned\s+int\s+__count;\s+int\s+__owner;\s+int\s+__kind;\s+unsigned\s+int\s+__nusers;\s+__extension__\s+union\s+{\s+struct\s+{\s+short\s+__espins;\s+short\s+__elision;\s+}\s+__elision_data;\s+__pthread_slist_t\s+__list;\s+};\s+}\s+__data;\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_mutex_t;') fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_mutex_s\s+{\s+int\s+__lock;\s+unsigned\s+int\s+__count;\s+int\s+__owner;\s+int\s+__kind;\s+unsigned\s+int\s+__nusers;\s+__extension__\s+union\s+{\s+int\s+__spins;\s+__pthread_slist_t\s+__list;\s+};\s+}\s+__data;\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_mutex_t;') fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_mutex_s\s+{\s+int\s+__lock;\s+unsigned\s+int\s+__count;\s+int\s+__owner;\s+unsigned\s+int\s+__nusers;\s+int\s+__kind;\s+short\s+__spins;\s+short\s+__elision;\s+__pthread_list_t\s+__list;\s+# 124 "/usr/include/x86_64-linux-gnu/bits/pthreadtypes\.h" 3 4\s+}\s+__data;\s+\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+} pthread_mutex_t;') fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_mutex_s\s+{\s+int\s+__lock;\s+unsigned\s+int\s+__count;\s+int\s+__owner;\s+int\s+__kind;\s+unsigned\s+int\s+__nusers;\s+__extension__\s+union\s+{\s+struct\s+{\s+short\s+__espins;\s+short\s+__elision;\s+}\s+d;\s+__pthread_slist_t\s+__list;\s+};\s+}\s+__data;\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_mutex_t;') @@ -176,6 +196,7 @@ def scrub_pthreads(s): s = re.sub(r'(__VERIFIER_atomic_((?!begin|end).)*?\(.*?\);)', r'__VERIFIER_atomic_begin(); \1 __VERIFIER_atomic_end();', s) + s = re.sub(r'\ninline ', r'\n', s) return s, True diff --git a/share/smack/svcomp/random_testing.py b/share/smack/svcomp/random_testing.py new file mode 100644 index 000000000..169547f7f --- /dev/null +++ b/share/smack/svcomp/random_testing.py @@ -0,0 +1,66 @@ +import re +import os +import smack.top +import subprocess +import sys + +def random_test(args, result): + f = args.input_files[0] + + # test if a file can be tested + with open(f, 'r') as fi: + s = fi.read() + + l = s.split('\n') + if not (len(l) < 20 and len(filter(lambda x: re.search(r'=\s*__VERIFIER_nondet_uint', x), l)) == 1): + return 'abort' + + UMAX_INT = 2**32 - 1 + for i in [8, 4, 2]: + status = compile_and_run(f, s, UMAX_INT/i, args) + if status != 'true': + return status + + return result + +def compile_and_run(f, s, n, args): + s = re.sub("=\s*(__VERIFIER_nondet_uint\(\))", "="+str(n), s) + s = re.sub("__VERIFIER_assert\((.+)\);", "assert(\\1);", s) + s = re.sub(r'(extern )?void __VERIFIER_error()', '//', s) + s = re.sub(r'(extern )?void __VERIFIER_assume()', '//', s) + s = re.sub(r'__VERIFIER_error\(\)', 'assert(0)', s) + s = '#include\n' + s + + name = os.path.splitext(os.path.basename(f))[0] + tmp1 = smack.top.temporary_file(name, '.c', args) + with open(tmp1, 'w') as fo: + fo.write(s) + + tmp2 = smack.top.temporary_file(name, '.bin', args) + tmp2 = tmp2.split('/')[-1] + #compile and run + cmd = ['clang', tmp1, '-o', tmp2] + + proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + + out, err = proc.communicate() + rc = proc.returncode + + if rc: + print 'Compiling error' + print err + return 'unknown' + else: + cmd = [r'./' + tmp2] + proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + out, err = proc.communicate() + rc = proc.returncode + if rc: + if re.search(r'Assertion.*failed', err): + return 'false' + else: + print 'Execution error' + print err + return 'unknown' + else: + return 'true' diff --git a/share/smack/svcomp/toSVCOMPformat.py b/share/smack/svcomp/toSVCOMPformat.py index f26ea1981..5e5662efb 100644 --- a/share/smack/svcomp/toSVCOMPformat.py +++ b/share/smack/svcomp/toSVCOMPformat.py @@ -8,6 +8,8 @@ import re import sys import pprint +import os +import hashlib nextNum = 0 @@ -26,8 +28,16 @@ def addKeyDefs(root): keys = [] #keys are [attr.name, attr.type, for, id, hasDefault, defaultVal] keys.append(["assumption", "string", "edge", "assumption", False]) + keys.append(["assumption.scope", "string", "edge", "assumption.scope", False]) keys.append(["sourcecode", "string", "edge", "sourcecode", False]) + keys.append(["witness-type", "string", "graph", "witness-type", False]) keys.append(["sourcecodeLanguage", "string", "graph", "sourcecodelang", False]) + keys.append(["producer", "string", "graph", "producer", False]) + keys.append(["specification", "string", "graph", "specification", False]) + keys.append(["programfile", "string", "graph", "programfile", False]) + keys.append(["programhash", "string", "graph", "programhash", False]) + keys.append(["MemoryModel", "string", "graph", "memorymodel", False]) + keys.append(["architecture", "string", "graph", "architecture", False]) keys.append(["tokenSet", "string", "edge", "tokens", False]) keys.append(["originTokenSet", "string", "edge", "origintokens", False]) keys.append(["negativeCase", "string", "edge", "negated", True, "false"]) @@ -88,7 +98,7 @@ def addGraphEdge(tree, source, target, data={}): return newEdge -def buildEmptyXmlGraph(): +def buildEmptyXmlGraph(args, hasBug): """Builds an empty witness xml file, with all the keys we will be using already defined.""" root = ET.Element('graphml') @@ -97,8 +107,20 @@ def buildEmptyXmlGraph(): tree = ElementTree(root) addKeyDefs(root) graph = ET.SubElement(root, "graph", attrib={"edgedefault" : "directed"}) + + addKey(graph, "witness-type", "violation_witness" if hasBug else "correctness_witness") addKey(graph, "sourcecodelang", "C") - addKey(graph, "specification", "CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )") + from smack.top import VERSION + addKey(graph, "producer", "SMACK " + VERSION) + with open(args.svcomp_property, 'r') as ppf: + addKey(graph, "specification", ppf.read().strip()) + programfile = os.path.abspath(args.orig_files[0]) + addKey(graph, "programfile", programfile) + with open(programfile, 'r') as pgf: + addKey(graph, "programhash", hashlib.sha1(pgf.read()).hexdigest()) + addKey(graph, "memorymodel", "precise") + addKey(graph, "architecture", + re.search(r'-m(32|64)', args.clang_options).group(1) + 'bit') return tree def formatAssign(assignStmt): @@ -106,82 +128,77 @@ def formatAssign(assignStmt): return assignStmt m = re.match(r'(.*)=(.*)', assignStmt) if m: - return re.sub(r'=(\s*\d+)bv\d+', r'=\1', m.group(1) + "==" + m.group(2)) + repl = lambda x: '='+ x.group(1) + 'U' if x.group(2) is not None else '' + return re.sub(r'=(\s*\d+)(bv\d+)', repl, m.group(1) + "==" + m.group(2)) else: return "" -def smackJsonToXmlGraph(strJsonOutput): +def smackJsonToXmlGraph(strJsonOutput, args, hasBug): """Converts output from SMACK (in the smackd json format) to a graphml format that conforms to the SVCOMP witness file format""" - # Convert json string to json object - smackJson = json.loads(strJsonOutput) - # Get the failure node, and the list of trace entries to get there - jsonViolation = smackJson["failsAt"] - jsonTraces = smackJson["traces"] - # Build tree & start node - tree = buildEmptyXmlGraph() + tree = buildEmptyXmlGraph(args, hasBug) # Add the start node, which gets marked as being the entry node start = addGraphNode(tree, {"entry":"true"}) - lastNode = start - lastEdge = None - pat = re.compile(".*smack\.[c|h]$") - prevLineNo = -1 - prevColNo = -1 - # Loop through each trace - for jsonTrace in jsonTraces: + if hasBug and not args.pthread: + # Convert json string to json object + smackJson = json.loads(strJsonOutput) + # Get the failure node, and the list of trace entries to get there + jsonViolation = smackJson["failsAt"] + jsonTraces = smackJson["traces"] + + lastNode = start + lastEdge = None + pat = re.compile(".*smack\.[c|h]$") + prevLineNo = -1 + prevColNo = -1 + callStack = ['main'] + # Loop through each trace + for jsonTrace in jsonTraces: # Make sure it isn't a smack header file if not pat.match(jsonTrace["file"]): - # If current trace has same line & column number as previous trace, - # don't create new edge/node - just append assumption - if prevLineNo == jsonTrace["line"] and prevColNo == jsonTrace["column"]: - #if not jsonTrace["assumption"] == "": - if formatAssign(jsonTrace["description"]): - assumpNode = None - # Loop through the children to find the assumption node - for dataNode in list(lastEdge.iter()): - if dataNode.tag == "data" and dataNode.attrib["key"] == "assumption": - assumpNode = dataNode - break - if assumpNode == None: - #addKey(lastEdge, "assumption",formatAssign(str(jsonTrace["assumption"])) + ";") - addKey(lastEdge, "assumption",formatAssign(str(jsonTrace["description"])) + ";") - else: - #assumpNode.text = assumpNode.text + " " + formatAssign(str(jsonTrace["assumption"])) + ";" - assumpNode.text = assumpNode.text + " " + formatAssign(str(jsonTrace["description"])) + ";" - if "CALL" in jsonTrace["description"]: - if not "__VERIFIER_nondet_" in jsonTrace["description"] and not "__VERIFIER_assume" in jsonTrace["description"] and \ - not "$memset" in jsonTrace["description"] and not "$memcpy" in jsonTrace["description"]: - addKey(lastEdge, "enterFunction", str(jsonTrace["description"][len("CALL"):])) - #addKey(lastNode, "violation", "true") - if ("__VERIFIER_error" in jsonTrace["description"][len("CALL"):]): - vNodes =tree.find("graph").findall("node") - for vNode in vNodes: - if vNode.attrib["id"] == lastNode: - addKey(vNode, "violation", "true") - if "RETURN from" in jsonTrace["description"]: - attribs["returnFrom"] = str(jsonTrace["description"][len("RETURN from"):]) - else: - # Create new node and edge - newNode = addGraphNode(tree) - #print type(newNode) - #attribs = {"originline":str(jsonTrace["line"])} - attribs = {"startline":str(jsonTrace["line"])} - if formatAssign(jsonTrace["description"]): - #if not jsonTrace["assumption"] == "": - attribs["assumption"] = formatAssign(str(jsonTrace["description"])) + ";" - if "CALL" in jsonTrace["description"]: - attribs["enterFunction"] = str(jsonTrace["description"][len("CALL"):]) - #if ("__VERIFIER_error" in jsonTrace["description"][len("CALL")]): - # attribs["violation"] = "true" - if "RETURN from" in jsonTrace["description"]: - attribs["returnFrom"] = str(jsonTrace["description"][len("RETURN from"):]) - newEdge = addGraphEdge(tree, lastNode, newNode, attribs) - prevLineNo = jsonTrace["line"] - prevColNo = jsonTrace["column"] - lastNode = newNode - lastEdge = newEdge - + if formatAssign(jsonTrace["description"]): + # Create new node and edge + newNode = addGraphNode(tree) + attribs = {"startline":str(jsonTrace["line"])} + attribs["assumption"] = formatAssign(str(jsonTrace["description"])) + ";" + attribs["assumption.scope"] = callStack[-1] + newEdge = addGraphEdge(tree, lastNode, newNode, attribs) + prevLineNo = jsonTrace["line"] + prevColNo = jsonTrace["column"] + lastNode = newNode + lastEdge = newEdge + if "CALL" in jsonTrace["description"]: + # Add function to call stack + calledFunc = str(jsonTrace["description"][len("CALL "):]).strip() + if calledFunc.startswith("devirtbounce"): + print "Warning: calling function pointer dispatch procedure at line {0}".format(jsonTrace["line"]) + continue + callStack.append(calledFunc) + if (("__VERIFIER_error" in jsonTrace["description"][len("CALL"):]) or + ("__SMACK_overflow_false" in jsonTrace["description"][len("CALL"):]) or + ("__SMACK_check_overflow" in jsonTrace["description"][len("CALL"):])): + newNode = addGraphNode(tree) + # addGraphNode returns a string, so we had to search the graph to get the node that we want + vNodes =tree.find("graph").findall("node") + for vNode in vNodes: + if vNode.attrib["id"] == newNode: + addKey(vNode, "violation", "true") + attribs = {"startline":str(jsonTrace["line"])} + if not args.signed_integer_overflow: + attribs["enterFunction"] = callStack[-1] + addGraphEdge(tree, lastNode, newNode, attribs) + break + if "RETURN from" in jsonTrace["description"]: + returnedFunc = str(jsonTrace["description"][len("RETURN from "):]).strip() + if returnedFunc.startswith("devirtbounce"): + print "Warning: returning from function pointer dispatch procedure at line {0}".format(jsonTrace["line"]) + continue + if returnedFunc != callStack[-1]: + raise RuntimeError('Procedure Call/Return dismatch at line {0}. Call stack head: {1}, returning from: {2}'.format(jsonTrace["line"], callStack[-1], returnedFunc)) + callStack.pop() + print + print return prettify(tree.getroot()) diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py index bcb9cdec8..3005085b7 100644 --- a/share/smack/svcomp/utils.py +++ b/share/smack/svcomp/utils.py @@ -6,12 +6,15 @@ import smack.top import filters from toSVCOMPformat import smackJsonToXmlGraph +from random_testing import random_test def svcomp_frontend(args): """Generate Boogie code from SVCOMP-style C-language source(s).""" # enable static LLVM unroll pass args.static_unroll = True + # disable dynamic execution + args.execute = False if len(args.input_files) > 1: raise RuntimeError("Expected a single SVCOMP input file.") @@ -25,10 +28,22 @@ def svcomp_frontend(args): file_type, executable = filters.svcomp_filter(args.input_files[0]) if file_type == 'bitvector': args.bit_precise = True - #Should be safe to comment out - #if file_type == 'float': + args.bit_precise_pointers = True + if file_type == 'float': #sys.exit(smack.top.results(args)['unknown']) + args.float = True + args.bit_precise = True + args.bit_precise_pointers = True + #args.verifier = 'boogie' + args.time_limit = 890 + args.unroll = 100 args.execute = executable + else: + with open(args.input_files[0], "r") as sf: + sc = sf.read() + if 'unsigned char b:2' in sc: + args.bit_precise = True + #args.bit_precise_pointers = True name, ext = os.path.splitext(os.path.basename(args.input_files[0])) svcomp_process_file(args, name, ext) @@ -52,10 +67,13 @@ def svcomp_check_property(args): prop = f.read() if "valid-deref" in prop: args.memory_safety = True + elif "overflow" in prop: + args.signed_integer_overflow = True elif not "__VERIFIER_error" in prop: sys.exit(smack.top.results(args)['unknown']) def svcomp_process_file(args, name, ext): + args.orig_files = list(args.input_files) with open(args.input_files[0], 'r') as fi: s = fi.read() args.input_files[0] = smack.top.temporary_file(name, ext, args) @@ -65,10 +83,25 @@ def svcomp_process_file(args, name, ext): if args.memory_safety: s = re.sub(r'typedef long unsigned int size_t', r'typedef unsigned int size_t', s) - if len(s.split('\n')) < 60: - # replace all occurrences of 100000 with 10 + if args.float: + if re.search("fesetround|fegetround|InvSqrt|ccccdp-1",s): + sys.exit(smack.top.results(args)['unknown']) + + if args.signed_integer_overflow: + if re.search(r'argv=malloc', s): + args.bit_precise = True + args.bit_precise_pointers = True + + length = len(s.split('\n')) + if length < 60: + # replace all occurrences of 100000 with 10 and 15000 with 5 # Only target at small examples s = re.sub(r'100000', r'10', s) + s = re.sub(r'15000', r'5', s) + s = re.sub(r'i<=10000', r'i<=1', s) + elif length < 710 and 'dll_create_master' in s: + args.no_memory_splitting = True + #Remove any preprocessed declarations of pthread types #Also, if file contains 'pthread', set pthread mode s,args.pthread = filters.scrub_pthreads(s) @@ -77,10 +110,54 @@ def svcomp_process_file(args, name, ext): with open(args.input_files[0], 'w') as fo: fo.write(s) +def is_crappy_driver_benchmark(args, bpl): + if ("205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--rtl8150.ko-entry_point_true-unreach-call" in bpl or + "32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful" in bpl or + "32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--media--dvb-core--dvb-core.ko-ldv_main5_sequence_infinite_withcheck_stateful" in bpl or + "32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--seq--snd-seq.ko-ldv_main2_sequence_infinite_withcheck_stateful" in bpl or + "43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call" in bpl or + "linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-xen-netfront_true-unreach-call" in bpl or + "linux-3.14__complex_emg__linux-drivers-clk1__drivers-net-ethernet-ethoc_true-unreach-call" in bpl or + "linux-3.14__linux-alloc-spinlock__drivers-net-xen-netfront_true-unreach-call" in bpl or + "linux-3.14__linux-usb-dev__drivers-media-usb-hdpvr-hdpvr_true-unreach-call" in bpl or + "linux-4.2-rc1.tar.xz-32_7a-drivers--net--usb--r8152.ko-entry_point_true-unreach-call" in bpl or + "linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-ethernet-smsc-smsc911x_true-unreach-call" in bpl or + "linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call" in bpl or + "linux-4.2-rc1.tar.xz-43_2a-drivers--net--ppp--ppp_generic.ko-entry_point_true-unreach-call" in bpl): + if not args.quiet: + print("Stumbled upon a crappy device driver benchmark\n") + while (True): + pass + def verify_bpl_svcomp(args): """Verify the Boogie source file using SVCOMP-tuned heuristics.""" heurTrace = "\n\nHeuristics Info:\n" + # invoke boogie for floats + # I have to copy/paste part of verify_bpl + if args.float: + args.verifier = 'boogie' + boogie_command = ["boogie"] + boogie_command += [args.bpl_file] + boogie_command += ["/nologo", "/noinfer", "/doModSetAnalysis"] + boogie_command += ["/timeLimit:%s" % args.time_limit] + boogie_command += ["/errorLimit:%s" % args.max_violations] + boogie_command += ["/loopUnroll:%d" % args.unroll] + if args.bit_precise: + x = "bopt:" if args.verifier != 'boogie' else "" + boogie_command += ["/%sproverOpt:OPTIMIZE_FOR_BV=true" % x] + boogie_command += ["/%sz3opt:smt.relevancy=0" % x] + boogie_command += ["/%sz3opt:smt.bv.enable_int2bv=true" % x] + boogie_command += ["/%sboolControlVC" % x] + + if args.verifier_options: + boogie_command += args.verifier_options.split() + + boogie_output = smack.top.try_command(boogie_command, timeout=args.time_limit) + boogie_result = smack.top.verification_result(boogie_output) + write_error_file(args, boogie_result, boogie_output) + sys.exit(smack.top.results(args)[boogie_result]) + # If pthreads found, perform lock set analysis if args.pthread: lockpwn_command = ["lockpwn"] @@ -98,13 +175,20 @@ def verify_bpl_svcomp(args): with open(args.bpl_file, "r") as f: bpl = f.read() + is_crappy_driver_benchmark(args, bpl) + if args.pthread: - corral_command += ["/k:3"] - if not "qrcu_reader2" in bpl and not "__VERIFIER_atomic_take_write_lock" in bpl: + if "fib_bench" in bpl or "27_Boop_simple_vf_false-unreach-call" in bpl: + heurTrace += "Increasing context switch bound for certain pthread benchmarks.\n" + corral_command += ["/k:30"] + else: + corral_command += ["/k:3"] + if not "qrcu_reader2" in bpl and not "__VERIFIER_atomic_take_write_lock" in bpl and not "fib_bench" in bpl: corral_command += ["/cooperative"] else: corral_command += ["/k:1"] - corral_command += ["/di"] + if not args.memory_safety or not args.bit_precise: + corral_command += ["/di"] # we are not modeling strcpy if args.pthread and "strcpy" in bpl: @@ -119,16 +203,41 @@ def verify_bpl_svcomp(args): if not args.bit_precise and "ssl3_accept" in bpl and "s__s3__tmp__new_cipher__algorithms" in bpl: heurTrace += "ControlFlow benchmark detected. Setting loop unroll bar to 23.\n" loopUnrollBar = 23 - elif args.bit_precise and "__VERIFIER_nondet__Bool" in bpl: - heurTrace += "Sequentialized benchmark detected. Setting loop unroll bar to 10.\n" - loopUnrollBar = 10 + elif "s3_srvr.blast.10_false-unreach-call" in bpl or "s3_srvr.blast.15_false-unreach-call" in bpl: + heurTrace += "ControlFlow benchmark detected. Setting loop unroll bar to 23.\n" + loopUnrollBar = 23 + elif " node3" in bpl: + heurTrace += "Sequentialized benchmark detected. Setting loop unroll bar to 100.\n" + loopUnrollBar = 100 elif "calculate_output" in bpl: heurTrace += "ECA benchmark detected. Setting loop unroll bar to 15.\n" loopUnrollBar = 15 elif "ldv" in bpl: - heurTrace += "LDV benchmark detected. Setting loop unroll bar to 12.\n" - loopUnrollBar = 13 + if "linux-4.2-rc1.tar.xz-08_1a-drivers--staging--lustre--lustre--llite--llite_lloop.ko-entry_point_false-unreach-call" in bpl: + heurTrace += "Special LDV benchmark detected. Setting loop unroll bar to 32.\n" + loopUnrollBar = 32 + else: + heurTrace += "LDV benchmark detected. Setting loop unroll bar to 13.\n" + loopUnrollBar = 13 staticLoopBound = 64 + elif "standard_strcpy_false-valid-deref_ground_true-termination" in bpl or "960521-1_false-valid-free" in bpl or "960521-1_false-valid-deref" in bpl or "lockfree-3.3" in bpl: + heurTrace += "Memory safety benchmark detected. Setting loop unroll bar to 129.\n" + loopUnrollBar = 129 + elif "is_relaxed_prefix" in bpl: + heurTrace += "Benchmark relax_* detected. Setting loop unroll bar to 15.\n" + loopUnrollBar = 15 + elif "id_o1000_false-unreach-call" in bpl: + heurTrace += "Recursive benchmark detected. Setting loop unroll bar to 1024.\n" + loopUnrollBar = 1024 + elif args.memory_safety and "__main(argc:" in bpl: + heurTrace += "BusyBox memory safety benchmark detected. Setting loop unroll bar to 128.\n" + loopUnrollBar = 128 + elif args.signed_integer_overflow and "__main(argc:" in bpl: + heurTrace += "BusyBox overflows benchmark detected. Setting loop unroll bar to 11.\n" + loopUnrollBar = 11 + elif args.signed_integer_overflow and "jain" in bpl: + heurTrace += "Infinite loop in overflow benchmark. Setting loop unroll bar to INT_MAX.\n" + loopUnrollBar = 2**31 - 1 if not "forall" in bpl: heurTrace += "No quantifiers detected. Setting z3 relevancy to 0.\n" @@ -151,16 +260,8 @@ def verify_bpl_svcomp(args): verifier_output = smack.top.try_command(command, timeout=time_limit) result = smack.top.verification_result(verifier_output) - if result == 'error' or result == 'invalid-deref' or result == 'invalid-free' or result == 'invalid-memtrack': #normal inlining + if result == 'error' or result == 'invalid-deref' or result == 'invalid-free' or result == 'invalid-memtrack' or result == 'overflow': #normal inlining heurTrace += "Found a bug during normal inlining.\n" - # Generate error trace and exit - if args.error_file: - if args.language == 'svcomp': - error = smackJsonToXmlGraph(smack.top.smackdOutput(verifier_output)) - else: - error = smack.top.error_trace(verifier_output, args) - with open(args.error_file, 'w') as f: - f.write(error) if not args.quiet: error = smack.top.error_trace(verifier_output, args) @@ -171,28 +272,38 @@ def verify_bpl_svcomp(args): heurTrace += "Determining result based on how far we unrolled.\n" # If we managed to unroll more than loopUnrollBar times, then return verified # First remove exhausted loop bounds generated during max static loop bound computation - verifier_output = re.sub(re.compile('.*Verifying program while tracking', re.DOTALL), - 'Verifying program while tracking', verifier_output) - it = re.finditer(r'Exhausted recursion bound of ([1-9]\d*)', verifier_output) unrollMax = 0 - for match in it: - if int(match.group(1)) > unrollMax: - unrollMax = int(match.group(1)) + if 'Verifying program while tracking' in verifier_output: + verifier_output = re.sub(re.compile('.*Verifying program while tracking', re.DOTALL), + 'Verifying program while tracking', verifier_output) + it = re.finditer(r'Exhausted recursion bound of ([1-9]\d*)', verifier_output) + for match in it: + if int(match.group(1)) > unrollMax: + unrollMax = int(match.group(1)) + else: + heurTrace += "Corral didn't even start verification.\n" if unrollMax >= loopUnrollBar: heurTrace += "Unrolling made it to a recursion bound of " heurTrace += str(unrollMax) + ".\n" heurTrace += "Reporting benchmark as 'verified'.\n" - if args.execute: + if args.execute and not args.pthread: heurTrace += "Hold on, let's see the execution result.\n" execution_result = run_binary(args) heurTrace += "Excecution result is " + execution_result + '\n' - if execution_result == 'false': - heurTrace += "Oops, execution result says no.\n" + if execution_result != 'true': + heurTrace += "Oops, execution result says {0}.\n".format(execution_result) if not args.quiet: print(heurTrace + "\n") sys.exit(smack.top.results(args)['unknown']) + 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']) if not args.quiet: print(heurTrace + "\n") + write_error_file(args, 'verified', verifier_output) sys.exit(smack.top.results(args)['verified']) else: heurTrace += "Only unrolled " + str(unrollMax) + " times.\n" @@ -200,6 +311,7 @@ def verify_bpl_svcomp(args): heurTrace += "Reporting 'timeout'.\n" if not args.quiet: print(heurTrace + "\n") + sys.stdout.flush() # Sleep for 1000 seconds, so svcomp shows timeout instead of unknown time.sleep(1000) elif result == 'verified': #normal inlining @@ -208,8 +320,25 @@ def verify_bpl_svcomp(args): heurTrace += "Normal inlining returned 'unknown'. See errors above.\n" if not args.quiet: print(heurTrace + "\n") + write_error_file(args, result, verifier_output) sys.exit(smack.top.results(args)[result]) +def write_error_file(args, status, verifier_output): + if args.memory_safety or status == 'timeout' or status == 'unknown': + return + hasBug = (status != 'verified') + #if not hasBug: + # return + if args.error_file: + error = None + if args.language == 'svcomp': + error = smackJsonToXmlGraph(smack.top.smackdOutput(verifier_output), args, hasBug) + elif hasBug: + error = smack.top.error_trace(verifier_output, args) + if error is not None: + with open(args.error_file, 'w') as f: + f.write(error) + def run_binary(args): #process the file to make it runnable with open(args.input_files[0], 'r') as fi: @@ -251,7 +380,8 @@ def run_binary(args): if re.search(r'Assertion.*failed', err): return 'false' else: - print 'execution error' + print 'Execution error' + print err return 'unknown' else: return 'true' diff --git a/share/smack/top.py b/share/smack/top.py index e198a0b1a..13dfeb3d2 100755 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -14,7 +14,7 @@ from svcomp.utils import svcomp_frontend from svcomp.utils import verify_bpl_svcomp -VERSION = '1.7.0' +VERSION = '1.7.1' temporary_files = [] def frontends(): @@ -39,6 +39,7 @@ def results(args): 'invalid-deref': 'SMACK found an error: invalid pointer dereference.', 'invalid-free': 'SMACK found an error: invalid memory deallocation.', 'invalid-memtrack': 'SMACK found an error: memory leak.', + 'overflow': 'SMACK found an error: signed integer overflow.', 'timeout': 'SMACK timed out.', 'unknown': 'SMACK result is unknown.' } @@ -141,6 +142,9 @@ def arguments(): translate_group.add_argument('--memory-safety', action='store_true', default=False, help='enable memory safety checks') + translate_group.add_argument('--signed-integer-overflow', action='store_true', default=False, + help='enable signed integer overflow checks') + verifier_group = parser.add_argument_group('verifier options') verifier_group.add_argument('--verifier', @@ -294,12 +298,13 @@ def smack_headers(): def smack_lib(): return os.path.join(smack_root(), 'share', 'smack', 'lib') -def default_clang_compile_command(args): +def default_clang_compile_command(args, lib = False): cmd = ['clang', '-c', '-emit-llvm', '-O0', '-g', '-gcolumn-info'] cmd += ['-I' + smack_headers()] cmd += args.clang_options.split() cmd += ['-DMEMORY_MODEL_' + args.mem_mod.upper().replace('-','_')] if args.memory_safety: cmd += ['-DMEMORY_SAFETY'] + if args.signed_integer_overflow: cmd += (['-ftrapv'] if not lib else ['-DSIGNED_INTEGER_OVERFLOW_CHECK']) if args.float: cmd += ['-DFLOAT_ENABLED'] return cmd @@ -309,11 +314,11 @@ def build_libs(args): libs = ['smack.c'] if args.pthread: - libs += ['pthread.c', 'spinlock.c'] + libs += ['pthread.c'] for c in map(lambda c: os.path.join(smack_lib(), c), libs): bc = temporary_file(os.path.splitext(os.path.basename(c))[0], '.bc', args) - try_command(default_clang_compile_command(args) + ['-o', bc, c]) + try_command(default_clang_compile_command(args, True) + ['-o', bc, c]) bitcodes.append(bc) return bitcodes @@ -391,6 +396,7 @@ def llvm_to_bpl(args): if args.no_byte_access_inference: cmd += ['-no-byte-access-inference'] if args.no_memory_splitting: cmd += ['-no-memory-splitting'] if args.memory_safety: cmd += ['-memory-safety'] + if args.signed_integer_overflow: cmd += ['-signed-integer-overflow'] if args.float: cmd += ['-float'] try_command(cmd, console=True) annotate_bpl(args) @@ -400,7 +406,7 @@ def procedure_annotation(name, args): return "{:entrypoint}" elif re.match("|".join(inlined_procedures()).replace("$","\$"), name): return "{:inline 1}" - elif args.verifier == 'boogie': + elif args.verifier == 'boogie' or args.float: return ("{:inline %s}" % args.unroll) else: return "" @@ -430,6 +436,8 @@ def verification_result(verifier_output): return 'invalid-free' elif re.search(r'ASSERTION FAILS assert {:valid_memtrack}', verifier_output): return 'invalid-memtrack' + elif re.search(r'ASSERTION FAILS assert {:overflow}', verifier_output): + return 'overflow' else: listCall = re.findall(r'\(CALL .+\)', verifier_output) if len(listCall) > 0 and re.search(r'free_', listCall[len(listCall)-1]): @@ -491,7 +499,7 @@ def verify_bpl(args): print results(args)[result] else: - if result == 'error' or result == 'invalid-deref' or result == 'invalid-free' or result == 'invalid-memtrack': + if result == 'error' or result == 'invalid-deref' or result == 'invalid-free' or result == 'invalid-memtrack' or result == 'overflow': error = error_trace(verifier_output, args) if args.error_file: diff --git a/svcomp/bench/src/benchexec/benchexec/tools/smack_benchexec_driver.py b/svcomp/bench/src/benchexec/benchexec/tools/smack_benchexec_driver.py index d90fccad9..b4981c747 100644 --- a/svcomp/bench/src/benchexec/benchexec/tools/smack_benchexec_driver.py +++ b/svcomp/bench/src/benchexec/benchexec/tools/smack_benchexec_driver.py @@ -35,7 +35,7 @@ def version(self, executable): Sets the version number for SMACK, which gets displayed in the "Tool" row in BenchExec table headers. """ - return '1.7.0' + return '1.7.1' def name(self): """ diff --git a/test/pthread/spinlock.c b/test/pthread/spinlock.c deleted file mode 100644 index 11f20f38b..000000000 --- a/test/pthread/spinlock.c +++ /dev/null @@ -1,31 +0,0 @@ -// Tests spin_lock_init() function - -// @expect verified - -#include -#include -#include - -int z = 1; - -void *t1(void *arg) { - spinlock_t* lock = arg; - spin_lock(lock); - z++; - spin_unlock(lock); -} - -int main() { - - spinlock_t lock; - spin_lock_init(&lock); - - pthread_t tid1; - - pthread_create(&tid1, 0, t1, &lock); - spin_lock(&lock); - z++; - spin_unlock(&lock); - pthread_join(tid1, 0); - assert(z == 3); -} diff --git a/test/pthread/spinlock2.c b/test/pthread/spinlock2.c deleted file mode 100644 index c27e79e3c..000000000 --- a/test/pthread/spinlock2.c +++ /dev/null @@ -1,31 +0,0 @@ -// Tests DEFINE_SPINLOCK() macro - -// @expect verified - -#include -#include -#include - -DEFINE_SPINLOCK(lock); - -int x = 1; - -void *t1(void *arg) { - spin_lock(&lock); - x++; - spin_unlock(&lock); -} - -int main() { - - pthread_t tid1, tid2; - - pthread_create(&tid1, 0, t1, 0); - pthread_create(&tid2, 0, t1, 0); - spin_lock(&lock); - x++; - spin_unlock(&lock); - pthread_join(tid1, 0); - pthread_join(tid2, 0); - assert(x == 4); -} diff --git a/test/pthread/spinlock2_fail.c b/test/pthread/spinlock2_fail.c deleted file mode 100644 index 269c069cd..000000000 --- a/test/pthread/spinlock2_fail.c +++ /dev/null @@ -1,29 +0,0 @@ -// Tests DEFINE_SPINLOCK() macro - -// @expect error - -#include -#include -#include - -DEFINE_SPINLOCK(lock); - -int x = 1; - -void *t1(void *arg) { - x++; -} - -int main() { - - pthread_t tid1, tid2; - - pthread_create(&tid1, 0, t1, 0); - pthread_create(&tid2, 0, t1, 0); - spin_lock(&lock); - x++; - spin_unlock(&lock); - pthread_join(tid1, 0); - pthread_join(tid2, 0); - assert(x == 4); -} diff --git a/test/pthread/spinlock3.c b/test/pthread/spinlock3.c deleted file mode 100644 index 3ae26ceb4..000000000 --- a/test/pthread/spinlock3.c +++ /dev/null @@ -1,37 +0,0 @@ -// Tests SPIN_LOCK_UNLOCKED macro - -// @expect verified - -#include -#include -#include - -spinlock_t lock = SPIN_LOCK_UNLOCKED; - -int x = 1; - -void *t1(void *arg) { - spin_lock(&lock); - x++; - spin_unlock(&lock); -} - -void *t2(void *arg) { - spin_lock(&lock); - x++; - spin_unlock(&lock); -} - -int main() { - - pthread_t tid1, tid2; - - pthread_create(&tid1, 0, t1, 0); - pthread_create(&tid2, 0, t2, 0); - spin_lock(&lock); - x++; - spin_unlock(&lock); - pthread_join(tid1, 0); - pthread_join(tid2, 0); - assert(x == 4); -} diff --git a/test/pthread/spinlock3_fail.c b/test/pthread/spinlock3_fail.c deleted file mode 100644 index d4bf034f4..000000000 --- a/test/pthread/spinlock3_fail.c +++ /dev/null @@ -1,35 +0,0 @@ -// Tests SPIN_LOCK_UNLOCKED macro - -// @expect error - -#include -#include -#include - -spinlock_t lock = SPIN_LOCK_UNLOCKED; - -int x = 1; - -void *t1(void *arg) { - spin_lock(&lock); - x++; - spin_unlock(&lock); -} - -void *t2(void *arg) { - x++; -} - -int main() { - - pthread_t tid1, tid2; - - pthread_create(&tid1, 0, t1, 0); - pthread_create(&tid2, 0, t2, 0); - spin_lock(&lock); - x++; - spin_unlock(&lock); - pthread_join(tid1, 0); - pthread_join(tid2, 0); - assert(x == 4); -} diff --git a/test/pthread/spinlock_fail.c b/test/pthread/spinlock_fail.c deleted file mode 100644 index 76dfbbca4..000000000 --- a/test/pthread/spinlock_fail.c +++ /dev/null @@ -1,29 +0,0 @@ -// Tests spin_lock_init() function - -// @expect error - -#include -#include -#include - -int z = 1; - -void *t1(void *arg) { - spinlock_t* lock = arg; - spin_lock(lock); - z++; - spin_unlock(lock); -} - -int main() { - - spinlock_t lock; - spin_lock_init(&lock); - - pthread_t tid1; - - pthread_create(&tid1, 0, t1, &lock); - z++; - pthread_join(tid1, 0); - assert(z == 3); -} diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp index 1918dd309..09af791aa 100644 --- a/tools/llvm2bpl/llvm2bpl.cpp +++ b/tools/llvm2bpl/llvm2bpl.cpp @@ -32,6 +32,7 @@ #include "smack/ExtractContracts.h" #include "smack/SimplifyLibCalls.h" #include "smack/MemorySafetyChecker.h" +#include "smack/SignedIntegerOverflowChecker.h" static llvm::cl::opt InputFilename(llvm::cl::Positional, llvm::cl::desc(""), @@ -53,6 +54,10 @@ static llvm::cl::opt DefaultDataLayout("default-data-layout", llvm::cl::desc("data layout string to use if not specified by module"), llvm::cl::init(""), llvm::cl::value_desc("layout-string")); +static llvm::cl::opt +SignedIntegerOverflow("signed-integer-overflow", llvm::cl::desc("Enable signed integer overflow checks"), + llvm::cl::init(false)); + std::string filenamePrefix(const std::string &str) { return str.substr(0, str.find_last_of(".")); } @@ -101,7 +106,7 @@ int main(int argc, char **argv) { llvm::legacy::PassManager pass_manager; pass_manager.add(llvm::createLowerSwitchPass()); - pass_manager.add(llvm::createCFGSimplificationPass()); + //pass_manager.add(llvm::createCFGSimplificationPass()); pass_manager.add(llvm::createInternalizePass()); pass_manager.add(llvm::createPromoteMemoryToRegisterPass()); @@ -127,6 +132,9 @@ int main(int argc, char **argv) { pass_manager.add(new smack::MemorySafetyChecker()); } + if (SignedIntegerOverflow) + pass_manager.add(new smack::SignedIntegerOverflowChecker()); + std::vector files; if (!FinalIrFilename.empty()) {