Merge pull request #1161 from goblint/issue_1156

Congruences: Make `%` sound by restricting cases where we return a constant

src/cdomains/intDomain.ml

@@ -3199,8 +3199,8 @@ struct
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | Some (c1, m1), Some(c2, m2) ->
       if m2 =: Ints_t.zero then
-        if (c2 |: m1) then
-          Some(c1 %: c2,Ints_t.zero)
+        if (c2 |: m1) && (c1 %: c2 =: Ints_t.zero || m1 =: Ints_t.zero || not (Cil.isSigned ik)) then
+          Some(c1 %: c2, Ints_t.zero)
         else
           normalize ik (Some(c1, (Ints_t.gcd m1 c2)))
       else

tests/regression/37-congruence/06-refinements.c

@@ -5,14 +5,15 @@ int main() {
     int top;
     int i = 0;
     if(top % 17 == 3) {
-        __goblint_check(top%17 ==3);
+        __goblint_check(top%17 ==3); //TODO (Refine top to be positive above, and reuse information in %)
         if(top %17 != 3) {
             i = 12;
         } else {
 
         }
     }
-    __goblint_check(i ==0);
+    __goblint_check(i ==0); // TODO
+    i = 0;
 
     if(top % 17 == 0) {
         __goblint_check(top%17 == 0);

tests/regression/37-congruence/07-refinements-o.c

@@ -32,15 +32,16 @@ int main() {
     int top;
     int i = 0;
     if(top % 17 == 3) {
-        __goblint_check(top%17 ==3);
+        __goblint_check(top%17 ==3); //TODO (Refine top to be positive above, and reuse information in %)
         if(top %17 != 3) {
             i = 12;
         } else {
 
         }
     }
-    __goblint_check(i ==0);
+    __goblint_check(i ==0); //TODO
 
+    i = 0;
     if(top % 17 == 0) {
         __goblint_check(top%17 == 0);
         if(top %17 != 0) {

tests/regression/37-congruence/11-overflow-signed.c

@@ -12,8 +12,8 @@ int basic(){
 	{
 		if (b % two_pow_16 == 5)
 		{
-			__goblint_check(a % two_pow_16 == 3);
-			__goblint_check(b % two_pow_16 == 5);
+			__goblint_check(a % two_pow_16 == 3); //TODO (Refine a to be positive above, and reuse information in %)
+			__goblint_check(b % two_pow_16 == 5); //TODO (Refine a to be positive above, and reuse information in %)
 
 			unsigned int e = a * b;
 			__goblint_check(e % two_pow_16 == 15); // UNKNOWN!
@@ -35,7 +35,7 @@ int special(){
 
 	if (a % two_pow_18 == two_pow_17)
 	{
-		__goblint_check(a % two_pow_18 == two_pow_17);
+		__goblint_check(a % two_pow_18 == two_pow_17); //TODO (Refine a to be positive above, and reuse information in %)
 
 		unsigned int e = a * a;
 		__goblint_check(e == 0); //UNKNOWN!

tests/regression/37-congruence/13-bitand.c

@@ -5,11 +5,16 @@ int main()
 {
 	// Assuming modulo expression
 
-	long x;
+	unsigned long x;
 	__goblint_assume(x % 2 == 1);
 	__goblint_check(x % 2 == 1);
 	__goblint_check(x & 1);
 
+	long xx;
+	__goblint_assume(xx % 2 == 1);
+	__goblint_check(xx % 2 == 1); //TODO (Refine xx to be positive above, and reuse information in %)
+	__goblint_check(xx & 1);
+
 	long y;
 	__goblint_assume(y % 2 == 0);
 	__goblint_check(y % 2 == 0);
@@ -27,14 +32,15 @@ int main()
 	__goblint_check(xz & 1);
 
 	// Assuming bitwise expression
+	// Does NOT actually lead to modulo information, as negative values may also have their last bit set!
 
 	long a;
 	__goblint_assume(a & 1);
-	__goblint_check(a % 2 == 1);
+	__goblint_check(a % 2 == 1); //UNKNOWN!
 	__goblint_check(a & 1);
 
 	int b;
 	__goblint_assume(b & 1);
-	__goblint_check(b % 2 == 1);
+	__goblint_check(b % 2 == 1); //UNKNOWN!
 	__goblint_check(b & 1);
 }

tests/regression/37-congruence/14-negative.c

@@ -0,0 +1,15 @@
+// PARAM: --enable ana.int.congruence --set sem.int.signed_overflow assume_none
+#include <goblint.h>
+
+int main()
+{
+	int top;
+
+	int c = -5;
+	if (top)
+	{
+		c = -7;
+	}
+	__goblint_check(c % 2 == 1); //UNKNOWN! (Does not hold at runtime)
+	__goblint_check(c % 2 == -1); //TODO (Track information that c is negative)
+}