Unexpected timeout on simple example program

[blizzard4591]

Dear developers,

I tested a small example program with Symbiotic. My command line was ./bin/symbiotic --sv-comp --prp=reach.prp example.c with version

$ ./bin/symbiotic --version
version: 7.0.0-dev
LLVM version: 8.0.1
symbiotic            -> 0b4b6e2584d014ebb6b57da8806dd8c78cfd8c69 (Release)
dg                   -> a2ba230b3898278c42bcca1a38af8413e75391a3 (Release)
sbt-slicer           -> fff6245c8c32ea42fe9827468e2ba0c997abf61d (Release)
sbt-instrumentation  -> 2db331fb32fa767cd48170b3c030c37e17cc65ea (Release)
klee                 -> 657644fdea473f309094d818dd0b32a7ec0b5b85 (Release)

The program in question is:

extern void __VERIFIER_error();

int a;
int main() {
  while (1)
    if (a)
      __VERIFIER_error();
}

This ran for over 12 hours and timed out. Is this expected behavior due to symbolic execution?

[mchalupa]

Hi,

yes, it is the expected behavior. The program contains only one path which is error-free and infinite, therefore, symbolic execution will just keep executing this infinite path forever.

[kdudka]

It looks like a finite-state program to me. Am I missing anything?

[blizzard4591]

The program contains only one path which is error-free and infinite, therefore, symbolic execution will just keep executing this infinite path forever.

Ah, this would explain the situation. Our use-case (from which this program is sliced/reduced) contains an outer infinite loop (processing of inputs from the environment and providing corresponding outputs) and this loop is build from finite-state logic. Since we can never be sure whether Symbiotic is just stuck or can not find any errors, it seems unsuitable for our application.

[mchalupa]

It looks like a finite-state program to me. Am I missing anything?

@kdudka : It is a finite state program, but symbolic execution does not remember states. It builds the tree of possible executions of the program and if the tree has infinitely many branches or a branch is infinite (as in this case), symbolic execution is also infinite. That is an unfortunate property of symbolic execution.

[mchalupa]

Since we can never be sure whether Symbiotic is just stuck or can not find any errors, it seems unsuitable for our application.

@blizzard4591 Well, you can try other verification backends that Symbiotic supports, e.g. CPAchecker, SeaHorn, or DIVINE. Or you can unroll the loop if you're OK with bounded verification.