# Efficient Path-Sensitive Data-Dependence Analysis

Peisen Yao  The Hong Kong University of Science and TechnologyHong Kong, China
<EMAIL_ADDRESS>,  Jinguo Zhou  Ant GroupChina<EMAIL_ADDRESS>,  Xiao
Xiao  Ant GroupChina<EMAIL_ADDRESS>,  Qingkai Shi  The Hong Kong
University of Science and TechnologyChina<EMAIL_ADDRESS>,  Rongxin Wu
Xiamen UniversityChina<EMAIL_ADDRESS>and  Charles Zhang  The Hong Kong
University of Science and TechnologyHong Kong, China<EMAIL_ADDRESS>
###### Abstract.

This paper presents a scalable path- and context-sensitive data-dependence
analysis. The key is to address the aliasing-path-explosion problem via a
sparse, demand-driven, and fused approach that piggybacks the computation of
pointer information with the resolution of data dependence. Specifically, our
approach decomposes the computational efforts of disjunctive reasoning into 1)
a context- and semi-path-sensitive analysis that concisely summarizes data
dependence as the symbolic and storeless value-flow graphs, and 2) a demand-
driven phase that resolves transitive data dependence over the graphs. We have
applied the approach to two clients, namely thin slicing and value flow
analysis. Using a suite of 16 programs ranging from 13 KLoC to 8 MLoC, we
compare our techniques against a diverse group of state-of-the-art analyses,
illustrating significant precision and scalability advantages of our approach.

data-dependence analysis, pointer analysis, path-sensitive analysis

††ccs: Theory of computation Program analysis

##  1\. Introduction

Data-dependence analysis aims to identify the def-use information in a
program. However, the presence of pointers and references obscure such
information. The analysis must cut through the tangle of aliasing to reason
about data dependence, which serves as a substrate for many program analysis
clients, such as impact analysis (Arnold, 1996) and program slicing (Sridharan
et al., 2007).

Path-sensitivity is a common axis for pursuing precision, yet is stunningly
challenging for data-dependence analysis, which can suffer from the “aliasing-
path-explosion” problem For instance, at a load statement $p=*x$, we need to
track the path condition of this statement, and the path conditions under
which $x$ points-to different memory objects. Each load or store statement may
access hundreds of memory objects, each memory object may be accessed at
dozens or hundreds of locations in the program, and the number of calling
contexts under which the statements execute can be exponential. Consequently,
the number of disjunctive cases to track grow extremely large, far too many to
enable a scalable analysis.

Existing path-sensitive data-dependence analyses can be classified into two
major categories. The “fused” approach can path-sensitively reasons about
data-dependence information without a points-to analysis as a priori, such as
symbolic execution (Cadar et al., 2008). The fused approach uses various
logics to generate formulas encoding the entire history of memory writes and
reads, which allow for establishing correlations between variables
automatically. However, it encodes constraints following control-flow paths,
regardless of whether they are relevant to the data dependence of interests or
not. Such “dense” analysis is known to have performance problems. For
instance, Focal (Kim et al., 2019), a state-of-the-art backward symbolic
executor, takes almost 230 hours in answering on-demand queries for a program
with near 33 KLoC.

Alternatively, the staged approach leverages an independent pointer analysis
to approximate the def-use information, which is then leveraged to bootstrap
the path-sensitive data-dependence analysis (Yan et al., 2018; Blackshear et
al., 2013). Although the idea of leveraging pre-computed pointer information
has advanced flow- and/or context-sensitive analysis (via sparsification (Yan
et al., 2018), pruning (Fink et al., 2006), or partitioning (Kahlon, 2008)),
how to replicate this success for path-sensitive data-dependence analysis
remains an open question.

The problem of computing transitive data-dependence relations can be
formulated as a graph reachability problem, where value-flow graphs varying in
precision act as the reachability indices. Without an index, the approaches
like symbolic execution are hard to scale, whether it be exhaustive or demand-
driven. When computing the index, there is a tension between tracking path-
sensitive pointer information too early (Livshits and Lam, 2003; Hackett and
Aiken, 2006; Dillig et al., 2011)–which leads to the overwhelming cost of
value-flow graph construction–and tracking path-sensitive pointer information
too late–which reduces the benefits of path-sensitivity, because pointer
information can be spuriously and/or redundantly propagated (Yan et al.,
2018).

In this paper, we present Falcon, a fused and sparse approach to path-
sensitive data-dependence analysis, which piggybacks the computation of
pointer information with the resolution of data dependence. The key insight is
that an data-dependence relation induced by pointer expressions can be
identified without knowing the concrete memory objects referenced by the
pointers. This enables us to efficiently and precisely build a reachability
index for value flows, alleviating the need for explicitly and repeatedly
enumerating sheer amounts of points-to information.

We first introduce an all-program-points but lazy pointer analysis: it
constructs the symbolical and compositional value-flow graphs for the entire
program, without computing exhaustive points-to information. The graphs act as
the “conduits” for tracking transitive data dependence in a sparse and demand-
driven manner. Our analysis provides the key precision benefit that path-
sensitivity brings, paths pruning and merging, via lightweight semi-decision
procedures. To achieve context-sensitivity but avoid expensive summary
cloning, it only clones the memory access-path expressions that are rooted at
a function parameter and incur side-effects, thus enabling local reasoning of
value flows, as opposed to global reasoning about the entire heap.

We then present two client analyses, thin slicing based program understanding
(Sridharan et al., 2007; Li et al., 2016) and value-flow analysis based bug
hunting (Sui et al., 2012; Shi et al., 2018; Yan et al., 2018). Crucially, the
guards qualifying the graph edges have concisely merged value flows going
through different memory objects. The clients (1) do not need to perform
explicit cast-splitting over the points-to sets when handling indirect
reads/writes, thereby alleviating a major source of case explosion in previous
path-sensitive analyses (Manevich et al., 2004; Blackshear et al., 2013; Yan
et al., 2018), because the size of a points-to set could be very large, and
(2) can sparsely track the value flows by following the value-flow edges,
aiding scalability. In summary, our approach separates the task of reasoning
about “how the values flow through different memory objects” from answering
queries about data dependence.

Specifically, there are two novel and critical features in our algorithm
itself:

  * •

The pointer analysis for building value-flow graphs is both on-the-fly sparse
and path-sensitive, in that it computes the heap def-use chains incrementally,
along with the path-sensitive pointer information discovered. The Spas
algorithm (Sui et al., 2011) is the only previous work that has the same
property, but they achieve incremental sparsity by following the level-by-
level analysis (Yu et al., 2010) and, thus, is exhaustive.

  * •

When answering demand data-dependence queries, our analysis can stop as soon
as enough evidence is gathered, without trying to find all pointed-by memory
objects. The previous analyses (Zheng and Rugina, 2008; Yan et al., 2011;
Späth et al., 2016; Späth et al., 2019) can answer demand alias queries
directly, via different storeless representations (Kanvar and Khedker, 2016).
However, none of the techniques can introduce path sensitivity.

Overall, this paper makes the following key contributions:

  * •

We identify and discuss the major challenges of scaling path-sensitive data-
dependence analysis.

  * •

We introduce an efficient path-sensitive data-dependence analysis, which, for
the first time, allow us to analyze multi-million-line code bases with the
precision of full path-sensitivity in minutes.

  * •

We demonstrate the utility of our approach with two clients, namely thin
slicing and value flow analysis.

  * •

We conduct a significant experiment on 16 real-world programs ranging from 13
KLoC to 8 MLoC.

    * –

In building value-flow graphs, Falcon outperforms Svf (Sui and Xue, 2016b),
Sfs (Hardekopf and Lin, 2011), and Dsa (Lattner et al., 2007), achieving on
average 17$\times$, $25\times$, and 4.4$\times$ speedups, respectively.

    * –

Compared with Supa (Sui and Xue, 2016a, 2018), the state-of-the-art demand-
driven flow- and context-sensitive pointer analysis for C/C++, Falcon is
54$\times$ in answering thin slicing queries, and it improves the precision by
1.6$\times$.

    * –

In comparison with Cred (Yan et al., 2018), a state-of-the-art path-sensitive
value flow analysis for bug hunting, Falcon is on average 6$\times$ faster,
and finds more real bugs (21 vs. 12) with a lower false-positive rate (25% vs.
47.8%).

##  2\. Overview

Figure 1.  An example comparing the conventional value-flow graph and our
value-flow graph for answering demand queries. In (b), the label on an edge
represents a memory object. In (c), the label on an edge is a path condition.

We take the program in Fig. 1 as an example to motivate the path-sensitive
data-dependence analysis, highlight its challenges, and explain the essence of
our approach.

#### Importance of Path-Sensitive Data-Dependence Information

Suppose we need to detect double-free bugs for the program in Fig. 1(a). In
this program, there are two memory deallocation statements free(a) and
free(e). Observe that the value of $a$ can flow to $e$ only under the
condition $\neg\phi_{2}$. Thus, the program is safe, because the deallocation
statements execute under the condition $\phi_{2}$.

Assume that we only approximate the data-dependence information with a path-
insensitive pointer analysis, and then partially track path correlations of
the memory deallocation statements. The pointer analysis can tell that $e$ may
be data-dependent on $a$, meaning that $e$ and $a$ may point-to the same
memory object. Observe that the path conditions for the two statements free(a)
and free(e) are both $\varphi_{2}$, which do not conflict with each other.
Here, if taking $\varphi_{2}$ as the path condition of a double-free
vulnerability, our analysis would raise a false alarm, because the condition
for $e$ to be data-dependent on $a$ is $\neg\varphi_{2}$. To summarize, the
imprecise data-dependence information caused by the points-to analysis would
be passed on to the clients, hurting the precision.

#### Problem of Aliasing-Path-Explosion

However, obtaining path-sensitive data-dependence information is far from
trivial, because tracking path-sensitive pointer information can require
reasoning about a considerable number of disjunctive cases. For instance, at a
load statement $p=*x$, we need to track the path condition of this statement,
and the path conditions under which $x$ points-to different memory objects.
each load or store statement may access hundreds of memory objects, each
memory object may be accessed at dozens or hundreds of locations in the
program, and the number of calling contexts under which the statements execute
can be exponential. In summary, the transfer function for each statement needs
to store and propagate an enormous amount of information. We term the problem
_aliasing-path-explosion_ : analyzing path-sensitive data-dependence
information can lead to reasoning about an excessive number of paths
(Blackshear et al., 2013).

#### The State-of-the-Art

A recent analysis (Yan et al., 2018) has leveraged the idea of _sparsity_ to
refine the flow-insensitive results into a path-sensitive one on demand. It
first constructs the flow-insensitive def-use chains with a pre-analysis,
which then enable the primary path-sensitive analysis to be performed sparsely
(Sui and Xue, 2016a, 2018; Yan et al., 2018). For instance, as shown in Fig.
1(b), the two edges between $*x=a$ and $d=*x$ state that the value of pointer
$a$ can flow to the pointer $d$ via the memory objects $o_{1}$ or $o_{2}$,
implying that $d$ may be data-dependent on $a$. The pre-computed def-use
chains enable the primary path-sensitive analysis to be performed sparsely
(Sui and Xue, 2016a, 2018; Yan et al., 2018).

However, the flow-insensitive pre-analysis drops path information. When
answering demand queries, the primary analysis still suffers from the
aliasing-path-explosion. For example, suppose a client asks, “what are the set
of variables $e$ may be data-dependent on?” Following their work (Yan et al.,
2018), we perform an on-demand backward traversal from $e=*y$ to
$*x=a,*x=b,*y=c$, respectively. Apparently, in the worst case, such graph
traversal needs to search five paths and solve five path constraints. This
number of paths exceeds the total number of paths in the program (which is
four), meaning that the aliasing-path-explosion can be even worse than the
well-known scalability problem caused by conditional branching in symbolic
execution.

In essence existing sparse analysis can use a pre-analysis to identify the
relevant memory objects (as in Fig. 1(b)). However, the pre-analysis can only
reduce the number of memory objects to track, but not the number of value flow
paths going through the relevant memory objects, because it is unaware of the
path conditions qualifying the value flows. When going for path sensitivity,
the primary path-sensitive analysis phase cannot avoid aliasing-path-
explosion.

#### Our Approach

At a high level, our approach works in two phases. In the first phase, we
compute the guarded and storless value-flow graphs. In the second stage, the
clients can utilize the graphs to track transitive program dependence on
demand. The crux is to judiciously merge abstract states while building the
graphs, since when and how to merge them drastically affect the accuracy and
performance of the client analyses.

We observe that many memory objects and paths qualifying data-dependence
relations are redundant, which can be symbolically identified and merged. For
example, intuitively, the variable $d$ may be data-dependent $a$, no matter
$x$ points-to $o_{1}$ or $o_{2}$. However, the analysis in the previous work
(Yan et al., 2018) _has to_ separate the two edges and label them with
different memory objects, so that it can preserve the capability of precision
refinement based on the memory objects.

Based on the observation, our key idea is to use a symbolical storeless
representation for pointer expressions, which concisely “index” how values
flow in and out of the memory in a precision-preserving manner. Crucially, as
illustrated in Fig. 1(c), our first phase takes advantage of a lightweight
semi-decision procedure to achieve the following two merits, which
significantly reduces the burden of the second phase: ① it can efficiently
prune a number of infeasible value flows; and ② it can effectively merge and
simplify path constraints at the time of merging value-flow edges. Besides, to
build interprocedural value-flow graphs, it only clones the memory access-path
expressions that are rooted at a function parameter and incur side-effects,
there by avoiding computing a whole-program image of the heap.

Then, in the second phase, we can answer demand data-dependence queries for
variables of interest. For example, consider the graph in Fig. 1(c), where the
memory objects pointed-by $x$ and $y$ are implicit.

  * •

To determine the values that $e$ is data-dependent on, we perform a backward
graph traversal, and only have to traverse two paths, i.e., from $e$ to $c$
and $a$, respectively.

  * •

To detect double free bugs, we perform a forward traverse from $a$ to $e$,
collecting the guard qualifying the edges (i.e.,
$\neg\varphi_{2}\land\neg\varphi_{2}$). We then collect the path conditions of
the two statements free(a) and free(e) (i.e., $\varphi_{2}\land\varphi_{2}$).
Clearly, we can eliminate the false positive because
$\neg\varphi_{2}\land\varphi_{2}$ is unsatisfiable.

##  3\. Preliminaries

This section presents the basic terminologies and notations used in the paper,
including the language, abstract domains, as well as the guarded value-flow
graph.

We formalize our analysis with a simple language, as in Fig. 2. Programs are
in the static single assignment form. Statements include address-taken
statements, common assignments, $\phi$-assignments, loads, stores, branches,
returns, procedure calls, and sequencing. In the $\phi$-assignment,
$\gamma_{i}$ is the gated function for each $v_{i}$, which means $v=v_{i}$ if
and only if $\gamma_{i}$ is satisfied. Such gated functions can be computed in
almost linear time (Ottenstein et al., 1990). With no loss of generality, we
assume each function has only one return statement.

$\displaystyle\begin{split}\textit{Program}\ \ P&:=F+\\\ Function\ \
F&:=f(v_{1},v_{2},...)\\{S;\\}\\\ Statement\ \ S&:=v_{1}=\&v_{2}\\\ &\ |\
v_{1}=v_{2}\ |\ v=\phi((\gamma_{1},v_{1}),(\gamma_{2},v_{2}),...)\\\ &\ |\
v_{1}=*v_{2}\ |\ *v_{1}=v_{2}\\\ &\ |\ \textit{if}\ (v)\ \textit{then}\ S_{1}\
\textit{else}\ S_{2}\ |\ \textit{return}\ v\\\ &\ |\ r=\textit{call}\
f(v_{1},v_{2},...)\ |\ S_{1};S_{2}\end{split}$ Figure 2.  The syntax of the
language.

#### Abstract Domains

The symbols and abstract domains are listed in Fig. 3. A label
$\ell\in\mathcal{L}$ indicates the position of a statement in the control flow
graph. An abstract value $v\in\mathcal{V}$ is a pointer that points-to a
memory location. A memory object $o\in\mathcal{O}$ represents a memory
location that may contain different abstract values on different guard
conditions $\psi$. We factor the abstract domain to the points-to environment
$\mathbb{E}$ and abstract store $\mathbb{S}$. $\mathbb{E}(v)=\\{(\psi,o)\\}$
means that the pointer $v$ points-to the memory object $o$ under the condition
$\psi$. $\mathbb{S}(o)=\\{(\psi,\ell,v)\\}$ states that the memory object
contains the value $v$, which is stored into the memory object at the program
point $\ell$ on the condition $\psi$. For simplicity, we define the operation
$\Pi_{\psi}$, so that we can query $\mathbb{E}$ and $\mathbb{S}$ under a
precondition $\psi$. Formally,

$\Pi_{\psi}(\mathbb{S}(o))=\\{(\pi\land\psi,\ell,v)\ |\
(\pi,\ell,v)\in\mathbb{S}(o)\\}$
$\Pi_{\psi}(\mathbb{E}(v))=\\{(\pi\land\psi,o)\ |\ (\pi,o)\in\mathbb{E}(v)\\}$

$\displaystyle\begin{split}Labels\ \ \ell&\in\mathcal{L}\\\ Values\ \
v&\in\mathcal{V}\\\ Objects\ \ o&\in\mathcal{O}\\\ Guard\ \
\psi&:=\textit{true}\ |\ \textit{false}\ |\ \psi_{0}\land\psi_{1}\ |\
\psi_{0}\lor\psi_{1}\ |\ \neg\psi\\\ Environment\ \
\mathbb{E}&:=\mathcal{V}\to 2^{(\psi,\mathcal{O})}\\\ Store\ \
\mathbb{S}&:=\mathcal{O}\to 2^{(\psi,\mathcal{L},\mathcal{V})}\\\ \end{split}$
Figure 3.  The abstract domains.

#### Guarded Value-Flow Graph

Intuitively, a value $q$ flows to $p$ if $q$ is assigned to $p$ directly (via
an assignment, such as $p=q$) or indirectly (via pointer dereferences, such as
$*x=q;y=x;p=*y;$). Formally, we define the guarded value-flow graph as below.

###### Definition 3.1.

(Guarded Value-Flow Graph) A guarded value-flow graph is a directed graph
$\mathcal{G}=(\mathcal{N},\mathcal{E},\mathcal{C})$, where $\mathcal{N}$,
$\mathcal{E}$, and $\mathcal{C}$ are defined as following:

  * •

$\mathcal{N}$ is a set of nodes, each of which is denoted by $v{@}\ell$,
meaning that the variable $v$ is defined or used at a program location $\ell$.

  * •

$\mathcal{E}\subseteq\mathcal{V}\times\mathcal{V}$ is a set of edges, each of
which represents a value-flow relation.
$(v_{1}{@}\ell_{1},v_{2}{@}\ell_{2})\in\mathcal{E}$ means that the value
$v_{1}{@}\ell_{1}$ flows to $v_{2}{@}\ell_{2}$.

  * •

$\mathcal{C}$ maps each edge in the graph to a condition $\psi$, meaning that
the value-flow relation holds only when the condition is satisfied.

Our approach first computes a guarded value-flow graph for each function. A
specific client of data-dependence analysis can then be reduced to graph
reachability problems, whereby the local value-flow graphs are stitched
together by matching formal and actual parameters as well as return value and
its receivers.

To achieve path-sensitivity, for a value-flow edge that only holds under some
condition, we label the edge with the constraint $\psi$. To establish such
guarded edges, the key is to record what values will be stored into a memory
object at a store statement (e.g., $*x=q$) and query what values can be loaded
at a load statement (e.g., $p=*y$). We will detail this process in the
following sections.

##  4\. Intraprocedural Analysis

This section presents our intraprocedural analysis to compute $\mathbb{E}$ and
$\mathbb{S}$, so that we can establish indirect value flows by querying what
values can be loaded at a load statement. We first define the abstract
transformers, which enables a conventional data-flow analysis. At the end of §
4.1, we summarize the challenges for optimization, which are addressed in §
4.2 and § 4.3.

###  4.1. Abstract Transformers

Fig. 4 lists the rules for analyzing the basic statements. The rule for
$\ell,\psi:stmt$ states that under the current points-to environment
$\mathbb{E}$, abstract store $\mathbb{S}$, and path condition $\psi$, the
statement $stmt$ produces new points-to environment $\mathbb{E^{\prime}}$
and/or abstract store $\mathbb{S^{\prime}}$.

$\inference[\textsc{addr}(\ell,\psi:p=\&a)]{\text{
}}{\mathbb{E}^{\prime}(p)=(\psi,\textit{alloc}_{a})}$

$\inference[\textsc{copy}(\ell,\psi:p=q)]{\forall(\pi,o)\in\Pi_{\psi}(\mathbb{E}(q))}{\mathbb{E}^{\prime}(p)=\mathbb{E}(p)\cup\\{(\pi,o)\\}}$

$\inference[\textsc{phi}(\ell,\psi:p=\phi((\gamma_{1},p_{1}),...,(\gamma_{n},p_{n}))]{\forall
i\in[1,n],\\\
\forall(\pi,o)\in\Pi_{\gamma_{i}}(\mathbb{E}(p_{i}))}{\mathbb{E}^{\prime}(p)=\mathbb{E}(p)\cup\\{(\pi,o)\\}}$

$\inference[\textsc{store}(\ell,\psi:*x=q)]{\forall(\pi,o)\in\Pi_{\psi}(\mathbb{E}(x))\\\
}{\mathbb{S^{\prime}}(o)=\mathbb{S}(o)\cup\\{(\pi,\ell,q)\\}}$

$\inference[\textsc{load}(\ell,\psi:p=*y)]{\forall(\pi,o)\in\Pi_{\psi}(\mathbb{E}(y))\\\
\forall(\varphi,\ell^{\prime},v)\in\Pi_{\pi}(\mathbb{S}(o))\\\
}{\mathbb{E^{\prime}}(p)=\mathbb{E}(p)\cup\Pi_{\varphi}(\mathbb{E}(v))}$

Figure 4. Basic rules for updating $\mathbb{E}$ and $\mathbb{S}$.

Rule addr creates memory objects at allocation sites. Rule copy and Rule phi
are self-explanatory; thus, we focus on the store and load rules.

Rule store processes a store statement $*x=q$ under path condition $\psi$,
which results in new configurations of the abstract store $\mathbb{S}$. We
first query the memory objects $x$ may point-to, denoted
$\Pi_{\psi}(\mathbb{E}(x))$. For all guarded memory objects
$(\pi,o)\in\Pi_{\psi}(\mathbb{E}(x))$, we update the abstract store
$\mathbb{S}$ to record the values that $o$ may hold. Following conventional
singleton-based algorithms, if $x$ points-to at most one concrete memory
object, we can perform an indirect strong update, which kills other values
hold by the memory object $o$ (Emami et al., 1994; Hardekopf and Lin, 2009,
2011; Lhoták and Chung, 2011; Yu et al., 2010).

Given a load statement $p=*y$ under path condition $\psi$ at program location
$\ell$, we apply Rule load as follows. Similar to the store rule, we query the
memory objects that $y$ may point-to under the condition $\psi$, denoted
$\Pi_{\psi}(\mathbb{E}(y))$. We then fetch the values from each memory object
$(\pi,o)\in\Pi_{\psi}(\mathbb{E}(y))$, denoted $\Pi_{\pi}(\mathbb{S}(o))$.
Finally, for every $(\varphi,\ell^{\prime},v)\in\Pi_{\pi}(\mathbb{S}(o))$, we
update $\mathbb{E}$ by adding the points-to set of $v$ under condition
$\varphi$ as a subset of the points-to set of $p$.

#### Merging Value-Flow Edges

Recall from § 3 that our analysis computes a guarded value-flow graph that
summarizes value flows induced by the memory. We formalize the rule of
building indirect value-flow edges in Fig. 5. The vflow rule states that when
$q{@}\ell_{1}$ and $p{@}\ell_{2}$ are stored and loaded from the same memory
object $o$, $p{@}\ell_{2}$ may alias with $q{@}\ell_{1}$.

$\inference[\textsc{ \qquad\qquad vflow}(\ell_{1},\psi_{1}:*x=q;\ \cdots;\
\ell_{2},\psi_{2}:p=*y)]{\forall(\pi_{i},o_{i})\in\Pi_{\psi_{2}}(\mathbb{E}(y))\\\
\forall(\varphi_{i},\ell_{1},q)\in\Pi_{\pi_{i}}(\mathbb{S}(o_{i}))}{(q@\ell_{1},p@\ell_{2})\in\mathcal{E},\mathcal{C}((q@\ell_{1},p@\ell_{2}))=\vee\varphi_{i}}$
Figure 5. Building indirect value-flow edges.

In the rule, suppose
$\Pi_{\psi_{2}}(\mathbb{E}(y))=\\{(\pi_{1},o_{1}),(\pi_{2},o_{2})\\}$ such
that $(\varphi_{1},\ell_{1},q)\in\Pi_{\pi_{1}}(\mathbb{S}(o_{1}))$ and
$(\varphi_{2},\ell_{1},q)\in\Pi_{\pi_{2}}(\mathbb{S}(o_{2}))$. As illustrated
in Fig. 1(b), conventional approaches build flow-insensitive value-flow edges
(Sui and Xue, 2016a; Yan et al., 2018). Thus, they have to distinguish a value
flow induced by different memory objects, so that they can preserve the
capability of precision refinement based on the memory objects. Such methods,
however, can still suffer from the aliasing-explosion-problem, making the
analysis not scalable.

To tackle the problem, the vflow rule merges the value-flow edges, which not
only reduces the number of edges, but also can normalize and simplify the
conditions based on some simple rewriting rules. For example, when merging two
value-flow edges under the conditions $\psi\land\pi$ and $\neg\psi\land\pi$
respectively, the condition can be simplified as $\pi$ after merging.

#### Challenges

However, a highly precise (e.g., flow- and path-sensitive) analysis that uses
the above rules to compute value-flow edges is notoriously expensive, due to
the following challenges:

  1. (1)

_Conservative propagation_. Propagating data-flow facts along control flows is
expensive and unnecessary (Hardekopf and Lin, 2011). To mitigate this problem,
data-flow facts can be propagated along with def-use chains. However, the def-
use information of memory objects is unavailable without a pointer analysis.
To resolve the paradox, most existing work (Hardekopf and Lin, 2011; Ye et
al., 2014; Sui et al., 2016; Sui and Xue, 2016a; Yan et al., 2018) perform a
lightweight but imprecise pointer analysis to over-approximate the def-use
chains. Due to the imprecision, many false def-use relations are introduced,
hurting performance.

  2. (2)

_Constraints explosion_. Our analysis needs to account for a sheer number of
guard updates for each statement, quickly causing the explosion of
constraints. For a demand-driven analysis, it is both intractable and
unnecessary to pay the full price of path-sensitive reasoning up front.

We address these challenges by the following means:

  * •

The first challenge is addressed via an _on-the-fly sparse_ analysis, which
computes def-use relations incrementally during the analysis, instead of
relying on precomputed imprecise def-use chains (§ 4.2).

  * •

The second challenge is addressed via a _semi-path-sensitive_ analysis that
simplifies and partially solves the constraints, to merge redundant value-flow
edges and prune obviously false value-flow edges (§ 4.3).

###  4.2. On-the-Fly Sparse Analysis

To address the challenge of conservative propagation, we utilize the idea of
sparsity to skip unnecessary control flows when propagating data-flow facts.
To this end, instead of leveraging the imprecise def-use relations computed by
a pre-analysis, we construct the def-use relations incrementally during the
analysis, along with the precise pointer information discovered. To formally
present the idea, we maintain the abstract store $\mathbb{S}$ as a set of
$\mathbb{S}_{\mathsf{b}}$, which describes the abstract store at the basic
block $\mathsf{b}$. Then the store and load rules are refined as follows.

#### The store Rule

We follow the idea in SSA form where a variable defined at a basic block
$\mathsf{b}$ can only be used in a basic block dominated by $\mathsf{b}$ or in
the dominance frontier where the definition is merged with other definitions
(Cytron et al., 1991). Suppose at basic block $\mathsf{b}$, a store statement
writes a guarded value $(\varphi,\ell,v)$ to the memory object $o$. As shown
in Alg. 1, it takes two steps to update the abstract store. First, we write
$(\varphi,\ell,v)$ into the local store $\mathbb{S}_{\mathsf{b}}(o)$ (Line 3).
Second, we propagate the abstract value to the dominance frontiers of
$\mathsf{b}$. We update the guard for the propagated abstract value, which is
the conjunction of $\varphi$ and the path condition of $\mathsf{b}$ (Lines
4-5). Note that it is unnecessary to propagate the abstract value to basic
blocks dominated by $\mathsf{b}$, because at the load time, we can walk up the
dominance tree to find the corresponding definitions (see the next paragraph).

Input: A store statement $\ell,\psi,*x=v$

Output: Update the abstract store $\mathbb{S}$

1 $\mathsf{b}\leftarrow$ the basic block of $\ell$;

2 for  _$(\pi,o)\in\Pi_{\psi}(\mathbb{E}(x))$_ do

3
$\mathbb{S}_{\mathsf{b}}(o)\leftarrow\mathbb{S}_{\mathsf{b}}(o)\cup\\{(\pi,\ell,v)\\}$
;

4 for  _$\mathsf{b}^{\prime}$ is a dominance frontier of  $\mathsf{b}$_ do

5
$\mathbb{S}_{\mathsf{b}^{\prime}}(o)\leftarrow\mathbb{S}_{\mathsf{b}^{\prime}}(o)\cup\\{(\pi\land\psi,\ell,v)\\}$
;

6

Algorithm 1 Write a value to memory objects and propagate the value Figure 6.
An example on sparse analysis.

###### Example 4.1.

Consider the program in Fig. 6. After $\ell_{1},\ell_{2}$, the variables $x,y$
points-to allocm, allocn, respectively. Suppose we are analyzing the store
statement $*x=d$ at basic block $\mathsf{b}_{2}$. The abstract value
$(\psi,\ell_{4},d)$ is stored into allocm and then propagated to the local
abstract store of $\mathsf{b}_{2}$’s dominance frontier $\mathsf{b}_{4}$.
Therefore, we have
$\mathbb{S}_{\mathsf{b}_{2}}(\textit{alloc}_{m})=\\{(\psi,\ell_{4},d)\\}$ and
$\mathbb{S}_{\mathsf{b}_{4}}(\textit{alloc}_{m})=\\{(\psi,\ell_{4},d)\\}$.
Similarly, after analyzing the store statement $*y=d$, we have
$\mathbb{S}_{\mathsf{b}_{3}}(\textit{alloc}_{n})=\\{(\neg\psi,\ell_{5},d)\\}$
and
$\mathbb{S}_{\mathsf{b}_{4}}(\textit{alloc}_{n})=\\{(\neg\psi,\ell_{5},d)\\}$.

#### The load Rule

As shown in Alg. 2, for a load statement $u=*x$ at the basic block
$\mathsf{b}$, we track the values that can be read from the memory objects
pointed-by $x$. For each memory object $o$, it suffices to walk up the
dominance tree (Lines 6-15) to gather abstract values until a strong update is
found. The basic idea behind the approach is that the definition of a variable
must dominate its uses. Clearly, this is a linear search in the dominance
tree.

Input: A load statement $\ell,\psi:u=*x$

Output: Values that can be loaded from $*x$

1

2$R\leftarrow\emptyset$; $\mathsf{b}\leftarrow$ the basic block of $\ell$;

3 for  _$(\beta,o)\in\Pi_{\psi}(\mathbb{E}(x))$_ do

4 $R\leftarrow R\ \cup$ ReadFromObject($\beta,o,\mathsf{b}$);

5

6return $R$;

7 Function  _ReadFromObject(_$\beta,o,\mathsf{b}$_)_:

8 $\sigma\leftarrow\texttt{true},R_{o}\leftarrow\emptyset$;

9 while  _$\mathsf{b}\neq null$_ do

10 for  _$(\pi,\ell^{\prime},v)\in\mathbb{S}_{\mathsf{b}}(o)$_ do

11 $\varphi\leftarrow\pi\land\sigma\land\beta$;

12 if  _$\varphi$ is satisfiable_ then

13 $R_{o}\leftarrow R_{o}\cup\\{(\varphi,\ell^{\prime},v)\\}$;

14

15 if  _$(\pi,\ell^{\prime},v)$ is a strong update at $\mathsf{b}$_ then

16 return $R_{o}$;

17 $\sigma\leftarrow\neg\pi\land\sigma$ ;

18

19 $\mathsf{b}\leftarrow$ the immediate dominator of $\mathsf{b}$;

20 return $R_{o}$;

21

Algorithm 2 Read values from memory objects by walking up the dominator tree

###### Example 4.2.

Consider the program in Fig. 6. When analyzing the load statement $f=*x$ at
the basic block $\mathsf{b}_{4}$, we need to read values from the memory
objects pointed-by $x$. To this end, we gather abstract values stored into
allocm that is pointed-by $x$. To do this, the sub-procedure ReadFromObject
only visits two basic blocks $\mathsf{b}_{4}$ and $\mathsf{b}_{1}$ by walking
up the dominator tree. From $\mathsf{b}_{4}$, we can read the value
$(\psi,\ell_{4},d)$, which is written into allocm at $\mathsf{b}_{2}$ and
propagated to $\mathsf{b}_{4}$. From $\mathsf{b}_{1}$, we can read the value
$(\psi,\ell_{3},c)$, which is written into allocm at $\mathsf{b}_{1}$ that
dominates $\mathsf{b}_{4}$.

###  4.3. Semi-Path-Sensitive Analysis

Path-sensitivity comes in many flavors, depending on the kind of information
encoded as constraints. Previous work on path-sensitive pointer analysis
either adopts relatively coarse abstractions where Boolean variables abstract
just the control flow, ignoring the actual predicate of a condition (Sui et
al., 2011); or takes expensive abstractions with first-order theory formulas
tracking data predicates, which can incur huge overhead (Livshits and Lam,
2003; Hackett and Aiken, 2006; Dillig et al., 2011).111Livshits and Lam (2003)
invoke a computer algebra system. Hackett and Aiken (2006) implement a
procedure similar to bit-blasting that translates arithmetic constraints to
SAT constraints. Dillig et al. (2011) use the Mistral SMT solver.

For constructing the guarded value-flow graph, we explore a sweet spot in the
space; it is _semi-path-sensitive_ from the two aspects below.

  * •

First, the guards are conceptually first-order formulas, but abstracted as
Boolean skeletons. For instance, we abstract the two branch conditions $x>2$
and $x\leq 2$ to fresh Boolean literals $p$ and $\neg p$, respectively. Such
encoding allows for certain degrees of branch correlation tracking. The design
is similar in spirit to the DPLL($T$) lazy SMT solving architecture, which
separates propositional reasoning and theory reasoning in a modular and
demand-driven way (Nieuwenhuis et al., 2006).

  * •

Second, instead of applying a full-featured SAT/SMT solver, we adopt several
linear time semi-decision procedures such as unit-propagation (Zhang and
Stickely, 1996) for identifying “easy” unsatisfiable or valid constraints, as
well as performing logical simplifications. In our experiment, we observe that
about 70% of the path conditions constructed in the analysis are satisfiable.
For the remaining ones, 80% of them are easy constraints and can be solved
with the semi-decision procedures.

Many infeasible path-sensitive data-flow facts can be filtered because
programmers tend to maintain an implicit and simple correlation of conditional
points-to relations, both for ensuring some required logical properties and
the good human readability. The semi-path-sensitive analysis makes this
correlation explicit.

#### Benefits

Compared with the state of the arts that construct the value-flow graph via a
flow-insensitive points-to analysis and label the edge with a memory object
(Sui et al., 2016; Yan et al., 2018), our analysis has two major benefits.
First, it catches the path correlations between different statements, thus
pruning more infeasible value flows than path-insensitive analyses. Second, it
concisely merges and simplifies the guards qualifying a value flow, when
merging the value-flow edges between load and store statements.

###### Example 4.3.

Consider the program in Fig. 1(a). Observe that the variable $x$ may point-to
$o_{1}$ or $o_{2}$. A path-insensitive algorithm will conclude that $d$ may
alias with $\\{a,b\\}$, where $b$ is a false positive. We now explain
intuitively how our algorithm works and prunes the false positive. Let us
consider the two cases where $x$ points-to $o_{1}$ or $o_{2}$, respectively.
First, if $x$ points-to $o_{1}$, as in Fig. 7(a), our analysis will obtain the
following values that may flow to $d{@}d=*x$:

  1. (1)

$(\varphi_{1}\land\neg\varphi_{2},a)$

  2. (2)

$(\varphi_{1}\land\varphi_{2}\land\neg\varphi_{2},b)$

The semi-path-sensitive analysis can decide that the guard of the second item
is unsatisfiable. Hence, the value $b$ is pruned. Second, if $x$ points-to
$o_{2}$, as in Fig. 7(b), the analysis can also prune the value $b$. Finally,
after merging the two graphs induced by $o_{1}$ and $o_{2}$, we obtain the
graph in Fig. 7(c).

Figure 7.  Pruning and merging value-flow graph edges for the program in Fig.
1(a).

#### Summary

The on-the-fly sparse analysis and the semi-path-sensitive analysis conspire
to address the challenges of conservative propagation and constraints
explosion (§ 4.1). The sparse analysis skips unnecessary control flows when
propagating data-flow facts, thereby improving the analysis efficiency. The
semi-path-sensitive analysis removes a lot of false pointer information, which
not only improves precision but also benefits efficiency because smaller
points-to sets lead to less work (Lhoták and Hendren, 2008; Smaragdakis et
al., 2014).

##  5\. Interprocedural Analysis

The tenet of our interprocedural analysis is breaking down the entire
abstraction into smaller components to enable on-demand resolution of alias
relations. To achieve context-sensitivity but avoid expensive summary cloning,
we first introduce the approach to building concise function summaries. We
then sketch the process of constructing inter-procedural value-flow graph.

#### Call Graph

A pointer analysis often faces the “chicken-and-egg” problem: performing the
analysis requires a call graph, which also needs reasoning about function
pointers (Grove and Chambers, 2001). In our approach, we consult a flow- and
context-insensitive analysis (Zhang et al., 2013) for obtaining a sound call
graph. Previous works (Milanova et al., 2004; Hardekopf and Lin, 2011) have
shown that a precise call graph for C-like programs can be constructed using
only flow-insensitive analysis. For C++ programs, we adopt the class hierarchy
analysis to resolve virtual function calls (Dean et al., 1995).

###  5.1. Cloning-Based Analysis with Concise Function Summaries

For building interprocedural value-flow graphs, we perform a bottom-up and
summary-based analysis. To achieve context-sensitivity, conventional summary-
based analyses conservatively identify the side effects of a function, which
are then cloned at every call site of the summarized function in the upper-
level callers (Xie and Aiken, 2005; Dillig et al., 2011). However, the size of
the side-effect summary can quickly explode, becoming a significant obstacle
to scalability. To illustrate, consider the program in Fig. 8(a). In
conventional approaches, the summary of foo is the points-to information,
$\mathbb{E}$ and $\mathbb{S}$, of the interface variable $y$ at the exit point
of foo. That is,

$\displaystyle\begin{split}\mathbb{E}(y)&=\\{(\texttt{true},o)\\};\ \
\mathbb{S}(o)=\\{(\varphi,\ell_{2},c),(\neg\varphi,\ell_{3},a)\\};\end{split}$

By cloning the summary to the two call sites in qux and bar, the two variables
$a$ and $c$ are cloned twice. When the summaries of qux and bar are cloned to
their upper-level callers, $a$ and $c$ will continue to be cloned. As a
result, the summary size will grow exponentially.

To mitigate the problem, our basic idea is to introduce symbolic auxiliary
variables, each of which stands for a class of variables to clone. Then we can
only clone a single auxiliary variable during interprocedural analysis,
reducing the burden of cloning. For the above example, we introduce an extra
value $R$ for the function foo to represent all values (e.g., $a$ and $c$)
stored in the memory object pointed-by $y$. As a result, the function summary
gets smaller as the following, and we only need to clone a single variable $R$
to the callers during the interprocedural analysis.

$\displaystyle\begin{split}\mathbb{E}(y)&=\\{(\texttt{true},o)\\};\ \
\mathbb{S}(o)=\\{(\texttt{true},\ell_{4},R)\\};\\\
R&\mapsto\\{(\varphi,\ell_{2},c),(\neg\varphi,\ell_{3},a)\\}\\\ \end{split}$

Intuitively, this process amounts to adding an extra return value to the
function foo, as shown in Fig. 8(b). Formally, this summarization process is
illustrated in Alg. 3, where the points-to results are always merged into a
single auxiliary variable so that the burden of the cloning processes can be
reduced. Each auxiliary variable stands for a modified non-local memory object
accessed through an access path rooted at an interface variable. In
conclusion, the summarization scheme enables local reasoning of the value
flows, as opposed to global reasoning about the entire heap.

Figure 8.  An example of using concise summary and performing on-demand
search.

Input: An interface variable (parameter or return) $x$

Output: Updated $\mathbb{E},\mathbb{S}$ with auxiliary variables

1 $WL\leftarrow\\{x\\}$;

2 while  _$WL$ is not empty_ do

3 $x\leftarrow$ pop an element from $WL$;

4 $R,o_{x}\leftarrow$ create an auxiliary variable and a memory object;

5 for  _$(\pi,o)\in\mathbb{E}(x)$_ do

6 for  _$(\varphi,\ell^{\prime},v)\in\Pi_{\pi}(\mathbb{S}(o))$_ do

7 $\mathbb{E}(R)\leftarrow\mathbb{E}(R)\cup\Pi_{\varphi}(\mathbb{E}(v))$ ;

8

9 $\mathbb{E}(x)\leftarrow\\{(\texttt{true},o_{x})\\}$,
$\mathbb{S}(o_{x})\leftarrow\\{(\texttt{true},\\_,R)\\}$;

10 if  _$R$ is a pointer_ then

11 $WL\leftarrow WL\cup\\{R\\}$

Algorithm 3 Summarize an interface variable

###  5.2. Constructing the Value-Flow Graphs

Alongside the analysis, we have been able to construct the value-flow graph (§
3) for each function. The graph has two types of edges representing value-flow
relations: the _direct edge_ connects a store to a load using the rule in Fig.
5, and the _summary edge_ connects $s$ to $t$ if $s$ can transitively flow to
$t$. The analysis eagerly connects the summary edges between a formal argument
(formal-in) at the function entry and the return value (formal-out) at the
function exit. As shown in Fig. 8(c), the local value-flow graphs are stitched
together by matching formal and actual parameters as well as return value and
its receivers.

##  6\. Answering Demand Queries

The storeless value-flow graphs allow tracking of transitive data dependence
in a demand-driven fashion. By a forward or backward graph traversal, the
graphs can be adopted in various applications.

#### Thin Slicing for Program Understanding

The first typical application is thin Slicing (Sridharan et al., 2007; Li et
al., 2016), which can be implemented via a backward traversal on the value-
flow graph. Thin slicing is introduced by Sridharan et al. (2007) to
facilitate program debugging and understanding. A thin slice for a program
variable, a.k.a., the slicing seed, includes only the _producer statements_
that directly affect the values of the variable. In contrast to conventional
slicing, control dependence and the data dependence of the variable’s base
pointer are excluded. Hence, thin slices are typically much smaller than
conventional program slices.

###### Example 6.1.

Consider the program in Figure 8. To build the thin slice for the slicing seed
$m$ at function qux, we only need to traverse the value-flow graphs from $m$
in a reversed direction. Such a traversal will visit all program statements
that need to be included in the slice. For instance, $*y=a$ and $*y=b$ will be
visited and included in the thin slice as they are the producer statements of
the variable $m$.

#### Value Flow Analysis for Bug Hunting

The second typical application is _value flow analysis_ (Cherem et al., 2007;
Sui et al., 2012). The analysis of value flows underpins the inspection of a
broad range of software bugs, such as the violations of memory safety (e.g.,
null dereference, double free, etc.), the violations of resource usage (e.g.,
memory leak, socket leak, etc.), and security problems (e.g., the use of
tainted data). Clearly, it is of vital importance to precisely resolve value
flows caused by pointer aliasing, which is the key problem we address in the
paper. Value flow analysis can be implemented via a forward traversal on the
value-flow graphs, during which the alias constraints and property-specific
constraints can be gathered together and handed to an SMT solver.

###### Example 6.2.

Suppose we need to detect double-free bugs for the program in Figure 8(a). We
traverse its value-flow graphs (Figure 8(c)) starting from $a$ and obtain one
path from $a$ to $n$. We then stitch together the path condition under which
$n$ is data-dependent on $a$ (i.e., $\neg\varphi$), and the path conditions of
the two statements free(a) and free(n) (i.e., $\varphi\land\varphi$). Observe
that we do not compute the interprocedural data dependence between $(a,m)$ or
$(c,n)$.

When used for full path-sensitive value flow analysis, our design has two
advantages. First, it enhances precision, as a combined domain of pointer and
source-sink information allows more precise information than could be obtained
by solving each domain separately (Cousot and Cousot, 1979; Fink et al.,
2006). Second, it allows scalability, because the client (1) does not need to
perform explicit cast-splitting over the points-to sets when handling indirect
reads/writes, alleviating a major source of case explosion in previous work
(Manevich et al., 2004; Blackshear et al., 2013; Yan et al., 2018); (2)
sparsely tracks the value flows by following the data-dependence edges; and
(3) can make distinctions between memory objects summarized by an access path
on demand. Consequently, the client concentrates computational effort on the
path- and context-sensitive pointer information only when it matters to the
properties of interest.

#### Summary

Both the value-flow graphs building phase and the on-demand analysis phase are
sparse, by piggybacking the computation of pointer information with the
resolution of data dependence. The two phases mitigate the aliasing-path-
explosion problem as follows. First, when constructing the value-flow graphs,
duplicate edges are merged, many false edges are pruned, and the data-
dependence guards are significantly simplified (§ 4). Second, when resolving
transitive data dependence over the graphs, the concise summaries serve as the
“conduits” to allow values of interests flow in and out of the function scope.
In particular, the client (1) does not need to perform explicit cast-splitting
over the points-to sets when handling indirect reads/writes, alleviating a
major source of case explosion in previous work (Manevich et al., 2004;
Blackshear et al., 2013; Yan et al., 2018); (2) can sparsely track the value
flows by following the data-dependence edges; and (3) can make distinctions
between memory objects summarized by an access path on demand. Consequently,
the client analysis can concentrate computational effort on the path- and
context-sensitive pointer information only when it matters to the properties
of interest.

##  7\. Evaluation

To demonstrate the utility of Falcon, we examine its scalability in
constructing the value-flow graphs (§ 7.2), and apply it to two practical
clients, namely semi-path-sensitive thing slicing (§ 7.3), and fully path-
sensitive bug hunting (§ 7.4).

#### Implementation

We have implement Falcon on top of LLVM 3.6. While the language in § 3 has
restricted language constructs, our implementations support most features of
C/C++, such as unions, arrays, classes, dynamic memory allocation, and virtual
functions. Arrays are considered monolithic. Falcon is _soundy_ (Livshits et
al., 2015), which means that it handles most language features in a sound
manner, while it also applies some unsound choices as in previous works (Babic
and Hu, 2008; Xie and Aiken, 2005). For instance, we unroll each loop twice on
the control flow graph and call graph, do not handle inline assembly, assume
distinct parameters are not alias with each other.

###  7.1. Experimental Setup

#### Baselines

In this section, we compare Falcon against three groups of analyses.

  1. (1)

First, we compare with the following analyses for constructing the value-flow
graphs: (1) Svf (Sui and Xue, 2016b), an inclusion-based, flow- and context-
insensitive pointer analysis; 222https://github.com/SVF-tools/SVF (2) Sfs
(Hardekopf and Lin, 2011), an inclusion-based, flow-sensitive, context-
insensitive pointer analysis; (3) Dsa (Lattner et al., 2007), a unification-
based, flow-insensitive, context-sensitive pointer analysis.
333https://github.com/seahorn/sea-dsa

  2. (2)

Second, for the thin slicing client, we compare with Supa (Sui and Xue, 2016a,
2018), 444https://github.com/SVF-tools/SUPA the state-of-the-art demand-driven
flow- and context-sensitive pointer analysis for C/C++. Supa relies on Svf to
build the value-flow graphs, base on which it answers demand queries.

  3. (3)

Finally, we compare with Cred (Yan et al., 2018), a state-of-the-art path-
sensitive pointer analysis for bug hunting.555The tool is not open-source. We
implement the algorithm on top of Svf.

All of these analyses are filed-sensitive, meaning that each field of a struct
is treated as a separate variable.

We cannot compare with the pointer analyses in (Guyer and Lin, 2005; Yu et
al., 2010; Li et al., 2011, 2013; Sui et al., 2011, 2014; Zhao et al., 2018)
because their implementations are not publicly available. For bug finding, we
tried our best to compare with Saturn (Hackett and Aiken, 2006) and Compass
(Dillig et al., 2010, 2011), but they are not runnable on the experimental
environment that we are able to set up.

#### Subjects and Environment

Tbl. 1 shows the benchmarks. Six of them are taken from SPEC CINT2000 and ten
from open-source projects. The programs cover a wide range of applications
such as text editors and database engines, and their sizes vary from 13 KLoC
to 8 MLoC. Note that since Falcon unrolls loops on the control flow graph and
call graph, we feed the same transformed code to other tools. All experiments
are conducted on a 64-bit machine with 40 Intel Xeon E5-2698<EMAIL_ADDRESS>GHz and
256 GB of RAM. All runtime numbers are medians of three runs.

###  7.2. Value-flow Graph Construction

First, we examine the scalability of Falcon for constructing value-flow
graphs. The cutoff time per tool per program is 12 hours.

####  Comparing with Svf, Sfs, and Dsa

Tbl. 1 and Fig. 9 show the results of the four analyses. In terms of runtime
overhead, we can see that they perform similarly in small-sized programs.
However, on programs with more than 500 KLoC, Svf and Sfs get derailed and
become orders-of-magnitude more expensive. In particular, both fail to analyze
mysql, rethinkdb, and firefox within 12 hours. Dsa is comparable to Falcon on
vim and php, but much slower than Falcon on other large programs (git, wrk,
libicu, and mysql). Also, Dsa cannot finish the analysis of rethinkdb and
firefox. To sum up, Falcon is on average 17$\times$, $25\times$, and
4.4$\times$ faster than Svf, Sfs, and Dsa, respectively. In terms of memory
consumption, on average, Falcon takes 1.4$\times$, 1.9$\times$, and
4.2$\times$ less memory than Svf, Sfs, and Dsa, respectively.

Table 1. Benchmark size (KLoC) and runtime (in minutes) of building value-flow
graphs.

Program | Size | Svf | Sfs | Dsa | Falcon | Falcon(Pi) | Falcon(Sat)
---|---|---|---|---|---|---|---
crafty | 13 |  $<$0.1 |  $<$0.1 |  $<$0.1 |  $<$0.1 | 0.2 | 1.9
eon | 22 | 0.3 | 0.7 | 0.2 | 0.3 | 0.4 | 2.1
gap | 36 | 0.4 | 1.7 | 0.9 | 0.5 | 0.7 | 13
vortex | 49 | 0.1 | 0.2 |  $<$0.1 | 0.3 | 0.3 | 26
perlbmk | 73 | 0.7 | 2.7 | 2.1 | 2.1 | 3.2 | 125
gcc | 135 | 0.7 | 7.4 | 8.6 | 7.8 | 8.1 | 145
git | 185 | 121 | 243 | 21 | 10 | 16 | 393
vim | 333 | 186 | 221 | 17 | 14 | 23 | 484
wrk | 340 | 85 | 115 | 131 | 6 | 15 | 537
libicu | 537 | 454 | 570 | 37 | 5 | 6 | OOT
php | 863 | 519 | 614 | 12 | 12 | 41 | OOT
ffmpeg | 967 | 43 | 122 | 113 | 13 | 36 | OOT
ppsspp | 1648 | 34 | 94 | 92 | 8 | 25 | OOT
mysql | 2030 | OOT | OOT | 113 | 46 | 64 | OOT
rethinkdb | 3776 | OOT | OOT | OOT | 90 | 113 | OOT
firefox | 7998 | OOT | OOT | OOT | 167 | 273 | OOT
OOT means the analysis runs out of the time budget (12 hours).

Figure 9.  Comparing time and memory cost of value-flow graphs construction.

We attribute the graceful scalability of Falcon to two factors. First, the
combination of on-the-fly sparsity and semi-path-sensitivity translates into
significant gains in both precision and performance (§ 4). Second, we do not
clone the full points-to information to achieve context-sensitivity. Instead,
we leverage a concise summary to avoid computing a whole-program image of the
heap (§ 5).

#### The Effects of Semi-Decision Procedures

To understand the effects of constraint solving, we set up two additional
configurations of Falcon for constructing value-flow graphs. Specifically,
Falcon-PI is path-insensitive, while Falcon-SAT uses a full-featured SAT
solver. The last three columns of Tbl. 1 compare the three configurations.
Falcon is usually more–and occasionally much more–efficient than Falcon-PI,
due to the increased precision. However, Falcon-SAT is not a good choice in
practice: its precision is offset by unbearable runtime overhead. In
particular, Falcon-SAT runs out of the time budget for all programs of more
than 500 KLoC.

The results indicate that solving constraints when building value-flow graphs
pays off, which naturally raises the question: could we do better by tuning
the semi-decision procedure more aggressively? However, we find that being
“too aggressive” can lead to performance overhead that overwhelms the
benefits. For instance, we tried the $O(n^{3})$ Gaussian elimination algorithm
for solving linear constraints, leaving the analysis hard to scale to millions
of lines of code. Adapting the decision procedures defines a sophisticated
design space that deserves further optimizations.

Figure 10.  Number of constraints Falcon deals with when building value-flow
graphs.

To provide insight into the nature of constraints explosion, in Fig. 10, we
report the number of constraints Falcon deals with. Even when unrolling all
loops, we can see that it is not unusual to have over $10^{7}$ constraints.

###  7.3.  Thin Slicing for Program Understanding

This study aims to give a measure for the precision of Falcon’s semi-path-
sensitive value-flow graphs (§ 4.3) with the thin slicing client. In the
experimental results, we exclude the time for building value-flow graphs.

To generate a realistic set of queries, we compare Falcon against Supa for
thin slicing, which is introduced by Sridharan et al. (2007) to facilitate
program understanding and debugging. The thin slice for a given pair of
program variable and statement, a.k.a., the slicing seed, includes only the
_producer statements_ that directly affect the values of the variable. In
contrast to conventional slicing, control dependence and the data dependence
of the variable’s base pointer are excluded. Hence, thin slices are typically
much smaller than conventional program slices.

We generate the queries from the bug reports issued by a third-party typestate
analysis, which only flags the buggy variables and program locations, but not
the trace under which the bugs may occur. Thus, the thin slices can assist the
developers in understanding the bug reports. Our results show that Falcon is
scalable for the thin slicing client, taking under 240 milliseconds for each
demand query. In summary, it achieves up to 302$\times$ speedups than Supa and
54$\times$ on average. Fig. 11 compares the precision of Falcon against Sfs,
Dsa, and Supa on the 13 programs that get analyzed by all tools. The data for
each program are normalized to the results of Svf, i.e, a higher bar
corresponds to a more precise analysis. Briefly, we make the following
observations:

  * •

The precision of Falcon is superior than other analyses. The average size of
slices produced by Falcon is 5.5$\times$, 1.9$\times$, 2.6$\times$, and
1.3$\times$ smaller than that of Svf, Sfs, Dsa, and Supa, respectively.

  * •

Comparing Sfs and Svf, we see that flow sensitivity can substantially improve
the precision of Andersen’s analysis in some programs, such as php and ffmpeg.

  * •

Dsa is comparable to Svf in some cases, and much more precise than Svf in many
programs (e.g., vim, libicu, ffmpeg). The combination of context-sensitivity
and unification may bring better precision than the flow- and context-
insensitive Andersen’s analysis.

Figure 11.  Improvement in average slice size compared with the baseline Svf.

#### Remarks

First, Falcon offers a clearly visible improved precision of pointer
information. An important reason is that Falcon’s semi-path-sensitive analysis
(§ 4.3) can prune away more spurious value flows, compared with the demand-
driven flow- and context-sensitive analysis offered by Supa.

Second, the performance improvement is because that the value-flow graphs of
Falcon are more compact than that of Supa. On the one hand, Supa constructs
the graphs with a flow-insensitive analysis, whereas Falcon uses a flow-
sensitive one. On the other hand, Supa has to explicate a memory object on en
edge so that it can answer demand queries, where many edges are redundant.

Third, we observe that Falcon’s unsound assumption that function parameters
are alias-free does not affect the soundness for more than $90\%$ of the
queries, validated by manually checking the results. Similar to our
observations, two recent studies (Sui et al., 2014; Gharat et al., 2016) also
show that the function parameters of real-world C/C++ programs tend to have
few aliasing relations.

###  7.4. Value Flow Analysis for Bug Hunting

In this study, we investigate the efficiency and effectiveness of Falcon for
double-free detection, by comparing it against Cred (Yan et al., 2018). Both
Falcon and Cred employ the Z3 SMT solver (De Moura and Bjørner, 2008) to
achieve full path-sensitivity. Each tool is run in a single-thread mode and
the cutoff time per program is 24 hours.

Table 2. Results of double-free detection.

Program | Cred | Falcon
---|---|---
Time(m) | Mem(G) | #FP/#Rep | Time(m) | Mem(G) | #FP/#Rep
crafty | 0.2 | 0.5 | 0/0 | 0.3 | 0.5 | 0/0
eon | 1.3 | 1.1 | 0/0 | 0.9 | 1.7 | 0/0
gap | 0.7 | 3.2 | 0/0 | 0.6 | 1.3 | 0/0
vortex | 0.4 | 1.4 | 1/1 | 0.5 | 4.3 | 0/0
perlbmk | 5.2 | 4.4 | 0/0 | 3.4 | 4.8 | 0/0
gcc | 16.1 | 5.7 | 2/2 | 9.4 | 1.3 | 0/0
git | 155 | 23 | 1/1 | 23 | 20 | 1/3
vim | 1100 | 63 | 0/0 | 112 | 27 | 0/0
wrk | 93 | 19 | 0/0 | 17 | 24 | 0/0
libicu | 824 | 78 | 0/0 | 79 | 28 | 0/2
php | 1310 | 84 | 5/11 | 26 | 51 | 2/9
ffmpeg | 56 | 61 | 2/7 | 21 | 54 | 2/8
ppsspp | 44 | 33 | 0/1 | 23 | 17 | 1/3
mysql | OOT | - | - | 178 | 74 | 1/3
rethinkdb | OOT | - | - | 274 | 108 | 0/0
firefox | OOT | - | - | 310 | 143 | 0/0
%FP | 47.8% (11/23) | 25% (7/28)
OOT means the tool runs out of the time budget (24 hours).

Tbl. 2 presents the time and memory overhead of the tools. As can be seen,
Falcon surpass the performance of Cred for most large-scale programs,
achieving up to 50$\times$ speedups, and 6$\times$ speedups on average.
Besides, on average, Falcon takes 2$\times$ less of memory than Cred. Although
not shown in the table, we remark that, if allowing the concurrent analysis of
10 threads, Falcon can finish the checking of each program within 45 minutes.
Tbl. 2 also shows the number of reported warnings (#Rep) as well as the number
and the rate of false positives (#FP and %FP). We can see that Falcon detects
more real vulnerabilities than Cred (21 vs. 12). The false-positive rates of
Falcon and Cred are 25% and 56.5%, respectively. Falcon is aligned with the
common industrial requirement of 30% false positives (Bessey et al., 2010;
McPeak et al., 2013).

Overall, our findings conclude that the ideas behind Falcon have considerably
practical value. In terms of all aspects, including not only the scaling
efforts but also the precision and recall, the tool itself is promising in
providing an industrial-strength capability of static bug hunting.

##  8\. Related Work

####  Path-Sensitive Analysis

Tbl. 3 gives key properties of several existing path-sensitive algorithms.
Here we summarize some of the approaches taken by previous analyses. with a
focus on pointer reasoning.

Table 3. A comparison of key properties of existing analyses. The “Inter-PS”
column represent interprocedurally path-sensitive. The “PS-Heap” and ‘Sparse”
columns respectively indicate whether the analysis uses path-sensitive heap
abstraction and is sparse. Finally, the “Shown to Scale” column indicates
whether the algorithm has been shown to scale to large programs with multi-
million lines of code.

Algorithm | Inter-PS | PS-Heap | Sparse |  | Shown to Scale
---
Das et al. (2002) | X |  |  | X
Ball and Rajamani (2002) | X |  |  |
Livshits and Lam (2003) | X | X |  |
Hackett and Aiken (2006) |  | X |  | X
Babic and Hu (2008) | X |  |  | X
Chandra et al. (2009) | X | X |  |
Dillig et al. (2011) | X | X |  |
Sui et al. (2011) |  | X | X | X
Blackshear et al. (2013) | X | X |  |
Li et al. (2017) | X | X |  |
Yan et al. (2018) | X | X | X |
Kim et al. (2019) | X | X |  |
Current paper | X | X | X | X

Livshits and Lam (2003) introduce a flow-, path-, and context-sensitive
pointer analysis, which only scales to programs up to 13KLoC. The pointer
analyses in (Hackett and Aiken, 2006) and (Sui et al., 2011) are only
intraprocedurally path-sensitive. Dillig et al. (2010, 2011) present a path-
and context-sensitive heap analysis that scales to program with 128KLoC.
Blackshear et al. (2013) introduce a symbolic-explicit representation that
incorporates the pre-computed flow-insensitive points-to facts to guide the
backward symbolic execution. Similar to the index variables in (Dillig et al.,
2010, 2011) and symbolic variables in (Blackshear et al., 2013), we use the
guards qualifying value-flow graph edges to enable lazy case splitting over
the points-to set. However, their approaches are either not demand-driven or
non-sparse and, thus, do not scale well for large-scale programs.

Our work follows a long line of research on path-sensitive dataflow analysis.
Esp (Das et al., 2002) encodes a typestate property into a finite state
automata, which is used as criteria for partitioning and merging program
paths. Essentially, Esp is similar to many other approaches such as _trace
partition_ (Mauborgne and Rival, 2005) and _elaborations_ (Sankaranarayanan et
al., 2006) that control the trade-off between performing joining operations or
logical disjunctions at control flow merge points. By contrast, Falcon uses
logical disjunction to precisely merge value-flow guard.

Counterexample-guided abstraction refinement starts with an imprecise
abstraction, which is iteratively and gradually refined (Clarke et al., 2003;
Ball and Rajamani, 2002). Our approach has a “refinement” flavor, but we
compute the path- and context-sensitive conditions directly in the on-demand
analysis phase, without using a refinement loop. Conceptually, our approach
bears similarities to the staged analyses for typestate verification (Fink et
al., 2006, 2008), but we focus on path-sensitive analysis and We decompose the
cost into semi-path-sensitive value-flow graphs construction and a full-path-
sensitive alias resolution over the graphs.

Shape analysis (Sagiv et al., 2002) proves data-structure invariants and has
had a major impact on the verification community. Precise shape analyses
(Sagiv et al., 2002; Li et al., 2017) that are capable of path-sensitive heap
reasoning do not readily scale to large programs (Fink et al., 2008). There
have been scalable solutions such as compositional shape analysis based on bi-
abduction (Calcagno et al., 2011; Gulavani et al., 2009), yet they do not
guarantee precision.

#### Demand-Driven Pointer Analysis

Demand-driven program analyses only analyze parts of the program that are
relevant for answering a given query. To date, most existing demand-driven
pointer analyses for C/C++ (Heintze and Tardieu, 2001; Saha and Ramakrishnan,
2005; Zheng and Rugina, 2008) and Java (Sridharan et al., 2005; Sridharan and
Bodík, 2006; Yan et al., 2011; Shang et al., 2012; Lu et al., 2013; Su et al.,
2014; Feng et al., 2015) are flow-insensitive. Their underlying data
structures, such as the pointer expression graph (Zheng and Rugina, 2008),
entirely or partially lose the control flow information and, thus, are not
easy to be extended for path-sensitivity. Recently, there has been a
resurgence of interest in demand-driven flow- or path-sensitive pointer
analysis (Späth et al., 2016; Sui and Xue, 2016a; Späth et al., 2019; Yan et
al., 2018). Some of these approaches are not sparse (Späth et al., 2016; Späth
et al., 2019). Some of them are sparse but suffer from the aliasing-path-
explosion issues that we address in this paper (Sui and Xue, 2016a; Yan et
al., 2018).

There is an increasing interest in _parametric pointer analyses_ (Kastrinis
and Smaragdakis, 2013; Smaragdakis et al., 2014; Wei and Ryder, 2015; Jeong et
al., 2017; Jeon et al., 2018; Hassanshahi et al., 2017; Li et al., 2018b, a)
that resemble demand-driven approaches. By contrast, they are not query-
driven, but schedule analysis strategies such as selective context-sensitivity
for different parts of the program. (functions, allocation sites)
_Introspective analysis_ (Smaragdakis et al., 2014) tunes context sensitivity
per-function based on a pre-analysis that computes heuristics such as “total
points-to information”. Jeong et al. (2017) present a data-driven approach to
guiding selective context-sensitive analysis, which assigns each function a
context length based on a set of program features. Most of the recent advances
focus on context-sensitive analysis. Our approach uses a flow-insensitive
analysis for function pointers, and precise path- and context-sensitive
analysis for other pointers of interest.

#### Data-Dependence Analysis

Data-dependence analysis aims to identify the def-use information in a
program. It has many applications such as change-impact analysis (Arnold,
1996; Orso et al., 2004; Acharya and Robinson, 2011), program slicing
(Sridharan et al., 2007; Li et al., 2016) and bug hunting (Tripp et al., 2009,
2013; Arzt et al., 2014).

There is a huge amount of literature on context-sensitive data-dependence
analysis via context-free language (CFL) reachability (Späth et al., 2019;
Horwitz et al., 1990; Chatterjee et al., 2017; Reps, 1998; Sridharan and
Bodík, 2006), or other language reachability problems (Tang et al., 2015;
Zhang and Su, 2017). Tang et al. (2015) propose a TAL-reachability formulation
that improves the scalability of on constructing function summaries of library
code. Zhang and Su (2017) introduce linear conjunctive language (LCL)
reachability for approximating the interleaved matching-parentheses problem of
filed- and context-sensitive data-dependence analysis. Späth et al. (2019)
present a context- and flow-sensitive data-flow analysis based on synchronized
pushdown systems. P/taint (Grech and Smaragdakis, 2017) unifies points-to and
taint analysis by extending the Datalog rules of the underlying points-to
analysis and then computing the information all together. All of these
techniques are path-insensitive.

The array dependence analysis (Maydan et al., 1991) community has developed
several path-sensitive approaches that are based on SMT solving (Mohammadi et
al., 2018), quantifier elimination (Mohammadi et al., 2019), among others
(Pothen and Toledo, 2004). Typically, these approaches focus on array
manipulating programs and do not scale to large-scale software with
complicated pointer operations.

#### Sparse Pointer Analysis

The idea of sparse analysis starts from the static single assignment (SSA)
form where def-use chains are explicitly encoded (Cytron et al., 1989; Choi et
al., 1991; Chow et al., 1996). Such def-use chains allow the propagation of
data-flow facts to skip unnecessary control flows. Hardekopf and Lin (2009)
present an inclusion-based and semi-sparse flow-sensitive pointer analysis by
leveraging the partial SSA form in LLVM (Lattner and Adve, 2004). It is semi-
sparse because it only utilizes the def-use chains of the top-level pointers.

To be fully sparse, the def-use information of other address-taken variables
is needed. There are two classes of full-sparse analysis. First, the staged
approaches (Hardekopf and Lin, 2011; Sui et al., 2016; Sui and Xue, 2016a; Yan
et al., 2018) exploit a lightweight and imprecise pre-computed pointer
analysis to approximate the def-use relations. Owing to the imprecision,
spurious value flows will be introduced and harm the performance. Second, the
on-the-fly approaches (Chase et al., 1990; Yu et al., 2010; Sui et al., 2011;
Li et al., 2011) construct the def-use chains alongside the pointer analysis.
However, their approaches are exhaustive and, thus, do not scale well when
path-sensitivity is required. Specifically, Spas (Sui et al., 2011) is the
only previous pointer analysis that is both path-sensitive and on-the-fly
sparse, but they achieve incremental sparsity by extending the level-by-level
analysis (Yu et al., 2010), which must be exhaustive because (1) a single
level can consist of pointers from the whole program, and (2) pointers with
higher levels strictly depend on the analysis results of pointers with lower
levels.

##  9\. Conclusion

We have presented Falcon, our approach to path-sensitive data-dependence
analysis. At its heart stands an analysis that concisely constructs the
guarded and compositional value-flow graphs, which allow tracking path- and
context-sensitive def-use information on demand. The graceful scalability and
high precision of Falcon rest on our solution to the aliasing-path-explosion
problem. Specifically, Falcon is sparse, demand-driven, and can prune and
simplify path constraints at an early stage of the analysis. Our work presents
strong evidence that path-sensitive data-dependence analysis is a reasonable
choice for millions of lines of code.

## References

  * (1)
  * Acharya and Robinson (2011) Mithun Acharya and Brian Robinson. 2011.  Practical change impact analysis based on static program slicing for industrial software systems. In _Proceedings of the 33rd International Conference on Software Engineering_ (Waikiki, Honolulu, HI, USA) _(ICSE ’11)_. 746–755.
  * Arnold (1996) Robert S Arnold. 1996\.  Software Change Impact Analysis.  (1996).
  * Arzt et al. (2014) Steven Arzt, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick McDaniel. 2014.  Flowdroid: Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps. In _Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Edinburgh, United Kingdom) _(PLDI ’14)_. 259–269.
  * Babic and Hu (2008) Domagoj Babic and Alan J Hu. 2008.  Calysto: scalable and precise extended static checking. In _Proceedings of the 30th International Conference on Software Engineering_ (Leipzig, Germany) _(ICSE ’08)_. 211–220.
  * Ball and Rajamani (2002) Thomas Ball and Sriram K Rajamani. 2002.  The SLAM project: debugging system software via static analysis. In _Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Portland, Oregon) _(POPL ’02)_. 1–3.
  * Bessey et al. (2010) Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, and Dawson Engler. 2010\.  A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World.  _Commun. ACM_ 53, 2 (Feb. 2010), 66–75.
  * Blackshear et al. (2013) Sam Blackshear, Bor-Yuh Evan Chang, and Manu Sridharan. 2013.  Thresher: Precise refutations for heap reachability. In _Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Seattle, Washington, USA) _(PLDI ’13)_. 275–286.
  * Cadar et al. (2008) Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008\.  KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs.. In _Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation_ (San Diego, California) _(OSDI’08)_. 209–224.
  * Calcagno et al. (2011) Cristiano Calcagno, Dino Distefano, Peter W O’hearn, and Hongseok Yang. 2011.  Compositional shape analysis by means of bi-abduction.  _J. ACM_ 58, 6, Article 26 (Dec. 2011), 66 pages.
  * Chandra et al. (2009) Satish Chandra, Stephen J. Fink, and Manu Sridharan. 2009\.  Snugglebug: A Powerful Approach to Weakest Preconditions. In _Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Dublin, Ireland) _(PLDI ’09)_. 363–374.
  * Chase et al. (1990) David R Chase, Mark Wegman, and F Kenneth Zadeck. 1990\.  Analysis of pointers and structures. In _Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation_ (White Plains, New York, USA) _(PLDI ’90)_. 296–310.
  * Chatterjee et al. (2017) Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis. 2017.  Optimal Dyck Reachability for Data-dependence and Alias Analysis.  _Proc. ACM Program. Lang._ 2, POPL, Article 30 (Dec. 2017), 30 pages.
  * Cherem et al. (2007) Sigmund Cherem, Lonnie Princehouse, and Radu Rugina. 2007\.  Practical memory leak detection using guarded value-flow analysis. In _Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (San Diego, California, USA) _(PLDI ’07)_.
  * Choi et al. (1991) Jong-Deok Choi, Ron Cytron, and Jeanne Ferrante. 1991\.  Automatic construction of sparse data flow evaluation graphs. In _Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Orlando, Florida, USA) _(POPL ’91)_. 55–66.
  * Chow et al. (1996) Fred Chow, Sun Chan, Shin-Ming Liu, Raymond Lo, and Mark Streich. 1996.  Effective representation of aliases and indirect memory operations in SSA form. In _Proceedings of the 6th International Conference on Compiler Construction_ _(CC ’96)_. 253–267.
  * Clarke et al. (2003) Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2003.  Counterexample-guided Abstraction Refinement for Symbolic Model Checking.  _J. ACM_ 50, 5 (Sept. 2003), 752–794.
  * Cousot and Cousot (1979) Patrick Cousot and Radhia Cousot. 1979.  Systematic Design of Program Analysis Frameworks. In _Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages_ (San Antonio, Texas) _(POPL ’79)_. 269–282.
  * Cytron et al. (1989) Ron Cytron, Jeanne Ferrante, Barry K Rosen, Mark N Wegman, and F Kenneth Zadeck. 1989.  An efficient method of computing static single assignment form. In _Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Austin, Texas, USA) _(POPL ’89)_. 25–35.
  * Cytron et al. (1991) Ron Cytron, Jeanne Ferrante, Barry K Rosen, Mark N Wegman, and F Kenneth Zadeck. 1991.  Efficiently computing static single assignment form and the control dependence graph.  _ACM Trans. Program. Lang. Syst._ 13, 4 (Oct. 1991), 451–490.
  * Das et al. (2002) Manuvir Das, Sorin Lerner, and Mark Seigle. 2002\.  ESP: Path-sensitive Program Verification in Polynomial Time. In _Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation_ (Berlin, Germany) _(PLDI ’02)_. 57–68.
  * De Moura and Bjørner (2008) Leonardo De Moura and Nikolaj Bjørner. 2008.  Z3: An efficient SMT solver. In _Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems_ (Budapest, Hungary) _(TACAS’08/ETAPS’08)_. 337–340.
  * Dean et al. (1995) Jeffrey Dean, David Grove, and Craig Chambers. 1995\.  Optimization of object-oriented programs using static class hierarchy analysis. In _European Conference on Object-Oriented Programming_. Springer, 77–101.
  * Dillig et al. (2010) Isil Dillig, Thomas Dillig, and Alex Aiken. 2010\.  Fluid Updates: Beyond Strong vs. Weak Updates. In _Proceedings of the 19th European Conference on Programming Languages and Systems_ (Paphos, Cyprus) _(ESOP’10)_. 246–266.
  * Dillig et al. (2011) Isil Dillig, Thomas Dillig, Alex Aiken, and Mooly Sagiv. 2011\.  Precise and compact modular procedure summaries for heap manipulating programs. In _Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation_ (San Jose, California, USA) _(PLDI ’11)_. 567–577.
  * Emami et al. (1994) Maryam Emami, Rakesh Ghiya, and Laurie J Hendren. 1994\.  Context-sensitive interprocedural points-to analysis in the presence of function pointers. In _Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation_ (Orlando, Florida, USA) _(PLDI ’94)_. 242–256.
  * Feng et al. (2015) Yu Feng, Xinyu Wang, Isil Dillig, and Calvin Lin. 2015\.  EXPLORER: query-and demand-driven exploration of interprocedural control flow properties. In _Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications_ (Pittsburgh, PA, USA) _(OOPSLA 2015)_. 520–534.
  * Fink et al. (2006) Stephen Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay. 2006.  Effective Typestate Verification in the Presence of Aliasing. In _Proceedings of the 2006 International Symposium on Software Testing and Analysis_ (Portland, Maine, USA) _(ISSTA ’06)_. 133–144.
  * Fink et al. (2008) Stephen J Fink, Eran Yahav, Nurit Dor, G Ramalingam, and Emmanuel Geay. 2008.  Effective typestate verification in the presence of aliasing.  _ACM Trans. Softw. Eng. Methodol._ 17, 2, Article 9 (May 2008), 34 pages.
  * Gharat et al. (2016) Pritam M Gharat, Uday P Khedker, and Alan Mycroft. 2016\.  Flow- and context-sensitive points-to analysis using generalized points-to graphs. In _International Static Analysis Symposium_ _(SAS ’16)_. Springer, 212–236.
  * Grech and Smaragdakis (2017) Neville Grech and Yannis Smaragdakis. 2017.  P/Taint: Unified Points-to and Taint Analysis.  _Proc. ACM Program. Lang._ 1, OOPSLA, Article 102 (Oct. 2017), 28 pages.
  * Grove and Chambers (2001) David Grove and Craig Chambers. 2001.  A framework for call graph construction algorithms.  _ACM Trans. Program. Lang. Syst._ 23, 6 (Nov. 2001), 685–746.
  * Gulavani et al. (2009) Bhargav S Gulavani, Supratik Chakraborty, Ganesan Ramalingam, and Aditya V Nori. 2009.  Bottom-up shape analysis. In _International Static Analysis Symposium_ _(SAS ’09)_. Springer, 188–204.
  * Guyer and Lin (2005) Samuel Z Guyer and Calvin Lin. 2005.  Error checking with client-driven pointer analysis.  _Sci. Comput. Program._ 58, 1-2 (Oct. 2005), 83–114.
  * Hackett and Aiken (2006) Brian Hackett and Alex Aiken. 2006.  How is aliasing used in systems software?. In _Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering_ (Portland, Oregon, USA) _(SIGSOFT ’06/FSE-14)_. 69–80.
  * Hardekopf and Lin (2009) Ben Hardekopf and Calvin Lin. 2009.  Semi-sparse flow-sensitive pointer analysis. In _Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Savannah, GA, USA) _(POPL ’09)_. ACM, New York, NY, USA, 226–238.
  * Hardekopf and Lin (2011) Ben Hardekopf and Calvin Lin. 2011.  Flow-sensitive pointer analysis for millions of lines of code. In _Proceedings of the 9th Annual IEEE/ACM International Symposium on Code Generation and Optimization_ _(CGO ’11)_. IEEE Computer Society, Washington, DC, USA, 289–298.
  * Hassanshahi et al. (2017) Behnaz Hassanshahi, Raghavendra Kagalavadi Ramesh, Padmanabhan Krishnan, Bernhard Scholz, and Yi Lu. 2017\.  An efficient tunable selective points-to analysis for large codebases. In _Proceedings of the 6th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis_ (Barcelona, Spain) _(SOAP 2017)_. 13–18.
  * Heintze and Tardieu (2001) Nevin Heintze and Olivier Tardieu. 2001.  Demand-driven pointer analysis. In _Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation_ (Snowbird, Utah, USA) _(PLDI ’01)_. 24–34.
  * Horwitz et al. (1990) Susan Horwitz, Thomas Reps, and David Binkley. 1990\.  Interprocedural slicing using dependence graphs.  _ACM Trans. Program. Lang. Syst._ 12, 1 (Jan. 1990), 26–60.
  * Jeon et al. (2018) Minseok Jeon, Sehun Jeong, and Hakjoo Oh. 2018.  Precise and scalable points-to analysis via data-driven context tunneling.  _Proc. ACM Program. Lang._ 2, OOPSLA, Article 140 (Oct. 2018), 29 pages.
  * Jeong et al. (2017) Sehun Jeong, Minseok Jeon, Sungdeok Cha, and Hakjoo Oh. 2017\.  Data-driven context-sensitivity for points-to analysis.  _Proc. ACM Program. Lang._ 1, OOPSLA, Article 100 (Oct. 2017), 28 pages.
  * Kahlon (2008) Vineet Kahlon. 2008\.  Bootstrapping: a technique for scalable flow and context-sensitive pointer alias analysis. In _Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Tucson, AZ, USA) _(PLDI ’08)_. 249–259.
  * Kanvar and Khedker (2016) Vini Kanvar and Uday P Khedker. 2016.  Heap abstractions for static analysis.  _ACM Comput. Surv._ 49, 2, Article 29 (June 2016), 47 pages.
  * Kastrinis and Smaragdakis (2013) George Kastrinis and Yannis Smaragdakis. 2013.  Hybrid context-sensitivity for points-to analysis. In _Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Seattle, Washington, USA) _(PLDI ’13)_. 423–434.
  * Kim et al. (2019) Yunho Kim, Shin Hong, and Moonzoo Kim. 2019.  Target-driven Compositional Concolic Testing with Function Summary Refinement for Effective Bug Detection. In _Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering_ (Tallinn, Estonia) _(ESEC/FSE 2019)_. 16–26.
  * Lattner and Adve (2004) Chris Lattner and Vikram Adve. 2004.  LLVM: A compilation framework for lifelong program analysis & transformation. In _Proceedings of the International Symposium on Code Generation and Optimization: Feedback-directed and Runtime Optimization_ (Palo Alto, California) _(CGO ’04)_. 75–.
  * Lattner et al. (2007) Chris Lattner, Andrew Lenharth, and Vikram Adve. 2007\.  Making context-sensitive points-to analysis with heap cloning practical for the real world. In _Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (San Diego, California, USA) _(PLDI ’07)_. 278–289.
  * Lhoták and Chung (2011) Ondrej Lhoták and Kwok-Chiang Andrew Chung. 2011.  Points-to analysis with efficient strong updates. In _Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Austin, Texas, USA) _(POPL ’11)_. 3–16.
  * Lhoták and Hendren (2008) Ondřej Lhoták and Laurie Hendren. 2008.  Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation.  _ACM Trans. Softw. Eng. Methodol._ 18, 1, Article 3 (Oct. 2008), 53 pages.
  * Li et al. (2017) Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, and Xavier Rival. 2017.  Semantic-directed clumping of disjunctive abstract states. In _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages_ (Paris, France) _(POPL 2017)_. 32–45.
  * Li et al. (2011) Lian Li, Cristina Cifuentes, and Nathan Keynes. 2011\.  Boosting the performance of flow-sensitive points-to analysis using value flow. In _Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering_ (Szeged, Hungary) _(ESEC/FSE ’11)_. 343–353.
  * Li et al. (2013) Lian Li, Cristina Cifuentes, and Nathan Keynes. 2013\.  Precise and scalable context-sensitive pointer analysis via value flow graph. In _Proceedings of the 2013 International Symposium on Memory Management_ (Seattle, Washington, USA) _(ISMM ’13)_. 85–96.
  * Li et al. (2018a) Yue Li, Tian Tan, Anders Moller, and Yannis Smaragdakis. 2018a.  Precision-guided context sensitivity for pointer analysis.  _Proc. ACM Program. Lang._ 2, OOPSLA, Article 141 (Oct. 2018), 29 pages.
  * Li et al. (2018b) Yue Li, Tian Tan, Anders Moller, and Yannis Smaragdakis. 2018b.  Scalability-First Pointer Analysis with Self-Tuning Context-Sensitivity. In _Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering_ (Lake Buena Vista, FL, USA) _(ESEC/FSE 2018)_. 129–140.
  * Li et al. (2016) Yue Li, Tian Tan, Yifei Zhang, and Jingling Xue. 2016\.  Program tailoring: Slicing by sequential criteria. In _30th European Conference on Object-Oriented Programming (ECOOP 2016)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 56)_ , Shriram Krishnamurthi and Benjamin S. Lerner (Eds.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 15:1–15:27.
  * Livshits et al. (2015) Benjamin Livshits, Manu Sridharan, Yannis Smaragdakis, Ondřej Lhoták, J Nelson Amaral, Bor-Yuh Evan Chang, Samuel Z Guyer, Uday P Khedker, Anders Møller, and Dimitrios Vardoulakis. 2015.  In defense of soundiness: a manifesto.  _Commun. ACM_ 58, 2 (Jan. 2015), 44–46.
  * Livshits and Lam (2003) V Benjamin Livshits and Monica S Lam. 2003.  Tracking pointers with path and context sensitivity for bug detection in C programs. In _Proceedings of the 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering_ (Helsinki, Finland) _(ESEC/FSE-11)_. 317–326.
  * Lu et al. (2013) Yi Lu, Lei Shang, Xinwei Xie, and Jingling Xue. 2013\.  An incremental points-to analysis with CFL-reachability. In _Proceedings of the 22Nd International Conference on Compiler Construction_ (Rome, Italy) _(CC’13)_. 61–81.
  * Manevich et al. (2004) Roman Manevich, Manu Sridharan, Stephen Adams, Manuvir Das, and Zhe Yang. 2004.  PSE: explaining program failures via postmortem static analysis. In _Proceedings of the 12th ACM SIGSOFT Twelfth International Symposium on Foundations of Software Engineering_ (Newport Beach, CA, USA) _(SIGSOFT ’04/FSE-12)_. 63–72.
  * Mauborgne and Rival (2005) Laurent Mauborgne and Xavier Rival. 2005.  Trace partitioning in abstract interpretation based static analyzers. In _Proceedings of the 14th European Conference on Programming Languages and Systems_ (Edinburgh, UK) _(ESOP’05)_. 5–20.
  * Maydan et al. (1991) Dror E Maydan, John L Hennessy, and Monica S Lam. 1991\.  Efficient and exact data dependence analysis. In _Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation_ (Toronto, Ontario, Canada) _(PLDI ’91)_. 1–14.
  * McPeak et al. (2013) Scott McPeak, Charles-Henri Gros, and Murali Krishna Ramanathan. 2013.  Scalable and Incremental Software Bug Detection. In _Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering_ (Saint Petersburg, Russia) _(ESEC/FSE 2013)_. 554–564.
  * Milanova et al. (2004) Ana Milanova, Atanas Rountev, and Barbara G Ryder. 2004\.  Precise call graphs for C programs with function pointers.  _Automated Software Engg._ 11, 1 (Jan. 2004), 7–26.
  * Mohammadi et al. (2018) Mahdi Soltan Mohammadi, Kazem Cheshmi, Maryam Mehri Dehnavi, Anand Venkat, Tomofumi Yuki, and Michelle Mills Strout. 2018.  Extending Index-Array Properties for Data Dependence Analysis _(LCPC ’14)_.
  * Mohammadi et al. (2019) Mahdi Soltan Mohammadi, Tomofumi Yuki, Kazem Cheshmi, Eddie C. Davis, Mary Hall, Maryam Mehri Dehnavi, Payal Nandy, Catherine Olschanowsky, Anand Venkat, and Michelle Mills Strout. 2019\.  Sparse Computation Data Dependence Simplification for Efficient Compiler-generated Inspectors. In _Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Phoenix, AZ, USA) _(PLDI 2019)_. 594–609.
  * Nieuwenhuis et al. (2006) Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. 2006\.  Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T).  _J. ACM_ 53, 6 (Nov. 2006), 937–977.
  * Orso et al. (2004) Alessandro Orso, Taweesup Apiwattanapong, James Law, Gregg Rothermel, and Mary Jean Harrold. 2004\.  An Empirical Comparison of Dynamic Impact Analysis Algorithms. In _Proceedings of the 26th International Conference on Software Engineering_ _(ICSE ’04)_. 491–500.
  * Ottenstein et al. (1990) Karl J Ottenstein, Robert A Ballance, and Arthur B MacCabe. 1990.  The program dependence web: a representation supporting control-, data-, and demand-driven interpretation of imperative languages. In _Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation_ (White Plains, New York, USA) _(PLDI ’90)_. 257–271.
  * Pothen and Toledo (2004) Alex Pothen and Sivan Toledo. 2004.  Elimination Structures in Scientific Computing.
  * Reps (1998) Thomas Reps. 1998\.  Program analysis via graph reachability.  _Information and software technology_ 40, 11 (1998), 701–726.
  * Sagiv et al. (2002) Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. 2002.  Parametric shape analysis via 3-valued logic.  _ACM Trans. Program. Lang. Syst._ 24, 3 (May 2002), 217–298.
  * Saha and Ramakrishnan (2005) Diptikalyan Saha and CR Ramakrishnan. 2005.  Incremental and demand-driven points-to analysis using logic programming. In _Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming_ (Lisbon, Portugal) _(PPDP ’05)_. 117–128.
  * Sankaranarayanan et al. (2006) Sriram Sankaranarayanan, Franjo Ivančić, Ilya Shlyakhter, and Aarti Gupta. 2006\.  Static analysis in disjunctive numerical domains. In _Proceedings of the 13th International Conference on Static Analysis_ (Seoul, Korea) _(SAS’06)_. 3–17.
  * Shang et al. (2012) Lei Shang, Xinwei Xie, and Jingling Xue. 2012.  On-demand dynamic summary-based points-to analysis. In _Proceedings of the Tenth International Symposium on Code Generation and Optimization_ (San Jose, California) _(CGO ’12)_. 264–274.
  * Shi et al. (2018) Qingkai Shi, Xiao Xiao, Rongxin Wu, Jinguo Zhou, Gang Fan, and Charles Zhang. 2018\.  Pinpoint: fast and precise sparse value flow analysis for million lines of code. In _Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Philadelphia, PA, USA) _(PLDI 2018)_. 693–706.
  * Smaragdakis et al. (2014) Yannis Smaragdakis, George Kastrinis, and George Balatsouras. 2014\.  Introspective analysis: context-sensitivity, across the board. In _Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Edinburgh, United Kingdom) _(PLDI ’14)_. 485–495.
  * Späth et al. (2019) Johannes Späth, Karim Ali, and Eric Bodden. 2019.  Context-, flow-, and field-sensitive data-flow analysis using synchronized Pushdown systems.  _Proc. ACM Program. Lang._ 3, POPL, Article 48 (Jan. 2019), 29 pages.
  * 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 _LIPIcs-Leibniz International Proceedings in Informatics_ , Vol. 56. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
  * Sridharan and Bodík (2006) Manu Sridharan and Rastislav Bodík. 2006.  Refinement-based context-sensitive points-to analysis for Java. In _Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Ottawa, Ontario, Canada) _(PLDI ’06)_. 387–400.
  * Sridharan et al. (2007) Manu Sridharan, Stephen J Fink, and Rastislav Bodik. 2007\.  Thin slicing. In _Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (San Diego, California, USA) _(PLDI ’07)_. 112–122.
  * Sridharan et al. (2005) Manu Sridharan, Denis Gopan, Lexin Shan, and Rastislav Bodík. 2005.  Demand-driven points-to analysis for Java. In _Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications_ (San Diego, CA, USA) _(OOPSLA ’05)_. 59–76.
  * Su et al. (2014) Yu Su, Ding Ye, and Jingling Xue. 2014.  Parallel Pointer Analysis with CFL-Reachability. In _Proceedings of the 2014 Brazilian Conference on Intelligent Systems_ _(BRACIS ’14)_. 451–460.
  * Sui et al. (2016) Yulei Sui, Peng Di, and Jingling Xue. 2016.  Sparse flow-sensitive pointer analysis for multithreaded programs. In _Proceedings of the 2016 International Symposium on Code Generation and Optimization_ (Barcelona, Spain) _(CGO ’16)_. 160–170.
  * Sui and Xue (2016a) Yulei Sui and Jingling Xue. 2016a.  On-demand strong update analysis via value-flow refinement. In _Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering_ (Seattle, WA, USA) _(FSE 2016)_. 460–473.
  * Sui and Xue (2016b) Yulei Sui and Jingling Xue. 2016b.  SVF: interprocedural static value-flow analysis in LLVM. In _Proceedings of the 25th International Conference on Compiler Construction_ (Barcelona, Spain) _(CC 2016)_. 265–266.
  * Sui and Xue (2018) Y. Sui and J. Xue. 2018\.  Value-Flow-Based Demand-Driven Pointer Analysis for C and C++.  _IEEE Transactions on Software Engineering_ (2018), 1–1.
  * Sui et al. (2012) Yulei Sui, Ding Ye, and Jingling Xue. 2012.  Static memory leak detection using full-sparse value-flow analysis. In _Proceedings of the 2012 International Symposium on Software Testing and Analysis_ (Minneapolis, MN, USA) _(ISSTA 2012)_. ACM, New York, NY, USA.
  * Sui et al. (2011) Yulei Sui, Sen Ye, Jingling Xue, and Pen-Chung Yew. 2011\.  SPAS: scalable path-sensitive pointer analysis on full-sparse SSA. In _Proceedings of the 9th Asian Conference on Programming Languages and Systems_ (Kenting, Taiwan) _(APLAS’11)_. 155–171.
  * Sui et al. (2014) Yulei Sui, Sen Ye, Jingling Xue, and Jie Zhang. 2014\.  Making context-sensitive inclusion-based pointer analysis practical for compilers using parameterised summarisation.  _Softw. Pract. Exper._ 44, 12 (Dec. 2014), 1485–1510.
  * Tang et al. (2015) Hao Tang, Xiaoyin Wang, Lingming Zhang, Bing Xie, Lu Zhang, and Hong Mei. 2015\.  Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks. In _Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Mumbai, India) _(POPL ’15)_. 83–95.
  * Tripp et al. (2013) Omer Tripp, Marco Pistoia, Patrick Cousot, Radhia Cousot, and Salvatore Guarnieri. 2013\.  Andromeda: Accurate and scalable security analysis of web applications. In _Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering_ (Rome, Italy) _(FASE’13)_. 210–225.
  * Tripp et al. (2009) Omer Tripp, Marco Pistoia, Stephen J Fink, Manu Sridharan, and Omri Weisman. 2009.  TAJ: effective taint analysis of web applications. In _Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Dublin, Ireland) _(PLDI ’09)_. 87–97.
  * Wei and Ryder (2015) Shiyi Wei and Barbara G Ryder. 2015.  Adaptive context-sensitive analysis for JavaScript. In _29th European Conference on Object-Oriented Programming (ECOOP 2015)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 37)_ , John Tang Boyland (Ed.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 712–734.
  * Xie and Aiken (2005) Yichen Xie and Alex Aiken. 2005.  Scalable error detection using boolean satisfiability. In _Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Long Beach, California, USA) _(POPL ’05)_. 351–363.
  * Yan et al. (2011) Dacong Yan, Guoqing Xu, and Atanas Rountev. 2011.  Demand-driven context-sensitive alias analysis for Java. In _Proceedings of the 2011 International Symposium on Software Testing and Analysis_ (Toronto, Ontario, Canada) _(ISSTA ’11)_. 155–165.
  * Yan et al. (2018) Hua Yan, Yulei Sui, Shiping Chen, and Jingling Xue. 2018\.  Spatio-temporal context reduction: a pointer-analysis-based static approach for detecting use-after-free vulnerabilities. In _Proceedings of the 40th International Conference on Software Engineering_ (Gothenburg, Sweden) _(ICSE ’18)_. 327–337.
  * Ye et al. (2014) Sen Ye, Yulei Sui, and Jingling Xue. 2014.  Region-based selective flow-sensitive pointer analysis. In _International Static Analysis Symposium_ _(SAS ’14)_. Springer, 319–336.
  * Yu et al. (2010) Hongtao Yu, Jingling Xue, Wei Huo, Xiaobing Feng, and Zhaoqing Zhang. 2010.  Level by level: making flow-and context-sensitive pointer analysis scalable for millions of lines of code. In _Proceedings of the 8th Annual IEEE/ACM International Symposium on Code Generation and Optimization_ (Toronto, Ontario, Canada) _(CGO ’10)_. 218–229.
  * Zhang and Stickely (1996) Hantao Zhang and Mark E Stickely. 1996.  An Efficient Algorithm for Unit Propagation.  _Proc. of AI-MATH_ 96 (1996).
  * Zhang et al. (2013) Qirun Zhang, Michael R Lyu, Hao Yuan, and Zhendong Su. 2013\.  Fast algorithms for Dyck-CFL-reachability with applications to alias analysis. In _Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Seattle, Washington, USA) _(PLDI ’13)_. 435–446.
  * Zhang and Su (2017) Qirun Zhang and Zhendong Su. 2017.  Context-sensitive Data-dependence Analysis via Linear Conjunctive Language Reachability. In _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages_ (Paris, France) _(POPL 2017)_. 344–358.
  * Zhao et al. (2018) Jisheng Zhao, Michael G Burke, and Vivek Sarkar. 2018\.  Parallel sparse flow-sensitive points-to analysis. In _Proceedings of the 27th International Conference on Compiler Construction_ (Vienna, Austria) _(CC 2018)_. 59–70.
  * Zheng and Rugina (2008) Xin Zheng and Radu Rugina. 2008.  Demand-driven alias analysis for C. In _Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (San Francisco, California, USA) _(POPL ’08)_. 197–208.