Strange overflow behaviour

[DrMichaelPetter]

The following issue popped up when doing intensive sv-comp tests:

//SKIP PARAM:  --enable ana.int.interval --set ana.activated[+] affeq --set sem.int.signed_overflow assume_none
int a;

int main() {
    a = 5;
    a = a + 1 - 1; //NOWARN
    return 0;
}

This test would fail due to eval_int of texpr a evaluating for some mysterious reason to top, and then in the next step being incremented by one, causing the overflow in line 6.

This

1. happens for affeq as well as lin2vareq; it is revealed during the expression conversion that happens for relationalAnalyses in sharedFunctions, since this does some calls to eval_int
2. happens only for a being a global variable, disappearing for a local a declaration.

Fixing this will make a few no-overflow tasks in sv-comp solvable for lin2vars and affeqs.

A quick dive into what happens during analysis time revealed some interactions with some a#in and a#out that I do not understand yet, but maybe someone wants to lend a hand.

[sim642]

A quick dive into what happens during analysis time revealed some interactions with some a#in and a#out that I do not understand yet, but maybe someone wants to lend a hand.

My quick guess would be that the overflow handling in relational analyses, which makes those queries, doesn't correctly handle those temporary variables and does queries on a#in, which other analyses know nothing about.

[DrMichaelPetter]

A quick dive into what happens during analysis time revealed some interactions with some a#in and a#out that I do not understand yet, but maybe someone wants to lend a hand.

My quick guess would be that the overflow handling in relational analyses, which makes those queries, doesn't correctly handle those temporary variables and does queries on a#in, which other analyses know nothing about.

That is probably what is happening - the resulting value "top" for an eval_int on a#in etc. is intended, then?

[michael-schwarz]

The worst parts about his are fixed in aed4cec by setting the speculative flag. However, this is not really a viable long-term solution.

[sim642]

There might be some discussion somewhere, but the clean solution would be to move overflow warning generation out of int domain operators themselves and have the new MaySignedOverflow query be used explicitly to generate these warnings.
Int domain operators already return overflow_info in addition to the result, so this could simply be used by MaySignedOverflow.