Termination: Unsound result with backend IMC?

[pwnchaser]

Hi, thanks for fixing my previous bug,
I may have another one, this time with --backend IMC:

void f(int x){  // x == -1
  while (x < 0){
  }
}

int main() {
  unsigned int allOne = 0xffffffff;
  f(allOne);
  long castToLong = allOne;
  return 0;
}

Theta says this is a terminating-program, but in fact when the unsigned integer is casted to signed, this is a negative number and the loop does not terminate.
It seems that there is an interplay with the unused variable castToLong as dropping this variable makes Theta return SafetyResult Unsafe as expected.

[leventeBajczi]

Thanks! This was a quick fix: we lost track of the original variable type when we used a too aggressive simplification of the variables.

[leventeBajczi]

Btw, if you find it easier, you can use our fairly new web interface to test Theta -- it still has some teething issues, but it works more or less.

For example, the input you submitted this time, with XCFA serialization enabled (check the svg file under the generated files) uncovers that with the castToLong, we suddenly don't know we should be casting to -1 when calling the function.

https://theta.mit.bme.hu/?mode=C&config=eyJjb2RlIjoidm9pZCBmKGludCB4KXsgIC8vIHggPT0gLTFcbiAgd2hpbGUgKHggPCAwKXtcbiAgfVxufVxuXG5pbnQgbWFpbigpIHtcbiAgdW5zaWduZWQgaW50IGFsbE9uZSA9IDB4ZmZmZmZmZmY7XG4gIGYoYWxsT25lKTtcbiAgbG9uZyBjYXN0VG9Mb25nID0gYWxsT25lO1xuICByZXR1cm4gMDtcbn0iLCJzZWxlY3RlZFByb3BlcnR5IjoidGVybWluYXRpb24ucHJwIiwic2VsZWN0ZWRFeGFtcGxlIjoiIiwic2VsZWN0ZWRSZWxlYXNlIjoidjYuMjcuMTQiLCJzZWxlY3RlZFByZXNldCI6IiIsImFyZ3MiOiItLWlucHV0ICVpbiAtLXByb3BlcnR5ICVwcm9wIC0tYmFja2VuZCBJTUMgLS1lbmFibGUteGNmYS1zZXJpYWxpemF0aW9uIn0%3D

[leventeBajczi]

And please keep the issues coming if you find more problems, we really appreciate it!