Interval Analysis for Floating-point values

[Dudeldu]

Issue

Current Situation

Currently, Goblint is unable to analyze double values (and for that matter, float values as well - but we will focus on
double for now).

Motivation

• floating-point models are quite complex and features such as rounding and special numbers (infinities, NaN , etc.) are not always understood by programmers.
• many (embedded) usecases for interaction with the real world (sensor input, motion output, etc.)
• prominent errors with floating points have already led to catastrophic behaviors, such as the Patriot missile accident [1]

Goal

We aim to implement an interval analysis for double values. Therefore, we heavily rely on [1]. As is written there, roundings
and underflows are tolerated, but not overflows, divisions by zero or invalid operations. For these, we want goblint
to generate a warning or an error.

In a first approach, in order to be able to tackle the four different rounding modes and arbitrary precision of
intermediate results, we will implement a worst-case analysis as proposed in [1]. In other words, we won't care about
the given rounding mode and instead work conservatively with the intervals. Like this, we won't necessarily be able to
say that a program is correct, but we will be able to say if might be incorrect.

With this information we aim to provide checking of assertions and dead-branches and warnings for potential usages of invalid double values - namely NaN, +/- infinity.

Example

int main()
{
    double middle;
    double a = DBL_MAX;
    double b = DBL_MAX;

    middle = middle * 1.;  // Of course this should result in a warning, due to no information about middle and
                           // since it could therefore be NaN / infinity / neg_infinity

    middle = (a + b) / 2.; // Naive way of computing the middle, which (might) result in an overflow

    return middle - 100.   // Further uses of the overflown middle value should result in a warning
}

[1]: https://www-apr.lip6.fr/~mine/publi/article-mine-esop04.pdf

WIP here

[michael-schwarz]

Nice, it's about time Goblint gets support for floating point numbers!

[sim642]

I suppose the current goal is to add this to our base analysis's ValueDomain?

I'm just wondering, because the other angle to floating-point would be to do it in the apron analysis, since the Apron library also supports floating-point arithmetic (but we currently only use integer portions of it).

[michael-schwarz]

I suppose the current goal is to add this to our base analysis's ValueDomain?

Yes! I also plan to play around with Apron's float support a bit. However, that seemed a bit involved for a practical course, and I am a bit unclear on how one would soundly handle rounding here. Also, I think having some (cheap) float support in the base analysis is crucial, as we quite often don't enable Apron for performance reasons!

[sim642]

Indeed, having something simple which isn't Apron-based would be useful too.
I don't want to go on a tangent, but Apron expressions allow specifying some rounding modes: https://antoinemine.github.io/Apron/doc/api/ocaml/Texpr1.html#TYPEround.

[michael-schwarz]

Apron expressions allow specifying some rounding modes

The question is if there is a rounding mode that is always sound or whether we have to analyze which C rounding mode is currently set which is annoying. In the thing that we'll be implementing, we are avoiding that by always rounding in the "worse" direction.

[michael-schwarz]

Closed in #761