Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses

TL;DR

The paper tackles precision loss in mixed flow-sensitive static analyses where globals are treated flow-insensitively. It introduces a generic, origin-aware update-rule framework with per-origin widening/narrowing, reluctant widening, and abstract garbage collection to recover precision without sacrificing termination. Through implementation in Goblint and extensive evaluation, the approach yields substantial precision gains on many tasks, including context-insensitive and context-sensitive analyses, while incurring manageable runtime and memory overheads and enabling significant trash removal in large benchmarks. This work advances practical techniques for refining global abstractions in multi-threaded and interprocedural settings, with implications for scalable and accurate static analysis. Key practical impact includes enabling finer-grained control over how partial flow-sensitivity contributes to globals, reducing false positives, and enabling incremental or incremental-like analyses through abstract garbage collection and per-origin strategies.

Abstract

Static analysis of real-world programs combines flow- and context-sensitive analyses of local program states with computation of flow- and context-insensitive invariants at globals, that, e.g., abstract data shared by multiple threads. The values of locals and globals may mutually depend on each other, with the analysis of local program states both making contributions to globals and querying their values. Usually, all contributions to globals are accumulated during fixpoint iteration, with widening applied to enforce termination. Such flow-insensitive information often becomes unnecessarily imprecise and can include superfluous contributions -- trash -- which, in turn, may be toxic to the precision of the overall analysis. To recover precision of globals, we propose techniques complementing each other: Narrowing on globals differentiates contributions by origin; reluctant widening limits the amount of widening applied at globals; and finally, abstract garbage collection undoes contributions to globals and propagates their withdrawal. The experimental evaluation shows that these techniques increase the precision of mixed flow-sensitive analyses at a reasonable cost.

Figures (7)

• Figure 1: Two scenarios involving trash. \ref{['fig:botnotprop']} displays the situation without abstract garbage collection. \ref{['fig:callcycle']} displays a case where abstract garbage collection fails. Hatched nodes represent unknowns that are trash. Arrows with double tips depict contributions to globals. Withdrawn contributions are dashed.
• Figure 2: Net precision difference to baseline for ReachSafety. All analyses are context-insensitive. The x-axis enumerates the $10042$ cases that run to completion for all four analyses. The cases are sorted by the net precision gain over the baseline. In some cases, the net precision difference flattens cases with improved and degraded or with incomparable unknowns. To visualize the effect on the plot, we include thin plots in which all flattened cases are assigned a net precision difference of zero, and shade the area between the two plots.
• Figure 3: Net precision difference to baseline for ReachSafety-Recursive. All analyses are context-insensitive.
• Figure 4: Precision differences for large multi-threaded programs compared to the baseline.
• Figure 5: Runtimes of the analyses of large, multi-threaded benchmarks.

Theorems & Definitions (18)

• Example 1.1
• Definition 2.1
• Definition 2.2
• Example 2.1
• Example 3.1
• Definition 3.1: Hosting Solver
• Definition 3.2: Sound Update Rule
• Theorem 3.3
• Example 4.1
• Example 4.2