lemmaLemma[section] theoremTheorem[section]

# Demanded Abstract Interpretation (Extended Version)

Benno Stein  University of Colorado Boulder<EMAIL_ADDRESS>,  Bor-
Yuh Evan Chang  0000-0002-1954-0774 University of Colorado BoulderAmazon
<EMAIL_ADDRESS>and  Manu Sridharan  0000-0001-7993-302X University of
California, Riverside<EMAIL_ADDRESS>
(2021)

###### Abstract.

We consider the problem of making expressive static analyzers _interactive_.
Formal static analysis is seeing increasingly widespread adoption as a tool
for verification and bug-finding, but even with powerful cloud infrastructure
it can take minutes or hours to get _batch_ analysis results after a code
change. While existing techniques offer some demand-driven _or_ incremental
aspects for certain classes of analysis, the fundamental challenge we tackle
is doing both for arbitrary abstract interpreters.

Our technique, demanded abstract interpretation, lifts program syntax and
analysis state to a dynamically evolving graph structure, in which program
edits, client-issued queries, and evaluation of abstract semantics are all
treated uniformly. The key difficulty addressed by our approach is the
application of general incremental computation techniques to the complex,
cyclic dependency structure induced by abstract interpretation of loops with
widening operators. We prove that desirable abstract interpretation meta-
properties, including soundness and termination, are preserved in our
approach, and that demanded analysis results are equal to those computed by a
batch abstract interpretation. Experimental results suggest promise for a
prototype demanded abstract interpretation framework: by combining incremental
and demand-driven techniques, our framework consistently delivers analysis
results at interactive speeds, answering 95% of queries within 1.2 seconds.

Abstract interpretation, Incremental computation, Demand-driven query
evaluation, Demanded fixed points

††copyright: rightsretained††doi: 10.1145/3453483.3454044††journalyear:
2021††submissionid: pldi21main-p111-p††isbn:
978-1-4503-8391-2/21/06††conference: Proceedings of the 42nd ACM SIGPLAN
International Conference on Programming Language Design and Implementation;
June 20–25, 2021; Virtual, Canada††booktitle: Proceedings of the 42nd ACM
SIGPLAN International Conference on Programming Language Design and
Implementation (PLDI ’21), June 20–25, 2021, Virtual, Canada††ccs: Theory of
computation Program analysis††ccs: Software and its engineering Formal
software verification

##  1\. Introduction

Static analysis is seeing increasing real-world adoption for verification and
bug finding, particularly as part of continuous integration (CI) and code
review processes (DBLP:conf/nfm/CalcagnoD11;
DBLP:journals/cacm/SadowskiAEMJ18). However, a pain point with these
deployments is that developers cannot get quick local analysis results for
code they are editing; ideally, updated results would appear nearly instantly
in their IDE. In this paper, we present an interactive analysis engine
designed to handle local queries and edits efficiently, which can complement a
batch engine that exhaustively analyzes a fixed program, for example by
quickly verifying whether a local change silences an alarm raised in CI.

The well-known techniques of demand-driven analysis and incremental analysis
help address this challenge. Demand-driven analyses compute only those results
needed to answer a set of extrinsicially-provided _queries_ , while
incremental analyses speed up re-analysis of an _edited_ program by re-using
as many previously-computed results as possible.

Powerful frameworks for incremental (e.g., (DBLP:conf/kbse/SzaboEV16;
DBLP:conf/icse/ArztB14)) _or_ demand-driven (e.g.,
(DBLP:conf/sigsoft/HorwitzRS95)) static analysis do exist, but nearly all such
frameworks target restricted analysis domains (e.g., finite or finite-height
domains), whereas well-known analyses like octagon and shape analysis require
an infinite-height abstract domain. There are also approaches to adapt
summary-based analyses to offer coarse-grained method- or file-level
incrementality (e.g., (DBLP:conf/nfm/CalcagnoD11;
DBLP:journals/cacm/DistefanoFLO19; DBLP:conf/foveoos/FahndrichL10)). Though
these approaches effectively scale to industrial codebases in CI pipelines,
they are not intended to achieve real-time interactivity during the
development process.

In contrast, our aim is to support fine-grained incremental and demand-driven
analysis over _arbitrary_ abstract domains expressed in general-purpose
languages, thus enabling the reuse of existing optimized abstract domain
implementations at interactive speeds. To our best knowledge, no general
technique exists to automatically compute a demand-driven or incremental
version of an arbitrary abstract interpretation with arbitrary widening
operators, a key requirement to ensure termination in more complex analyses.

This paper presents _demanded abstract interpretation_ , an abstract
interpretation framework with first-class support for both demand-driven and
incremental analysis. We build on abstract interpretation
(DBLP:conf/popl/CousotC77), which provides a methodology for expressing static
analyses and guaranteeing their correctness, and take inspiration from work on
general incremental computation using “demanded computation graphs”
(DBLP:conf/pldi/HammerKHF14).

Our framework reifies the abstract interpretation (AI) of a program as a
dynamically evolving _demanded abstract interpretation graph_ (DAIG), which
explicitly represents program statements, abstract states, and the dependency
structure of analysis computations. In this representation, program edits,
client-issued queries, and the evaluation of abstract semantics can all be
treated uniformly. Cyclic control flow is a key difficulty for this approach,
since cyclic dependencies lead to unclear evaluation semantics. We define an
operational semantics for DAIGs that preserves an acyclic invariant while
modifying and extending the graph on demand, thus soundly analyzing loops with
guaranteed termination, assuming termination of the underlying abstract
interpretation.

The DAIG encoding and evaluation enables efficient abstract interpretation in
an interactive mode, analyzing a minimal number of statements to respond to
queries with maximal reuse of previously-computed results. In particular, this
paper makes the following key contributions:

  * •

We introduce a framework for demanded abstract interpretation in which program
syntax and analysis computation structure are reified into demanded abstract
interpretation graphs (DAIGs) (Section 4).

  * •

We specify an operational semantics for DAIGs that realizes incremental
updates and demand-driven evaluation via demanded unrolling of abstract
interpretation fixed-point computations (Section 5).

  * •

We prove that demanded abstract interpretation preserves soundness and
termination, and that its results are from-scratch consistent with classical
abstract interpretation by global fixed-point iteration (Section 6).

  * •

We provide evidence for the expressivity and efficacy of demanded abstract
interpretation using a prototype framework instantiated with interval,
octagon, and shape domains (Section 7). In our experiments, DAIGs support
context-sensitive interprocedural analysis at interactive speeds, answering
95% of queries within 1.2 seconds.

##  2\. Overview

Fig. 1 shows a simple imperative program that appends two linked lists. Given
well-formed (i.e., null-terminated and acyclic) input lists p and q, append
must return a well-formed list and not dereference null in order to be
correct. These properties can be verified using a separation logic, abstract
interpretation-based shape analysis (DBLP:conf/fmco/BerdineCO05;
DBLP:conf/tacas/DistefanoOY06; magill2006inferring), tracking facts like
$\texttt{\small lseg}(p,null)$ to represent well-formedness of list p. Our
goal is to enable interactive performance for arbitrary abstract
interpretations, including such analyses, in response to a user’s edits and
queries.

In this section, we illustrate our approach to _demanded abstract
interpretation_ by example. We demonstrate how abstract interpretation of
forwards control flow is reified in a DAIG (Section 2.1), and then show how
the DAIG supports both demand-driven and incremental interactions with the
underlying abstract interpretation (Section 2.2). Finally, we highlight key
difficulties introduced by cyclic control flow, show how analysis thereof can
be encoded acyclically, and demonstrate how our operational semantics evolve
the DAIG on-demand to soundly compute fixed points (Section 2.3).

###  2.1. Reifying Abstract Interpretation in DAIGs

The append procedure from Fig. 1 may equivalently be represented as a control-
flow graph (CFG) as shown in Fig. 2, with vertices for program locations and
edges labelled by atomic program statements.111As is standard, we have simply
broken down the guard conditions from if and while into assume guard
statements for each side of a branch. A classical abstract interpreter
analyzes such a program by starting with some initial abstract state at the
entry location and applying an abstract transfer function
$\llbracket\cdot\rrbracket^{\sharp}$ to interpret statements, a join operator
$\sqcup$ at nodes with multiple predecessors, and a widen operator $\nabla$ at
cycles as needed until a fixed point is reached.

⬇

function append(p: List, q: List): List { $\lst@savelstnumber=-1$

$\ell_{1}$ if (p == null) {

$\ell_{2}$ return q; }

$\ell_{3}$ var r: List = p;

$\ell_{4}$ while (r.next != null) {

$\ell_{5}$ r = r.next; }

$\ell_{6}$ r.next = q;

$\ell_{7}$ return p;

$\ell_{\text{ret}}$}

Figure 1. A procedure to append two linked lists. The labels $\ell_{i}$ mark
program locations in its control flow.
$\ell_{0}$$\ell_{2}$$\ell_{3}$$\ell_{5}$$\ell_{6}$$\ell_{\tiny\textsf{ret}}$$\ell_{1}$$\ell_{4}$assumep
== null;assumep != null;r = p;assumer.next == null;r.next = q;ret =
p;assumer.next != null;r = r.next;ret = q; Figure 2. The control-flow graph
(CFG) of the append procedure from Fig. 1.  assume p == null;
$\underline{\ell_{0}}\\!\cdot\\!\underline{\ell_{1}}$ $\varphi_{0}$
$\underline{\ell_{0}}$ assume p != null;
$\underline{\ell_{0}}\\!\cdot\\!\underline{\ell_{2}}$ $\underline{\ell_{1}}$r
=
p;$\underline{\ell_{2}}\\!\cdot\\!\underline{\ell_{3}}$$\underline{\ell_{2}}$
ret = q;
$\underline{\ell_{1}}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$Elided
encoding of the$\ell_{3}$-to-$\ell_{4}$-to-$\ell_{3}$ loop
body$\underline{1}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$assumer.next
==
null;$\underline{\ell_{3}}\\!\cdot\\!\underline{\ell_{5}}$$\underline{\ell_{5}}$r.next
=
q;$\underline{\ell_{5}}\\!\cdot\\!\underline{\ell_{6}}$$\underline{\ell_{6}}$ret
=
p;$\underline{\ell_{6}}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$$\underline{2}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$$\underline{\ell_{\tiny\textsf{ret}}}$$\llbracket\cdot\rrbracket^{\sharp}$$\llbracket\cdot\rrbracket^{\sharp}$$\llbracket\cdot\rrbracket^{\sharp}$$\llbracket\cdot\rrbracket^{\sharp}$$\llbracket\cdot\rrbracket^{\sharp}$
$\llbracket\cdot\rrbracket^{\sharp}$$\llbracket\cdot\rrbracket^{\sharp}$$\sqcup$
Figure 3. A demanded abstract interpretation graph (DAIG) for the program
given in Fig. 1 before any queries are issued. The elided loop encoding is
shown in Fig. 4(c).

The demanded abstract interpretation graph (DAIG) shown in Fig. 3 reifies the
computational structure of such an abstract interpretation of the Fig. 2 CFG.
Its vertices are uniquely-named mutable reference cells containing program
syntax or abstract state, and its edges fully specify the computations of an
abstract interpretation. Names identify values for reuse across edits and
queries, and hence must uniquely identify the inputs and intermediate results
of the abstract interpretation. In Fig. 3 and throughout this paper,
underlined symbols denote a name derived from that symbol: hashes,
essentially.

To encode abstract interpretation computations, DAIG edges are labelled by a
symbol for an abstract interpretation function and connect cells storing the
function inputs to the cell storing the output, capturing the dependency
structure of the analysis computation.222More precisely, DAIGs have hyper-
edges, since they connect multiple sources (function inputs) to one
destination (function output). For example, the computation of the abstract
transfer function over the CFG edge $\ell_{0}\rightarrow\ell_{1}$ is encoded
in Fig. 3 as a DAIG edge with input cells $\underline{\ell_{0}}$ and
$\underline{\ell_{0}}\cdot\underline{\ell_{1}}$ (respectively containing the
fixed-point state at $\ell_{0}$ and the corresponding statement
${s_{0}\colon\leavevmode\hbox{\set@color\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{assume}}({\@listingGroup{ltx_lst_identifier}{p}}{\@listingGroup{ltx_lst_space}{
}}=={\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{null}})}}}}$), labelled by the abstract
transfer function symbol $\llbracket\cdot\rrbracket^{\sharp}$.

###  2.2. Demand-Driven and Incremental Analysis

Next, we demonstrate how a DAIG encoding naturally supports demand-driven and
incremental analysis. We use the aformentioned shape-analysis domain for our
example, a separation logic-based domain with a “list segment” primitive
$\texttt{\small lseg}(x,y)$ that abstracts the heaplet containing a list
segment from $x$ to $y$.333That is, a sequence of iterated next pointer
dereferences from $x$ to $y$. This domain is of infinite height, absent a best
abstraction function, and with complex widening operators, and therefore
incompatible with previous frameworks that restrict the domain form.

assume p == null; $\underline{\ell_{0}}\\!\cdot\\!\underline{\ell_{1}}$
$\varphi_{0}\colon\begin{array}[]{@{}l@{}}\texttt{lseg}(\texttt{q},\textit{null})\,\ast\\\
\texttt{lseg}(\texttt{p},\textit{null})\end{array}$ $\underline{\ell_{0}}$
$\begin{array}[]{@{}l@{}}\texttt{lseg}(\texttt{q},\textit{null})\\\
\wedge~{}\texttt{p}=\textit{null}\end{array}$ $\underline{\ell_{1}}$ ret = q;
$\underline{\ell_{1}}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$
$\begin{array}[]{@{}l@{}}\texttt{lseg}(\texttt{ret},\textit{null})\\\
\wedge~{}\texttt{p}=\textit{null}\end{array}$
$\underline{1}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$$\llbracket\cdot\rrbracket^{\sharp}$$\llbracket\cdot\rrbracket^{\sharp}$

(a) Demand-driven query

$\varphi$ $\underline{\ell_{1}}$ print("p
is null"); $\underline{\ell_{1}}\\!\cdot\\!\underline{\ell_{7}}$
$\underline{\ell_{7}}$ $\varphi^{\prime}$
$\underline{1}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$
$\underline{2}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$
$\varphi^{\prime\prime}$ $\underline{\ell_{\tiny\textsf{ret}}}$ ret = p;
$\underline{\ell_{7}}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$$\vdots$$\vdots$$\llbracket\cdot\rrbracket^{\sharp}$$\llbracket\cdot\rrbracket^{\sharp}$$\sqcup$

(b) Incremental edit

$\underline{\ell_{3}}^{\hskip 0.28001pt(0)}$assumer.next !=
null;$\underline{\ell_{3}}\\!\cdot\\!\underline{\ell_{4}}$r =
r.next;$\underline{\ell_{4}}\\!\cdot\\!\underline{\ell_{3}}$$\underline{\ell_{4}}^{\hskip
0.28001pt(0)}$$\underline{\ell_{3}}^{\hskip 0.28001pt(0)}$$\\!\cdot\\!$
$\underline{\ell_{3}}^{\hskip 0.28001pt(1)}$$\underline{\ell_{3}}^{\hskip
0.28001pt(1)}$ $\underline{\ell_{4}}^{\hskip 0.28001pt(1)}$
$\underline{\ell_{3}}^{\hskip 0.28001pt(1)}$$\\!\cdot\\!$
$\underline{\ell_{3}}^{\hskip 0.28001pt(2)}$ $\underline{\ell_{3}}^{\hskip
0.28001pt(2)}$$\underline{\ell_{3}}$$\vdots$$\vdots$$\llbracket\cdot\rrbracket^{\sharp}$$\llbracket\cdot\rrbracket^{\sharp}$$\nabla$$\llbracket\cdot\rrbracket^{\sharp}$$\llbracket\cdot\rrbracket^{\sharp}$$\nabla$fixfix

(c) Cyclic-control flow and demanded fixed points

Figure 4. Demanded abstract interpretation: (4(a)) Demanding a value for
$\underline{1}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$ recursively
triggers demand for its dependencies and is resolved by computing its value
from the statements in $\underline{\ell_{0}}\\!\cdot\\!\underline{\ell_{1}}$
and $\underline{\ell_{1}}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$ and
the initial state $\varphi_{0}$ in $\underline{\ell_{0}}$. We show only the
relevant subgraph here, but this operation occurs in the full DAIG of Fig. 3.
(4(b)) DAIG from Fig. 3 updated to reflect nodes added (
$\underline{\ell_{1}}\\!\cdot\\!\underline{\ell_{7}}$ and
$\underline{\ell_{7}}$) and potentially affected
($\underline{1}\\!\cdot\\!\underline{\ell_{\textsf{ret}}}$ and
$\underline{\ell_{\textsf{ret}}}$) by the edit in Section 2.2. All other nodes
are unchanged. (4(c)) DAIG for the $\ell_{3}$-to-$\ell_{4}$-to-$\ell_{3}$ loop
of Fig. 2 after one demanded unrolling, with the new DAIG region shown in red
and the (removed) pre-unrolling fix edge shown in dotted  grey. Note that
cells containing program syntax are not duplicated. The DAIG with the black
vertices and edges along with the  grey edge (but not the red ones) is the
initial sub-DAIG for the dashed ellipse in Fig. 3.

In Fig. 4(a), we show the result of evaluating a demand query on our example
DAIG. Suppose a client issues a query for the
$\underline{1}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$ cell in Fig. 3,
the abstract state corresponding to the return q statement at $\ell_{1}$ in
Fig. 1. Since the
$\underline{1}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$ cell has
predecessors
$\underline{\ell_{1}}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$ and
$\underline{\ell_{1}}$, we issue requests for the values of those cells. Cell
$\underline{\ell_{1}}$ is empty, but depends on
$\underline{\ell_{0}}\\!\cdot\\!\underline{\ell_{1}}$ and
$\underline{\ell_{0}}$, so more requests are issued. Both of those cells hold
values, so we can compute and store the value of $\underline{\ell_{1}}$. Now,
having satisfied its dependencies, we can compute the value of
$\underline{1}\cdot\underline{\ell_{\tiny\textsf{ret}}}$, as shown in Fig.
4(a). Note that DAIGs are always acyclic, so this recursive traversal of
dependencies is well-founded.

Crucially, these results are now memoized for future incremental reuse; a
subsequent query for $\underline{\ell_{\text{\tiny ret}}}$, for example, will
memo match on $\underline{1}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$
and only need to compute
$\underline{2}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$ and its
dependencies from scratch. This fine-grained reuse of intermediate abstract
interpretation results is a key feature of the DAIG encoding for demand-driven
analysis.

To handle developer edits to code, DAIGs are also naturally incremental,
efficiently recomputing and reusing analysis results across multiple program
versions, following the incremental computation with names approach
(DBLP:conf/oopsla/HammerDHLFHH15).

Consider a program edit which adds a logging statement print("p is null") just
before the return at $\ell_{1}$ in Fig. 1. Intuitively, program behaviors are
unchanged at those locations unreachable from the added statement, so an
incremental analysis should only need to re-analyze the sub-DAIG reachable
from the new statement.

Fig. 4(b) illustrates this program edit’s effect on the DAIG. The green nodes
correspond to the added statement cell
$\underline{\ell_{1}}\\!\cdot\\!\underline{\ell_{7}}$ and its corresponding
abstract state cell $\underline{\ell_{7}}$. Nodes forward-reachable from the
green nodes — those marked in red — are invalidated (a.k.a. “dirtied”) by our
incremental computation engine. In particular, cells
$\underline{\ell_{1}}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$ and
$\underline{\ell_{\tiny\textsf{ret}}}$ containing abstract states
$\varphi^{\prime}$ and $\varphi^{\prime\prime}$, respectively, are dirtied.

Crucially, while nodes are dirtied eagerly, they are recomputed from up-to-
date inputs lazily, only when demanded. That is, the DAIG encoding allows our
analysis to avoid constant recomputation of an analysis as a program is
edited, instead computing results on demand while soundly keeping track of
which intermediate results — possibly from a previous program version — are
available for reuse. For example, assuming that $\underline{\ell_{1}}$ and
$\underline{2}\\!\cdot\\!\underline{\ell_{\tiny\textsf{ret}}}$ were both
computed before the edit, a query for $\underline{\ell_{\text{\tiny ret}}}$
must execute only two transfers and one join: the red and green edges of Fig.
4(b). This represents a significant savings over recomputing the entire
analysis — including the loop fixed point — as would be necessary without
incremental analysis.

If desired, an auxiliary memoization (memo) table can also be used to cache
computations independent of program locations to enable further
incrementalization, with names based on the input values (e.g., memoizing
$\llbracket s_{0}\rrbracket^{\sharp}(\varphi_{0})$ in a cell named
$\underline{\llbracket\cdot\rrbracket^{\sharp}}\cdot\underline{s_{0}}\cdot\underline{\varphi_{0}}$).
As with batch analysis, it is sound to drop cached results from the DAIG
and/or memo table and later recompute those results if needed, trading
efficiency of reuse for a lower memory footprint.

###  2.3. Cyclic Control Flow and Demanded Fixed Points

As shown in Section 2.1, encoding program structure and analysis data-flow
into a dependency graph is relatively straightforward when the control-flow
graph is acyclic. However, when handling loops or recursion, like lines
$\ell_{3}$ and $\ell_{4}$ in Fig. 1, an abstract interpreter’s fixed-point
computation is inherently cyclic. Properly handling these cyclic control-flow
and data-flow dependency structures is the crux of realizing demanded abstract
interpretation. For instance, introducing cyclic dependencies in the DAIG
yields an unclear evaluation semantics. The key insight we leverage is that we
can instead enrich the demand-driven query evaluation and the incremental edit
semantics to dynamically evolve DAIGs such that each step preserves the
acyclic dependency structure invariant. To do so, we use a distinguished edge
label (fix) to indicate a dependency on the fixed-point of a given region of
the DAIG, which is then dynamically unrolled on-demand by query evaluation and
rolled by incremental edits.

The details are formalized in Section 5; we proceed here by example on the
demanded abstract interpretation of the append program of Fig. 2. Consider
Fig. 4(c), and focus on the black and  grey vertices and edges, ignoring the
red for the moment. Rather than encoding the CFG back edge from $\ell_{4}$ to
$\ell_{3}$ directly into the DAIG (violating acyclicity in the process), the
$\ell_{3}$-to-$\ell_{4}$-to-$\ell_{3}$ loop is initially encoded with separate
reference cells for the $0$th and $1$st abstract iterates at the loop head
$\ell_{3}$ (named $\underline{\ell_{3}}^{\;(0)}$ and
$\underline{\ell_{3}}^{\;(1)}$ respectively), along with a fix edge from those
two cells to $\ell_{3}$’s fixed-point cell $\underline{\ell_{3}}$, as seen in
the  grey dotted edge. Crucially, this initial DAIG is acyclic.

_Query Evaluation._ For query evaluation, we can compute fixed points on
demand by “unrolling” the _abstract interpretation_ of loop bodies in the DAIG
one abstract iteration at a time until a fixed point is reached, preserving
the acyclic DAIG invariant at each step. That is, our key observation is to
unroll at the semantic level of the abstract interpretation rather than the
syntactic level of the control-flow graph.

From the initial DAIG in Fig. 4(c), when the fixed-point
$\underline{\ell_{3}}$ is demanded, its dependencies — the $0$th and $1$st
abstract iterates — are computed. If their values are equal, then a fixed-
point has been reached and may be written to $\underline{\ell_{3}}$.444We
describe here the widening strategy of applying $\nabla$ every iteration until
a fixed-point is reached for simplicity, but the same general idea applies for
other widening strategies or checking convergence with $\sqsubseteq$ instead
of $=$. If their values are not equal, then the abstract interpretation of the
loop body — but not the loop body statements — is unrolled one step further
and the fix edge slides forward to now depend on the $1$st and $2$nd abstract
iterates, as seen in the red cells and edges of Fig. 4(c). And crucially, this
one-step unrolled DAIG is also acyclic.

From here, the process continues, and termination is guaranteed by leveraging
the standard argument of abstract interpretation meta-theory: the sequence of
abstract iterates in the cells
$\underline{\ell_{3}}^{\;(0)},\underline{\ell_{3}}^{\;(1)},\underline{\ell_{3}}^{\;(2)},\dots$
converges because it is produced by widening a monotonically increasing
sequence of abstract states, so this demanded unrolling of fix occurs only
finitely — but unboundedly — many times. We see that in essence, the sequence
of abstract interpretation iterates
$\underline{\ell_{3}}^{\;(0)},\underline{\ell_{3}}^{\;(1)},\underline{\ell_{3}}^{\;(2)},\dots$
are encoded into the DAIG on demand during query evaluation.

In classical abstract interpretation, a widen $\nabla$ is a join that enforces
convergence during interpretation and thus is only strictly needed if the
abstract domain has infinite height. Our approach can be seen as an
application of this widening principle to demanded computation. For an
abstract domain of finite height $k$, it would have been sufficient to encode
the unrolling of fix eagerly into an acyclic DAIG by inlining the abstract
iteration $k$ times to $k$ iterate cells
$\underline{\ell_{3}}^{\;(0)},\dots,\underline{\ell_{3}}^{\;(k)}$. However,
many expressive, real-world abstract domains — including the shape analysis
domain of our example and most numerical domains — are of infinite height.

_Incremental Edits._ Since the acyclic DAIG invariant is always preserved,
invalidating on incremental edits still only requires eager dirtying forwards
in the DAIG, with some special semantics for fix edges. When dirtying along a
fix edge, the fix edge is rolled back to a non-dirty cell (i.e., the $0$th and
$1$st iterate). In Fig. 4(c), if the statement cell
$\underline{\ell_{4}}\cdot\underline{\ell_{3}}$ is edited, then dirtying will
happen along the red solid fix edge at which point it will slide back to be
the  grey dotted one.

_Interprocedural Demand._ This demanded unrolling of fix also suggests an
approach to interprocedural demanded analysis parameterized by a context-
sensitivity policy. To analyze a call when evaluating a query, we construct a
DAIG for the callee procedure on demand, indexed by a context determined
opaquely by the context-sensitivity policy.

The “functional approach” to interprocedural analysis of sharir1978two could
also potentially be adapted to our framework by constructing disjoint DAIGs
for each phase and inserting dependencies from phase-$2$ callsites to
corresponding phase-$1$ summaries.

These techniques both rely on a static call graph, which can be computed
soundly using either abstract interpretation (which may itself be expressed in
a DAIG) or type-/constraint-based approaches.

##  3\. Preliminary Definitions

Our technique lifts a program and an abstract interpreter _together_ into a
demanded abstract interpretation graph (DAIG), a representation that is
amenable for sound incremental and demand-driven program analysis. By design,
this construction is generic in the underlying programming language and
concrete semantics as well as the abstract domain and abstract semantics. In
this section, we fix a generic programming language and an abstract
interpreter interface that serve as inputs to DAIG construction, both to
define syntax and to make explicit our assumptions about their semantic
properties. Selected instantiations of the framework for real-world analysis
problems are given in Section 7.

$\begin{array}[]{rcl}\text{statements}&s\in\mathit{Stmt}\\\
\text{locations}&\ell\in\mathit{Loc}&\\\ \text{control-flow
edges}&e\in\mathit{Edge}&::=\ell\\!-\mbox{-}[s]\shortrightarrow\\!\ell^{\prime}\\\
\text{programs}&\langle
L,E,\ell_{0}\rangle&:~{}\mathcal{P}(\textit{Loc})\times\mathcal{P}(\textit{Edge})\times\textit{Loc}\\\
\text{concrete states}&\sigma\in\Sigma&\text{(with initial state
$\sigma_{0}$)}\\\ \text{concrete
semantics}&\llbracket\cdot\rrbracket&:~{}\mathit{Stmt}\to\Sigma\to\Sigma_{\bot}\\\
\text{collecting semantics}&\llbracket\cdot\rrbracket^{\ast}_{\langle
L,E,\ell_{0}\rangle}&:~{}\mathit{Loc}\rightarrow\mathcal{P}(\Sigma)\end{array}$
Figure 5. A generic programming language of control-flow graphs edge-labelled
by an unspecified statement language.

Programs under analysis are given as control-flow graphs, edge-labelled by an
unspecified statement language and interpreted by a denotational concrete
semantics as shown in Fig. 5. A program $\langle L,E,\ell_{0}\rangle$ is a
3-tuple composed of a set $L$ of control locations, a set $E$ of directed,
statement-labelled control-flow edges between locations, and an initial
location $\ell_{0}$. We say that a program $\langle L,E,\ell_{0}\rangle$ is
well-formed when (1) $\ell_{0}$ and all locations in $E$ are drawn from $L$,
and (2) $L$ and $E$ form a reducible control-flow graph. These conditions
ensure that we avoid degenerate edge cases and only consider control flow
graphs which correspond to realistic programs (dragon_book).

Statements are interpreted by the concrete denotational semantics
$\llbracket\cdot\rrbracket$ as partial functions over concrete program states.
As is standard, we can also lift this statement semantics to a collecting
$\llbracket\cdot\rrbracket^{\ast}_{\langle L,E,\ell_{0}\rangle}$ of full
programs, by computing the transitive closure of the statement semantics over
a flow graph. That is, $\llbracket\ell\rrbracket^{*}_{\langle
L,E,\ell_{0}\rangle}$ is the set of all concrete states that can be witnessed
at program location $\ell$ in a valid program execution. We elide the
subscript when it is clear from context. Such a collecting semantics is
uncomputable in general, but is an important tool for reasoning about analysis
soundness.

Now, we define the interface of a generic abstract interpreter over this
control-flow graph language. These definitions are intended simply to fix
notation and minimize ambiguity and are as standard as possible.

An abstract interpreter is a $6$-tuple
$\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$
composed of:

  * -

An abstract domain $\Sigma^{\sharp}$ (elements of which are referred to as
abstract states) which forms a semi-lattice under

    * -

a partial order
$\sqsubseteq~{}\in\mathcal{P}(\Sigma^{\sharp}\times\Sigma^{\sharp})$ with a
bottom $\bot\in\Sigma^{\sharp}$

    * -

an upper bound (a.k.a. join)
$\sqcup~{}:~{}\Sigma^{\sharp}\rightarrow\Sigma^{\sharp}\rightarrow\Sigma^{\sharp}$

  * -

An initial abstract state $\varphi_{0}\in\Sigma^{\sharp}$

  * -

An abstract semantics
$\llbracket\cdot\rrbracket^{\sharp}:\mathit{Stmt}\rightarrow\Sigma^{\sharp}\rightarrow\Sigma^{\sharp}$
that interprets program statements as monotone functions over abstract states.

  * -

A widening operator
$\nabla~{}:~{}\Sigma^{\sharp}\rightarrow\Sigma^{\sharp}\rightarrow\Sigma^{\sharp}$
that is an upper bound operator (i.e.,
$(\varphi\sqcup\varphi^{\prime})\sqsubseteq(\varphi\nabla\varphi^{\prime})$
for all $\varphi,\varphi^{\prime}$) and enforces convergence (i.e., for all
increasing sequences of abstract states
$\varphi_{0}\sqsubseteq\varphi_{1}\sqsubseteq\varphi_{2}\sqsubseteq\cdots$,
the sequence
$\varphi_{0},~{}\varphi_{0}\nabla\varphi_{1},~{}(\varphi_{0}\nabla\varphi_{1})\nabla\varphi_{2},~{}\dots$
converges).

Furthermore, a concretization function
$\gamma:\Sigma^{\sharp}\rightarrow\mathcal{P}(\Sigma)$ gives meaning to
abstract states. We say that a concrete state $\sigma$ models an abstract
state $\varphi$ (equivalently, that $\varphi$ abstracts $\sigma$), written
$\sigma\models\varphi$, when $\sigma\in\gamma(\varphi)$.

###### Definition 3.1 (Local Abstract Interpreter Soundness).

An abstract interpreter
$\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$
is locally sound if for all $\sigma,\varphi,s$, if $\sigma\models\varphi$ and
$\llbracket s\rrbracket\sigma\neq\bot$ then $\llbracket
s\rrbracket\sigma\models\llbracket s\rrbracket^{\sharp}\varphi$.

Local soundness can be extended to a global soundness property: if the
abstract semantics are locally sound, then the abstract interpreter computes a
sound over-approximation of the possible concrete states at each location.

###### Proposition 3.2 (Global Abstract Interpreter Soundness).

If
$\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$
is locally sound and $\sigma_{0}\models\varphi_{0}$ then it induces an
abstract collecting semantics
${\llbracket\cdot\rrbracket^{\sharp}}^{\ast}_{\langle
L,E,\ell_{0}\rangle}:\mathit{Loc}\to\Sigma^{\sharp}$ such that for all
$\sigma\in\llbracket\ell\rrbracket^{\ast}_{\langle L,E,\ell_{0}\rangle}$,
$\sigma\models{\llbracket\ell\rrbracket^{\sharp}}^{\ast}_{\langle
L,E,\ell_{0}\rangle}$.

We elide the abstract collecting semantics
${\llbracket\cdot\rrbracket^{\sharp}}^{\ast}_{\langle L,E,\ell_{0}\rangle}$;
it is similarly a transitive closure of the abstract statement semantics over
a flow graph. It is a well-known result that global abstract interpreter
soundness is implied by local soundness (DBLP:conf/popl/CousotC77) and that
such a global fixed-point is computable using the chaotic iteration method
with widening (DBLP:conf/ershov/Bourdoncle93).

##  4\. Demanded AI Graphs

Recall from Section 2 that a demanded abstract interpretation graph (DAIG) is
a directed acyclic hypergraph, whose vertices are reference cells containing
program syntax or intermediate analysis results, and whose edges reflect
analysis dataflow relationships among those cells. In Fig. 6, we show a syntax
for DAIGs. A DAIG $\mathcal{D}=\langle R,C\rangle$ is composed of a set
$R\subseteq\mathit{Ref}$ of named reference cells connected by computation
edges $C\subseteq\mathit{Comp}$. A computation $c\colon n\leftarrow
f(n_{1},\dots,n_{k})$ is an edge connecting sources $\\{n_{1},\dots,n_{k}\\}$
to a singleton destination $\\{n\\}$, labeled by some analysis function $f$.

$\begin{array}[]{rcl}\text{functions}&f&::=\llbracket\cdot\rrbracket^{\sharp}~{}|~{}\sqcup~{}|~{}\nabla~{}|~{}\textsf{fix}\\\
\text{values}&v&::=s~{}|~{}\varphi\\\
\text{names}&n\in\mathit{Nm}&::=\underline{\ell}~{}|~{}\underline{f}~{}|~{}\underline{i}~{}|~{}\underline{v}~{}|~{}n_{1}\\!\cdot\\!n_{2}~{}|~{}n^{(i)}\\\
\text{types}&\tau&\in\\{\mathit{Stmt},~{}\Sigma^{\sharp}\\}\\\ \text{reference
cells}&r\in\mathit{Ref}&::=n[v:\tau]~{}|~{}n[\varepsilon:\tau]\\\
\text{computations}&c\in\mathit{Comp}&::=n\leftarrow f(n_{1},\dots,n_{k})\\\
\text{DAIGs}&\mathcal{D}&:\mathcal{P}(\mathit{Ref})\times\mathcal{P}(\mathit{Comp})\end{array}$
Figure 6. Demanded Abstract Interpretation Graphs, edge-labelled by analysis
functions and connecting named reference cells storing statements and abstract
states.

Names $\underline{\ell}$, $\underline{f}$, $\underline{v}$ and $\underline{i}$
correspond respectively to locations $\ell$, functions $f$, values $v$ and
integers $i$, supporting memoization of those syntactic constructs. Name
products $n_{1}\\!\cdot\\!n_{2}$ support the construction of more complicated
names, and $i$-primed names $n^{(i)}$ allow variants of a single name to be
distinguished as loops are unrolled: $n^{(i)}$ is the $i$th unrolled copy of
the name $n$ in a loop. All name equalities are decided structurally.

Values include statements $s$ and abstract states $\varphi\in\Sigma^{\sharp}$.
Reference cells bind names to values or the absence thereof (denoted
$\varepsilon$), while computations specify analysis data-flow dependencies
between reference cells.

We denote by $\mathcal{D}[n\mapsto v]$ the DAIG identical to $\mathcal{D}$
except that the reference cell named $n$ now holds value $v$. We also denote
DAIG reachability by $n\rightsquigarrow_{\mathcal{D}}n^{\prime}$ (eliding the
subscript when it is clear from context), and define helper functions name,
srcs, and dest to project out, respectively, the name $n$ of a reference cell
$n[v_{\varepsilon}:\tau]$ and the source names $\\{n_{1},\dots,n_{k}\\}$ or
destination name $n$ of a computation $n\leftarrow f(n_{1},\dots,n_{k})$.
Finally, the typing judgment $R\vdash n\leftarrow f(n_{1},\dots,n_{k})$ holds
when $n_{1}$ through $n_{k}$ name references in $R$ with the same types as
$f$’s inputs and $n$ names a reference in $R$ with the same type as $f$’s
output.

###### Definition 4.1 (DAIG Well-formedness).

A DAIG $\mathcal{D}=\langle R,C\rangle$ is subject to the following well-
formedness constraints.

  * (1)

References are named uniquely:
. $\forall r,r^{\prime}\in
R~{}.~{}\texttt{name}(r)=\texttt{name}(r^{\prime})~{}\Leftrightarrow~{}r=r^{\prime}$

  * (2)

Computations have unique destinations:
. $\forall c,c^{\prime}\in
C~{}.~{}\texttt{dest}(c)=\texttt{dest}(c^{\prime})~{}\Leftrightarrow~{}c=c^{\prime}$

  * (3)

Dependencies are acyclic: $\not\exists~{}r\in
R~{}.~{}\textsf{name}(r)\rightsquigarrow\textsf{name}(r)$

  * (4)

Computations are well-typed with respect to references:
. $\forall c\in C~{}.~{}R\vdash c$

  * (5)

Empty references have dependencies:
. $\forall n[\varepsilon:\tau]\in R~{}.~{}\exists~{}c\in
C~{}.~{}n=\texttt{dest}(c)$

(1) Straightline statements(2) Control-flow joins(3) Back
edges$\ell^{\prime}$$\ell$$s$$\ell_{1}$$\ell_{k}$$\ell$$s_{1}$$s_{k}$$\ell$$\ell^{\prime}$loop
body$s$$n_{\ell^{\prime}}$ $s$
$\underline{\ell^{\prime}}\\!\cdot\\!\underline{\ell}$$n_{\ell}$$\llbracket\cdot\rrbracket^{\sharp}$$n_{\ell_{1}}$
$s_{1}$
$\underline{1}\\!\cdot\\!\underline{\ell_{1}}\\!\cdot\\!\underline{\ell}$$\underline{1}\\!\cdot\\!n_{\ell}$$\llbracket\cdot\rrbracket^{\sharp}$$n_{\ell_{k}}$
$s_{k}$
$\underline{k}\\!\cdot\\!\underline{\ell_{k}}\\!\cdot\\!\underline{\ell}$$\underline{k}\\!\cdot\\!n_{\ell}$$\llbracket\cdot\rrbracket^{\sharp}$$n_{\ell}$$\sqcup$$\underline{\ell}^{\;(0)}$$\underline{\ell^{\prime}}^{\;(0)}$$\mathcal{D}_{\Sigma^{\sharp}}^{(0)}$$\mathcal{D}_{\textit{Stmt}}$
$s$
$\underline{\ell^{\prime}}\\!\cdot\\!\underline{\ell}$$\underline{\ell}^{\;(0)}\\!\\!\cdot\\!\underline{\ell}^{\;(1)}$$\underline{\ell}^{\;(1)}$$\nabla$$\llbracket\cdot\rrbracket^{\sharp}$$\underline{\ell}^{\;(k-1)}$$\underline{\ell^{\prime}}^{\;(k-1)}$$\mathcal{D}_{\Sigma^{\sharp}}^{(k-1)}$$\underline{\ell}^{\;(k-1)}\\!\\!\cdot\\!\underline{\ell}^{\;(k)}$$\underline{\ell}^{\;(k)}$$\nabla$$\llbracket\cdot\rrbracket^{\sharp}$$\underline{\ell}$fix
Figure 7. DAIG–CFG Consistency (Definition 4.2) in diagram form, illustrating
how different CFG structures are encoded into DAIG structures. In subfigure
(3), we apply some ad-hoc shorthands for the DAIG encoding of the loop body:
$\mathcal{D}_{\textit{Stmt}}$ contains all of its statement reference cells,
while $\mathcal{D}_{\Sigma^{\sharp}}^{(i)}$ contains all of its abstract state
reference cells, with iteration counts set to $i$. Each dotted line from
$D_{\textit{Stmt}}$ thus represents one or more DAIG edges, from each
statement to corresponding abstract states.

Beyond these basic well-formedness conditions, a DAIG’s structure must also
properly encode an abstract interpretation computation over an underlying
program. Given a program’s CFG and an abstract interpreter interface (as
defined in Section 3), there are three general cases shown in Fig. 7 to
consider when examining a corresponding DAIG. The key property is that demand-
driven query evaluation and incremental edits will evolve the DAIG but
preserve the following consistency conditions:

  * (1)

A forward CFG edge $\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell$ to a
non-join location is encoded by a transfer function-labelled DAIG edge,
connecting reference cells for its abstract pre-state (named
$n_{\ell^{\prime}}$) and statement label (named
$\underline{\ell^{\prime}}\\!\cdot\\!\underline{\ell}$) to a reference cell
for its abstract post-state (named $n_{\ell}$).555We write $n_{\ell}$ for the
name of the abstract state at $\ell$ throughout this section:
$\underline{\ell}^{\;(0)}$ if $\ell$ belongs to any natural loop and
$\underline{\ell}$ otherwise. Loop heads $\ell$ are a special case: $n_{\ell}$
is $\underline{\ell}^{\;(0)}$ (the abstract state at loop entry) when the
destination of a DAIG edge and $\underline{\ell}$ (the fixed point at $\ell$)
otherwise.

  * (2)

Forward CFG edges to a join location $\ell$ are a bit more complex,
introducing intermediate cells to encode the join $\sqcup$ into the DAIG. For
each incoming edge to $\ell$ with statement $s_{i}$, we introduce a three-cell
transfer function construct similar to case (1), with an output cell
$\underline{i}\\!\cdot\\!n_{\ell}$ named uniquely for that edge. Then, a
single join edge connects each pre-join abstract state
$\underline{i}\\!\cdot\\!n_{\ell}$ to $n_{\ell}$, the abstract post-state at
$\ell$.

  * (3)

As described informally in Section 2.3, our framework analyzes CFG back edges
by unrolling the abstract fixed-point computation to evolve DAIGs on demand,
so this diagram is parameterized by a number $k$ of such unrollings. Given the
CFG back edge $\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell$, a
transfer function DAIG edge connects the abstract state after one abstract
iteration (named $\underline{\ell^{\prime}}^{\;(0)}$) and $s$ to a pre-widen
abstract state at the loop head $\ell$ (named
$\underline{\ell}^{\;(0)}\\!\cdot\\!\underline{\ell}^{\;(1)}$), which is
connected with the previous abstract state at the loop head
($\underline{\ell}^{(0)}$) to the next ($\underline{\ell}^{(1)}$) via a widen
edge. This acyclic structure is repeated $k$ times in the DAIG (with $k=1$ in
the initial construction and further unrollings generated on demand as
decribed in Section 5), thereby encoding the unbounded fixed-point
computation. Lastly, the fix edge — indicating a dependency on the eventual
fixed point — connects the two greatest abstract iterates to the reference
cell ($\underline{\ell}$) for the fixed-point abstract state at the loop head.

###### Definition 4.2 (DAIG–CFG Consistency).

A DAIG $\mathcal{D}=\langle R,C\rangle$ is consistent with a program CFG
$\langle L,E,\ell_{0}\rangle$, written $\mathcal{D}\approxeq\langle
L,E,\ell_{0}\rangle$, when it is well-formed and its structure is consistent
with that of the program.

A formal statement of the $\mathcal{D}\approxeq\langle L,E,\ell_{0}\rangle$
relation is given in the appendix, closely following the structure of the
above description and Fig. 7.

First, we fix some notation and terminology related to flow graphs and their
structure, all of which is fairly standard:

The edges $E$ of a reducible flow graph program $\langle L,E,\ell_{0}\rangle$
may be partitioned disjointly into a set $E_{f}$ of forward edges and a set
$E_{b}$ of back edges, where forward edges form a directed acyclic graph that
spans $L$ and the destination $\ell^{\prime}$ of each back edge
$\ell\\!-\mbox{-}[s]\shortrightarrow\\!\ell^{\prime}\in E_{b}$ dominates666A
vertex $\ell$ dominates a vertex $\ell^{\prime}$ if every path from the entry
to $\ell^{\prime}$ passes through $\ell$. the source $\ell$. A vertex is a
loop head if it is the destination of an edge in $E_{b}$.

Furthermore, each back edge
$e=\ell\\!-\mbox{-}[s]\shortrightarrow\\!\ell^{\prime}\in E_{b}$ in a
reducible flow graph uniquely determines a natural loop
$\textsf{loop}(\ell^{\prime}):\mathcal{P}(L)$, the set of locations from which
$\ell$ can be reached without passing through $\ell^{\prime}$. Intuitively,
the natural loop is the “body” of the loop with head $\ell^{\prime}$, and we
define $\textsf{loop}(\ell)\triangleq\emptyset$ for all non-loop head
locations $\ell$.

There are well-known efficient algorithms both to partition forward/back edges
and to find natural loops in reducible flow graphs (e.g., (dragon_book), Sec.
9.6) which we do not repeat here.

We also define a helper function $\textsf{fwd-edges-to}_{\langle
L,E,\ell_{0}\rangle}:\mathit{Loc}\to\mathcal{P}(\mathbb{N}\times\mathit{Edge})$
which assigns indices to forward control-flow edges into the given location.
These indices will be essential for DAIG construction, allowing us to uniquely
name the intermediate abstract states before a join.

We denote by $L_{\sqcup}$ the set of CFG join points
$\big{\\{}\ell~{}\big{|}~{}|\textsf{fwd-edges-to}(\ell)|\geq 2\big{\\}}$ and
by $L_{\not\sqcup}$ its complement $L/L_{\sqcup}$. Note that our definition is
non-standard: these points are determined by forwards indegree rather than
total indegree, since no join operation is necessary at a loop entry with only
a single non-loop predecessor.

###### Definition 4.3 (DAIG–CFG Consistency).

A DAIG $\mathcal{D}=\langle R,C\rangle$ is consistent with a program CFG
$\langle L,E,\ell_{0}\rangle$, written $\mathcal{D}\approxeq\langle
L,E,\ell_{0}\rangle$, when it is well-formed and its structure accurately
encodes the abstract interpretation of that program by satisfying the
following conditions. See Fig. 7 for a visual representation of this
definition to build intuition for the more formal statements below.

  * (1)

Forward CFG edges to non-join locations are encoded by a transfer function
edge connecting the abstract pre-state and statement to the abstract post-
state.

$\forall\ell^{\prime}\in
L_{\not\sqcup},~{}\ell\\!-\mbox{-}[s]\shortrightarrow\\!\ell^{\prime}\in
E_{f}\quad.\quad\underline{\ell}\\!\cdot\\!\underline{\ell^{\prime}}[s:\mathit{Stmt}]\in
R\quad\wedge\quad
n_{\ell^{\prime}}\leftarrow\llbracket\cdot\rrbracket^{\sharp}(n_{\ell}\\!\cdot\\!n_{\ell^{\prime}},n_{\ell})\in
C$

  * (2)

Forward CFG edges to join locations are slightly more complex: for each join
location $\ell$, fwd-edges-to assigns a unique integer index $i$ to each
incoming CFG edge. For each such CFG edge, a transfer function edge connects
the reference cells containing its statement label and the abstract state at
its source location to a pre-join abstract state (named by
$\underline{i}\\!\cdot\\!n_{\ell}$) specific to that edge. Then, a single join
edge connects each pre-join abstract state $\underline{i}\\!\cdot\\!n_{\ell}$
to $n_{\ell}$, the actual abstract state at $\ell$.

$\forall\ell\in L_{\sqcup}~{}.\quad
n_{\ell}\leftarrow\sqcup(\underline{1}\cdot
n_{\ell},...,\underline{|\textsf{fwd-edges-to}(\ell)|}\cdot n_{\ell})\in
C\quad\wedge\quad\left({\begin{array}[]{c}\forall(i,\ell_{i}\\!-\mbox{-}[s_{i}]\shortrightarrow\\!\ell)\in\textsf{fwd-
edges-to}(\ell)~{}.\\\
\underline{i}\\!\cdot\\!\underline{\ell_{i}}\\!\cdot\\!\underline{\ell}[s_{i}:\mathit{Stmt}]\in
R~{}~{}\wedge~{}~{}\underline{i}\\!\cdot\\!n_{\ell}\leftarrow\llbracket\cdot\rrbracket^{\sharp}(\underline{i}\\!\cdot\\!\underline{\ell_{i}}\\!\cdot\\!\underline{\ell},~{}n_{\ell^{\prime}})\in
C\end{array}}\right)$

  * (3)

CFG back edges are encoded by some $k$ analysis iterations over the
corresponding loop body. First, a transfer function edge connects the
reference cell (named by
$n_{\ell^{\prime}}=\underline{\ell^{\prime}}^{\;(0)}$) at the end of the first
loop iteration and the back edge’s statement label to the first pre-widen
abstract state at the loop head (named by
$\underline{\ell}^{\;(0)}\\!\cdot\\!\underline{\ell}^{\;(1)}$). Then, for each
$i\in[0,k)$, the loop body is unrolled with iteration count $i$, and widen
edges connect the $i$th abstract iterate and pre-widen abstract state to the
next abstract iterate. Lastly, a fix edge connects the final two abstract
iterates to the loop head fixed point $\underline{\ell}$.

$\forall\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell\in
E_{b}~{}.~{}\exists~{}k\geq
1~{}.{\begin{array}[]{l}\underline{\ell^{\prime}}\\!\cdot\\!\underline{\ell}[s:\textit{Stmt}]\in
R~{}~{}\wedge\\\
\underline{\ell}^{(0)}\\!\cdot\\!\underline{\ell}^{(1)}\leftarrow\\!\llbracket\cdot\rrbracket^{\sharp}(\underline{\ell^{\prime}}\\!\\!\cdot\\!\underline{\ell},\underline{\ell^{\prime}}^{(0)})\\!\in
C~{}~{}\wedge\\\
\underline{\ell}\leftarrow\textsf{fix}(\underline{\ell}^{(k-1)}\\!\\!,\underline{\ell}^{(k)})\in
C~{}~{}\wedge\\\ \forall
i\in[0,k)~{}.\left({\begin{array}[]{l}\underline{\ell}^{\;(i)}\leftarrow\nabla(\underline{\ell}^{\;(i-1)},~{}\underline{\ell}^{\;(i-1)}\\!\cdot\\!\underline{\ell}^{\;(i)})\in
C~{}\wedge\\\
\hfill\left\\{\textsf{incr-c}^{i}(c)~{}\middle|~{}c\in\textsf{loop-
comps}(\ell)\right\\}\subseteq C\end{array}}\right)\end{array}}$

The initial name $n_{\ell}$ for a location $\ell$ is
$\underline{\ell}^{\;(0)}$ if it belongs to any natural loop and
$\underline{\ell}$ if it does not, and we denote by $\textsf{loop-
comps}(\ell)$ the subset of $C$ whose elements contain a name
$\underline{\ell^{\prime}}^{\;(0)}$ such that
$\ell^{\prime}\in\textsf{loop}(\ell)$. The helper function incr increments the
loop-iteration counts in names, and we write incr-c for the pointwise lifting
of incr to edges $c\in\mathit{Comp}$.

$\displaystyle\textsf{incr}(n)$
$\displaystyle\triangleq\left\\{{\begin{array}[]{lr}\underline{\ell}^{\;(k+1)}&\text{
if }n=\underline{\ell}^{\;(k)}\\\
\textsf{incr}(n_{1})\\!\cdot\\!\textsf{incr}(n_{2})&\text{ if
}n=n_{1}\\!\cdot\\!n_{2}\\\ n&\text{ otherwise}\end{array}}\right.$

The above establishes when the structure of a DAIG is consistent with the
program’s CFG. A DAIG is consistent with an abstract interpret _ation_ of the
program when the partial analysis results stored in the DAIG are consistent
with the partial abstract interpretation, or formally as follows:

###### Definition 4.4 (DAIG–AI Consistency).

A DAIG $\mathcal{D}=\langle R,C\rangle$ is consistent with an abstract
interpreter
$\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$,
written
$\mathcal{D}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$,
when all partial analysis results stored in $R$ are consistent with the
computations encoded by $C$, such that
$\underline{\ell_{0}}[\varphi_{0}:\Sigma^{\sharp}]\in R$ and

$\forall~{}n[v:\Sigma^{\sharp}]\in
R~{},~{}~{}n\\!\leftarrow\\!f(n_{1},...,n_{k})\in C~{}~{}.\\\
\left\\{n_{i}[v_{i}\\!:\\!\tau_{i}]\middle|1\leq i\leq
k\right\\}\\!\subseteq\\!R~{}\wedge~{}\left\\{\\!{\begin{array}[]{lr}v=v_{1}=v_{2}&\text{if
}f=\textsf{fix}\\\
v=f(v_{1},\dots,v_{k})&\\!\\!\text{otherwise}\end{array}}\right.$

###### Definition 4.5 (Initial DAIG Construction).

The initial DAIG $\mathcal{D}_{\small\textsf{init}}(\langle
L,E,\ell_{0}\rangle,\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle)$
for program $\langle L,E,\ell_{0}\rangle$ and abstract domain
$\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$.
consists of several distinct categories of both reference cells and
computation edges, which we describe and define separately for clarity and
ease of presentation.

Reference cells in $R_{\mathit{Stmt}}$ contain program statements, those in
$R_{\Sigma^{\sharp}}$ contain abstract states at each control location and
join point, and those in $R_{\circlearrowleft}$ contain those needed to encode
loops, while computation edges in each $C_{f}$ encode the uses of that
function $f$. As in Definition 4.2, we denote by $n_{\ell}$ the initial name
at $\ell$, which is defined as $\underline{\ell}^{\;(0)}$ if $\ell$ is in the
natural loop of some back edge in $E_{b}$, or $\underline{\ell}$ otherwise.

That is, $\mathcal{D}_{\small\textsf{init}}\left(\langle
L,E,\ell_{0}\rangle,\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle\right)\triangleq\left\langle
R_{\mathit{Stmt}}\cup R_{\Sigma^{\sharp}}\cup
R_{\circlearrowleft},~{}C_{\llbracket\cdot\rrbracket^{\sharp}}\cup
C_{\sqcup}\cup C_{\textsf{fix}}\cup C_{\nabla}\right\rangle$, where:

  * •

Reference cells in $R_{\mathit{Stmt}}$ each contain a program statement and
are named by the locations before and after that statement, along with a
disambiguating integer index when multiple forwards777A reducible CFG has at
most one back edge to each vertex, so no disambiguation is necessary for back
edges. control-flow edges share a destination.

$\displaystyle R_{\mathit{Stmt}}\triangleq$
$\displaystyle\left\\{\underline{\ell}\\!\cdot\\!\underline{\ell^{\prime}}[s:\mathit{Stmt}]~{}\middle|~{}(\ell^{\prime}\in
L_{\not\sqcup}~{}\wedge~{}\ell\\!-\mbox{-}[s]\shortrightarrow\\!\ell^{\prime}\in
E)\vee\quad\ell\\!-\mbox{-}[s]\shortrightarrow\\!\ell^{\prime}\in
E_{b}\right\\}$ $\displaystyle\cup$
$\displaystyle\left\\{\underline{i}\\!\cdot\\!\underline{\ell}\\!\cdot\\!\underline{\ell^{\prime}}[s:\mathit{Stmt}]~{}\middle|~{}\ell\in
L_{\sqcup}~{}\wedge~{}(i,\ell^{\prime}\\!\\!-\mbox{-}[s]\shortrightarrow\\!\ell)\in\textsf{fwd-
edges-to}(\ell)\right\\}$

  * •

$R_{\Sigma^{\sharp}}$ contains one reference cell of abstract state type per
program location, with the initial location $\ell_{0}$’s cell populated by the
initial abstract state $\varphi_{0}$, along with indexed reference cells for
the pre-join abstract states at join point locations.

$\displaystyle R_{\Sigma^{\sharp}}\triangleq$
$\displaystyle\left\\{\underline{\ell_{0}}[\varphi_{0}:\Sigma^{\sharp}]\right\\}\cup\left\\{n_{\ell}[\varepsilon:\Sigma^{\sharp}]~{}\middle|~{}\ell\in
L/\\{\ell_{0}\\}\right\\}\cup\left\\{\underline{i}\\!\cdot\\!n_{\ell}[\varepsilon:\Sigma^{\sharp}]~{}\middle|~{}\ell\in
L_{\sqcup}~{}\wedge~{}1\leq i\leq|\textsf{fwd-edges-to}(\ell)|\right\\}$

  * •

Reference cells in $R_{\circlearrowleft}$ encode the zeroth
($\underline{\ell}^{\;(0)}$) and first ($\underline{\ell}^{\;(1)}$) abstract
iterates and the first pre-widening abstract state
($\underline{\ell}^{\;(0)}\\!\cdot\\!~{}\underline{\ell}^{\;(1)}$) at each
loop head $\ell$. Names for further iterations’ intermediate abstract states
are dynamically generated as needed by the operational semantics via demanded
unrolling.

$R_{\circlearrowleft}\triangleq\left\\{{\underline{\ell}}^{\;(i)}[\varepsilon:\Sigma^{\sharp}]~{}\middle|~{}\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell\in
E_{b}~{}\wedge~{}i\in\\{0,1\\}\right\\}\cup\left\\{\underline{\ell}^{\;(0)}\\!\cdot\\!~{}\underline{\ell}^{\;(1)}[\varepsilon:\Sigma^{\sharp}]~{}\middle|~{}\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell\in
E_{b}\right\\}$

  * •

Computations in $C_{\llbracket\cdot\rrbracket^{\sharp}}$ encode abstract
transfers. Its three subsets respectively encode the abstract semantics of
forward edges to non-join locations, forward edges to join locations, and back
edges.

We define the shorthand $\textsf{src-nm}(\ell,\ell^{\prime})$ to be
$\underline{\ell}$ when $\ell$ is a loop head and
$\ell^{\prime}\not\in\textsf{loop}(\ell)$ and $n_{\ell}$ otherwise.

$\displaystyle C_{\llbracket\cdot\rrbracket^{\sharp}}\triangleq$
$\displaystyle\left\\{n_{\ell}\leftarrow\llbracket\cdot\rrbracket^{\sharp}\left(\underline{\ell^{\prime}}\\!\cdot\\!\underline{\ell},\textsf{src-
nm}(\ell^{\prime},\ell)\right)~{}\middle|~{}\ell\in
L_{\not\sqcup}~{}\wedge~{}\ell^{\prime}\\!\\!-\mbox{-}[s]\shortrightarrow\\!\ell\in
E_{f}\right\\}$ $\displaystyle\cup$
$\displaystyle\left\\{\underline{i}\\!\cdot\\!n_{\ell}\leftarrow\llbracket\cdot\rrbracket^{\sharp}\left(\underline{i}\\!\cdot\\!\underline{\ell^{\prime}}\\!\cdot\\!\underline{\ell},~{}\textsf{src-
nm}(\ell^{\prime},\ell)\right)~{}\middle|~{}\ell\in
L_{\sqcup}~{}\wedge~{}(i,~{}\ell^{\prime}\\!\\!-\mbox{-}[s]\shortrightarrow\\!\ell)\in\textsf{fwd-
edges-to}(\ell)\right\\}$ $\displaystyle\cup$
$\displaystyle\left\\{\underline{\ell}^{\;(0)}\\!\cdot\\!~{}\underline{\ell}^{\;(1)}\leftarrow\llbracket\cdot\rrbracket^{\sharp}(\underline{\ell^{\prime}}\\!\cdot\\!\underline{\ell},n_{\ell^{\prime}})~{}\middle|~{}\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell\in
E_{b}\right\\}$

  * •

Computations in $C_{\sqcup}$ encode joins at program locations of forwards
indegree $\geq 2$; the abstract state at $\ell$ is the join of the abstract
states on each incoming edge to $\ell$.

$C_{\sqcup}\triangleq\left\\{n_{\ell}\leftarrow\sqcup(\underline{1}\\!\cdot\\!n_{\ell},\dots,\underline{k}\\!\cdot\\!n_{\ell})~{}\middle|~{}\ell\in
L_{\sqcup}~{}\wedge~{}k=|\textsf{fwd-edges-to}(\ell)|\right\\}$

  * •

Computations in $C_{\textsf{fix}}$ connect the $0$th and $1$st abstract
iterates at a loop head to its fixed point. The symbol fix is not a function
per se but rather an indicator of a CFG back edge that is abstractly unrolled
by the operational semantics without introducing cyclic dependencies in the
static DAIG structure itself.

$C_{\textsf{fix}}\triangleq\left\\{\underline{\ell}\leftarrow\textsf{fix}\left(\underline{\ell}^{\;(0)},\underline{\ell}^{\;(1)}\right)~{}\middle|~{}\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell\in
E_{b}\right\\}$

  * •

Finally, $C_{\nabla}$ contains widening computations at loop heads; in its
initial state, the DAIG includes only the first widen for each loop.

$C_{\nabla}\triangleq\left\\{\underline{\ell}^{\;(1)}\leftarrow\nabla(\underline{\ell}^{\;(0)},~{}~{}\underline{\ell}^{\;(0)}\\!\cdot\\!~{}\underline{\ell}^{\;(1)})~{}\middle|~{}\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell\in
E_{b}\right\\}$

Given a program’s CFG and a generic abstract interpretation interface, we can
construct an initial DAIG that is consistent with a classical (batch) abstract
interpretation:

###### Lemma 4.6 (Initial DAIG Construction, Well-Formedness, CFG-Consistency,
and AI-Consistency).

There exists a constructive procedure
$\mathcal{D}_{\small\textsf{\emph{init}}}$ such that for all well-formed
programs $\langle L,E,\ell_{0}\rangle$, the initial DAIG

$\mathcal{D}=\mathcal{D}_{\small\textsf{\emph{init}}}(\langle
L,E,\ell_{0}\rangle,\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle)$

is well formed and consistent with both the target program (i.e.
$\mathcal{D}\approxeq\langle L,E,\ell_{0}\rangle$) and underlying abstract
interpreter (i.e.
$\mathcal{D}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$).

We define such a $\mathcal{D}_{\small\textsf{init}}$ in the appendix and show
that it produces well-formed results consistent with both the target program
and the underlying abstract interpreter. Its definition tracks closely with
the informal and diagrammatic descriptions above, constructing DAIG structures
that correspond to the input CFG.

[Initial DAIG Well-Formedness, CFG-Consistency, and AI-Consistency] For all
well-formed programs $\langle L,E,\ell_{0}\rangle$,
$\mathcal{D}_{\small\textsf{init}}(\langle L,E,\ell_{0}\rangle)$ is well-
formed, $\mathcal{D}_{\small\textsf{init}}(\langle
L,E,\ell_{0}\rangle)\approxeq\langle L,E,\ell_{0}\rangle$, and
$\mathcal{D}_{\small\textsf{init}}(\langle
L,E,\ell_{0}\rangle)\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$.

###### Proof.

DAIG well-formedness holds by construction:

  * (1)

Each component of $R$ constructs reference cell names of a different
structure, so no two reference names are equal.

  * (2)

Each component of $C$ destination names of a different structure, with the
possible exception of $C_{\sqcup}$, $C_{\textsf{fix}}$, and the first
component of $C_{\llbracket\cdot\rrbracket^{\sharp}}$, all of which may
construct destination names of the form $\ell$ or $\ell^{\;(0)}$. However,
since $L_{\sqcup}$ and $L_{\not\sqcup}$ are disjoint, there is no overlap
between the destination names of $C_{\sqcup}$ and
$C_{\llbracket\cdot\rrbracket^{\sharp}}$. Furthermore, there is no overlap
between $C_{\textsf{fix}}$ and either $C_{\sqcup}$ or
$C_{\llbracket\cdot\rrbracket^{\sharp}}$ because if
$\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell\in E_{b}$ then
$n_{\ell}=\ell^{\;(0)}\neq\underline{\ell}$.

  * (3)

By construction, $n_{\ell}\rightsquigarrow n_{\ell^{\prime}}$ only if there
exists a path in $E_{f}$ from $\ell$ to $\ell^{\prime}$. CFG back edges
$\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell$ in $E_{b}$ maintain this
antisymmetry;
$n_{\ell^{\prime}}\rightsquigarrow\underline{\ell}^{\;(0)}\\!\cdot\\!\underline{\ell}^{\;(1)}\rightsquigarrow\underline{\ell}^{\;(1)}\rightsquigarrow\underline{\ell}$
through the computations of $C_{\llbracket\cdot\rrbracket^{\sharp}}$,
$C_{\nabla}$, and $C_{\textsf{fix}}$ respectively, and
$\underline{\ell}\not\rightsquigarrow n_{\ell^{\prime}}$ since $\ell^{\prime}$
is in the natural loop of $\ell$ and $\underline{\ell}$ may only appear as the
source of edges not into $\ell$’s natural loop.

  * (4)

Each edge in $C$ is well-typed by construction; names of the form
$\underline{\ell}\\!\cdot\\!\underline{\ell^{\prime}}$ and and
$\underline{i}\\!\cdot\\!\underline{\ell}\\!\cdot\\!\underline{\ell^{\prime}}$
are of type $\mathit{Stmt}$ and all others are of type $\Sigma^{\sharp}$.

  * (5)

The name of each empty reference in $R$ appears as the destination of an edge
in $C$.

We elide the details of CFG-consistency, but it is straightforward to verify
by cross-referencing the conditions of Definition 4.2 with the set
constructions of Definition 4.5. AI-consistency holds vacuously, as the only
non-empty reference of type $\Sigma^{\sharp}$ in
$\mathcal{D}_{\small\textsf{init}}$ is $\underline{\ell_{0}}$, which contains
$\varphi_{0}$. ∎

##  5\. Demanded AI by Evaluating DAIGs

In this section, we give an operational semantics for demand-driven and
incremental evaluation of DAIGs. A state in the operational semantics consists
of a DAIG $\mathcal{D}$ and also an auxiliary memoization table $M$, which can
be used to reuse previously-computed analysis results independent of program
location. Memoization tables are finite maps from names $n$ to abstract states
$\varphi\in\Sigma^{\sharp}$, and we write $M(n)$ for the abstract state mapped
to by $n$ in $M$, dom$(M)$ for the set of names in the domain of $M$, and
$M[n\mapsto\varphi]$ for the extension of $M$ with a new mapping from $n$ to
$\varphi$.

The DAIG operational semantics are split into two judgments, corresponding to
queries and edits over both analysis results and program syntax. Both
interaction modes are given in a small-step style, describing the effects of
each operation on the DAIG and auxiliary memo table.

$None$ [Q-Reuse] n[v:τ]∈R ⟨R,C⟩, M ⊢n ⇒v ; ⟨R,C⟩,M

[Q-Match] D_0=⟨R,C⟩
n[ε:τ]∈R
n←f(n_1,…,n_k)∈C

D_i-1, M_i-1 ⊢n_i ⇒v_i ; D_i,M_i (for i∈[1, k])

f ⋅(v_1 ⋯v_k)∈dom(M_k)
v=M_k(f ⋅(v_1 ⋯v_k)) D_0, M_0 ⊢n ⇒M_k(f ⋅(v_1 ⋯v_k)) ; D_k[n↦M_k(f ⋅(v_1
⋯v_k))],M_k

[Q-Miss] D_0=⟨R,C⟩
n[ε:τ]∈R
n←f(n_1,…,n_k)∈C

D_i-1, M_i-1 ⊢n_i ⇒v_i ; D_i,M_i (for i∈[1,k])

f ⋅(v_1 ⋯v_k)／∈dom(M_k)
v= f(v_1,…,v_k)
f≠fix D_0, M_0 ⊢n ⇒v ; D_k[n↦v],M_k[f ⋅(v_1 ⋯v_k)↦v]

[Q-Loop-Converge] n[ε:τ]∈R
n←fix(n_1,n_2)∈C

⟨R,C⟩, M ⊢n_1 ⇒v ; D’,M’ D’, M’ ⊢n_2 ⇒v ; D”,M”
⟨R,C⟩, M ⊢n ⇒v ; D”[n↦v],M”

[Q-Loop-Unroll] n[ε:τ]∈R
c=n←fix(ℓ^ (k-1), ℓ^ (k))∈C

⟨R,C⟩, M ⊢ℓ^ (k-1) ⇒v’ ; D’,M’
D’, M’ ⊢ℓ^ (k) ⇒v” ; D”,M”

v’≠v”
unroll(D”,c), M” ⊢n ⇒v ; D”’,M”’ ⟨R,C⟩, M ⊢n ⇒v ; D”’,M”’

Figure 8.  Operational semantics rules governing queries for the contents of a
DAIG. The judgment form $\mathcal{D},M\vdash n\Rightarrow
v~{};\mathcal{D}^{\prime},M^{\prime}$ is read as “Requesting $n$ from DAIG
$\mathcal{D}$ with auxiliary memo table $M$ yields value $v$, updated DAIG
$\mathcal{D}^{\prime}$, and updated memo table $M^{\prime}$.”

###  5.1. Query Evaluation Semantics

A query for the value of the reference cell with name $n$, given some initial
DAIG $\mathcal{D}$ and auxiliary memo table $M$, yields a value $v$ and
(possibly unchanged) DAIG and memo-table structures $\mathcal{D}^{\prime}$ and
$M^{\prime}$. This operation is defined inductively by the
$\mathcal{D},M\vdash n\Rightarrow v~{};\mathcal{D}^{\prime},M^{\prime}$
judgment form, whose inference rules are given in Fig. 8.

There are two potential ways to reuse previously-computed analysis results:
either in DAIG $\mathcal{D}$ or the auxiliary memo table $M$. The Q-Reuse rule
handles the case where the DAIG cell named by $n$ already holds a value,
returning that value and leaving the DAIG and memo table unchanged.

The Q-Match and Q-Miss rules handle the case where $n$ is empty in
$\mathcal{D}$. In both cases, queries are issued for the input cells $n_{1}$
through $n_{k}$ to the computation $f$ that outputs to $n$. In Q-Match, the
auxiliary memo table is matched: $f$ has already been computed for the
relevant inputs, so the result is retrieved from $M_{k}$, the memo table after
querying the input cells, and stored in $n$ (i.e., via
$\mathcal{D}_{k}[n\mapsto
M_{k}(\underline{f}\\!\cdot\\!(\underline{v_{1}}\cdots\underline{v_{k}}))]$).
Note that this notation is a low-level mutation of the reference cell named by
$n$, not an external edit that would trigger invalidation (which we will
describe below in Section 5.3).

Q-Miss handles memo table misses by computing and memoizing
$f(v_{1},\dots,v_{k})$ before storing the result in both the DAIG
$\mathcal{D}$ and the auxiliary memo table $M$ (i.e., at names $n$ and
$\underline{f}\\!\cdot\\!(\underline{v_{1}}\cdots\underline{v_{k}})$,
respectively).

###  5.2. Demanded Fixed Points

Demanded unrolling is the process by which we compute abstract interpretation
fixed-points over cyclic control flow graphs without introducing cyclic
dependencies into DAIGs, as described informally in Section 2 and represented
graphically in Fig. 4(c). The semantics are formalized by the Q-Loop-Converge
and Q-Loop-Unroll rules in Fig. 8.

Recall that fix is a special function symbol indicating an analysis fixed-
point computation. The destination of a fix edge is a loop-head cell for
storing a fixed-point invariant, and its sources are the two greatest abstract
iterates of said loop head yet computed. When those abstract iterates have the
same value $v$, the analysis has reached a fixed point, and a query for the
fixed point may return $v$. However, when they are unequal, a query triggers
an unrolling in the DAIG: the loop body’s abstract state reference cells are
unrolled one more iteration, the fix edge’s sources are shifted forward one
iteration, and then the fixed-point query is reissued.

This procedure differs from concrete/syntactic loop unrolling — e.g. as
applied by an optimizing compiler or bounded model checker — in that it
applies to the DAIG’s reified abstract interpretation computation, including
joins and widens, _not_ to the concrete syntax of the program under analysis.
That is, the $k$-th demanded unrolling corresponds to the $k$-th application
of the loop body’s abstract semantics (i.e. the $k$-th abstract iteration)
rather than the $k$-th concrete execution of the loop. As a result, it is
sound with respect to the concrete semantics of the program under analysis and
is guaranteed to converge.

As the name suggests, Q-Loop-Converge applies when the abstract interpretation
has reached a fixed point. Since the dependencies of the fix edge, $n_{1}$ and
$n_{2}$, are consecutive abstract iterates at the head of the corresponding
loop, their evaluation to the same value $v$ indicates that loop analysis has
converged, so $v$ may be stored in the DAIG and returned.

On the other hand, Q-Loop-Unroll applies when the abstract interpretation has
not yet reached a fixed point, since the two most recent abstract iterates are
unequal. In this case, the loop is unrolled once by the unroll helper function
and the query for the fixed point is reissued. The unroll helper function used
in Q-Loop-Unroll takes a DAIG $\mathcal{D}$ and a fix edge and unrolls the
loop corresponding to the fix edge by one iteration in $\mathcal{D}$. It is
defined as follows:

$\textsf{unroll}\left(\langle
R,C\rangle,c=\underline{\ell}\leftarrow\textsf{fix}(\underline{\ell}^{\;(k-1)},\underline{\ell}^{\;(k)})\right)\triangleq\langle
R^{\prime},C^{\prime}\rangle\text{, where}$
---
$R^{\prime}=R\cup\left\\{\textsf{incr}(n)[\varepsilon:\Sigma^{\sharp}]~{}\middle|~{}\underline{\ell}^{\;(k-1)}\\!\rightsquigarrow
n\rightsquigarrow\\!\underline{\ell}^{\;(k)}\right\\}$ and
$C^{\prime}=C/\\{c\\}\cup\left\\{\underline{\ell}\leftarrow\textsf{fix}\left(\underline{\ell}^{\;(k)},\underline{\ell}^{\;(k+1)}\right)\right\\}$
$\phantom{C^{\prime}=C/\\{c\\}}\cup\left\\{\textsf{incr-c}(c)~{}\middle|~{}\underline{\ell}^{\;(k-1)}\\!\rightsquigarrow\\!\texttt{dest}(c)\\!\rightsquigarrow\\!\underline{\ell}^{\;(k)}\right\\}$

where incr and incr-c increment the iteration counts of names. Intuitively,
unroll takes the region of the DAIG forwards-reachable from the $k-1^{th}$
abstract iterate $\underline{\ell}^{\;(k-1)}$ and backwards-reachable from the
$k^{th}$ abstract iterate $\underline{\ell}^{\;(k)}$ and duplicates it while
incrementing all name’s iterations counts from $k\\!-\\!1$ to $k$, then shifts
the fix edge forward one iteration. Crucially, this operation preserves the
DAIG acyclicity invariant.

###  5.3. Incremental Edit Semantics

An _edit_ to a DAIG $\mathcal{D}$ occurs when a value $v$ is written to some
reference cell named $n$ in $\mathcal{D}$ by an external mutator. This edit
must both update $n$ and also clear the value of (or “dirty”) any reference
cell that (transitively) depends on $n$. Here we give a full definition of the
edit operation, using the $\mathcal{D}\vdash n\Leftarrow
v_{\varepsilon}~{};\mathcal{D}^{\prime}$ judgment given in Fig. 9.

$None$[E-Commit] ∀c∈C . n∈srcs(c)⟹dest(c)[ε:τ]∈R

ℓ←fix(ℓ^ (i), ℓ^ (i+1))∈C⟹ℓ^ (1)[ε:τ]∈R

v_ε=ε ⟹ ∃c∈C . n=dest(c)

v_ε／=ε ⟹ ∃n[_:τ]∈R . v_ε: τ ⟨R,C⟩⊢n ⇐v_ε ; ⟨R,C⟩[n↦v_ε]

[E-Propagate] n↝_D n’
D⊢n’ ⇐ε ; D’
D’⊢n ⇐v_ε ; D” D⊢n ⇐v_ε ; D”

[E-Loop] ℓ←fix(ℓ^ (k-1), ℓ^ (k))∈C
⟨R,C’⟩⊢ℓ^ (1) ⇐ε ; D’

C’ = C / {ℓ←fix(ℓ^ (k-1), ℓ^ (k))}∪{ℓ←fix(ℓ^ (0), ℓ^ (1))} ⟨R,C⟩⊢ℓ^ (k) ⇐ε ;
D’

Figure 9. Operational semantics rules governing edits to the contents of a
DAIG. The judgment $\mathcal{D}\vdash n\Leftarrow
v_{\varepsilon}~{};\mathcal{D}^{\prime}$ is read as “Editing reference cell
$n$ of DAIG $\mathcal{D}$ with value $v_{\varepsilon}$ yields updated DAIG
$\mathcal{D}^{\prime}$,” where $v_{\varepsilon}$ ranges over values $v$ and
the “empty” symbol $\varepsilon$.

As described informally in Section 2, invalidation proceeds by dirtying
forwards in the acyclic DAIG, except that the implicit cyclic dependency from
fix edges must be accounted for, by rolling back to a non-dirty source cell.

The E-Commit rule is a base case: if the edited cell’s downstream dependencies
are all empty, then the edit may be performed directly. Its second premise
accounts for the implicit dependency of abstract iterate cells
$\underline{\ell}^{\;(i)}$ for $i>0$ on the fixed point cell
$\underline{\ell}$ (corresponding to the loop back edge in the control-flow
graph); it suffices to check that the $1$st abstract iterate cell has been
emptied, as all abstract iterates $\underline{\ell}^{\;(i)}$ for $i>1$ are
reachable from $\underline{\ell}^{\;(1)}$. The third and fourth premises
ensure that DAIG well-formedness is preserved, by preventing emptying of
source nodes and ill-typed edits respectively.

The E-Propagate rule recursively empties reference cells that depend on the
edited cell, eventually bottoming out when no such cells are non-empty and
E-Commit can be used to derive the $\mathcal{D}^{\prime}\vdash n\Leftarrow
v_{\varepsilon}~{};\mathcal{D}^{\prime\prime}$ premise. Note that there is no
recomputation here in E-Propagate, only emptying.

The E-Loop rule applies when the final abstract iterate of a loop is dirtied.
The sources of its fix edge are reset to its $0$th and $1$st abstract iterates
and dirtying continues from the $1$st abstract iterate. This handling is
slightly more conservative than necessary in the case that an intermediate
abstract iterate (i.e., with $k>1$) is edited since results from some previous
iterations (up to that $k$) may not need to be discarded, but it simplifies
the presentation and handles all program edits with maximal reuse.

##  6\. Soundness, Termination, and From-Scratch Consistency

In this section, we state two key properties of demanded abstract
interpretation graphs: from-scratch consistency, which guarantees that DAIG
query results are identical to the analysis results computed by the underlying
abstract interpreter at a global fixed-point, and query termination, which
guarantees termination of the DAIG query semantics even in the presence of
unbounded abstract loop unrolling. The proofs are deferred to the appendix due
to space constraints.

Both theorems rely on the preservation of DAIG well-formedness (Definition
4.1), DAIG–CFG consistency (Definition 4.2), and DAIG–AI consistency
(Definition 4.4) under queries and program edits.

###### Lemma 6.1 (DAIG Well-Formedness Preservation).

If $\mathcal{D}$ is well-formed and either $\mathcal{D},M\vdash n\Rightarrow
v~{};\mathcal{D}^{\prime},M^{\prime}$ or $\mathcal{D}\vdash n\Leftarrow
v_{\varepsilon}~{};\mathcal{D}^{\prime}$, then $\mathcal{D}^{\prime}$ is well-
formed.

[DAIG Well-Formedness Preservation] If $\mathcal{D}$ is well-formed and either
$\mathcal{D},M\vdash n\Rightarrow v~{};\mathcal{D}^{\prime},M^{\prime}$ or
$\mathcal{D}\vdash n\Leftarrow v_{\varepsilon}~{};\mathcal{D}^{\prime}$, then
$\mathcal{D}^{\prime}$ is well-formed.

###### Proof.

By structural induction on the operational semantics derivation.

Note that the only DAIG well-formedness condition that refers to reference
cells contents is (5), which is trivially preserved by each query rule
Q-$\ast$ since they never empty reference cells. Edit rule E-Commit’s third
premise ensures that edits don’t violate (5), while E-Loop and E-Propagate
only affect cells with non-zero indegree and therefore also preserve (5).
Thus, only those rules that affect the structure of the DAIG must be
considered: Q-Loop-Unroll and E-Loop.

Case Q-Loop-Unroll: By induction, $\mathcal{D}^{\prime}$ and
$\mathcal{D}^{\prime\prime}$ are well-formed. The unroll procedure preserves
well-formedness condition (1) since $incr(n)\neq n$ for each $n$ in the set of
added reference cells
$\left\\{\textsf{incr}(n)[\varepsilon:\Sigma^{\sharp}]~{}\middle|~{}\underline{\ell}^{\;(k-1)}\\!\\!\\!\rightsquigarrow
n\rightsquigarrow\\!\underline{\ell}^{\;(k)}\right\\}$ as each such $n$ is an
abstract state in a loop body and therefore has an iteration count; condition
(2) since $c$ is removed from C before it is replaced and by the same argument
as (1) for the destination of each edge in
$\left\\{\textsf{incr-c}(c)~{}\middle|~{}\underline{\ell}^{\;(k-1)}\\!\\!\\!\rightsquigarrow\\!\texttt{dest}(c)\\!\rightsquigarrow\\!\underline{\ell}^{\;(k)}\right\\}$;
conditions (3) and (4) by isomorphism from the previous iteration’s edges to
the unrolled iteration’s edges; and condition (5) since each added reference
has a corresponding added incoming edge.

Therefore, $\textsf{unroll}(\mathcal{D}^{\prime\prime},c)$ is well-formed, so
by induction $\mathcal{D}^{\prime\prime\prime}$ is well-formed.

Case E-Loop: Except for the fix edge whose inputs are changed, the
intermediate DAIG $\langle R,C^{\prime}\rangle$ is identical to $\mathcal{D}$,
which is well-formed. Therefore, $\langle R,C^{\prime}\rangle$ trivially
satisfies well-formedness conditions (1) and (3), which refer only to
references. It satisfies conditions (2) and (5) since each reference in $R$
has the same number of incoming edges in $C$ and $C^{\prime}$ because the
added and removed edge have the same destination, and condition (4) since the
sources of both the added and removed edge are of type $\Sigma^{\sharp}$.
Therefore, $\langle R,C^{\prime}\rangle$ is well-formed, so by induction
$\mathcal{D}^{\prime}$ is well-formed.

∎

###### Lemma 6.2 (DAIG–CFG Consistency Preservation).

If $\mathcal{D}\approxeq\langle L,E,\ell_{0}\rangle$ then:

  * -

if $\mathcal{D},M\vdash n\Rightarrow v~{};\mathcal{D}^{\prime},M^{\prime}$
then $\mathcal{D}^{\prime}\approxeq\langle L,E,\ell_{0}\rangle$;

  * -

if $\mathcal{D}\vdash n\Leftarrow s~{};\mathcal{D}^{\prime}$ then
$\mathcal{D}^{\prime}\approxeq\langle L,E^{\prime},\ell_{0}\rangle$, where
$E^{\prime}$ is $E$ with the edit applied (see Lemma 6.2 for details).

[DAIG–CFG Consistency Preservation] If $\mathcal{D}\approxeq\langle
L,E,\ell_{0}\rangle$ then:

  * -

if $\mathcal{D},M\vdash n\Rightarrow v~{};\mathcal{D}^{\prime},M^{\prime}$
then $\mathcal{D}^{\prime}\approxeq\langle L,E,\ell_{0}\rangle$;

  * -

if $\mathcal{D}\vdash n\Leftarrow s~{};\mathcal{D}^{\prime}$ then
$\mathcal{D}^{\prime}\approxeq\langle L,E^{\prime},\ell_{0}\rangle$, where
$E^{\prime}$ is $E$ with the edit applied.

The first bullet point states that DAIG–CFG consistency is preserved under
DAIG evaluation, while the second states that a program edit (not an arbitrary
edit to abstract state) in a DAIG consistent with an initial CFG yields a DAIG
consistent with the corresponding edited CFG.

The post-edit CFG is defined as follows: since $n$ names a reference cell of
type $\mathit{Stmt}$ in $\mathcal{D}$ and $\mathcal{D}\approxeq\langle
L,E,\ell_{0}\rangle$, $n$ is either of the form
$\underline{i}\\!\cdot\\!\underline{\ell}\\!\cdot\\!\underline{\ell}^{\prime}$
or $\underline{\ell}\\!\cdot\\!\underline{\ell}^{\prime}$, said reference cell
holds some non-$\varepsilon$ value $s^{\prime}:\mathit{Stmt}$, and
$\ell\\!-\mbox{-}[s^{\prime}]\shortrightarrow\\!\ell^{\prime}\in E$. Thus, the
post-edit CFG edges are $E^{\prime}\triangleq
E/\\{\ell\\!-\mbox{-}[s^{\prime}]\shortrightarrow\\!\ell^{\prime}\\}\cup\\{\ell\\!-\mbox{-}[s]\shortrightarrow\\!\ell^{\prime}\\}$.
That is, $E^{\prime}$ is $E$ with whichever edge corresponds to DAIG name $n$
re-labelled by $s$.

Note that this lemma as stated applies only to in-place edits of CFG edges,
but the same technique applies for deletions (which can be seen as in-place
edits where $s$ is the no-op skip statement) and insertions (for which a new
sub-DAIG is constructed and inserted, before dirtying proceeds as usual).

###### Proof (Bullet 1):.

By cases on the derivation $\mathcal{D},M\vdash n\Rightarrow
v~{};\mathcal{D}^{\prime},M^{\prime}$. All cases other than Q-Loop-Unroll are
trivial since they don’t modify the structure of the CFG.

Q-Loop-Unroll abstractly unrolls a loop body by adding DAIG reference cells
and computations with unroll. Since unroll increments the iteration counts of
names in the new unrolling, conditions (1) and (2) of 4.2 are vacuously
satisfied as they only reference the initial (i.e. zeroth) copy of loop body
reference cells. Condition (3) requires that for each fix edge, there exist
unrollings of the corresponding loop body’s DAIG region for all iterations up
to that fix edge’s sources. The $i=0$ through $i=k-1$ cases are satisfied in
the pre-unrolling DAIG, and unroll adds the $k$th unrolling by incrementing
each reference in the $k-1$th, so Q-Loop-Unroll preserves DAIG–CFG consistency
as well. ∎

###### Proof (Bullet 2):.

The proof is straightforward: the only possible structural changes from the
initial DAIG $\mathcal{D}$ to the post-edit DAIG $\mathcal{D}^{\prime}$ are
fix edges reset to $k=1$ by rule E-Loop, which preserve condition (3) of
definition Definition 4.3 for any back edges reachable from the edit. The only
possible reference cell content changes from $\mathcal{D}$ to
$\mathcal{D}^{\prime}$ are dirtied abstract state cells (which don’t affect
Definition 4.3) and the edited statement cell $r=n[s:\textit{Stmt}]$, whose
value $s$ agrees with the corresponding CFG edge in $E^{\prime}$ and thus
satisfies the relevant $r\in R$ conjunct of whichever condition of Definition
4.3 applies to its edge type (i.e. straightline forward edge, join-point
forward edge, or back edge). ∎

###### Lemma 6.3 (DAIG–AI Consistency Preservation).

If
$\mathcal{D}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$
and either $\mathcal{D},M\vdash n\Rightarrow
v~{};\mathcal{D}^{\prime},M^{\prime}$ or $\mathcal{D}\vdash n\Leftarrow
s~{};\mathcal{D}^{\prime}$, then
$\mathcal{D}^{\prime}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$.

[DAIG–AI Consistency Preservation] If
$\mathcal{D}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$
and either $\mathcal{D},M\vdash n\Rightarrow
v~{};\mathcal{D}^{\prime},M^{\prime}$ or $\mathcal{D}\vdash n\Leftarrow
s~{};\mathcal{D}^{\prime}$, then
$\mathcal{D}^{\prime}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$.

###### Proof.

The two cases in the premise of the lemma correspond to query evaluation and
program edits.

For program edits, DAIG–AI consistency is clearly preserved:

  * -

Reference cell $\underline{\ell_{0}}$ in $\mathcal{D}^{\prime}$ is unchanged
from $\mathcal{D}$ since it is not reachable from any statement-type reference
cell (which $n$ is guaranteed to be by the well-typedness premise of rule
E-Commit).

  * -

All in-degree $\geq 1$ reference cells in $\mathcal{D}^{\prime}$ are either
empty (in which case they vacuously satisfy Def. 4.4) or non-empty (in which
case they satisfy Def. 4.4 for $\mathcal{D}^{\prime}$ because they did so for
$\mathcal{D}$).

For query evaluation, we proceed by cases on the derivation of
$\mathcal{D},M\vdash n\Rightarrow v~{};\mathcal{D}^{\prime},M^{\prime}$.

  * -

The Q-Reuse and Q-Loop-Unroll cases are trivial because they do not change
reference cells contents or add non-empty reference cells.

  * -

Q-Miss’s premises are identical to Definition 4.4’s $f\neq\textsf{fix}$ case,
and Q-Match’s premises, given that
$M_{k}(\underline{f}\\!\cdot\\!(\underline{v_{1}}\cdots\underline{v_{k}}))=f(v_{1},\dots,v_{k})$
by memoization table soundness, are the same.

  * -

Q-Loop-Converge’s premises are identical to Definition 4.4’s $f=\textsf{fix}$
case.

∎

With these preservation results, we can now prove that DAIG query results for
abstract states at program locations are from-scratch consistent with the
global fixed-point invariant map of the DAIG’s underlying abstract
interpreter.

###### Theorem 6.4 (DAIG From-Scratch Consistency).

For all sound $M$ and well-formed $\mathcal{D}$ such that
$\mathcal{D}\approxeq\langle L,E,\ell_{0}\rangle$ and
$\mathcal{D}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$,
if $\mathcal{D},M\vdash\underline{\ell}\Rightarrow
v~{};\mathcal{D}^{\prime},M^{\prime}$ then
$v={\llbracket\ell\rrbracket^{\sharp}}^{\ast}_{\langle L,E,\ell_{0}\rangle}$.

[DAIG From-Scratch Consistency] For all sound $M$ and well-formed
$\mathcal{D}$ such that $\mathcal{D}\approxeq\langle L,E,\ell_{0}\rangle$ and
$\mathcal{D}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$,
if $\mathcal{D},M\vdash\underline{\ell}\Rightarrow
v~{};\mathcal{D}^{\prime},M^{\prime}$ then
$v={\llbracket\ell\rrbracket^{\sharp}}^{\ast}_{\langle L,E,\ell_{0}\rangle}$.

###### Proof.

If the reference cell named by $\underline{\ell}$ is non-empty in
$\mathcal{D}$, then Q-Reuse must be the root of the derivation
$\mathcal{D},M\vdash\underline{\ell}\Rightarrow
v~{};\mathcal{D}^{\prime},M^{\prime}$. Therefore, since
$\mathcal{D}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$,
$v=\llbracket\ell\rrbracket^{\sharp}{}^{\ast}$.

Otherwise, the reference cell named by $\underline{\ell}$ is empty in
$\mathcal{D}$ and we will proceed by cases on $\ell$, a non-join location
$\ell\in L_{\not\sqcup}$ with CFG in-degree 1, a join location $\ell\in
L_{\sqcup}$ with CFG in-degree $\geq 2$, or a loop head $\ell$ such that there
exists a back edge $\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell\in
E_{b}$. Note that $\ell_{0}$ — the only location that doesn’t fall into one of
those cases — is excluded because is the reference cell with name
$\underline{\ell_{0}}$ is non-empty by
$\mathcal{D}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$.

Case $\ell\in L_{\not\sqcup}$: Since $\mathcal{D}\approxeq\langle
L,E,\ell_{0}\rangle$, there exists an
$\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell^{\prime}\in E_{f}$,
$\underline{\ell^{\prime}}\\!\cdot\\!\underline{\ell}[s:\textit{Stmt}]\in R$,
and
$\underline{\ell}\leftarrow\llbracket\cdot\rrbracket^{\sharp}(\underline{\ell^{\prime}}\\!\cdot\\!\underline{\ell},\underline{\ell^{\prime}})\in
C$. Therefore, the root of the derivation of
$\mathcal{D},M\vdash\underline{\ell}\Rightarrow
v~{};\mathcal{D}^{\prime},M^{\prime}$ is either Q-Miss or Q-Match.

Sub-case Q-Miss: $n_{1}=\underline{\ell^{\prime}}\\!\cdot\\!\underline{\ell}$
and therefore $v_{1}=s$ by Q-Reuse. Due to the preceding preservation lemmas
and the inductive hypothesis,
$\mathcal{D}_{1},M_{1}\vdash\underline{\ell^{\prime}}\Rightarrow
v_{2}~{};\mathcal{D}_{2},M_{2}$ and
$v_{2}=\llbracket\ell^{\prime}\rrbracket^{\sharp}{}^{\ast}$. Therefore,
$v=\llbracket
s\rrbracket^{\sharp}\llbracket\ell^{\prime}\rrbracket^{\sharp}{}^{\ast}$
which, by local abstract interpreter soundness, is equal to
$\llbracket\ell\rrbracket^{\sharp}{}^{\ast}$.

Sub-case Q-Match: By the same arguments as for the Q-Miss case — which follow
from premises shared between the two rules — $v_{1}=s$ and
$v_{2}=\llbracket\ell^{\prime}\rrbracket^{\sharp}{}^{\ast}$. Therefore, by
memoization table soundness,
$v=M_{2}(\underline{\llbracket\cdot\rrbracket^{\sharp}}\\!\cdot\\!\underline{s}\\!\cdot\\!\underline{\llbracket\ell^{\prime}\rrbracket^{\sharp}{}^{\ast}})=\llbracket
s\rrbracket^{\sharp}\llbracket\ell^{\prime}\rrbracket^{\sharp}{}^{\ast}$
which, by local abstract interpreter soundness, is equal to
$\llbracket\ell\rrbracket^{\sharp}{}^{\ast}$.

Case $\ell\in L_{\sqcup}$: Since $\mathcal{D}\approxeq\langle
L,E,\ell_{0}\rangle$, there are $k$ forward CFG edges into $\ell$ and for each
such $\ell_{i}\\!-\mbox{-}[s_{i}]\shortrightarrow\\!\ell$, we have
$\underline{i}\cdot\underline{\ell}_{i}\cdot\underline{\ell}[s_{i}:\textit{Stmt}]\in
R$ and
$\underline{i}\cdot\underline{\ell}\leftarrow\llbracket\cdot\rrbracket^{\sharp}(\underline{i}\\!\cdot\\!\underline{\ell}_{i}\\!\cdot\\!\underline{\ell},~{}\underline{\ell}_{i})\in
C$. Also by $\mathcal{D}\approxeq\langle L,E,\ell_{0}\rangle$, there is an
edge
$\underline{\ell}\leftarrow\sqcup(\underline{1}\\!\cdot\\!\underline{\ell},\dots,\underline{k}\\!\cdot\\!\underline{\ell})\in
C$. Therefore, the root of the derivation of
$\mathcal{D},M\vdash\underline{\ell}\Rightarrow
v~{};\mathcal{D}^{\prime},M^{\prime}$ is either Q-Miss or Q-Match. We omit the
Q-Match subcase as it is analogous to the Q-Miss subcase in the same manner as
the previous ($\ell\in L_{\not\sqcup}$) case.

Sub-case Q-Miss: For each $i$, $n_{i}$ =
$\underline{i}\\!\cdot\\!\underline{\ell}$. Since
$\underline{i}\\!\cdot\\!\underline{\ell}_{i}\\!\cdot\\!\underline{\ell}[s_{i}:Stmt]\in
R$ and
$\underline{i}\\!\cdot\\!\underline{\ell}\leftarrow\llbracket\cdot\rrbracket^{\sharp}(\underline{i}\\!\cdot\\!\underline{\ell}_{i}\\!\cdot\\!\underline{\ell},~{}\underline{\ell}_{i})\in
C$, we know that $v_{i}=\llbracket
s_{i}\rrbracket^{\sharp}\llbracket\ell_{i}\rrbracket^{\sharp}{}^{\ast}$, as
the subquery for
$\underline{i}\\!\cdot\\!\underline{\ell}_{i}\\!\cdot\\!\underline{\ell}$
resolves to $s_{i}$ via Q-Reuse and the subquery for $\underline{\ell}_{i}$
resolves to $\llbracket\ell_{i}\rrbracket^{\sharp}{}^{\ast}$ by the inductive
hypothesis. Then, $v=\sqcup(\llbracket
s_{1}\rrbracket^{\sharp}\llbracket\ell_{1}\rrbracket^{\sharp}{}^{\ast},\dots,\llbracket
s_{k}\rrbracket^{\sharp}\llbracket\ell_{k}\rrbracket^{\sharp}{}^{\ast})$ which
by global abstract interpreter soundness is equal to
$\llbracket\ell\rrbracket^{\sharp}{}^{\ast}$ — the invariant at $\ell$ is the
join of each of its predecessor’s invariants, transformed by the abstract
semantics of the CFG edge by which they’re connected.

Case $\ell$ is a loop head: Since $\mathcal{D}\approxeq\langle
L,E,\ell_{0}\rangle$, $\ell$ is the destination of a CFG back-edge
$\ell^{\prime}\\!-\mbox{-}[s]\shortrightarrow\\!\ell\in E_{b}$ and
$\underline{\ell}$ is the destination of a DAIG fix edge
$\underline{\ell}\leftarrow\textsf{fix}(\underline{\ell}^{\;(k-1)},\underline{\ell}^{\;(k)})\in
C$.

By natural number induction, a query for $\underline{\ell}^{\;(i)}$ yields the
$i$th abstract iterate at $\underline{\ell}$. In the $i=0$ base case, a query
for $\underline{\ell}^{\;(0)}$ yields the $0$th abstract iterate at $\ell$ by
precisely the argument888Modulo the change of name; note that the initial name
$n_{\ell}$ for a loop head $\ell$ is $\underline{\ell}^{\;(0)}$ as opposed to
$\underline{\ell}$. of the previous two cases, which deal with analysis of
forwards dataflow. In the inductive case, a query for
$\underline{\ell}^{\;(k)}$ yields the $k$th abstract iterate at $\ell$, since
$\underline{\ell}^{\;(k)}\leftarrow\nabla(\underline{\ell}^{\;(k-1)},\underline{\ell}^{\;(k-1)}\\!\cdot\\!\underline{\ell}^{\;(k)})\in
C$ by $\mathcal{D}\approxeq\langle L,E,\ell_{0}\rangle$, and a query for
$\underline{\ell}^{\;(k-1)}\\!\cdot\\!\underline{\ell}^{\;(k)}$ yields the
image of the $k$th abstract iterate in the abstract semantics of the loop body
— as unrolled by definition of unroll — by local abstract interpreter
soundness and
$\mathcal{D}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$.

The root of the derivation tree of
$\mathcal{D},M\vdash\underline{\ell}\Rightarrow
v~{};\mathcal{D}^{\prime},M^{\prime}$ is either Q-Loop-Converge — in which
case the result $v$ of the subqueries for the two most recent abstract
iterates are equal and $v$ is therefore the fixed-point
$\llbracket\ell\rrbracket^{\sharp}{}^{\ast}$ — or Q-Loop-Unroll, in which case
$v$ is equal to $\llbracket\ell\rrbracket^{\sharp}{}^{\ast}$ by the inductive
hypothesis. ∎

###### Corollary 6.5.

Query results are sound.

Since the global invariant map $\llbracket\cdot\rrbracket^{\sharp}{}^{\ast}$
of the underlying abstract interpreter
$\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$
is sound (by Global Abstract Interpreter Soundness (Proposition 3.2)) and a
DAIG query for the abstract state at a location $\ell$ returns
$\llbracket\ell\rrbracket^{\sharp}{}^{\ast}$, DAIG query results themselves
are sound.

###### Theorem 6.6 (DAIG Query Termination).

For all $M$ and well formed $\mathcal{D}$ such that
$\mathcal{D}\approxeq\langle L,E,\ell_{0}\rangle$ and
$\mathcal{D}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$,
if $n$ is in the namespace of $\mathcal{D}$ then there exist
$v,\mathcal{D}^{\prime},M^{\prime}$ such that $\mathcal{D},M\vdash
n\Rightarrow v~{};\mathcal{D}^{\prime},M^{\prime}$.

[DAIG Query Termination] For all $M$ and well formed $\mathcal{D}$ such that
$\mathcal{D}\approxeq\langle L,E,\ell_{0}\rangle$ and
$\mathcal{D}\approxeq\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$,
if $n$ is in the namespace of $\mathcal{D}$ then there exist
$v,\mathcal{D}^{\prime},M^{\prime}$ such that $\mathcal{D},M\vdash
n\Rightarrow v~{};\mathcal{D}^{\prime},M^{\prime}$.

###### Proof.

Let the ancestors of a name $n$ in $\mathcal{D}$ be the set of backwards-
reachable names $\\{n^{\prime}~{}|~{}n^{\prime}\rightsquigarrow n\\}$. Note
that, since $\mathcal{D}$ is well formed and therefore acyclic, if
$n\leftarrow f(n_{1},\dots,n_{k})\in C$ then each $n_{i}$ has strictly fewer
ancestors than $n$. We will proceed by induction on the number of ancestors of
$n$.

Base case: Since $n$ has no ancestors, there is no $c\in C$ such that
$\texttt{dest}(c)=n$. Thus, by definition 4.1.5, $n$ names a non-empty
reference cell (i.e. $n[v:\tau]\in R$). Therefore, by Q-Reuse,
$\mathcal{D},M\vdash n\Rightarrow v~{};\mathcal{D},M$.

Inductive case: By well-formedness of $\mathcal{D}$ (definition 4.1.2), there
is exactly one edge $c=n\leftarrow f(n_{1},\dots,n_{k})\in C$ with destination
$n$. We proceed by cases on $f$.

Case $f\in\\{\llbracket\cdot\rrbracket^{\sharp},\sqcup,\nabla\\}$: By repeated
application of the inductive hypothesis (along with the preceding preservation
lemmas for well-formedness and CFG/AI consistency), for each $n_{i}$ we may
derive $\mathcal{D}_{i-1},M_{i-1}\vdash n_{i}\Rightarrow
v_{i}~{};\mathcal{D}_{i},M_{i}$, where $\mathcal{D}_{0}\triangleq\mathcal{D}$
and $M_{0}\triangleq M$.

Then, either
$\underline{f}\\!\cdot\\!(\underline{v_{1}}\cdots\underline{v_{k}})\in\textsf{dom}(M_{k})$,
in which case we apply Q-Match to derive

$\mathcal{D}_{0},M_{0}\vdash n\Rightarrow
M_{k}(\underline{f}\\!\cdot\\!(\underline{v_{1}}\cdots\underline{v_{k}}))~{};\mathcal{D}_{k}[n\mapsto
M_{k}(\underline{f}\\!\cdot\\!(\underline{v_{1}}\cdots\underline{v_{k}}))],M_{k}$

or
$\underline{f}\\!\cdot\\!(\underline{v_{1}}\cdots\underline{v_{k}})\not\in\textsf{dom}(M_{k})$,
in which case we apply Q-Miss to derive

$\mathcal{D}_{0},M_{0}\vdash n\Rightarrow
v~{};D_{k}[v/n],M_{k};\underline{f}\\!\cdot\\!(\underline{v_{1}}\cdots\underline{v_{k}})\mapsto
v$

where $v=f(v_{1},\dots,v_{k})$.

Case $f=\textsf{fix}$: Since $\mathcal{D}\approxeq\langle
L,E,\ell_{0}\rangle$,
$c=n\leftarrow\textsf{fix}(\underline{\ell}^{\;(k-1)},\underline{\ell}^{\;(k)})$.
By the inductive hypothesis (along with the preceding preservation lemmas for
well-formedness and CFG/AI consistency),
$\mathcal{D},M\vdash\underline{\ell}^{\;(k-1)}\Rightarrow
v_{1}~{};\mathcal{D}^{\prime},M^{\prime}$ and
$\mathcal{D}^{\prime},M^{\prime}\vdash\underline{\ell}^{\;(k)}\Rightarrow
v_{2}~{};\mathcal{D}^{\prime\prime},M^{\prime\prime}$. If $v_{1}=v_{2}$ then
Q-Loop-Converge applies and we derive $\mathcal{D},M\vdash n\Rightarrow
v_{1}~{};\mathcal{D}^{\prime\prime},M^{\prime\prime}$.

Otherwise, Q-Loop-Unroll applies but, since $n$ has more ancestors in
$\textsf{unroll}(\mathcal{D}^{\prime\prime},c)$ than in $\mathcal{D}$, we can
not simply apply induction to derive the final premise. Note, however, that
the final premise is also a query for $n$ in the unrolled DAIG, which by
definition contains the edge
$n\leftarrow\textsf{fix}(\underline{\ell}^{\;(k)},\underline{\ell}^{\;(k+1)})$
and the empty reference cell $n[\varepsilon:\tau]$; therefore, it must be
derived either by Q-Loop-Unroll or Q-Loop-Converge. If Q-Loop-Unroll is used
then this argument repeats, yielding a tree of nested applications of Q-Loop-
Unroll in direct correspondence to the sequence of abstract iterates
$\underline{\ell}^{\;(k)},\underline{\ell}^{\;(k+1)},\dots$, which is an
increasing sequence of abstract states computed by repeated application of
$\nabla$. Therefore, by the convergence property of widening in the underlying
abstract interpreter, this process may repeat only finitely many times before
Q-Loop-Converge applies, yielding a finite derivation tree.

∎

##  7\. Implementation and Evaluation

Here, we describe a prototype implementation and evaluation of demanded
abstract interpretation via our DAIG framework. Our evaluation studied two
research questions:

  * •

Expressivity: Does the DAIG framework allow for clean and straightforward
implementations of rich analysis domains that cannot be handled by existing
incremental and/or demand-driven frameworks?

  * •

Scalability: For these rich analysis domains, what degree of performance
improvement can be obtained by performing incremental and/or demand-driven
analysis, as compared to batch analysis?

###  7.1. Implementation

Our DAIG framework is implemented in approximately 2,500 lines of OCaml code
(dai-github-repo; dai-artifact-zenodo). Incremental and demand-driven analysis
logic, including demanded unrolling, operates over an explicit graph
representation of DAIGs, but per-function memoization (i.e., the auxiliary
memo table $M$ in the Fig. 8 semantics) is provided via adapton.ocaml, an
open-source implementation of the technique of
DBLP:conf/oopsla/HammerDHLFHH15.

Our implementation is parametric in an abstract domain, and the effort
required to instantiate the framework to a new abstract domain is comparable
to the effort required to do so in a classical abstract interpreter framework.
The required module signature is essentially the abstract interpreter
signature
$\langle\Sigma^{\sharp},\varphi_{0},\llbracket\cdot\rrbracket^{\sharp},\sqsubseteq,\sqcup,\nabla\rangle$,
extended with some standard utilities which can often be automatically
derived.

_Interprocedurality._ Although the formalism is defined over control-flow
graphs for clarity and brevity, our implementation supports context-sensitive
analysis of non-recursive programs with static calling semantics (i.e., no
virtual dispatch or higher-order functions).

In order to analyze such programs, we initially construct a DAIG only for the
“main” procedure in the initial context. Then, when a query is issued for the
abstract state after a call, we construct a DAIG for its callee in the proper
context. When a query is issued at a location/context for which no DAIG has
yet been constructed, we construct the DAIG for its containing function and
analyze dataflow to its entry.

These operations are parametric in a context-sensitivity policy for choosing a
context in which to analyze a callee at a call site. Our implementation
includes functors that implement context-insensitivity and also 1- and 2-call-
site-sensitivity (sharir1978two).

###  7.2. Expressivity

To demonstrate the expressivity of our DAIG framework, we have instantiated it
with three existing well-known abstract interpretation techniques — interval,
octagon and shape analysis — all of which are inexpressible using existing
incremental and/or demand-driven analysis frameworks. Here, we describe our
experience applying the DAIG-based interval and shape analyses to a small set
of programs. In Section 7.3, we use the octagon domain to investigate the
scalability of demanded analysis on synthetic benchmarks.

Together, these analysis implementations provide evidence for our approach’s
agnosticity to the underlying abstract domain, including domains with black-
box external dependencies and/or complicated non-monotone abstract operations.

_Interval Analysis._ The interval abstract domain is a textbook example of an
infinite-height lattice, requiring widening to guarantee analysis convergence.
An interval $[l,u]$ abstracts the set of numbers between lower bound $l$ and
upper bound $u$. Join and widen operations and abstract states are defined in
the standard way (DBLP:conf/popl/CousotC77). Abstract interpretation in this
domain is known as interval analysis and is commonly used, e.g., to verify the
safety of array accesses. Interval analysis has been applied at industrial
scale, for example by DBLP:conf/esop/CousotCFMMMR05.

In practice, it is common to use an optimized off-the-shelf interval abstract
domain such as that of APRON (DBLP:conf/cav/JeannetM09) or Elina
(DBLP:conf/popl/SinghPV17). We have implemented an APRON-backed interval
analysis for JavaScript programs in the DAIG framework. As an indication of
the flexibity of our framework, we were able to use the APRON library without
modification.

In order to validate our implementation, we analyzed 23 array-manipulating
programs — with functions such as contains, equals, swap, and indexof — from
the test suite of Buckets.JS, a JavaScript data structure library (buckets).

Using the 2-call-string-sensitive context policy, our analysis verified the
safety of all 85 array accesses in the programs; with 1-call-string-
sensitivity, it verified 71/74 (96%), and with context-insensitive analysis it
verified 4/18 (22%). These figures show that standard numerical analyses on
DAIGs behave as they would in a batch analysis engine.

_Shape Analysis._ Precise analysis of recursive data structures such as linked
lists is essential in many domains. Such analysis relies on complex abstract
domains that cannot be expressed in existing frameworks for incremental and
demand-driven analysis. We have implemented a DAIG-based demanded shape
analysis for singly-linked lists. An abstract state in this shape domain is a
triple consisting of

  * -

A separation logic formula over points-to ($\alpha.f\mapsto\alpha^{\prime}$)
and list-segment (lseg$(\alpha,\alpha^{\prime})$) atomic propositions, stating
respectively that the $f$ field of the object at symbolic address $\alpha$
points to $\alpha^{\prime}$ and that there exists a sequence of next pointer
dereferences from $\alpha$ to $\alpha^{\prime}$ (DBLP:conf/lics/Reynolds02),

  * -

A collection of pure constraints: equalities and disequalities over memory
addresses, and

  * -

An environment mapping variables to memory addresses.

Join, widen, and implication all rely on a collection of rewrite rules over
such states from DBLP:conf/sas/ChangRN07 (specialized to a fixed inductive
definition for list segments). All told, the implementation of this shape
domain requires approximately 500 lines of OCaml code.

We have applied this DAIG-based shape analysis to successfully verify the
correctness and memory-safety of the list append procedure of Fig. 2, along
with several linked list utilities from the aforementioned Buckets.js library
including foreach and indexof (buckets). Analysis of the
$\ell_{3}$-to-$\ell_{4}$-to-$\ell_{3}$ loop of the list append procedure
converges in one demanded unrolling with a precise result.

###  7.3. Scalability

To study scalability, we conducted an initial investigation of what
performance improvements are possible with demanded analysis variants in our
framework. We compared the performance of analysis with and without
incrementality and demand on interleaved sequences of program edits and
queries. Throughout this section, our framework is instantiated with a
context-insensitive APRON-backed octagon domain: a relational numerical domain
representing invariants of the form $\pm x\pm y\leq y$, widely used in
practice due to its balance of expressivity and efficiency
(DBLP:journals/lisp/Mine06).

Analysis Time (sec) mean p50 p90 p95 p99 Batch 9.0 1.4 18.9 36.2 173.6 Incr.
1.7 0.6 3.6 6.3 16.6 DD 1.5 0.1 3.7 7.9 16.7 I&DD 0.3 0.1 0.7 1.2 3.0

Figure 10. Performance of octagon analysis on the synthetic workload of
interleaved program edits and analysis queries described in Section 7.3. The
four scatter plots show the scaling of each configuration as the program size
is increased by edits, and their color-coding serves as a legend to the fifth
figure: a cumulative distribution plot showing the fraction of analysis runs
($y$ axis) completed by each configuration within some time interval ($x$
axis). Lastly, the table shows summary statistics for each configuration,
including the mean, median, $90$th, $95$th, and $99$th percentile analysis
latency.

To exercise the analyses, we created synthetic workloads consisting of 3,000
random edits to an initially-empty program. Programs are generated in a
JavaScript subset with assignment, arrays, conditional branching, while loops,
and (non-recursive) function calls of the form x = f(y). An “edit” is an
insertion of a randomly generated statement, if-then-else conditional, or
while loop at a randomly-sampled program location, with 85%, 10%, and 5%
probability respectively, and statements and expressions are generated
probabilistically from their respective grammars.

We evaluate four analysis configurations on this workload:

  * (1)

Batch analysis: Classical whole-program abstract interpretation, fully re-
analyzing the entire program from scratch in response to each edit.

  * (2)

Incremental analysis: An incremental-only configuration which applies the edit
semantics to dirty as few previously-computed analysis results as possible,
but eagerly recomputes all dirtied cells.

  * (3)

Demand-driven analysis: A demand-driven-only configuration which dirties the
full DAIG after each edit, but applies the query semantics to avoid computing
analysis results that aren’t demanded.

  * (4)

Incremental & demand-driven analysis: The full demanded abstract
interpretation technique, which applies both the edit and query semantics to
maximize reuse and minimize redundant computation.

In the demand-driven configurations, queries are issued at five randomly-
sampled program locations between each edit. Note that since the first three
configurations were implemented atop our DAIG framework, which is designed to
support both incremental and demand-driven analysis, they may not be as tuned
as specialized implementations.

Each plot includes data points from 9 separate trials, with fixed random seeds
such that the same edits (and, in the two demand-driven configurations,
queries) are issued to each configuration. In total, this data set includes
27,000 analysis executions in each exhaustive configuration and 135,000
queries in each demand-driven configuration.

The results, as shown in Fig. 10, indicate that while incremental and demand-
driven analysis each significantly improve analysis latencies with respect to
the batch analysis baseline, combining the two provides an additional large
reduction in latency. This effect is most apparent in the tail of the
distribution, since edits that dirty large regions of the program are costly
for incremental analysis, and queries that depend on large regions of the
graph are costly for demand-driven analysis. By combining incremental dirtying
with demand-driven evaluation, demanded abstract interpretation mitigates
these worst-case scenarios and consistently keeps analysis costs low even as
the program grows.

In particular, at the 95th percentile, the 1.2s latency of incremental demand-
driven analysis is more than five times lower than the next best
configuration, and potentially low enough to support interactive use. Fig. 10
gives a cumulative distribution of analysis latencies, again showing the large
advantage of the incremental demand-driven analysis over other configurations.

##  8\. Related Work

_Incremental Computation._ Techniques for the efficient caching and reuse of
computation results, particularly those based on memoization of pure functions
(DBLP:conf/icfp/AbadiLL96; DBLP:conf/lfp/FieldT90; DBLP:conf/popl/PughT89) and
dependency graphs (DBLP:conf/popl/DemersRT81; DBLP:conf/popl/Reps82), have
been the subject of a great deal of research and seen widespread practical
application.

More recently, dependency graph-based approaches to incremental computation
have improved on generic memoization and graph-based techniques, allowing for
fine-grained automatic caching and reuse even in the presence of changes to
inputs or an underlying data store (DBLP:conf/popl/AcarBH02;
DBLP:conf/popl/AcarAB08). Building on these graph-based techniques for self-
adjusting computation, some recent work has focused on support for interactive
and demand-driven computations (DBLP:conf/oopsla/HammerDHLFHH15;
DBLP:conf/pldi/HammerKHF14). Although this approach yields a general and
powerful system for incremental computation, its low-level primitives make it
difficult to express the complex fixed-point computation over cyclic control-
flow graphs in arbitrary abstract interpretations. We take inspiration from
demanded computation graphs but instead specialize the language of demanded
computations to demanded abstract interpretations, both with syntactic
structures and with a query/edit semantics which dynamically modifies the
dependency graph to model such computations.

_Incremental Analysis._ The application of incremental computation to program
analysis is similarly well-studied, going back at least to the development of
incremental dataflow analyses to support responsive continuous compilation
(DBLP:conf/popl/Ryder83; DBLP:conf/sigplan/Zadeck84). Recent work has
contributed incremental versions of several classes of program analysis,
including IFDS/IDE dataflow analyses (DBLP:conf/icse/ArztB14;
DBLP:conf/issta/DoALBSM17) and analyses based on extensions to Datalog
(DBLP:conf/kbse/SzaboEV16; DBLP:journals/pacmpl/SzaboBEV18). These specialized
approaches offer effective solutions for certain classes of program analysis,
but place restrictions on abstract domains that rule out arbitrary abstract
interpretations in infinite-height domains.

Compositional program analysis, in which summaries are computed for individual
files or compilation units rather than a whole program, naturally supports
incrementality in the sense that results need only be recomputed for changed
files. This has shown to be very effective for scaling program analyses to
massive codebases in CI/CD systems (DBLP:conf/nfm/CalcagnoD11;
DBLP:journals/cacm/DistefanoFLO19; DBLP:conf/foveoos/FahndrichL10), but it
operates at a much coarser granularity than both the aforementioned approaches
and our own, since it is designed to scale up to massive programs rather than
to minimize analysis latencies at development-time.

DBLP:conf/cav/LeinoW15 propose a fine-grained incremental verification
technique for the Boogie language, which verifies user-provided specifications
of imperative procedures. These specifications include loop invariants,
allowing their algorithm to ignore cyclic dependencies altogether.

_Demand-Driven Analysis._ Demand-driven techniques for dataflow analysis are
also well-studied. The intra-procedural problem was studied by
10.1007/BF00264319. Several extensions to inter-procedural analysis have been
presented, for example, by Reps1994SolvingDV, DBLP:conf/popl/DuesterwaldGS95,
and DBLP:journals/tcs/SagivRH96. In nearly all cases previous work has been
focused on finite domains. The work of DBLP:journals/tcs/SagivRH96 allows for
infinite domains of finite height, but does not consider infinite-height
domains like intervals.

Any static analysis expressible as a context-free-language reachability (CFL-
reachability) problem can be computed in a demand-driven fashion as a “single-
source” problem (reps98cfl). As such, a number of papers have presented
demand-driven algorithms for flow-insensitive pointer analysis
(DBLP:conf/pldi/HeintzeT01; sridharan05demand; DBLP:conf/ecoop/SpathDAB16).

Reference attribute grammars (RAGs) are declarative specifications of
properties over ASTs (including potentially-cyclic flow analyses) which can be
evaluated incrementally and on-demand (DBLP:journals/scp/MagnussonH07;
incremental_rag_tr). Termination of RAG evaluation requires that all cyclic
computations converge to a fixed-point in finitely-many iterations
(DBLP:journals/scp/MagnussonH07; DBLP:conf/sigplan/Farrow86); this convergence
property holds for finite domains with monotone operators but may also be
achieved through other means (e.g. widening).

Improving on prior work, our framework comes with proofs of termination and
from-scratch consistency, and specifies the exact conditions required to
ensure termination in infinite-height domains with non-monotone widening
operators.

##  9\. Conclusion

We have presented a novel framework for demanded abstract interpretation, in
which an arbitrary abstract interpretation can be made both incremental and
demand-driven. Unlike previous frameworks, ours supports arbitrary lattices
and widening operators. The framework is based on a novel demanded abstract
interpretation graph (DAIG) representation of the analysis problem, where
careful handling of loops ensures the DAIG remains acyclic. We have proved
various key properties of the framework, including soundness, termination, and
from-scratch consistency. Our implementation shows that complex analyses can
be easily implemented with our framework, with the potential for significant
performance wins in incremental and demand-driven scenarios.

###### Acknowledgements.

We thank Matthew A. Hammer and Jared Wright for their valuable contributions
in the early stages of this research. We also thank the anonymous reviewers
and members of the CUPLV lab for their helpful reviews and suggestions. This
research was supported in part by the National Science Foundation under grants
CCF-1619282, CCF-2008369, and CCF-2007024, and also by a gift from Oracle
Labs.

## References

  * (1)
  * Abadi et al. (1996) Martín Abadi, Butler W. Lampson, and Jean-Jacques Lévy. 1996.  Analysis and Caching of Dependencies. In _International Conference on Functional Programming (ICFP)_.  https://doi.org/10.1145/232627.232638
  * Acar et al. (2008) Umut A. Acar, Amal Ahmed, and Matthias Blume. 2008.  Imperative self-adjusting computation. In _Principles of Programming Languages (POPL)_.  https://doi.org/10.1145/1328438.1328476
  * Acar et al. (2002) Umut A. Acar, Guy E. Blelloch, and Robert Harper. 2002\.  Adaptive functional programming. In _Principles of Programming Languages (POPL)_.  https://doi.org/10.1145/1186634
  * Aho et al. (2006) Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006.  _Compilers: Principles, Techniques, and Tools (2nd Edition)_.
  * Arzt and Bodden (2014) Steven Arzt and Eric Bodden. 2014.  Reviser: efficiently updating IDE-/IFDS-based data-flow analyses in response to incremental program changes. In _International Conference on Software Engineering (ICSE)_.  https://doi.org/10.1145/2568225.2568243
  * Babich and Jazayeri (1978) Wayne A. Babich and Mehdi Jazayeri. 1978.  The Method of Attributes for Data Flow Analysis: Part II. Demand analysis.  _Acta Informatica_ 3 (1978).  https://doi.org/10.1007/BF00264320
  * Berdine et al. (2005) Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005\.  Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In _Formal Methods for Components and Objects (FMCO)_.  https://doi.org/10.1007/11804192_6
  * Bourdoncle (1993) François Bourdoncle. 1993\.  Efficient chaotic iteration strategies with widenings. In _Formal Methods in Programming and Their Applications_.  https://doi.org/10.1007/BFb0039704
  * Calcagno and Distefano (2011) Cristiano Calcagno and Dino Distefano. 2011.  Infer: An Automatic Program Verifier for Memory Safety of C Programs. In _NASA Formal Methods (NFM)_.  https://doi.org/10.1007/978-3-642-20398-5_33
  * Chang et al. (2007) Bor-Yuh Evan Chang, Xavier Rival, and George C. Necula. 2007\.  Shape Analysis with Structural Invariant Checkers. In _Static Analysis (SAS)_.  https://doi.org/10.1007/978-3-540-74061-2_24
  * Cousot and Cousot (1977) Patrick Cousot and Radhia Cousot. 1977.  Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In _Principles of Programming Languages (POPL)_.  https://doi.org/10.1145/512950.512973
  * Cousot et al. (2005) Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2005\.  The ASTREÉ Analyzer. In _European Symposium on Programming (ESOP)_.  https://doi.org/10.1007/978-3-540-31987-0_3
  * Demers et al. (1981) Alan J. Demers, Thomas W. Reps, and Tim Teitelbaum. 1981\.  Incremental Evaluation for Attribute Grammars with Application to Syntax-Directed Editors. In _Principles of Programming Languages (POPL)_.  https://doi.org/10.1145/567532.567544
  * Distefano et al. (2019) Dino Distefano, Manuel Fähndrich, Francesco Logozzo, and Peter W. O’Hearn. 2019.  Scaling static analyses at Facebook.  _Commun. ACM_ 8 (2019).  https://doi.org/10.1145/3338112
  * Distefano et al. (2006) Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2006\.  A Local Shape Analysis Based on Separation Logic. In _Tools and Algorithms for the Construction and Analysis of Systems (TACAS)_.  https://doi.org/10.1007/11691372_19
  * Do et al. (2017) Lisa Nguyen Quang Do, Karim Ali, Benjamin Livshits, Eric Bodden, Justin Smith, and Emerson R. Murphy-Hill. 2017.  Just-in-time Static Analysis. In _Software Testing and Analysis (ISSTA)_.  https://doi.org/10.1145/3092703.3092705
  * Duesterwald et al. (1995) Evelyn Duesterwald, Rajiv Gupta, and Mary Lou Soffa. 1995\.  Demand-Driven Computation of Interprocedural Data Flow. In _Principles of Programming Languages (POPL)_.  https://doi.org/10.1145/199448.199461
  * Fähndrich and Logozzo (2010) Manuel Fähndrich and Francesco Logozzo. 2010.  Static Contract Checking with Abstract Interpretation. In _Formal Verification of Object-Oriented Software (FoVeOOS)_.  https://doi.org/10.1007/978-3-642-18070-5_2
  * Farrow (1986) Rodney Farrow. 1986\.  Automatic generation of fixed-point-finding evaluators for circular, but well-defined, attribute grammars. In _Compiler Construction (CC)_.  https://doi.org/10.1145/12276.13320
  * Field and Teitelbaum (1990) John Field and Tim Teitelbaum. 1990.  Incremental Reduction in the lambda Calculus. In _LISP and Functional Programming_.  https://doi.org/10.1145/91556.91679
  * Hammer et al. (2015) Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael W. Hicks, and David Van Horn. 2015.  Incremental computation with names. In _Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)_.  https://doi.org/10.1145/2814270.2814305
  * Hammer et al. (2014) Matthew A. Hammer, Yit Phang Khoo, Michael Hicks, and Jeffrey S. Foster. 2014.  Adapton: composable, demand-driven incremental computation. In _Programming Language Design and Implementation (PLDI)_.  https://doi.org/10.1145/2594291.2594324
  * Heintze and Tardieu (2001) Nevin Heintze and Olivier Tardieu. 2001.  Demand-Driven Pointer Analysis. In _Programming Language Design and Implementation (PLDI)_.  https://doi.org/10.1145/378795.378802
  * Horwitz et al. (1995) Susan Horwitz, Thomas W. Reps, and Shmuel Sagiv. 1995\.  Demand Interprocedural Dataflow Analysis. In _Foundations of Software Engineering (FSE)_.  https://doi.org/10.1145/222124.222146
  * Jeannet and Miné (2009) Bertrand Jeannet and Antoine Miné. 2009.  Apron: A Library of Numerical Abstract Domains for Static Analysis. In _Computer-Aided Verification (CAV)_.  https://doi.org/10.1007/978-3-642-02658-4_52
  * Leino and Wüstholz (2015) K. Rustan M. Leino and Valentin Wüstholz. 2015.  Fine-Grained Caching of Verification Results. In _Computer-Aided Verification (CAV)_.  https://doi.org/10.1007/978-3-319-21690-4_22
  * Magill et al. (2006) Stephen Magill, Aleksandar Nanevski, Edmund Clarke, and Peter Lee. 2006.  Inferring invariants in separation logic for imperative list-processing programs. In _Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE)_.
  * Magnusson and Hedin (2007) Eva Magnusson and Görel Hedin. 2007.  Circular reference attributed grammars - their evaluation and applications.  _Sci. Comput. Program._ 1 (2007).  https://doi.org/10.1016/j.scico.2005.06.005
  * Miné (2006) Antoine Miné. 2006\.  The octagon abstract domain.  _High. Order Symb. Comput._ 1 (2006).  https://doi.org/10.1007/s10990-006-8609-1
  * Pugh and Teitelbaum (1989) William Pugh and Tim Teitelbaum. 1989.  Incremental Computation via Function Caching. In _Principles of Programming Languages (POPL)_.  https://doi.org/10.1145/75277.75305
  * Reps (1998) Thomas Reps. 1998\.  Program analysis via graph reachability.  _Information and Software Technology_ 11-12 (1998).  https://doi.org/10.1016/S0950-5849(98)00093-7
  * Reps (1982) Thomas W. Reps. 1982\.  Optimal-Time Incremental Semantic Analysis for Syntax-Directed Editors. In _Principles of Programming Languages (POPL)_.  https://doi.org/10.1145/582153.582172
  * Reps (1994) Thomas W. Reps. 1994\.  Solving Demand Versions of Interprocedural Analysis Problems. In _Compiler Construction (CC)_.  https://doi.org/10.1007/3-540-57877-3_26
  * Reynolds (2002) John C. Reynolds. 2002\.  Separation Logic: A Logic for Shared Mutable Data Structures. In _Logic in Computer Science (LICS)_.  https://doi.org/10.1109/LICS.2002.1029817
  * Ryder (1983) Barbara G. Ryder. 1983\.  Incremental Data Flow Analysis. In _Principles of Programming Languages (POPL)_.  https://doi.org/10.1145/567067.567084
  * Sadowski et al. (2018) Caitlin Sadowski, Edward Aftandilian, Alex Eagle, Liam Miller-Cushon, and Ciera Jaspan. 2018\.  Lessons from building static analysis tools at Google.  _Commun. ACM_ 4 (2018).  https://doi.org/10.1145/3188720
  * Sagiv et al. (1996) Shmuel Sagiv, Thomas W. Reps, and Susan Horwitz. 1996\.  Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation.  _Theor. Comput. Sci._ 1&2 (1996).  https://doi.org/10.1016/0304-3975(96)00072-2
  * Santos (2016) Mauricio Santos. 2016\.  _Buckets-JS: A JavaScript Data Structure Library_.  https://github.com/mauriciosantos/Buckets-JS.
  * Sharir and Pnueli (1981) Micha Sharir and Amir Pnueli. 1981.  Two Approaches to Interprocedural Data Flow Analysis.  In _Program Flow Analysis: Theory and Applications_.
  * Singh et al. (2017) Gagandeep Singh, Markus Püschel, and Martin T. Vechev. 2017\.  Fast polyhedra abstract domain. In _Principles of Programming Languages (POPL)_.  https://doi.org/10.1145/3093333.3009885
  * Söderberg and Hedin (2012) Emma Söderberg and Görel Hedin. 2012.  Incremental Evaluation of Reference Attribute Grammars using Dynamic Dependency Tracking.  LU-CS-TR:2012-249 (2012).
  * Späth et al. (2016) Johannes Späth, Lisa Nguyen Quang Do, Karim Ali, and Eric Bodden. 2016.  Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java. In _Object-Oriented Programming (ECOOP)_.  https://doi.org/10.4230/DARTS.2.1.12
  * Sridharan et al. (2005) Manu Sridharan, Denis Gopan, Lexin Shan, and Rastislav Bodík. 2005.  Demand-Driven Points-To Analysis for Java. In _Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)_.  https://doi.org/10.1145/1094811.1094817
  * Stein et al. (2021a) Benno Stein, Bor-Yuh Evan Chang, and Manu Sridharan. 2021a.  _DAI: Demanded Abstract Interpretation_.  https://github.com/cuplv/dai.
  * Stein et al. (2021b) Benno Stein, Bor-Yuh Evan Chang, and Manu Sridharan. 2021b.  _Demanded Abstract Interpretation (artifact)_.  https://doi.org/10.5281/zenodo.4663292.
  * Szabó et al. (2018) Tamás Szabó, Gábor Bergmann, Sebastian Erdweg, and Markus Voelter. 2018.  Incrementalizing lattice-based program analyses in Datalog. In _Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)_.  https://doi.org/10.1145/3276509
  * Szabó et al. (2016) Tamás Szabó, Sebastian Erdweg, and Markus Voelter. 2016\.  IncA: a DSL for the definition of incremental program analyses. In _Automated Software Engineering (ASE)_.  https://doi.org/10.1145/2970276.2970298
  * Zadeck (1984) F. Kenneth Zadeck. 1984\.  Incremental data flow analysis in a structured program editor. In _Compiler Construction (CC)_.  https://doi.org/10.1145/502874.502888