Improve precision for `%`

[michael-schwarz]

  int top;

  int c = -5;
  if(top) { c= -7;}
  __goblint_check(c % 2 == 1); // Doesn't hold at runtime

Goblint claims that this would hold.

For constants it works correctly:

  __goblint_check(-5 % 2 == -1);

Update: This has now been fixed to be sound in #1161, but remains more imprecise than possible, so we should carefully attempt to make it more precise while remaining sound.

[michael-schwarz]

After some discussion with Helmut, it seems that just our implementation of [[x%y]]# is wrong, as it would need to return both the positive and the negative value if we don't know the sign of x.

[michael-schwarz]

I would propose dividing this issue into two issues, one to be sound again, which I'll work on and one to restore precision which I'll leave for someone else.

[sim642]

Something related to this shows up in our own witness validation in SV-COMP. This is illustrated with the following test, where the assertion is unknown:

#include <assert.h>

int main() {
  int x;
  if (x % 2 == 1) {
    assert(x % 2 == 1);
    return 1;
  }
  return 0;
}

According to tracing %%% congruence: rem : 1+2ℤ 2 -> 1+2ℤ , although it should be 1.

[michael-schwarz]

%%% congruence: rem : 1+2ℤ 2 -> 1+2ℤ unless we know the sign of the the argument to %2, this is the best we can do!

[michael-schwarz]

One way to fix this is to have the guard Pos(x % 2 == 1) refine x to be positive.

[michael-schwarz]

@hseidl and I constructed another example of this issue.

// PARAM: --enable ana.int.congruence --enable ana.int.interval --set sem.int.signed_overflow assume_none
#include <goblint.h>

int main()
{
	int x,y;

	if( y > 0) {
	if(x % 3 == 0){
		if(x + y == 5) {
                       // We have  x:  2+3ℤ
                       // But do not make use of it
                        
			if(y % 3 == 2) {
                                 // Neither by showing this to be the case in the __goblint_check
				__goblint_check(y % 3 == 2);
			} else {
				// Nor by finding this to be unreachable
			}

		}
	}
	}
}