Conversation
|
Also I'm thinking of pulling different objects to be handled by LLVM; e.g. create an GazerContextAnalysisPass that can be accessed by all passes. MemoryModelWrapperPass would determine from its arguments, that which memory model is to be used... |
opt -load GazerLLVM.so
-mem2reg
-gazer-promote-undefs
-gazer-normalize-verifer-calls
-gazer-register-checks
-gazer-mark-entries
-gazer-internalize-non-main
-gazer-simple-inline
-globaldce
-gazer-inline-global-vars
-globaldce
-mem2reg
-mergereturn
-callgraphwrapperxx
-lift-error-calls
-dce
-simplifycfg
-basic-aa
-licm
-globalopt
-globaldce
-simplifycfg
-loop-simplify
-instnamer
-mergereturn
# -gazer-memory-model # this would be required by module2automata
-gazer-module2automatashould run everything when you run gazer-bmc, except the backend itself. |
|
So, update: I want to move settings to the part of the code that uses it. Currently LLVMFrontend(Settings).cpp contains the flags understood by LLVM, it is build into an LLVMFrontendSettings... Next step is to include more passes. This is limited by passes that have parameters... So including an analysis pass for initializing the later-parameters (that will be queried by the specific passes) will do the trick. Somthing like LLVMFrontentSettingsWrapperPass :D |
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.
1 participant
This PR is to improve generic high-level structure of Gazer. Bugs are hard to catch, and finding out which exact passes introduce an error or a weird instruction is hard. This PR would contain some improvements.
src/LLVM/Verifierinsidetools/gazer-bmc/lib(as it works the same as the files intools/gazer-theta/lib/)opttool to test specific passes. (This might also need restructure from passes that use objects with their lifetime handled outside LLVM's framework, e.g. that use GazerContext)