Hi, 1. Both KLEE floating point implementations mentioned in the paper have been mostly dormant since we finished the paper.
2. This question rates a fairly complicated answer, so let me go at it in pieces: a) Both implementations are reasonably stable for many kinds of simple floating point operations. b) There are many different and increasingly complicated sides to floating point operations. For example things like changing the floating point environment to modify rounding modes are not supported in either implementation. c) Exact Floating point analysis is a very much a problem: The floating point theory exhibited by our SMT solver of choice (Z3) does not always map naturally onto x86_64 (e.g. bit-exact reasoning over NaNs is problematic). The floating point theories exhibited by clang and GCC do not always agree. Some of the most prolific uses of floating point numbers (e.g. graphics) have spawned devices that simply don't work exactly (you are not going to notice a difference in the lowest bit of the mantissa of the red value of a single pixel on your screen). d) Floating point SMT solving is still in its infancy, causing floating point reasoning to very quickly exhibit atrocious performance behavior. For example, when we were doing the work for the paper about 2 years ago, I had a benchmark that simply squared a number repeatedly waiting for it to overflow to infinity. After only a few multiplications (low single-digits), solving costs on that branch would spiral out of control. We also encountered several instances of the solver giving incorrect results. e) On the other hand, size of the *program* does not really specifically impact the floating point reasoning and neither does the complexity of the integer reasoning. f) To the best of my knowledge, neither prototype has seen much use beyond our work on the ASE paper. Most importantly, we are really lacking someone independent from us to give a proper answer to the real-world usability. g) In summary, basic arithmetic operations on symbolic FP variables should not be a problem. I still would not claim that analysis of a medium-complexity FP program would work out - since I expect the SMT solver to exhibit insufficient performance. 3. We had a discussion if we should try to incorporate floating point solving into KLEE, but mainly decided FP SMT solving was not yet stable enough. The technical complexity of moving our changes to KLEE 1.4 should not be that large. Yours, Daniel Schemmel On 31.07.2018 02:26, Guo,Shengjian wrote: > > Hi all, > > > > Recently I work on a project with KLEE which involves floating point > inputs. > > I read Daniel Liew’s ASE’17 paper regarding the comparison of KLEE’s > two extensions supporting floating point symbolization. > > And here are some questions about it: > > 1. What’s the current status of the klee-float repository > (https://github.com/srg-imperial/klee-float, seems no commits this > year)? > 2. Is it quite stable to run some medium-sized programs invoking > floating point operations? E.g., add, sub, multiply, divide and > combinations of these on symbolic floating point variables. > 3. How difficult could it be to incorporate klee-float to KLEE-1.4? > Is it possible to finish this job in one or two weeks? (I’ve been > working with KLEE for 4 years). > > > > Thanks, > > Daniel. > > > > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
