Simplifying failure modes in ExplodedNode creation

I described the direct consequences of removing the early return here: Issues with ExplodedNode deduplication ("caching out")


Commit e39bd407ba29c which has introduced this early return in 2015 claims that this is just a “defensive check to prevent accidental caching out”. For a long time I thought that the implementation is defective because the early return does not predict “caching out” accurately and often prevents the node creation in cases where caching out wouldn’t happen.

However, now I realized that this old commit (and perhaps other commits that modified the surrounding code?) accidentally introduced good logic which is important to prevent the creation of many irrelevant ExplodedNodes. (By the way note that the tempting “return the predecessor if node creation caches out” logic would be wrong and insufficient.) Now probably many checkers rely on this logic (presumably most of them began to do so after 2015), so instead of removing it, we should polish it into a clean and well-documented feature of CheckerContext.

The main idea is that a checker may have two reasons for adding a transition:

  1. sometimes it really needs the node (as the “anchor point” of a note tag or a bug report, or to sink a path);
  2. in many other cases the checker won’t use the node, but wants to record a state change.

When the checker doesn’t need the node and didn’t change the state, it should not create an ExplodedNode, because it has no reason to do so. (This improves the performance and acts as a workaround for Issues with ExplodedNode deduplication ("caching out") .)

Many checkers have logic that calculates a state change and produces a new State which is often but not always different from the old state. We could in theory introduce logic like if (State != OldState) C.addTransition(State) into these checkers – but it is very comfortable that now we can just write C.addTransition(State) and it will automatically “do the right thing”.

This feature is provided (or at least sufficiently approximated) by the early return in addTransitionImpl. Recall that this early return condition is:

if (!State || (State == Pred->getState() && !Tag && !MarkAsSink))          
      return Pred;
  • Here !Tag && !MarkAsSink covers the “doesn’t need the node” part:
    • an attached note tag would be a non-null Tag;
    • the methods that make error nodes[1] explicitly pass the checker as the tag to addTransitionImpl[2];
    • MarkAsSink is true when we want to sink a path.
  • State == Pred->getState() approximates the “didn’t modify the state” part: here Pred is the node passed to the CheckerContext constructor (while the parameter P of addTransitionImpl is the potentially more recent node that would be predecessor of the freshly created node), but often P == Pred and then this functions correctly.
  • !State is a mostly unrelated “did not manage to create a valid new state” failsafe. This is inelegant and could theoretically cause problems (e.g. if generateErrorNode would return the unrelated non-sink predecessor node), but is probably harmless in practice.

Based on these, I’m planning to implement the following changes:

  • (1) add accurate doc-comments;
  • (2) apply NFC changes to highlight the “methods that intend to make error nodes prevent the early return” logic (which is currently very easy to miss);
  • (3) use P (the argument of addTransitionImpl) instead of Pred (the node passed to the CheckerContext constructor) to guarantee that this logic also activates consistently when a checker makes multiple transitions;
  • (4) (probably) split off the !State condition into a separate early return that looks like if (!State) return nullptr; to avoid e.g cases when a checker would attach a bug report to a non-sink predecessor node.

(1) and (2) are easy NFC changes, (3) is a very low risk change (it only prevents the creation of nodes that don’t change the state and aren’t used for anything) and (4) is a bit more complex, but I would be careful to verify that every checker is prepared to receive a nullptr in this case[3].


  1. generateErrorNode, generateNonFatalErrorNode ↩︎

  2. The only difference between passing nullptr and the checker as the Tag is that the latter avoids the early return ↩︎

  3. btw addTransitionImpl can already return nullptr in rare cases, so a checker that is not prepared is already buggy ↩︎