[klee-dev] Klee replay-path ignore branches from uclibc
Mohammad Wamiq Saifi
wamiqsaifi at gmail.com
Sun Jul 12 07:51:46 BST 2015
Hi,
I wanted to do a replay path using klee on a program handling symbolic
files. I am using uclibc library with posix runtime enabled. I have a
replay-path according to the control flow graph of the program. But, when I
do a replay path, klee consumes the path with branches inside the uclibc
library. I there a way to prevent this to happen and allow klee to only
consume replay-path with branches inside the program?
Here is a klee's instruction execution trace for replay-path=[0,1]. One
more point to notice that the replay-path provided to klee has just two
branches but klee actually fails on the fourth branch.
KLEE: NOTE: Using klee-uclibc :
/home/wamiq/klee-unsat-core/build/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model:
/home/wamiq/klee-unsat-core/build/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/wamiq/tests/totinfo/klee-out-13"
[no debug info]: 0 call void @__uClibc_main(i32 (i32, i8**,
i8**)* bitcast (i32 (i32, i8**)* @__user_main to i32 (i32, i8**, i8**)*),
i32 %0, i8** %1, void ()* null, void ()* null, void ()* null, i8* null)
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
1 %main.addr = alloca i32 (i32, i8**, i8**)*, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
2 %argc.addr = alloca i32, align 4
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
3 %argv.addr = alloca i8**, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
4 %app_init.addr = alloca void ()*, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
5 %app_fini.addr = alloca void ()*, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
6 %rtld_fini.addr = alloca void ()*, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
7 %stack_end.addr = alloca i8*, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
8 %aux_dat = alloca i64*, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
9 %auxvt = alloca [15 x %struct.Elf64_auxv_t], align 16
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
10 %auxv_entry = alloca %struct.Elf64_auxv_t*, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
11 store i32 (i32, i8**, i8**)* %main, i32 (i32, i8**, i8**)**
%main.addr, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
12 store i32 %argc, i32* %argc.addr, align 4
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
13 store i8** %argv, i8*** %argv.addr, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
14 store void ()* %app_init, void ()** %app_init.addr, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
15 store void ()* %app_fini, void ()** %app_fini.addr, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
16 store void ()* %rtld_fini, void ()** %rtld_fini.addr, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
17 store i8* %stack_end, i8** %stack_end.addr, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
18 %0 = load i8** %stack_end.addr, align 8, !dbg !3139
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:288:
19 store i8* %0, i8** @__libc_stack_end, align 8, !dbg !3139
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:291:
20 %1 = load void ()** %rtld_fini.addr, align 8, !dbg !3141
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:291:
21 store void ()* %1, void ()** @__rtld_fini, align 8, !dbg !3141
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:294:
22 %2 = load i32* %argc.addr, align 4, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:294:
23 %add = add nsw i32 %2, 1, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:294:
24 %idxprom = sext i32 %add to i64, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:294:
25 %3 = load i8*** %argv.addr, align 8, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:294:
26 %arrayidx = getelementptr inbounds i8** %3, i64 %idxprom,
!dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:294:
27 store i8** %arrayidx, i8*** @__environ, align 8, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:298:
28 %4 = load i8*** @__environ, align 8, !dbg !3143
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:298:
29 %5 = bitcast i8** %4 to i8*, !dbg !3143
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:298:
30 %6 = load i8*** %argv.addr, align 8, !dbg !3143
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:298:
31 %7 = load i8** %6, align 8, !dbg !3143
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:298:
32 %cmp = icmp eq i8* %5, %7, !dbg !3143
*
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:298:
33 br i1 %cmp, label %if.then, label %if.end, !dbg !3143*
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:305:
34 %arraydecay = getelementptr inbounds [15 x
%struct.Elf64_auxv_t]* %auxvt, i32 0, i32 0, !dbg !3147
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:305:
35 %10 = bitcast %struct.Elf64_auxv_t* %arraydecay to i8*, !dbg
!3147
/home/wamiq/klee-3.4/klee-uclibc/libc/misc/internals/__uClibc_main.c:305:
36 %call = call i8* @memset(i8* %10, i32 0, i64 240) nounwind,
!dbg !3147
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:19: 37
%s.addr = alloca i8*, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:19: 38
%c.addr = alloca i32, align 4
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:19: 39
%n.addr = alloca i64, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:19: 40
%p = alloca i8*, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:19: 41
store i8* %s, i8** %s.addr, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:19: 42
store i32 %c, i32* %c.addr, align 4
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:19: 43
store i64 %n, i64* %n.addr, align 8
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:19: 44
%0 = load i8** %s.addr, align 8, !dbg !3139
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:19: 45
store i8* %0, i8** %p, align 8, !dbg !3139
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:27: 46
br label %while.cond, !dbg !3141
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:27: 47
%1 = load i64* %n.addr, align 8, !dbg !3141
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:27: 48
%tobool = icmp ne i64 %1, 0, !dbg !3141
* /home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:27: 49
br i1 %tobool, label %while.body, label %while.end, !dbg !3141*
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:28: 50
%2 = load i32* %c.addr, align 4, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:28: 51
%conv = trunc i32 %2 to i8, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:28: 52
%3 = load i8** %p, align 8, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:28: 53
%incdec.ptr = getelementptr inbounds i8* %3, i32 1, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:28: 54
store i8* %incdec.ptr, i8** %p, align 8, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:28: 55
store i8 %conv, i8* %3, align 1, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:29: 56
%4 = load i64* %n.addr, align 8, !dbg !3144
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:29: 57
%dec = add i64 %4, -1, !dbg !3144
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:29: 58
store i64 %dec, i64* %n.addr, align 8, !dbg !3144
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:30: 59
br label %while.cond, !dbg !3145
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:27: 60
%1 = load i64* %n.addr, align 8, !dbg !3141
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:27: 61
%tobool = icmp ne i64 %1, 0, !dbg !3141
* /home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:27: 62
br i1 %tobool, label %while.body, label %while.end, !dbg !3141*
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:28: 63
%2 = load i32* %c.addr, align 4, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:28: 64
%conv = trunc i32 %2 to i8, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:28: 65
%3 = load i8** %p, align 8, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:28: 66
%incdec.ptr = getelementptr inbounds i8* %3, i32 1, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:28: 67
store i8* %incdec.ptr, i8** %p, align 8, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:28: 68
store i8 %conv, i8* %3, align 1, !dbg !3142
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:29: 69
%4 = load i64* %n.addr, align 8, !dbg !3144
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:29: 70
%dec = add i64 %4, -1, !dbg !3144
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:29: 71
store i64 %dec, i64* %n.addr, align 8, !dbg !3144
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:30: 72
br label %while.cond, !dbg !3145
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:27: 73
%1 = load i64* %n.addr, align 8, !dbg !3141
/home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:27: 74
%tobool = icmp ne i64 %1, 0, !dbg !3141
* /home/wamiq/klee-3.4/klee-uclibc/libc/string/memset.c:27: 75
br i1 %tobool, label %while.body, label %while.end, !dbg !3141*
klee: /home/wamiq/klee-unsat-core/lib/Core/Executor.cpp:757:
klee::Executor::StatePair klee::Executor::fork(klee::ExecutionState&,
klee::ref<klee::Expr>, bool): Assertion `replayPosition<replayPath->size()
&& "ran out of branches in replay path mode"' failed.
0 libLLVM-3.2svn.so 0x00007fe66d82a85f
1 libLLVM-3.2svn.so 0x00007fe66d82ad99
2 libpthread.so.0 0x00007fe66c7b7cb0
3 libc.so.6 0x00007fe66bb900d5 gsignal + 53
4 libc.so.6 0x00007fe66bb9383b abort + 379
5 libc.so.6 0x00007fe66bb88d9e
6 libc.so.6 0x00007fe66bb88e42
7 klee 0x00000000004a25c7
klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
7815
8 klee 0x00000000004a6c96
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 7382
9 klee 0x00000000004a9f96
klee::Executor::run(klee::ExecutionState&) + 1654
10 klee 0x00000000004aa841
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1681
11 klee 0x00000000004887d3 main + 10227
12 libc.so.6 0x00007fe66bb7b76d __libc_start_main + 237
13 klee 0x00000000004919c9
Regards,
Wamiq
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list