Hello,
I'm interested in using KLEE to test for integer overflow along different execution paths. C programs, by default, do not raise any exception or warning in the case of an overflow. However, since KLEE relies on the LLVM interpreter and the constraint solver, I assume this functionality would be possible to add by modifying KLEE or STP in some way. Let's assume I'm only interested in the results of binary addition operations to keep things simple, and that I simply want to print an error message if an addition operation takes place that overflows (or could have overflowed, depending on the constraints) along some path of execution. Presumably, detecting overflow would require distinguishing cases in which one or both operands are symbolic, and cases in which both arguments are concrete. In the concrete case, it may also be necessary to distinguish constants from variables. Other relevant issues might include the bit widths of the operands, and whether the values are signed or unsigned. I've examined the LLVM interpreter, and successfully identified the location at which simple binary arithmetic takes place, but this code does not appear to be used directly in KLEE. I'm specifically referring to code in lib/ExecutionEngine/Interpreter/Execution.cpp. As I'm largely unfamiliar with the KLEE codebase, I was wondering if anyone with more experience could simply suggest the files / locations in the source relevant to solving this problem. I can write back with more specific questions if necessary. Thank you for any assistance, Matt -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110225/f773fda2/attachment.html
