Int domain refinement causes fixpoint error

[AdrianKrauss]

A second program, which we believe has the same problem but terminates with a fixpoint error (which maybe makes the debugging easier), is the following:

// PARAM:  --conf ./svcomp_bitfield.json --set ana.specification ./unreach-call.prp

reach_error() {}
a(b) {
  if (!b) {
    reach_error();
    abort();
  }
}

main() {
  int c = 0;
  unsigned d;
  unsigned e = 0;
  while (5) {
    c = c + 1;
    d = d + 2;
    e = e + 3;
    a(e == c + d);
  }
}

However, the fixpoint error of the second program only occured with activated refinements and the activated bitfield domain of our PR (see #1623 ). Without our bitfield domain but still with activated refinements, the second program terminates normally without any problems. Therefore, we need a slightly different config file to produce this error:
svcomp_bitfield.json

[sim642]

Domain refinement interacting poorly with widening is a known phenomenon in abstract interpretation. For this reason, IntDomTuple is supposed to not do refinement in widening:

analyzer/src/cdomain/value/cdomains/int/intDomTuple.ml

Lines 393 to 394 in bce9f92

	let widen ik =
	map2 ~norefine:true ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.widen ik)}

So it's quite surprising that there's somehow still an issue. I thought that the join in widen old (join old new) by the solvers might be the issue, but that also disables refinement.

[michael-schwarz]

Have you tried disabling witnesses? They often cause issues.

[sim642]

Have you tried disabling witnesses? They often cause issues.

If so, then it might be another example of #1322. I suspect the join old new has something to do with it by always joining in old path dependencies. PR #1484 has a similar case where widen old new would be really beneficial (and where the transition to https://link.springer.com/chapter/10.1007/978-981-19-9601-6_4 would be a good idea).

[michael-schwarz]

The problem seems to be unrelated to witnesses.

// PARAM: --set ana.int.refinement fixpoint --enable ana.int.enums  --enable ana.int.interval --set sem.int.signed_overflow assume_none
int main() {
   int count = 0;
   while (1) {
     count++;
     count++;
   }
 }

However, it appears to be connected to assume_none for sem.int.signed_overflow...

[michael-schwarz]

And huge props to @AdrianKrauss and the rest of you, this minimized example has been essential in getting to the root cause!

[michael-schwarz]

Minimal example where it misbehaves with not finding the fixpoint (decoupled from SV-COMP). Interestingly #1674 does not fix the issue, whereas #1675 does.

// PARAM: --set ana.activated[+] abortUnless --set exp.unrolling-factor 4  --enable ana.int.interval_threshold_widening --enable ana.int.bitfield --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval --set ana.int.refinement fixpoint

int a(int b) {
  if (!b) {
    abort();
  }
}

main() {
  int c = 0;
  unsigned d;
  unsigned e = 0;
  while (1) {
    c = c + 1;
    d = d + 2;
    e = e + 3;
    a(e == c + d);
  }
}

[michael-schwarz]

// PARAM: --set ana.activated[+] abortUnless  --enable ana.int.interval_threshold_widening --enable ana.int.bitfield --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval --set ana.int.refinement fixpoint

int a(int b) {
  if (!b) {
    abort();
  }
}

int main(void)
{
  int c = 1;
  unsigned int d = 2;
  unsigned int e = 3;

  a(e == (unsigned int )c + d);

  c ++;
  d += 2U;
  e += 3U;


  c ++;
  d += 2U;
  e += 3U;

  while (1) {
    c ++;
    d += 2U;
    e += 3U;
    a(e == (unsigned int )c + d);
  }


  return (0);

}

Without loop unrolling.

[michael-schwarz]

With @jerhard I traced the fixpoint error and it is in fact due to a mistake in Congruences (#1587)

%%% congruence: sub : 3ℤ ℤ -> 3ℤ

The minimized program if someone wants to take a look again:

// PARAM: --enable ana.int.bitfield --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval --set ana.int.refinement fixpoint

int main(void)
{
  unsigned int c = 3;
  unsigned int d = 6;
  unsigned int e = 9;
  int burgo;

  while (1) {
    c ++;

    d += 2U;

    e += 3U;

    assert(e == (unsigned int )c + d);

    burgo = 23;
  }

  return (0);

}