Path Sensitivity and the Cost of Remembering Branch Conditions

Consider a function that checks two fields of a request object. If the request has a body, it also has a content type; the code tests both and dereferences the body only when both are present. A path-insensitive analysis that tracks each flag independently will consider the state “body present, content type absent” reachable, because each value is possible somewhere. That state cannot occur. Every report derived from it is a false positive, and no amount of rule tuning removes it.

One state per point is an abstraction

A flow-sensitive analysis associates a state with each program point. At a branch, the precise thing to do is fork: one state in which the condition is true, one in which it is false. If both forks are carried forward separately, the analysis is path-sensitive. If they are merged immediately with a join, the analysis is path-insensitive with respect to that branch. The join itself follows the lattice rules in Monotone Dataflow and Fixpoint Convergence; path sensitivity is a choice about how much of that lattice is kept disjunctive.

Merging is cheap and loses information. The join of the state where body != null and the state where body == null is a state in which body is “maybe null”. That is enough to answer “can this dereference be null” with a maybe, but not enough to answer “is this dereference definitely safe”. The distinction matters: a rule that reports only definite null dereferences will miss the bug, and a rule that reports possible ones will report the safe code too.

Correlation is the deeper loss. Suppose two variables are assigned together:

if has_body:
    body = read_body()
    content_type = read_type()
if has_body and content_type is not None:
    parse(body, content_type)

Merging after the first block yields a state where has_body is true and content_type is null, even though the assignment order makes that combination impossible. A path-sensitive analysis that forks on has_body keeps the two paths separate and never forms the impossible state.

Splitting paths is easy; bounding them is not

The direct implementation is a symbolic executor. The state carries a path condition, a formula over program inputs and program variables that is true exactly on the paths that reach the point. A branch conjoins the branch condition or its negation. A feasibility check against a decision procedure prunes infeasible paths. A dereference check asks whether the path condition implies the pointer is non-null.

Without pruning, the number of paths through a function with n sequential branches is 2^n in the worst case, and loops make it unbounded. Real code has far more branches than any budget allows, so every practical tool imposes a cutoff. The common strategies are:

• Depth limiting: explore paths up to a fixed number of branch decisions, then merge or abandon.
• Loop unrolling: execute a loop body a fixed number of times and then apply a summary or a widening operator.
• State merging with constraints: keep disjunctions of path conditions but simplify them, accepting a larger formula in exchange for fewer states.
• Selective splitting: fork only on conditions the analysis cares about, such as null checks or type tests, and merge on everything else.

Each strategy trades precision for a bound. Unrolling twice and then joining the loop state is sound for may properties if the join over-approximates, but it loses the correlation between the loop counter and the data, which is often exactly what a rule needs.

Widening is the standard way to terminate on loops in abstract interpretation. When a fixpoint iteration detects that a value is growing without bound, it jumps to a coarser element, such as the whole type’s range, and continues. The jump guarantees termination but discards the relationship that made the precise value useful. A nullness analysis that widens a field from “non-null” to “maybe null” after a loop may then report every use after the loop, even when the loop body is known to preserve non-nullness.

Predicate abstraction keeps the facts that matter

Predicate abstraction is a middle path. Instead of tracking the full state, the analysis tracks the truth value of a finite set of predicates chosen in advance: x != null, i < n, state == OPEN. The abstract state is a bit vector over those predicates, and a decision procedure computes the strongest postcondition of a statement in terms of them.

The join of two abstract states keeps only the predicates that are true in both. That is still a loss of correlation, but the loss is confined to the predicates the analysis chose. If the predicate set includes the pair that matters, the analysis can prove the property; if it does not, the analysis is blind to it. Choosing predicates is therefore a manual or semi-automatic design step, and it is where most of the engineering effort goes.

The abstraction is also where the cost lives. Each transfer function requires a satisfiability query, and each query can be expensive. A tool that issues a query per statement on a large codebase will spend most of its time in the solver, which is why practical analyzers cache query results, simplify formulas before sending them, and restrict the theory to the fragment the solver handles well.

Relational domains encode arithmetic correlations

For numeric properties, the correlation can be captured without enumerating paths by using a relational domain. An interval domain tracks a lower and upper bound per variable but cannot express y > x. The octagon domain adds constraints of the form ±x ± y ≤ c, which is enough for many bounds checks and array index proofs. Polyhedra generalise to arbitrary linear inequalities, at a cost that grows quickly with the number of variables.

These domains are attractive because they are closed under join and include efficient algorithms for the operations the fixpoint needs. The join of two octagons is the smallest octagon containing both, which is a convex hull in that domain. The catch is that the convex hull of two paths can include points that neither path reaches, so the analysis remains sound but loses disjunctive information. A check that holds on both branches may fail to be proved on the hull, or a bug that exists on one branch may be masked by the hull.

# Two path states for the same variable, then their join.
state_true  = {"x": ("const", 1)}
state_false = {"x": ("const", 2)}
joined = {"x": ("range", 1, 2)}   # correlation with the branch condition is gone

The snippet is deliberately small: the join keeps the range but drops the fact that the branch condition determines which end applies. Any later check that needs that implication must either keep the paths separate or add the condition as a predicate.

What the cutoff costs in both directions

Every precision decision has a failure mode in each direction. Splitting too little produces false positives from infeasible states, which is the dominant complaint about path-insensitive analyzers, and the reason The Structure of False Positives treats infeasible paths as a structural source rather than a bug. Splitting too much produces timeouts and, worse, unsound pruning: if a tool gives up on an infeasible path by assuming it is infeasible without proof, it can miss a real bug. The distinction between “infeasible” and “not proved feasible” must be explicit in the implementation, because collapsing the two turns a conservative analysis into an unsound one.

A second failure mode is the environment. A path condition that assumes a function argument is non-null is only valid if every caller respects that assumption. Without interprocedural summaries, which are the subject of Interprocedural Summaries and Context Sensitivity, the analysis either assumes the best and risks unsoundness or assumes the worst and loses precision at every call.

The practical shape of a path-sensitive linter is therefore a budgeted search: split on the conditions that the rule names, merge elsewhere, widen loops, cache solver results, and record when the budget was exhausted so that a “no finding” result can be distinguished from “not analyzed”. That last distinction is what separates a tool whose silence means something from one whose silence means nothing.