Hi Li,
klee_assume can be confusing, because it works based on the result of
the expression. In cases when the expression branched, this usually
isn't what was intended. klee_assume is roughly equivalent to:
--
void klee_assume(int constraint) {
if (!constraint) klee_silent_exit(0);
}
--
except that it doesn't actually cause a fork, and it complains if the
condition is provably false. In cases where the execution forked,
usually some of states will end up getting false as the constraint
argument, which triggers the error.
On Fri, Jun 11, 2010 at 8:59 PM, Li Xuan Ji <xuanji at gmail.com> wrote:
> 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?
By default, KLEE only generates at most one error per instruction. You
can use --emit-all-errors to disable this.
- Daniel
>
> Thanks!
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
>
