[klee-dev] KLEE intermixing concrete and symbolic execution question

[Mark Mossberg]

Hi all,

I have a question about KLEE. In the article "Symbolic Execution for Software Testing: Three Decades Later”[1], there is this quotation:

> Execution-Generated Testing (EGT): The EGT approach [9], implemented and extended by the EXE [10] and KLEE [8] tools, works by making a distinction between the concrete and symbolic state of a program. To this end, EGT in- termixes concrete and symbolic execution by dynamically checking before every operation if the values involved are all concrete. If so, the operation is executed just as in the original program. Otherwise, if at least one value is sym- bolic, the operation is performed symbolically, by updat- ing the path condition for the current path.


Could someone please point out to me where in the code the aforementioned “dynamic check” occurs? Looking at the tree as of commit d19500e, I would expect some kind of check before `executeInstruction` is called in `Executor:run()`, since `executeInstruction` appears to directly symbolically execute an LLVM IR instruction. However, I don’t see any kind of check like this.

The article is from 2013, so please let me know if that quote isn’t accurate for the current state of KLEE.

Thanks,
Mark

[1]: https://pdfs.semanticscholar.org/1144/3efe465ad544f478524da6c66c085b16e28b.pdf <https://pdfs.semanticscholar.org/1144/3efe465ad544f478524da6c66c085b16e28b.pdf>

-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3866 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20170825/a5c154b2/attachment.p7s>