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.

Sign up for GitHub

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

Jump to bottom

LLVM Optimizations with KLEE #16

Open
rafaelsamenezes opened this issue Oct 2, 2019 · 0 comments
Open

LLVM Optimizations with KLEE #16

rafaelsamenezes opened this issue Oct 2, 2019 · 0 comments
Assignees
@hbgit @rafaelsamenezes
Labels
enhancement

Comments

@rafaelsamenezes
Copy link
Collaborator

Is your feature request related to a problem? Please describe.
Not related to a problem. Currently, we default to -O3 optimizations and let KLEE decides which solver to be used. The -O3 may not be the best for Symbolic Execution and the SMT formula generated by KLEE may not be the best for the selected solver.

Describe the solution you'd like
We should select which solver and the best optimization for Symbolic Execution.

Describe alternatives you've considered
Extend Map2Check to have a class to select which optimizations will be done.

Additional context
The paper Studying the influence of standard compiler optimizations on symbolic execution contains details on how LLVM optimizations affects KLEE and the solvers
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@hbgit hbgit

@rafaelsamenezes rafaelsamenezes

Labels
enhancement
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@hbgit @rafaelsamenezes