ftsrg · radl97 · Feb 12, 2021 · Feb 13, 2021 · Feb 13, 2021 · Feb 13, 2021
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -8,18 +8,20 @@ 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 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: Add LLVM repo
+      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 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 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 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

diff --git 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 11.1 REQUIRED CONFIG)
 message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}")
 message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}")
 

diff --git a/Dockerfile b/Dockerfile
@@ -1,20 +1,20 @@
-FROM ubuntu:18.04
+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
 
 # 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 && \
+    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 && \
-    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-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 && \

diff --git 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/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

diff --git 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<void(llvm::ImmutableCallSite, llvm2cfa::GenerationStepExtensionPoint& ep)>;
+    using HandlerFuncTy = std::function<void(const llvm::CallBase*, llvm2cfa::GenerationStepExtensionPoint& ep)>;
 
     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<SpecialFunctionHandler> mHandlers;

diff --git 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 <llvm/Pass.h>
 #include <llvm/IR/LegacyPassManager.h>
 #include <llvm/Support/ToolOutputFile.h>
+#include "llvm/Support/ManagedStatic.h"
 
 namespace gazer
 {

diff --git 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<VariableAssignment>& 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
@@ -26,7 +26,7 @@
 #include <llvm/IR/Operator.h>
 #include <llvm/Pass.h>
 #include <llvm/IR/ValueHandle.h>
-#include <llvm/IR/CallSite.h>
+#include <llvm/IR/AbstractCallSite.h>
 
 #include <boost/iterator/indirect_iterator.hpp>
 
@@ -334,21 +334,21 @@ 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)
     {}
 
     static bool classof(const MemoryObjectDef* def) {
         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,20 +445,20 @@ 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;
 
     static bool classof(const MemoryObjectUse* use) {
         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
@@ -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<MemorySSA> build();

diff --git a/include/gazer/Support/GrowingStackAllocator.h b/include/gazer/Support/GrowingStackAllocator.h
@@ -49,7 +49,8 @@ class GrowingStackAllocator : public llvm::AllocatorBase<GrowingStackAllocator<A
 
     LLVM_ATTRIBUTE_RETURNS_NONNULL void* Allocate(size_t size, size_t alignment)
     {
-        size_t adjustment = llvm::alignmentAdjustment(slab().Current, alignment);
+        //size_t adjustment = llvm::alignmentAdjustment(slab().Current, alignment);
+        size_t adjustment = llvm::offsetToAlignedAddr(slab().Current, llvm::Align(alignment));
         assert(adjustment + size >= size);
 
         if (size > SlabSize) {

diff --git a/src/Core/Expr/ExprPrinter.cpp b/src/Core/Expr/ExprPrinter.cpp
@@ -299,20 +299,20 @@ class InfixPrintVisitor : public ExprWalker<InfixPrintVisitor, std::string>
             bv->getValue().toStringSigned(buffer, mRadix);
             rso << "bv" << bv->getType().getWidth();
 
-            return rso.str();
+            return rso.str().str();
         }
 
         if (auto fl = llvm::dyn_cast<FloatLiteralExpr>(expr)) {
             fl->getValue().toString(buffer);
             rso << "fp" << fl->getType().getWidth();
 
-            return rso.str();
+            return rso.str().str();
         }
 
         if (auto rl = llvm::dyn_cast<RealLiteralExpr>(expr)) {
             rso << rl->getValue().numerator() << "%" << rl->getValue().denominator();
 
-            return rso.str();
+            return rso.str().str();
         }
 
         if (auto al = llvm::dyn_cast<ArrayLiteralExpr>(expr)) {
@@ -336,7 +336,7 @@ class InfixPrintVisitor : public ExprWalker<InfixPrintVisitor, std::string>
             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
@@ -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
@@ -34,6 +34,7 @@
 #include <llvm/IR/Instructions.h>
 #include <llvm/Analysis/LoopInfo.h>
 #include <llvm/ADT/MapVector.h>
+#include <llvm/Support/CommandLine.h>
 
 #include <variant>
 

diff --git 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<BasicBlock*> visitedBlocks;
 

diff --git 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
@@ -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;
@@ -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<std::string>& args)

diff --git a/src/LLVM/FrontendConfig.cpp b/src/LLVM/FrontendConfig.cpp
@@ -110,7 +110,7 @@ void FrontendConfig::createChecks(std::vector<std::unique_ptr<Check>>& 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;