Restructure packages

include/gazer/LLVM/Automaton/InstToExpr.h

@@ -118,6 +118,8 @@ class InstToExpr
     const LLVMFrontendSettings& mSettings;
 };
 
+bool& isArithmeticInteger();
+
 } // end namespace gazer
 
 #endif

include/gazer/LLVM/Automaton/ModuleToAutomata.h

@@ -191,8 +191,8 @@ class ModuleToAutomataPass : public llvm::ModulePass
 public:
     static char ID;
 
-    ModuleToAutomataPass(GazerContext& context, LLVMFrontendSettings& settings)
-        : ModulePass(ID), mContext(context), mSettings(settings)
+    ModuleToAutomataPass(GazerContext& context)
+        : ModulePass(ID), mContext(context)
     {}
 
     void getAnalysisUsage(llvm::AnalysisUsage& au) const override;
@@ -212,7 +212,6 @@ class ModuleToAutomataPass : public llvm::ModulePass
     llvm::DenseMap<llvm::Value*, Variable*> mVariables;
     CfaToLLVMTrace mTraceInfo;
     GazerContext& mContext;
-    LLVMFrontendSettings& mSettings;
 };
 
 class SpecialFunctions;

include/gazer/LLVM/LLVMFrontend.h

@@ -63,14 +63,14 @@ class FrontendConfig
         llvm::LLVMContext& llvmContext
     );
 
-    LLVMFrontendSettings& getSettings() { return mSettings; }
+    //LLVMFrontendSettings& getSettings() { return mSettings; }
 
 private:
     void createChecks(std::vector<std::unique_ptr<Check>>& checks);
 
 private:
     ClangOptions mClangSettings;
-    LLVMFrontendSettings mSettings;
+    //LLVMFrontendSettings mSettings;
     std::map<std::string, CheckFactory> mFactories;
 };
 
@@ -88,7 +88,7 @@ class FrontendConfigWrapper
         return config.buildFrontend(inputs, context, llvmContext);
     }
 
-    LLVMFrontendSettings& getSettings() { return config.getSettings(); }
+    //LLVMFrontendSettings& getSettings() { return config.getSettings(); }
 
 private:
     llvm::llvm_shutdown_obj mShutdown; // This should be kept as first, will be destroyed last
@@ -103,8 +103,7 @@ class LLVMFrontend
 public:
     LLVMFrontend(
         std::unique_ptr<llvm::Module> module,
-        GazerContext& context,
-        LLVMFrontendSettings& settings
+        GazerContext& context
     );
 
     LLVMFrontend(const LLVMFrontend&) = delete;
@@ -140,7 +139,7 @@ class LLVMFrontend
     void run();
 
     CheckRegistry& getChecks() { return mChecks; }
-    LLVMFrontendSettings& getSettings() { return mSettings; }
+    //LLVMFrontendSettings& getSettings() { return mSettings; }
 
     GazerContext& getContext() const { return mContext; }
     llvm::Module& getModule() const { return *mModule; }
@@ -159,8 +158,7 @@ class LLVMFrontend
     CheckRegistry mChecks;
     llvm::legacy::PassManager mPassManager;
 
-    LLVMFrontendSettings& mSettings;
-    std::unique_ptr<VerificationAlgorithm> mBackendAlgorithm = nullptr; 
+    std::unique_ptr<VerificationAlgorithm> mBackendAlgorithm = nullptr;
 
     std::unique_ptr<llvm::ToolOutputFile> mModuleOutput = nullptr;
 };

include/gazer/LLVM/LLVMFrontendSettings.h

@@ -19,6 +19,7 @@
 #define GAZER_LLVM_LLVMFRONTENDSETTINGS_H
 
 #include <string>
+#include <llvm/Support/CommandLine.h>
 
 namespace llvm
 {
@@ -29,6 +30,17 @@ class Function;
 
 } // namespace llvm
 
+// settings getting sinked to their respective classes, etc.
+// this helps appending a settings to their respective category without
+// having to be in the same file
+namespace gazer
+{
+extern llvm::cl::OptionCategory LLVMFrontendCategory;
+extern llvm::cl::OptionCategory IrToCfaCategory;
+extern llvm::cl::OptionCategory TraceCategory;
+extern llvm::cl::OptionCategory ChecksCategory;
+} // end namespace gazer
+
 namespace gazer
 {
 

include/gazer/LLVM/LLVMFrontendSettingsProviderPass.h

@@ -0,0 +1,42 @@
+//==-------------------------------------------------------------*- C++ -*--==//
+//
+// Copyright 2020 Contributors to the Gazer project
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+//
+//===----------------------------------------------------------------------===//
+#ifndef GAZER_LLVMFRONTENDSETTINGSPROVIDERPASS_H
+#define GAZER_LLVMFRONTENDSETTINGSPROVIDERPASS_H
+
+#include "gazer/LLVM/LLVMFrontendSettings.h"
+
+#include <llvm/Pass.h>
+
+namespace gazer {
+
+class LLVMFrontendSettingsProviderPass final : public llvm::ImmutablePass {
+    LLVMFrontendSettings mSettings;
+public:
+    void initializePass() override;
+
+    static char ID;
+    LLVMFrontendSettingsProviderPass() : llvm::ImmutablePass(ID) { }
+
+    virtual gazer::LLVMFrontendSettings& getSettings() { return mSettings; }
+};
+
+llvm::Pass* createLLVMFrontendSettingsProviderPass();
+
+} // namespace gazer
+
+#endif // GAZER_LLVMFRONTENDSETTINGSPROVIDERPASS_H

include/gazer/LLVM/Memory/MemoryModel.h

@@ -70,8 +70,8 @@ class MemoryModelWrapperPass : public llvm::ModulePass
 public:
     static char ID;
 
-    MemoryModelWrapperPass(GazerContext& context, const LLVMFrontendSettings& settings)
-        : ModulePass(ID), mContext(context), mSettings(settings)
+    MemoryModelWrapperPass(GazerContext& context)
+        : ModulePass(ID), mContext(context)
     {}
 
     void getAnalysisUsage(llvm::AnalysisUsage& au) const override;
@@ -85,10 +85,12 @@ class MemoryModelWrapperPass : public llvm::ModulePass
 
 private:
     GazerContext& mContext;
-    const LLVMFrontendSettings& mSettings;
+    //const LLVMFrontendSettings& mSettings;
     std::unique_ptr<MemoryModel> mMemoryModel;
 };
 
+/// not read-only for forcing havoc mem model
+MemoryModelSetting& getMemoryModel();
 
 } // namespace gazer
 #endif //GAZER_MEMORY_MEMORYMODEL_H

include/gazer/LLVM/Transform/Passes.h

@@ -31,13 +31,13 @@ llvm::Pass* createInlineGlobalVariablesPass();
 
 /// This pass combines each 'gazer.error_code' call within the function
 /// into a single one.
-llvm::Pass* createLiftErrorCallsPass(llvm::Function& entry);
+llvm::Pass* createLiftErrorCallsPass();
 
 /// This pass normalizes some known verifier calls into a uniform format.
 llvm::Pass* createNormalizeVerifierCallsPass();
 
 /// A simpler (and more restricted) inlining pass.
-llvm::Pass* createSimpleInlinerPass(llvm::Function& entry, InlineLevel level);
+llvm::Pass* createSimpleInlinerPass();
 
 llvm::Pass* createCanonizeLoopExitsPass();
 

src/CMakeLists.txt

@@ -2,7 +2,6 @@ add_subdirectory(Core)
 add_subdirectory(Automaton)
 add_subdirectory(LLVM)
 add_subdirectory(Trace)
-add_subdirectory(Verifier)
 add_subdirectory(Support)
 
 # Add requested solvers

src/LLVM/Automaton/AutomatonPasses.cpp

@@ -27,6 +27,8 @@
 #include "gazer/LLVM/Automaton/SpecialFunctions.h"
 #include "gazer/LLVM/Memory/MemoryModel.h"
 
+#include <gazer/LLVM/LLVMFrontendSettingsProviderPass.h>
+
 using namespace gazer;
 using namespace gazer::llvm2cfa;
 
@@ -56,13 +58,16 @@ char ModuleToAutomataPass::ID;
 
 void ModuleToAutomataPass::getAnalysisUsage(llvm::AnalysisUsage& au) const
 {
+    au.addRequired<LLVMFrontendSettingsProviderPass>();
     au.addRequired<llvm::DominatorTreeWrapperPass>();
     au.addRequired<MemoryModelWrapperPass>();
     au.setPreservesAll();
 }
 
 bool ModuleToAutomataPass::runOnModule(llvm::Module& module)
 {
+    auto& settings = getAnalysis<LLVMFrontendSettingsProviderPass>()
+        .getSettings();
     // We need to save loop information here as a on-the-fly LoopInfo pass would delete
     // the acquired loop information when the lambda function exits.
     llvm::DenseMap<const llvm::Function*, std::unique_ptr<llvm::LoopInfo>> loopInfos;
@@ -86,9 +91,9 @@ bool ModuleToAutomataPass::runOnModule(llvm::Module& module)
     auto specialFunctions = SpecialFunctions::get();
 
     mSystem = translateModuleToAutomata(
-        module, mSettings, loops, mContext, memoryModel, mVariables, mTraceInfo, specialFunctions.get());
+        module, settings, loops, mContext, memoryModel, mVariables, mTraceInfo, specialFunctions.get());
 
-    if (mSettings.loops == LoopRepresentation::Cycle) {
+    if (settings.loops == LoopRepresentation::Cycle) {
         // Transform the main automaton into a cyclic CFA if requested.
         // Note: This yields an invalid CFA, which will not be recognizable by
         // most built-in analysis algorithms. Use it only if you are going to

src/LLVM/Automaton/InstToExpr.cpp

@@ -26,6 +26,14 @@
 using namespace gazer;
 using namespace llvm;
 
+namespace {
+
+cl::opt<bool> ArithInts(
+    "math-int", cl::desc("Use mathematical unbounded integers instead of bitvectors"),
+    cl::cat(IrToCfaCategory));
+
+}
+
 ExprPtr InstToExpr::transform(const llvm::Instruction &inst, Type &expectedType)
 {
     ExprPtr result = this->doTransform(inst, expectedType);
@@ -995,3 +1003,8 @@ gazer::Type& InstToExpr::translateType(const llvm::Type* type)
 {
     return mTypes.get(type);
 }
+
+bool& gazer::isArithmeticInteger()
+{
+    return ArithInts.getValue();
+}

src/LLVM/CMakeLists.txt

@@ -1,4 +1,4 @@
-set(SOURCE_FILES
+set(MODULE_SOURCE_FILES
     Transform/InlineGlobalVariablesPass.cpp
     Transform/UndefToNondet.cpp
     Transform/LiftErrorsPass.cpp
@@ -14,12 +14,6 @@ set(SOURCE_FILES
     Automaton/InstToExpr.cpp
     Automaton/TranslationSupport.cpp
     Automaton/SpecialFunctions.cpp
-    LLVMTraceBuilder.cpp
-    TypeTranslator.cpp
-    LLVMFrontendSettings.cpp
-    LLVMFrontend.cpp
-    ClangFrontend.cpp
-    FrontendConfig.cpp
     Memory/MemoryObject.cpp
     Memory/FlatMemoryModel.cpp
     Memory/HavocMemoryModel.cpp
@@ -31,12 +25,28 @@ set(SOURCE_FILES
     Automaton/ExtensionPoints.cpp
     Automaton/ValueOrMemoryObject.cpp
     Analysis/PDG.cpp
+    TypeTranslator.cpp
     Instrumentation/Checks/AssertionFailCheck.cpp
     Instrumentation/Checks/DivisionByZeroCheck.cpp
-    Instrumentation/Checks/SignedIntegerOverflowCheck.cpp Transform/LoopExitCanonizationPass.cpp)
+    Instrumentation/Checks/SignedIntegerOverflowCheck.cpp Transform/LoopExitCanonizationPass.cpp
+)
+
+set(SOURCE_FILES
+    LLVMTraceBuilder.cpp
+    LLVMFrontendSettings.cpp
+    LLVMFrontend.cpp
+    ClangFrontend.cpp
+    FrontendConfig.cpp
+    LLVMFrontendSettingsProviderPass.cpp)
+
+# module for LLVM opt integration (use like opt -load src/LLVM/libGazerLLVMBare.so -gazer-... test.ll)
+add_library(GazerLLVMBare SHARED ${MODULE_SOURCE_FILES})
+target_link_libraries(GazerLLVMBare GazerCore GazerAutomaton GazerTrace GazerSupport)
 
 llvm_map_components_to_libnames(GAZER_LLVM_LIBS core irreader transformutils scalaropts ipo)
 message(STATUS "Using LLVM libraries: ${GAZER_LLVM_LIBS}")
 
+# original target, with libraries linked
+# add_library must have options
 add_library(GazerLLVM SHARED ${SOURCE_FILES})
-target_link_libraries(GazerLLVM ${GAZER_LLVM_LIBS} GazerCore GazerTrace GazerZ3Solver GazerAutomaton GazerVerifier)
+target_link_libraries(GazerLLVM GazerLLVMBare ${GAZER_LLVM_LIBS})

src/LLVM/FrontendConfig.cpp

@@ -34,7 +34,6 @@
 using namespace gazer;
 
 FrontendConfig::FrontendConfig()
-    : mSettings(LLVMFrontendSettings::initFromCommandLine())
 {
     // Insert default checks
     registerCheck("assertion-fail",     &checks::createAssertionFailCheck);
@@ -62,20 +61,22 @@ auto FrontendConfig::buildFrontend(
         return nullptr;
     }
 
-    if (!mSettings.validate(*module, llvm::errs())) {
+    // TODO
+    LLVMFrontendSettings settings = LLVMFrontendSettings::initFromCommandLine();
+    if (!settings.validate(*module, llvm::errs())) {
         llvm::errs() << "Settings could not be applied to the input module.\n";
         return nullptr;
     }
 
-    auto frontend = std::make_unique<LLVMFrontend>(std::move(module), context, mSettings);
+    auto frontend = std::make_unique<LLVMFrontend>(std::move(module), context);
 
     // The Witness generator has to get the initial name of the sourcefile
     // ( witnesses support programs with a single source file only )
-    if (!mSettings.witness.empty()) {
+    if (!settings.witness.empty()) {
         if (inputs.size()!=1) {
             llvm::errs() << "Witnesses support programs with a single source file only. Gazer won't generate a witness, as there were more than one input files";
-            mSettings.witness = "";
-            mSettings.hash = "";
+            settings.witness = "";
+            settings.hash = "";
         } else { // TODO something more elegant?
             llvm::StringRef filename = llvm::sys::path::filename(inputs[0]);
             gazer::ViolationWitnessWriter::SourceFileName = filename;
@@ -93,7 +94,9 @@ auto FrontendConfig::buildFrontend(
 
 void FrontendConfig::createChecks(std::vector<std::unique_ptr<Check>>& checks)
 {
-    std::string filter = llvm::StringRef{mSettings.checks}.lower();
+    // TODO
+    LLVMFrontendSettings settings = LLVMFrontendSettings::initFromCommandLine();
+    std::string filter = llvm::StringRef{settings.checks}.lower();
     llvm::SmallVector<llvm::StringRef, 8> fragments;
     if (filter.empty()) {
         // Do the defaults

src/LLVM/Instrumentation/MarkFunctionEntries.cpp

@@ -147,6 +147,12 @@ class MarkFunctionEntriesPass : public ModulePass
 
 char MarkFunctionEntriesPass::ID = 0;
 
+
+static llvm::RegisterPass<MarkFunctionEntriesPass> X("gazer-mark-function-entries",
+                                                      "Gazer function entry marker pass",
+                                                      false /* Only looks at CFG */,
+                                                      false /* Analysis Pass */);
+
 namespace gazer {
     llvm::Pass* createMarkFunctionEntriesPass() {
         return new MarkFunctionEntriesPass();