From b55ab1489eca755ed03fe08b600e33c098097861 Mon Sep 17 00:00:00 2001 From: radl97 Date: Mon, 21 Sep 2020 15:48:05 +0200 Subject: [PATCH 1/8] Remove Z3Solver duplicate linkage --- src/LLVM/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/LLVM/CMakeLists.txt b/src/LLVM/CMakeLists.txt index 8f6ccff2..af021f7b 100644 --- a/src/LLVM/CMakeLists.txt +++ b/src/LLVM/CMakeLists.txt @@ -38,4 +38,4 @@ llvm_map_components_to_libnames(GAZER_LLVM_LIBS core irreader transformutils sca message(STATUS "Using LLVM libraries: ${GAZER_LLVM_LIBS}") add_library(GazerLLVM SHARED ${SOURCE_FILES}) -target_link_libraries(GazerLLVM ${GAZER_LLVM_LIBS} GazerCore GazerTrace GazerZ3Solver GazerAutomaton GazerVerifier) +target_link_libraries(GazerLLVM ${GAZER_LLVM_LIBS} GazerCore GazerTrace GazerAutomaton GazerVerifier) From 1c291d9f65d08aa51692771b74cfc9c3b0e4b1aa Mon Sep 17 00:00:00 2001 From: radl97 Date: Mon, 21 Sep 2020 15:49:22 +0200 Subject: [PATCH 2/8] Move BMC (LLVM/Verifier) inside gazer-bmc --- src/CMakeLists.txt | 3 +-- src/LLVM/CMakeLists.txt | 2 +- src/Verifier/CMakeLists.txt | 7 ------- tools/gazer-bmc/CMakeLists.txt | 10 +++++++++- {src/Verifier => tools/gazer-bmc/lib}/BmcTrace.cpp | 0 .../gazer-bmc/lib}/BoundedModelChecker.cpp | 0 .../gazer-bmc/lib}/BoundedModelCheckerImpl.h | 0 tools/gazer-bmc/lib/CMakeLists.txt | 0 8 files changed, 11 insertions(+), 11 deletions(-) delete mode 100644 src/Verifier/CMakeLists.txt rename {src/Verifier => tools/gazer-bmc/lib}/BmcTrace.cpp (100%) rename {src/Verifier => tools/gazer-bmc/lib}/BoundedModelChecker.cpp (100%) rename {src/Verifier => tools/gazer-bmc/lib}/BoundedModelCheckerImpl.h (100%) create mode 100644 tools/gazer-bmc/lib/CMakeLists.txt diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 52df5ca4..4599a1b7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -2,10 +2,9 @@ add_subdirectory(Core) add_subdirectory(Automaton) add_subdirectory(LLVM) add_subdirectory(Trace) -add_subdirectory(Verifier) add_subdirectory(Support) # Add requested solvers if ("z3" IN_LIST GAZER_ENABLE_SOLVERS) add_subdirectory(SolverZ3) -endif() \ No newline at end of file +endif() diff --git a/src/LLVM/CMakeLists.txt b/src/LLVM/CMakeLists.txt index af021f7b..42bc3cd8 100644 --- a/src/LLVM/CMakeLists.txt +++ b/src/LLVM/CMakeLists.txt @@ -38,4 +38,4 @@ llvm_map_components_to_libnames(GAZER_LLVM_LIBS core irreader transformutils sca message(STATUS "Using LLVM libraries: ${GAZER_LLVM_LIBS}") add_library(GazerLLVM SHARED ${SOURCE_FILES}) -target_link_libraries(GazerLLVM ${GAZER_LLVM_LIBS} GazerCore GazerTrace GazerAutomaton GazerVerifier) +target_link_libraries(GazerLLVM ${GAZER_LLVM_LIBS} GazerCore GazerTrace GazerAutomaton) 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/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 From 76bc3d4e98718d9d415af2ca3471ad1657516fd1 Mon Sep 17 00:00:00 2001 From: radl97 Date: Thu, 24 Sep 2020 11:58:48 +0200 Subject: [PATCH 3/8] Remove LLVM linkage from GazerSupport --- src/Support/CMakeLists.txt | 3 --- 1 file changed, 3 deletions(-) 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}) From fcefdd525ed43949f97cd2ac6adc231423709db8 Mon Sep 17 00:00:00 2001 From: radl97 Date: Thu, 24 Sep 2020 12:19:49 +0200 Subject: [PATCH 4/8] Register the simplest passes for opt integration --- src/LLVM/Transform/InlineGlobalVariablesPass.cpp | 6 +++++- src/LLVM/Transform/NormalizeVerifierCalls.cpp | 5 +++++ src/LLVM/Transform/UndefToNondet.cpp | 6 +++++- 3 files changed, 15 insertions(+), 2 deletions(-) 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/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(); } From 6d1066b338e9aca32e02d9f3d25835e7dbb2422f Mon Sep 17 00:00:00 2001 From: radl97 Date: Thu, 24 Sep 2020 12:24:08 +0200 Subject: [PATCH 5/8] Create module for usage with LLVM's opt tool --- src/LLVM/CMakeLists.txt | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/src/LLVM/CMakeLists.txt b/src/LLVM/CMakeLists.txt index 42bc3cd8..bf17260b 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 @@ -15,12 +15,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 @@ -32,10 +26,25 @@ set(SOURCE_FILES Automaton/ExtensionPoints.cpp Automaton/ValueOrMemoryObject.cpp Analysis/PDG.cpp + TypeTranslator.cpp ) +set(SOURCE_FILES + LLVMTraceBuilder.cpp + LLVMFrontendSettings.cpp + LLVMFrontend.cpp + ClangFrontend.cpp + FrontendConfig.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 GazerAutomaton) +target_link_libraries(GazerLLVM GazerLLVMBare ${GAZER_LLVM_LIBS}) From d7c03a396f3b892d1437fa6f9d476a8615df894f Mon Sep 17 00:00:00 2001 From: radl97 Date: Thu, 24 Sep 2020 15:36:07 +0200 Subject: [PATCH 6/8] Link against GazerLLVM in unit tests --- unittest/ADT/CMakeLists.txt | 4 ++-- unittest/Automaton/CMakeLists.txt | 4 ++-- unittest/Core/CMakeLists.txt | 2 +- unittest/SolverZ3/CMakeLists.txt | 4 ++-- unittest/Support/CMakeLists.txt | 4 ++-- 5 files changed, 9 insertions(+), 9 deletions(-) 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) From e8d229b255f8bd7e88e7086140e00e45127ce0f6 Mon Sep 17 00:00:00 2001 From: radl97 Date: Mon, 9 Nov 2020 23:18:16 +0100 Subject: [PATCH 7/8] Create Settings provider pass LLVM uses passes for managing configuration/settings data. LLVMFrontendSettingsProviderPass is created to better integrate with LLVM's infrastructure, which is useful for e.g. creating small tests for single LLVM passes with opt. Some settings are moved inside their most representing classes: MemoryModel setting inside MemoryModel.(cpp|h), Arithmetic int representation inside InstToExpr.(cpp|h) The goal is to be able to create passes without additional arguments (include "arguments" through analysis). This way with opt, gazer-* passes can be managed from the commandline, which in turn can be used for testing unit transformations in the pipeline. --- include/gazer/LLVM/Automaton/InstToExpr.h | 2 + .../gazer/LLVM/Automaton/ModuleToAutomata.h | 5 +- include/gazer/LLVM/LLVMFrontend.h | 14 ++-- include/gazer/LLVM/LLVMFrontendSettings.h | 12 +++ .../LLVM/LLVMFrontendSettingsProviderPass.h | 42 ++++++++++ include/gazer/LLVM/Memory/MemoryModel.h | 8 +- include/gazer/LLVM/Transform/Passes.h | 4 +- src/LLVM/Automaton/AutomatonPasses.cpp | 9 ++- src/LLVM/Automaton/InstToExpr.cpp | 13 +++ src/LLVM/CMakeLists.txt | 2 +- src/LLVM/FrontendConfig.cpp | 17 ++-- src/LLVM/LLVMFrontend.cpp | 79 ++++++++++--------- src/LLVM/LLVMFrontendSettings.cpp | 26 +++--- src/LLVM/LLVMFrontendSettingsProviderPass.cpp | 34 ++++++++ src/LLVM/Memory/MemoryModel.cpp | 32 +++++++- src/LLVM/Transform/Inline.cpp | 21 +++-- src/LLVM/Transform/LiftErrorsPass.cpp | 15 ++-- tools/gazer-bmc/gazer-bmc.cpp | 7 +- tools/gazer-cfa/gazer-cfa.cpp | 13 +-- tools/gazer-theta/gazer-theta.cpp | 4 +- 20 files changed, 258 insertions(+), 101 deletions(-) create mode 100644 include/gazer/LLVM/LLVMFrontendSettingsProviderPass.h create mode 100644 src/LLVM/LLVMFrontendSettingsProviderPass.cpp 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/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 665f09a4..caf566e8 100644 --- a/src/LLVM/CMakeLists.txt +++ b/src/LLVM/CMakeLists.txt @@ -37,7 +37,7 @@ set(SOURCE_FILES 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}) 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/LLVMFrontend.cpp b/src/LLVM/LLVMFrontend.cpp index 86abb3aa..121f2884 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(/* *settings.getEntryFunction(*mModule)*/)); // 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..e1b75c3a 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,7 @@ bool InlinePass::runOnModule(llvm::Module& module) return changed; } -llvm::Pass* gazer::createSimpleInlinerPass(llvm::Function& entry, InlineLevel level) +llvm::Pass* gazer::createSimpleInlinerPass() { - return new InlinePass(&entry, level); + return new InlinePass(); } 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/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/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); From 6f67360dac4e8564c304c1c60148133cf21ba43e Mon Sep 17 00:00:00 2001 From: radl97 Date: Sun, 6 Dec 2020 17:11:07 +0100 Subject: [PATCH 8/8] Add some pass registrations --- src/LLVM/Instrumentation/MarkFunctionEntries.cpp | 6 ++++++ src/LLVM/LLVMFrontend.cpp | 2 +- src/LLVM/Transform/Inline.cpp | 5 +++++ src/LLVM/Transform/LoopExitCanonizationPass.cpp | 5 +++++ 4 files changed, 17 insertions(+), 1 deletion(-) 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 121f2884..51922040 100644 --- a/src/LLVM/LLVMFrontend.cpp +++ b/src/LLVM/LLVMFrontend.cpp @@ -161,7 +161,7 @@ void LLVMFrontend::registerVerificationPipeline() // Run assertion lifting. if (settings.liftAsserts) { mPassManager.add(new llvm::CallGraphWrapperPass()); - mPassManager.add(gazer::createLiftErrorCallsPass(/* *settings.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. diff --git a/src/LLVM/Transform/Inline.cpp b/src/LLVM/Transform/Inline.cpp index e1b75c3a..3d820906 100644 --- a/src/LLVM/Transform/Inline.cpp +++ b/src/LLVM/Transform/Inline.cpp @@ -152,6 +152,11 @@ bool InlinePass::runOnModule(llvm::Module& module) return changed; } +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(); 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