Can klee produce tests when it cannot solve complex constraints?

[陈厅]

Hi everyone


I find klee cannot produce a test for a path when the corresponding path condition is too complex to solve. Below is my program.


#include <stdio.h>
int complex(int x, int y) {
if(x == (y + 100) * (y + 100) * (y + 100) * (y + 100) * (y + 100) * (y + 100) * (y + 100) * (y + 100) * (y + 100) * (y + 100) * (y + 100) * (y + 100) * (y + 100) * (y + 100))
// the right side of '==' is an expression that stp cannot solve in reasonable cost
return 1;
return 2;
}
int main() {
int a, b;
klee_make_symbolic(&a, sizeof(a), "a");
klee_make_symbolic(&b, sizeof(b), "b");
printf("%d\n", complex(a, b));
return 0;
}


I compile this program by the command: llvm-gcc -g -c -emit-llvm complex.c
I run this program by the command: klee -use-forked-stp -max-stp-time=10 -write-paths --use-query-log=solver:smt2 complex.o
You can see that I limit the solving time to 10 seconds to avoid too high memory cost and long delay.
The result is:
KLEE: output directory = "klee-out-8"
KLEE: Logging queries that reach solver in .smt2 format to /home/ting/work/klee/examples/non_linear/./klee-out-8/solver-queries.smt2
KLEE: WARNING: undefined reference to function: printf
error: STP timed out
KLEE: done: total instructions = 70
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1


You can see that klee produce one test which covers the 'else' branch of function complex. The 'then' branch is not explored because of stp time out.
I think there is a solution to this kind of problem. One can solve the path condition before the complex expression. In this example, the path condition is 'true'. So we can get a solution of y, for example, y = 0. We do not get the concrete value of x because the following complex expression does not involve x. So now the path condition is solvable because we fix y to a concrete value, thus we can produce a test for the 'then' branch.
Does klee provide any similar or better mechanism to handle the above problem?


Thanks in advance.


Ting Chen