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_struct6.c with WP #377

Closed rasoolmaghareh closed 1 year ago

rasoolmaghareh commented 4 years ago

Crash in TxWPHelper::substituteExpr:

KLEE: Deterministic memory allocation starting from 0x7ff30000000
0  libLLVM-3.4.so  0x00007f1f94b8e052 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  libLLVM-3.4.so  0x00007f1f94b8d7c4
2  libpthread.so.0 0x00007f1f9428b390
3  klee            0x000000000051429e klee::TxWPHelper::substituteExpr(klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::ref<klee::Expr>) + 3086
4  klee            0x0000000000513d2b klee::TxWPHelper::substituteExpr(klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::ref<klee::Expr>) + 1691
5  klee            0x000000000050fb11 klee::TxWeakestPreCondition::PushUp(std::vector<std::pair<klee::KInstruction*, int>, std::allocator<std::pair<klee::KInstruction*, int> > >) + 1521
6  klee            0x00000000004e9448 klee::TxTreeNode::generateWPInterpolant() + 1032
7  klee            0x00000000004eff6b klee::TxSubsumptionTableEntry::TxSubsumptionTableEntry(klee::TxTreeNode*, std::vector<llvm::Instruction*, std::allocator<llvm::Instruction*> > const&) + 1131
8  klee            0x00000000004f03eb klee::TxTree::remove(klee::ExecutionState*, klee::TimingSolver*, bool) + 795
9  klee            0x000000000047d12e klee::Executor::updateStates(klee::ExecutionState*) + 526
10 klee            0x0000000000494380 klee::Executor::run(klee::ExecutionState&) + 5744
11 klee            0x0000000000494fd6 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1686
12 klee            0x000000000046560d main + 12765
13 libc.so.6       0x00007f1f91c14830 __libc_start_main + 240
14 klee            0x000000000046e0c9 _start + 41
Command terminated by signal 11
0.10user 0.01system 0:00.22elapsed 53%CPU (0avgtext+0avgdata 35628maxresident)k
rasoolmaghareh commented 1 year ago

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

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

KLEE: Deterministic memory allocation starting from 0x7ff30000000
0  klee            0x0000000000e983e2 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  klee            0x0000000000e97c34
2  libpthread.so.0 0x00007f529a35c390
3  klee            0x00000000005e24fe klee::TxWPHelper::substituteExpr(klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::ref<klee::Expr>) + 3086
4  klee            0x00000000005e1f8b klee::TxWPHelper::substituteExpr(klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::ref<klee::Expr>) + 1691
5  klee            0x00000000005ddded klee::TxWeakestPreCondition::PushUp(std::vector<std::pair<klee::KInstruction*, int>, std::allocator<std::pair<klee::KInstruction*, int> > >) + 1517
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       0x00007f5297b04840 __libc_start_main + 240
14 klee            0x000000000053bb69 _start + 41
Command terminated by signal 11
0.21user 0.01system 0:00.52elapsed 42%CPU (0avgtext+0avgdata 28576maxresident)k
0inputs+248outputs (0major+2636minor)pagefaults 0swaps
make[2]: Entering directory '/home/issta21-322/TracerX-examples/basic'
warning: ignoring debug info with an invalid version (1) in pointer_struct6.bc
Writing 'cfg.main.dot'...
Printing analysis 'Print CFG of function to 'dot' file' for function 'main':
Writing 'cfg.search_insert.dot'...
Printing analysis 'Print CFG of function to 'dot' file' for function 'search_insert':
---------------------------------------------------------------------------------
|       Path       |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
---------------------------------------------------------------------------------
|pointer_struct6.tx|       0|     0.00|     0.00|     0.00|     382|        0.00|
---------------------------------------------------------------------------------
make[2]: Leaving directory '/home/issta21-322/TracerX-examples/basic'
make[1]: Leaving directory '/home/issta21-322/TracerX-examples/basic'
grep: pointer_struct6.tx/tree.dot: No such file or directory
ERROR: Subsumption number (0) disagrees with reference data for pointer_struct6.c (132)
../Makefile.common:120: recipe for target 'pointer_struct6.tx' failed
make: *** [pointer_struct6.tx] Error 1
rm regexp_mark.bc overmark.bc addition_safe8.bc DP-local.bc P1-L-T-R161.bc openssl.bc loop_unsafe1.bc pointer_wp5.bc testmem.bc pointer_struct6.bc
ArpitaDutta commented 1 year ago

Getting the following output after new fixes in Sel expr.

************Basic Block Coverage Report Starts****************
KLEE: done: Total number of single time Visited Basic Blocks: 17
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 = 901
KLEE: done: Total number of visited basic blocks = 4057

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) = 112.464
KLEE: done:     Symbolic store expression build time (ms) = 0.022
KLEE: done:     Solver access time (ms) = 3.337
KLEE: done:     Average table entries per subsumption checkpoint = 153.00
KLEE: done:     Number of subsumption checks = 901
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 5.747
KLEE: done:     remove = 3952.79
KLEE: done:     subsumptionCheck = 6377.77
KLEE: done:     markPathCondition = 2.207
KLEE: done:     split = 4.757
KLEE: done:     executeOnNode = 7.198
KLEE: done:     executeMemoryOperation = 27.254

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.286
KLEE: done:     get WP Interpolant = 3180.87
KLEE: done:     addConstraintTime = 7.611
KLEE: done:     splitTime = 3.534
KLEE: done:     execute = 6.338
KLEE: done:     bindCallArguments = 0.434
KLEE: done:     bindReturnValue = 0.069
KLEE: done:     getStoredExpressions = 2.046
KLEE: done:     getStoredCoreExpressions = 11.776

KLEE: done: total instructions = 18095
KLEE: done: completed paths = 451, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 12.9238
KLEE: done:     average branching depth of subsumed paths = 9.50735
KLEE: done:     average instructions of completed paths = 304.26
KLEE: done:     average instructions of subsumed paths = 222.779
KLEE: done:     subsumed paths = 136
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 315
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_struct6-3/klee-out-0|   18095|    11.77|    31.41|    13.16|     382|       10.99|
-------------------------------------------------------------------------------------------
rasoolmaghareh commented 1 year ago

thanks we can close this issue.