Int domain refinement causes fixpoint error

[sim642]

Given the following program:

// PARAM: --set ana.int.refinement fixpoint --enable ana.int.interval
// FIXPOINT
#include<assert.h>

int g = 0;

void main()
{
   int i = 0;
   while (1) {
      i++;
      for (int j=0; j < 10; j++) {
         if (i > 100) g = 1;
      }
      if (i>9) i=0;
   }
   return;
}

The verify phase fails with the fixpoint error due to

Map: g =
 (Unknown int([0,1]),[0,2147483647]) instead of (Unknown int([0,1]),[0,1]).

Although we implement interval refinement from exclusion range, this isn't applied here, probably because int domain refinement is disabled for join and widen. However, some refinement is required here because the two abstractions have the same concretization, so verification should succeed as it is sound.

There is possible need for int domain refinement in precise incremental benchmarks. Otherwise there are spurious precision comparisons due to similar reasons (exclusion range being more precise than interval).

[sim642]

Surprisingly, letting join not refine, but making widen refine passes all our tests, including this one.

https://link.springer.com/chapter/10.1007/978-3-540-77505-8_23 mention an obscure concept of pre-widening as a version of join which doesn't refine/reduce. Seems like we might want that in some places (like widening iterations), but a refining join in most others (joining over all incoming edges). The non-refinement in join and widen is only to make widening correct and terminating, elsewhere it should be fine to have that extra precision.

[sim642]

Turns out there are other angles to this issue as well. With --disable ana.opt.hashcons everything is fine. Hashconsing assumes that lattice operations are idempotent and skips the operation if arguments are equal.

However, int domains violate this assumption, for example:

(Unknown int([0,1]),[0,2147483647]) narrow (Unknown int([0,1]),[0,2147483647]) = (Unknown int([0,1]),[0,1])

[sim642]

Reopening because the root cause isn't fixed by #1186:

#1005 also mentions a different but related issue that refinement could be applied more often still, but I think this we can save for a separate PR, this PR fixes the immediate issue and makes refinement usable together with hash consing).

[michael-schwarz]

New example of this problem not fixed by #1186:

On master (5cd8650)

 ./goblint --conf /home/goblint/michael-schwarz-dissertation/analyzer/conf/traces.json --set ana.base.privatization lock --enable ana.int.interval --set ana.int.refinement once  ../bench/concrat/cava/cava.c

causes fixpoint errors that are clearly due to missing refinement:

 Difference: Map: [mutex:(lockset:{}, multiplicity:{})] = [base:Map: p =
  {Map: autobars = (Unknown int([0,1]),[0,2147483647],{0, 1}) instead of (Unknown int([0,1]),[0,1],{0, 1})
    Map: is_bin = (Unknown int([-7,7]),[-2147483648,2147483647],{-1, 0, 1}) instead of (Unknown int([-7,7]),[-1,1],{-1, 0, 1})
    Map: stereo = (Unknown int([-7,7]),[-2147483648,2147483647],{-1, 0, 1}) instead of (Unknown int([-7,7]),[-1,1],{-1, 0, 1})
    Map: xaxis = (Unknown int([0,7]),[0,4294967295],{0, 1, 2}) instead of (Unknown int([0,7]),[0,2],{0, 1, 2}) ...}]

The same holds when the refinement strategy is set to fixpoint.