search

tracer-x / TracerX

TracerX Symbolic Virtual Machine
https://tracer-x.github.io/
Other
31 stars 11 forks source link

Crash on klee-examples/basic/pointer_struct4.c #393

Closed rasoolmaghareh closed 11 months ago

rasoolmaghareh commented 1 year ago

This is the output that I am seeing:

clang -emit-llvm -g -I/home/issta21-322/TracerX/tracerx/Release+Asserts/include -I/home/issta21-322/TracerX/tracerx/Release+Asserts/../include -Wno-int-conversion -c pointer_struct4.c
SOLVER_FLAGS="-solver-backend=z3" OUTPUT_DIR=pointer_struct4.tx make pointer_struct4.klee-out
make[1]: Entering directory '/home/issta21-322/TracerX-examples/basic'
KLEE: output directory is "/home/issta21-322/TracerX-examples/basic/pointer_struct4.tx"
Using Z3 solver backend
KLEE: Logging all queries in .pc format to /home/issta21-322/TracerX-examples/basic/pointer_struct4.tx/all-queries.pc

KLEE: Logging all queries in .smt2 format to /home/issta21-322/TracerX-examples/basic/pointer_struct4.tx/all-queries.smt2

KLEE: Deterministic memory allocation starting from 0x7ff30000000
klee: TxWP.cpp:1193: klee::ref<klee::Expr> klee::TxWeakestPreCondition::getCallInst(llvm::CallInst*): Assertion `ret && "Return instruction is null!"' failed.
0  klee            0x0000000000e983e2 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  klee            0x0000000000e97c34
2  libpthread.so.0 0x00007f28b0a69390
3  libc.so.6       0x00007f28ae226438 gsignal + 56
4  libc.so.6       0x00007f28ae22803a abort + 362
5  libc.so.6       0x00007f28ae21ebe7
6  libc.so.6       0x00007f28ae21ec92
7  klee            0x00000000005dd326 klee::TxWeakestPreCondition::getCallInst(llvm::CallInst*) + 294
8  klee            0x00000000005db8d5 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 933
9  klee            0x00000000005dcb27 klee::TxWeakestPreCondition::getCastInst(llvm::CastInst*) + 87
10 klee            0x00000000005db873 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 835
11 klee            0x00000000005dd93f klee::TxWeakestPreCondition::PushUp(std::vector<std::pair<klee::KInstruction*, int>, std::allocator<std::pair<klee::KInstruction*, int> > >) + 319
12 klee            0x00000000005b7cd8 klee::TxTreeNode::generateWPInterpolant() + 1032
13 klee            0x00000000005be5eb klee::TxSubsumptionTableEntry::TxSubsumptionTableEntry(klee::TxTreeNode*, std::vector<llvm::Instruction*, std::allocator<llvm::Instruction*> > const&) + 1163
14 klee            0x00000000005be96b klee::TxTree::remove(klee::ExecutionState*, klee::TimingSolver*, bool) + 779
15 klee            0x000000000054a3b1 klee::Executor::updateStates(klee::ExecutionState*) + 513
16 klee            0x000000000056142e klee::Executor::run(klee::ExecutionState&) + 5982
17 klee            0x0000000000561f59 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1705
18 klee            0x000000000052825d main + 10365
19 libc.so.6       0x00007f28ae211840 __libc_start_main + 240
20 klee            0x000000000053bb69 _start + 41
Command terminated by signal 6
0.03user 0.01system 0:00.28elapsed 14%CPU (0avgtext+0avgdata 25820maxresident)k
0inputs+144outputs (0major+1526minor)pagefaults 0swaps
make[2]: Entering directory '/home/issta21-322/TracerX-examples/basic'
warning: ignoring debug info with an invalid version (1) in pointer_struct4.bc
Writing 'cfg.main.dot'...
Printing analysis 'Print CFG of function to 'dot' file' for function 'main':
---------------------------------------------------------------------------------
|       Path       |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
---------------------------------------------------------------------------------
|pointer_struct4.tx|       0|     0.00|     0.00|     0.00|     314|        0.00|
---------------------------------------------------------------------------------
make[2]: Leaving directory '/home/issta21-322/TracerX-examples/basic'
make[1]: Leaving directory '/home/issta21-322/TracerX-examples/basic'
grep: pointer_struct4.tx/tree.dot: No such file or directory
for KTEST in pointer_struct4.tx/*.ktest ; do \
ArpitaDutta commented 1 year ago

This program is facing the same issue as Issue #378 Crash on klee-examples/basic/pointer_struct7.c with WP

Unable to return the callInst to TxWeakestPreCondition::generateExprFromOperand() for the following instruction %8 = call noalias i8* @malloc(i64 16) #6, !dbg !133

rasoolmaghareh commented 1 year ago

We need more discussion on these two programs.

ArpitaDutta commented 1 year ago

Yes.

Here is the log of this program.

KLEE: Subsumption check for Node #1, Program Point 43130904
KLEE: #1: Check failure due to control point not found in table
KLEE: Storing entry for Node #1, Program Point 43130904
Current Pushup Instruction: ret i32 %32, !dbg !142
Current Pushup Instruction: %32 = sext i8 %31 to i32, !dbg !142
Current Pushup Instruction: %31 = load i8* %30, align 1, !dbg !142
Current Pushup Instruction:  %30 = getelementptr inbounds %struct.Node* %29, i32 0, i32 0, !dbg !142
Current Pushup Instruction: %29 = load %struct.Node** %q, align 8, !dbg !142
Current Pushup Instruction: br i1 %6, label %7, label %28, !dbg !131
Current Pushup Instruction: %6 = icmp slt i32 %5, 2, !dbg !131
Current Pushup Instruction: %5 = load i32* %i, align 4, !dbg !131
Current Pushup Instruction: br label %4, !dbg !131
Current Pushup Instruction: store i32 %27, i32* %i, align 4, !dbg !131
Current Pushup Instruction:  %27 = add nsw i32 %26, 1, !dbg !131
Current Pushup Instruction: %26 = load i32* %i, align 4, !dbg !131
Current Pushup Instruction: br label %25, !dbg !141
Current Pushup Instruction: store %struct.Node* %24, %struct.Node** %p, align 8, !dbg !140
Current Pushup Instruction: %24 = load %struct.Node** %new_node, align 8, !dbg !140
Current Pushup Instruction: br i1 %20, label %21, label %23, !dbg !137
Current Pushup Instruction: %20 = icmp eq %struct.Node* %19, null, !dbg !137
Current Pushup Instruction: %19 = load %struct.Node** %p, align 8, !dbg !137
Current Pushup Instruction: store %struct.Node* %16, %struct.Node** %18, align 8, !dbg !136
Current Pushup Instruction:  %18 = getelementptr inbounds %struct.Node* %17, i32 0, i32 1, !dbg !136
Current Pushup Instruction: %17 = load %struct.Node** %new_node, align 8, !dbg !136
Current Pushup Instruction: %16 = load %struct.Node** %p, align 8, !dbg !136
Current Pushup Instruction: store i8 %13, i8* %15, align 1, !dbg !135
Current Pushup Instruction: %15 = getelementptr inbounds %struct.Node* %14, i32 0, i32 0, !dbg !135
Current Pushup Instruction:  %14 = load %struct.Node** %new_node, align 8, !dbg !135
Current Pushup Instruction: %13 = trunc i32 %12 to i8, !dbg !135
Current Pushup Instruction: %12 = add nsw i32 %11, 96, !dbg !135
Current Pushup Instruction: %11 = sub nsw i32 2, %10, !dbg !135
Current Pushup Instruction: %10 = load i32* %i, align 4, !dbg !135
Current Pushup Instruction: store %struct.Node* %9, %struct.Node** %new_node, align 8, !dbg !133
Current Pushup Instruction:  %9 = bitcast i8* %8 to %struct.Node*, !dbg !133
Current Pushup Instruction: %8 = call noalias i8* @malloc(i64 16) #6, !dbg !133
Current Pushup Instruction: br i1 %6, label %7, label %28, !dbg !131
Current Pushup Instruction: %6 = icmp slt i32 %5, 2, !dbg !131
Current Pushup Instruction:  %5 = load i32* %i, align 4, !dbg !131
Current Pushup Instruction:  br label %4, !dbg !131
Current Pushup Instruction: store i32 %27, i32* %i, align 4, !dbg !131
Current Pushup Instruction: %27 = add nsw i32 %26, 1, !dbg !131
Current Pushup Instruction: %26 = load i32* %i, align 4, !dbg !131
Current Pushup Instruction: br label %25, !dbg !141
Current Pushup Instruction: store %struct.Node* %24, %struct.Node** %p, align 8, !dbg !140
Current Pushup Instruction: %24 = load %struct.Node** %new_node, align 8, !dbg !140
Current Pushup Instruction: br label %23, !dbg !139
Current Pushup Instruction: store %struct.Node* %22, %struct.Node** %q, align 8, !dbg !139
Current Pushup Instruction:  %22 = load %struct.Node** %new_node, align 8, !dbg !139
Current Pushup Instruction:  br i1 %20, label %21, label %23, !dbg !137
Current Pushup Instruction: %20 = icmp eq %struct.Node* %19, null, !dbg !137
Current Pushup Instruction:  %19 = load %struct.Node** %p, align 8, !dbg !137
Current Pushup Instruction: store %struct.Node* %16, %struct.Node** %18, align 8, !dbg !136
Current Pushup Instruction:  %18 = getelementptr inbounds %struct.Node* %17, i32 0, i32 1, !dbg !136
Current Pushup Instruction:  %17 = load %struct.Node** %new_node, align 8, !dbg !136
Current Pushup Instruction:  %16 = load %struct.Node** %p, align 8, !dbg !136
Current Pushup Instruction: store i8 %13, i8* %15, align 1, !dbg !135
Current Pushup Instruction:  %15 = getelementptr inbounds %struct.Node* %14, i32 0, i32 0, !dbg !135
Current Pushup Instruction: %14 = load %struct.Node** %new_node, align 8, !dbg !135
Current Pushup Instruction: %13 = trunc i32 %12 to i8, !dbg !135
Current Pushup Instruction: %12 = add nsw i32 %11, 96, !dbg !135
Current Pushup Instruction: %11 = sub nsw i32 2, %10, !dbg !135
Current Pushup Instruction: %10 = load i32* %i, align 4, !dbg !135
Current Pushup Instruction: store %struct.Node* %9, %struct.Node** %new_node, align 8, !dbg !133 

****** Flag = 3 *******
  store %struct.Node* %9, %struct.Node** %new_node, align 8, !dbg !133
------
No of operands: 2
 getOperand(0) ==> %9 = bitcast i8* %8 to %struct.Node*, !dbg !133
   getOperand(0) type ==> %struct.Node*
 getOperand(1) ==> %new_node = alloca %struct.Node*, align 8
   getOperand(1) type ==> %struct.Node**
****** Flag = 4 *******
  store %struct.Node* %9, %struct.Node** %new_node, align 8, !dbg !133
------
Cp1
  %9 = bitcast i8* %8 to %struct.Node*, !dbg !133
Cp1
  %8 = call noalias i8* @malloc(i64 16) #6, !dbg !133
Cp9
klee: TxWP.cpp:1286: klee::ref<klee::Expr> klee::TxWeakestPreCondition::getCallInst(llvm::CallInst*): Assertion `ret && "Return instruction is null!"' failed.
0  klee            0x0000000000ea1582 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  klee            0x0000000000ea0dd4
2  libpthread.so.0 0x00007fc15f964390
3  libc.so.6       0x00007fc15d0e3438 gsignal + 56
4  libc.so.6       0x00007fc15d0e503a abort + 362
5  libc.so.6       0x00007fc15d0dbbe7
6  libc.so.6       0x00007fc15d0dbc92
7  klee            0x00000000005e5686 klee::TxWeakestPreCondition::getCallInst(llvm::CallInst*) + 294
8  klee            0x00000000005e3bfb klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 1387
9  klee            0x00000000005e4e87 klee::TxWeakestPreCondition::getCastInst(llvm::CastInst*) + 87
10 klee            0x00000000005e3b33 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 1187
11 klee            0x00000000005e60f5 klee::TxWeakestPreCondition::PushUp(std::vector<std::pair<klee::KInstruction*, int>, std::allocator<std::pair<klee::KInstruction*, int> > >) + 1429
12 klee            0x00000000005bf5d8 klee::TxTreeNode::generateWPInterpolant() + 1032
13 klee            0x00000000005c6a9b klee::TxSubsumptionTableEntry::TxSubsumptionTableEntry(klee::TxTreeNode*, std::vector<llvm::Instruction*, std::allocator<llvm::Instruction*> > const&) + 1051
14 klee            0x00000000005c6c1c klee::TxTree::remove(klee::ExecutionState*, klee::TimingSolver*, bool) + 300
15 klee            0x00000000005542d1 klee::Executor::updateStates(klee::ExecutionState*) + 513
16 klee            0x00000000005691ce klee::Executor::run(klee::ExecutionState&) + 6222
17 klee            0x0000000000569e7a klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1850
18 klee            0x000000000052f71d main + 12941
19 libc.so.6       0x00007fc15d0ce840 __libc_start_main + 240
20 klee            0x0000000000543089 _start + 41
KLEE: WARNING: KLEE: watchdog exiting (no child)
ArpitaDutta commented 1 year ago

Fixed with commit 7672a88a54253578375ea9facb2e990e86922c4c .

ArpitaDutta commented 1 year ago

WP output: 

************Basic Block Coverage Report Starts****************
KLEE: done: Total number of single time Visited Basic Blocks: 7
KLEE: done: Total number of Basic Blocks: 7
************Basic Block Coverage Report Ends****************
************ICMP/Atomic Condition Coverage Report Starts****************
KLEE: done: Total number of Covered ICMP/Atomic Condition: 2
KLEE: done: Total number of All ICMP/Atomic Condition: 2
************ICMP/Atomic Condition Coverage Report Ends****************
KLEE: Memory cap NOT exceeded!

KLEE: done: Total reduced symbolic execution tree nodes = 1
KLEE: done: Total number of visited basic blocks = 12

KLEE: done: Subsumption statistics
KLEE: done:     Time for actual solver calls in subsumption check (ms) = 0
KLEE: done:     Number of solver calls for subsumption check (failed) = 0 (0)
KLEE: done:     Concrete store expression build time (ms) = 0
KLEE: done:     Symbolic store expression build time (ms) = 0
KLEE: done:     Solver access time (ms) = 0
KLEE: done:     Average table entries per subsumption checkpoint = 1.00
KLEE: done:     Number of subsumption checks = 1
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 0.211
KLEE: done:     remove = 27.841
KLEE: done:     subsumptionCheck = 0.035
KLEE: done:     markPathCondition = 0.039
KLEE: done:     split = 0
KLEE: done:     executeOnNode = 0.162
KLEE: done:     executeMemoryOperation = 0.401

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.002
KLEE: done:     get WP Interpolant = 27.665
KLEE: done:     addConstraintTime = 0
KLEE: done:     splitTime = 0
KLEE: done:     execute = 0.144
KLEE: done:     bindCallArguments = 0
KLEE: done:     bindReturnValue = 0
KLEE: done:     getStoredExpressions = 0
KLEE: done:     getStoredCoreExpressions = 0

KLEE: done: total instructions = 82
KLEE: done: completed paths = 1, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 0
KLEE: done:     average branching depth of subsumed paths = 0
KLEE: done:     average instructions of completed paths = 81
KLEE: done:     average instructions of subsumed paths = 0
KLEE: done:     subsumed paths = 0
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 1
KLEE: done: generated tests = 0, among which
KLEE: done:     early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     error tests = 0
KLEE: done:     program exit tests = 0

KLEE: done: NOTE:
KLEE: done:     Subsumed paths / tests counts are nondeterministic for
KLEE: done:     programs with dynamically-allocated memory such as those
KLEE: done:     using malloc, since KLEE may reuse the address of the
KLEE: done:     same malloc calls in different paths. This nondeterminism
KLEE: done:     does not cause loss of error reports.
-------------------------------------------------------------------------------------------
|            Path            |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
-------------------------------------------------------------------------------------------
|pointer_struct4-3/klee-out-0|      82|     0.03|    16.56|     5.71|     314|        0.00|
-------------------------------------------------------------------------------------------
ArpitaDutta commented 1 year ago

Deletion Output: 

************Basic Block Coverage Report Starts****************
KLEE: done: Total number of single time Visited Basic Blocks: 7
KLEE: done: Total number of Basic Blocks: 7
************Basic Block Coverage Report Ends****************
************ICMP/Atomic Condition Coverage Report Starts****************
KLEE: done: Total number of Covered ICMP/Atomic Condition: 2
KLEE: done: Total number of All ICMP/Atomic Condition: 2
************ICMP/Atomic Condition Coverage Report Ends****************
KLEE: Memory cap NOT exceeded!

KLEE: done: Total reduced symbolic execution tree nodes = 1
KLEE: done: Total number of visited basic blocks = 12

KLEE: done: Subsumption statistics
KLEE: done:     Time for actual solver calls in subsumption check (ms) = 0
KLEE: done:     Number of solver calls for subsumption check (failed) = 0 (0)
KLEE: done:     Concrete store expression build time (ms) = 0
KLEE: done:     Symbolic store expression build time (ms) = 0
KLEE: done:     Solver access time (ms) = 0
KLEE: done:     Average table entries per subsumption checkpoint = 1.00
KLEE: done:     Number of subsumption checks = 1
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 0.21
KLEE: done:     remove = 0.152
KLEE: done:     subsumptionCheck = 0.034
KLEE: done:     markPathCondition = 0.037
KLEE: done:     split = 0
KLEE: done:     executeOnNode = 0.191
KLEE: done:     executeMemoryOperation = 0.398

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.001
KLEE: done:     addConstraintTime = 0
KLEE: done:     splitTime = 0
KLEE: done:     execute = 0.172
KLEE: done:     bindCallArguments = 0
KLEE: done:     bindReturnValue = 0
KLEE: done:     getStoredExpressions = 0
KLEE: done:     getStoredCoreExpressions = 0

KLEE: done: total instructions = 82
KLEE: done: completed paths = 1, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 0
KLEE: done:     average branching depth of subsumed paths = 0
KLEE: done:     average instructions of completed paths = 81
KLEE: done:     average instructions of subsumed paths = 0
KLEE: done:     subsumed paths = 0
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 1
KLEE: done: generated tests = 0, among which
KLEE: done:     early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     error tests = 0
KLEE: done:     program exit tests = 0

KLEE: done: NOTE:
KLEE: done:     Subsumed paths / tests counts are nondeterministic for
KLEE: done:     programs with dynamically-allocated memory such as those
KLEE: done:     using malloc, since KLEE may reuse the address of the
KLEE: done:     same malloc calls in different paths. This nondeterminism
KLEE: done:     does not cause loss of error reports.
-------------------------------------------------------------------------------------------
|            Path            |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
-------------------------------------------------------------------------------------------
|pointer_struct4-2/klee-out-0|      82|     0.01|    16.56|     5.71|     314|        0.00|
-------------------------------------------------------------------------------------------
rasoolmaghareh commented 11 months ago

Issue got fixed.