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

[Richard Rutledge]

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
> 
-------------- next part --------------
HTML attachment scrubbed and removed