Exact observable summaries (strongest necessary / weakest sufficient conditions) in path-sensitive static analysis: lifting the finitary-domain qualification for heap and other non-finite abstraction domains

A 2008 result by Dillig, Dillig and Aiken — 'Sound, complete and scalable path-sensitive analysis' (PLDI 2008), condensed in the CACM 2010 Research Highlights article 'Reasoning about the unknown in static analysis' — made interprocedural, path-sensitive program summaries exact: statically unknown values (user input, network data, OS state) are modeled as fresh non-deterministic choice variables, and a fixed-point elimination computes, for every function and property, a bracketing constraint consisting of the strongest necessary condition (SNC) and weakest sufficient condition (WSC) over observable (summarizable) variables, so that all may and must queries are answered exactly relative to the chosen abstraction. That exactness rests on qualifications the authors state themselves: completeness is guaranteed only when the base domain of abstract values is finite — more generally finitary, finite for the given program — and the technique 'is not complete for arbitrary non-finite domains', with shape properties of the heap the canonical exclusion; separately computed per-property summaries cannot be conjoined precisely, because SNCs do not distribute over conjunctions, and the authors' remedy is to compute SNCs and WSCs for the combined property; the results 'are generally qualified by an assumption that the program terminates', leaving the $\bot$/$\top$ fixed-point semantics of nontermination unhandled; and the smallness of the solved forms is demonstrated only experimentally. Of these qualifications the authors single out exactly one item as future work: 'Saturn does not have a sophisticated shape analysis; hence, the overwhelming majority (> 95%) of errors reported for elements of unbounded data structures are false positives. However, shape analysis is an orthogonal problem; we leave incorporating shape analysis as future work.' No known method computes exact observable SNC/WSC summaries for heap/shape or other nonfinitary domains, which is the gap this task addresses. The problem — extending exact observable-summary computation to nonfinitary domains, heap/shape being the instance the authors left open, or precisely delimiting which nonfinitary domains admit no such exact summaries — remains open.

Background

Static analysis infers properties of a program that hold for all possible inputs without executing it. A sound analysis never misses a real error but must approximate program behavior, and approximation produces false positives — spurious warnings about correct code — so a central goal is analyses that are simultaneously sound, precise, and scalable to millions of lines of code. Precision is lost whenever the analysis cannot distinguish different execution histories: an analysis is path-sensitive if it tracks facts separately along different branches (for example, recording under which condition a pointer is dereferenced, not merely that it may be), and context-sensitive if it distinguishes different call sites of a function. Path sensitivity compounds across function boundaries: the number of path conditions grows with the program, and a scalable analysis instead summarizes each function — a procedure summary is a compact description of the function's effect reusable at every call site.

Dillig, Dillig and Aiken's PLDI 2008 paper (condensed in the CACM 2010 Research Highlights article) made such summaries exact for a large class of properties, implemented in Saturn, a constraint-based bug finder for C programs. Statically unknown values — user input, data from the network, operating-system state — are modeled as choice variables: fresh non-deterministic variables, one per occurrence, so that the analysis can recognize when two reads return the same unknown value. Constraint generation then yields, for each function $f$ and abstract value $C_i$ of a finite abstraction, a recursive constraint $\Pi_{f,\alpha,C_i}$ expressing the condition under which $f$ returns $C_i$. The paper separates observable variables (parameter and return abstractions, which a summary may mention) from choice variables (which a summary may not mention, since every call introduces fresh ones and the system would otherwise not converge). Choice variables are eliminated by computing for each constraint its strongest necessary condition — the logically strongest formula over observable variables that the constraint implies — and its weakest sufficient condition — the logically weakest observable formula that implies it. These notions go back to Boole's technique of eliminating the middle term and were studied for fragments of first-order logic by Lin (2001); the source's contribution is computing them for the solution of recursive constraint systems. The result is a bracketing constraint $\langle \varphi_{NC}, \varphi_{SC} \rangle$ per function and property that answers every may query ('can $f$ return $C_i$ under observable condition $\varphi_{NC}$?') and must query ('must it, given $\varphi_{SC}$?') exactly, relative to the initial abstraction — sound and complete path-sensitive analysis that ran on the entire Linux kernel: in the null-dereference experiment on Linux 2.6.17.1, the same 134 real bugs were reported with only 37 false positives, versus 1344 for the baseline that tracks path conditions only within each function.

The exactness carries qualifications that the papers state themselves. First, the abstraction must be finitary — finite, or at least finite for each given program — because the reduction to boolean constraints and the convergence of the fixed-point elimination rely on enumerating abstract values; 'the proposed technique is not complete for arbitrary non-finite domains', and shape properties of the heap (the graph structure of pointers: aliases, points-to relations, inductive data types like linked lists) are the canonical exclusion, with arbitrary arithmetic in path constraints a second instance where the technique 'may fail to compute the strongest necessary and weakest sufficient conditions'. Second, strongest necessary conditions do not distribute over conjunctions (dually, weakest sufficient conditions do not distribute over disjunctions), so separately computed summaries for two properties $P_1$ and $P_2$ cannot be conjoined into a precise summary of $P_1 \wedge P_2$; a combined property must be re-analyzed wholesale. Third, the constraint semantics uses a four-point lattice in which $\bot$ in the least-fixed-point reading and $\top$ in the greatest-fixed-point reading both represent nontermination, and the results 'are qualified by the assumption that the program terminates' — the summaries are not guaranteed sound for nonterminating behaviors. Fourth, the solved forms were observed only empirically to be small (about 95% of conditions had fewer than five subclauses, and their sizes did not grow with program size), with no theoretical explanation of why; the papers' only theoretical size remark is the worst-case note that the strongest necessary and weakest sufficient conditions of a formula 'may double the size of the original formula'. Finally, the evaluation excluded array elements and recursive fields of data structures because Saturn lacked a shape analysis, whose integration the authors left as future work; since shape properties constitute a non-finitary domain, this is the concrete instance of the first qualification.

Problem Statement

The problem is to extend, or precisely delimit, exact observable-summary computation for path- and context-sensitive static analysis — the strongest-necessary/weakest-sufficient-condition (SNC/WSC) bracketing-constraint technique of Dillig, Dillig and Aiken — beyond the finitary-domain restriction under which its completeness is currently valid. This is the item the authors themselves leave open: completeness 'is only guaranteed if the base domain of abstract values is finite', so that for infinite domains the method 'is still sound, but not necessarily complete' and applies to typestate, type qualifier or dataflow properties 'but not, for example, arbitrary shape properties'; the CACM Limitations section states that 'the proposed technique is not complete for arbitrary non-finite domains'; and the evaluation reports that 'Saturn does not have a sophisticated shape analysis; hence, the overwhelming majority (> 95%) of errors reported for elements of unbounded data structures are false positives. However, shape analysis is an orthogonal problem; we leave incorporating shape analysis as future work.' Since shape properties constitute a nonfinitary domain, heap/shape is the concrete instance of the restriction. Concretely, the objective is:

Give a method that, for heap/shape properties (the graph structure of pointers: aliases, points-to relations, inductive data types such as linked lists) or for a characterized class of nonfinitary abstraction domains that includes them, computes sound and relatively complete observable summaries — bracketing constraints $\langle \varphi_{NC}, \varphi_{SC} \rangle$ over observable variables, with choice variables eliminated, that answer every may and must query exactly relative to the chosen abstraction — with finite representations; or establish which nonfinitary domains provably admit no such exact finite summaries and which do, with heap/shape properties classified by that delimitation. Either alternative, taken by itself, resolves the task: a method for heap/shape properties alone suffices (the 'characterized class of nonfinitary abstraction domains' phrasing widens that alternative but is not a separate requirement), and a delimitation of which nonfinitary domains admit exact finite summaries and which provably do not likewise suffices on its own; a solution need not pursue both alternatives.

The source states three further qualifications of the technique. (a) Single properties: strongest necessary conditions do not distribute over conjunctions (dually, weakest sufficient conditions do not distribute over disjunctions), so separately computed summaries for $P_1$ and $P_2$ do not yield a precise summary of $P_1 \wedge P_2$; the authors' stated remedy is that 'if one is interested in combining reasoning about two distinct properties, it is necessary to compute strongest necessary and weakest sufficient conditions for the combined property'. (b) Termination: 'we do not attempt to reason about termination, and our results are generally qualified by an assumption that the program terminates', the $\bot$/$\top$ (least versus greatest fixed-point) readings of nontermination being unhandled. (c) Size: the smallness of the solved forms is demonstrated experimentally, the only theoretical remark being the worst-case note that SNC/WSC elimination may double the size of a formula. They are context only: a solution must state how its method or delimitation interacts with (a) and (b) — whether summaries are computed one property at a time, and under which fixed-point reading they are exact — but need not resolve (a), (b), or (c).

The original framing of the open item was tool-specific — composing a shape analysis with the choice-variable elimination inside Saturn — and Saturn is no longer maintained; the objective above is its general form, exact observable summaries for heap/shape and other nonfinitary domains. Later modular heap analyses address parts of the heap facet without exactness guarantees.

References

1. Isil Dillig, Thomas Dillig, Alex Aiken. Sound, complete and scalable path-sensitive analysis. In Proc. 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2008, pages 270-280. DOI 10.1145/1375581.1375615. https://doi.org/10.1145/1375581.1375615
2. Isil Dillig, Thomas Dillig, Alex Aiken. Reasoning about the unknown in static analysis. Communications of the ACM 53(8):115-123, 2010. DOI 10.1145/1787234.1787259. https://doi.org/10.1145/1787234.1787259
3. Isil Dillig, Thomas Dillig, Alex Aiken. Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis. In Proc. 17th International Static Analysis Symposium (SAS), 2010, pages 236-252. DOI 10.1007/978-3-642-15769-1_15. https://doi.org/10.1007/978-3-642-15769-1_15
4. Isil Dillig, Thomas Dillig, Alex Aiken, Mooly Sagiv. Precise and compact modular procedure summaries for heap manipulating programs. In Proc. 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2011, pages 567-577. DOI 10.1145/1993498.1993565. https://doi.org/10.1145/1993498.1993565
5. Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Alex Aiken. Minimum Satisfying Assignments for SMT. In Proc. 24th International Conference on Computer Aided Verification (CAV), 2012, pages 394-409. DOI 10.1007/978-3-642-31424-7_30. https://doi.org/10.1007/978-3-642-31424-7_30
6. Isil Dillig, Thomas Dillig, Alex Aiken. Automated error diagnosis using abductive inference. In Proc. 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2012, pages 181-192. DOI 10.1145/2254064.2254087. https://doi.org/10.1145/2254064.2254087
7. Cristiano Calcagno, Dino Distefano, Peter O'Hearn, Hongseok Yang. Compositional shape analysis by means of bi-abduction. In Proc. 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2009, pages 289-300. DOI 10.1145/1480881.1480917. https://doi.org/10.1145/1480881.1480917
8. Bhargav S. Gulavani, Supratik Chakraborty, G. Ramalingam, Aditya V. Nori. Bottom-Up Shape Analysis. In Proc. 16th International Static Analysis Symposium (SAS), 2009, pages 188-204. DOI 10.1007/978-3-642-03237-0_14. https://doi.org/10.1007/978-3-642-03237-0_14
9. Byron Cook, Andreas Podelski, Andrey Rybalchenko. Summarization for termination: no return! Formal Methods in System Design 35(3):369-387, 2009. DOI 10.1007/s10703-009-0087-8. https://doi.org/10.1007/s10703-009-0087-8
10. Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, Sai Deep Tetali. Compositional may-must program analysis: unleashing the power of alternation. In Proc. 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2010, pages 43-56. DOI 10.1145/1706299.1706307. https://doi.org/10.1145/1706299.1706307
11. Fangzhen Lin. On strongest necessary and weakest sufficient conditions. Artificial Intelligence 128(1-2):143-159, 2001. DOI 10.1016/S0004-3702(01)00070-4. https://doi.org/10.1016/S0004-3702(01)00070-4
12. Markus Müller-Olm, Helmut Seidl. Precise interprocedural analysis through linear algebra. In Proc. 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2004, pages 330-341. DOI 10.1145/964001.964029. https://doi.org/10.1145/964001.964029
13. Narges Khakpour, Nicolas Berthier. Symmaries: Automatic Inference of Formal Security Summaries for Java Programs. arXiv:2512.20396, 2025. https://arxiv.org/abs/2512.20396