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/validation.c #392

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

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

KLEE: Deterministic memory allocation starting from 0x7ff30000000
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING ONCE: calling external: printf(8792603367936)
Try again...
  %11 = ptrtoint i8* %9 to i64, !dbg !134
KLEE: WARNING: TxWeakestPreCondition::generateExprFromOperand Unary Operand not implemented...

  %12 = ptrtoint i8* %10 to i64, !dbg !134
KLEE: WARNING: TxWeakestPreCondition::generateExprFromOperand Unary Operand not implemented...

0  klee            0x0000000000e983e2 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  klee            0x0000000000e97c34
2  libpthread.so.0 0x00007fbeca9d3390
3  klee            0x00000000005dc785 klee::TxWeakestPreCondition::getBinaryInst(llvm::BinaryOperator*) + 149
4  klee            0x00000000005db763 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 563
5  klee            0x00000000005dc74e klee::TxWeakestPreCondition::getBinaryInst(llvm::BinaryOperator*) + 94
6  klee            0x00000000005db763 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 563
7  klee            0x00000000005dd2dd klee::TxWeakestPreCondition::getCallInst(llvm::CallInst*) + 221
8  klee            0x00000000005db8d5 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 933
9  klee            0x00000000005dc74e klee::TxWeakestPreCondition::getBinaryInst(llvm::BinaryOperator*) + 94
10 klee            0x00000000005db763 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 563
11 klee            0x00000000005dc779 klee::TxWeakestPreCondition::getBinaryInst(llvm::BinaryOperator*) + 137
12 klee            0x00000000005db763 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 563
13 klee            0x00000000005dcdbe klee::TxWeakestPreCondition::getCmpCondition(llvm::CmpInst*) + 94
14 klee            0x00000000005dd3bd klee::TxWeakestPreCondition::getCondition(llvm::Value*) + 77
15 klee            0x00000000005dd789 klee::TxWeakestPreCondition::getBrCondition(llvm::Instruction*) + 57
16 klee            0x00000000005ddaf3 klee::TxWeakestPreCondition::PushUp(std::vector<std::pair<klee::KInstruction*, int>, std::allocator<std::pair<klee::KInstruction*, int> > >) + 755
17 klee            0x00000000005b7cd8 klee::TxTreeNode::generateWPInterpolant() + 1032
18 klee            0x00000000005be5eb klee::TxSubsumptionTableEntry::TxSubsumptionTableEntry(klee::TxTreeNode*, std::vector<llvm::Instruction*, std::allocator<llvm::Instruction*> > const&) + 1163
19 klee            0x00000000005be96b klee::TxTree::remove(klee::ExecutionState*, klee::TimingSolver*, bool) + 779
20 klee            0x000000000054a3b1 klee::Executor::updateStates(klee::ExecutionState*) + 513
21 klee            0x000000000056142e klee::Executor::run(klee::ExecutionState&) + 5982
22 klee            0x0000000000561f59 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1705
23 klee            0x000000000052825d main + 10365
24 libc.so.6       0x00007fbec817b840 __libc_start_main + 240
25 klee            0x000000000053bb69 _start + 41
Command terminated by signal 11
0.02user 0.00system 0:00.35elapsed 10%CPU (0avgtext+0avgdata 27032maxresident)k
0inputs+208outputs (0major+1527minor)pagefaults 0swaps
make[2]: Entering directory '/home/issta21-322/TracerX-examples/basic'
warning: ignoring debug info with an invalid version (1) in validation.bc
Writing 'cfg.strlen.dot'...
Printing analysis 'Print CFG of function to 'dot' file' for function 'strlen':
Writing 'cfg.main.dot'...
Printing analysis 'Print CFG of function to 'dot' file' for function 'main':
----------------------------------------------------------------------------
|    Path     |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
----------------------------------------------------------------------------
|validation.tx|       0|     0.00|     0.00|     0.00|     491|        0.00|
----------------------------------------------------------------------------
make[2]: Leaving directory '/home/issta21-322/TracerX-examples/basic'
make[1]: Leaving directory '/home/issta21-322/TracerX-examples/basic'
grep: validation.tx/tree.dot: No such file or directory
ERROR: Subsumption number (0) disagrees with reference data for validation.c (36)
../Makefile.common:120: recipe for target 'validation.tx' failed
ArpitaDutta commented 1 year ago

We are getting error because the for the instruction %14 = sub i64 %12, %13, !dbg !134, getBinaryInst() is getting null expr for both the operands. Operand 1:

%11 = ptrtoint i8* %9 to i64, !dbg !134
KLEE: WARNING: TxWeakestPreCondition::generateExprFromOperand Unary Operand not implemented...

Operand 2:

%12 = ptrtoint i8* %10 to i64, !dbg !134
KLEE: WARNING: TxWeakestPreCondition::generateExprFromOperand Unary Operand not implemented...

since the [PtrToInt ](llvm::Instruction::PtrToInt:) type is not supported yet.

The check was missing inside TxWeakestPreCondition::getBinaryInst to return dummy and fail the subsumption check when any of the operand is missing.

After adding this check program is working fine. I will add the PR as well in this thread.

    ref<Expr> ret;
    ref<Expr> arg1 = generateExprFromOperand(bo->getOperand(0));
    ref<Expr> arg2 = generateExprFromOperand(bo->getOperand(1));
    if (arg1.isNull() || arg2.isNull())
    return ret;
ArpitaDutta commented 1 year ago

Getting the below output now:


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

KLEE: done: Total reduced symbolic execution tree nodes = 279
KLEE: done: Total number of visited basic blocks = 908

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) = 125.117
KLEE: done:     Symbolic store expression build time (ms) = 0.001
KLEE: done:     Solver access time (ms) = 0.887
KLEE: done:     Average table entries per subsumption checkpoint = 9.72
KLEE: done:     Number of subsumption checks = 279
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 1.157
KLEE: done:     remove = 336.585
KLEE: done:     subsumptionCheck = 222.043
KLEE: done:     markPathCondition = 0.562
KLEE: done:     split = 1.568
KLEE: done:     executeOnNode = 11.944
KLEE: done:     executeMemoryOperation = 4.857

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.207
KLEE: done:     get WP Interpolant = 260.851
KLEE: done:     addConstraintTime = 1.306
KLEE: done:     splitTime = 1.331
KLEE: done:     execute = 11.779
KLEE: done:     bindCallArguments = 0.007
KLEE: done:     bindReturnValue = 0.055
KLEE: done:     getStoredExpressions = 0.61
KLEE: done:     getStoredCoreExpressions = 2.581

KLEE: done: total instructions = 3413
KLEE: done: completed paths = 140, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 50.2885
KLEE: done:     average branching depth of subsumed paths = 19
KLEE: done:     average instructions of completed paths = 402.875
KLEE: done:     average instructions of subsumed paths = 295.444
KLEE: done:     subsumed paths = 36
KLEE: done:     error paths = 2
KLEE: done:     program exit paths = 102
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(%)|
--------------------------------------------------------------------------------------
|validation-3/klee-out-0|    3413|     0.68|    45.82|    30.21|     491|        9.37|
--------------------------------------------------------------------------------------
ArpitaDutta commented 1 year ago

Output for the deletion branch as well: 


KLEE: NOTE: now ignoring this error at this location
************Basic Block Coverage Report Starts****************
KLEE: done: Total number of single time Visited Basic Blocks: 35
KLEE: done: Total number of Basic Blocks: 36
************Basic Block Coverage Report Ends****************
************ICMP/Atomic Condition Coverage Report Starts****************
KLEE: done: Total number of Covered ICMP/Atomic Condition: 15
KLEE: done: Total number of All ICMP/Atomic Condition: 15
************ICMP/Atomic Condition Coverage Report Ends****************
KLEE: Memory cap NOT exceeded!

KLEE: done: Total reduced symbolic execution tree nodes = 279
KLEE: done: Total number of visited basic blocks = 908

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) = 1.66
KLEE: done:     Symbolic store expression build time (ms) = 0.006
KLEE: done:     Solver access time (ms) = 0.101
KLEE: done:     Average table entries per subsumption checkpoint = 9.72
KLEE: done:     Number of subsumption checks = 279
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 1.491
KLEE: done:     remove = 4.627
KLEE: done:     subsumptionCheck = 3.109
KLEE: done:     markPathCondition = 0.337
KLEE: done:     split = 1.789
KLEE: done:     executeOnNode = 1.904
KLEE: done:     executeMemoryOperation = 3.529

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.18
KLEE: done:     addConstraintTime = 1.413
KLEE: done:     splitTime = 1.505
KLEE: done:     execute = 1.738
KLEE: done:     bindCallArguments = 0.009
KLEE: done:     bindReturnValue = 0.043
KLEE: done:     getStoredExpressions = 0.607
KLEE: done:     getStoredCoreExpressions = 2.36

KLEE: done: total instructions = 3413
KLEE: done: completed paths = 140, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 50.2885
KLEE: done:     average branching depth of subsumed paths = 19
KLEE: done:     average instructions of completed paths = 402.875
KLEE: done:     average instructions of subsumed paths = 295.444
KLEE: done:     subsumed paths = 36
KLEE: done:     error paths = 2
KLEE: done:     program exit paths = 102
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(%)|
--------------------------------------------------------------------------------------
|validation-2/klee-out-0|    3413|     0.13|    45.82|    30.21|     491|       55.14|
--------------------------------------------------------------------------------------
ArpitaDutta commented 1 year ago

Commit 60c20f9 fixes the issue.

rasoolmaghareh commented 1 year ago

Thanks