I see, thanks Rick! > On Aug 25, 2017, at 8:07 PM, Richard Rutledge <[email protected]> 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 <[email protected]> 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> >>
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
