Missing error in klee-examples/basic/veritesting.c (over-subsumption)

[rasoolmaghareh]

In this example, WP misses the error:

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

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

KLEE: Deterministic memory allocation starting from 0x7ff30000000
KLEE: Deterministic memory allocation starting from 0x7ff30000000
KLEE: Memory cap NOT exceeded!

KLEE: done: Total reduced symbolic execution tree nodes = 51
KLEE: done: Total number of visited basic blocks = 161

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) = 0.157
KLEE: done:     Symbolic store expression build time (ms) = 0
KLEE: done:     Solver access time (ms) = 0.047
KLEE: done:     Average table entries per subsumption checkpoint = 9.00
KLEE: done:     Number of subsumption checks = 51
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 0.458
KLEE: done:     remove = 23.866
KLEE: done:     subsumptionCheck = 0.558
KLEE: done:     markPathCondition = 0.051
KLEE: done:     split = 0.241
KLEE: done:     executeOnNode = 0.424
KLEE: done:     executeMemoryOperation = 1.054

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.007
KLEE: done:     get WP Interpolant = 23.341
KLEE: done:     addConstraintTime = 0.554
KLEE: done:     splitTime = 0.184
KLEE: done:     execute = 0.294
KLEE: done:     bindCallArguments = 0
KLEE: done:     bindReturnValue = 0
KLEE: done:     getStoredExpressions = 0.053
KLEE: done:     getStoredCoreExpressions = 0.165

KLEE: done: total instructions = 530
KLEE: done: completed paths = 26, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 9
KLEE: done:     average branching depth of subsumed paths = 5.875
KLEE: done:     average instructions of completed paths = 192
KLEE: done:     average instructions of subsumed paths = 116.25
KLEE: done:     subsumed paths = 24
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 2
KLEE: done: generated tests = 2, 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 = 2

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.
0.05user 0.00system 0:00.07elapsed 84%CPU (0avgtext+0avgdata 26032maxresident)k
0inputs+264outputs (0major+1542minor)pagefaults 0swaps
make[2]: Entering directory '/home/issta21-322/TracerX-examples/basic'
warning: ignoring debug info with an invalid version (1) in veritesting_plus_small.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(%)|
----------------------------------------------------------------------------------------
|veritesting_plus_small.tx|     530|     0.06|    14.01|     6.94|     307|       40.35|
----------------------------------------------------------------------------------------
make[2]: Leaving directory '/home/issta21-322/TracerX-examples/basic'
make[1]: Leaving directory '/home/issta21-322/TracerX-examples/basic'
ERROR: Error count (0) disagrees with reference data for veritesting_plus_small.c (1)
../Makefile.common:120: recipe for target 'veritesting_plus_small.tx' failed

[ArpitaDutta]

Is there any special significance of the comment written on this program?

Copied the whole comment below.

/*
 * From Avgerinos et al.: Enhancing Symbolic Execution with
 * Veritesting, with modifications proposed by Chu Duc Hiep.
 *
 * In this example, Tracer-X KLEE over-subsumes and not able to
 * demonstrate the assertion violation, which can be demonstrated by
 * LLBMC. In this version, the variable start is also replaced with 0,
 * and the loop iterations reduced to 9.
 *
 * To run with LLBMC, compile with -DLLBMC, and execute LLBMC with the
 * options --ignore-missing-function-bodies -function-name=main
 * -no-overflow-checks -max-loop-iterations=0
 * -max-function-call-depth=0 -counterexample.
 *
 * Portions copyright 2017 National University of Singapore
 */

[rasoolmaghareh]

My tests show that deletion can find the bug, while WP can't. Can you please retry? I think TracerX was missing the bug before due to a bug on deletion side and it is passing now since the bug is fixed.

[ArpitaDutta]

Yes, WP is still missing the bug.

[rasoolmaghareh]

Can you please compare the interpolants to see at which point we have the over subsumption? thanks

[ArpitaDutta]

Sure.

[ArpitaDutta]

Initially WP has generated the correct interpolant. First interpolant:

wp interpolant = [(And (Not (Eq 37
               (Add w32 (WPVar w32 (counter)) N0:(WPVar w32 (i)))))
      (Sle 8 N0))]

but the second interpolant is incorrect and because of this interpolant, assert is getting missed. Second interpolant:

wp interpolant = [(And (Not (Eq 36 (WPVar w32 (counter))))
      (Sle 8 (WPVar w32 (i))))]

After generating the above interpolants, TX is switched to the Deletion for rest of the nodes and all the deletion interpolants are correct.

[ArpitaDutta]

Today when I started debugging this program, unfortunately, I am unable to get the crash by changing counter++ to counter= counter+1. Interpolants are same for both the versions by WP and Deletion.

[ArpitaDutta]

The oversubsumption problem is happening for for (int i = 0; i < 5; i++) and klee_assert(counter != 11); onwards.

Both WP Interpolation and Deletion interpolation are correctly finding the assertions for

1. for (int i = 0; i < 4; i++) and klee_assert(counter != 7);
2. for (int i = 0; i < 3; i++) and klee_assert(counter != 4);
3. for (int i = 0; i < 2; i++) and klee_assert(counter != 2);

I am trying to find the node with incorrect interpolant leading the oversubsumption.

[ArpitaDutta]

We are getting incorrect subsumption because only the value of variable 'i'is stored in the miu part. Somehow the value of the variable 'counter' is not stored. And this is causing the problem.

In deletion interpolation, we use coreValues.insert()to keep record of variables involved in the subsumption of a node. Later we use theinterpolateValues()and mark those variables.

Whereas on the wp-side, we are only storing the wp expression.

The variable 'counter' is considered as 'a non-interpolant value'on the wp-side at Node#6 (from its node->getStoredCoreExpressions). On the other hand, deletion interpolation is correctly storing the information for the variable as'a left and right interpolant value'.

This is happening because of the update performed for each TxStateValue responsible for the subsumption on the deletion side.

[ArpitaDutta]

To keep track of the variables present in the wp-interpolant during the subsumption which of the following options is better?

1. Creating a separate function to keep record of the variables?
2. Shifting the wp-subsumption check after the deletion checks.

[rasoolmaghareh]

So the summary of the discussion today was that we try to identify the places that .empty() is checked in the subsumed() function and ensure in all cases the markings are being passed to the parent nodes.

[ArpitaDutta]

As I can see that then even after disabling the empty() function, we are unable to correctly pass the markings. This is because the deletion interpolation checks for the concretely-addressed store and symbolically-addressed store of the present node and based on their values it updates the markings and passes them to the parent node. However, in our case both Node 7 and Node 8 have empty concretely-addressed store = [] and symbolically-addressed store = []. So ultimately we are still unable to pass the information to the parent.

Here is the link to the tree for our easy reference.

[rasoolmaghareh]

I think we need to move this to the partitioning function and perform this action before removing items from concretely-addressed store and symbolically-addressed store

[ArpitaDutta]

We can do this information transfer at this function

expr = wp->intersectWPExpr(branchCondition, childWPInterpolant[0],childWPInterpolant[1]);

where we decide to continue with wp-interpolation or switch to the deletion interpolation.

We will do this information transfer only when we are proceeding with the wp-interpolation.

[rasoolmaghareh]

sure, lets see if this fixes the issue.

[rasoolmaghareh]

Arpi tried a few changes and the program doesn't have oversubsumption. But we need to discuss the logic. Logic used:

Is this logic correct?

• Whenever we try to generate the WP intp. (in generateWPInterpolant() function) , for each variables used in WP intp., the logic marks those variables in the parent nodes.
• This is needed since at some point we give up the WP push up (since we can't push through a if-cond due to the abduction problem). At that point we need the marked variables to switch back to deletion interpolation.
• In general, we don't need to mark WP vars, but we need this when a node is subsumed and we need to switch to deletion at the parent node and we need to notify of its parent of the markings.

The logic seems correct, but let's verify it by running on some more tests and make sure that it does not cause over- or under-subsumption.

Note: Since this logic is complex, lets create a new PR for this change.

[ArpitaDutta]

I have implemented the above logic in this PR (marking_new_WP) a22b8d1.

[rasoolmaghareh]

I think you have pushed the branch and have not created the PR yet. Is that correct?

[ArpitaDutta]

Sorry. I missed that. Let me create the PR.