Analysis tracking equality between calls to math library functions to improve invariant

[FelixKrayer]

I was part of last year's practical course implementing the interval domain for floats. One issue we were unfortunately unable to solve was using certain math library functions in the invariant. Consider the following piece of code:

if (isfinite(f)) {
    __goblint_check(! isnan(f)); 
}

In this case the check would result in unknown, because the code is transformed into the following where the call to the library function cannot be detected at the if-check. Thus f cannot be refined to be finite in this example:

tmp__0 = isfinite(f);
if (tmp__0) {
    tmp__1 = isnan(f);
    __goblint_check(! tmp__1);
}

This pull request adds a new analysis TmpSpecial tracking equalities between lvals and calls to library functions together with the corresponding arguments.
Additionally a set of lval is tracked for each equality. This describes the lvals the equality depends on, i.e., lvals contained within the arguments as well as the lval of the assignment. This set is used to delete equalities when an lval it depends on is written.
The information this analysis collects is accessed in the base Invariant via a query to refine arguments of a call. Some examples of this refinement can be seen in regtest 57/19.

TODO:

• better inversion of ceil and floor

[michael-schwarz]

I will first start a run of sv-comp on the current master, such that we have a baseline to compare against.

[michael-schwarz]

I started the run with this analysis enabled just now, let's see what the results are!

[michael-schwarz]

Something to consider: What is the relationship of this with the varEq analysis we already have? Can there be some reuse?

[sim642]

Something to consider: What is the relationship of this with the varEq analysis we already have? Can there be some reuse?

var_eq tracks equalities between CIL expressions, but function calls are not part of those, so I don't think there's much to be done. If anything, then this is more similar to condvars, which I think exists for a similar purpose, but with logical expressions (transformed by CIL) instead of special function calls.

This could be combined with var_eq in another (not reuse) way. That is, to track the return value of a special function not just through a single assignment to temporary just before a branch, but through a longer chain of manually written assignments. But that would just involve some extra queries to var_eq I suppose.

[michael-schwarz]

I did a run on sv-comp but it seems that the analysis sadly does not really make a difference 😞

tmpSpecial.zip

[michael-schwarz]

I started another run after the fixes now, let's see if that changes something!

[sim642]

I did a run on sv-comp but it seems that the analysis sadly does not really make a difference disappointed

It might be worth checking with grep if sv-benchmarks even contains such pattern in the first place, or whether it's something that only exists in real-world programs. I didn't look deeply at the implementation, but sv-benchmarks contains many cilled programs, where such transformation could already be hard-coded instead of being introduced by our CIL. Maybe that affects the applicability of this analysis?

[FelixKrayer]

I did a run on sv-comp but it seems that the analysis sadly does not really make a difference disappointed

It might be worth checking with grep if sv-benchmarks even contains such pattern in the first place, or whether it's something that only exists in real-world programs. I didn't look deeply at the implementation, but sv-benchmarks contains many cilled programs, where such transformation could already be hard-coded instead of being introduced by our CIL. Maybe that affects the applicability of this analysis?

I did a quick search through the sv-comp repository and did only find 1456 files that include math.h. From what I could find, most of them do not use any interesting function (fabs, isfinite, isnan) in a way where this analysis is helpful.
Furthermore a search for fabs (380 files), isfinite (28 files) and isnan (150 files) only resulted in me finding many "custom" implementations of these functions and only a few uses of the library functions. Unfortunately none of these were in cases, where this analysis could provide an improvement (mostly the functions were just used in checks, but then there was no way, a refinement could be beneficial).
It seems like this analysis is in general not useful for the sv-comp benchmarks.

As for the transformations already being hardcoded, this should not be a problem. The analysis tracks the equality between a variable and the math descriptor and it does not matter, if the transformation was introduced by CIL or if it was already hardcoded in the code.

[FelixKrayer]

I have implemented the requested changes as well as a better inversion of the floor and ceil functions. The current version is quite sophisticated. It differentiates between float / double , which Goblint represents with the correct precision, and long double / float128, which are represented using double intervals. There are some insights we can use to be more precise when we know that the precision used for the abstract intervals is the same as in the concrete values.

The commit prior to the most recent one implements a more conservative way to invert floor and ceil that does not use these insights.

[michael-schwarz]

Thank you for sticking with this @FelixKrayer, very happy to see this merged now! 🎉

[FelixKrayer]

Awesome! Glad to see it merged after I now finally finished it up.