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

Regenerate the CDE package #42

Closed
ccadar opened this issue Oct 14, 2013 · 5 comments
Closed

Regenerate the CDE package #42

ccadar opened this issue Oct 14, 2013 · 5 comments
Labels
Feature Request New feature that should be implemented in KLEE

Comments

@ccadar
Copy link
Contributor

ccadar commented Oct 14, 2013

The CDE package for KLEE (http://ccadar.github.io/klee/GetStarted.html#cde) is out-of-date and needs to be regenerated.
@delcypher
Copy link
Contributor

Perhaps we should consider using Docker instead. It is actively worked on and seems pretty cool :)

@riyadparvez
Copy link

Hi,
I've built a docker image for Klee experimental version which built against llvm 3.4. Please find it here https://github.com/riyadparvez/klee-docker.

@ccadar
Copy link
Contributor Author

ccadar commented Jan 16, 2015

Thanks. Is there any reason for which you haven't uploaded it to the Docker registry? If everything works fine, it would be also useful to have instructions on the KLEE website on how to use Docker to quickly getting started with KLEE.

@delcypher
Copy link
Contributor

@riyadparvez You should add a non-root user and switch to that once all the required packages are installed. It is not desirable to be building or running KLEE as root inside a container.

@ccadar
Copy link
Contributor Author

ccadar commented Nov 19, 2015

Given the availability of Docker images now, I think we don't need CDE packages anymore.

@ccadar ccadar closed this as completed Nov 19, 2015
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 18, 2016
@zaddach
Initial implementation of BitField simplifier (refs klee#42).
a57d3ae 
git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@14968 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 18, 2016
@zaddach
Move work on expression simplifier (refs klee#42):
f22213c 
- Implemented top-down ignoredBits simplification
- Cache already-optimized subexpressions
- Invoke simplifications from Executor

git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@14977 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 18, 2016
@zaddach
Implemented more optimizations (refs klee#42)
e786e7d 
git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@14980 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 18, 2016
@zaddach
Implemented Concat optimizations (refs klee#42).
e78be73 
git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@14981 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 18, 2016
@zaddach
- Disabled select instruction optimization, which is incorrect (refs k…
be69eee 
…lee#42) - Added pass to remove select instructions from the LLVM code. These instructions end up as is in the constraint set and complicate the solving - Optimized expression builder to remove redundant chains of ZExt/Truncates.

git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@15000 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 18, 2016
@zaddach
Bugfix (refs klee#42).
0d68db1 
git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@15033 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 18, 2016
@zaddach
Bugfix (refs klee#42)
fc24ffc 
git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@15040 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 19, 2016
@zaddach
Initial implementation of BitField simplifier (refs klee#42).
4fe62f4 
git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@14968 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 19, 2016
@zaddach
Move work on expression simplifier (refs klee#42):
18c62b4 
- Implemented top-down ignoredBits simplification
- Cache already-optimized subexpressions
- Invoke simplifications from Executor

git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@14977 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 19, 2016
@zaddach
Implemented more optimizations (refs klee#42)
4d1fbe9 
git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@14980 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 19, 2016
@zaddach
Implemented Concat optimizations (refs klee#42).
728b0c7 
git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@14981 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 19, 2016
@zaddach
- Disabled select instruction optimization, which is incorrect (refs k…
9c017b7 
…lee#42) - Added pass to remove select instructions from the LLVM code. These instructions end up as is in the constraint set and complicate the solving - Optimized expression builder to remove redundant chains of ZExt/Truncates.

git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@15000 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 19, 2016
@zaddach
Bugfix (refs klee#42).
0857f1b 
git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@15033 f94e2f5b-dfd8-4992-a279-46519bc7c46e
zaddach pushed a commit to avatarone/news2e-klee that referenced this issue Jul 19, 2016
@zaddach
Bugfix (refs klee#42)
0917062 
git-svn-id: https://dslabpc10.epfl.ch/svn/src/s2e/trunk@15040 f94e2f5b-dfd8-4992-a279-46519bc7c46e
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
Feature Request New feature that should be implemented in KLEE
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@riyadparvez @delcypher @ccadar