Resetting WP Interpolant for assertion failure/memory error

[ArpitaDutta]

At present, the wp-interpolant is set as true even when we hit an error/failure for a node. In the last to last meeting, we decided to reset the value of the wp-interpolant to false whenever reach a failure.

For to achieve this, in TxTree::remove() function, before TxSubsumptionTable::insert(node->getProgramPoint(),node->entryCallHistory, entry);, I have reset the wp-interpolant value based on the assert failure value of that node.

if (WPInterpolant) {
  ref<Expr> WPExpr = entry->getWPInterpolant();
    if (!WPExpr.isNull()) {
        entry = node->wp->updateSubsumptionTableEntry(entry);
    }
    if(node->assertionFail){
        ref<Expr> resetWPExpr = ConstantExpr::alloc(0, Expr::Bool);
        entry->setWPInterpolant(resetWPExpr);
    }
  }

[ArpitaDutta]

Made this change in commit 9f3e629.

[rasoolmaghareh]

should we close this issue?

[ArpitaDutta]

I wanted to discuss a few things regarding this change.

With this change, we are not able to subsume any other path with the same assertion violation. Every assert_failure has a separate path.

We are expecting this behavior only. Am I correct?

[rasoolmaghareh]

Comment from Arpi:

After resetting WP Interpolant for assertion failure/memory error to false, "wp interpolant = [false]", we are not subsuming other nodes with the same assertion violation at the same program point. Each assert_failure leads to a separate path. For example, in the tree [tree_with-Assert-Update.pdf], node#14 is not getting subsumed by node#11 by setting wp interpolant = [false] for node #11. tree_without-Assert-Update.pdf presents the tree when the wp interpolant = [] and node#14 is subsumed by node#11. We are expecting the behavior of the Tracerx as shown in tree_with-Assert-Update.pdf. Please let me know if I am missing something. tree_with-Assert-Update.pdf tree_without-Assert-Update.pdf

[rasoolmaghareh]

This is intended behaviour, one of the cases emits all occurances of an error and the other emits only the first occurance of an error. We have a command-line option which toggles this off/on on deletion. We can use the same command-line option here too.

[ArpitaDutta]

Are you suggesting for this option -emit-all-errors-in-same-path? By default this option is off. It has separate computation of the number of error paths.

[ArpitaDutta]

In my opinion this commit https://github.com/tracer-x/TracerX/commit/9f3e629fbd06733a7f1a79b3a23f82b000c45609 will increase a bit of run-time by ignoring the subsumption of a error path starting from the same program point for which earlier a error is reported.

Can we disable this commit for our test-comp submission?

[rasoolmaghareh]

sure.

[ArpitaDutta]

I am disabling this commit and let you know once this branch is ready for the MR.

[ArpitaDutta]

I have made the changes in commit 1d5f8d3.