Normally when the timeout and watchdog work correctly, we get the following Klee messages:
Output-1:
KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via INT
KLEE: ctrl-c detected, requesting interpreter to halt.
or
KLEE: HaltTimer invoked
KLEE: halting execution, dumping remaining states
Followed by the statistics .......
But for the programs on which --watchdog option is not working correctly have the following output.
Output-2:
KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via INT
KLEE: ctrl-c detected, requesting interpreter to halt.
KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via gdb
Could not attach to process. If your uid matches the uid of the target
process, check the setting of /proc/sys/kernel/yama/ptrace_scope, or try
again as the root user. For more details, see /etc/sysctl.d/10-ptrace.conf
ptrace: Operation not permitted.
No symbol table is loaded. Use the "file" command.
The program is not being run.
KLEE: WARNING: KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)
The black highlighted messages in Output-1 are coming from the main. cpp where it checks for a variable 'level' whenever any interrupted is detected and tried to set a variable 'haltExecution' to halt the execution and call the function 'doDumpStates().
But in Output-2: all the highlighted messages are coming from the main.cpp when they are failed to correctly set and pass the effect of
'haltExecution' value and ultimately the program is getting killed by the SIGKILL operation.
In the Executor.cpp we check for the 'haltExecution' variable to continue the process or doDumpStates and exit.
But now even though the halting of initiated from the main.cpp but it is not accessed by the executor and the executor is getting stuck in the updateStates(&state); function.
On checking the updateStates(&state) function, [line no 4654, inside void Executor::run(ExecutionState &initialState) in Executor.cpp]
I found that it calls the 'TxTree::remove(ExecutionState state, TimingSolver solver, bool dumping)' function
and when the remove function creates an entry object [TxSubsumptionTableEntry *entry = new TxSubsumptionTableEntry(node, node->entryCallHistory);,
the program is getting stuck while this object creation.
Unable to understand how this is creating an issue.
Normally when the timeout and watchdog work correctly, we get the following Klee messages: Output-1: KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via INT KLEE: ctrl-c detected, requesting interpreter to halt. or KLEE: HaltTimer invoked KLEE: halting execution, dumping remaining states Followed by the statistics .......
But for the programs on which --watchdog option is not working correctly have the following output. Output-2: KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via INT KLEE: ctrl-c detected, requesting interpreter to halt. KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via gdb Could not attach to process. If your uid matches the uid of the target process, check the setting of /proc/sys/kernel/yama/ptrace_scope, or try again as the root user. For more details, see /etc/sysctl.d/10-ptrace.conf ptrace: Operation not permitted. No symbol table is loaded. Use the "file" command. The program is not being run. KLEE: WARNING: KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)
The black highlighted messages in Output-1 are coming from the main. cpp where it checks for a variable 'level' whenever any interrupted is detected and tried to set a variable 'haltExecution' to halt the execution and call the function 'doDumpStates().
But in Output-2: all the highlighted messages are coming from the main.cpp when they are failed to correctly set and pass the effect of 'haltExecution' value and ultimately the program is getting killed by the SIGKILL operation.
In the Executor.cpp we check for the 'haltExecution' variable to continue the process or doDumpStates and exit. But now even though the halting of initiated from the main.cpp but it is not accessed by the executor and the executor is getting stuck in the updateStates(&state); function.
On checking the updateStates(&state) function, [line no 4654, inside void Executor::run(ExecutionState &initialState) in Executor.cpp] I found that it calls the 'TxTree::remove(ExecutionState state, TimingSolver solver, bool dumping)' function and when the remove function creates an entry object [TxSubsumptionTableEntry *entry = new TxSubsumptionTableEntry(node, node->entryCallHistory);, the program is getting stuck while this object creation.
Unable to understand how this is creating an issue.