Mark,
The quote is accurate, but the "dynamic check" is not explicitly coded
into 'executeInstruction'. Rather, the check is implicitly incorporated
in the values operated upon by 'executeInstruction'.
Operands to the instruction set are expressed as an abstraction (Expr)
encompassing both concrete and symbolic values.
For details, look in Expr.h and lib/Expr/*.cpp
Cheers!
Rick Rutledge
On Fri, Aug 25, 2017 at 5:44 PM, Mark Mossberg <m...@trailofbits.com>
wrote:
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
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
