On Thu, Dec 02, 2010 at 06:52:14PM -0500, Denver Gingerich wrote: > Peter Collingbourne mentioned back in July that there was a branch of > KLEE that includes floating point support: > > http://keeda.stanford.edu/pipermail/klee-dev/2010-July/000428.html > > I'd like to use this branch, but before I invest a bunch of time > getting it setup, I'm interested in knowing how stable it is. I plan > to run some fairly complicated programs through it; does it seem > likely that it will break in a significant number of non-trivial use > cases?
Hi Denver, Since July we have added SIMD capabilities to the KLEE-FP branch, and we have also used it to cross check the scalar vs SIMD implementations of a large open source computer vision library (1000's of lines of code were tested in total), so it's been proven to work on (largely) unmodified real world code. Perhaps you can say a bit more about the kinds of programs you are planning to test and the benchmarks you plan to run. As I mentioned in my previous email, KLEE-FP is designed for equality testing using structural equivalence, which to a certain extent limits its floating point capabilities to cross checking problems. If you would like to learn more I gave a talk at the LLVM developers meeting this year, the slides and video are online. http://llvm.org/devmtg/2010-11/ I can also send you (off-list) a preview copy of a research paper we have been working on. Thanks, -- Peter
