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

[Mark Mossberg]

I see, thanks Rick!

> On Aug 25, 2017, at 8:07 PM, Richard Rutledge <rrutledge3 at gatech.edu> wrote:
> 
> 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 <mark at 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 <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/20170828/f7343e30/attachment.p7s>