Hi, I have a question about how klee_assume interacts with functions, in
this case the strlen function.
~/klee-test/assume_strlen:85$ cat asl.c
#include <string.h>
#include <klee/klee.h>
int main(int argc, char *argv[])
{
char resolved[8];
klee_make_symbolic(resolved, sizeof(resolved), "resolved");
klee_assume(resolved[7] == '\0');
klee_assume(strlen(resolved) == 4);
return 0;
}
~/klee-test/assume_strlen:86$ llvm-gcc --emit-llvm -c -g ./asl.c
~/klee-test/assume_strlen:87$ klee -libc=uclibc ./asl.o
KLEE: output directory = "klee-out-0"
KLEE: WARNING: undefined reference to function: __syscall_rt_sigaction
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: fstat
KLEE: WARNING: undefined reference to function: ioctl
KLEE: WARNING: undefined reference to function: open
KLEE: WARNING: undefined reference to function: write
KLEE: WARNING: undefined reference to function: kill (UNSAFE)!
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING: calling external: ioctl(0, 21505, 173457000)
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: ERROR: /home/xuanji/klee-test/assume_strlen/./asl.c:10: invalid
klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 11190
KLEE: done: completed paths = 8
KLEE: done: generated tests = 2
~/klee-test/assume_strlen:88$ cd klee-last
~/klee-test/assume_strlen/klee-last:89$ ls
assembly.ll run.istats test000001.pc warnings.txt
info run.stats test000001.user.err
messages.txt test000001.ktest test000002.ktest
~/klee-test/assume_strlen/klee-last:90$ ktest-tool test000001.ktest
ktest file : 'test000001.ktest'
args : ['./asl.o']
num objects: 1
object 0: name: 'resolved'
object 0: size: 8
object 0: data: '\x00\x00\x00\x00\x00\x00\x00\x00'
~/klee-test/assume_strlen/klee-last:91$ ktest-tool test000002.ktest
ktest file : 'test000002.ktest'
args : ['./asl.o']
num objects: 1
object 0: name: 'resolved'
object 0: size: 8
object 0: data: '\x02\x01\x01\x01\x00\x00\x00\x00'
Notice the ERROR that says the call to klee_assume is provably false. I
believe it's because when klee executes strlen() it branches execution, and
one of the branches (the one where resolved is the empty string) obviously
does not satisfy the klee_assume(strlen(resolved) == 4). So my question is,
why are 8 paths searched by only 2 test cases generated? Surely something
like resolved = "ab" takes execution of the program down a different path
and should also generate an ERROR at the klee_assume. Is there some kind of
caching?
Thanks!
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100612/cacf7db1/attachment.html
