diff --git a/include/gazer/LLVM/Automaton/InstToExpr.h b/include/gazer/LLVM/Automaton/InstToExpr.h index c97277c7..c0eb50ce 100644 --- a/include/gazer/LLVM/Automaton/InstToExpr.h +++ b/include/gazer/LLVM/Automaton/InstToExpr.h @@ -118,6 +118,8 @@ class InstToExpr const LLVMFrontendSettings& mSettings; }; +bool& isArithmeticInteger(); + } // end namespace gazer #endif diff --git a/include/gazer/LLVM/Automaton/ModuleToAutomata.h b/include/gazer/LLVM/Automaton/ModuleToAutomata.h index 41349f2a..6f30ebaa 100644 --- a/include/gazer/LLVM/Automaton/ModuleToAutomata.h +++ b/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 mVariables; CfaToLLVMTrace mTraceInfo; GazerContext& mContext; - LLVMFrontendSettings& mSettings; }; class SpecialFunctions; diff --git a/include/gazer/LLVM/LLVMFrontend.h b/include/gazer/LLVM/LLVMFrontend.h index 50fbc638..19173d8f 100644 --- a/include/gazer/LLVM/LLVMFrontend.h +++ b/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>& checks); private: ClangOptions mClangSettings; - LLVMFrontendSettings mSettings; + //LLVMFrontendSettings mSettings; std::map 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 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 mBackendAlgorithm = nullptr; + std::unique_ptr mBackendAlgorithm = nullptr; std::unique_ptr mModuleOutput = nullptr; }; diff --git a/include/gazer/LLVM/LLVMFrontendSettings.h b/include/gazer/LLVM/LLVMFrontendSettings.h index cf7a4d13..6904681e 100644 --- a/include/gazer/LLVM/LLVMFrontendSettings.h +++ b/include/gazer/LLVM/LLVMFrontendSettings.h @@ -19,6 +19,7 @@ #define GAZER_LLVM_LLVMFRONTENDSETTINGS_H #include +#include 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 { diff --git a/include/gazer/LLVM/LLVMFrontendSettingsProviderPass.h b/include/gazer/LLVM/LLVMFrontendSettingsProviderPass.h new file mode 100644 index 00000000..77788e01 --- /dev/null +++ b/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 + +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 diff --git a/include/gazer/LLVM/Memory/MemoryModel.h b/include/gazer/LLVM/Memory/MemoryModel.h index d5b90be0..55a55720 100644 --- a/include/gazer/LLVM/Memory/MemoryModel.h +++ b/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 mMemoryModel; }; +/// not read-only for forcing havoc mem model +MemoryModelSetting& getMemoryModel(); } // namespace gazer #endif //GAZER_MEMORY_MEMORYMODEL_H diff --git a/include/gazer/LLVM/Transform/Passes.h b/include/gazer/LLVM/Transform/Passes.h index bce13d39..373d0799 100644 --- a/include/gazer/LLVM/Transform/Passes.h +++ b/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(); diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 08da86ef..4599a1b7 100644 --- a/src/CMakeLists.txt +++ b/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 diff --git a/src/LLVM/Automaton/AutomatonPasses.cpp b/src/LLVM/Automaton/AutomatonPasses.cpp index 856ea237..4c209021 100644 --- a/src/LLVM/Automaton/AutomatonPasses.cpp +++ b/src/LLVM/Automaton/AutomatonPasses.cpp @@ -27,6 +27,8 @@ #include "gazer/LLVM/Automaton/SpecialFunctions.h" #include "gazer/LLVM/Memory/MemoryModel.h" +#include + using namespace gazer; using namespace gazer::llvm2cfa; @@ -56,6 +58,7 @@ char ModuleToAutomataPass::ID; void ModuleToAutomataPass::getAnalysisUsage(llvm::AnalysisUsage& au) const { + au.addRequired(); au.addRequired(); au.addRequired(); au.setPreservesAll(); @@ -63,6 +66,8 @@ void ModuleToAutomataPass::getAnalysisUsage(llvm::AnalysisUsage& au) const bool ModuleToAutomataPass::runOnModule(llvm::Module& module) { + auto& settings = getAnalysis() + .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> 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 diff --git a/src/LLVM/Automaton/InstToExpr.cpp b/src/LLVM/Automaton/InstToExpr.cpp index 58d9846e..afa56e59 100644 --- a/src/LLVM/Automaton/InstToExpr.cpp +++ b/src/LLVM/Automaton/InstToExpr.cpp @@ -26,6 +26,14 @@ using namespace gazer; using namespace llvm; +namespace { + +cl::opt 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(); +} \ No newline at end of file diff --git a/src/LLVM/CMakeLists.txt b/src/LLVM/CMakeLists.txt index a9911068..caf566e8 100644 --- a/src/LLVM/CMakeLists.txt +++ b/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}) diff --git a/src/LLVM/FrontendConfig.cpp b/src/LLVM/FrontendConfig.cpp index 8ed56d62..32218953 100644 --- a/src/LLVM/FrontendConfig.cpp +++ b/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(std::move(module), context, mSettings); + auto frontend = std::make_unique(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>& checks) { - std::string filter = llvm::StringRef{mSettings.checks}.lower(); + // TODO + LLVMFrontendSettings settings = LLVMFrontendSettings::initFromCommandLine(); + std::string filter = llvm::StringRef{settings.checks}.lower(); llvm::SmallVector fragments; if (filter.empty()) { // Do the defaults diff --git a/src/LLVM/Instrumentation/MarkFunctionEntries.cpp b/src/LLVM/Instrumentation/MarkFunctionEntries.cpp index 0d2a183f..4ef701b9 100644 --- a/src/LLVM/Instrumentation/MarkFunctionEntries.cpp +++ b/src/LLVM/Instrumentation/MarkFunctionEntries.cpp @@ -147,6 +147,12 @@ class MarkFunctionEntriesPass : public ModulePass char MarkFunctionEntriesPass::ID = 0; + +static llvm::RegisterPass 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(); diff --git a/src/LLVM/LLVMFrontend.cpp b/src/LLVM/LLVMFrontend.cpp index 86abb3aa..51922040 100644 --- a/src/LLVM/LLVMFrontend.cpp +++ b/src/LLVM/LLVMFrontend.cpp @@ -16,6 +16,7 @@ // //===----------------------------------------------------------------------===// #include "gazer/LLVM/LLVMFrontend.h" +#include "gazer/LLVM/LLVMFrontendSettingsProviderPass.h" #include "gazer/LLVM/Instrumentation/DefaultChecks.h" #include "gazer/LLVM/InstrumentationPasses.h" #include "gazer/LLVM/Transform/Passes.h" @@ -79,14 +80,14 @@ namespace RunVerificationBackendPass( const CheckRegistry& checks, - VerificationAlgorithm& algorithm, - const LLVMFrontendSettings& settings - ) : ModulePass(ID), mChecks(checks), mAlgorithm(algorithm), mSettings(settings) + VerificationAlgorithm& algorithm + ) : ModulePass(ID), mChecks(checks), mAlgorithm(algorithm) {} void getAnalysisUsage(llvm::AnalysisUsage& au) const override { au.addRequired(); + au.addRequired(); au.setPreservesCFG(); } @@ -99,7 +100,6 @@ namespace private: const CheckRegistry& mChecks; VerificationAlgorithm& mAlgorithm; - const LLVMFrontendSettings& mSettings; std::unique_ptr mResult; }; @@ -109,21 +109,13 @@ char RunVerificationBackendPass::ID; LLVMFrontend::LLVMFrontend( std::unique_ptr module, - GazerContext& context, - LLVMFrontendSettings& settings) + GazerContext& context) : mContext(context), mModule(std::move(module)), - mChecks(mModule->getContext()), - mSettings(settings) + mChecks(mModule->getContext()) { llvm::initializeAnalysis(*llvm::PassRegistry::getPassRegistry()); - // Force settings to be consistent - if (mSettings.ints == IntRepresentation::Integers) { - emit_warning("-math-int mode forces havoc memory model, analysis may be unsound\n"); - mSettings.memoryModel = MemoryModelSetting::Havoc; - } - if (!PrintFinalModule.empty()) { std::error_code ec; mModuleOutput = std::make_unique(PrintFinalModule, ec, llvm::sys::fs::F_None); @@ -137,6 +129,8 @@ LLVMFrontend::LLVMFrontend( void LLVMFrontend::registerVerificationPipeline() { + mPassManager.add(createLLVMFrontendSettingsProviderPass()); + if (SkipPipeline) { mPassManager.add(new llvm::DominatorTreeWrapperPass()); this->registerVerificationStep(); @@ -162,10 +156,12 @@ void LLVMFrontend::registerVerificationPipeline() // Unify function exit nodes mPassManager.add(llvm::createUnifyFunctionExitNodesPass()); + // TODO + LLVMFrontendSettings settings = LLVMFrontendSettings::initFromCommandLine(); // Run assertion lifting. - if (mSettings.liftAsserts) { + if (settings.liftAsserts) { mPassManager.add(new llvm::CallGraphWrapperPass()); - mPassManager.add(gazer::createLiftErrorCallsPass(*mSettings.getEntryFunction(*mModule))); + mPassManager.add(gazer::createLiftErrorCallsPass()); // Assertion lifting creates a lot of dead code. Run a lightweight DCE pass // and a subsequent CFG simplification to clean up. @@ -201,17 +197,19 @@ void LLVMFrontend::registerVerificationPipeline() void LLVMFrontend::registerVerificationStep() { // Perform module-to-automata translation. - mPassManager.add(new gazer::MemoryModelWrapperPass(mContext, mSettings)); - mPassManager.add(new gazer::ModuleToAutomataPass(mContext, mSettings)); + mPassManager.add(new gazer::MemoryModelWrapperPass(mContext/*, mSettings*/)); + mPassManager.add(new gazer::ModuleToAutomataPass(mContext/*, mSettings*/)); // Execute the verifier backend if there is one. if (mBackendAlgorithm != nullptr) { - mPassManager.add(new RunVerificationBackendPass(mChecks, *mBackendAlgorithm, mSettings)); + mPassManager.add(new RunVerificationBackendPass(mChecks, *mBackendAlgorithm/*, mSettings*/)); } } bool RunVerificationBackendPass::runOnModule(llvm::Module& module) { + auto& settings = getAnalysis() + .getSettings(); auto& moduleToCfa = getAnalysis(); AutomataSystem& system = moduleToCfa.getSystem(); @@ -228,7 +226,7 @@ bool RunVerificationBackendPass::runOnModule(llvm::Module& module) llvm::outs() << "Verification FAILED.\n"; llvm::outs() << " " << msg << "\n"; - if (mSettings.trace) { + if (settings.trace) { auto writer = trace::CreateTextWriter(llvm::outs(), true); llvm::outs() << "Error trace:\n"; llvm::outs() << "------------\n"; @@ -239,24 +237,24 @@ bool RunVerificationBackendPass::runOnModule(llvm::Module& module) } } - if (!mSettings.witness.empty() && fail->hasTrace() && !mSettings.hash.empty()) { + if (!settings.witness.empty() && fail->hasTrace() && !settings.hash.empty()) { if (fail->hasTrace()) { std::error_code EC{}; - llvm::raw_fd_ostream fouts{ StringRef{mSettings.witness}, EC }; + llvm::raw_fd_ostream fouts{ StringRef{settings.witness}, EC }; - ViolationWitnessWriter witnessWriter{ fouts, mSettings.hash }; + ViolationWitnessWriter witnessWriter{ fouts, settings.hash }; witnessWriter.initializeWitness(); witnessWriter.write(fail->getTrace()); witnessWriter.closeWitness(); - } else if (mSettings.hash.empty()) { + } else if (settings.hash.empty()) { llvm::outs() << "Hash of the source file must be given to produce a witness (--hash)"; - } else if (!mSettings.witness.empty()) { + } else if (!settings.witness.empty()) { llvm::outs() << "Error witness is unavailable.\n"; } } - if (!mSettings.testHarnessFile.empty() && fail->hasTrace()) { + if (!settings.testHarnessFile.empty() && fail->hasTrace()) { llvm::outs() << "Generating test harness.\n"; auto test = GenerateTestHarnessModuleFromTrace( fail->getTrace(), @@ -264,7 +262,7 @@ bool RunVerificationBackendPass::runOnModule(llvm::Module& module) module ); - llvm::StringRef filename(mSettings.testHarnessFile); + llvm::StringRef filename(settings.testHarnessFile); std::error_code osError; llvm::raw_fd_ostream testOS(filename, osError, llvm::sys::fs::OpenFlags::OF_None); @@ -278,14 +276,14 @@ bool RunVerificationBackendPass::runOnModule(llvm::Module& module) } case VerificationResult::Success: llvm::outs() << "Verification SUCCESSFUL.\n"; - if (!mSettings.witness.empty() && !mSettings.hash.empty()) { + if (!settings.witness.empty() && !settings.hash.empty()) { // puts the witness file in the working directory of gazer std::error_code EC{}; - llvm::raw_fd_ostream fouts{ StringRef{mSettings.witness}, EC }; + llvm::raw_fd_ostream fouts{ StringRef{settings.witness}, EC }; - CorrectnessWitnessWriter witnessWriter{ fouts, mSettings.hash }; + CorrectnessWitnessWriter witnessWriter{ fouts, settings.hash }; witnessWriter.outputWitness(); - } else if(!mSettings.witness.empty() && mSettings.hash.empty()) { + } else if(!settings.witness.empty() && settings.hash.empty()) { llvm::outs() << "Hash of the source file must be given to produce a witness (--hash)"; } break; @@ -314,20 +312,23 @@ void LLVMFrontend::registerEnabledChecks() void LLVMFrontend::registerInlining() { - if (mSettings.inlineLevel != InlineLevel::Off) { + // TODO ; static because of internalizepass + static LLVMFrontendSettings settings = LLVMFrontendSettings::initFromCommandLine(); + if (settings.inlineLevel != InlineLevel::Off) { mPassManager.add(llvm::createInternalizePass([this](auto& gv) { + // TODO move to a class, require the analysis pass, etc. if (auto fun = llvm::dyn_cast(&gv)) { - return mSettings.getEntryFunction(*gv.getParent()) == fun; + return settings.getEntryFunction(*gv.getParent()) == fun; } return false; })); - mPassManager.add(gazer::createSimpleInlinerPass(*mSettings.getEntryFunction(*mModule), mSettings.inlineLevel)); + mPassManager.add(gazer::createSimpleInlinerPass()); // Remove dead functions mPassManager.add(llvm::createGlobalDCEPass()); // Inline eligible global variables - if (mSettings.inlineGlobals) { + if (settings.inlineGlobals) { mPassManager.add(gazer::createInlineGlobalVariablesPass()); } @@ -351,7 +352,9 @@ void LLVMFrontend::run() void LLVMFrontend::registerEarlyOptimizations() { - if (!mSettings.optimize) { + // TODO + LLVMFrontendSettings settings = LLVMFrontendSettings::initFromCommandLine(); + if (!settings.optimize) { return; } @@ -401,7 +404,9 @@ void LLVMFrontend::registerEarlyOptimizations() void LLVMFrontend::registerLateOptimizations() { - if (mSettings.optimize) { + // TODO + LLVMFrontendSettings settings = LLVMFrontendSettings::initFromCommandLine(); + if (settings.optimize) { mPassManager.add(llvm::createBasicAAWrapperPass()); mPassManager.add(llvm::createLICMPass()); } diff --git a/src/LLVM/LLVMFrontendSettings.cpp b/src/LLVM/LLVMFrontendSettings.cpp index 78a60523..4a12afff 100644 --- a/src/LLVM/LLVMFrontendSettings.cpp +++ b/src/LLVM/LLVMFrontendSettings.cpp @@ -17,6 +17,11 @@ //===----------------------------------------------------------------------===// #include "gazer/LLVM/LLVMFrontendSettings.h" #include "gazer/LLVM/Instrumentation/Check.h" +#include "gazer/Support/Warnings.h" + +// TODO these are bad dependencies +#include "gazer/LLVM/Memory/MemoryModel.h" +#include "gazer/LLVM/Automaton/InstToExpr.h" #include #include @@ -68,9 +73,6 @@ namespace cl::init(ElimVarsLevel::Normal), cl::cat(IrToCfaCategory) ); - cl::opt ArithInts( - "math-int", cl::desc("Use mathematical unbounded integers instead of bitvectors"), - cl::cat(IrToCfaCategory)); cl::opt NoSimplifyExpr( "no-simplify-expr", cl::desc("Do not simplify expressions"), cl::cat(IrToCfaCategory) @@ -86,14 +88,6 @@ namespace "dump-memssa", cl::desc("Dump the built MemorySSA information to stderr"), cl::cat(IrToCfaCategory) ); - cl::opt MemoryModelOpt("memory", cl::desc("Memory model to use:"), - cl::values( - clEnumValN(MemoryModelSetting::Flat, "flat", "Bit-precise flat memory model"), - clEnumValN(MemoryModelSetting::Havoc, "havoc", "Dummy havoc model") - ), - cl::init(MemoryModelSetting::Flat), - cl::cat(IrToCfaCategory) - ); // Traceability options cl::opt PrintTrace( @@ -158,14 +152,14 @@ LLVMFrontendSettings LLVMFrontendSettings::initFromCommandLine() settings.inlineLevel = InlineLevelOpt; settings.elimVars = ElimVarsLevelOpt; - settings.memoryModel = MemoryModelOpt; + settings.memoryModel = getMemoryModel(); settings.checks = EnabledChecks; settings.function = EntryFunctionName; - if (ArithInts) { + if (gazer::isArithmeticInteger()) { settings.ints = IntRepresentation::Integers; } else { settings.ints = IntRepresentation::BitVectors; @@ -178,6 +172,12 @@ LLVMFrontendSettings LLVMFrontendSettings::initFromCommandLine() settings.hash = Hash; settings.testHarnessFile = TestHarnessFile; + // Force settings to be consistent + if (settings.ints == IntRepresentation::Integers) { + emit_warning("-math-int mode forces havoc memory model, analysis may be unsound\n"); + settings.memoryModel = MemoryModelSetting::Havoc; + } + return settings; } diff --git a/src/LLVM/LLVMFrontendSettingsProviderPass.cpp b/src/LLVM/LLVMFrontendSettingsProviderPass.cpp new file mode 100644 index 00000000..88bac9df --- /dev/null +++ b/src/LLVM/LLVMFrontendSettingsProviderPass.cpp @@ -0,0 +1,34 @@ +//==-------------------------------------------------------------*- 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. +// +//===----------------------------------------------------------------------===// +#include "gazer/LLVM/LLVMFrontendSettingsProviderPass.h" + +using namespace gazer; + +void gazer::LLVMFrontendSettingsProviderPass::initializePass() { + mSettings = gazer::LLVMFrontendSettings::initFromCommandLine(); +} + +char gazer::LLVMFrontendSettingsProviderPass::ID; + +static llvm::RegisterPass + X("gazer-settings-provider", "Gazer Settings Provider Pass", false, true); + +llvm::Pass* gazer::createLLVMFrontendSettingsProviderPass() +{ + return new LLVMFrontendSettingsProviderPass(); +} diff --git a/src/LLVM/Memory/MemoryModel.cpp b/src/LLVM/Memory/MemoryModel.cpp index bd0c2f2d..71d9ac29 100644 --- a/src/LLVM/Memory/MemoryModel.cpp +++ b/src/LLVM/Memory/MemoryModel.cpp @@ -16,13 +16,27 @@ // //===----------------------------------------------------------------------===// +#include "gazer/LLVM/Memory/MemoryModel.h" + #include "gazer/Core/LiteralExpr.h" #include "gazer/LLVM/Memory/MemorySSA.h" -#include "gazer/LLVM/Memory/MemoryModel.h" +#include "gazer/LLVM/LLVMFrontendSettingsProviderPass.h" #include +#include + using namespace gazer; +using namespace llvm; + +cl::opt MemoryModelOpt("memory", cl::desc("Memory model to use:"), + cl::values( + clEnumValN(MemoryModelSetting::Flat, "flat", "Bit-precise flat memory model"), + clEnumValN(MemoryModelSetting::Havoc, "havoc", "Dummy havoc model") + ), + cl::init(MemoryModelSetting::Flat), + cl::cat(IrToCfaCategory) +); // LLVM pass implementation //===----------------------------------------------------------------------===// @@ -31,7 +45,11 @@ char MemoryModelWrapperPass::ID; void MemoryModelWrapperPass::getAnalysisUsage(llvm::AnalysisUsage& au) const { - switch (mSettings.memoryModel) { + au.addRequired(); + + // TODO + LLVMFrontendSettings settings = LLVMFrontendSettings::initFromCommandLine(); + switch (settings.memoryModel) { case MemoryModelSetting::Flat: au.addRequired(); case MemoryModelSetting::Havoc: @@ -45,13 +63,15 @@ void MemoryModelWrapperPass::getAnalysisUsage(llvm::AnalysisUsage& au) const bool MemoryModelWrapperPass::runOnModule(llvm::Module& module) { - switch (mSettings.memoryModel) { + auto& settings = getAnalysis() + .getSettings(); + switch (settings.memoryModel) { case MemoryModelSetting::Flat: { auto dominators = [this](llvm::Function& function) -> llvm::DominatorTree& { return getAnalysis(function).getDomTree(); }; - mMemoryModel = CreateFlatMemoryModel(mContext, mSettings, module, dominators); + mMemoryModel = CreateFlatMemoryModel(mContext, settings, module, dominators); break; } case MemoryModelSetting::Havoc: { @@ -64,3 +84,7 @@ bool MemoryModelWrapperPass::runOnModule(llvm::Module& module) return true; } + +MemoryModelSetting& gazer::getMemoryModel() { + return MemoryModelOpt.getValue(); +} \ No newline at end of file diff --git a/src/LLVM/Transform/Inline.cpp b/src/LLVM/Transform/Inline.cpp index 5dd02555..3d820906 100644 --- a/src/LLVM/Transform/Inline.cpp +++ b/src/LLVM/Transform/Inline.cpp @@ -24,6 +24,7 @@ #include "TransformUtils.h" #include "gazer/LLVM/Transform/Passes.h" +#include "gazer/LLVM/LLVMFrontendSettingsProviderPass.h" #include #include @@ -44,15 +45,15 @@ class InlinePass : public llvm::ModulePass static char ID; public: - InlinePass(llvm::Function* entry, InlineLevel level) - : ModulePass(ID), mEntryFunction(entry), mLevel(level) + InlinePass() + : ModulePass(ID) { - assert(mEntryFunction != nullptr); } void getAnalysisUsage(llvm::AnalysisUsage& au) const override { au.addRequired(); + au.addRequired(); } bool runOnModule(llvm::Module& module) override; @@ -64,7 +65,6 @@ class InlinePass : public llvm::ModulePass private: bool shouldInlineFunction(llvm::CallGraphNode* target, unsigned allowedRefs); - llvm::Function* mEntryFunction; InlineLevel mLevel; }; @@ -104,6 +104,13 @@ bool InlinePass::shouldInlineFunction(llvm::CallGraphNode* target, unsigned allo bool InlinePass::runOnModule(llvm::Module& module) { + auto& settings = getAnalysis() + .getSettings(); + auto* entryFunction = settings.getEntryFunction(module); + assert(entryFunction != nullptr); + + mLevel = settings.inlineLevel; + if (mLevel == InlineLevel::Off) { return false; } @@ -114,7 +121,7 @@ bool InlinePass::runOnModule(llvm::Module& module) llvm::InlineFunctionInfo ifi(&cg); llvm::SmallVector wl; - llvm::CallGraphNode* entryCG = cg[mEntryFunction]; + llvm::CallGraphNode* entryCG = cg[entryFunction]; for (auto& [call, target] : *entryCG) { if (this->shouldInlineFunction(target, 1)) { @@ -145,7 +152,12 @@ bool InlinePass::runOnModule(llvm::Module& module) return changed; } -llvm::Pass* gazer::createSimpleInlinerPass(llvm::Function& entry, InlineLevel level) +static llvm::RegisterPass X("gazer-inline", + "Gazer Simple inline pass", + false /* Only looks at CFG */, + false /* Analysis Pass */); + +llvm::Pass* gazer::createSimpleInlinerPass() { - return new InlinePass(&entry, level); + return new InlinePass(); } diff --git a/src/LLVM/Transform/InlineGlobalVariablesPass.cpp b/src/LLVM/Transform/InlineGlobalVariablesPass.cpp index 95e639e9..b8642fed 100644 --- a/src/LLVM/Transform/InlineGlobalVariablesPass.cpp +++ b/src/LLVM/Transform/InlineGlobalVariablesPass.cpp @@ -209,6 +209,10 @@ bool InlineGlobalVariablesPass::runOnModule(Module& module) } // end anonymous namespace +static llvm::RegisterPass X("gazer-inline-global-vars", "Gazer Inline Global Variables", + false /* Only looks at CFG */, + false /* Analysis Pass */); + namespace gazer { @@ -216,4 +220,4 @@ llvm::Pass* createInlineGlobalVariablesPass() { return new InlineGlobalVariablesPass(); } -} // end namespace gazer \ No newline at end of file +} // end namespace gazer diff --git a/src/LLVM/Transform/LiftErrorsPass.cpp b/src/LLVM/Transform/LiftErrorsPass.cpp index d19e08ce..0cac1bd2 100644 --- a/src/LLVM/Transform/LiftErrorsPass.cpp +++ b/src/LLVM/Transform/LiftErrorsPass.cpp @@ -23,6 +23,7 @@ #include "gazer/LLVM/Transform/Passes.h" #include "gazer/LLVM/Instrumentation/Check.h" #include "gazer/LLVM/Transform/BackwardSlicer.h" +#include "gazer/LLVM/LLVMFrontendSettingsProviderPass.h" #include #include @@ -105,20 +106,24 @@ class LiftErrorCallsPass : public llvm::ModulePass static char ID; public: - LiftErrorCallsPass(llvm::Function* function) - : ModulePass(ID), mEntryFunction(function) + LiftErrorCallsPass() + : ModulePass(ID) {} void getAnalysisUsage(AnalysisUsage& au) const override { au.addRequired(); + au.addRequired(); } bool runOnModule(Module& module) override { auto& cg = getAnalysis(); + auto* entryFunction = getAnalysis() + .getSettings() + .getEntryFunction(module); - LiftErrorCalls impl(module, cg.getCallGraph(), *mEntryFunction); + LiftErrorCalls impl(module, cg.getCallGraph(), *entryFunction); return impl.run(); } @@ -318,7 +323,7 @@ bool LiftErrorCalls::run() return true; } -llvm::Pass* gazer::createLiftErrorCallsPass(llvm::Function& entry) +llvm::Pass* gazer::createLiftErrorCallsPass() { - return new LiftErrorCallsPass(&entry); + return new LiftErrorCallsPass(); } diff --git a/src/LLVM/Transform/LoopExitCanonizationPass.cpp b/src/LLVM/Transform/LoopExitCanonizationPass.cpp index 59f17048..54033cb8 100644 --- a/src/LLVM/Transform/LoopExitCanonizationPass.cpp +++ b/src/LLVM/Transform/LoopExitCanonizationPass.cpp @@ -110,6 +110,11 @@ bool LoopExitCanonizationPass::runOnFunction(llvm::Function& function) return changed; } +static llvm::RegisterPass X("gazer-canonize-loop-exit", + "Gazer loop exit canonizer pass", + false /* Only looks at CFG */, + false /* Analysis Pass */); + llvm::Pass* gazer::createCanonizeLoopExitsPass() { return new LoopExitCanonizationPass(); } \ No newline at end of file diff --git a/src/LLVM/Transform/NormalizeVerifierCalls.cpp b/src/LLVM/Transform/NormalizeVerifierCalls.cpp index fb73b51c..0545a6f1 100644 --- a/src/LLVM/Transform/NormalizeVerifierCalls.cpp +++ b/src/LLVM/Transform/NormalizeVerifierCalls.cpp @@ -132,6 +132,11 @@ void NormalizeVerifierCallsPass::runOnFunction(llvm::Function& function) } } +static llvm::RegisterPass X("gazer-normalize-verifier-calls", + "Gazer Normalize Verifier Calls", + false /* Only looks at CFG */, + false /* Analysis Pass */); + llvm::Pass* gazer::createNormalizeVerifierCallsPass() { return new NormalizeVerifierCallsPass(); diff --git a/src/LLVM/Transform/UndefToNondet.cpp b/src/LLVM/Transform/UndefToNondet.cpp index 96e03978..618f1c09 100644 --- a/src/LLVM/Transform/UndefToNondet.cpp +++ b/src/LLVM/Transform/UndefToNondet.cpp @@ -86,5 +86,9 @@ bool UndefToNondetCallPass::runOnModule(llvm::Module& module) return changed; } +static llvm::RegisterPass X("gazer-promote-undefs", + "Gazer Promote Undef values", + false /* Only looks at CFG */, + false /* Analysis Pass */); -llvm::Pass* gazer::createPromoteUndefsPass() { return new UndefToNondetCallPass(); } \ No newline at end of file +llvm::Pass* gazer::createPromoteUndefsPass() { return new UndefToNondetCallPass(); } diff --git a/src/Support/CMakeLists.txt b/src/Support/CMakeLists.txt index 3fa14045..123e9e25 100644 --- a/src/Support/CMakeLists.txt +++ b/src/Support/CMakeLists.txt @@ -2,7 +2,4 @@ set(SOURCE_FILES SExpr.cpp Runtime.cpp) -llvm_map_components_to_libnames(LLVM_LIBS support) - add_library(GazerSupport ${SOURCE_FILES}) -target_link_libraries(GazerSupport ${LLVM_LIBS}) diff --git a/src/Verifier/CMakeLists.txt b/src/Verifier/CMakeLists.txt deleted file mode 100644 index 76c91746..00000000 --- a/src/Verifier/CMakeLists.txt +++ /dev/null @@ -1,7 +0,0 @@ -set(SOURCE_FILES - BoundedModelChecker.cpp - BmcTrace.cpp -) - -add_library(GazerVerifier SHARED ${SOURCE_FILES}) -target_link_libraries(GazerVerifier GazerCore GazerAutomaton GazerTrace) diff --git a/tools/gazer-bmc/CMakeLists.txt b/tools/gazer-bmc/CMakeLists.txt index 510de546..ef2b0e10 100644 --- a/tools/gazer-bmc/CMakeLists.txt +++ b/tools/gazer-bmc/CMakeLists.txt @@ -2,5 +2,13 @@ set(SOURCE_FILES gazer-bmc.cpp ) +set(LIB_SOURCE_FILES + lib/BoundedModelChecker.cpp + lib/BmcTrace.cpp +) + +add_library(GazerBackendBmc ${LIB_SOURCE_FILES}) +target_link_libraries(GazerBackendBmc GazerLLVM) + add_executable(gazer-bmc ${SOURCE_FILES}) -target_link_libraries(gazer-bmc GazerLLVM GazerZ3Solver) \ No newline at end of file +target_link_libraries(gazer-bmc GazerLLVM GazerZ3Solver GazerBackendBmc) diff --git a/tools/gazer-bmc/gazer-bmc.cpp b/tools/gazer-bmc/gazer-bmc.cpp index 2be82f00..4820e9e5 100644 --- a/tools/gazer-bmc/gazer-bmc.cpp +++ b/tools/gazer-bmc/gazer-bmc.cpp @@ -101,8 +101,11 @@ int main(int argc, char* argv[]) Z3SolverFactory solverFactory; auto bmcSettings = initBmcSettingsFromCommandLine(); - bmcSettings.simplifyExpr = frontend->getSettings().simplifyExpr; - bmcSettings.trace = frontend->getSettings().trace; + + // TODO + LLVMFrontendSettings settings = LLVMFrontendSettings::initFromCommandLine(); + bmcSettings.simplifyExpr = settings.simplifyExpr; + bmcSettings.trace = settings.trace; frontend->setBackendAlgorithm(new BoundedModelChecker(solverFactory, bmcSettings)); frontend->registerVerificationPipeline(); diff --git a/src/Verifier/BmcTrace.cpp b/tools/gazer-bmc/lib/BmcTrace.cpp similarity index 100% rename from src/Verifier/BmcTrace.cpp rename to tools/gazer-bmc/lib/BmcTrace.cpp diff --git a/src/Verifier/BoundedModelChecker.cpp b/tools/gazer-bmc/lib/BoundedModelChecker.cpp similarity index 100% rename from src/Verifier/BoundedModelChecker.cpp rename to tools/gazer-bmc/lib/BoundedModelChecker.cpp diff --git a/src/Verifier/BoundedModelCheckerImpl.h b/tools/gazer-bmc/lib/BoundedModelCheckerImpl.h similarity index 100% rename from src/Verifier/BoundedModelCheckerImpl.h rename to tools/gazer-bmc/lib/BoundedModelCheckerImpl.h diff --git a/tools/gazer-bmc/lib/CMakeLists.txt b/tools/gazer-bmc/lib/CMakeLists.txt new file mode 100644 index 00000000..e69de29b diff --git a/tools/gazer-cfa/gazer-cfa.cpp b/tools/gazer-cfa/gazer-cfa.cpp index 0d7fa1e1..c3638251 100644 --- a/tools/gazer-cfa/gazer-cfa.cpp +++ b/tools/gazer-cfa/gazer-cfa.cpp @@ -40,7 +40,8 @@ namespace { cl::list InputFilenames(cl::Positional, cl::OneOrMore, cl::desc("")); cl::opt ViewCfa("view", cl::desc("View the CFA in the system's GraphViz viewier.")); - cl::opt CyclicCfa("cyclic", cl::desc("Represent LoopRep as cycles instead of recursive calls.")); + // TODO does not work in this setting + //cl::opt CyclicCfa("cyclic", cl::desc("Represent LoopRep as cycles instead of recursive calls.")); cl::opt RunPipeline("run-pipeline", cl::desc("Run the early stages of the verification pipeline, such as instrumentation.")); } @@ -61,15 +62,15 @@ int main(int argc, char* argv[]) return 1; } - if (CyclicCfa) { - frontend->getSettings().loops = LoopRepresentation::Cycle; - } + //if (CyclicCfa) { + // frontend->getSettings().loops = LoopRepresentation::Cycle; + //} if (RunPipeline) { frontend->registerVerificationPipeline(); } else { - frontend->registerPass(new gazer::MemoryModelWrapperPass(config.context, frontend->getSettings())); - frontend->registerPass(new gazer::ModuleToAutomataPass(config.context, frontend->getSettings())); + frontend->registerPass(new gazer::MemoryModelWrapperPass(config.context)); + frontend->registerPass(new gazer::ModuleToAutomataPass(config.context)); frontend->registerPass(gazer::createCfaPrinterPass()); } diff --git a/tools/gazer-theta/gazer-theta.cpp b/tools/gazer-theta/gazer-theta.cpp index 0bcdfd26..e489ba9a 100644 --- a/tools/gazer-theta/gazer-theta.cpp +++ b/tools/gazer-theta/gazer-theta.cpp @@ -19,6 +19,7 @@ #include "lib/ThetaCfaGenerator.h" #include "gazer/LLVM/LLVMFrontend.h" +#include "gazer/LLVM/Automaton/InstToExpr.h" #include "gazer/Support/Runtime.h" #include "gazer/Support/Warnings.h" @@ -120,7 +121,8 @@ int main(int argc, char* argv[]) } // Force -math-int - config.getSettings().ints = IntRepresentation::Integers; + gazer::isArithmeticInteger() = true; + // config.getSettings().ints = IntRepresentation::Integers; // Create the frontend object auto frontend = config.buildFrontend(InputFilenames); diff --git a/unittest/ADT/CMakeLists.txt b/unittest/ADT/CMakeLists.txt index d912c8aa..ecd97689 100644 --- a/unittest/ADT/CMakeLists.txt +++ b/unittest/ADT/CMakeLists.txt @@ -4,5 +4,5 @@ SET(TEST_SOURCES ) add_executable(GazerAdtTest ${TEST_SOURCES}) -target_link_libraries(GazerAdtTest gtest_main GazerSupport) -add_test(GazerAdtTest GazerAdtTest) \ No newline at end of file +target_link_libraries(GazerAdtTest gtest_main GazerLLVM) +add_test(GazerAdtTest GazerAdtTest) diff --git a/unittest/Automaton/CMakeLists.txt b/unittest/Automaton/CMakeLists.txt index bd2d7942..45481d0b 100644 --- a/unittest/Automaton/CMakeLists.txt +++ b/unittest/Automaton/CMakeLists.txt @@ -5,5 +5,5 @@ SET(TEST_SOURCES ) add_executable(GazerAutomatonTest ${TEST_SOURCES}) -target_link_libraries(GazerAutomatonTest gtest_main GazerCore GazerAutomaton) -add_test(GazerAutomatonTest GazerAutomatonTest) \ No newline at end of file +target_link_libraries(GazerAutomatonTest gtest_main GazerLLVM) +add_test(GazerAutomatonTest GazerAutomatonTest) diff --git a/unittest/Core/CMakeLists.txt b/unittest/Core/CMakeLists.txt index abccdf59..f40b38e8 100644 --- a/unittest/Core/CMakeLists.txt +++ b/unittest/Core/CMakeLists.txt @@ -11,4 +11,4 @@ SET(TEST_SOURCES add_test(GazerCoreTest GazerCoreTest) add_executable(GazerCoreTest ${TEST_SOURCES}) -target_link_libraries(GazerCoreTest GazerCore gtest_main) \ No newline at end of file +target_link_libraries(GazerCoreTest GazerLLVM gtest_main) diff --git a/unittest/SolverZ3/CMakeLists.txt b/unittest/SolverZ3/CMakeLists.txt index fdd5fa7e..fde63c3e 100644 --- a/unittest/SolverZ3/CMakeLists.txt +++ b/unittest/SolverZ3/CMakeLists.txt @@ -4,5 +4,5 @@ SET(TEST_SOURCES ) add_executable(GazerSolverZ3Test ${TEST_SOURCES}) -target_link_libraries(GazerSolverZ3Test gtest_main GazerCore GazerZ3Solver) -add_test(GazerSolverZ3Test GazerSolverZ3Test) \ No newline at end of file +target_link_libraries(GazerSolverZ3Test gtest_main GazerLLVM GazerZ3Solver) +add_test(GazerSolverZ3Test GazerSolverZ3Test) diff --git a/unittest/Support/CMakeLists.txt b/unittest/Support/CMakeLists.txt index 9544b2c3..379eb033 100644 --- a/unittest/Support/CMakeLists.txt +++ b/unittest/Support/CMakeLists.txt @@ -3,5 +3,5 @@ SET(TEST_SOURCES ) add_executable(GazerSupportTest ${TEST_SOURCES}) -target_link_libraries(GazerSupportTest gtest_main GazerSupport) -add_test(GazerSupportTest GazerSupportTest) \ No newline at end of file +target_link_libraries(GazerSupportTest gtest_main GazerLLVM) +add_test(GazerSupportTest GazerSupportTest)