Refine intervals with def_exc exclusion range

[sim642]

Currently opened on top of #634 because that fix makes many spurious precision comparisons disappear on incremental bench. This PR should probably be rebased to master.

Changes

1. Adds def_exc exclusion range (bits) to refine_with_excl_list argument, so intervals can refine themselves accordingly. If combined with once int refinement, the original problem from Basic incremental can be more precise than from-scratch due to type-based interval widening #626 is fixed.
2. Adds the option ana.int.interval_narrow_by_meet. This is necessary because the previous refinement can actually cause precision loss! Namely, a more precise interval than the type bounds prevents interval narrow from improving. Doing a meet instead allows that to happen regardless.

[michael-schwarz]

ana.int.interval_narrow_by_meet sounds really problematic, there is not even really a guarantee that it would terminate (for previous versions of TD3 we had such non-terminating examples, c.f. loops that are only spuriously live and one could probably construct such loops where we are not strict in the loop entry as it has multiple entry points).

Might not hurt to have it, but I would suggest not making it the default.

[sim642]

If I remember correctly, @vesalvojdani thought it should be the default. And I'm not sure about the examples, because we have examples where one narrowing is required to improve the widened upper bound (which a single meet would do as well and even better in this situation), but I don't remember us ever having any where narrowing itself was the cause of non-termination.

I'm not sure what the spuriously live loops, strict loop entry and multi-entry loops have to do with this. The example in #233 (comment) wasn't problematic for TD3 to begin with (only full-phased solvers) and the involved narrowing is one-step: [50, inf] -> [50, 50].

Do you have a better way of fixing the internal consistency between int domains in mind? Because otherwise enabling int domain refinement can actually make observable precision worse, which is completely against any intuition or the goal of that refinement.

[michael-schwarz]

I'm not sure what the spuriously live loops, strict loop entry and multi-entry loops have to do with this.

Even though at the time we could not discuss it on the issue tracker, because we had a student who was supposed to investigate these things for his thesis, the example in #233 is an example in which (non-accelerated) narrowing by meet will not terminate (or take very long to converge in our setting where there are no infinite descending chains) depending on the solver strategy chosen.

int g = 0;

int main() {
  int x;

  for(x=0; x < 50; x++){
    g = 1;
  }
  // x = [50, 50] after narrow
  if(x>50){ // live after widen, but dead after narrow
    // node after Pos(x>50) is marked dead at the end
    for(int i=0; i<=0; i--){
      // narrowing at the loop head by meet will produce values
      // [-infinity,0] -> [-infinity,-1] -> [-infinity,-2] -> ...
      // as the maximum will be decreased by 1 in the loop, and only the
      // back edge has a non-bot contribution
      g = 57;
    }
  }
}

This example does not currently not work anymore, as we are strict in the loop entry, but there are cases where we are not. I don't see any reason why one should not be able to construct a similar non-terminating execution also for TD3. This is why I am skeptical about turning narrow by meet on by default.

[michael-schwarz]

I found an example for slr3tp that shows the problem:

int g = 0;

int main() {
  int x;

  for(x=0; x < 50; x++){
    g = 1;
  }

  // x = [50, 50] after narrow
  if(x>50){ // live after widen, but dead after narrow
    // node after Pos(x>50) is marked dead at the end
    // but the loop is not with x = [51,2147483647]
	for(int i=0;i<=0; i--){
      l: g = 57;
    }
  }

  // x = [50, 50] after narrow
  if( x> 50) {
  	goto l;
  }

e: return 5;
}

on this branch with ./goblint 1.c --set solver slr3tp --html --enable ana.int.interval --set sem.int.signed_overflow assume_none it does not terminate.

If I add --disable ana.int.interval_narrow_by_meet it does.

[vesalvojdani]

Yes, I'm not sure I wanted this to be the global default. Helmut had some argument why intervals will always terminate since there will always be a non-empty intersection, but I guess that was an argument that assumed very simple solvers. Anyway, this will be the base configuration for our incremental analysis, especially for comparisons, where we know what solver we use. But more generally, most people would expect interval narrowings to work as defined in textbooks and we should pick defaults that cause the least surprise.

[sim642]

Alright, I flipped the default, but to get a bunch of precision annotation tests to pass (because they use int domain refinement), I had to still enable it for those.

Anyway, this will be the base configuration for our incremental analysis

Then if this is approved, (rebased to master) and merged, everyone has to update their incremental configurations. Otherwise there's no consistency and we're comparing apples to oranges.