Pedantically: > unsigned a,b,c,d; I assume you mean int; undefined overflow is perfectly well defined in C99 (6.2.5p9, if you are bored).
In general, klee is not set up to do this sort of thing. Actually, this is not a klee problem but a by-product of using LLVM. It isn't valid to try to apply C language semantics to the LLVM IR. Ultimately, the front-end would have to communicate the semantics about about may or may not overflow. By the time things are translated into LLVM, the semantics are precise; it would be a mistake to diagnose overflow because the LLVM instructions are well defined and optimization passes and other transformations (for example, code created by the front-end but not something the user wrote directly) are free to create them (and most certainly do). The "correct" approach to this problem is to modify the front-end to diagnose "undefined" overflow. We have actually talked about doing this in clang, and for overflow it is not even that difficult. For example, modifying clang to call abort on overflowing add of signed integers would be about < 10 lines of code. This has the advantages of not requiring modifications to klee, and allowing compile time elimination of many overflow checks. Since I've brought it up, clang's code generation for C is getting complete enough that it is conceivable to run klee on clang generated LLVM code instead of using llvm-gcc (some recent milestones are building working versions of gcc 4.2 and the FreeBSD kernel). Two particularly salient reasons to do this are: (1) Hacking clang to add these kinds of checks in the frontend is relatively simple. (2) clang includes a full blown gcc-compatible driver. Although currently the driver only focuses on building native object files, it can readily be extended to support building linked LLVM bitcode executables (getting rid of the hacky klee-gcc). This would simplify the process of building things to run with klee. - Daniel On Wed, Mar 4, 2009 at 11:27 PM, Dawson Engler <engler at csl.stanford.edu> wrote: > > let's say we have a complex arithmetic expression. ?is there a simple > clean way to assert that no intermediate results (subexpressions) > contain an overflow? > > e.g., if we have > ? ? ? ?unsigned a,b,c,d; > > ? ? ? ?a+b+c+d > > > i'd like to assert that a+b+c+d does not overflow. ?however i'm worried > that the way klee works subexpressions can overflow, ?but the entire > expression won't. ?for example, if a+b overflows, KLEE could perform > the addition, truncate the result to 32 bits, then do the rest of the > additions with the result that the entire expression does not overflow, > but the subexpression does. > > i believe we had this problem w/ FT when doing underconstrained, but > don't know if it also shows up in KLEE. > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.Stanford.EDU > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
