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/local.c bug #395

Closed rasoolmaghareh closed 1 year 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 local.c
SOLVER_FLAGS="-solver-backend=z3" OUTPUT_DIR=local.tx make local.klee-out
make[1]: Entering directory '/home/issta21-322/TracerX-examples/basic'
KLEE: output directory is "/home/issta21-322/TracerX-examples/basic/local.tx"
Using Z3 solver backend
KLEE: Logging all queries in .pc format to /home/issta21-322/TracerX-examples/basic/local.tx/all-queries.pc

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

KLEE: Deterministic memory allocation starting from 0x7ff30000000
  %13 = load i32** %c, align 8, !dbg !142
KLEE: WARNING: TxWeakestPreCondition::getLoad: Not implemented yet!
0  klee            0x0000000000e983e2 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  klee            0x0000000000e97c34
2  libpthread.so.0 0x00007fa399de9390
3  klee            0x00000000005dc785 klee::TxWeakestPreCondition::getBinaryInst(llvm::BinaryOperator*) + 149
4  klee            0x00000000005db763 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 563
5  klee            0x00000000005dd93f klee::TxWeakestPreCondition::PushUp(std::vector<std::pair<klee::KInstruction*, int>, std::allocator<std::pair<klee::KInstruction*, int> > >) + 319
6  klee            0x00000000005b7cd8 klee::TxTreeNode::generateWPInterpolant() + 1032
7  klee            0x00000000005be5eb klee::TxSubsumptionTableEntry::TxSubsumptionTableEntry(klee::TxTreeNode*, std::vector<llvm::Instruction*, std::allocator<llvm::Instruction*> > const&) + 1163
8  klee            0x00000000005be96b klee::TxTree::remove(klee::ExecutionState*, klee::TimingSolver*, bool) + 779
9  klee            0x000000000054a3b1 klee::Executor::updateStates(klee::ExecutionState*) + 513
10 klee            0x000000000056142e klee::Executor::run(klee::ExecutionState&) + 5982
11 klee            0x0000000000561f59 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1705
12 klee            0x000000000052825d main + 10365
13 libc.so.6       0x00007fa397591840 __libc_start_main + 240
14 klee            0x000000000053bb69 _start + 41
Command terminated by signal 11
0.03user 0.01system 0:00.34elapsed 13%CPU (0avgtext+0avgdata 26592maxresident)k
0inputs+192outputs (0major+1578minor)pagefaults 0swaps
make[2]: Entering directory '/home/issta21-322/TracerX-examples/basic'
warning: ignoring debug info with an invalid version (1) in local.bc
Writing 'cfg.add2.dot'...
Printing analysis 'Print CFG of function to 'dot' file' for function 'add2':
Writing 'cfg.add1.dot'...
Printing analysis 'Print CFG of function to 'dot' file' for function 'add1':
Writing 'cfg.add.dot'...
Printing analysis 'Print CFG of function to 'dot' file' for function 'add':
Writing 'cfg.main.dot'...
Printing analysis 'Print CFG of function to 'dot' file' for function 'main':
-----------------------------------------------------------------------
|  Path  |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
-----------------------------------------------------------------------
|local.tx|       0|     0.00|     0.00|     0.00|     393|        0.00|
-----------------------------------------------------------------------
make[2]: Leaving directory '/home/issta21-322/TracerX-examples/basic'
make[1]: Leaving directory '/home/issta21-322/TracerX-examples/basic
ArpitaDutta commented 1 year ago

After fixing the issue #392, ie., by adding the check for null expr in TxWeakestPreCondition::getBinaryInst(), this issue also got resolved.

ArpitaDutta commented 1 year ago

WP output: 

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

KLEE: done: Total reduced symbolic execution tree nodes = 15
KLEE: done: Total number of visited basic blocks = 39

KLEE: done: Subsumption statistics
KLEE: done:     Time for actual solver calls in subsumption check (ms) = 237.123
KLEE: done:     Number of solver calls for subsumption check (failed) = 10 (8)
KLEE: done:     Concrete store expression build time (ms) = 0.096
KLEE: done:     Symbolic store expression build time (ms) = 0
KLEE: done:     Solver access time (ms) = 260.787
KLEE: done:     Average table entries per subsumption checkpoint = 1.85
KLEE: done:     Number of subsumption checks = 15
KLEE: done:     Average solver calls per subsumption check = 0.66

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 0.162
KLEE: done:     remove = 38.895
KLEE: done:     subsumptionCheck = 261.225
KLEE: done:     markPathCondition = 0.074
KLEE: done:     split = 0.059
KLEE: done:     executeOnNode = 0.143
KLEE: done:     executeMemoryOperation = 0.896

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.077
KLEE: done:     get WP Interpolant = 32.481
KLEE: done:     addConstraintTime = 0.11
KLEE: done:     splitTime = 0.047
KLEE: done:     execute = 0.132
KLEE: done:     bindCallArguments = 0.018
KLEE: done:     bindReturnValue = 0.008
KLEE: done:     getStoredExpressions = 0.032
KLEE: done:     getStoredCoreExpressions = 0.146

KLEE: done: total instructions = 312
KLEE: done: completed paths = 8, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 3
KLEE: done:     average branching depth of subsumed paths = 3
KLEE: done:     average instructions of completed paths = 111.5
KLEE: done:     average instructions of subsumed paths = 93.5
KLEE: done:     subsumed paths = 2
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 6
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.
'local-3' already present. Replacing with a new folder
---------------------------------------------------------------------------------
|       Path       |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
---------------------------------------------------------------------------------
|local-3/klee-out-0|     312|     0.31|    32.82|     9.46|     393|        2.50|
---------------------------------------------------------------------------------
ArpitaDutta commented 1 year ago

Deletion Output: 

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

KLEE: done: Total reduced symbolic execution tree nodes = 15
KLEE: done: Total number of visited basic blocks = 39

KLEE: done: Subsumption statistics
KLEE: done:     Time for actual solver calls in subsumption check (ms) = 76.236
KLEE: done:     Number of solver calls for subsumption check (failed) = 10 (8)
KLEE: done:     Concrete store expression build time (ms) = 0.064
KLEE: done:     Symbolic store expression build time (ms) = 0.002
KLEE: done:     Solver access time (ms) = 86.77
KLEE: done:     Average table entries per subsumption checkpoint = 1.85
KLEE: done:     Number of subsumption checks = 15
KLEE: done:     Average solver calls per subsumption check = 0.66

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 0.254
KLEE: done:     remove = 0.281
KLEE: done:     subsumptionCheck = 86.929
KLEE: done:     markPathCondition = 0.046
KLEE: done:     split = 0.061
KLEE: done:     executeOnNode = 0.176
KLEE: done:     executeMemoryOperation = 1.134

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.051
KLEE: done:     addConstraintTime = 0.169
KLEE: done:     splitTime = 0.049
KLEE: done:     execute = 0.158
KLEE: done:     bindCallArguments = 0.038
KLEE: done:     bindReturnValue = 0.011
KLEE: done:     getStoredExpressions = 0.022
KLEE: done:     getStoredCoreExpressions = 0.092

KLEE: done: total instructions = 312
KLEE: done: completed paths = 8, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 3
KLEE: done:     average branching depth of subsumed paths = 3
KLEE: done:     average instructions of completed paths = 111.5
KLEE: done:     average instructions of subsumed paths = 93.5
KLEE: done:     subsumed paths = 2
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 6
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(%)|
---------------------------------------------------------------------------------
|local-2/klee-out-0|     312|     0.11|    32.82|     9.46|     393|       10.44|
---------------------------------------------------------------------------------
ArpitaDutta commented 1 year ago

Commit 60c20f9 fixes the issue.