Skip to content
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

Draft
wants to merge 9 commits into
base: master
Choose a base branch
from
Draft

Restructure packages #49

wants to merge 9 commits into from

Conversation

radl97
Copy link
Contributor

@radl97 radl97 commented Sep 21, 2020

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.

  • Move src/LLVM/Verifier inside tools/gazer-bmc/lib (as it works the same as the files in tools/gazer-theta/lib/)
  • Remove Z3Solver as a dependency (this was a small bug)
  • Create a way to use LLVM's 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)

@radl97 radl97 added the enhancement New feature or request label Sep 21, 2020
@radl97 radl97 self-assigned this Sep 21, 2020
@radl97
Copy link
Contributor Author

radl97 commented Sep 21, 2020

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...
This should enable debugging pass-by-pass, if all goes well...

@radl97
Copy link
Contributor Author

radl97 commented Sep 21, 2020

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.

@radl97
Copy link
Contributor Author

radl97 commented Sep 24, 2020

So, update:
Binaries are non-inclusive right now. Specifically: LLVM libraries are not linked to the smallest unit of projects (directories/shared binaries). GazerLLVM is the smallest package that contains its own transitive closure.
This is because opt tool requires that you do NOT LLVM libraries inside your binaries, and it does not seem a pain right now. (However unit tests are linked against the whole library, so it will get slower link-time)

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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant