-
Notifications
You must be signed in to change notification settings - Fork 5
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Restructure packages #49
base: master
Are you sure you want to change the base?
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-module2automata should 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.
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/Verifier
insidetools/gazer-bmc/lib
(as it works the same as the files intools/gazer-theta/lib/
)opt
tool 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)