Force concretization to follow seeds#1117
Conversation
Codecov Report
@@ Coverage Diff @@
## master #1117 +/- ##
==========================================
+ Coverage 67.45% 67.61% +0.15%
==========================================
Files 155 155
Lines 17540 17552 +12
Branches 4046 4051 +5
==========================================
+ Hits 11832 11868 +36
+ Misses 3856 3828 -28
- Partials 1852 1856 +4
|
|
Thanks, @hoangmle, that's a useful contribution! I'm a bit behind with reviewing PRs, but I'll try to take a look soon. |
|
@hoangmle thanks again for the patch! It makes a lot of sense, and I'm happy with the code (there might be an argument for refactoring the concretization sequence into a separate function, but we can revise this later). I have only a few change requests in the tests. |
| @@ -0,0 +1,26 @@ | |||
| // RUN: %clang -emit-llvm -c -g %s -o %t.bc | |||
| // RUN: rm -rf %t.klee-out | |||
| // RUN: %klee --output-dir=%t.klee-out --entry-point=TestGen %t.bc "initial" | |||
| // RUN: not test -f %t.klee-out/test000002.ktest | ||
|
|
||
| // RUN: rm -rf %t.klee-out-2 | ||
| // RUN: %klee --external-calls=all --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest %t.bc |
There was a problem hiding this comment.
I would structure this test as follows:.
- run KLEE here with
-exit-on-error, 2) remove theRUN: grepline and 3) change the assert into an equality, i.e.,assert(abs(z) == 0xBADA55)
There was a problem hiding this comment.
Also add a comment at the beginning of the test saying what this is testing, e.g., "Testing that seeds are used during concretization of arguments in external calls".
| @@ -0,0 +1,27 @@ | |||
| // RUN: %clang -emit-llvm -c -g %s -o %t.bc | |||
| @@ -0,0 +1,27 @@ | |||
| // RUN: %clang -emit-llvm -c -g %s -o %t.bc | |||
There was a problem hiding this comment.
I would also structure this test as the other two. This also seems a bit more complicated than it should be. I would just allocate a very large value, and then check via an assert that you get it back.
|
@hoangmle are you still interested in merging this patch? It was almost ready (modulo some small changes in the tests), although now it will need to be rebased. |
|
@ccadar thanks for the reminder, I'll try to finish the PR next week |
|
Superseded by #1663 |
2 participants
Even in seed mode, KLEE still concretizes expressions to solver-picked values ignoring all seeds. This behavior is not very useful, especially for hybrid fuzzing. This PR tries to force concretization to follow one of the seeds in the 3 most common cases (symbolic memory allocation, floating point instructions and external calls). It is also possible to keep following all seeds by forking multiple states, but the implementation is more complex and I do not currently have a use-case for that.