davidtr1037 / chopper Goto Github PK
View Code? Open in Web Editor NEWKLEE / CSE Project
License: Other
chopper's People
Contributors
Stargazers
Watchers
Forkers
zdzhjx zhuyue1314 chubbymaggie gavz ufwt lukas-dresel bovinspectortool1 martinnowack davidbuterez fanyao labba everpall develacker yiyuaner jordr heruix lambda2023 loongwalker ctfpwner phan123123 sunxfancychopper's Issues
Port to LLVM 3.8
There exists experimental support for Klee on LLVM 3.8.
Softening "function unreachable" asserts
Running vanilla Chopper on the is_lower benchmark from KLEE:
/*
* First KLEE tutorial: testing a small function
*/
#include <klee/klee.h>
int my_islower(int x) {
if (x >= 'a' && x <= 'z')
return 1;
else return 0;
}
int main() {
char c;
klee_make_symbolic(&c, sizeof(c), "input");
return my_islower(c);Skipping main is the easiest way to trigger the assert:
$ kleegacy -libc=klee -search=dfs -skip-functions=main islower.bc
KLEE: output directory is "/home/ubuntu/code/chopper/examples/islower/klee-out-9"
Using STP solver backend
KLEE: Runnining pointer analysis...
KLEE: Runnining reachability analysis...
function '__wrap_main' is not found
KLEE: Runnining mod-ref analysis...
function '__wrap_main' is not found (or unreachable)
kleegacy: /home/ubuntu/code/chopper/lib/Analysis/ModRefAnalysis.cpp:61: void ModRefAnalysis::run(): Assertion `false' failed.
0 kleegacy 0x0000561c70fc2992 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1 kleegacy 0x0000561c70fc228c
2 libpthread.so.0 0x00007f3af3c52890
3 libc.so.6 0x00007f3af2b20e97 gsignal + 199
4 libc.so.6 0x00007f3af2b22801 abort + 321
5 libc.so.6 0x00007f3af2b1239a
6 libc.so.6 0x00007f3af2b12412
7 kleegacy 0x0000561c70675874 ModRefAnalysis::run() + 434
8 kleegacy 0x0000561c705d8b2c klee::KModule::prepare(klee::Interpreter::ModuleOptions const&, std::vector<klee::Interpreter::SkippedFunctionOption, std::allocator<klee::Interpreter::SkippedFunctionOption> > const&, klee::InterpreterHandler*, ReachabilityAnalysis*, Inliner*, AAPass*, ModRefAnalysis*, Cloner*, SliceGenerator*) + 3550
9 kleegacy 0x0000561c70520640 klee::Executor::setModule(llvm::Module*, klee::Interpreter::ModuleOptions const&) + 1656
10 kleegacy 0x0000561c70503b35 main + 4654
11 libc.so.6 0x00007f3af2b03b97 __libc_start_main + 231
12 kleegacy 0x0000561c704fd71a _start + 42
[1] 5458 abort (core dumped) kleegacy -libc=klee -search=dfs -skip-functions=main islower.bcIt does not seem to me like it is a critical error, and so I wrote this patch in order to recover and continue with the analysis:
diff --git a/lib/Analysis/ModRefAnalysis.cpp b/lib/Analysis/ModRefAnalysis.cpp
index fc154c5a..b15c6ce2 100644
--- a/lib/Analysis/ModRefAnalysis.cpp
+++ b/lib/Analysis/ModRefAnalysis.cpp
@@ -54,15 +55,23 @@ void ModRefAnalysis::run() {
assert(false);
}
+ vector<vector<string>::iterator> todel;
for (vector<string>::iterator i = targets.begin(); i != targets.end(); i++) {
string name = *i;
Function *f = module->getFunction(name);
if (!f) {
errs() << "function '" << name << "' is not found (or unreachable)\n";
- assert(false);
+ todel.push_back(i);
+ continue; // JOR: TODO: ensure safety
}
targetFunctions.push_back(f);
}
+ for (vector<vector<string>::iterator>::iterator d = todel.begin(); d != todel.end(); d++) {
+ targets.erase(*d); // JOR: not sure this helps
+ }and do the same in ReachabilityAnalysis.
On larger benchmarks like bc, a lot of functions may be found unreachable when trying to skip (almost) everything:
[791b55] KLEE: Runnining mod-ref analysis...
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yywrap' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'bc_out_long' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'usage' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_delete_buffer' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'bc_str2num' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function '__sigdelset' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_switch_to_buffer' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_flush_buffer' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'new_yy_file' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'find_id' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_scan_buffer' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'get_var' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'long_val' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'copy_array' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'pn' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'assign' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'pv' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_scan_string' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'num2str' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_scan_bytes' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'bc_is_near_zero' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_load_buffer_state' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'yy_init_buffer' is not found (or unreachable)
[8b29fc] KLEE: WARNING: [ModRefAnalysis] function 'bc_raisemod' is not found (or unreachable)Q: Is this a safe way to proceed with this issue? Is it correct to assume that this assertion is not critical?
Multiple lines in a skipped function option
Add support for multiple lines in the skipped function option.
Should be something like:
-skip-functions=foo:10;12,bar:1;2;3
KLEE crashes on seq
/home/andrea/work/klee-slicing/klee-build/bin/klee -search=dfs -print-functions --posix-runtime --libc=uclibc -skip-functions=setlocale,atexit,getopt_long coreutils-6.10/obj-llvm/src/seq.bc -f %0 1
...
klee: /home/andrea/work/klee-slicing/klee/lib/Core/Executor.cpp:4232: void klee::Executor::getLoadInfo(klee::ExecutionState&, klee::KInstruction*, uint64_t&, uint64_t&, ModRefAnalysis::AllocSite&): Assertion `false' failed.
0 libSlicing.so 0x00002aaaab26b1e2 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1 libSlicing.so 0x00002aaaab26a954
2 libpthread.so.0 0x00002aaaabaae390
3 libc.so.6 0x00002aaaac590428 gsignal + 56
4 libc.so.6 0x00002aaaac59202a abort + 362
5 libc.so.6 0x00002aaaac588bd7
6 libc.so.6 0x00002aaaac588c82
7 klee 0x0000000000539983 klee::Executor::getLoadInfo(klee::ExecutionState&, klee::KInstruction*, unsigned long&, unsigned long&, std::pair<llvm::Value const*, unsigned long>&) + 499
8 klee 0x0000000000539ce4 klee::Executor::getAllRecoveryInfo(klee::ExecutionState&, klee::KInstruction*, std::__cxx11::list<klee::ref<klee::RecoveryInfo>, std::allocator<klee::ref<klee::RecoveryInfo> > >&) + 132
9 klee 0x000000000054590f klee::Executor::handleMayBlockingLoad(klee::ExecutionState&, klee::KInstruction*) + 47
10 klee 0x00000000005499b2 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 15714
11 klee 0x000000000054bc17 klee::Executor::run(klee::ExecutionState&) + 1927
12 klee 0x000000000054c47d klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1901
13 klee 0x0000000000516b06 main + 12998
14 libc.so.6 0x00002aaaac57b830 __libc_start_main + 240
15 klee 0x0000000000526f79 _start + 41
Aborted (core dumped)KLEE crashes on Coreutils 6.10 ptx
Invocation
/home/andrea/work/klee-slicing/klee-build/bin/klee --posix-runtime -libc=uclibc --search=random-state --max-time=360. --skip-functions=usage,quotearg ptx.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout
Output:
...
%2 = load i8* %1, align 1, !dbg !4400
Not able to retrieve address for LoadInst
UNREACHABLE executed at /home/andrea/work/klee-slicing/klee/lib/Core/Executor.cpp:4248!
0 libSlicing.so 0x00002aaaab266302 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1 libSlicing.so 0x00002aaaab265a74
2 libpthread.so.0 0x00002aaaabaa8390
3 libc.so.6 0x00002aaaac58a428 gsignal + 56
4 libc.so.6 0x00002aaaac58c02a abort + 362
5 libSlicing.so 0x00002aaaab236fb0 LLVMInstallFatalErrorHandler + 0
6 klee 0x00000000005398ad klee::Executor::getLoadInfo(klee::ExecutionState&, klee::KInstruction*, unsigned long&, unsigned long&, std::pair<llvm::Value const*, unsigned long>&) + 1101
7 klee 0x00000000005399a4 klee::Executor::getAllRecoveryInfo(klee::ExecutionState&, klee::KInstruction*, std::__cxx11::list<klee::ref<klee::RecoveryInfo>, std::allocator<klee::ref<klee::RecoveryInfo> > >&) + 132
8 klee 0x00000000005452ff klee::Executor::handleMayBlockingLoad(klee::ExecutionState&, klee::KInstruction*) + 47
9 klee 0x0000000000549344 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 15716
10 klee 0x000000000054b5a7 klee::Executor::run(klee::ExecutionState&) + 1927
11 klee 0x000000000054be0d klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1901
12 klee 0x0000000000516b96 main + 12998
13 libc.so.6 0x00002aaaac575830 __libc_start_main + 240
14 klee 0x0000000000526fc9 _start + 41
Aborted (core dumped)CVE 2014 now crashes
/data/klee-slicing/klee-build/bin/klee --libc=uclibc --search=dfs
--skip-functions=_asn1_get_octet_string:1092,asn1_delete_structure:1374
--no-output test.bc 32
[..]
klee: /data/klee-slicing/klee/lib/Core/Executor.cpp:4526: void klee::Executor::onRecoveryStateWrite(klee::ExecutionState&, klee::ref<klee::Expr>, const klee::MemoryObject*, klee::ref<klee::Expr>, klee::ref<klee::Expr>): Assertion `isa<ConstantExpr>(address)' failed.
0 klee 0x0000000001030c72 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1 klee 0x00000000010304cc
2 libpthread.so.0 0x00002aeb3f18c390
3 libc.so.6 0x00002aeb3fc6e428 gsignal + 56
4 libc.so.6 0x00002aeb3fc7002a abort + 362
5 libc.so.6 0x00002aeb3fc66bd7
6 libc.so.6 0x00002aeb3fc66c82
7 klee 0x000000000059a2c5 klee::Executor::onRecoveryStateWrite(klee::ExecutionState&, klee::ref<klee::Expr>, klee::MemoryObject const*, klee::ref<klee::Expr>, klee::ref<klee::Expr>) + 1141
8 klee 0x000000000059af7d klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 3149
9 klee 0x000000000059edaa klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 8554
10 klee 0x00000000005a31b4 klee::Executor::run(klee::ExecutionState&) + 2260
11 klee 0x00000000005a398f klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1727
12 klee 0x0000000000569bb8 main + 13080
13 libc.so.6 0x00002aeb3fc59830 __libc_start_main + 240
14 klee 0x000000000057ddb9 _start + 41
Aborted (core dumped)KLEE fails due to missing AllocationRecord
andrea@ruchill:~/work/klee-slicing/klee-slicing-experiments/bc$ /home/andrea/work/klee-slicing/klee-build/bin/klee --stats-write-interval=1000 --istats-write-interval=1000 --simplify-sym-indices --output-module --max-memory=4095 --max-sym-array-size=4096 --disable-inlining --use-cex-cache --libc=uclibc --allow-external-sym-calls --only-output-states-covering-new --watchdog --switch-type=internal --environ=/tmp/test.env --run-in=/tmp/sandbox --max-instruction-time=100. --max-solver-time=30. --max-time=3600. --posix-runtime -split-search --search=random-state --search=nurs:covnew --output-dir=cse-out-bc3 -skip-functions=parse_args,init_storage,yyerror /home/andrea/work/klee-slicing/klee-slicing-experiments/bc/bc-1.06/build/bc/bc.bc A --sym-files 1 8 --sym-stdin 8 --sym-stdout
KLEE: KLEE: WATCHDOG: watching 16217
KLEE: NOTE: Using klee-uclibc : /home/andrea/work/klee-slicing/klee-build/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/andrea/work/klee-slicing/klee-build/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/andrea/work/klee-slicing/klee-slicing-experiments/bc/cse-out-bc3"
Using STP solver backend
KLEE: Runnining pointer analysis...
KLEE: Runnining reachability analysis...
KLEE: Runnining mod-ref analysis...
IntToPtr with constant: <badref> = inttoptr i64 -1 to void (i32)*
Unhandled instruction %reverse690 = shufflevector <16 x i8> %reverse687, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>, !dbg !3523
Unhandled instruction %reverse691 = shufflevector <16 x i8> %reverse689, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>, !dbg !3523
Unhandled instruction %reverse448 = shufflevector <16 x i8> %reverse, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>, !dbg !3529
Unhandled instruction %reverse449 = shufflevector <16 x i8> %reverse447, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>, !dbg !3529
Unhandled instruction %reverse464 = shufflevector <16 x i8> %reverse, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>, !dbg !3522
Unhandled instruction %reverse465 = shufflevector <16 x i8> %reverse463, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>, !dbg !3522
Unhandled instruction %reverse = shufflevector <16 x i8> %wide.load, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>, !dbg !3535
Unhandled instruction %reverse241 = shufflevector <16 x i8> %wide.load240, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>, !dbg !3535
...
KLEE: WARNING: undefined reference to function: __ctype_b_loc
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 104914640)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: ioctl: (TCGETS) symbolic file, incomplete model
INFO: Points-to analysis took 0 sec 0 ms
INFO: Reaching defs analysis took 2 sec 227 ms
DEF-USE: no information for: %new_argv = alloca [1024 x i8*], align 16
DEF-USE: no information for: %call = call noalias i8* @malloc(i64 144) #5
DEF-USE: no information for: %argtype = alloca [3 x i32], align 4
DEF-USE: no information for: %buf = alloca [32 x i8], align 16
DEF-USE: no information for: %buf = alloca [128 x i8], align 16
DEF-USE: no information for: %pad = alloca [1 x i8], align 1
DEF-USE: no information for: %uc = alloca i8, align 1
No reaching definition for: %call.i.i = tail call noalias i8* @malloc(i64 %conv.i.i) #5, !dbg !3503 off: 0
No reaching definition for: %call.i = tail call noalias i8* @malloc(i64 16) #5, !dbg !3473 off: 0
DEF-USE: no information for: %yyssa = alloca [200 x i16], align 16
DEF-USE: no information for: %yyvsa = alloca [200 x %union.YYSTYPE], align 16
No reaching definition for: %call.i14 = tail call noalias i8* @malloc(i64 %conv.i) #5, !dbg !3486 off: 0
No reaching definition for: %call.i = tail call i8* @realloc(i8* %28, i64 %conv.i) #5, !dbg !3520 off: 1
No reaching definition for: %call.i = tail call noalias i8* @malloc(i64 %conv.i) #5, !dbg !3474 off: 0
No reaching definition for: %f = alloca %struct.__STDIO_FILE_STRUCT.244, align 8 off: 4
No reaching definition for: %call = call noalias i8* @malloc(i64 %size) #18, !dbg !3489 off: 8
No reaching definition for: %call = call noalias i8* @malloc(i64 80) #18, !dbg !3502 off: 8
No reaching definition for: %call92 = call noalias i8* @malloc(i64 4096) #18, !dbg !3530 off: 8
DEF-USE: no information for: %call1 = call noalias i8* @malloc(i64 %mul) #5
DEF-USE: no information for: %call5 = call noalias i8* @malloc(i64 24) #5
DEF-USE: no information for: %call16 = call noalias i8* @malloc(i64 24) #5
DEF-USE: no information for: %call9 = call noalias i8* @malloc(i64 4) #5
No reaching definition for: %call.i.i = tail call noalias i8* @malloc(i64 40) #5, !dbg !3492 off: 16
No reaching definition for: %call.i = tail call noalias i8* @malloc(i64 40) #5, !dbg !3537 off: 16
No reaching definition for: %call.i7 = tail call noalias i8* @malloc(i64 40) #5, !dbg !3553 off: 16
No reaching definition for: %call.i22 = tail call noalias i8* @malloc(i64 40) #5, !dbg !3565 off: 16
No reaching definition for: %call.i39 = tail call noalias i8* @malloc(i64 40) #5, !dbg !3582 off: 16
No reaching definition for: %call.i54 = tail call noalias i8* @malloc(i64 40) #5, !dbg !3596 off: 16
No reaching definition for: %call.i69 = tail call noalias i8* @malloc(i64 40) #5, !dbg !3608 off: 16
No reaching definition for: %call.i = tail call noalias i8* @malloc(i64 40) #5, !dbg !3486 off: 16
No reaching definition for: %call.i8 = tail call noalias i8* @malloc(i64 40) #5, !dbg !3509 off: 16
No reaching definition for: %call.i = tail call noalias i8* @malloc(i64 40) #5, !dbg !3490 off: 16
No reaching definition for: %call.i = tail call noalias i8* @malloc(i64 40) #5, !dbg !3492 off: 16
No reaching definition for: %call.i = tail call noalias i8* @malloc(i64 40) #5, !dbg !3502 off: 16
No reaching definition for: %call.i = tail call noalias i8* @malloc(i64 40) #5, !dbg !3515 off: 16
No reaching definition for: %call = tail call noalias i8* @malloc(i64 40) #5, !dbg !3485 off: 16
No reaching definition for: %call.i = tail call noalias i8* @malloc(i64 40) #5, !dbg !3502 off: 16
No reaching definition for: %call.i366 = tail call noalias i8* @malloc(i64 40) #5, !dbg !3682 off: 16
No reaching definition for: %call.i = tail call noalias i8* @malloc(i64 40) #5, !dbg !3507 off: 16
No reaching definition for: %call.i490 = tail call noalias i8* @malloc(i64 40) #5, !dbg !3574 off: 16
No reaching definition for: %call.i144 = call noalias i8* @malloc(i64 40) #5, !dbg !3543 off: 16
INFO: Adding Def-Use edges took 0 sec 272 ms
INFO: Computing control dependencies took 0 sec 0 ms
INFO: Finding dependent nodes took 0 sec 1 ms
INFO: Slicing dependence graph took 0 sec 30 ms
INFO: Sliced away 2069 from 3002 nodes in DG
INFO: saving sliced module to: test.sliced
Could not find any entry for the context
UNREACHABLE executed at /home/andrea/work/klee-slicing/klee/lib/Core/AllocationRecord.cpp:81!
0 libSlicing.so 0x00002aaaab27ab52 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1 libSlicing.so 0x00002aaaab27a2c4
2 libpthread.so.0 0x00002aaaabac2390
3 libc.so.6 0x00002aaaac5a4428 gsignal + 56
4 libc.so.6 0x00002aaaac5a602a abort + 362
5 libSlicing.so 0x00002aaaab24b800 LLVMInstallFatalErrorHandler + 0
6 klee 0x00000000005737cc klee::AllocationRecord::getAddr(klee::ASContext&) + 124
7 klee 0x00000000005322a7 klee::Executor::onExecuteAlloc(klee::ExecutionState&, unsigned long, bool, llvm::Instruction*, bool) + 199
8 klee 0x000000000053ffde klee::Executor::executeAlloc(klee::ExecutionState&, klee::ref<klee::Expr>, bool, klee::KInstruction*, bool, klee::ObjectState const*) + 718
9 klee 0x00000000005643c7 klee::SpecialFunctionHandler::handleMalloc(klee::ExecutionState&, klee::KInstruction*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 87
10 klee 0x0000000000564047 klee::SpecialFunctionHandler::handle(klee::ExecutionState&, llvm::Function*, klee::KInstruction*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 199
11 klee 0x0000000000537b83 klee::Executor::callExternalFunction(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 83
12 klee 0x0000000000544a2e klee::Executor::executeCall(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 254
13 klee 0x0000000000549cea klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 14874
14 klee 0x000000000054c2a7 klee::Executor::run(klee::ExecutionState&) + 1927
15 klee 0x000000000054cb3d klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1949
16 klee 0x0000000000517316 main + 13206
17 libc.so.6 0x00002aaaac58f830 __libc_start_main + 240
18 klee 0x0000000000527759 _start + 41
KLEE: WARNING: KLEE: watchdog exiting (no child)KLEE hangs on dwarfdump/readelf while computing pointer analysis
/home/andrea/work/klee-slicing/klee-build/bin/klee -print-functions -posix-runtime -libc=uclibc -link-llvm-lib=/home/andrea/work/klee-slicing/klee-slicing-experiments/libdwarf/libelf-0.8.13/lib/libelf.a.bc -skip-functions=dwarf_whatform dwarfdump.bc -ka -vvv -R -M ../../regressiontests/marinescu/hello.original
KLEE: NOTE: Using klee-uclibc : /home/andrea/work/klee-slicing/klee-build/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/andrea/work/klee-slicing/klee-build/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: Linking in library: /home/andrea/work/klee-slicing/klee-slicing-experiments/libdwarf/libelf-0.8.13/lib/libelf.a.bc.
KLEE: output directory is "/home/andrea/work/klee-slicing/klee-slicing-experiments/libdwarf/dwarf-20110612/dwarfdump/klee-out-14"
Using STP solver backend
KLEE: Runnining reachability analysis...
KLEE: Runnining pointer analysis...KLEE does not proceed even after one hour. A quick debug with gdb points out that the analysis might get stuck here:
(gdb) r
Starting program: /home/andrea/work/klee-slicing/klee-build/bin/klee -print-functions -posix-runtime -libc=uclibc -link-llvm-lib=/home/andrea/work/klee-slicing/klee-slicing-experiments/libdwarf/libelf-0.8.13/lib/libelf.a.bc -skip-functions=dwarf_whatform dwarfdump.bc -ka -vvv -R -M ../../regressiontests/marinescu/hello.original
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".
KLEE: NOTE: Using klee-uclibc : /home/andrea/work/klee-slicing/klee-build/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/andrea/work/klee-slicing/klee-build/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: Linking in library: /home/andrea/work/klee-slicing/klee-slicing-experiments/libdwarf/libelf-0.8.13/lib/libelf.a.bc.
KLEE: output directory is "/home/andrea/work/klee-slicing/klee-slicing-experiments/libdwarf/dwarf-20110612/dwarfdump/klee-out-13"
Using STP solver backend
KLEE: Runnining reachability analysis...
KLEE: Runnining pointer analysis...
^C
Program received signal SIGINT, Interrupt.
0x00002aaaaca37380 in Andersen::processCopy(unsigned int, ConstraintEdge const*) () from /home/andrea/work/klee-slicing/SVF/build/lib/Svf.so
(gdb) where
#0 0x00002aaaaca37380 in Andersen::processCopy(unsigned int, ConstraintEdge const*) () from /home/andrea/work/klee-slicing/SVF/build/lib/Svf.so
#1 0x00002aaaaca362ce in Andersen::processNode(unsigned int) () from /home/andrea/work/klee-slicing/SVF/build/lib/Svf.so
#2 0x00002aaaaaed8f2d in WPASolver<ConstraintGraph*>::postProcessNode (this=0x222f8d0, node=119766) at /home/andrea/work/klee-slicing/SVF/include/WPA/WPASolver.h:120
#3 0x00002aaaaca20b80 in Andersen::analyze(llvm::Module&) () from /home/andrea/work/klee-slicing/SVF/build/lib/Svf.so
#4 0x00002aaaaaed54b6 in AAPass::runPointerAnalysis (this=0x2e77290, module=..., kind=0) at AAPass.cpp:45
#5 0x00002aaaaaed5310 in AAPass::runOnModule (this=0x2e77290, module=...) at AAPass.cpp:19
#6 0x00002aaaab1d97d8 in llvm::legacy::PassManagerImpl::run(llvm::Module&) () from /home/andrea/work/klee-slicing/se-slicing/libSlicing.so
#7 0x000000000058a8ff in klee::KModule::prepare (this=0x45f4ce0, opts=..., skippedFunctions=std::vector of length 1, capacity 1 = {...}, ih=0x3513740, ra=0x2e5dd00, inliner=0x3b17480, aa=0x2e77290, mra=0x3cd8a00,
cloner=0x37dd4c0, sliceGenerator=0x39e2830) at /home/andrea/work/klee-slicing/klee/lib/Module/KModule.cpp:459
#8 0x000000000053414f in klee::Executor::setModule (this=0x28e6a30, module=0x142a540, opts=...) at /home/andrea/work/klee-slicing/klee/lib/Core/Executor.cpp:470
#9 0x0000000000514a41 in main (argc=<optimized out>, argv=<optimized out>, envp=<optimized out>) at /home/andrea/work/klee-slicing/klee/tools/klee/main.cpp:1528
(gdb) continue
Continuing.
^C
Program received signal SIGINT, Interrupt.
0x00002aaaaca37384 in Andersen::processCopy(unsigned int, ConstraintEdge const*) () from /home/andrea/work/klee-slicing/SVF/build/lib/Svf.so
(gdb) where
#0 0x00002aaaaca37384 in Andersen::processCopy(unsigned int, ConstraintEdge const*) () from /home/andrea/work/klee-slicing/SVF/build/lib/Svf.so
#1 0x00002aaaaca362ce in Andersen::processNode(unsigned int) () from /home/andrea/work/klee-slicing/SVF/build/lib/Svf.so
#2 0x00002aaaaaed8f2d in WPASolver<ConstraintGraph*>::postProcessNode (this=0x222f8d0, node=419) at /home/andrea/work/klee-slicing/SVF/include/WPA/WPASolver.h:120
#3 0x00002aaaaca20b80 in Andersen::analyze(llvm::Module&) () from /home/andrea/work/klee-slicing/SVF/build/lib/Svf.so
#4 0x00002aaaaaed54b6 in AAPass::runPointerAnalysis (this=0x2e77290, module=..., kind=0) at AAPass.cpp:45
#5 0x00002aaaaaed5310 in AAPass::runOnModule (this=0x2e77290, module=...) at AAPass.cpp:19
#6 0x00002aaaab1d97d8 in llvm::legacy::PassManagerImpl::run(llvm::Module&) () from /home/andrea/work/klee-slicing/se-slicing/libSlicing.so
#7 0x000000000058a8ff in klee::KModule::prepare (this=0x45f4ce0, opts=..., skippedFunctions=std::vector of length 1, capacity 1 = {...}, ih=0x3513740, ra=0x2e5dd00, inliner=0x3b17480, aa=0x2e77290, mra=0x3cd8a00,
cloner=0x37dd4c0, sliceGenerator=0x39e2830) at /home/andrea/work/klee-slicing/klee/lib/Module/KModule.cpp:459
#8 0x000000000053414f in klee::Executor::setModule (this=0x28e6a30, module=0x142a540, opts=...) at /home/andrea/work/klee-slicing/klee/lib/Core/Executor.cpp:470
#9 0x0000000000514a41 in main (argc=<optimized out>, argv=<optimized out>, envp=<optimized out>) at /home/andrea/work/klee-slicing/klee/tools/klee/main.cpp:1528Is it where you try to optimize by computing a fixed point?
KLEE has memory leaks
- Configured CMake with ASAN:
$ CXXFLAGS="-fno-rtti -fsanitize=address -fno-omit-frame-pointer" CFLAGS="-fsanitize=address -fno-omit-frame-pointer" cmake -DENABLE_SOLVER_STP=ON -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=/home/andrea/work/klee-slicing/klee-uclibc -DLLVM_CONFIG_BINARY=/usr/local/bin/llvm-config -DENABLE_UNIT_TESTS=OFF -DKLEE_RUNTIME_BUILD_TYPE=Release+Asserts -DENABLE_SYSTEM_TESTS=ON -DSVF_ROOT_DIR=/home/andrea/work/klee-slicing/SVF -DDG_ROOT_DIR=/home/andrea/work/klee-slicing/dg -DSLICING_ROOT_DIR=/home/andrea/work/klee-slicing/se-slicing ../klee- Compiled with:
$ make -j8- Check the tests:
$ make check
...
********************
Testing Time: 25.86s
********************
Failing Tests (31):
KLEE :: Slicing/basic.c
KLEE :: Slicing/dependent-functions.c
KLEE :: Slicing/dynamic-list.c
KLEE :: Slicing/field-sensitivity.c
KLEE :: Slicing/fork.c
KLEE :: Slicing/function-pointer.c
KLEE :: Slicing/function-pointer2.c
KLEE :: Slicing/function-pointer3.c
KLEE :: Slicing/guiding-constraints-in-recovery-state.c
KLEE :: Slicing/independent-functions.c
KLEE :: Slicing/infeasible.c
KLEE :: Slicing/infeasible2.c
KLEE :: Slicing/infeasible3.c
KLEE :: Slicing/infeasible4.c
KLEE :: Slicing/libc-atexit.c
KLEE :: Slicing/malloc.c
KLEE :: Slicing/multiple-allocsite-multiple-callsite.c
KLEE :: Slicing/multiple-slices.c
KLEE :: Slicing/non-void-skip.c
KLEE :: Slicing/overriding-store.c
KLEE :: Slicing/overriding-store2.c
KLEE :: Slicing/single-allocsite-multiple-callsite.c
KLEE :: Slicing/single-allocsite-multiple-callsite2.c
KLEE :: Slicing/single-allocsite-single-callsite.c
KLEE :: Slicing/skip-called-function.c
KLEE :: Slicing/skip-calling-function.c
KLEE :: Slicing/skip-multiple-without-recovery.c
KLEE :: Slicing/skip-with-buffer.c
KLEE :: Slicing/skip-with-buffer2.c
KLEE :: Slicing/skip-without-recovery.c
KLEE :: Slicing/test-check-consistency.c
Expected Passes : 192
Expected Failures : 2
Unsupported Tests : 2
Unexpected Failures: 31The complete list of memory leaks is usually displayed on stdout. For example, you can run:
$ bin/klee -search=dfs -skip-functions=foo /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/single-allocsite-multiple-callsite2.c.tmp.bcto get a complete list of memory leaks.
ReturnToVoidFunction pass does not properly handle functions that return structs
The issue is mainly due to how LLVM handles the returned struct:
define i32 @main(i32 %argc, i8** %argv, i8** %envp) #0 {
entry:
%retval = alloca i32, align 4
%argc.addr = alloca i32, align 4
%argv.addr = alloca i8**, align 8
%envp.addr = alloca i8**, align 8
%k = alloca i32, align 4
%o = alloca %struct.point, align 4
store i32 0, i32* %retval
store i32 %argc, i32* %argc.addr, align 4
store i8** %argv, i8*** %argv.addr, align 8
store i8** %envp, i8*** %envp.addr, align 8
%0 = bitcast i32* %k to i8*
call void @klee_make_symbolic(i8* %0, i64 4, i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0))
%call = call { i64, i64 } @f()
%1 = bitcast %struct.point* %o to { i64, i64 }*
%2 = getelementptr { i64, i64 }* %1, i32 0, i32 0
%3 = extractvalue { i64, i64 } %call, 0
store i64 %3, i64* %2, align 1
%4 = getelementptr { i64, i64 }* %1, i32 0, i32 1
%5 = extractvalue { i64, i64 } %call, 1
store i64 %5, i64* %4, align 1
%x = getelementptr inbounds %struct.point* %o, i32 0, i32 0
store i32 876, i32* %x, align 4
%6 = load i32* %k, align 4
%cmp = icmp sgt i32 %6, 0My guess is that we should remove all the code related to the copy of values from struct to struct.
Skipping getenv gives "unbound load" and "memory error: out of bound pointer"
This is on the bc benchmark again. Unfortunately, I was not able to isolate a list of skipped functions that triggers it on vanilla Chopper, so reproducibility is bad for this one. Maybe you would have a clue regardless. This is how it goes:
I specify a list of functions that should not be skipped, and skip everything else. I have narrowed down that if I specify to not skip:
- __errno_location
- __h_errno_location
- __user_main
- __uClibc_main
- isatty
- getenv
then I get no error but if I specify to *not * skip
- __errno_location
- __h_errno_location
- __user_main
- __uClibc_main
- isatty
I get:
$ klee -libc=uclibc -simplify-sym-indices -search=nurs:covnew -split-search -skip-functions-not=__errno_location,__h_errno_location,__user_main,__uClibc_main,isatty -autokeep=0 bc.bc
[dc58bf] KLEE: ■ __uClibc_main
[dc58bf] KLEE: ■ ■ __wrap_memset
[dc58bf] KLEE: ■ ■ __uClibc_init
[dc58bf] KLEE: ■ ■ __wrap_strrchr
[dc58bf] KLEE: ■ ■ __wrap_llvm.expect.i64
[dc58bf] KLEE: ■ ■ __uClibc_init
[dc58bf] KLEE: ■ ■ ■ __wrap_llvm.expect.i64
[dc58bf] KLEE: ■ ■ __errno_location
[dc58bf] KLEE: ■ ■ __wrap_llvm.expect.i64
[dc58bf] KLEE: ■ ■ __uClibc_init
[dc58bf] KLEE: ■ ■ ■ __wrap_llvm.expect.i64
[dc58bf] KLEE: ■ ■ __h_errno_location
[64b40a] KLEE: WARNING ONCE: calling __user_main with extra arguments.
[dc58bf] KLEE: ■ ■ ■ isatty
[dc58bf] KLEE: ■ ■ ■ ■ __wrap_tcgetattr
[dc58bf] KLEE: ■ ■ ■ setvbuf
[dc58bf] KLEE: ■ ■ ■ __wrap_getenv
[13eaf3] KLEE: WARNING: UNBOUND, inst=load
[d6c361] KLEE: ERROR: /home/ubuntu/code/chopper-experiments/bc/bc-1.06/build/bc/../../bc/main.c:184: memory error: out of bound pointer
[b3874e] KLEE: NOTE: now ignoring this error at this location
Do you know the signification of this WARNING: UNBOUND, inst=load and this memory error: out of bound pointer?
KLEE crashes on dwarfdump
/home/andrea/work/klee-slicing/klee-build/bin/klee --link-llvm-lib=/home/andrea/work/klee-slicing/klee-slicing-experiments/libdwarf/libelf-0.8.13/lib/libelf.a.bc -skip-functions=dwarf_record_cmdline_options dwarfdump.bc -ka ../../regressiontests/marinescu/hello.original
KLEE: Linking in library: /home/andrea/work/klee-slicing/klee-slicing-experiments/libdwarf/libelf-0.8.13/lib/libelf.a.bc.
KLEE: output directory is "/home/andrea/work/klee-slicing/klee-slicing-experiments/libdwarf/dwarf-20110612/dwarfdump/klee-out-48"
Using STP solver backend
KLEE: Runnining reachability analysis...
KLEE: Runnining pointer analysis...
KLEE: Runnining mod-ref analysis...
KLEE: Computing slices...
IntToPtr with constant: <badref> = inttoptr i64 -1 to i8*
%reverse463 = shufflevector <16 x i8> %reverse, <16 x i8> undef, <16 x i32> <i32 15, i32 14, i32 13, i32 12, i32 11, i32 10, i32 9, i32 8, i32 7, i32 6, i32 5, i32 4, i32 3, i32 2, i32 1, i32 0>
klee: /home/andrea/work/klee-slicing/dg/src/llvm/analysis/PointsTo/PointerSubgraph.cpp:1419: dg::analysis::pta::PSNodesSeq dg::analysis::pta::LLVMPointerSubgraphBuilder::buildInstruction(const llvm::Instruction&): Assertion `0 && "Unhandled instruction"' failed.
0 libSlicing.so 0x00002aaaab266752 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1 libSlicing.so 0x00002aaaab265ec4
2 libpthread.so.0 0x00002aaaabaa9390
3 libc.so.6 0x00002aaaac58b428 gsignal + 56
4 libc.so.6 0x00002aaaac58d02a abort + 362
5 libc.so.6 0x00002aaaac583bd7
6 libc.so.6 0x00002aaaac583c82
7 libLLVMpta.so 0x00002aaaad3168f0 dg::analysis::pta::LLVMPointerSubgraphBuilder::buildInstruction(llvm::Instruction const&) + 678
8 libLLVMpta.so 0x00002aaaad3139e0 dg::analysis::pta::LLVMPointerSubgraphBuilder::buildNode(llvm::Value const*) + 118
9 libLLVMpta.so 0x00002aaaad313c75 dg::analysis::pta::LLVMPointerSubgraphBuilder::getOperand(llvm::Value const*) + 93
10 libLLVMpta.so 0x00002aaaad314eb1 dg::analysis::pta::LLVMPointerSubgraphBuilder::createStore(llvm::Instruction const*) + 59
11 libLLVMpta.so 0x00002aaaad3166d1 dg::analysis::pta::LLVMPointerSubgraphBuilder::buildInstruction(llvm::Instruction const&) + 135
12 libLLVMpta.so 0x00002aaaad316f77 dg::analysis::pta::LLVMPointerSubgraphBuilder::buildPointerSubgraphBlock(llvm::BasicBlock const&) + 249
13 libLLVMpta.so 0x00002aaaad31713e dg::analysis::pta::LLVMPointerSubgraphBuilder::buildFunction(llvm::Function const&) + 354
14 libLLVMpta.so 0x00002aaaad31419c dg::analysis::pta::LLVMPointerSubgraphBuilder::createCallToFunction(llvm::Function const*) + 236
15 libLLVMpta.so 0x00002aaaad31432e dg::analysis::pta::LLVMPointerSubgraphBuilder::createOrGetSubgraph(llvm::CallInst const*, llvm::Function const*) + 54
16 libLLVMpta.so 0x00002aaaad314c8d dg::analysis::pta::LLVMPointerSubgraphBuilder::createCall(llvm::Instruction const*) + 321
17 libLLVMpta.so 0x00002aaaad3167e5 dg::analysis::pta::LLVMPointerSubgraphBuilder::buildInstruction(llvm::Instruction const&) + 411
18 libLLVMpta.so 0x00002aaaad316f77 dg::analysis::pta::LLVMPointerSubgraphBuilder::buildPointerSubgraphBlock(llvm::BasicBlock const&) + 249
19 libLLVMpta.so 0x00002aaaad31713e dg::analysis::pta::LLVMPointerSubgraphBuilder::buildFunction(llvm::Function const&) + 354
20 libLLVMpta.so 0x00002aaaad31419c dg::analysis::pta::LLVMPointerSubgraphBuilder::createCallToFunction(llvm::Function const*) + 236
21 libLLVMpta.so 0x00002aaaad31432e dg::analysis::pta::LLVMPointerSubgraphBuilder::createOrGetSubgraph(llvm::CallInst const*, llvm::Function const*) + 54
22 libLLVMpta.so 0x00002aaaad314c8d dg::analysis::pta::LLVMPointerSubgraphBuilder::createCall(llvm::Instruction const*) + 321
23 libLLVMpta.so 0x00002aaaad3167e5 dg::analysis::pta::LLVMPointerSubgraphBuilder::buildInstruction(llvm::Instruction const&) + 411
24 libLLVMpta.so 0x00002aaaad316f77 dg::analysis::pta::LLVMPointerSubgraphBuilder::buildPointerSubgraphBlock(llvm::BasicBlock const&) + 249
25 libLLVMpta.so 0x00002aaaad31713e dg::analysis::pta::LLVMPointerSubgraphBuilder::buildFunction(llvm::Function const&) + 354
26 libLLVMpta.so 0x00002aaaad31419c dg::analysis::pta::LLVMPointerSubgraphBuilder::createCallToFunction(llvm::Function const*) + 236
27 libLLVMpta.so 0x00002aaaad31432e dg::analysis::pta::LLVMPointerSubgraphBuilder::createOrGetSubgraph(llvm::CallInst const*, llvm::Function const*) + 54
28 libLLVMpta.so 0x00002aaaad314c8d dg::analysis::pta::LLVMPointerSubgraphBuilder::createCall(llvm::Instruction const*) + 321
29 libLLVMpta.so 0x00002aaaad3167e5 dg::analysis::pta::LLVMPointerSubgraphBuilder::buildInstruction(llvm::Instruction const&) + 411
30 libLLVMpta.so 0x00002aaaad316f77 dg::analysis::pta::LLVMPointerSubgraphBuilder::buildPointerSubgraphBlock(llvm::BasicBlock const&) + 249
31 libLLVMpta.so 0x00002aaaad31713e dg::analysis::pta::LLVMPointerSubgraphBuilder::buildFunction(llvm::Function const&) + 354
32 libLLVMpta.so 0x00002aaaad31419c dg::analysis::pta::LLVMPointerSubgraphBuilder::createCallToFunction(llvm::Function const*) + 236
33 libLLVMpta.so 0x00002aaaad31432e dg::analysis::pta::LLVMPointerSubgraphBuilder::createOrGetSubgraph(llvm::CallInst const*, llvm::Function const*) + 54
34 libLLVMpta.so 0x00002aaaad3142f5 dg::analysis::pta::LLVMPointerSubgraphBuilder::createFuncptrCall(llvm::CallInst const*, llvm::Function const*) + 51
35 libSlicing.so 0x00002aaaaaefa95d SVFPointerAnalysis::functionPointerCall(dg::analysis::pta::PSNode*, dg::analysis::pta::PSNode*) + 239
36 libSlicing.so 0x00002aaaaaefa848 SVFPointerAnalysis::handleFuncPtr(dg::analysis::pta::PSNode*) + 198
37 libSlicing.so 0x00002aaaaaefa540 SVFPointerAnalysis::handleVirtualCalls() + 314
38 libSlicing.so 0x00002aaaaaefa1cf SVFPointerAnalysis::run() + 39
39 libSlicing.so 0x00002aaaaaf32283 SliceGenerator::generate() + 333
40 klee 0x000000000058a92b klee::KModule::prepare(klee::Interpreter::ModuleOptions const&, std::vector<klee::Interpreter::SkippedFunctionOption, std::allocator<klee::Interpreter::SkippedFunctionOption> > const&, klee::InterpreterHandler*, ReachabilityAnalysis*, Inliner*, AAPass*, ModRefAnalysis*, Cloner*, SliceGenerator*) + 3435
41 klee 0x000000000053414f klee::Executor::setModule(llvm::Module*, klee::Interpreter::ModuleOptions const&) + 1551
42 klee 0x0000000000514a41 main + 4689
43 libc.so.6 0x00002aaaac576830 __libc_start_main + 240
44 klee 0x0000000000526f29 _start + 41
Aborted (core dumped)Do we support vectors?
Slicing fails and introduces false positives
On seq I can observe this:
andrea@ruchill:~/work/klee-slicing/klee-slicing-experiments/coreutils$ /home/andrea/work/klee-slicing/klee-build/bin/klee --simplify-sym-indices --output-module --max-memory=4095 --max-sym-array-size=4096 --disable-inlining --use-forked-solver --use-cex-cache --libc=uclibc --posix-runtime --allow-external-sym-calls --only-output-states-covering-new --max-memory-inhibit=false --environ=/tmp/test.env --run-in=/tmp/sandbox --max-instruction-time=200. --max-solver-time=200. --max-time=4000. -split-search -split-ratio=10 --search=nurs:covnew --skip-functions=parse_options,scan_arg --exit-on-error-type=Ptr /home/andrea/work/klee-slicing/klee-slicing-experiments/coreutils/coreutils-6.10/obj-llvm/src/seq.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout
KLEE: NOTE: Using klee-uclibc : /home/andrea/work/klee-slicing/klee-build/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/andrea/work/klee-slicing/klee-build/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/andrea/work/klee-slicing/klee-slicing-experiments/coreutils/coreutils-6.10/obj-llvm/src/klee-out-9"
Using STP solver backend
KLEE: Runnining reachability analysis...
KLEE: Runnining pointer analysis...
KLEE: Runnining mod-ref analysis...
KLEE: Computing slices...
...
KLEE: WARNING: undefined reference to function: __crit_80_0
KLEE: WARNING: undefined reference to function: __crit_81_0
KLEE: WARNING: undefined reference to function: __crit_82_0
KLEE: WARNING: undefined reference to function: __crit_83_0
KLEE: WARNING: undefined reference to function: __crit_84_0
KLEE: WARNING: undefined reference to function: __crit_85_0
KLEE: WARNING: undefined reference to function: __crit_86_0
KLEE: WARNING: undefined reference to function: __crit_87_0
KLEE: WARNING: undefined reference to function: __crit_88_0
KLEE: WARNING: undefined reference to function: __crit_89_0
...
KLEE: WARNING ONCE: calling __user_main with extra arguments.
INFO: Points-to analysis took 0 sec 0 ms
INFO: Reaching defs analysis took 10 sec 360 ms
DEF-USE: no information for: %call16 = call noalias i8* @malloc(i64 24) #6
DEF-USE: no information for: %call1 = call noalias i8* @malloc(i64 %mul) #6
DEF-USE: no information for: %call5 = call noalias i8* @malloc(i64 24) #6
DEF-USE: no information for: %new_argv = alloca [1024 x i8*], align 16
DEF-USE: no information for: %call = call noalias i8* @malloc(i64 144) #6
No reaching definition for: %o = alloca %struct.quoting_options, align 4 off: 0
DEF-USE: no information for: %ret = alloca %struct.operand, align 16
DEF-USE: no information for: %call9 = call noalias i8* @malloc(i64 4) #6
No reaching definition for: %f = alloca %struct.__STDIO_FILE_STRUCT.19, align 8 off: 64
No reaching definition for: %arg = alloca [1 x %struct.__va_list_tag], align 16 off: 18446744073709551615
No reaching definition for: %ppfs = alloca %struct.ppfs_t, align 16 off: 96
No reaching definition for: %arg = alloca [1 x %struct.__va_list_tag], align 16 off: 18446744073709551615
DEF-USE: no information for: %arg = alloca [1 x %struct.__va_list_tag], align 16
INFO: Adding Def-Use edges took 1 sec 61 ms
INFO: Computing control dependencies took 0 sec 4 ms
INFO: Finding dependent nodes took 0 sec 50 ms
INFO: Slicing dependence graph took 0 sec 52 ms
INFO: Sliced away 2383 from 9101 nodes in DG
INFO: saving sliced module to: test.sliced
INFO: Points-to analysis took 0 sec 0 ms
INFO: Reaching defs analysis took 10 sec 564 ms
INFO: Adding Def-Use edges took 0 sec 65 ms
INFO: Computing control dependencies took 0 sec 4 ms
INFO: Finding dependent nodes took 0 sec 925 ms
INFO: Slicing dependence graph took 0 sec 50 ms
INFO: Sliced away 2337 from 9101 nodes in DG
INFO: saving sliced module to: test.sliced
INFO: Points-to analysis took 0 sec 0 ms
INFO: Reaching defs analysis took 10 sec 686 ms
INFO: Adding Def-Use edges took 0 sec 702 ms
INFO: Computing control dependencies took 0 sec 4 ms
INFO: Finding dependent nodes took 0 sec 43 ms
INFO: Slicing dependence graph took 0 sec 49 ms
INFO: Sliced away 2348 from 9101 nodes in DG
INFO: saving sliced module to: test.sliced
INFO: Points-to analysis took 0 sec 0 ms
Did not find slicing criterion
- __crit_81_0
INFO: saving sliced module to: test.slicedHowever, in the sa.log file I can find references to the criterion:
define i32 @fclose_clone_150(%struct.__STDIO_FILE_STRUCT.189* %stream) #-1 {
entry:
%0 = load %struct.__STDIO_FILE_STRUCT.189** @_stdio_openlist, align 8, !dbg !0
%1 = load %struct.__STDIO_FILE_STRUCT.189** @_stdio_openlist, align 8, !dbg !41
%cmp = icmp eq %struct.__STDIO_FILE_STRUCT.189* %1, %stream, !dbg !41
br i1 %cmp, label %if.then, label %while.cond, !dbg !41
...
if.end10: ; preds = %if.then9, %if.end7
%rv.0 = phi i32 [ %call, %if.then9 ], [ 0, %if.end7 ]
%__filedes = getelementptr inbounds %struct.__STDIO_FILE_STRUCT.189* %stream, i32 0, i32 2, !dbg !61
%7 = load i32* %__filedes, align 4, !dbg !61
%call11 = call i32 @close(i32 %7) #0, !dbg !61
%cmp12 = icmp slt i32 %call11, 0, !dbg !61
%.rv.0 = select i1 %cmp12, i32 -1, i32 %rv.0, !dbg !61
%__filedes16 = getelementptr inbounds %struct.__STDIO_FILE_STRUCT.189* %stream, i32 0, i32 2, !dbg !63
store i32 -1, i32* %__filedes16, align 4, !dbg !63
%__crit_arg_1079 = load i32* %__filedes16, align 4
call void @__crit_81_0(i32 %__crit_arg_1079)
...What's happening?
Optimization: avoid expensive slicing when everything is concrete
What counts as a reproduction? Will the generated test cases for CVEs crash the original program?
Hi, I am using chopper to reproduce CVE-2012-1569. I have run the following command:make run-cse-dfs under the folder chopper-experiments/libtasn1/CVE-2012-1569 . I have commented out the option --no-output in the Makefile to generate testcases.
After that, I tried to create a crash directly on the original program:
KTEST_FILE=./cse-run-dfs/test001085.ktest ./test 32
where test001085.ktest is the generated test file which triggered memory error (since there is a file named test001085.ptr.err inside cse-run-dfs directory) and ./test was compiled from chopper-experiments/libtasn1/CVE-2012-1569/main.c.
This run will not crash the program. In fact it only overflows the input buffer to asn1_der_decoding slightly, in decoding.c, line 1118:
if ((der[counter]) || der[counter + 1])
Here der is the input buffer to asn1_der_decoding which has a size of 32 bytes and counter also equal to 32. klee correctly reported it as a memory access error and aborted searching but the effect of this particular buffer overflow is benign and will not crash the program.
However, the original description of CVE-2012-1569 mentions a different behavior: asn1_get_length_der returns a very large length value which can crash the program.
I am curious what is the principle you used to claim a "CVE reproduction"? Does any memory access error found by KLEE near the CVE crash location count as a "reproduction"(even though these errors may not actually crash the program when replayed) ? Thanks.
Reduce sa.log size
Currently we dump many interesting things. Unfortunately, on large applications this leads to huge files:
andrea@ruchill$ ll -h coreutils-6.10/obj-llvm/src/klee-last/sa.log
-rw-rw-r-- 1 andrea andrea 3.4M Aug 14 09:23 coreutils-6.10/obj-llvm/src/klee-last/sa.logmake error
I have encountered the following error during the installation process and how can I fix it?
sunghyun@ubuntu:~/chopper/klee_build$ make
[ 9%] Built target kleeAnalysis
[ 21%] Built target kleaverExpr
[ 29%] Built target kleeSupport
[ 48%] Built target kleaverSolver
[ 52%] Built target kleeBasic
[ 72%] Built target kleeCore
[ 82%] Built target kleeModule
[ 83%] Performing RuntimeBuild step for 'BuildKLEERuntimes'
make[3]: Entering directory /home/sunghyun/chopper/klee_build/runtime' make[4]: Entering directory /home/sunghyun/chopper/klee_build/runtime/Intrinsic'
make[4]: Leaving directory /home/sunghyun/chopper/klee_build/runtime/Intrinsic' make[4]: Entering directory /home/sunghyun/chopper/klee_build/runtime/klee-libc'
make[4]: Leaving directory /home/sunghyun/chopper/klee_build/runtime/klee-libc' make[4]: Entering directory /home/sunghyun/chopper/klee_build/runtime/POSIX'
make[4]: Leaving directory /home/sunghyun/chopper/klee_build/runtime/POSIX' make[3]: Leaving directory /home/sunghyun/chopper/klee_build/runtime'
[ 83%] Completed 'BuildKLEERuntimes'
[ 90%] Built target BuildKLEERuntimes
[ 92%] Built target kleeRuntest
[ 93%] Built target gen-random-bout
Linking CXX executable ../../bin/kleaver
../../lib/libkleaverSolver.a(FastCexSolver.cpp.o): In function propogateValues': /home/sunghyun/chopper/lib/Solver/FastCexSolver.cpp:1012: undefined reference to llvm::DebugFlag'
/home/sunghyun/chopper/lib/Solver/FastCexSolver.cpp:1012: undefined reference to llvm::isCurrentDebugType(char const*)' ../../lib/libkleaverSolver.a(FastCexSolver.cpp.o): In function CexData::propogatePossibleValues(klee::refklee::Expr, ValueRange)':
/home/sunghyun/chopper/lib/Solver/FastCexSolver.cpp:444: undefined reference to llvm::DebugFlag' /home/sunghyun/chopper/lib/Solver/FastCexSolver.cpp:444: undefined reference to llvm::isCurrentDebugType(char const*)'
../../lib/libkleaverSolver.a(IndependentSolver.cpp.o): In function getIndependentConstraints': /home/sunghyun/chopper/lib/Solver/IndependentSolver.cpp:353: undefined reference to llvm::DebugFlag'
/home/sunghyun/chopper/lib/Solver/IndependentSolver.cpp:353: undefined reference to `llvm::isCurrentDebugType(char const*)'
collect2: error: ld returned 1 exit status
make[2]: *** [bin/kleaver] Error 1
make[1]: *** [tools/kleaver/CMakeFiles/kleaver.dir/all] Error 2
make: *** [all] Error 2
Tests now fail
Updating SVF to a newer version that fixes #10 leads KLEE to fail on 6 test cases:
FAIL: KLEE :: Slicing/infeasible.c (173 of 245)
******************** TEST 'KLEE :: Slicing/infeasible.c' FAILED ********************
Script:
--
/usr/local/bin/clang-3.4 -I/home/andrea/work/klee-slicing/klee/include /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible.c -emit-llvm -O0 -c -o /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.bc
rm -rf /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.klee-out
/home/andrea/work/klee-slicing/klee-build/bin/klee --output-dir=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.klee-out -search=dfs -skip-functions=f,g /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.bc > /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.out 2>&1
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.out -check-prefix=CHECK-PATHS -check-prefix=CHECK-STATES -check-prefix=CHECK-SLICES -check-prefix=CHECK-SNAPSHOTS
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.out -check-prefix=CHECK-A
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.out -check-prefix=CHECK-ANOT
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.out -check-prefix=CHECK-Y
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.out -check-prefix=CHECK-YNOT
--
Exit Code: 1
Command Output (stdout):
--
$ "/usr/local/bin/clang-3.4" "-I/home/andrea/work/klee-slicing/klee/include" "/home/andrea/work/klee-slicing/klee/test/Slicing/infeasible.c" "-emit-llvm" "-O0" "-c" "-o" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.bc"
$ "rm" "-rf" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.klee-out"
$ "/home/andrea/work/klee-slicing/klee-build/bin/klee" "--output-dir=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.klee-out" "-search=dfs" "-skip-functions=f,g" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.bc"
$ "FileCheck" "/home/andrea/work/klee-slicing/klee/test/Slicing/infeasible.c" "-input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.out" "-check-prefix=CHECK-PATHS" "-check-prefix=CHECK-STATES" "-check-prefix=CHECK-SLICES" "-check-prefix=CHECK-SNAPSHOTS"
# command stderr:
/home/andrea/work/klee-slicing/klee/test/Slicing/infeasible.c:11:18: error: expected string not found in input
// CHECK-STATES: KLEE: done: recovery states = 4
^
/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.out:36:1: note: scanning from here
KLEE: done: generated tests = 3
^
/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible.c.tmp.out:37:1: note: possible intended match here
KLEE: done: recovery states = 6
^
error: command failed with exit status: 1
--
********************
FAIL: KLEE :: Slicing/infeasible3.c (176 of 245)
******************** TEST 'KLEE :: Slicing/infeasible3.c' FAILED ********************
Script:
--
/usr/local/bin/clang-3.4 -I/home/andrea/work/klee-slicing/klee/include /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible3.c -emit-llvm -O0 -c -o /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.bc
rm -rf /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.klee-out
/home/andrea/work/klee-slicing/klee-build/bin/klee --output-dir=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.klee-out -search=dfs -skip-functions=f,g /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.bc > /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.out 2>&1
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible3.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.out -check-prefix=CHECK-PATHS -check-prefix=CHECK-STATES -check-prefix=CHECK-SLICES -check-prefix=CHECK-SNAPSHOTS
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible3.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.out -check-prefix=CHECK-A
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible3.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.out -check-prefix=CHECK-ANOT
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible3.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.out -check-prefix=CHECK-B
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible3.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.out -check-prefix=CHECK-BNOT
--
Exit Code: 1
Command Output (stdout):
--
$ "/usr/local/bin/clang-3.4" "-I/home/andrea/work/klee-slicing/klee/include" "/home/andrea/work/klee-slicing/klee/test/Slicing/infeasible3.c" "-emit-llvm" "-O0" "-c" "-o" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.bc"
$ "rm" "-rf" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.klee-out"
$ "/home/andrea/work/klee-slicing/klee-build/bin/klee" "--output-dir=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.klee-out" "-search=dfs" "-skip-functions=f,g" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.bc"
$ "FileCheck" "/home/andrea/work/klee-slicing/klee/test/Slicing/infeasible3.c" "-input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.out" "-check-prefix=CHECK-PATHS" "-check-prefix=CHECK-STATES" "-check-prefix=CHECK-SLICES" "-check-prefix=CHECK-SNAPSHOTS"
# command stderr:
/home/andrea/work/klee-slicing/klee/test/Slicing/infeasible3.c:11:18: error: expected string not found in input
// CHECK-STATES: KLEE: done: recovery states = 6
^
/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.out:38:1: note: scanning from here
KLEE: done: generated tests = 5
^
/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible3.c.tmp.out:39:1: note: possible intended match here
KLEE: done: recovery states = 8
^
error: command failed with exit status: 1
--
********************
FAIL: KLEE :: Slicing/infeasible4.c (178 of 245)
******************** TEST 'KLEE :: Slicing/infeasible4.c' FAILED ********************
Script:
--
/usr/local/bin/clang-3.4 -I/home/andrea/work/klee-slicing/klee/include /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible4.c -emit-llvm -O0 -c -o /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.bc
rm -rf /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.klee-out
/home/andrea/work/klee-slicing/klee-build/bin/klee --output-dir=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.klee-out -search=dfs -skip-functions=f,g,h /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.bc > /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.out 2>&1
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible4.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.out -check-prefix=CHECK-PATHS -check-prefix=CHECK-STATES -check-prefix=CHECK-SLICES -check-prefix=CHECK-SNAPSHOTS
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible4.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.out -check-prefix=CHECK-A
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible4.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.out -check-prefix=CHECK-ANOT
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible4.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.out -check-prefix=CHECK-B
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible4.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.out -check-prefix=CHECK-BNOT
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/infeasible4.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.out -check-prefix=CHECK-Z
--
Exit Code: 1
Command Output (stdout):
--
$ "/usr/local/bin/clang-3.4" "-I/home/andrea/work/klee-slicing/klee/include" "/home/andrea/work/klee-slicing/klee/test/Slicing/infeasible4.c" "-emit-llvm" "-O0" "-c" "-o" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.bc"
$ "rm" "-rf" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.klee-out"
$ "/home/andrea/work/klee-slicing/klee-build/bin/klee" "--output-dir=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.klee-out" "-search=dfs" "-skip-functions=f,g,h" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.bc"
$ "FileCheck" "/home/andrea/work/klee-slicing/klee/test/Slicing/infeasible4.c" "-input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.out" "-check-prefix=CHECK-PATHS" "-check-prefix=CHECK-STATES" "-check-prefix=CHECK-SLICES" "-check-prefix=CHECK-SNAPSHOTS"
# command stderr:
/home/andrea/work/klee-slicing/klee/test/Slicing/infeasible4.c:11:17: error: expected string not found in input
// CHECK-PATHS: KLEE: done: completed paths = 7
^
/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.out:1:1: note: scanning from here
KLEE: output directory is "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.klee-out"
^
/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/infeasible4.c.tmp.out:51:1: note: possible intended match here
KLEE: done: completed paths = 10
^
error: command failed with exit status: 1
--
********************
FAIL: KLEE :: Slicing/skip-multiple-without-recovery.c (195 of 245)
******************** TEST 'KLEE :: Slicing/skip-multiple-without-recovery.c' FAILED ********************
Script:
--
/usr/local/bin/clang-3.4 -I/home/andrea/work/klee-slicing/klee/include /home/andrea/work/klee-slicing/klee/test/Slicing/skip-multiple-without-recovery.c -emit-llvm -O0 -c -o /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.bc
rm -rf /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.klee-out
/home/andrea/work/klee-slicing/klee-build/bin/klee --output-dir=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.klee-out -search=dfs -skip-functions=f,g /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.bc > /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.out 2>&1
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/skip-multiple-without-recovery.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.out -check-prefix=CHECK-PATHS -check-prefix=CHECK-STATES -check-prefix=CHECK-SLICES -check-prefix=CHECK-SNAPSHOTS
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/skip-multiple-without-recovery.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.out -check-prefix=CHECK-CORRECT
not FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/skip-multiple-without-recovery.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.out -check-prefix=CHECK-INCORRECT
--
Exit Code: 1
Command Output (stdout):
--
$ "/usr/local/bin/clang-3.4" "-I/home/andrea/work/klee-slicing/klee/include" "/home/andrea/work/klee-slicing/klee/test/Slicing/skip-multiple-without-recovery.c" "-emit-llvm" "-O0" "-c" "-o" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.bc"
$ "rm" "-rf" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.klee-out"
$ "/home/andrea/work/klee-slicing/klee-build/bin/klee" "--output-dir=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.klee-out" "-search=dfs" "-skip-functions=f,g" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.bc"
$ "FileCheck" "/home/andrea/work/klee-slicing/klee/test/Slicing/skip-multiple-without-recovery.c" "-input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.out" "-check-prefix=CHECK-PATHS" "-check-prefix=CHECK-STATES" "-check-prefix=CHECK-SLICES" "-check-prefix=CHECK-SNAPSHOTS"
# command stderr:
/home/andrea/work/klee-slicing/klee/test/Slicing/skip-multiple-without-recovery.c:11:18: error: expected string not found in input
// CHECK-STATES: KLEE: done: recovery states = 0
^
/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.out:33:1: note: scanning from here
KLEE: done: generated tests = 1
^
/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-multiple-without-recovery.c.tmp.out:34:1: note: possible intended match here
KLEE: done: recovery states = 3
^
error: command failed with exit status: 1
--
********************
FAIL: KLEE :: Slicing/skip-with-buffer2.c (201 of 245)
******************** TEST 'KLEE :: Slicing/skip-with-buffer2.c' FAILED ********************
Script:
--
/usr/local/bin/clang-3.4 -I/home/andrea/work/klee-slicing/klee/include /home/andrea/work/klee-slicing/klee/test/Slicing/skip-with-buffer2.c -emit-llvm -O0 -c -o /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.bc
rm -rf /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.klee-out
/home/andrea/work/klee-slicing/klee-build/bin/klee --output-dir=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.klee-out -search=dfs -skip-functions=target /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.bc > /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.out 2>&1
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/skip-with-buffer2.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.out -check-prefix=CHECK-PATHS -check-prefix=CHECK-RECOVERY -check-prefix=CHECK-SLICES -check-prefix=CHECK-SNAPSHOTS
--
Exit Code: 1
Command Output (stdout):
--
$ "/usr/local/bin/clang-3.4" "-I/home/andrea/work/klee-slicing/klee/include" "/home/andrea/work/klee-slicing/klee/test/Slicing/skip-with-buffer2.c" "-emit-llvm" "-O0" "-c" "-o" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.bc"
$ "rm" "-rf" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.klee-out"
$ "/home/andrea/work/klee-slicing/klee-build/bin/klee" "--output-dir=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.klee-out" "-search=dfs" "-skip-functions=target" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.bc"
$ "FileCheck" "/home/andrea/work/klee-slicing/klee/test/Slicing/skip-with-buffer2.c" "-input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.out" "-check-prefix=CHECK-PATHS" "-check-prefix=CHECK-RECOVERY" "-check-prefix=CHECK-SLICES" "-check-prefix=CHECK-SNAPSHOTS"
# command stderr:
/home/andrea/work/klee-slicing/klee/test/Slicing/skip-with-buffer2.c:7:20: error: expected string not found in input
// CHECK-RECOVERY: KLEE: done: recovery states = 2
^
/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.out:13:1: note: scanning from here
KLEE: done: generated tests = 1
^
/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer2.c.tmp.out:14:1: note: possible intended match here
KLEE: done: recovery states = 0
^
error: command failed with exit status: 1
--
********************
FAIL: KLEE :: Slicing/skip-with-buffer.c (205 of 245)
******************** TEST 'KLEE :: Slicing/skip-with-buffer.c' FAILED ********************
Script:
--
/usr/local/bin/clang-3.4 -I/home/andrea/work/klee-slicing/klee/include /home/andrea/work/klee-slicing/klee/test/Slicing/skip-with-buffer.c -emit-llvm -O0 -c -o /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.bc
rm -rf /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.klee-out
/home/andrea/work/klee-slicing/klee-build/bin/klee --output-dir=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.klee-out -search=dfs -skip-functions=target /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.bc > /home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.out 2>&1
FileCheck /home/andrea/work/klee-slicing/klee/test/Slicing/skip-with-buffer.c -input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.out -check-prefix=CHECK-PATHS -check-prefix=CHECK-RECOVERY -check-prefix=CHECK-SLICES -check-prefix=CHECK-SNAPSHOTS
--
Exit Code: 1
Command Output (stdout):
--
$ "/usr/local/bin/clang-3.4" "-I/home/andrea/work/klee-slicing/klee/include" "/home/andrea/work/klee-slicing/klee/test/Slicing/skip-with-buffer.c" "-emit-llvm" "-O0" "-c" "-o" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.bc"
$ "rm" "-rf" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.klee-out"
$ "/home/andrea/work/klee-slicing/klee-build/bin/klee" "--output-dir=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.klee-out" "-search=dfs" "-skip-functions=target" "/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.bc"
$ "FileCheck" "/home/andrea/work/klee-slicing/klee/test/Slicing/skip-with-buffer.c" "-input-file=/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.out" "-check-prefix=CHECK-PATHS" "-check-prefix=CHECK-RECOVERY" "-check-prefix=CHECK-SLICES" "-check-prefix=CHECK-SNAPSHOTS"
# command stderr:
/home/andrea/work/klee-slicing/klee/test/Slicing/skip-with-buffer.c:7:20: error: expected string not found in input
// CHECK-RECOVERY: KLEE: done: recovery states = 1
^
/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.out:13:1: note: scanning from here
KLEE: done: generated tests = 1
^
/home/andrea/work/klee-slicing/klee-build/test/Slicing/Output/skip-with-buffer.c.tmp.out:14:1: note: possible intended match here
KLEE: done: recovery states = 0
^
error: command failed with exit status: 1
--
********************
Testing Time: 6.75s
********************
Failing Tests (6):
KLEE :: Slicing/infeasible.c
KLEE :: Slicing/infeasible3.c
KLEE :: Slicing/infeasible4.c
KLEE :: Slicing/skip-multiple-without-recovery.c
KLEE :: Slicing/skip-with-buffer.c
KLEE :: Slicing/skip-with-buffer2.c
Expected Passes : 235
Expected Failures : 2
Unsupported Tests : 2
Unexpected Failures: 6
test/CMakeFiles/systemtests.dir/build.make:59: recipe for target 'test/CMakeFiles/systemtests' failed
make[3]: *** [test/CMakeFiles/systemtests] Error 1
CMakeFiles/Makefile2:897: recipe for target 'test/CMakeFiles/systemtests.dir/all' failed
make[2]: *** [test/CMakeFiles/systemtests.dir/all] Error 2
CMakeFiles/Makefile2:74: recipe for target 'CMakeFiles/check.dir/rule' failed
make[1]: *** [CMakeFiles/check.dir/rule] Error 2
Makefile:162: recipe for target 'check' failed
make: *** [check] Error 2
KLEE crashes on ptx while merging constraints
andrea@ruchill:~/work/klee-slicing/klee-slicing-experiments/coreutils$ make run-cse-ptx
Running KLEE with random-state on program ptx
KLEE: KLEE: WATCHDOG: watching 13288
KLEE: NOTE: Using klee-uclibc : /home/andrea/work/klee-slicing/klee-build/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/andrea/work/klee-slicing/klee-build/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/andrea/work/klee-slicing/klee-slicing-experiments/coreutils/cse-out-ptx"
Using STP solver backend
KLEE: Deterministic memory allocation starting from 0x7ffef66f3000
KLEE: Runnining reachability analysis...
KLEE: Runnining pointer analysis...
KLEE: Runnining mod-ref analysis...
KLEE: Computing slices...
...
klee: /home/andrea/work/klee-slicing/klee/lib/Core/Executor.cpp:4692: void klee::Executor::mergeConstraints(klee::ExecutionState&, klee::ref<klee::Expr>): Assertion `dependentState.isNormalState()' failed.
0 libSlicing.so 0x00002aaaab26b2b2 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1 libSlicing.so 0x00002aaaab26aa24
2 libpthread.so.0 0x00002aaaabaae390
3 libc.so.6 0x00002aaaac590428 gsignal + 56
4 libc.so.6 0x00002aaaac59202a abort + 362
5 libc.so.6 0x00002aaaac588bd7
6 libc.so.6 0x00002aaaac588c82
7 klee 0x0000000000535481 klee::Executor::mergeConstraints(klee::ExecutionState&, klee::ref<klee::Expr>) + 129
8 klee 0x000000000053550b klee::Executor::mergeConstraintsForAll(klee::ExecutionState&, klee::ref<klee::Expr>) + 107
9 klee 0x0000000000542242 klee::Executor::branch(klee::ExecutionState&, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> >&) + 2274
10 klee 0x000000000054a84a klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 17338
11 klee 0x000000000054c457 klee::Executor::run(klee::ExecutionState&) + 1927
12 klee 0x000000000054ccbd klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1901
13 klee 0x0000000000516ec6 main + 12998
14 libc.so.6 0x00002aaaac57b830 __libc_start_main + 240
15 klee 0x0000000000527329 _start + 41Slicer can't find slicing criterion in some cases
In some cases, the slicer can't find the given criterion function.
This happens because the reachable functions (from a given skipped function) computed by the our analysis is different from the reachable functions computed by the slicer. As a result, our static analysis annotates a store instruction in a function which is not reachable according to the slicer.
Possible solution: We can use in the slicer the reachable functions computed by our analysis (but before doing this, we might want to make our analysis more precise).
KLEE crashes on Coreutils / dwarfdump
KLEE consistently crashes when run on Coreutils while looking for StoreInst:
andrea@ruchill:~/work/klee-slicing/klee-slicing-experiments/coreutils$ /home/andrea/work/klee-slicing/klee-build/bin/klee --stats-write-interval=1500 --istats-write-interval=1500 --simplify-sym-indices --output-module --max-memory=4095 --allocate-determ=true --allocate-determ-size=4095 --allocate-determ-start-address=0x7ffef66f3000 --max-sym-array-size=4096 --disable-inlining --use-forked-solver --use-cex-cache --libc=uclibc --posix-runtime --allow-external-sym-calls --only-output-states-covering-new --watchdog --max-memory-inhibit=false --max-static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal --dump-states-on-halt=false --environ=/tmp/test.env --run-in=/tmp/sandbox --max-instruction-time=200. --max-solver-time=200. --max-time=4000. --search=random-state --exit-on-error-type=Ptr --skip-functions=usage /home/andrea/work/klee-slicing/klee-slicing-experiments/coreutils/coreutils-6.10/obj-llvm/src/seq.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout
KLEE: KLEE: WATCHDOG: watching 17942
KLEE: NOTE: Using klee-uclibc : /home/andrea/work/klee-slicing/klee-build/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/andrea/work/klee-slicing/klee-build/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/andrea/work/klee-slicing/klee-slicing-experiments/coreutils/coreutils-6.10/obj-llvm/src/klee-out-5"
Using STP solver backend
KLEE: Deterministic memory allocation starting from 0x7ffef66f3000
KLEE: Runnining reachability analysis...
KLEE: Runnining pointer analysis...
KLEE: Runnining mod-ref analysis...
KLEE: Computing slices...
KLEE: WARNING: undefined reference to function: __crit_100_0
[...]
KLEE: WARNING: undefined reference to function: __crit_9_1
KLEE: WARNING: undefined reference to function: __ctype_b_loc
KLEE: WARNING: undefined reference to function: freelocale
KLEE: WARNING: undefined reference to function: newlocale
KLEE: WARNING: undefined reference to function: strtold_l
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 140733032923104)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: calling external: newlocale(8127, 140733032908096, 0)
KLEE: WARNING ONCE: calling external: strtold_l(140733032932552, 140733032962168, 46912528022368)
KLEE: WARNING ONCE: calling external: freelocale(46912528022368)
KLEE: WARNING ONCE: calling external: vprintf(140733032911768, 140733032989456)
/home/andrea/work/klee-slicing/klee-slicing-experiments/coreutils/coreutils-6.10/obj-llvm/src/seq.bc: invalid option --
/home/andrea/work/klee-slicing/klee-slicing-experiments/coreutils/coreutils-6.10/obj-llvm/src/seq.bc: option requires an argument --
/home/andrea/work/klee-slicing/klee-slicing-experiments/coreutils/coreutils-6.10/obj-llvm/src/seq.bc: invalid option --
/home/andrea/work/klee-slicing/klee-slicing-experiments/coreutils/coreutils-6.10/obj-llvm/src/seq.bc: option requires an argument --
/home/andrea/work/klee-slicing/klee-slicing-experiments/coreutils/coreutils-6.10/obj-llvm/src/seq.bc: invalid option --
/home/andrea/work/klee-slicing/klee-slicing-experiments/coreutils/coreutils-6.10/obj-llvm/src/seq.bc: invalid option --
INFO: Points-to analysis took 0 sec 0 ms
Had no PTA node %229 = load i64 (%struct.__STDIO_FILE_STRUCT.286*, i64, i64, i64)** %fp_outfunc.addr, align 8, !dbg !2868
klee: /home/andrea/work/klee-slicing/dg/src/llvm/analysis/ReachingDefinitions/ReachingDefinitions.cpp:305: dg::analysis::rd::RDNode* dg::analysis::rd::LLVMRDBuilder::createStore(const llvm::Instruction*): Assertion `pts && "Don't have the points-to information for store"' failed.
0 libSlicing.so 0x00002aaaab266302 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1 libSlicing.so 0x00002aaaab265a74
2 libpthread.so.0 0x00002aaaabaa8390
3 libc.so.6 0x00002aaaac58a428 gsignal + 56
4 libc.so.6 0x00002aaaac58c02a abort + 362
5 libc.so.6 0x00002aaaac582bd7
6 libc.so.6 0x00002aaaac582c82
7 libLLVMdg.so 0x00002aaaad03f327 dg::analysis::rd::LLVMRDBuilder::createStore(llvm::Instruction const*) + 187
8 libLLVMdg.so 0x00002aaaad03f9c0 dg::analysis::rd::LLVMRDBuilder::buildBlock(llvm::BasicBlock const&) + 542
9 libLLVMdg.so 0x00002aaaad03ff1b dg::analysis::rd::LLVMRDBuilder::buildFunction(llvm::Function const&) + 351
10 libLLVMdg.so 0x00002aaaad04118b dg::analysis::rd::LLVMRDBuilder::build() + 151
11 libSlicing.so 0x00002aaaaaf05df4 dg::analysis::rd::LLVMReachingDefinitions::run() + 48
12 libSlicing.so 0x00002aaaaaf00486 Slicer::computeEdges() + 202
13 libSlicing.so 0x00002aaaaaf001cf Slicer::mark() + 503
14 libSlicing.so 0x00002aaaaaeffe81 Slicer::run() + 149
15 libSlicing.so 0x00002aaaaaf3229d SliceGenerator::generateSlice(llvm::Function*, unsigned int, ModRefAnalysis::SideEffectType) + 805
16 klee 0x000000000053cf6c klee::Executor::getSlice(llvm::Function*, unsigned int, ModRefAnalysis::SideEffectType) + 108
17 klee 0x0000000000544571 klee::Executor::executeCall(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 753
18 klee 0x000000000054961a klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 14874
19 klee 0x000000000054bbc7 klee::Executor::run(klee::ExecutionState&) + 1927
20 klee 0x000000000054c42d klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1901
21 klee 0x0000000000516ab6 main + 12998
22 libc.so.6 0x00002aaaac575830 __libc_start_main + 240
23 klee 0x0000000000526f29 _start + 41
KLEE: WARNING: KLEE: watchdog exiting (no child)There's something fundamentally wrong in how we compute the mod/ref set.
KLEE crashes due to not empty parent in PTree
KLEE: halting execution, dumping remaining states
klee: /home/andrea/work/klee-slicing/klee/lib/Core/PTree.cpp:37: void klee::PTree::remove(klee::PTree::Node*): Assertion `!n->left && !n->right' failed.
0 libSlicing.so 0x00002aaaab26b2b2 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1 libSlicing.so 0x00002aaaab26aa24
2 libpthread.so.0 0x00002aaaabaae390
3 libc.so.6 0x00002aaaac590428 gsignal + 56
4 libc.so.6 0x00002aaaac59202a abort + 362
5 libc.so.6 0x00002aaaac588bd7
6 libc.so.6 0x00002aaaac588c82
7 klee 0x0000000000560649
8 klee 0x000000000053b4e7 klee::Executor::updateStates(klee::ExecutionState*) + 967
9 klee 0x000000000053b691 klee::Executor::doDumpStates() + 193
10 klee 0x000000000054c1e0 klee::Executor::run(klee::ExecutionState&) + 1744
11 klee 0x000000000054cb2d klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1949
12 klee 0x0000000000516f86 main + 13206
13 libc.so.6 0x00002aaaac57b830 __libc_start_main + 240
14 klee 0x0000000000527399 _start + 41
onNormalStateWrite wrongly assumes that the size should be multiple of 8
For example, boolean size is not multiple of 8 since it is 1.
Unknown command line argument '-skip-functions=f'.
I have followed the commands to install SVF, DG and KLEE. But when I have tried the example, I am getting the following problem.
Unknown command line argument '-skip-functions=f'.
"failed external call" on bc and --posix-runtime
Running Chopper on the bc benchmark without any skip instructions yields:
$ kleegacy -libc=uclibc -simplify-sym-indices -search=nurs:covnew -split-search -output-module bc.bc
...
KLEE: WARNING ONCE: calling external: __syscall_rt_sigaction(2, 94287618746464, 94287622407168, 8)
KLEE: ERROR: /home/ubuntu/code/klee-uclibc/libc/signal/sigaction.c:58: failed external call: __syscall_rt_sigaction
KLEE: NOTE: now ignoring this error at this locationWhen I add --posix-runtime, the error disappears (--allow-external-sym-calls does not seem to help). What KLEE says about --posix-runtime is:
-posix-runtime - Link with POSIX runtime. Options that can be passed as arguments to the programs are: --sym-arg <max-len> --sym-args <min-argvs> <max-argvs> <max-len> + file model options
What happens?
KLEE Crash in libtasn1 (CVE-2015-3622)
We have a SEGFAULT when running the experiment for CVE-2015-3622.
Here is the log:
log.txt
It seems that it crashes when it tries to dump the assembly.ll file.
I ran it with ASAN, it seems that there is a use after free in our pass,
but I am not sure if this is the reason for the crash.
ReturningToVoidPass crashes when code is compiled with optimizations
For example, add -O1 or -O2 to overriding-store-non-void2.c to observe the phenomenon.
KLEE leads to memory exhaustion on Coreutils tac
/home/andrea/work/klee-slicing/klee-build/bin/klee --stats-write-interval=1500
--istats-write-interval=1500 --simplify-sym-indices --output-module --max-memory=4095
--allocate-determ=true --allocate-determ-size=4095 --allocate-determ-start-address=0x7ffef66f3000
--max-sym-array-size=4096 --disable-inlining --use-forked-solver --use-cex-cache --libc=uclibc
--posix-runtime --allow-external-sym-calls --only-output-states-covering-new --max-memory-inhibit=false
--max-static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal
--dump-states-on-halt=false --environ=/tmp/test.env --run-in=/tmp/sandbox --max-instruction-time=200.
--max-solver-time=200. --max-time=4000. --exit-on-error-type=Ptr --search=random-state
-skip-functions=usage,getopt_long tac.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8
--sym-stdin 8 --sym-stdoutQuickly leads to memory exhaustion during Snapshot creation:
Program received signal SIGINT, Interrupt.
klee::Snapshot::Snapshot (this=<optimized out>) at /home/andrea/work/klee-slicing/klee/include/klee/ExecutionState.h:100
100 struct Snapshot {
(gdb) bt
#0 klee::Snapshot::Snapshot (this=<optimized out>) at /home/andrea/work/klee-slicing/klee/include/klee/ExecutionState.h:100
#1 std::_Construct<klee::Snapshot, klee::Snapshot const&> (__p=<optimized out>) at /usr/include/c++/5/bits/stl_construct.h:75
#2 std::__uninitialized_copy<false>::__uninit_copy<__gnu_cxx::__normal_iterator<klee::Snapshot const*, std::vector<klee::Snapshot, std::allocator<klee::Snapshot> > >, klee::Snapshot*> (__result=<optimized out>, __last=...,
__first=...) at /usr/include/c++/5/bits/stl_uninitialized.h:75
#3 std::uninitialized_copy<__gnu_cxx::__normal_iterator<klee::Snapshot const*, std::vector<klee::Snapshot, std::allocator<klee::Snapshot> > >, klee::Snapshot*> (__result=<optimized out>, __last=..., __first=...)
at /usr/include/c++/5/bits/stl_uninitialized.h:126
#4 std::__uninitialized_copy_a<__gnu_cxx::__normal_iterator<klee::Snapshot const*, std::vector<klee::Snapshot, std::allocator<klee::Snapshot> > >, klee::Snapshot*, klee::Snapshot> (__result=<optimized out>, __last=...,
__first=...) at /usr/include/c++/5/bits/stl_uninitialized.h:281
#5 std::vector<klee::Snapshot, std::allocator<klee::Snapshot> >::vector (__x=std::vector of length 11407, capacity 16384 = {...}, this=0x213aa5c70) at /usr/include/c++/5/bits/stl_vector.h:322
#6 klee::ExecutionState::ExecutionState (this=0x213aa5c30, state=...) at /home/andrea/work/klee-slicing/klee/lib/Core/ExecutionState.cpp:162
#7 0x00000000005329f1 in klee::Executor::createSnapshotState (this=this@entry=0x3338cb0, state=...) at /home/andrea/work/klee-slicing/klee/lib/Core/Executor.cpp:4814
#8 0x00000000005449ea in klee::Executor::executeCall (this=this@entry=0x3338cb0, state=..., ki=ki@entry=0xe922fc0, f=f@entry=0x1449e60, arguments=std::vector of length 1, capacity 1 = {...})
at /home/andrea/work/klee-slicing/klee/lib/Core/Executor.cpp:1447
#9 0x000000000054961a in klee::Executor::executeInstruction (this=this@entry=0x3338cb0, state=..., ki=ki@entry=0xe922fc0) at /home/andrea/work/klee-slicing/klee/lib/Core/Executor.cpp:1989
#10 0x000000000054bbc7 in klee::Executor::run (this=this@entry=0x3338cb0, initialState=...) at /home/andrea/work/klee-slicing/klee/lib/Core/Executor.cpp:2979
#11 0x000000000054c42d in klee::Executor::runFunctionAsMain (this=0x3338cb0, f=0x23b3b00, argc=15, argv=0x2161800, envp=0x268bc40) at /home/andrea/work/klee-slicing/klee/lib/Core/Executor.cpp:3821
#12 0x0000000000516ab6 in main (argc=<optimized out>, argv=<optimized out>, envp=<optimized out>) at /home/andrea/work/klee-slicing/klee/tools/klee/main.cpp:1630
"Bad signature" LLVM assert raised when replacing calls with wrappers
I have had this LLVM assert raised on the bc benchmark on several functions, on several functions, such as prog_char and some floating point functions. I get different errors, sometimes the arguments count is bad, sometimes it's the argument type.
Possibly this is related to structs (my best guess).
Minimal steps to reproduce it on a smaller program:
- Write
main.c:
int main(int argc, char *argv[]) {
_fp_out_narrow(0, 0, 0, 0);
return 0;
}(I was not able to isolate the part of __fp_out_narrow that causes this, so this minimal example is not very well self-contained)
- Run
clang(+opt -mem2reg file.bc -o file.bc)
$ clang -c -g -emit-llvm main.c -o main.bc -I~/code/chopper/include/
main.c:3:5: warning: implicit declaration of function '_fp_out_narrow' is invalid in C99 [-Wimplicit-function-declaration]
_fp_out_narrow(0, 0, 0, 0);
^
1 warning generated.- Run legacy Chopper, skip
_fp_out_narrow1:
$ kleegacy -libc=uclibc -simplify-sym-indices -search=nurs:covnew -split-search -output-module -skip-functions=_fp_out_narrow1 main.bc
KLEE: NOTE: Using klee-uclibc : /home/ubuntu/code/chopper/legacy_build/Release+Asserts/lib/klee-uclibc.bca
kleegacy: /home/ubuntu/code/llvm-project/llvm/lib/IR/Instructions.cpp:281: void llvm::CallInst::init(llvm::Value*, llvm::ArrayRef<llvm::Value*>, const llvm::Twine&): Assertion `(i >= FTy->getNumParams() || FTy->getParamType(i) == Args[i]->getType()) && "Calling a function with a bad signature!"' failed.
0 kleegacy 0x0000555731055992 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1 kleegacy 0x000055573105528c
2 libpthread.so.0 0x00007f9e9c453890
3 libc.so.6 0x00007f9e9b321e97 gsignal + 199
4 libc.so.6 0x00007f9e9b323801 abort + 321
5 libc.so.6 0x00007f9e9b31339a
6 libc.so.6 0x00007f9e9b313412
7 kleegacy 0x0000555730fc5a3f llvm::CallInst::init(llvm::Value*, llvm::ArrayRef<llvm::Value*>, llvm::Twine const&) + 335
8 kleegacy 0x000055573059c999
9 kleegacy 0x000055573059c688
10 kleegacy 0x000055573068457a
11 kleegacy 0x0000555730683afa klee::ReturnToVoidFunctionPass::replaceCall(llvm::CallInst*, llvm::Function*, llvm::Function*) + 812
12 kleegacy 0x0000555730683712 klee::ReturnToVoidFunctionPass::replaceCalls(llvm::Function*, llvm::Function*, std::vector<unsigned int, std::allocator<unsigned int> > const&) + 480
13 kleegacy 0x0000555730682fcd klee::ReturnToVoidFunctionPass::runOnFunction(llvm::Function&, llvm::Module&) + 469
14 kleegacy 0x0000555730683d18 klee::ReturnToVoidFunctionPass::runOnModule(llvm::Module&) + 138
15 kleegacy 0x0000555730fdcef1 llvm::legacy::PassManagerImpl::run(llvm::Module&) + 849
16 kleegacy 0x000055573066b3c9 klee::KModule::prepare(klee::Interpreter::ModuleOptions const&, std::vector<klee::Interpreter::SkippedFunctionOption, std::allocator<klee::Interpreter::SkippedFunctionOption> > const&, klee::InterpreterHandler*, ReachabilityAnalysis*, Inliner*, AAPass*, ModRefAnalysis*, Cloner*, SliceGenerator*) + 1659
17 kleegacy 0x00005557305b3640 klee::Executor::setModule(llvm::Module*, klee::Interpreter::ModuleOptions const&) + 1656
18 kleegacy 0x0000555730596b35 main + 4654
19 libc.so.6 0x00007f9e9b304b97 __libc_start_main + 231
20 kleegacy 0x000055573059071a _start + 42
Aborted (core dumped)3bis. You can also directly reproduce it on bc by skipping prog_char:
$ kleegacy -libc=uclibc -simplify-sym-indices -search=nurs:covnew -split-search -output-module -skip-functions=prog_char bc.bc
KLEE: NOTE: Using klee-uclibc : /home/ubuntu/code/chopper/legacy_build/Release+Asserts/lib/klee-uclibc.bca
KLEE: output directory is "/home/ubuntu/code/chopper-experiments/bc/klee-out-24"
Using STP solver backend
kleegacy: /home/ubuntu/code/llvm-project/llvm/lib/IR/Instructions.cpp:276: void llvm::CallInst::init(llvm::Value*, llvm::ArrayRef<llvm::Value*>, const llvm::Twine&): Assertion `(Args.size() == FTy->getNumParams() || (FTy->isVarArg() && Args.size() > FTy->getNumParams())) && "Calling a function with bad signature!"' failed.Dodging the issue
I was not able to fix the issue, and instead I dodged it by aborting the replaceCalls. The ugly workaround is jordr@6feb19d and yields:
[4941c8] KLEE: WARNING: Wrapper has bad signature: 'prog_char'! LLVM refuses to create call. Args.size()=3, FTy->getNumParams()=1, FTY->isVarArg()=0
[4941c8] KLEE: WARNING: Wrapper has bad signature: 'input_char'! LLVM refuses to create call. Args.size()=3, FTy->getNumParams()=1, FTY->isVarArg()=0
[eab1d] KLEE: WARNING: Wrapper has bad signature: '_fp_out_narrow'! bad type of Args[2].type=4 =/= wrapper.type=10 LLVM refuses to create call.Some debugging
Sometimes the mismatch happens on the type of the arguments, sometimes on the count of arguments.
prog_char
Using a modified Chopper, I get:
$ klee -libc=uclibc -simplify-sym-indices -search=nurs:covnew -split-search -skip-functions-not=__errno_location,__h_errno_location,__user_main bc.bc
[988dcb] KLEE: createWrapperFunction(f=prog_char)
[a17b2a] KLEE: WARNING: [createWrapperFunction] Set the arguments
[596ea7] KLEE: WARNING: !!
[6b00f9] KLEE: WARNING: [createWrapperFunction] Create BB entry
[e1f7eb] KLEE: WARNING: replaceCall to call, arg[0]= (2 args) by f=prog_char
[69a30f] KLEE: WARNING: - originalCall.argoperand[0] =
; Function Attrs: nounwind uwtable
define zeroext i8 @prog_char() #0 {
entry:
tail call void @llvm.dbg.value(metadata !3258, i64 0, metadata !3259), !dbg !3261
%0 = load i32* getelementptr inbounds (%struct.program_counter* @pc, i64 0, i32 1), align 4, !dbg !3262, !tbaa !3263
%inc.i = add nsw i32 %0, 1, !dbg !3262
store i32 %inc.i, i32* getelementptr inbounds (%struct.program_counter* @pc, i64 0, i32 1), align 4, !dbg !3262, !tbaa !3263
%idxprom.i = sext i32 %0 to i64, !dbg !3262
%1 = load i32* getelementptr inbounds (%struct.program_counter* @pc, i64 0, i32 0), align 4, !dbg !3262, !tbaa !3268
%idxprom1.i = sext i32 %1 to i64, !dbg !3262
%2 = load %struct.bc_function** @functions, align 8, !dbg !3262, !tbaa !3269
%f_body.i = getelementptr inbounds %struct.bc_function* %2, i64 %idxprom1.i, i32 1, !dbg !3262
%3 = load i8** %f_body.i, align 8, !dbg !3262, !tbaa !3271
%arrayidx2.i = getelementptr inbounds i8* %3, i64 %idxprom.i, !dbg !3262
%4 = load i8* %arrayidx2.i, align 1, !dbg !3262, !tbaa !3273
ret i8 %4, !dbg !3260
}
(TYPE=i8 ()*)(TID=14)
[69a30f] KLEE: WARNING: - originalCall.argoperand[1] = %const_base.0 = load i32* %const_base.0.in, align 4, !dbg !3362(TYPE=i32)(TID=10)
[21c4f4] KLEE: WARNING: CreateCall! wrapper=__wrap_prog_char, origCallInst->getNumArgOperands()=2,
[1780fd] KLEE: WARNING: getNumParams of wrapper= 1, type = 14
[510366] KLEE: WARNING: f.CONV:0, wrapper.CONV:0
[f81146] KLEE: WARNING: Wrapper has bad signature! LLVM refuses to create call.
[6c15e4] KLEE: WARNING: Failed to replace call to f=prog_char_fp_out_narrow
With the minimal example from above, I get:
$ klee -libc=uclibc -simplify-sym-indices -search=nurs:covnew -split-search -skip-functions-not=__errno_location,__h_errno_location,__user_main,prog_char,input_char bc.bc
[988dcb] KLEE: createWrapperFunction(f=_fp_out_narrow)
[a17b2a] KLEE: WARNING: [createWrapperFunction] Set the arguments
[6b00f9] KLEE: WARNING: [createWrapperFunction] Create BB entry
[e1f7eb] KLEE: WARNING: replaceCall to call, arg[0]= (4 args) by f=_fp_out_narrow
[69a30f] KLEE: WARNING: - originalCall.argoperand[0] = %struct.__STDIO_FILE_STRUCT.215* %stream(TYPE=%struct.__STDIO_FILE_STRUCT.215*)(TID=14)
[69a30f] KLEE: WARNING: - originalCall.argoperand[1] = %cond194 = phi x86_fp80 [ %42, %cond.true188 ], [ %conv192, %cond.false190 ], !dbg !3435(TYPE=x86_fp80)(TID=4)
[69a30f] KLEE: WARNING: - originalCall.argoperand[2] = %info195 = getelementptr inbounds %struct.ppfs_t* %ppfs, i32 0, i32 1, !dbg !3435(TYPE=%struct.printf_info.315*)(TID=14)
[69a30f] KLEE: WARNING: - originalCall.argoperand[3] =
; Function Attrs: nounwind uwtable
define internal i64 @_fp_out_narrow(%struct.__STDIO_FILE_STRUCT.215* %fp, i64 %type, i64 %len, i64 %buf) #10 {
entry:
call void @llvm.dbg.value(metadata !{%struct.__STDIO_FILE_STRUCT.215* %fp}, i64 0, metadata !3258), !dbg !3259
call void @llvm.dbg.value(metadata !{i64 %type}, i64 0, metadata !3260), !dbg !3259
call void @llvm.dbg.value(metadata !{i64 %len}, i64 0, metadata !3261), !dbg !3259
call void @llvm.dbg.value(metadata !{i64 %buf}, i64 0, metadata !3262), !dbg !3259
call void @llvm.dbg.value(metadata !3263, i64 0, metadata !3264), !dbg !3265
%and = and i64 %type, 128, !dbg !3266
%tobool = icmp ne i64 %and, 0, !dbg !3266
br i1 %tobool, label %if.then, label %if.end12, !dbg !3266
if.then: ; preds = %entry
%0 = inttoptr i64 %buf to i8*, !dbg !3268
%call = call i64 @strlen(i8* %0) #17, !dbg !3268
%conv = trunc i64 %call to i32, !dbg !3268
call void @llvm.dbg.value(metadata !{i32 %conv}, i64 0, metadata !3270), !dbg !3268
%conv1 = sext i32 %conv to i64, !dbg !3271
%sub = sub nsw i64 %len, %conv1, !dbg !3271
call void @llvm.dbg.value(metadata !{i64 %sub}, i64 0, metadata !3261), !dbg !3271
%cmp = icmp sgt i64 %sub, 0, !dbg !3271
br i1 %cmp, label %if.then3, label %if.end10, !dbg !3271
if.then3: ; preds = %if.then
%and4 = and i64 %type, 127, !dbg !3273
%conv5 = trunc i64 %and4 to i32, !dbg !3273
%1 = alloca i64, !dbg !3273
call void @__wrap__charpad(i64* %1, %struct.__STDIO_FILE_STRUCT.215* %fp, i32 %conv5, i64 %sub), !dbg !3273
%2 = load i64* %1, !dbg !3273
call void @llvm.dbg.value(metadata !{i64 %2}, i64 0, metadata !3264), !dbg !3273
%cmp7 = icmp ne i64 %2, %sub, !dbg !3273
br i1 %cmp7, label %if.then9, label %if.end, !dbg !3273
if.then9: ; preds = %if.then3
br label %return, !dbg !3276
if.end: ; preds = %if.then3
br label %if.end10, !dbg !3278
if.end10: ; preds = %if.end, %if.then
%r.0 = phi i64 [ %2, %if.end ], [ 0, %if.then ]
%conv11 = sext i32 %conv to i64, !dbg !3279
call void @llvm.dbg.value(metadata !{i64 %conv11}, i64 0, metadata !3261), !dbg !3279
br label %if.end12, !dbg !3280
if.end12: ; preds = %if.end10, %entry
%len.addr.0 = phi i64 [ %conv11, %if.end10 ], [ %len, %entry ]
%r.1 = phi i64 [ %r.0, %if.end10 ], [ 0, %entry ]
%cmp13 = icmp sgt i64 %len.addr.0, 0, !dbg !3281
br i1 %cmp13, label %cond.true, label %cond.false, !dbg !3281
cond.true: ; preds = %if.end12
%3 = inttoptr i64 %buf to i8*, !dbg !3281
%call15 = call i64 @__stdio_fwrite(i8* %3, i64 %len.addr.0, %struct.__STDIO_FILE_STRUCT.215* %fp) #18, !dbg !3281
br label %cond.end, !dbg !3281
cond.false: ; preds = %if.end12
br label %cond.end, !dbg !3281
cond.end: ; preds = %cond.false, %cond.true
%cond = phi i64 [ %call15, %cond.true ], [ 0, %cond.false ], !dbg !3281
%add = add i64 %r.1, %cond, !dbg !3281
br label %return, !dbg !3281
return: ; preds = %cond.end, %if.then9
%retval.0 = phi i64 [ %2, %if.then9 ], [ %add, %cond.end ]
ret i64 %retval.0, !dbg !3282
}
(TYPE=i64 (%struct.__STDIO_FILE_STRUCT.215*, i64, i64, i64)*)(TID=14)
[21c4f4] KLEE: WARNING: CreateCall! wrapper=__wrap__fp_out_narrow, origCallInst->getNumArgOperands()=4,
[1780fd] KLEE: WARNING: getNumParams of wrapper= 5, type = 14
[510366] KLEE: WARNING: f.CONV:0, wrapper.CONV:0
[4322c4] KLEE: WARNING: Wrapper has bad signature! bad type of Args[2].type=4 =/= wrapper.type=10 LLVM refuses to create call.
[6c15e4] KLEE: WARNING: Failed to replace call to f=_fp_out_narrowThe mismatch happens on the type:
[4322c4] KLEE: WARNING: Wrapper has bad signature! bad type of Args[2].type=4 =/= wrapper.type=10 LLVM refuses to create call.
According to llvm/IR/type.h, 4 and 10 are:
X86_FP80TyID, ///< 4: 80-bit floating point type (X87)
/* ... */
IntegerTyID, ///< 10: Arbitrary bit width integersDo you have any clue about this?
RetToVoid Pass
For example:
int foo(int x) {
return x + 1;
}
int main() {
int k;
klee_make_symbolic(&k, sizeof(k), "k");
int r = foo(7);
if (k) {
printf("%d\n", r);
} else {
printf("\n");
}
}In this case, we expect to have a recovery state only in one path,
but the recovery state is created before the branch.
When looking at the assembly,
the blocking load instruction appears after the call to __wrap_foo (and before the branch).
I think that the compiler will always generate the code in such way.
We probably need to move the load before every use?
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.