This topic highlights and documents architectural issues; I don’t have immediate actionable suggestions. (However, feel free to suggest improvements, and I may also suggest some if I have any ideas.)
As I was inspecting the early return statement in CheckerContext::addTransitionImpl[1], I realized that the current node deduplication (“caching out”) logic is fragile.
The node deduplication logic ensures that when we reach the same exploded node again, the node creation methods like addTransition just add an edge to the graph and then return nullptr to abort the current symbolic execution path. This is very useful to save time: the analyzer can avoid traversing the same node series twice.
This would be justified in a simple engine that takes a node from the WorkList, computes its successors and immediately puts them back on the WorkList: here each node is created in the same context, so reaching the same node again cannot lead to new paths.
However, the static analyzer usually transitions through multiple steps before reaching a node that will be re-added to the WorkList, and if the same node is reached twice with different future (= remaining steps), then “caching out” is a mistake.
Theoretically speaking, the node deduplication should say that two nodes are different when
- (1) have different state; OR
- (2) have different metadata (e.g. one of them displays a note tag if it appears on a bug path); OR
- (3) have different future (i.e. the analyzer would execute the same checker callbacks and other steps to build the path after them).
Here (1) and (2) are already correct, but (3) is only approximated by the combination of:
- Nodes created in the engine are often distinguished by different
ProgramPoints. - Nodes created by checkers are tagged with the checker.
- Some nodes have ad hoc tags as concrete workarounds.
I don’t know about any case where this imperfect approximation causes actual buggy behavior[2], but we would see serious problems without the early return in addTransitionImpl (which, roughly speaking, prevents node creation when the state is identical to the state of the predecessor node).
When I disabled the early return, MallocChecker terminated a large fraction of execution paths with the following pattern:
- A
PreCallcallback ofMallocCheckeradds a transition to a node N1. - Some other checkers perform additional transitions, but none of them changes the state.
- A
PostCallcallback ofMallocCheckerperforms another transition, which again doesn’t change the state, so the node becomes a duplicate of N1 (same state, again tagged withMallocChecker) so the analyzer caches out.
At first I intended to replace the early return in addTransitionImpl with a more elegant “return the parent node if the freshly created node is a duplicate of its parent” logic. Unfortunately, this does not fix the problem: after node N1 was created by the PreCall of MallocChecker, other checkers transition to nodes that are different (have the same state, but different tag), and then the PostCall of MallocChecker still goes back to N1 (still the same state, now the tag is again MallocChecker and the node is different from its direct parent, but coincides with an earlier node).
It may be worth to tag checker created nodes with {checker, callback kind} pairs (instead of just the checker) to make the approximation of (3) more accurate. (We wouldn’t be able to remove the early return even with this change, because without the early return we would complicate the graph with many pointless identical-state transitions – however this would make the “caching out” logic theoretically more robust.)
I think this early return is problematic; my complaints are collected in in Simplifying failure modes in ExplodedNode creation ↩︎
This does not mean that there is no such buggy behavior: unjustified termination of certain analysis paths isn’t easy to spot unless it happens very often. ↩︎