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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
