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

Rethink building procedure #28

Open
ghost opened this issue Aug 24, 2020 · 2 comments
Open

Rethink building procedure #28

ghost opened this issue Aug 24, 2020 · 2 comments
Assignees
Labels
enhancement New feature or request

Comments

@ghost
Copy link

ghost commented Aug 24, 2020

Linking with LLVM is heavy operation and for development, it would be good to not link LLVM to GazerLLVM module, rather only link (of course, still dynamically) to the main binary.
Plus this allows us to use LLVM's opt utility which is useful for debugging. (opt already links LLVM: the error is similar to this: ziglang/zig#67 )

@ghost ghost changed the title Improve link time Rethink building procedure Sep 2, 2020
@ghost ghost added the enhancement New feature or request label Sep 2, 2020
@radl97 radl97 self-assigned this Sep 14, 2020
@radl97
Copy link
Contributor

radl97 commented Sep 14, 2020

The build process has some flaws:

  1. Only gazer-bmc uses GazerZ3Solver, but disabling it does not work. (update: Also, GazerVerifier is used only in gazer-bmc)
  2. gazer-bmc, gazer-theta and gazer-cfa functional tests could be split to test only portion of the code.
  3. GazerLLVM linkage is a heavy operation because of the big LLVM library (libraries, to be exact). This could be added at the last build stage, if I'm not mistaken.
  4. Z3Solver is downloaded (or at least the version is checked online) at every make invocation, which is too heavy for an iterative build system.

I'm not too familiar with the CMake build system, I'll try play around a bit to speed up the process (mainly for the iterative building)

@radl97
Copy link
Contributor

radl97 commented Sep 14, 2020

Here are the dependencies, according to CMake

gazer_build_tree

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

No branches or pull requests

1 participant