SVF-tools / Test-Suite

PTABen: Micro-benchmark Suite for Pointer Analysis
70 stars 38 forks source link

Non-terminating recursive call before assertions in `cs_tests/recur10.c` #29

Open taquangtrung opened 3 years ago

taquangtrung commented 3 years ago

Hi,

For this test case, the first recursive call to f() inside the body of f will be non-terminating.

So, I wonder if it is OK to check alias information after this call? Such assertions will never be reached anyway.

// cs_tests/recur10.c

#include "aliascheck.h"
int **p,*x, y, z;

void f() {
  p = &x;
  if (1) {
    *p = &y;
    MUSTALIAS(x,&y);
    f();
    *p = &z;
    /// p doesn't point to x at the above line: although p's
    /// value changed by stmt "p=&x", the value flow can not
    /// reach "*p=&z" since it will flow into f() before
    /// "*p=&z" and connected with the entry of f(). So the
    /// store "*p=&z" can not be completed as p's pts is empty.
    NOALIAS(x,&z);
    NOALIAS(x,&y);
    f();
  }
}

int main()
{
    f();
    return 0;
}
yuleisui commented 3 years ago

Yes, correct. I guess the reason might because the test case writer was not considering path sensitivity (branch conditions). I am changing the if condition to make it terminable.

taquangtrung commented 3 years ago

Thank you for the update!

taquangtrung commented 3 years ago

Hi,

Do you have any updates for this test case?

Is it possible to change the condition if (1) to something like if (z)? I saw that if (z) is also used by the other test case recur4.c

yuleisui commented 3 years ago

Added the base case: 60848d6ad3110fe793674e03b9604d6cba700164

taquangtrung commented 3 years ago

Thank you for the quick update! I also notice the same issue in recur0.c

void f() {
  if (1) {
    x = &y;
    MUSTALIAS(x, &y)
    f();
    x = &z;
    MUSTALIAS(x, &z)
    NOALIAS(x, &y)
    f();
  }
}
yuleisui commented 3 years ago

Done. dca7f8d2f5b73271e5d18c51ffebaf0bad71ff3f