Crash on klee-examples/basic/argument1.c

[rasoolmaghareh]

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

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

KLEE: Deterministic memory allocation starting from 0x7ff30000000
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING ONCE: calling external: printf(8792603367768, 1, 8792603361984)
argument 1:argument1.bc
0  klee            0x0000000000e98402 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  klee            0x0000000000e97c54
2  libpthread.so.0 0x00007ff6bd37b390
3  klee            0x00000000005dc220 klee::TxWeakestPreCondition::getFunctionArgument(llvm::Argument*) + 880
4  klee            0x00000000005db840 klee::TxWeakestPreCondition::generateExprFromOperand(llvm::Value*, klee::ref<klee::Expr>) + 752
5  klee            0x00000000005dd95f klee::TxWeakestPreCondition::PushUp(std::vector<std::pair<klee::KInstruction*, int>, std::allocator<std::pair<klee::KInstruction*, int> > >) + 319
6  klee            0x00000000005b7d58 klee::TxTreeNode::generateWPInterpolant() + 1032
7  klee            0x00000000005be66b klee::TxSubsumptionTableEntry::TxSubsumptionTableEntry(klee::TxTreeNode*, std::vector<llvm::Instruction*, std::allocator<llvm::Instruction*> > const&) + 1163
8  klee            0x00000000005be9eb klee::TxTree::remove(klee::ExecutionState*, klee::TimingSolver*, bool) + 779
9  klee            0x000000000054a341 klee::Executor::updateStates(klee::ExecutionState*) + 513
10 klee            0x00000000005613be klee::Executor::run(klee::ExecutionState&) + 5982
11 klee            0x0000000000561ee9 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1705
12 klee            0x000000000052821d main + 10365
13 libc.so.6       0x00007ff6bab23840 __libc_start_main + 240
14 klee            0x000000000053baf9 _start + 41
Command terminated by signal 11
0.02user 0.01system 0:00.27elapsed 12%CPU (0avgtext+0avgdata 27776maxresident)k
0inputs+144outputs (0major+1518minor)pagefaults 0swaps
make[2]: Entering directory '/home/issta21-322/TracerX-examples/basic'
warning: ignoring debug info with an invalid version (1) in argument1.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(%)|
---------------------------------------------------------------------------
|argument1.tx|       0|     0.00|     0.00|     0.00|     291|        0.00|
---------------------------------------------------------------------------

[ArpitaDutta]

Bug in TxWeakestPreCondition::getFunctionArgument(). It is unable to get the correct function.

[rasoolmaghareh]

Can you elaborate more please. thanks

[ArpitaDutta]

The present TxWeakestPreCondition::getFunctionArgument() tries to search for the call instruction to get the function arguments. However, in this program there is no specific call to the function because it is the main() function and these are command line arguments. Unlike the parameters passed from one function to another function.

It will be great if we can discuss this issue as well in tonight's meeting.

[ArpitaDutta]

This program is a special case.

 #include <stdio.h>
 int main (int argc, char **argv) { 
   int test = 0;
   for (int i=0; i< argc; i++) {
     printf("argument %d:%s\n", i+1, argv[i]);  
   }
   return 0;
}

We actually don't have any values for argc and argv. So our program is unable to obtain any value for it.