From de1ae1724a949b61788c85a2e80b8ae504a34d43 Mon Sep 17 00:00:00 2001 From: radl97 Date: Fri, 12 Feb 2021 19:08:49 +0100 Subject: [PATCH 01/21] Add support for LLVM11, breaks 9 currently --- CMakeLists.txt | 2 +- .../gazer/LLVM/Automaton/SpecialFunctions.h | 8 ++--- include/gazer/LLVM/LLVMFrontend.h | 2 ++ .../LLVM/Memory/MemoryInstructionHandler.h | 4 +-- include/gazer/LLVM/Memory/MemoryObject.h | 16 +++++----- include/gazer/LLVM/Memory/MemorySSA.h | 4 +-- include/gazer/Support/GrowingStackAllocator.h | 3 +- src/Core/Expr/ExprPrinter.cpp | 8 ++--- src/LLVM/Automaton/ExtensionPoints.cpp | 2 +- src/LLVM/Automaton/FunctionToCfa.h | 1 + src/LLVM/Automaton/ModuleToAutomata.cpp | 4 +-- src/LLVM/Automaton/SpecialFunctions.cpp | 10 +++---- src/LLVM/ClangFrontend.cpp | 6 ++-- src/LLVM/FrontendConfig.cpp | 2 +- .../Instrumentation/MarkFunctionEntries.cpp | 8 ++--- src/LLVM/LLVMTraceBuilder.cpp | 12 ++++---- src/LLVM/Memory/FlatMemoryModel.cpp | 17 ++++++----- src/LLVM/Memory/HavocMemoryModel.cpp | 2 +- src/LLVM/Memory/MemoryObject.cpp | 2 +- src/LLVM/Memory/MemorySSA.cpp | 12 ++++---- src/LLVM/Transform/Inline.cpp | 15 +++++----- .../Transform/InlineGlobalVariablesPass.cpp | 3 +- src/LLVM/Transform/LiftErrorsPass.cpp | 29 ++++++++++--------- src/LLVM/Transform/NormalizeVerifierCalls.cpp | 10 +++---- src/LLVM/Transform/TransformUtils.cpp | 2 +- src/SolverZ3/Z3Solver.cpp | 12 ++++---- src/Support/Runtime.cpp | 2 +- src/Support/SExpr.cpp | 2 +- tools/gazer-bmc/gazer-bmc.cpp | 1 + tools/gazer-cfa/gazer-cfa.cpp | 1 + tools/gazer-theta/gazer-theta.cpp | 3 +- tools/gazer-theta/lib/ThetaCfaGenerator.cpp | 4 +-- 32 files changed, 111 insertions(+), 98 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 5a6fc7dd..66a91f67 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -58,7 +58,7 @@ if (GAZER_ENABLE_COVERAGE) endif() # Get LLVM -find_package(LLVM 9.0 REQUIRED CONFIG) +find_package(LLVM REQUIRED CONFIG) message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}") message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}") diff --git a/include/gazer/LLVM/Automaton/SpecialFunctions.h b/include/gazer/LLVM/Automaton/SpecialFunctions.h index fdc2f624..7adcea19 100644 --- a/include/gazer/LLVM/Automaton/SpecialFunctions.h +++ b/include/gazer/LLVM/Automaton/SpecialFunctions.h @@ -29,7 +29,7 @@ namespace gazer class SpecialFunctionHandler { public: - using HandlerFuncTy = std::function; + using HandlerFuncTy = std::function; enum MemoryBehavior { @@ -44,7 +44,7 @@ class SpecialFunctionHandler : mHandlerFunction(function), mMemory(memory) {} - void operator()(llvm::ImmutableCallSite cs, llvm2cfa::GenerationStepExtensionPoint& ep) const + void operator()(const llvm::CallBase* cs, llvm2cfa::GenerationStepExtensionPoint& ep) const { return mHandlerFunction(cs, ep); } @@ -66,11 +66,11 @@ class SpecialFunctions llvm::StringRef name, SpecialFunctionHandler::HandlerFuncTy function, SpecialFunctionHandler::MemoryBehavior memory = SpecialFunctionHandler::Memory_Default); - bool handle(llvm::ImmutableCallSite cs, llvm2cfa::GenerationStepExtensionPoint& ep) const; + bool handle(const llvm::CallBase* cs, llvm2cfa::GenerationStepExtensionPoint& ep) const; // Some handlers for common cases public: - static void handleAssume(llvm::ImmutableCallSite cs, llvm2cfa::GenerationStepExtensionPoint& ep); + static void handleAssume(const llvm::CallBase* cs, llvm2cfa::GenerationStepExtensionPoint& ep); private: llvm::StringMap mHandlers; diff --git a/include/gazer/LLVM/LLVMFrontend.h b/include/gazer/LLVM/LLVMFrontend.h index 50fbc638..8db7cc3f 100644 --- a/include/gazer/LLVM/LLVMFrontend.h +++ b/include/gazer/LLVM/LLVMFrontend.h @@ -23,9 +23,11 @@ #include "gazer/LLVM/LLVMFrontendSettings.h" #include "gazer/Verifier/VerificationAlgorithm.h" +#include "llvm/Analysis/CallGraph.h" #include #include #include +#include "llvm/Support/ManagedStatic.h" namespace gazer { diff --git a/include/gazer/LLVM/Memory/MemoryInstructionHandler.h b/include/gazer/LLVM/Memory/MemoryInstructionHandler.h index 81520b36..2e4a0851 100644 --- a/include/gazer/LLVM/Memory/MemoryInstructionHandler.h +++ b/include/gazer/LLVM/Memory/MemoryInstructionHandler.h @@ -129,7 +129,7 @@ class MemoryInstructionHandler /// The parameters \p inputAssignments and \p outputAssignments will be placed /// on the resulting automaton call _after_ the regular input/output assignments. virtual void handleCall( - llvm::CallSite call, + llvm::CallBase* call, llvm2cfa::GenerationStepExtensionPoint& callerEp, llvm2cfa::AutomatonInterfaceExtensionPoint& calleeEp, llvm::SmallVectorImpl& inputAssignments, @@ -142,7 +142,7 @@ class MemoryInstructionHandler /// function, the translation process already generates a havoc assignment for /// it _before_ calling this function. virtual void handleExternalCall( - llvm::CallSite call, llvm2cfa::GenerationStepExtensionPoint& ep) {} + llvm::CallBase* call, llvm2cfa::GenerationStepExtensionPoint& ep) {} // Memory safety predicates //==--------------------------------------------------------------------==// diff --git a/include/gazer/LLVM/Memory/MemoryObject.h b/include/gazer/LLVM/Memory/MemoryObject.h index bf6470e7..a92d13bd 100644 --- a/include/gazer/LLVM/Memory/MemoryObject.h +++ b/include/gazer/LLVM/Memory/MemoryObject.h @@ -26,7 +26,7 @@ #include #include #include -#include +#include #include @@ -334,7 +334,7 @@ class StoreDef : public InstructionAnnotationDef class CallDef : public InstructionAnnotationDef { public: - CallDef(MemoryObject* object, unsigned int version, llvm::CallSite call) + CallDef(MemoryObject* object, unsigned int version, llvm::CallBase* call) : InstructionAnnotationDef(object, version, MemoryObjectDef::Call), mCall(call) {} @@ -342,13 +342,13 @@ class CallDef : public InstructionAnnotationDef return def->getKind() == MemoryObjectDef::Call; } - llvm::Instruction* getInstruction() const override { return mCall.getInstruction(); } + llvm::Instruction* getInstruction() const override { return mCall; } protected: void doPrint(llvm::raw_ostream& os) const override; private: - llvm::CallSite mCall; + llvm::CallBase* mCall; }; class LiveOnEntryDef : public BlockAnnotationDef @@ -445,12 +445,12 @@ class LoadUse : public MemoryObjectUse class CallUse : public MemoryObjectUse { public: - CallUse(MemoryObject* object, llvm::CallSite callSite) + CallUse(MemoryObject* object, llvm::CallBase* callSite) : MemoryObjectUse(object, MemoryObjectUse::Call), mCallSite(callSite) {} - llvm::Instruction* getInstruction() const override { return mCallSite.getInstruction(); } - llvm::CallSite getCallSite() const { return mCallSite; } + llvm::Instruction* getInstruction() const override { return mCallSite; } + llvm::CallBase* getCallSite() const { return mCallSite; } void print(llvm::raw_ostream& os) const override; @@ -458,7 +458,7 @@ class CallUse : public MemoryObjectUse return use->getKind() == MemoryObjectUse::Call; } private: - llvm::CallSite mCallSite; + llvm::CallBase* mCallSite; }; class RetUse : public MemoryObjectUse diff --git a/include/gazer/LLVM/Memory/MemorySSA.h b/include/gazer/LLVM/Memory/MemorySSA.h index 1821bdf9..65db00bc 100644 --- a/include/gazer/LLVM/Memory/MemorySSA.h +++ b/include/gazer/LLVM/Memory/MemorySSA.h @@ -144,10 +144,10 @@ class MemorySSABuilder ); memory::AllocaDef* createAllocaDef(MemoryObject* object, llvm::AllocaInst& alloca); memory::StoreDef* createStoreDef(MemoryObject* object, llvm::StoreInst& inst); - memory::CallDef* createCallDef(MemoryObject* object, llvm::CallSite call); + memory::CallDef* createCallDef(MemoryObject* object, llvm::CallBase* call); memory::LoadUse* createLoadUse(MemoryObject* object, llvm::LoadInst& load); - memory::CallUse* createCallUse(MemoryObject* object, llvm::CallSite call); + memory::CallUse* createCallUse(MemoryObject* object, llvm::CallBase* call); memory::RetUse* createReturnUse(MemoryObject* object, llvm::ReturnInst& ret); std::unique_ptr build(); diff --git a/include/gazer/Support/GrowingStackAllocator.h b/include/gazer/Support/GrowingStackAllocator.h index 7cabe74c..ad989982 100644 --- a/include/gazer/Support/GrowingStackAllocator.h +++ b/include/gazer/Support/GrowingStackAllocator.h @@ -49,7 +49,8 @@ class GrowingStackAllocator : public llvm::AllocatorBase= size); if (size > SlabSize) { diff --git a/src/Core/Expr/ExprPrinter.cpp b/src/Core/Expr/ExprPrinter.cpp index 9b4f5ed6..1a8f8dea 100644 --- a/src/Core/Expr/ExprPrinter.cpp +++ b/src/Core/Expr/ExprPrinter.cpp @@ -299,20 +299,20 @@ class InfixPrintVisitor : public ExprWalker bv->getValue().toStringSigned(buffer, mRadix); rso << "bv" << bv->getType().getWidth(); - return rso.str(); + return rso.str().str(); } if (auto fl = llvm::dyn_cast(expr)) { fl->getValue().toString(buffer); rso << "fp" << fl->getType().getWidth(); - return rso.str(); + return rso.str().str(); } if (auto rl = llvm::dyn_cast(expr)) { rso << rl->getValue().numerator() << "%" << rl->getValue().denominator(); - return rso.str(); + return rso.str().str(); } if (auto al = llvm::dyn_cast(expr)) { @@ -336,7 +336,7 @@ class InfixPrintVisitor : public ExprWalker rso << llvm::join(orderedElems, ", "); rso << "]"; - return rso.str(); + return rso.str().str(); } llvm_unreachable("Unknown literal expression kind."); diff --git a/src/LLVM/Automaton/ExtensionPoints.cpp b/src/LLVM/Automaton/ExtensionPoints.cpp index 7da09b9d..a03b812a 100644 --- a/src/LLVM/Automaton/ExtensionPoints.cpp +++ b/src/LLVM/Automaton/ExtensionPoints.cpp @@ -41,7 +41,7 @@ std::string GenerationContext::uniqueName(const llvm::Twine& base) name = (base + llvm::Twine(mTmp++)).toStringRef(buffer); } - return buffer.str(); + return buffer.str().str(); } void CfaGenInfo::addVariableToContext(ValueOrMemoryObject value, Variable* variable) diff --git a/src/LLVM/Automaton/FunctionToCfa.h b/src/LLVM/Automaton/FunctionToCfa.h index d26cb091..6b7a7beb 100644 --- a/src/LLVM/Automaton/FunctionToCfa.h +++ b/src/LLVM/Automaton/FunctionToCfa.h @@ -34,6 +34,7 @@ #include #include #include +#include #include diff --git a/src/LLVM/Automaton/ModuleToAutomata.cpp b/src/LLVM/Automaton/ModuleToAutomata.cpp index 7bc73594..216decc3 100644 --- a/src/LLVM/Automaton/ModuleToAutomata.cpp +++ b/src/LLVM/Automaton/ModuleToAutomata.cpp @@ -195,7 +195,7 @@ static std::string getLoopName(const llvm::Loop* loop, unsigned& loopCount, llvm const BasicBlock* header = loop->getHeader(); assert(header != nullptr && "Loop without a loop header?"); - std::string name = prefix; + std::string name = prefix.str(); name += '/'; if (header->hasName()) { name += header->getName(); @@ -273,7 +273,7 @@ void ModuleToCfa::createAutomata() auto& memoryInstHandler = mMemoryModel.getMemoryInstructionHandler(function); - Cfa* cfa = mSystem->createCfa(function.getName()); + Cfa* cfa = mSystem->createCfa(function.getName().str()); LLVM_DEBUG(llvm::dbgs() << "Created CFA " << cfa->getName() << "\n"); DenseSet visitedBlocks; diff --git a/src/LLVM/Automaton/SpecialFunctions.cpp b/src/LLVM/Automaton/SpecialFunctions.cpp index adc4afee..cbc34589 100644 --- a/src/LLVM/Automaton/SpecialFunctions.cpp +++ b/src/LLVM/Automaton/SpecialFunctions.cpp @@ -41,13 +41,13 @@ void SpecialFunctions::registerHandler( assert(result.second && "Attempt to register duplicate handler!"); } -auto SpecialFunctions::handle(llvm::ImmutableCallSite cs, llvm2cfa::GenerationStepExtensionPoint& ep) const +auto SpecialFunctions::handle(const llvm::CallBase* cs, llvm2cfa::GenerationStepExtensionPoint& ep) const -> bool { - assert(cs.getCalledFunction() != nullptr); + assert(cs->getCalledFunction() != nullptr); // Check if we have an appropriate handler - auto it = mHandlers.find(cs.getCalledFunction()->getName()); + auto it = mHandlers.find(cs->getCalledFunction()->getName()); if (it == mHandlers.end()) { return false; } @@ -59,9 +59,9 @@ auto SpecialFunctions::handle(llvm::ImmutableCallSite cs, llvm2cfa::GenerationSt // Default handler implementations //===----------------------------------------------------------------------===// -void SpecialFunctions::handleAssume(llvm::ImmutableCallSite cs, llvm2cfa::GenerationStepExtensionPoint& ep) +void SpecialFunctions::handleAssume(const llvm::CallBase* cs, llvm2cfa::GenerationStepExtensionPoint& ep) { - const llvm::Value* arg = cs.getArgOperand(0); + const llvm::Value* arg = cs->getArgOperand(0); ExprPtr assumeExpr = ep.getAsOperand(arg); ep.splitCurrentTransition(assumeExpr); diff --git a/src/LLVM/ClangFrontend.cpp b/src/LLVM/ClangFrontend.cpp index 97bb8aa5..0012ee5e 100644 --- a/src/LLVM/ClangFrontend.cpp +++ b/src/LLVM/ClangFrontend.cpp @@ -180,7 +180,7 @@ auto gazer::ClangCompileAndLink( for (llvm::StringRef inputFile : files) { if (inputFile.endswith_lower(".bc") || inputFile.endswith_lower(".ll")) { - bitcodeFiles.push_back(inputFile); + bitcodeFiles.push_back(inputFile.str()); continue; } @@ -210,7 +210,7 @@ auto gazer::ClangCompileAndLink( return nullptr; } - bitcodeFiles.push_back(outputPath.str()); + bitcodeFiles.push_back(outputPath.str().str()); } // Run llvm-link @@ -236,7 +236,7 @@ using namespace gazer; void ClangOptions::addSanitizerFlag(llvm::StringRef flag) { - mSanitizerFlags.insert(flag); + mSanitizerFlags.insert(flag.str()); } void ClangOptions::createArgumentList(std::vector& args) diff --git a/src/LLVM/FrontendConfig.cpp b/src/LLVM/FrontendConfig.cpp index 8ed56d62..2793c344 100644 --- a/src/LLVM/FrontendConfig.cpp +++ b/src/LLVM/FrontendConfig.cpp @@ -110,7 +110,7 @@ void FrontendConfig::createChecks(std::vector>& checks) } for (llvm::StringRef name : fragments) { - auto it = mFactories.find(name); + auto it = mFactories.find(name.str()); if (it == mFactories.end()) { emit_warning("unknown check '%s', parameter ignored", name.data()); continue; diff --git a/src/LLVM/Instrumentation/MarkFunctionEntries.cpp b/src/LLVM/Instrumentation/MarkFunctionEntries.cpp index 0d2a183f..b890c7f7 100644 --- a/src/LLVM/Instrumentation/MarkFunctionEntries.cpp +++ b/src/LLVM/Instrumentation/MarkFunctionEntries.cpp @@ -46,7 +46,7 @@ class MarkFunctionEntriesPass : public ModulePass bool runOnModule(Module& module) override { LLVMContext& context = module.getContext(); - llvm::DenseMap returnValueMarks; + llvm::DenseMap returnValueMarks; auto retMarkVoid = GazerIntrinsic::GetOrInsertFunctionReturnVoid(module); auto callReturnedMark = GazerIntrinsic::GetOrInsertFunctionCallReturned(module); @@ -92,15 +92,15 @@ class MarkFunctionEntriesPass : public ModulePass llvm::Value* retValue = ret->getReturnValue(); if (retValue != nullptr) { auto retValueTy = retValue->getType(); - llvm::Value* retMark = returnValueMarks[retValueTy]; - if (retMark == nullptr) { + llvm::FunctionCallee retMark = returnValueMarks[retValueTy]; + if (retMark.getCallee() == nullptr) { std::string nameBuffer; llvm::raw_string_ostream rso(nameBuffer); retValueTy->print(rso, false, true); rso.flush(); // Insert a new function for this mark type - retMark = GazerIntrinsic::GetOrInsertFunctionReturnValue(module, retValueTy).getCallee(); + retMark = GazerIntrinsic::GetOrInsertFunctionReturnValue(module, retValueTy); returnValueMarks[retValueTy] = retMark; } diff --git a/src/LLVM/LLVMTraceBuilder.cpp b/src/LLVM/LLVMTraceBuilder.cpp index 269586e7..4d7c44de 100644 --- a/src/LLVM/LLVMTraceBuilder.cpp +++ b/src/LLVM/LLVMTraceBuilder.cpp @@ -236,7 +236,7 @@ auto LLVMTraceBuilder::build( } events.push_back(std::make_unique( - diSP->getName(), + diSP->getName().str(), args )); } else if (callee->getName() == GazerIntrinsic::FunctionReturnVoidName) { @@ -245,7 +245,7 @@ auto LLVMTraceBuilder::build( ); events.push_back(std::make_unique( - diSP->getName(), + diSP->getName().str(), nullptr )); } else if (callee->getName().startswith(GazerIntrinsic::FunctionReturnValuePrefix)) { @@ -255,7 +255,7 @@ auto LLVMTraceBuilder::build( auto expr = this->getLiteralFromValue(loc->getAutomaton(), call->getArgOperand(1), currentVals); events.push_back(std::make_unique( - diSP->getName(), + diSP->getName().str(), expr )); } else if (callee->getName() == GazerIntrinsic::FunctionCallReturnedName) { @@ -264,7 +264,7 @@ auto LLVMTraceBuilder::build( ); events.push_back(std::make_unique( - diSP->getName() + diSP->getName().str() )); } else if (callee->getName().startswith("gazer.undef_value.")) { // Register that we have passed through an undef value. @@ -299,7 +299,7 @@ auto LLVMTraceBuilder::build( } events.push_back(std::make_unique( - callee->getName(), + callee->getName().str(), expr, std::vector>(), location @@ -396,6 +396,6 @@ TraceVariable LLVMTraceBuilder::traceVarFromDIVar(const llvm::DIVariable* diVar) } } - return TraceVariable(diVar->getName(), rep, diType->getSizeInBits()); + return TraceVariable(diVar->getName().str(), rep, diType->getSizeInBits()); } diff --git a/src/LLVM/Memory/FlatMemoryModel.cpp b/src/LLVM/Memory/FlatMemoryModel.cpp index a28551da..658458d0 100644 --- a/src/LLVM/Memory/FlatMemoryModel.cpp +++ b/src/LLVM/Memory/FlatMemoryModel.cpp @@ -27,6 +27,7 @@ #include #include #include +#include #define DEBUG_TYPE "FlatMemoryModel" @@ -62,7 +63,7 @@ struct FlatMemoryFunctionInfo // Maps non-lifted globals to their addresses in memory. llvm::DenseMap> globalPointers; - llvm::DenseMap calls; + llvm::DenseMap calls; std::unique_ptr memorySSA; }; @@ -85,7 +86,7 @@ class FlatMemoryModel : public MemoryModel, public MemoryTypeTranslator ); void insertCallDefsUses( - llvm::CallSite call, FlatMemoryFunctionInfo& info, memory::MemorySSABuilder& builder); + llvm::CallBase* call, FlatMemoryFunctionInfo& info, memory::MemorySSABuilder& builder); MemoryTypeTranslator& getMemoryTypeTranslator() override { return *this; } @@ -249,9 +250,9 @@ FlatMemoryModel::FlatMemoryModel( } void FlatMemoryModel::insertCallDefsUses( - llvm::CallSite call, FlatMemoryFunctionInfo& info, memory::MemorySSABuilder& builder) + llvm::CallBase* call, FlatMemoryFunctionInfo& info, memory::MemorySSABuilder& builder) { - llvm::Function* callee = call.getCalledFunction(); + llvm::Function* callee = call->getCalledFunction(); if (callee == nullptr) { builder.createCallDef(info.memory, call); @@ -335,7 +336,7 @@ class FlatMemoryModelInstTranslator : public MemorySSABasedInstructionHandler llvm2cfa::GenerationStepExtensionPoint& ep) override; void handleCall( - llvm::CallSite call, + llvm::CallBase* call, llvm2cfa::GenerationStepExtensionPoint& parentEp, llvm2cfa::AutomatonInterfaceExtensionPoint& calleeEp, llvm::SmallVectorImpl& inputAssignments, @@ -631,15 +632,15 @@ ExprPtr FlatMemoryModelInstTranslator::handleLoad( } void FlatMemoryModelInstTranslator::handleCall( - llvm::CallSite call, + llvm::CallBase* call, llvm2cfa::GenerationStepExtensionPoint& parentEp, llvm2cfa::AutomatonInterfaceExtensionPoint& calleeEp, llvm::SmallVectorImpl& inputAssignments, llvm::SmallVectorImpl& outputAssignments) { - LLVM_DEBUG(llvm::dbgs() << "Handling call instruction " << *call.getInstruction() << "\n"); + LLVM_DEBUG(llvm::dbgs() << "Handling call instruction " << *call << "\n"); - const llvm::Function* callee = call.getCalledFunction(); + const llvm::Function* callee = call->getCalledFunction(); assert(callee != nullptr); auto& calleeInfo = mMemoryModel.getInfoFor(callee); diff --git a/src/LLVM/Memory/HavocMemoryModel.cpp b/src/LLVM/Memory/HavocMemoryModel.cpp index f38e9ec8..98be80a5 100644 --- a/src/LLVM/Memory/HavocMemoryModel.cpp +++ b/src/LLVM/Memory/HavocMemoryModel.cpp @@ -93,7 +93,7 @@ class HavocMemoryModel : } void handleCall( - llvm::CallSite call, + llvm::CallBase* call, llvm2cfa::GenerationStepExtensionPoint& callerEp, llvm2cfa::AutomatonInterfaceExtensionPoint& calleeEp, llvm::SmallVectorImpl& inputAssignments, diff --git a/src/LLVM/Memory/MemoryObject.cpp b/src/LLVM/Memory/MemoryObject.cpp index 147ad5a9..3a5959e5 100644 --- a/src/LLVM/Memory/MemoryObject.cpp +++ b/src/LLVM/Memory/MemoryObject.cpp @@ -92,7 +92,7 @@ void MemoryObjectDef::print(llvm::raw_ostream& os) const std::string MemoryObjectDef::getName() const { - std::string objName = getObject()->getName(); + std::string objName = getObject()->getName().str(); if (objName.empty()) { objName = std::to_string(getObject()->getId()); } diff --git a/src/LLVM/Memory/MemorySSA.cpp b/src/LLVM/Memory/MemorySSA.cpp index 5e82eb76..4bc33431 100644 --- a/src/LLVM/Memory/MemorySSA.cpp +++ b/src/LLVM/Memory/MemorySSA.cpp @@ -172,11 +172,11 @@ memory::StoreDef* MemorySSABuilder::createStoreDef(MemoryObject* object, llvm::S return def; } -memory::CallDef* MemorySSABuilder::createCallDef(gazer::MemoryObject* object, llvm::CallSite call) +memory::CallDef* MemorySSABuilder::createCallDef(gazer::MemoryObject* object, llvm::CallBase* call) { auto def = new memory::CallDef(object, mVersionNumber++, call); - mObjectInfo[object].defBlocks.insert(call.getInstruction()->getParent()); - mValueDefs[call.getInstruction()].push_back(def); + mObjectInfo[object].defBlocks.insert(call->getParent()); + mValueDefs[call].push_back(def); object->addDefinition(def); return def; @@ -203,10 +203,10 @@ memory::LoadUse* MemorySSABuilder::createLoadUse(MemoryObject* object, llvm::Loa return use; } -memory::CallUse* MemorySSABuilder::createCallUse(MemoryObject* object, llvm::CallSite call) +memory::CallUse* MemorySSABuilder::createCallUse(MemoryObject* object, llvm::CallBase* call) { auto use = new memory::CallUse(object, call); - mValueUses[call.getInstruction()].push_back(use); + mValueUses[call].push_back(use); object->addUse(use); return use; @@ -305,7 +305,7 @@ void MemorySSABuilder::renameBlock(llvm::BasicBlock* block) } // Handle successors - for (llvm::DomTreeNode* child : mDominatorTree.getNode(block)->getChildren()) { + for (llvm::DomTreeNode* child : mDominatorTree.getNode(block)->children()) { renameBlock(child->getBlock()); } diff --git a/src/LLVM/Transform/Inline.cpp b/src/LLVM/Transform/Inline.cpp index 5dd02555..c65d75cd 100644 --- a/src/LLVM/Transform/Inline.cpp +++ b/src/LLVM/Transform/Inline.cpp @@ -27,6 +27,7 @@ #include #include +#include #include #include #include @@ -74,7 +75,7 @@ char InlinePass::ID; bool InlinePass::shouldInlineFunction(llvm::CallGraphNode* target, unsigned allowedRefs) { - bool viable = llvm::isInlineViable(*target->getFunction()); + bool viable = llvm::isInlineViable(*target->getFunction()).isSuccess(); viable |= !isRecursive(target); if (!viable) { @@ -112,25 +113,25 @@ bool InlinePass::runOnModule(llvm::Module& module) llvm::CallGraph& cg = getAnalysis().getCallGraph(); llvm::InlineFunctionInfo ifi(&cg); - llvm::SmallVector wl; + llvm::SmallVector wl; llvm::CallGraphNode* entryCG = cg[mEntryFunction]; for (auto& [call, target] : *entryCG) { if (this->shouldInlineFunction(target, 1)) { LLVM_DEBUG(llvm::dbgs() << "Decided to inline call " << *call << " to target " << target->getFunction()->getName() << "\n"); - wl.emplace_back(call); + wl.emplace_back(llvm::dyn_cast(*call)); } } while (!wl.empty()) { - llvm::CallSite cs = wl.pop_back_val(); - bool success = llvm::InlineFunction(cs, ifi); + llvm::CallBase* cs = wl.pop_back_val(); + bool success = llvm::InlineFunction(*cs, ifi).isSuccess(); changed |= success; for (llvm::Value* newCall : ifi.InlinedCalls) { - llvm::CallSite newCS(newCall); - auto callee = newCS.getCalledFunction(); + llvm::CallBase* newCS = llvm::dyn_cast(newCall); + auto callee = newCS->getCalledFunction(); if (callee == nullptr) { continue; } diff --git a/src/LLVM/Transform/InlineGlobalVariablesPass.cpp b/src/LLVM/Transform/InlineGlobalVariablesPass.cpp index 95e639e9..eee1fba2 100644 --- a/src/LLVM/Transform/InlineGlobalVariablesPass.cpp +++ b/src/LLVM/Transform/InlineGlobalVariablesPass.cpp @@ -161,7 +161,8 @@ bool InlineGlobalVariablesPass::runOnModule(Module& module) AllocaInst* alloc = builder.CreateAlloca(type, nullptr, gv.getName()); Constant* init = gv.getInitializer(); - builder.CreateAlignedStore(init, alloc, module.getDataLayout().getABITypeAlignment(type)); + // This was only deprecated TODO remove the comment + builder.CreateAlignedStore(init, alloc, llvm::Align(module.getDataLayout().getABITypeAlignment(type))); // TODO: We should check external calls and clobber the alloca with a nondetermistic // store if the ExternFuncGlobalBehavior setting requires this. diff --git a/src/LLVM/Transform/LiftErrorsPass.cpp b/src/LLVM/Transform/LiftErrorsPass.cpp index d19e08ce..37cf408d 100644 --- a/src/LLVM/Transform/LiftErrorsPass.cpp +++ b/src/LLVM/Transform/LiftErrorsPass.cpp @@ -26,6 +26,7 @@ #include #include +#include #include #include #include @@ -46,14 +47,14 @@ class LiftErrorCalls struct FunctionInfo { std::vector selfFails; - std::vector mayFailCalls; + std::vector mayFailCalls; llvm::PHINode* uniqueErrorPhi = nullptr; llvm::CallInst* uniqueErrorCall = nullptr; llvm::Function* alwaysFailClone = nullptr; llvm::BasicBlock* failCopyEntry = nullptr; std::vector failCopyArgumentPHIs; - + llvm::PHINode* failCloneErrorPhi = nullptr; bool canFail() const @@ -69,7 +70,7 @@ class LiftErrorCalls private: void combineErrorsInFunction(llvm::Function* function, FunctionInfo& info); - + llvm::FunctionCallee getDummyBoolFunc() { return mModule.getOrInsertFunction("gazer.dummy_nondet.i1", llvm::FunctionType::get( @@ -85,8 +86,8 @@ class LiftErrorCalls ); } - llvm::Value* getErrorFunction() - { return CheckRegistry::GetErrorFunction(mModule).getCallee(); } + llvm::FunctionCallee getErrorFunction() + { return CheckRegistry::GetErrorFunction(mModule); } llvm::Type* getErrorCodeType() { return CheckRegistry::GetErrorCodeType(mModule.getContext()); } @@ -194,7 +195,7 @@ bool LiftErrorCalls::run() continue; } - if (auto call = llvm::dyn_cast(callRecord.first)) { + if (auto *call = llvm::dyn_cast(*callRecord.first)) { mInfos[function].mayFailCalls.emplace_back(call); } } @@ -219,7 +220,7 @@ bool LiftErrorCalls::run() } // Do the interprocedural transformation. - std::vector mayFailCallsInMain = mInfos[mEntryFunction].mayFailCalls; + std::vector mayFailCallsInMain = mInfos[mEntryFunction].mayFailCalls; // Copy the bodies of the possibly-failing functions into main. for (auto& [function, info] : mInfos) { @@ -276,7 +277,7 @@ bool LiftErrorCalls::run() // Add all possible calls into main mayFailCallsInMain.reserve(mayFailCallsInMain.size() + info.mayFailCalls.size()); for (auto cs : info.mayFailCalls) { - mayFailCallsInMain.emplace_back(vmap[cs.getInstruction()]); + mayFailCallsInMain.emplace_back(llvm::dyn_cast(vmap[cs])); } // Remove the error call from the original function @@ -290,13 +291,13 @@ bool LiftErrorCalls::run() mBuilder.CreateBr(clonedEntry); } - for (llvm::CallSite call : mayFailCallsInMain) { - assert(call.getCalledFunction() != nullptr); - auto& calleeInfo = mInfos[call.getCalledFunction()]; + for (llvm::CallBase* call : mayFailCallsInMain) { + assert(call->getCalledFunction() != nullptr); + auto& calleeInfo = mInfos[call->getCalledFunction()]; // Split the block for each call, create a nondet branch. llvm::BasicBlock* origBlock = call->getParent(); - llvm::BasicBlock* successBlock = llvm::SplitBlock(origBlock, call.getInstruction()); + llvm::BasicBlock* successBlock = llvm::SplitBlock(origBlock, call); llvm::BasicBlock* errorBlock = llvm::BasicBlock::Create(mModule.getContext(), "", mEntryFunction); // Create the nondetermistic branch between the success and error. @@ -310,8 +311,8 @@ bool LiftErrorCalls::run() mBuilder.SetInsertPoint(errorBlock); mBuilder.CreateBr(calleeInfo.failCopyEntry); - for (size_t i = 0; i < call.arg_size(); ++i) { - calleeInfo.failCopyArgumentPHIs[i]->addIncoming(call.getArgOperand(i), errorBlock); + for (size_t i = 0; i < call->getNumArgOperands(); ++i) { + calleeInfo.failCopyArgumentPHIs[i]->addIncoming(call->getArgOperand(i), errorBlock); } } diff --git a/src/LLVM/Transform/NormalizeVerifierCalls.cpp b/src/LLVM/Transform/NormalizeVerifierCalls.cpp index fb73b51c..3a5468b8 100644 --- a/src/LLVM/Transform/NormalizeVerifierCalls.cpp +++ b/src/LLVM/Transform/NormalizeVerifierCalls.cpp @@ -23,7 +23,7 @@ #include "gazer/LLVM/Transform/Passes.h" #include -#include +#include #include #include @@ -91,12 +91,12 @@ void NormalizeVerifierCallsPass::runOnFunction(llvm::Function& function) continue; } - llvm::CallSite cs(llvm::cast(&inst)); + llvm::CallBase* cs = llvm::cast(&inst); llvm::IRBuilder<> builder(function.getContext()); builder.SetInsertPoint(&inst); - llvm::Function* callee = cs.getCalledFunction(); + llvm::Function* callee = cs->getCalledFunction(); if (callee == nullptr) { // TODO: This should be handled for simple cases. continue; @@ -106,7 +106,7 @@ void NormalizeVerifierCallsPass::runOnFunction(llvm::Function& function) callee->getName() == "klee_assume" || callee->getName() == "__llbmc_assume" ) { - llvm::Value* condition = cs.getArgument(0); + llvm::Value* condition = cs->getArgOperand(0); // These functions may have differing input argument types, such // as i1, i32 or i64. Strip possible ZExt casts and convert to @@ -121,7 +121,7 @@ void NormalizeVerifierCallsPass::runOnFunction(llvm::Function& function) )); } - builder.CreateCall(mAssume.getCallee(), { condition }); + builder.CreateCall(mAssume, { condition }); toKill.emplace_back(&inst); } } diff --git a/src/LLVM/Transform/TransformUtils.cpp b/src/LLVM/Transform/TransformUtils.cpp index 5fcf48a3..a81173e0 100644 --- a/src/LLVM/Transform/TransformUtils.cpp +++ b/src/LLVM/Transform/TransformUtils.cpp @@ -32,7 +32,7 @@ bool isRecursive(llvm::CallGraphNode* target) auto end = llvm::scc_end(target); for (auto it = begin; it != end; ++it) { - if (it.hasLoop()) { + if (it.hasCycle()) { return true; } } diff --git a/src/SolverZ3/Z3Solver.cpp b/src/SolverZ3/Z3Solver.cpp index 27f5875a..9796b945 100644 --- a/src/SolverZ3/Z3Solver.cpp +++ b/src/SolverZ3/Z3Solver.cpp @@ -276,16 +276,18 @@ auto Z3ExprTransformer::visitTupleConstruct(const ExprRef& e auto Z3ExprTransformer::transformRoundingMode(llvm::APFloat::roundingMode rm) -> Z3AstHandle { switch (rm) { - case llvm::APFloat::roundingMode::rmNearestTiesToEven: + case llvm::APFloat::roundingMode::NearestTiesToEven: return createHandle(Z3_mk_fpa_round_nearest_ties_to_even(mZ3Context)); - case llvm::APFloat::roundingMode::rmNearestTiesToAway: + case llvm::APFloat::roundingMode::NearestTiesToAway: return createHandle(Z3_mk_fpa_round_nearest_ties_to_away(mZ3Context)); - case llvm::APFloat::roundingMode::rmTowardPositive: + case llvm::APFloat::roundingMode::TowardPositive: return createHandle(Z3_mk_fpa_round_toward_positive(mZ3Context)); - case llvm::APFloat::roundingMode::rmTowardNegative: + case llvm::APFloat::roundingMode::TowardNegative: return createHandle(Z3_mk_fpa_round_toward_negative(mZ3Context)); - case llvm::APFloat::roundingMode::rmTowardZero: + case llvm::APFloat::roundingMode::TowardZero: return createHandle(Z3_mk_fpa_round_toward_zero(mZ3Context)); + case llvm::APFloat::roundingMode::Dynamic: + llvm_unreachable("Dynamic rounding mode not supported"); } llvm_unreachable("Invalid rounding mode"); diff --git a/src/Support/Runtime.cpp b/src/Support/Runtime.cpp index abed0403..a693e82e 100644 --- a/src/Support/Runtime.cpp +++ b/src/Support/Runtime.cpp @@ -95,7 +95,7 @@ llvm::ErrorOr gazer::findProgramLocation(llvm::StringRef argvZero) return ec; } - return path.str(); + return path.str().str(); } // See if we can look it up in the PATH diff --git a/src/Support/SExpr.cpp b/src/Support/SExpr.cpp index 89896c04..3f7729c8 100644 --- a/src/Support/SExpr.cpp +++ b/src/Support/SExpr.cpp @@ -73,7 +73,7 @@ std::unique_ptr gazer::sexpr::parse(llvm::StringRef input) auto gazer::sexpr::atom(llvm::StringRef data) -> sexpr::Value* { - return new sexpr::Value(data); + return new sexpr::Value(data.str()); } auto gazer::sexpr::list(std::vector data) -> sexpr::Value* diff --git a/tools/gazer-bmc/gazer-bmc.cpp b/tools/gazer-bmc/gazer-bmc.cpp index 2be82f00..00fc4014 100644 --- a/tools/gazer-bmc/gazer-bmc.cpp +++ b/tools/gazer-bmc/gazer-bmc.cpp @@ -26,6 +26,7 @@ #include #include #include +#include #ifndef NDEBUG #include diff --git a/tools/gazer-cfa/gazer-cfa.cpp b/tools/gazer-cfa/gazer-cfa.cpp index 0d7fa1e1..99ccb4af 100644 --- a/tools/gazer-cfa/gazer-cfa.cpp +++ b/tools/gazer-cfa/gazer-cfa.cpp @@ -24,6 +24,7 @@ #include "gazer/LLVM/Automaton/ModuleToAutomata.h" #include "gazer/LLVM/ClangFrontend.h" #include "gazer/LLVM/Memory/MemoryModel.h" +#include #include diff --git a/tools/gazer-theta/gazer-theta.cpp b/tools/gazer-theta/gazer-theta.cpp index 0bcdfd26..82b53be3 100644 --- a/tools/gazer-theta/gazer-theta.cpp +++ b/tools/gazer-theta/gazer-theta.cpp @@ -24,6 +24,7 @@ #include #include +#include #ifndef NDEBUG #include @@ -185,7 +186,7 @@ bool lookupTheta(llvm::StringRef argvZero, theta::ThetaSettings* settings) return false; } - std::string parentPath = llvm::sys::path::parent_path(pathToBinary.get()); + std::string parentPath = llvm::sys::path::parent_path(pathToBinary.get()).str(); if (settings->thetaCfaPath.empty()) { settings->thetaCfaPath = parentPath + "/theta/theta-cfa-cli.jar"; diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp index 13a7ff07..49c84587 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp @@ -278,7 +278,7 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace if (auto assignEdge = dyn_cast(edge)) { for (auto& assignment : *assignEdge) { - auto lhsName = vars[assignment.getVariable()]->getName(); + auto lhsName = vars[assignment.getVariable()]->getName().str(); if (llvm::isa(assignment.getValue())) { stmts.push_back(ThetaStmt::Havoc(lhsName)); @@ -301,7 +301,7 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace return variable->getName(); } - return vars[variable]->getName(); + return vars[variable]->getName().str(); }; os << "main process __gazer_main_process {\n"; From 1cf7243e359ad90309e5e64b52af372008078599 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 13 Feb 2021 13:06:57 +0100 Subject: [PATCH 02/21] Require LLVM 11. Breaking change --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 66a91f67..74188e94 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -58,7 +58,7 @@ if (GAZER_ENABLE_COVERAGE) endif() # Get LLVM -find_package(LLVM REQUIRED CONFIG) +find_package(LLVM 11 REQUIRED CONFIG) message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}") message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}") From e14812fb61fa377f5fcd56a1ed94c2f7bc8cfa86 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 13 Feb 2021 13:09:10 +0100 Subject: [PATCH 03/21] Rename -inline to -inline-level. This is a major change. This is needed so that later this flag does not collide with the tool `opt`. This LLVM tool is used mostly for pass-wise testing. --- src/LLVM/LLVMFrontendSettings.cpp | 2 +- test/verif/regression/eval_error_fail.c | 2 +- test/verif/regression/floats/fp_if_not_inlined.c | 2 +- test/verif/regression/inline_globals_error_fail.c | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/LLVM/LLVMFrontendSettings.cpp b/src/LLVM/LLVMFrontendSettings.cpp index 78a60523..90d9e4cd 100644 --- a/src/LLVM/LLVMFrontendSettings.cpp +++ b/src/LLVM/LLVMFrontendSettings.cpp @@ -38,7 +38,7 @@ namespace // LLVM frontend and transformation options // LLVM IR to CFA translation options - cl::opt InlineLevelOpt("inline", cl::desc("Level for variable elimination:"), + cl::opt InlineLevelOpt("inline-level", cl::desc("Level for variable elimination:"), cl::values( clEnumValN(InlineLevel::Off, "off", "Do not eliminate variables"), clEnumValN(InlineLevel::Default, "default", "Eliminate variables having only one use"), diff --git a/test/verif/regression/eval_error_fail.c b/test/verif/regression/eval_error_fail.c index 995f0ea5..80d27b03 100644 --- a/test/verif/regression/eval_error_fail.c +++ b/test/verif/regression/eval_error_fail.c @@ -1,4 +1,4 @@ -// RUN: %bmc -bound 1 -inline=all -trace "%s" | FileCheck "%s" +// RUN: %bmc -bound 1 -inline-level=all -trace "%s" | FileCheck "%s" // CHECK: Verification FAILED diff --git a/test/verif/regression/floats/fp_if_not_inlined.c b/test/verif/regression/floats/fp_if_not_inlined.c index ccece61e..efbb7215 100644 --- a/test/verif/regression/floats/fp_if_not_inlined.c +++ b/test/verif/regression/floats/fp_if_not_inlined.c @@ -1,7 +1,7 @@ // This test failed if gazer-bmc was invoked without the "-inline=all" flag. // The underlying issue was that the translation process did not handle PHI nodes correctly when jumping out of loops. -// RUN: %bmc -bound 10 -inline=all "%s" | FileCheck "%s" +// RUN: %bmc -bound 10 -inline-level=all "%s" | FileCheck "%s" // RUN: %bmc -bound 10 "%s" | FileCheck "%s" // CHECK: Verification {{(SUCCESSFUL|BOUND REACHED)}} diff --git a/test/verif/regression/inline_globals_error_fail.c b/test/verif/regression/inline_globals_error_fail.c index 90951fa8..8882d516 100644 --- a/test/verif/regression/inline_globals_error_fail.c +++ b/test/verif/regression/inline_globals_error_fail.c @@ -1,4 +1,4 @@ -// RUN: %bmc -bound 1 -inline=all -trace "%s" | FileCheck "%s" +// RUN: %bmc -bound 1 -inline-level=all -trace "%s" | FileCheck "%s" // CHECK: Verification FAILED From b6c5719c5f8aa4d82209e09c655082ec2df69979 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 13 Feb 2021 13:14:19 +0100 Subject: [PATCH 04/21] Update docker image to Ubuntu 20.04 --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 8e6e958e..67648f52 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,4 +1,4 @@ -FROM ubuntu:18.04 +FROM ubuntu:20.04 ENV THETA_VERSION v2.10.0 From 1a752d4a7fa3211208ecf4667b310fd001c29d16 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 13 Feb 2021 13:24:47 +0100 Subject: [PATCH 05/21] Update build workflow to use LLVM11 --- .github/workflows/build.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 554a712f..20c0af2c 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -13,10 +13,10 @@ jobs: run: sudo apt-get install build-essential cmake wget lsb-release software-properties-common zlib1g-dev openjdk-11-jre python3 python3-pip python3-setuptools python3-psutil - name: Set up some more dependencies run: | - sudo apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime libboost-all-dev - sudo ln -sf /usr/bin/clang-9 /usr/bin/clang - sudo ln -s `which opt-9` /usr/bin/opt -f - sudo ln -s `which FileCheck-9` /usr/bin/FileCheck + sudo apt-get install -y clang-11 llvm-11-dev llvm-11-tools llvm-11-runtime libboost-all-dev + sudo ln -sf /usr/bin/clang-11 /usr/bin/clang + sudo ln -s `which opt-11` /usr/bin/opt -f + sudo ln -s `which FileCheck-11` /usr/bin/FileCheck sudo pip3 install lit - name: Set up portfolio dependencies run: sudo apt-get install perl libyaml-tiny-perl libproc-processtable-perl From 7880554a6f2ae73ee0f6d8a9ec83e1f56a12fdad Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 13 Feb 2021 13:32:47 +0100 Subject: [PATCH 06/21] Update --inline to --inline-level --- doc/Portfolio.md | 4 ++-- test/portfolio/SVComp_configuration.yml | 4 ++-- test/portfolio/SVComp_finish_all_configuration.yml | 4 ++-- test/verif/regression/floats/fp_if_not_inlined.c | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/doc/Portfolio.md b/doc/Portfolio.md index 0bab479d..17f9a953 100644 --- a/doc/Portfolio.md +++ b/doc/Portfolio.md @@ -76,10 +76,10 @@ configurations: - name: config1 tool: gazer-bmc timeout: 1 # sec - flags: --inline all --bound 1000000* + flags: --inline-level all --bound 1000000* - name: config2 tool: gazer-theta - flags: --inline all --domain EXPL + flags: --inline-level all --domain EXPL ``` - The `name` and `tool` attributes are required, while `timeout` and `flags` are optional. - The `name` can be an arbitrary identifier, which just makes the output easier to interpret. diff --git a/test/portfolio/SVComp_configuration.yml b/test/portfolio/SVComp_configuration.yml index 55f59be5..ca1c8df1 100644 --- a/test/portfolio/SVComp_configuration.yml +++ b/test/portfolio/SVComp_configuration.yml @@ -11,7 +11,7 @@ configurations: # list of configs to be run. For every configuration a tool is m - name: bmc-inline tool: gazer-bmc timeout: 150 # sec - flags: --inline all --bound 1000000 + flags: --inline-level all --bound 1000000 - name: theta-expl tool: gazer-theta @@ -20,4 +20,4 @@ configurations: # list of configs to be run. For every configuration a tool is m - name: theta-pred tool: gazer-theta - flags: --inline all --search ERR --domain PRED_CART --refinement BW_BIN_ITP --initprec EMPTY + flags: --inline-level all --search ERR --domain PRED_CART --refinement BW_BIN_ITP --initprec EMPTY diff --git a/test/portfolio/SVComp_finish_all_configuration.yml b/test/portfolio/SVComp_finish_all_configuration.yml index fe963467..973c9b3e 100644 --- a/test/portfolio/SVComp_finish_all_configuration.yml +++ b/test/portfolio/SVComp_finish_all_configuration.yml @@ -11,7 +11,7 @@ configurations: # list of configs to be run. For every configuration a tool is m - name: bmc-inline tool: gazer-bmc timeout: 150 # sec - flags: --inline all --bound 1000000 + flags: --inline-level all --bound 1000000 - name: theta-expl tool: gazer-theta @@ -20,4 +20,4 @@ configurations: # list of configs to be run. For every configuration a tool is m - name: theta-pred tool: gazer-theta - flags: --inline all --search ERR --domain PRED_CART --refinement BW_BIN_ITP --initprec EMPTY + flags: --inline-level all --search ERR --domain PRED_CART --refinement BW_BIN_ITP --initprec EMPTY diff --git a/test/verif/regression/floats/fp_if_not_inlined.c b/test/verif/regression/floats/fp_if_not_inlined.c index efbb7215..30560c6a 100644 --- a/test/verif/regression/floats/fp_if_not_inlined.c +++ b/test/verif/regression/floats/fp_if_not_inlined.c @@ -1,4 +1,4 @@ -// This test failed if gazer-bmc was invoked without the "-inline=all" flag. +// This test failed if gazer-bmc was invoked without the "-inline-level=all" flag. // The underlying issue was that the translation process did not handle PHI nodes correctly when jumping out of loops. // RUN: %bmc -bound 10 -inline-level=all "%s" | FileCheck "%s" From 2d92ce5feec87dd10f2d40905eaa1b8880c4ba4d Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 13 Feb 2021 13:56:26 +0100 Subject: [PATCH 07/21] Fix Iterator breaking due to LLVM upgrade --- include/gazer/ADT/Iterator.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/gazer/ADT/Iterator.h b/include/gazer/ADT/Iterator.h index 6512716c..a6f94f3c 100644 --- a/include/gazer/ADT/Iterator.h +++ b/include/gazer/ADT/Iterator.h @@ -50,7 +50,7 @@ class SmartPtrGetIterator : public llvm::iterator_adaptor_base< : SmartPtrGetIterator::iterator_adaptor_base(std::move(it)) {} - ReturnTy operator*() { return this->wrapped()->get(); } + ReturnTy operator*() const { return this->wrapped()->get(); } }; } // namespace gazer From c48a8d7796028d4e998f2f15005b01a94ed24440 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 13 Feb 2021 14:06:11 +0100 Subject: [PATCH 08/21] Update expected output --- test/theta/cfa/Expected/counter.theta | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/test/theta/cfa/Expected/counter.theta b/test/theta/cfa/Expected/counter.theta index 139f30b1..26194e89 100644 --- a/test/theta/cfa/Expected/counter.theta +++ b/test/theta/cfa/Expected/counter.theta @@ -1,6 +1,7 @@ main process __gazer_main_process { var main_RET_VAL : int - var main_tmp : int + var main_i : int + var main_error_phi : int var main___gazer_error_field : int init loc loc0 final loc loc1 @@ -15,15 +16,16 @@ main process __gazer_main_process { } loc2 -> loc3 { - havoc main_tmp + havoc main_i } loc3 -> loc6 { - assume (not (1 <= main_tmp)) + assume ((if (main_i <= 0) then 0 else main_i) = 0) + main_error_phi := 2 } loc3 -> loc4 { - assume (not (not (1 <= main_tmp))) + assume (not ((if (main_i <= 0) then 0 else main_i) = 0)) } loc4 -> loc5 { @@ -41,7 +43,7 @@ main process __gazer_main_process { } loc7 -> loc8 { - main___gazer_error_field := 2 + main___gazer_error_field := main_error_phi } } From 34fa95dd1cf92630be326c3f19dd348ef6957c2f Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 6 Mar 2021 20:45:32 +0100 Subject: [PATCH 09/21] Update Github workflow Github workflow died due to missing `-y` flag on `apt install` --- .github/workflows/build.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 20c0af2c..c1c299a1 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -10,7 +10,7 @@ jobs: - name: Update apt run: sudo apt-get update - name: Set up dependencies - run: sudo apt-get install build-essential cmake wget lsb-release software-properties-common zlib1g-dev openjdk-11-jre python3 python3-pip python3-setuptools python3-psutil + run: sudo apt-get install -y build-essential cmake wget lsb-release software-properties-common zlib1g-dev openjdk-11-jre python3 python3-pip python3-setuptools python3-psutil - name: Set up some more dependencies run: | sudo apt-get install -y clang-11 llvm-11-dev llvm-11-tools llvm-11-runtime libboost-all-dev @@ -19,7 +19,7 @@ jobs: sudo ln -s `which FileCheck-11` /usr/bin/FileCheck sudo pip3 install lit - name: Set up portfolio dependencies - run: sudo apt-get install perl libyaml-tiny-perl libproc-processtable-perl + run: sudo apt-get install -y perl libyaml-tiny-perl libproc-processtable-perl - name: Build run: cmake -DCMAKE_CXX_COMPILER=clang++-9 -DGAZER_ENABLE_UNIT_TESTS=On -DCMAKE_BUILD_TYPE=Debug -DCMAKE_EXPORT_COMPILE_COMMANDS=On . && make - name: Get Theta From 8bdbf41b6ba7b1c1f3dae4d0983a566a601bc086 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 6 Mar 2021 20:58:35 +0100 Subject: [PATCH 10/21] Fix github workflow Upgrade from 18.04 to 20.04 proved problematic -.- --- .github/workflows/build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index c1c299a1..5b419aac 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -8,7 +8,7 @@ jobs: steps: - uses: actions/checkout@v2 - name: Update apt - run: sudo apt-get update + run: sudo DEBIAN_FRONTEND=noninteractive apt-get update - name: Set up dependencies run: sudo apt-get install -y build-essential cmake wget lsb-release software-properties-common zlib1g-dev openjdk-11-jre python3 python3-pip python3-setuptools python3-psutil - name: Set up some more dependencies From ca290214b7842ff9072d8afcb669e4ddf33dca87 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 6 Mar 2021 21:07:23 +0100 Subject: [PATCH 11/21] Fixup --- .github/workflows/build.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 5b419aac..e797d1e2 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -10,16 +10,16 @@ jobs: - name: Update apt run: sudo DEBIAN_FRONTEND=noninteractive apt-get update - name: Set up dependencies - run: sudo apt-get install -y build-essential cmake wget lsb-release software-properties-common zlib1g-dev openjdk-11-jre python3 python3-pip python3-setuptools python3-psutil + run: sudo DEBIAN_FRONTEND=noninteractive apt-get install -y build-essential cmake wget lsb-release software-properties-common zlib1g-dev openjdk-11-jre python3 python3-pip python3-setuptools python3-psutil - name: Set up some more dependencies run: | - sudo apt-get install -y clang-11 llvm-11-dev llvm-11-tools llvm-11-runtime libboost-all-dev + sudo DEBIAN_FRONTEND=noninteractive apt-get install -y clang-11 llvm-11-dev llvm-11-tools llvm-11-runtime libboost-all-dev sudo ln -sf /usr/bin/clang-11 /usr/bin/clang sudo ln -s `which opt-11` /usr/bin/opt -f sudo ln -s `which FileCheck-11` /usr/bin/FileCheck sudo pip3 install lit - name: Set up portfolio dependencies - run: sudo apt-get install -y perl libyaml-tiny-perl libproc-processtable-perl + run: sudo DEBIAN_FRONTEND=noninteractive apt-get install -y perl libyaml-tiny-perl libproc-processtable-perl - name: Build run: cmake -DCMAKE_CXX_COMPILER=clang++-9 -DGAZER_ENABLE_UNIT_TESTS=On -DCMAKE_BUILD_TYPE=Debug -DCMAKE_EXPORT_COMPILE_COMMANDS=On . && make - name: Get Theta From 27c4f2c947efea3631949e88c068f08a917052a5 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 6 Mar 2021 21:18:38 +0100 Subject: [PATCH 12/21] Fixup --- Dockerfile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Dockerfile b/Dockerfile index 67648f52..d3197f35 100644 --- a/Dockerfile +++ b/Dockerfile @@ -11,10 +11,10 @@ RUN apt-get update && \ # fetch LLVM and other dependencies RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - && \ add-apt-repository "deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-9 main" && \ - apt-get update && \ + DEBIAN_FRONTEND=noninteractive apt-get update && \ add-apt-repository ppa:mhier/libboost-latest && \ - apt-get update && \ - apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime libboost1.70-dev perl libyaml-tiny-perl + DEBIAN_FRONTEND=noninteractive apt-get update && \ + DEBIAN_FRONTEND=noninteractive apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime libboost1.70-dev perl libyaml-tiny-perl # create a new user `user` with the password `user` and sudo rights RUN useradd -m user && \ From 4040f0a178dbf18fbde468f9a533ec73771e7d4a Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 6 Mar 2021 21:26:30 +0100 Subject: [PATCH 13/21] Fixup --- Dockerfile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Dockerfile b/Dockerfile index d3197f35..98d8355c 100644 --- a/Dockerfile +++ b/Dockerfile @@ -2,8 +2,8 @@ FROM ubuntu:20.04 ENV THETA_VERSION v2.10.0 -RUN apt-get update && \ - apt-get install -y build-essential git cmake \ +RUN DEBIAN_FRONTEND=noninteractive apt-get update && \ + DEBIAN_FRONTEND=noninteractive apt-get install -y build-essential git cmake \ wget sudo vim lsb-release \ software-properties-common zlib1g-dev \ openjdk-11-jre From 0fe5838a030ae85965b92b40029c152e09ffcd5b Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 6 Mar 2021 21:38:10 +0100 Subject: [PATCH 14/21] Update Dockerfile --- Dockerfile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Dockerfile b/Dockerfile index 98d8355c..8b1a37c7 100644 --- a/Dockerfile +++ b/Dockerfile @@ -10,11 +10,11 @@ RUN DEBIAN_FRONTEND=noninteractive apt-get update && \ # fetch LLVM and other dependencies RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - && \ - add-apt-repository "deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-9 main" && \ + add-apt-repository "deb http://apt.llvm.org/focal/ llvm-toolchain-focal-11 main" && \ DEBIAN_FRONTEND=noninteractive apt-get update && \ add-apt-repository ppa:mhier/libboost-latest && \ DEBIAN_FRONTEND=noninteractive apt-get update && \ - DEBIAN_FRONTEND=noninteractive apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime libboost1.70-dev perl libyaml-tiny-perl + DEBIAN_FRONTEND=noninteractive apt-get install -y clang-11 llvm-11-dev llvm-11-tools llvm-11-runtime libboost1.70-dev perl libyaml-tiny-perl # create a new user `user` with the password `user` and sudo rights RUN useradd -m user && \ @@ -23,7 +23,7 @@ RUN useradd -m user && \ echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers # (the portfolio uses clang) -RUN ln -sf /usr/bin/clang-9 /usr/bin/clang +RUN ln -sf /usr/bin/clang-11 /usr/bin/clang USER user @@ -32,7 +32,7 @@ ENV GAZER_DIR /home/user/gazer ADD --chown=user:user . $GAZER_DIR WORKDIR $GAZER_DIR -RUN cmake -DCMAKE_CXX_COMPILER=clang++-9 -DGAZER_ENABLE_UNIT_TESTS=On -DCMAKE_BUILD_TYPE=Debug -DCMAKE_EXPORT_COMPILE_COMMANDS=On . && make +RUN cmake -DCMAKE_CXX_COMPILER=clang++-11 -DGAZER_ENABLE_UNIT_TESTS=On -DCMAKE_BUILD_TYPE=Debug -DCMAKE_EXPORT_COMPILE_COMMANDS=On . && make # download theta (and libs) RUN mkdir $GAZER_DIR/tools/gazer-theta/theta && \ From 14cd99807809105786786dbcf71baa8c5c78cf4a Mon Sep 17 00:00:00 2001 From: radl97 Date: Sat, 6 Mar 2021 21:51:27 +0100 Subject: [PATCH 15/21] Fixup ladjfhlkjhdsfgsd --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 74188e94..935c6bf3 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -58,7 +58,7 @@ if (GAZER_ENABLE_COVERAGE) endif() # Get LLVM -find_package(LLVM 11 REQUIRED CONFIG) +find_package(LLVM 11.1 REQUIRED CONFIG) message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}") message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}") From 590e4baa9af7725aff4d2c22edb6e13e881ce550 Mon Sep 17 00:00:00 2001 From: radl97 Date: Mon, 22 Mar 2021 21:51:53 +0100 Subject: [PATCH 16/21] Update ClangFrontend.cpp --- src/LLVM/ClangFrontend.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/LLVM/ClangFrontend.cpp b/src/LLVM/ClangFrontend.cpp index 0012ee5e..d5d7263a 100644 --- a/src/LLVM/ClangFrontend.cpp +++ b/src/LLVM/ClangFrontend.cpp @@ -163,13 +163,13 @@ auto gazer::ClangCompileAndLink( llvm::SMDiagnostic err; // Find clang and llvm-link. - auto clang = llvm::sys::findProgramByName("clang-9"); + auto clang = llvm::sys::findProgramByName("clang-11"); if (clang.getError()) clang = llvm::sys::findProgramByName("clang"); - CHECK_ERROR(clang.getError(), "Could not find clang-9 or clang."); + CHECK_ERROR(clang.getError(), "Could not find clang-11 or clang."); - auto llvm_link = llvm::sys::findProgramByName("llvm-link-9"); + auto llvm_link = llvm::sys::findProgramByName("llvm-link-11"); if (llvm_link.getError()) llvm_link = llvm::sys::findProgramByName("llvm-link"); - CHECK_ERROR(llvm_link.getError(), "Could not find llvm-link-9 or llvm-link."); + CHECK_ERROR(llvm_link.getError(), "Could not find llvm-link-11 or llvm-link."); // Create a temporary working directory llvm::SmallString<128> workingDir; From 54c9be6b3762e08bff12dc93ae87fc9614d186b8 Mon Sep 17 00:00:00 2001 From: radl97 Date: Tue, 23 Mar 2021 22:06:30 +0100 Subject: [PATCH 17/21] Update CMakeLists.txt --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 935c6bf3..aded773c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -58,7 +58,7 @@ if (GAZER_ENABLE_COVERAGE) endif() # Get LLVM -find_package(LLVM 11.1 REQUIRED CONFIG) +find_package(LLVM 11.0...<12.0 REQUIRED CONFIG) message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}") message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}") From 7b81cd0c58fbcea10f2a468e2e9cb111acca7eed Mon Sep 17 00:00:00 2001 From: radl97 Date: Tue, 23 Mar 2021 22:22:40 +0100 Subject: [PATCH 18/21] Update build.yml --- .github/workflows/build.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index e797d1e2..af8e1dca 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -11,6 +11,8 @@ jobs: run: sudo DEBIAN_FRONTEND=noninteractive apt-get update - name: Set up dependencies run: sudo DEBIAN_FRONTEND=noninteractive apt-get install -y build-essential cmake wget lsb-release software-properties-common zlib1g-dev openjdk-11-jre python3 python3-pip python3-setuptools python3-psutil + - name: Add LLVM repo + run: sudo wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - && add-apt-repository "deb http://apt.llvm.org/focal/ llvm-toolchain-focal-11 main" - name: Set up some more dependencies run: | sudo DEBIAN_FRONTEND=noninteractive apt-get install -y clang-11 llvm-11-dev llvm-11-tools llvm-11-runtime libboost-all-dev From 71c4f05c258a32e6b88bcecd980ef44befe6cb07 Mon Sep 17 00:00:00 2001 From: radl97 Date: Tue, 23 Mar 2021 22:25:30 +0100 Subject: [PATCH 19/21] Update build.yml --- .github/workflows/build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index af8e1dca..62de3bc1 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -12,7 +12,7 @@ jobs: - name: Set up dependencies run: sudo DEBIAN_FRONTEND=noninteractive apt-get install -y build-essential cmake wget lsb-release software-properties-common zlib1g-dev openjdk-11-jre python3 python3-pip python3-setuptools python3-psutil - name: Add LLVM repo - run: sudo wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - && add-apt-repository "deb http://apt.llvm.org/focal/ llvm-toolchain-focal-11 main" + run: sudo wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - && sudo add-apt-repository "deb http://apt.llvm.org/focal/ llvm-toolchain-focal-11 main" - name: Set up some more dependencies run: | sudo DEBIAN_FRONTEND=noninteractive apt-get install -y clang-11 llvm-11-dev llvm-11-tools llvm-11-runtime libboost-all-dev From 8ec3e291a2ce20b35674413d060b1bbf23718a7e Mon Sep 17 00:00:00 2001 From: radl97 Date: Tue, 23 Mar 2021 22:28:51 +0100 Subject: [PATCH 20/21] Update build.yml --- .github/workflows/build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 62de3bc1..8be157a6 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -12,7 +12,7 @@ jobs: - name: Set up dependencies run: sudo DEBIAN_FRONTEND=noninteractive apt-get install -y build-essential cmake wget lsb-release software-properties-common zlib1g-dev openjdk-11-jre python3 python3-pip python3-setuptools python3-psutil - name: Add LLVM repo - run: sudo wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - && sudo add-apt-repository "deb http://apt.llvm.org/focal/ llvm-toolchain-focal-11 main" + run: sudo wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add - && sudo add-apt-repository "deb http://apt.llvm.org/focal/ llvm-toolchain-focal-11 main" - name: Set up some more dependencies run: | sudo DEBIAN_FRONTEND=noninteractive apt-get install -y clang-11 llvm-11-dev llvm-11-tools llvm-11-runtime libboost-all-dev From 7e31470acccd0fdc695029dd301f661cfee90bdd Mon Sep 17 00:00:00 2001 From: radl97 Date: Tue, 23 Mar 2021 23:18:06 +0100 Subject: [PATCH 21/21] Update CMakeLists.txt --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index aded773c..935c6bf3 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -58,7 +58,7 @@ if (GAZER_ENABLE_COVERAGE) endif() # Get LLVM -find_package(LLVM 11.0...<12.0 REQUIRED CONFIG) +find_package(LLVM 11.1 REQUIRED CONFIG) message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}") message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}")