On Thu, Jul 01, 2010 at 04:38:04PM -0400, Robby Cochran wrote: > I'm interested in running klee on code that would generate constraints > on floating point operations. Is anyone else doing this? Would it be > possible to couple a constraint solver, other than STP, that supports > arithmetic on reals?
Hi Robby, I (together with others at Imperial) am working on an experimental KLEE branch that among other things adds floating point capabilities to KLEE. We decided against modelling floating point arithmetic using real arithmetic for a number of reasons. The main reason is that real arithmetic does not model the loss of precision inherent to floating point arithmetic. Nor does it model the degenerate floating point cases such as infinities or NaNs. Instead we have opted for an approach that is suited more for cross checking purposes. To test an equality constraint we test the two trees for structural equivalence, modulo certain transformation rules. In general no constraint solvers are involved in this process. If you are interested in the code it is publically available in our git repository: http://git.pcc.me.uk/?p=~peter/klee-fp.git;a=summary As I mentioned this is an experimental branch so it may crash when dealing with certain constraints. The build instructions in www/GetStarted.html are also changed. Thanks, -- Peter
