On Mon, Dec 6, 2010 at 12:58 PM, Peter Collingbourne <peter at pcc.me.uk> wrote: > 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.
I'd like to use KLEE-FP to generate test cases for various floating point inputs, similar to what is done for integers in Tutorial One (http://klee.llvm.org/Tutorial-1.html). However, it seems like this might be outside of the cross checking scope of the current KLEE-FP. Is the test generation I described possible with KLEE-FP? If not, is it something that is easy and/or likely to be implemented? Thanks for your time. Denver http://ossguy.com/
