[klee-dev] Question about the status of KLEE-float (https://github.com/srg-imperial/klee-float).

[Daniel Schemmel]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed