Remove tasks with overflows from termination (!1543) · Merge requests · SoSy-Lab / Benchmarking / SV-Benchmarks

Marek Jankola requested to merge remove-tasks-with-overflows-from-termination into main Apr 17, 2024

We found 17 tasks with possible signed integer overflows in the termination category. Since signed integer overflows are undefined behaviour, there is no concrete interepretation of the result values after the overflow. Based on the interpretation of the values after the overflow, all of the following programs can be terminating/non-terminating. Only one of these programs was confirmed by Taipan, UAutomizer and CPAchecker, for the other tasks these tools timed out. We went through all the programs by hand and we show that they indeed contain overflows.

An obvious fix would be to change the signed integers to unsigned integers, however this fix would change the expected result in some of the programs and it would need to be further analyzed. For now, we propose to remove them from the competition.

### Mysore-3.c

int main()
{
	int x;
	int c;
    x = __VERIFIER_nondet_int();
    c = __VERIFIER_nondet_int();
  //prevent overflows
    if(!(-65535<=x && x<=65535)) return 0;
    if(!(-65535<=c && c<=65535)) return 0;
	if (c < 0) {
    	while (x + c >= 0) {
	    	x = x - c;
		    c = c - 1;
	    }
	}
	return 0;
}

It is sufficient to set `x=65535` and `c=-65535`. Value of `x+c` will be greater than `0` in every iteration, since `c` decreases just by one, whereas `x` grows by value of `-c`. Therefore, `x` eventually overflows.

### and-01-false.c

int main (){
  int a, x;
  x = __VERIFIER_nondet_int();
  a = 34;
  while (x==0){
    a--;
    x=x&a;
  }
  return 0;
}

It is sufficient to set `x=0`. `x = (x&a)` and `(x&a) = 0` then holds in every iteration and `a` eventually underflows.

### and-02-false.c

int main (){
    int a;
    int x;
    x = __VERIFIER_nondet_int();
    a = 16;
    while (x!=0){
        a--;
        if (x > 0){
           x = x&a;
        }
        else {
            x++;
        }
    }
    return 0;
}

This task is claimed to be nonterminating in the sv-benchmarks. Therefore, there exists an assignment for `x` so that the loop does not terminate. However, that means that `a` eventually underflows.

### gcnr2008.i

int main() {
    int x,y,z,w;
    x = y = z = w = 0;
    while (__VERIFIER_nondet_int() && y < 10000) {
 if (__VERIFIER_nondet_int()) {
     x = x + 1;
     y = y + 100;
 } else if (__VERIFIER_nondet_int()) {
     if (x >= 4) {
  x = x + 1;
  y = y + 1;
     }
 } else if (y > 10*w && z >= 100*x) {
     y = -y;
 }
 w = w + 1;
 z = z + 10;
    }
    __VERIFIER_assert(x >= 4 && y <= 2);
    return 0;
}

In each iteration of the while loop we can decide to stay in the loop. Moreover, the nondet values can force us not to satisfy any of the conditions (the last one ist also not satisfied because `y<=10*w`, since we will keep `y=0` and `w` increases in every iteration). After such decisions, the whole loop can be summarized just to `w = w + 1` and `z = z + 10`. Both of the variables eventually overflow.

### mannadiv-both-nt.c

int main() {
    int x1, x2;
    int y1, y2, y3;
    x1 = __VERIFIER_nondet_int();
    x2 = __VERIFIER_nondet_int();

    // assume_abort_if_not(x1 >= 0);
    // assume_abort_if_not(x2 != 0);

    if (x1 < 0 || x2 == 0) {
        return 0;
    }

    y1 = 0;
    y2 = 0;
    y3 = x1;

    while (1) {
        // __VERIFIER_assert(y1*x2 + y2 + y3 == x1);

        if (!(y1*x2 + y2 + y3 == x1)) break;

        if (y2 + 1 == x2) {
            y1 = y1 + 1;
            y2 = 0;
            y3 = y3 - 1;
        } else {
            y2 = y2 + 1;
            y3 = y3 - 1;
        }
    }
    // __VERIFIER_assert(y1*x2 + y2 == x1);
    return 0;
}

We can set `x1 = 0` and `x2 = 1`. The break condition inside the loop will not be satisfied because `0 == 0`. After that, the else branch is always taken in the second condition. Eventually, `y2` and `y3` overflow.

### or-01-false.c

int main (){
  int a, b;
  int x;
  a = 16;
  b = 30;
  x = __VERIFIER_nondet_int();

  while (x>=0){
    b = b|a;
    x= x+b;
  }
  return 0;
}

This task was proven by UAutomizer, Taipan and CPAchecker to contain overflow.

### cohencu1-both-nt.c

int main() {
    int a, n, x, y, z;
    a = __VERIFIER_nondet_int();
    n = 0;
    x = 0;
    y = 1;
    z = 6;

    while (z <= 6 * n + 6) {
      //__VERIFIER_assert(z == 6 * n + 6);
      //__VERIFIER_assert(y == 3 * n * n + 3 * n + 1);
      //__VERIFIER_assert(x == n * n * n);
      //__VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
      //__VERIFIER_assert((z*z) - 12*y - 6*z + 12 == 0);
        //if (!(n <= a))            break;

        n = n + 1;
        x = x + y;
        y = y + z;
        z = z + 6;
    }
    /*
    __VERIFIER_assert(z == 6*n + 6);
    __VERIFIER_assert(6*a*x - x*z + 12*x == 0);
    __VERIFIER_assert(a*z - 6*a - 2*y + 2*z - 10 == 0);
    __VERIFIER_assert(2*y*y - 3*x*z - 18*x - 10*y + 3*z - 10 == 0);
    __VERIFIER_assert(z*z - 12*y - 6*z + 12 == 0);
    __VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
    */    
    return 0;
}

This program is deterministic (value of `a` does not matter) and it is claimed to be non-terminating. Since for example value of `n` is strictly increasing, then it necesserally overflows.

### cohencu2-both-nt.c

int main() {
    int a, n, x, y, z;
    a = __VERIFIER_nondet_int();
    n = 0;
    x = 0;
    y = 1;
    z = 6;
    
    while (y == 3 * n * n + 3 * n + 1) {
      //__VERIFIER_assert(z == 6 * n + 6);
      //__VERIFIER_assert(y == 3 * n * n + 3 * n + 1);
      //__VERIFIER_assert(x == n * n * n);
      //__VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
      //__VERIFIER_assert((z*z) - 12*y - 6*z + 12 == 0);
        //if (!(n <= a))            break;

        n = n + 1;
        x = x + y;
        y = y + z;
        z = z + 6;
    }
    /*
    __VERIFIER_assert(z == 6*n + 6);
    __VERIFIER_assert(6*a*x - x*z + 12*x == 0);
    __VERIFIER_assert(a*z - 6*a - 2*y + 2*z - 10 == 0);
    __VERIFIER_assert(2*y*y - 3*x*z - 18*x - 10*y + 3*z - 10 == 0);
    __VERIFIER_assert(z*z - 12*y - 6*z + 12 == 0);
    __VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
    */    
    return 0;
}

Same as previous case.

### cohencu3-both-nt.c

int main() {
    int a, n, x, y, z;
    a = __VERIFIER_nondet_int();
    n = 0;
    x = 0;
    y = 1;
    z = 6;
    
    while (x == n * n * n) {
      //__VERIFIER_assert(z == 6 * n + 6);
      //__VERIFIER_assert(y == 3 * n * n + 3 * n + 1);
      //__VERIFIER_assert(x == n * n * n);
      //__VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
      //__VERIFIER_assert((z*z) - 12*y - 6*z + 12 == 0);
        //if (!(n <= a))            break;

        n = n + 1;
        x = x + y;
        y = y + z;
        z = z + 6;
    }
    /*
    __VERIFIER_assert(z == 6*n + 6);
    __VERIFIER_assert(6*a*x - x*z + 12*x == 0);
    __VERIFIER_assert(a*z - 6*a - 2*y + 2*z - 10 == 0);
    __VERIFIER_assert(2*y*y - 3*x*z - 18*x - 10*y + 3*z - 10 == 0);
    __VERIFIER_assert(z*z - 12*y - 6*z + 12 == 0);
    __VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
    */    
    return 0;
}

Same as previous case.

### cohencu4-both-nt.c

int main() {
    int a, n, x, y, z;
    a = __VERIFIER_nondet_int();
    n = 0;
    x = 0;
    y = 1;
    z = 6;

    while (y*z - 18*x - 12*y + 2*z - 6 == 0) {
      //__VERIFIER_assert(z == 6 * n + 6);
      //__VERIFIER_assert(y == 3 * n * n + 3 * n + 1);
      //__VERIFIER_assert(x == n * n * n);
      //__VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
      //__VERIFIER_assert((z*z) - 12*y - 6*z + 12 == 0);
        //if (!(n <= a))            break;

        n = n + 1;
        x = x + y;
        y = y + z;
        z = z + 6;
    }
    /*
    __VERIFIER_assert(z == 6*n + 6);
    __VERIFIER_assert(6*a*x - x*z + 12*x == 0);
    __VERIFIER_assert(a*z - 6*a - 2*y + 2*z - 10 == 0);
    __VERIFIER_assert(2*y*y - 3*x*z - 18*x - 10*y + 3*z - 10 == 0);
    __VERIFIER_assert(z*z - 12*y - 6*z + 12 == 0);
    __VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
    */    
    return 0;
}

Same as previous case.

### cohencu5-both-nt.c

int main() {
    int a, n, x, y, z;
    a = __VERIFIER_nondet_int();
    n = 0;
    x = 0;
    y = 1;
    z = 6;
    
    while ((z*z) - 12*y - 6*z + 12 == 0) {
      //__VERIFIER_assert(z == 6 * n + 6);
      //__VERIFIER_assert(y == 3 * n * n + 3 * n + 1);
      //__VERIFIER_assert(x == n * n * n);
      //__VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
      //__VERIFIER_assert((z*z) - 12*y - 6*z + 12 == 0);
        //if (!(n <= a))            break;

        n = n + 1;
        x = x + y;
        y = y + z;
        z = z + 6;
    }
    /*
    __VERIFIER_assert(z == 6*n + 6);
    __VERIFIER_assert(6*a*x - x*z + 12*x == 0);
    __VERIFIER_assert(a*z - 6*a - 2*y + 2*z - 10 == 0);
    __VERIFIER_assert(2*y*y - 3*x*z - 18*x - 10*y + 3*z - 10 == 0);
    __VERIFIER_assert(z*z - 12*y - 6*z + 12 == 0);
    __VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
    */    
    return 0;
}

Same as previous case.

### ps2-both-nt.c

int main() {
    int k, y, x, c;
    k = __VERIFIER_nondet_int();

    y = 0;
    x = 0;
    c = 0;

    while (1) {
        // __VERIFIER_assert((y * y) - 2 * x + y == 0);

        if (!((y * y) - 2 * x + y == 0))
            break;

        c = c + 1;
        y = y + 1;
        x = y + x;
    }
    // __VERIFIER_assert((y*y) - 2*x + y == 0);
     
    return 0;
}

Same as cohencu tasks.

### ps3-both-nt.c

int main() {
    int k, y, x, c;
    k = __VERIFIER_nondet_int();

    y = 0;
    x = 0;
    c = 0;

    while (1) {
        // __VERIFIER_assert(6*x - 2*y*y*y - 3*y*y - y == 0);

        if (!(6*x - 2*y*y*y - 3*y*y - y == 0))
            break;

        c = c + 1;
        y = y + 1;
        x = y * y + x;
    }
    // __VERIFIER_assert(6*x - 2*y*y*y - 3*y*y - y == 0);
    return 0;
}

Same as cohencu tasks.

### ps4-both-nt.c

int main() {
    int k, y, x, c;
    k = __VERIFIER_nondet_int();

    y = 0;
    x = 0;
    c = 0;

    while (1) {
        // __VERIFIER_assert(4*x - y*y*y*y - 2*y*y*y - y*y == 0);

        if (!(4*x - y*y*y*y - 2*y*y*y - y*y == 0))
            break;

        c = c + 1;
        y = y + 1;
        x = y * y * y + x;
    }
    // __VERIFIER_assert(k*y - (y*y) == 0);
    // __VERIFIER_assert(4*x - y*y*y*y - 2*y*y*y - y*y == 0);
    return 0;
}

Same as cohencu tasks.

### ps5-both-nt.c

int main() {
    int k, y, x, c;
    k = __VERIFIER_nondet_int();

    y = 0;
    x = 0;
    c = 0;

    while (1) {
        // __VERIFIER_assert(6*y*y*y*y*y + 15*y*y*y*y + 10*y*y*y - 30*x - y == 0);

        if (!(6*y*y*y*y*y + 15*y*y*y*y + 10*y*y*y - 30*x - y == 0))
            break;

        c = c + 1;
        y = y + 1;
        x = y * y * y * y + x;
    }

    // __VERIFIER_assert(6*y*y*y*y*y + 15*y*y*y*y + 10*y*y*y - 30*x - y == 0);
    // __VERIFIER_assert(k*y == y*y);
    return 0;
}

Same as cohencu tasks.

### ps6-both-nt.c

int main() {
    int k, y, x, c;
    k = __VERIFIER_nondet_int();

    y = 0;
    x = 0;
    c = 0;

    while (1) {
        // __VERIFIER_assert(-2*y*y*y*y*y*y - 6 * y*y*y*y*y - 5 * y*y*y*y + y*y + 12*x == 0);

        if (!(-2*y*y*y*y*y*y - 6 * y*y*y*y*y - 5 * y*y*y*y + y*y + 12*x == 0))
            break;

        c = c + 1;
        y = y + 1;
        x = y * y * y * y * y + x;
    }
    
    // __VERIFIER_assert(-2*y*y*y*y*y*y - 6 * y*y*y*y*y - 5 * y*y*y*y + y*y + 12*x == 0);
    // __VERIFIER_assert(k*y == y*y);      
    return 0;
}

Same as cohencu tasks.

### sqrt1-both-nt.c

int main() {
    int n, a, s, t;
    n = __VERIFIER_nondet_int();

    a = 0;
    s = 1;
    t = 1;

    while (t*t - 4*s + 2*t + 1 == 0) {
      //__VERIFIER_assert(t == 2*a + 1);
      //__VERIFIER_assert(s == (a + 1) * (a + 1));
      //__VERIFIER_assert(t*t - 4*s + 2*t + 1 == 0);
        // the above 2 should be equiv to 
      //if (!(s <= n))break;
        a = a + 1;
        t = t + 2;
        s = s + t;
    }
    
    //__VERIFIER_assert(t == 2 * a + 1);
    //__VERIFIER_assert(s == (a + 1) * (a + 1));
    //__VERIFIER_assert(t*t - 4*s + 2*t + 1 == 0);

    return 0;
}

Same as cohencu tasks.

Edited Apr 17, 2024 by Marek Jankola

Admin message

Remove tasks with overflows from termination

Merge request reports