# Computing Maximum Fixed Point Solutions over Feasible Paths in Data Flow
Analyses

Komal Pathade<EMAIL_ADDRESS>TCS Research, India  Uday Khedker
<EMAIL_ADDRESS>Indian Institute of Technology Bombay, India

###### Abstract

The _control flow graph_ (CFG) representation of a procedure used by virtually
all flow-sensitive program analyses, admits a large number of _infeasible_
control flow paths i.e., these paths do not occur in any execution of the
program. Hence the information reaching along infeasible paths in an analysis
is spurious. This affects the precision of the conventional _maximum fixed
point_ (MFP) solution of the data flow analysis, because it includes the
information reaching along all control flow paths. The existing approaches for
removing this imprecision are either specific to a data flow problem with no
straightforward generalization or involve control flow graph restructuring
which may exponentially blow up the size of the CFG.

We lift the notion of MFP solution to define the notion of _feasible path MFP_
(FPMFP) solutions that exclude the data flowing along known infeasible paths.
The notion of FPMFP is generic and does not involve CFG restructuring.
Instead, it takes externally supplied information about infeasible paths and
lifts any data flow analysis to an analysis that maintains the distinctions
between different paths where these distinctions are beneficial, and ignores
them where they are not. Thus it gets the benefit of a path-sensitive analysis
where it is useful without performing a conventional path-sensitive analysis.
Hence, an FPMFP solution is more precise than the corresponding MFP solution
in most cases; it is guaranteed to be sound in each case.

We implemented the proposed computation of feasible path MFP solutions for
reaching definitions analysis and potentially uninitialized variable analysis.
We evaluated the precision improvement in these two analyses by analyzing 30
benchmark applications selected from open source, industry, and SPEC CPU 2006.
The evaluation results indicate that the precision improvement in these two
analyses respectively reduce the number def-use pairs by up to 13.6% (average
2.87%, geometric mean 1.75%), and reduce the potentially uninitialized
variable alarms by up to 100% (average 18.5%, geo. mean 3%). We found that the
FPMFP computation time was $2.9\times$ of the MFP computation time on average.

###### keywords:

Compilers, Data Flow Analysis, Infeasible Control Flow Paths, Static Program
Analysis, Maximum Fixed-Point Solution

##  1 Introduction

The effectiveness of techniques that optimize, verify, and debug computer
programs depends on the availability of accurate information describing the
program behavior during various executions. To this end, data flow analysis
gathers code level information that could answer either a subset of queries
over a program (demand-driven analyses) or all possible queries of a
particular type over a program (exhaustive analyses) without executing the
program. It is well known that computing highly precise exhaustive data flow
analysis solutions (like _meet over paths_ (MOP) [1]) is undecidable; even in
the instances where it is computable, it does not scale well to practical
programs. On the other hand, scalable and widely used solutions (like _maximum
fixed-point_ (MFP) [1]) are not as precise.

###  1.1 The Context of This Work

In this work, we focus on exhaustive data flow analyses because they compute
information that can be used to answer all queries of a particular type over
all program executions. In particular, we compute MFP solutions (details in
Section 4) and try to make them more precise.

A MFP solution includes the data flow values that reach a program point along
all _control flow paths_ (CFPs) [1] which are paths in the _control flow
graph_ (CFG) [1] representation of the program. Experimental evidence [2] on
Linux kernel code suggests that 9-40% of conditional statements in a program
lead to at least one infeasible CFP i.e., these CFPs do not occur in any
execution of the program. Additionally, we found in our benchmarks on average
60% (Geometric mean 29%) functions had at least one infeasible CFP in their
CFG. Inclusion of data flow values reaching along such infeasible CFPs makes
the computed data flow information an over-approximation of the actual data
flow information. This dilutes the usefulness of the information for client
analyses.

Various approaches reported in the literature detect infeasible CFPs [2, 3, 4,
5, 6, 7, 8, 9, 10, 11, 12]. Most of these approaches cater to the needs of
program testing, in which the knowledge of infeasible CFPs is used to refine
various test coverage criteria (like branch, path coverage) leading to less
testing overhead. However, not much attention has been given towards improving
the precision of data flow analysis by avoiding the data flow values reaching
along known infeasible CFPs. A potential reason being that CFP based data flow
approaches like MOP computation (that considers CFPs independently, and hence
can inherently exclude infeasible CFPs) are not scalable, because the number
of CFPs as well as the number of data flow values may be very large or even
unbounded. Hence, scalable approaches like MFP computation do not maintain a
mapping between individual CFPs and the corresponding data flow values, thus
making it non-trivial to identify (and discard) the data flow values reaching
along infeasible CFPs.

We name the MFP solutions computed by restricting the data flow values at each
program point to those values that reach along feasible CFPs as _feasible path
MFP_ (FPMFP) solutions. Existing approaches that attempt to compute such
solutions are either unsuitable because they involve CFG restructuring which
can exponentially blow up the size of the CFG or are analysis specific with no
straightforward generalization.

###  1.2 Our Contributions

We observe that infeasible CFPs are a property of programs and not of any
particular data flow analysis over programs. We use this observation to
separate the identification of infeasible CFPs in the CFG of a program, from
computation of FPMFP solutions that exclude data flow values reaching along
known infeasible CFPs. These two phases are described below.

  1. 1.

In the first phase, we use the work done by Bodik et.al [2] to detect
infeasible CFPs in the CFG of a program. In their work, they identify _minimal
infeasible path segments_ (MIPS) which are minimal length sub-segments of
infeasible CFPs such that the following holds: if a CFP $\sigma$ contains a
MIPS as a sub-segment then $\sigma$ is infeasible. MIPS 111We use the acronym
MIPS as an irregular noun, whose plural form is same as its singular form.
captures the infeasibility property of CFPs in a concise form (illustrated in
Section 3).

Given a set of MIPS as input, we do the following processing over them.

    1. (i)

We propose a novel criteria (called _contains-prefix-of_) to cluster MIPS.
This clustering is necessary because treating each MIPS in isolation may lead
to an imprecise solution, if the MIPS are intersecting with each other
(illustrated in Section 3.3).

    2. (ii)

We establish an equivalence relation over the clusters of MIPS, so that the
clusters that belong to the same equivalence class can be treated as a single
unit during FPMFP computation (illustrated in Section 6). This increases the
scalability of FPMFP computation without reducing the precision of the
computed solution.

  2. 2.

In the second phase, we automatically lift the existing MFP specifications of
an analysis to its FPMFP specifications using the processed MIPS from the
first phase. These specifications are then used to compute the FPMFP solution.
The computation of FPMFP solution satisfies the following properties that
distinguish FPMFP from existing approaches:

    1. (i)

Computation restricts the data flow values at each program point to those
values that reach along feasible CFPs (data flow values reaching along known
infeasible CFPs are identified and discarded).

    2. (ii)

Computation does not involve CFG restructuring and is generically applicable
for all MFP based data flow analyses.

Items (i) and (ii) in each of the above phases describe the distinguishing
features of FPMFP over existing approaches. Moreover, separating the above two
phases is an useful insight that avoids the costly repetition involved in
identifying infeasible CFPs for each different data flow analysis over the
same underlying program, which happens in analysis specific approaches [13,
14, 15, 16, 17, 18]. Instead, we perform the first phase that involves
identification of infeasible CFPs once for each program, and the second phase
that involves computation of FPMFP is performed once for each different data
flow analysis.

The core ideas of FPMFP have been presented before [19, 20]. This paper
enhances the core ideas significantly and provides a complete treatment. In
particular, the following contributions are exclusive to this paper.

  1. 1.

We unify our earlier approaches [19, 20] by proposing a novel formalization
for handling infeasible paths in the MFP computations. This formalization is
based on the contains-prefix-of relation (explained in Section 3.3) that
precisely distills the useful interactions between MIPS from all possible
interactions. The formalization is more intuitive to understand because of its
declarative nature as opposed to the procedural formalization earlier, and its
correctness is easier to prove and verify. Moreover, the new formalization of
FPMFP is close to the standard MFP formalization. We believe this will ease
the adoption of the FPMFP technique in data flow analysis.

  2. 2.

We formalize the concept of FPMFP for inter-procedural setting. In particular,
we extend it to the _functional approach_ [21] of inter-procedural data flow
analysis. We evaluate our inter-procedural technique of FPMFP computation on
an industry strength static program analysis tool called TCS ECA [22]. Inter-
procedural static analyses are known to be desirable to software developer
community [23].

  3. 3.

We improve the practical applicability of the FPMFP by adding novel
optimizations that improve the scalability of the FPMFP computation by the
factor of 2 without affecting soundness or precision of the computed solution.
The approach has now scaled on the codesets of size 150 KLOC.

  4. 4.

We prove that the FPMFP computes an over-approximation of the most precise
solution of a data flow problem. The most precise solution is called the _meet
over feasible paths_ (MOFP) solution and is explained in Section 2.

###  1.3 Organization of the Paper

Section 2 describes the limitations of existing approaches of data flow
analysis. Section 3 describes the concept of Minimal Infeasible Path Segments
that facilitate FPMFP solutions, and illustrates the FPMFP solution using an
example. Section 4 explains the computation of FPMFP. Section 5 explains FPMFP
computation in inter-procedural setting. Section 6 presents the optimizations
that improve the scalability of FPMFP computation and explains the worst-case
complexity of the FPMFP computation. Section 7 presents experimental
evaluation and Section 8 describes related work. Section 9 concludes the
paper. The appendix (Section 10) gives the proof of soundness of FPMFP
solution.

##  2 Existing Approaches and Their Limitations

Solution | Traverses CFPs | Merges information | Decidable | Precision
---|---|---|---|---
| Infeasible | Feasible | Spurious |  | Across
---
CFPs
| Across
---
program
points
MOFP | No | Yes | No | No | No | No | Most
MOP | Yes | Yes | No | No | No | No |
MFP | Yes | Yes | No | Yes | No | Yes |
FI | Yes | Yes | Yes | Yes | Yes | Yes | Least
Table 1: Solutions of a data flow analysis. As we go down the rows, more
entries become “Yes” leading to increased efficiency and decreased precision.

Table 1 lists the conventional solutions of a data flow analysis and mentions
their computability and (relative) precision by describing the nature of paths
traversed in computing the solutions. These paths are illustrated in Figure 1.
In particular, the paths that are traversed by a data flow analysis consist of
CFG paths or spurious paths (described below) or both. CFG paths (CFPs) that
do not represent any possible execution of the program are _infeasible_ ;
others are _feasible_. Apart from feasible and infeasible CFPs, a data flow
analysis could also traverse _spurious_ CFPs which are paths that result from
an over-approximation of CFPs—they do not appear in the CFG but are
effectively traversed by a specific method of data flow analysis as shown in
Table 1 and as explained below.

  * •

Meet Over Feasible Paths (MOFP) solution captures the information reaching a
program point along _feasible_ CFPs only and does not merge information across
CFPs. Since a program could have infinitely many CFPs, computing this solution
is _undecidable_. The information defined by MOFP precisely represents the
possible runtime information at each program point because it does not include
information reaching along infeasible and spurious CFPs.

  * •

Meet Over Paths (MOP) [1] solution captures the information reaching a program
point along _feasible_ and _infeasible_ CFPs. Since the information reaching
along infeasible CFPs is also considered, MOP is less precise compared to
MOFP. Computing MOP is also _undecidable_.

  * •

Maximum Fixed Point (MFP) [1] solution differs from MOP in that the
information is effectively merged in the shared segments of CFPs because the
solution is inductively computed. Since only one piece of information is
stored at a program point regardless of the number of paths passing through
it, computing MFP is _decidable_. MFP is less precise than MOP because
information across paths is merged and this over-approximation cannot
distinguish between feasible and infeasible paths. Spurious CFPs are not
traversed in MFP computation.

  * •

Flow Insensitive (FI) [1] solution merges information across all program
points by ignoring the control flow. Effectively, it over-approximates the set
of CFPs and hence includes information along feasible, infeasible, and
spurious CFPs.

All Paths$\begin{array}[]{c}\text{Spurious}\\\
\text{Paths}\end{array}$$\begin{array}[]{c}\text{\text{CFG}}\\\
\text{Paths}\end{array}$$\begin{array}[]{c}\text{Infeasible}\\\
\text{Paths}\end{array}$$\begin{array}[]{c}\text{Feasible}\\\
\text{Paths}\end{array}$ Figure 1: Paths Traversed During Data Flow Analyses

We propose an approach to compute FPMFP solutions in which the computation at
each program point is restricted to those data flow values that reach along
feasible CFPs (data flow values reaching along known infeasible CFPs are
excluded and spurious CFPs are not traversed).

Our work can be seen in the mould of trace partitioning [24] which tries to
maintain some disjunction over data flow values based on path conditions that
represent control flow of values instead of merging the values
indiscriminately across all paths to compute an MFP solution. However, in
trace partitioning, the desirable disjunctions (over data flow values) are not
generic, instead, they need to be specified for each data flow analysis
separately which limits the usefulness of trace partitioning.

Towards this end, we use the infeasibility of control flow paths—a property of
programs and not of any particular data flow analysis over the program—as the
criteria for trace partitioning. This allows us to achieve a generic and
practical trace partitioning that can be automatically incorporated in any
data flow analysis to obtain a more precise solution.

The main challenge in achieving this automatic approach is that it is
difficult to eliminate the effect of an infeasible path when data flow values
are merged which happens in MFP computation. We meet this challenge by
identifying MIPS (computed using existing approaches [2]) and creating
equivalence classes of CFPs; such that all CFPs in one equivalence class
overlap with the same set of MIPS. These classes allow us to lift any data
flow analysis to a data flow analysis that computes one data flow value for
each equivalence class. The resulting solution ignores data flow values
corresponding to equivalence classes containing infeasible CFPs and hence is
more precise than MFP (and sometimes more precise than MOP and as precise as
MOFP like in Figure 2).

| $a=0$$n_{1}$if $(x\\!\geq\\!0)$$n_{2}$$a=a+5$$n_{3}$print $x$$n_{4}$if
$(x==5)$$n_{5}$assert $(a\ !\\!=0)$$n_{6}$print
x$n_{7}$$e_{1}$$\\{a\\!\mapsto\\!0\;\text{(true)}\\}$[npos=.35,labelsep=.5]$e_{2}$[npos=.35,labelsep=.5]true
[npos=.9,labelsep=.5]$\\{a\\!\mapsto\\!0\;(x\\!\geq\\!0)\\}$[npos=.3,labelsep=.5]$e_{3}$[npos=.15,labelsep=.5]false
[npos=.5,labelsep=.5]$\\{a\\!\mapsto\\!0\;(x\\!<\\!0)\\}$[npos=.6,labelsep=.5]$e_{4}$[npos=.3,labelsep=.5]$\\{a\\!\mapsto\\!5\;(x\\!\geq\\!0)\\}$[labelsep=1]$e_{5}$[npos=.5,labelsep=1]$\begin{array}[]{@{}l@{}}\\{a\\!\mapsto\\!5\;(x\\!\geq\\!0),\\\
\phantom{\\{}a\\!\mapsto\\!0\;(x\\!<\\!0)\\}\end{array}$[npos=.35,labelsep=.5]$e_{6}$[npos=.35,labelsep=.2]true
[npos=0.9,labelsep=-.5]$\begin{array}[]{@{}l@{}}\\{a\\!\mapsto\\!5\;(x\\!=\\!5\land
x\\!\geq\\!0),\\\ \phantom{\\{}\text{\sout{$a\\!\mapsto\\!0\;(x\\!=\\!5\
\land\
x\\!<\\!0)$}}\\}\end{array}$[npos=.27,labelsep=1]$e_{7}$[npos=.15,labelsep=1]false
[npos=.6,labelsep=.5]$\begin{array}[]{@{}l@{}}\\{a\\!\mapsto\\!5\;(\begin{array}[t]{@{}l@{}}x\\!\neq\\!5\land\\\
x\\!\geq\\!0),\end{array}\\\
\phantom{\\{}a\\!\mapsto\\!0\;(\begin{array}[t]{@{}l@{}}x\\!\neq\\!5\land\\\
x\\!<\\!0)\\}\end{array}\end{array}$[npos=.55,labelsep=.5]$e_{8}$[npos=.25,labelsep=-.5]$\begin{array}[]{@{}l@{}}\\{a\\!\mapsto\\!5\;(x\\!=\\!5\land
x\\!\geq\\!0),\\\ \phantom{\\{}\text{\sout{$a\\!\mapsto\\!0\;(x\\!=\\!5\
\land\ x\\!<\\!0)$}}\\}\end{array}$
---
| $a=0$$n_{1}$if $(x\\!\geq\\!0)$$n_{2}$$a=a+5$$n_{3}$print $x$$n_{4}$if
$(x==5)$$n_{5}$assert $(a\ !\\!=0)$$n_{6}$print
x$n_{7}$$e_{1}$$\\{a\\!\mapsto\\![0,0]\\}$[npos=.35,labelsep=.5]$e_{2}$[npos=.35,labelsep=.5]true
[npos=.9,labelsep=.5]$\\{a\\!\mapsto\\![0,0]\\}$[npos=.3,labelsep=.5]$e_{3}$[npos=.15,labelsep=.5]false
[npos=.5,labelsep=.5]$\\{a\\!\mapsto\\![0,0]\\}$[npos=.6,labelsep=.5]$e_{4}$[npos=.3,labelsep=.5]$\\{a\\!\mapsto\\![5,5]\\}$[labelsep=1]$e_{5}$[npos=.5,labelsep=1]$\begin{array}[]{@{}l@{}}\\{a\\!\mapsto\\![0,5]\\}\end{array}$[npos=.35,labelsep=.5]$e_{6}$[npos=.35,labelsep=.2]true
[npos=.9,labelsep=.5]$\begin{array}[]{@{}l@{}}\\{a\\!\mapsto\\![0,5]\\}\end{array}$[npos=.4,labelsep=1]$e_{7}$[npos=.15,labelsep=1]false
[npos=.6,labelsep=.5]$\begin{array}[]{@{}l@{}}\\{a\\!\mapsto\\![0,5]\\}\end{array}$[npos=.55,labelsep=.5]$e_{8}$[npos=.3,labelsep=.5]$\\{a\\!\mapsto\\![0,5]\\}$
---
(a)  |  The MOP solution. The MOFP sol-
---
ution discards the struck off values.
(b)  |  The MFP solution. In FPMFP
---
solution, edges $e_{6}$ and $e_{8}$ have
the interval $[5,5]$.
Figure 2: Different solutions of value analysis for an example program. The
nodes in the CFG are numbered $n_{i}$, and the edges are numbered $e_{i}$. A
value $a\\!\mapsto\\!k\;(p)$ at edge $e$ indicates that the variable $a$ has
value $k$ at edge $e$ along CFP represented by condition $p$. The path
reaching $n_{6}$ shown by double lines is infeasible. For simplicity we have
shown the values for $a$ alone. The FI solution merges values across all
program points resulting in a single interval $[0,5]$.

Example 1.  Figure 2 shows an example of different solutions for an analysis
that determines the values of variables. For MOP and MOFP, each data flow
value has a constraint that represents the CFPs along which the value reaches
the program point. Since MFP, FPMFP, and FI solutions merge the values, they
compute a range of values in terms of lower and upper bounds. FPMFP solution
is more precise than MOP and MFP because it excludes the data flow value
$a\\!\mapsto\\![0,0]$ reaching along infeasible path at node $n_{6}$ (the
infeasible path is shown by double lines).

##  3 Feasible Path MFP Solutions

In this section, we define minimal infeasible path segments and show how they
allow us to define the FPMFP solution. Section 4 describes how FPMFP solution
is computed.

###  3.1 Background

#### Control Flow Paths

A control flow path is a path in the control flow graph representation of a
procedure. The start node of a CFP is always the start node of the CFG,
however, the end node of a CFP can be any node in the CFG. We use the term
“CFPs that reach node n” to refer to all CFPs that have $n$ as the end node.
All CFPs referred henceforth are intra-procedural, unless explicitly stated
otherwise.

#### Infeasible Control Flow Paths

We use the following concepts related to infeasible paths [2].

We denote a CFP by
$\rho:n_{1}\xrightarrow{e_{1}}n_{2}\xrightarrow{e_{2}}n_{3}\xrightarrow{e_{3}}\ldots\rightarrow
n_{p}\xrightarrow{e_{p}}n_{p+1}$, $p\geq 2$, where $n_{i}$ denotes the node at
the $i^{th}$ position in the path, and $e_{i}$ denotes its out edge. CFP
$\rho$ is an _infeasible control flow path_ if there is some conditional node
$n_{k},\,k\leq p$ such that the subpath from $n_{1}$ to $n_{k}$ of $\rho$ is a
prefix of some execution path but the subpath from $n_{1}$ to $n_{k+1}$ is not
a prefix of any execution path.222Note that the subscripts used in the nodes
and edges in a path segment signify positions of the nodes and edges in the
path segment and should not be taken as labels. By abuse of notation, we also
use $n_{1}$, $e_{2}$ etc. as labels of nodes and edge in a control flow graph
and then juxtapose them when we write path segments. A path segment
$\text{$\mu$}:n_{i}\xrightarrow{e_{i}}\ldots\rightarrow
n_{k}\xrightarrow{e_{k}}n_{k+1},\ e_{i}\not=e_{k}$ of CFP $\rho$ above is a
_minimal infeasible path segment_ (MIPS) if $\mu$ is not a subpath of any
execution path but every subpath of $\mu$ is a subpath of some execution path.
Infeasibility occurs when inconsistent conditions are expected to hold at two
different edges across a path segment. Hence every infeasible path must have
at least two edges.333We assume that the infeasible paths arising from the
conditional statements of the form _if_(_cond_) where _cond_ is known to be
either definitely zero or definitely non-zero, have been eliminated by the
compiler in the CFG.

For MIPS $\mu$ of the previous paragraph, we call all nodes $n_{j},\ i<j<k+1$
as the _intermediate_ nodes of $\mu$. Additionally, we call the edges $e_{i},\
e_{k}$ as the _start_ and the _end_ edge of $\mu$ respectively, while all
edges $e_{j},\ i<j<k$ are called as the _inner_ edges of MIPS $\mu$. As a
rule, the end edge of a MIPS is always a conditional edge, and inner edges
exist only if a MIPS has at least 3 edges. For the FPMFP computation, we only
admit MIPS that do not contain cycles. All MIPS referred henceforth are MIPS
without cycles.

|  Let $a$ be an integer variable, then the _states_ representing possible
value range for variable $a$ at each edge over all executions are: •
$\text{\emph{states}$(e_{0},\\{a\\})$}=\left\\{\\{a\mapsto i\\}\mid-\infty\leq
i\leq\infty\right\\}$ •
$\text{\emph{states}$(e_{1},\\{a\\})$}=\left\\{\\{a\mapsto 0\\}\right\\}$ •
$\text{\emph{states}$(e_{2},\\{a\\})$}=\left\\{\\{a\mapsto i\\}\mid-\infty\leq
i\leq\infty\right\\}$ •
$\text{\emph{states}$(e_{3},\\{a\\})$}=\left\\{\\{a\mapsto i\\}\mid-\infty\leq
i\leq\infty\right\\}$ •
$\text{\emph{states}$(e_{4},\\{a\\})$}=\left\\{\\{a\mapsto i\\}\mid
5<i\leq\infty\right\\}$ •
$\text{\emph{states}$(e_{5},\\{a\\})$}=\left\\{\\{a\mapsto i\\}\mid-\infty\leq
i\leq 5\right\\}$ Path segment
$\text{$\mu$}_{1}:n_{1}\xrightarrow{e_{1}}n_{3}\xrightarrow{e_{3}}n_{4}\xrightarrow{e_{4}}n_{5}$
is a MIPS because $e_{4}$ cannot be reached from $e_{1}$ in any execution
although it can be reached from $e_{3}$ in some execution i.e.,
$\text{\emph{states}$(e_{1},\\{a\\})$}\cap\text{\emph{states}$(e_{4},\\{a\\})$}=\Phi$,
$\text{\emph{states}$(e_{3},\\{a\\})$}\cap\text{\emph{states}$(e_{4},\\{a\\})$}=\\{\\{a\mapsto
i\\}\mid 5<i\leq\infty\\}$ The _start_ , _inner_ , and _end_ edges of
$\text{$\mu$}_{1}$ are given by, $\emph{start}(\text{$\mu$}_{1})=\\{e_{1}\\},\
\emph{inner}(\text{$\mu$}_{1})=\\{e_{3}\\},\
\emph{end}(\text{$\mu$}_{1})=\\{e_{4}\\}$
---
| $z<1$$n_{0}$$a\\!=\\!0$$n_{1}$use a$n_{3}$$a\\!>\\!5$$n_{4}$use a$n_{5}$use
a[npos=0.4,labelsep=.5]$e_{0}$[npos=0.7,labelsep=0.2]true[npos=0.35,labelsep=0]$e_{1}$[npos=0.5,labelsep=.5]$e_{2}$[npos=0.65,labelsep=0.2]false[npos=0.5,labelsep=.5]$e_{3}$[npos=0.5,labelsep=0.2]$e_{4}$[npos=0.7,labelsep=0.2]true[npos=0.33,labelsep=.2]$e_{5}$[npos=0.8,labelsep=.2]false
---
Figure 3: Illustrating minimal infeasible path segment (MIPS).

Example 1.  Figure 3 illustrates infeasible paths and MIPS. Observe that the
CFP
$\displaystyle\rho:n_{0}\xrightarrow{e_{0}}n_{1}\xrightarrow{e_{1}}n_{3}\xrightarrow{e_{3}}n_{4}\xrightarrow{e_{4}}n_{5}$
is infeasible but not minimal . However, its suffix $\text{$\mu$}_{1}$ is a
MIPS,
$\text{$\mu$}_{1}:n_{1}\xrightarrow{e_{1}}n_{3}\xrightarrow{e_{3}}n_{4}\xrightarrow{e_{4}}n_{5}$,
because $\text{$\mu$}_{1}$ is infeasible but no sub-segment of
$\text{$\mu$}_{1}$ is infeasible.

###  3.2 Our Key Idea

We define the following notations that allow us to describe the key ideas. For
a given MIPS $\mu$, let $\emph{start}(\text{$\mu$})$,
$\emph{inner}(\text{$\mu$})$, and $\emph{end}(\text{$\mu$})$ denote the set of
start, inner, and end edges of $\mu$. Sets $\emph{start}(\text{$\mu$})$ and
$\emph{end}(\text{$\mu$})$ are singleton because each MIPS has exactly one
start and one end edge. MIPS exhibit the following interesting property:

###### Observation 3.1

CFPs that contain a MIPS $\mu$ as a sub-segment are infeasible. Consequently,
the data flow values computed along CFPs that contain $\mu$ are unreachable at
the end edge of $\mu$, so these values should be blocked at the end edge.
Thus, if we define a data flow analysis that separates the data flow values
that are to be blocked, we can eliminate them thereby avoiding the effect of
infeasible paths.

Example 1.  In Figure 3, a CFP
$\sigma:n_{0}\xrightarrow{e_{0}}n_{1}\xrightarrow{e_{1}}n_{3}\xrightarrow{e_{3}}n_{4}\xrightarrow{e_{4}}n_{5}$
is infeasible because it contains MIPS
$\text{$\mu$}_{1}:n_{1}\xrightarrow{e_{1}}n_{3}\xrightarrow{e_{3}}n_{4}\xrightarrow{e_{4}}n_{5}$.
Hence, the data flow value that reaches along $\sigma$ (e.g., $a\mapsto[0,0]$,
$z\mapsto[-\infty,0]$) is blocked at $e_{4}$ (which is end edge of MIPS
$\text{$\mu$}_{1}$).

Observation 3.1 leads us to the following key idea to handle infeasible paths:
at each program point, we separate the data flow values reaching along CFPs
that contain a MIPS, from the data flow values reaching along CFPs that do not
contain any MIPS. This allows us to discard these values at the end of the
MIPS (because these values are unreachable as per Observation 3.1).

|  | Data Flow Values | Meet
---|---|---|---
|  | flowing through $\text{$\mu$}_{1}$ | not flowing through $\text{$\mu$}_{1}$ | $\sqcap$
Edges | $e_{0}$ | $\top$ | $z\mapsto[-\infty,0]$ | $z\mapsto[-\infty,0]$
$e_{2}$ | $\top$ | $z\mapsto[1,\infty]$ | $z\mapsto[1,\infty]$
$e_{1}$ | $z\mapsto[-\infty,0]$ | $\top$ | $z\mapsto[-\infty,0]$
$e_{3}$ | $z\mapsto[-\infty,0]$ | $z\mapsto[1,\infty]$ | $z\mapsto[-\infty,\infty]$
| $e_{4}$ |  $\top$ $z\mapsto[-\infty,0]$ | $z\mapsto[1,\infty]$ | $z\mapsto[1,\infty]$
| $e_{5}$ | $z\mapsto[-\infty,0]$ | $z\mapsto[1,\infty]$ | $z\mapsto[-\infty,\infty]$
Table 2: Separating the Values Flowing through MIPS $\text{$\mu$}_{1}$ for
example in Figure 3: $\top$ represents top value of the lattice, the last
column contains the result of meet of all data flow values present in a row at
each edge, for simplicity values of only $z$ are shown.

For a MIPS $\mu$, following is a sufficient condition to block the data flow
values that reach along CFPs that contain $\mu$.

> $\mathbb{C}$: At the end edge of $\mu$, block the data flow values that
> _flow through_ $\mu$ (i.e., values that flow along $\mu$ —from start edge of
> $\mu$ till the end edge of $\mu$).

Example 2.  For example in Figure 3, the values (of variable $z$) that _flow
through_ MIPS $\mu_{1}$ are shown in Table 2. The value $z\mapsto[-\infty,0]$
reaches the start edge ($e_{1}$) of $\mu_{1}$, and flows through $\mu_{1}$.
This value is separated from the values that do not flow through $\mu_{1}$
e.g., $z\mapsto[1,\infty]$. This separation allows us to identify and block
the value $z\mapsto[-\infty,0]$ at the end edge ($e_{4}$) of $\mu_{1}$. The
final value at each edge, except the end edge, is computed by taking a meet of
values that _flow through_ $\mu_{1}$, with values that do not flow through
$\mu_{1}$. However, the final value at end edge contains only the values that
do not flow through $\mu_{1}$. Thus, we get a precise value range for $z$ at
edge $e_{4}$ (i.e., $z\mapsto[1,\infty]$) because value $z\mapsto[-\infty,0]$
is blocked (a MFP solution that includes data flow values along infeasible
CFPs gives value range $z\mapsto[-\infty,\infty]$ at edge $e_{4}$).

Note that the data flow values that reach the start edge of a MIPS $\mu$ may
change or get killed at intermediate nodes or edges when they flow through
$\mu$, depending on the type of data flow analysis. In this case, we block the
updated data flow value accordingly, as illustrated in example 3.2 below.

Example 3.  Consider a MIPS $\mu$:
$n_{1}\xrightarrow{e_{1}}n_{2}\xrightarrow{e_{2}}n_{3}\xrightarrow{e_{3}}n_{4}$
with $e_{1},\ e_{2},\ e_{3}$ as the start, the inner, and the end edge
respectively. Let $x$ be an integer variable such that $n_{1}:x=0$,
$n_{2}:x=x+1$ be two assignment nodes, and nodes $n_{3},n_{4}$ do not modify
the value of the variable $x$. The data flow value $x\mapsto[0,0]$ at the
start edge ($e_{1}$) of $\mu$ will be changed to $x\mapsto[1,1]$ as it flows
through $\mu$. Hence $x\mapsto[1,1]$ is blocked at $e_{3}$.

###  3.3 An Overview of FPMFP computation

We now briefly explain the steps of FPMFP computation that ensure that
condition $\mathbb{C}$ (from the previous section) is satisfied for all MIPS
in the program. The formal details of FPMFP computation are presented in
sections 3.4 and 4.

We first explain the FPMFP computation in presence of single MIPS in the
program. Later, we introduce the necessary changes to handle multiple MIPS in
the program. We use the example in Figure 4a as a running example for
explaining FPMFP computation. Two MIPS in Figure 4a are
$\text{$\mu_{1}$}:e_{3}\rightarrow e_{4}\rightarrow e_{5}$ and
$\text{$\mu_{2}$}:e_{3}\rightarrow e_{4}\rightarrow e_{8}$ (They are marked
with double arrows). For simplicity of exposition, we restrict the discussion
to computation of value range of variable $l$ only.

In FPMFP computation for the example in Figure 4a, we separate the value
$l\mapsto[0,0]$ that flows through $\mu_{1}$ from the value $l\mapsto[2,2]$
that does not flow through $\mu_{1}$ as shown in Figure 4b. This allows us to
block $l\mapsto[0,0]$ at the end edge ($e_{5}$) of $\mu_{1}$. Thus, the FPMFP
solution —computed by meet of data flow values in each row at each edge
—contains $l\mapsto[2,2]$ (a precise value) at edge $e_{5}$.

The FPMFP computation explained in previous paragraph becomes imprecise if we
additionally separate the data flow values that flow through MIPS $\mu_{2}$,
as explained below. For MIPS $\mu_{2}$: $e_{3}\rightarrow e_{4}\rightarrow
e_{8}$, we separate the values that flow through $\mu_{2}$ (i.e.,
$l\mapsto[0,0]$) as shown in Figure 4c. This allows us to block
$l\mapsto[0,0]$ at end edge ($e_{8}$) of $\mu_{2}$. However, the FPMFP
solution (computed in Figure 4c) is imprecise because it includes the value
$l\mapsto[0,0]$ at edge $e_{5}$ and $e_{8}$. In particular, at edge $e_{5}$,
$l\mapsto[0,0]$ is blocked within $\mu_{1}$ but it is retained in $\mu_{2}$
because $e_{5}$ is not end edge of $\mu_{2}$. Similarly, at edge $e_{8}$,
$l\mapsto[0,0]$ is blocked within $\mu_{2}$ but is retained in $\mu_{1}$.

| $\begin{array}[]{@{}l@{}}\emph{l=2}\\\ \emph{input c}\\\
\emph{if$(p1>0)$}\end{array}$$\begin{array}[]{c}l=0\\\ c=0\end{array}$
_print l_ switch$(c)$$\begin{array}[]{c}assert\\\
(l!\\!=0)\end{array}$$\begin{array}[]{c}assert\\\
(l!\\!=0)\end{array}$
_exit_[npos=.2,labelsep=.2]$e_{1}$[npos=.6,labelsep=.5]true
[npos=.2,labelsep=.2]false
[npos=.35,labelsep=.5]$e_{2}$[npos=.6,labelsep=.5]$e_{3}$[npos=.6,labelsep=.5]$e_{4}$[npos=.9,labelsep=.1]$e_{5}$[npos=.45,labelsep=.1,nrot=0]case
1 [npos=.9,labelsep=.1]$e_{8}$[npos=.45,labelsep=.01,nrot=0]case 2
[npos=.2,labelsep=.5]$e_{7}$[npos=.45,labelsep=.5] default
[npos=.6,labelsep=.5]$e_{6}$[npos=.6,labelsep=.5]$e_{9}$
---
|  | $\begin{array}[]{l}\text{Paths and \text{MIPS}:}\\\ \bullet\ \text{MIPS}\ \text{$\mu$}_{1}:e_{3}\rightarrow e_{4}\rightarrow e_{5}\\\ \bullet\ \text{MIPS}\ \text{$\mu$}_{2}:e_{3}\rightarrow e_{4}\rightarrow e_{8}\\\ \bullet\ \emph{start}(\text{$\mu$}_{1})=\emph{start}(\text{$\mu$}_{2})=e_{3}\\\ \bullet\ \emph{inner}(\text{$\mu$}_{1})=\emph{inner}(\text{$\mu$}_{2})=e_{4}\\\ \bullet\ \emph{end}(\text{$\mu$}_{1})=e_{5},\emph{end}(\text{$\mu$}_{2})=e_{8}\\\ \end{array}$
---
|  Edges | Data Flow Values | FPMFP
---|---|---
flowing | not flowing | $\sqcap$
|  through $\text{$\mu$}_{1}$ |  through $\text{$\mu$}_{1}$ |
$e_{3}$ | $l\mapsto[0,0]$ | $\top$ | $l\mapsto[0,0]$
$e_{4}$ | $l\mapsto[0,0]$ | $l\mapsto[2,2]$ | $l\mapsto[0,2]$
$e_{5}$ | $\top$ | $l\mapsto[2,2]$ | $l\mapsto[2,2]$
$e_{8}$ | $l\mapsto[0,0]$ | $l\mapsto[2,2]$ | $l\mapsto[0,2]$
(b)
|  Edges | Data Flow Values | FPMFP
---|---|---
flowing through | not flowing | $\sqcap$
| MIPS | through |
| $\text{$\mu$}_{1}$ | $\text{$\mu$}_{2}$ | MIPS |
$e_{3}$ | $l\mapsto[0,0]$ | $l\mapsto[0,0]$ | $\top$ | $l\mapsto[0,0]$
$e_{4}$ | $l\mapsto[0,0]$ | $l\mapsto[0,0]$ | $l\mapsto[2,2]$ | $l\mapsto[0,2]$
$e_{5}$ | $\top$ | $l\mapsto[0,0]$ | $l\mapsto[2,2]$ | $l\mapsto[0,2]$
$e_{8}$ | $l\mapsto[0,0]$ | $\top$ | $l\mapsto[2,2]$ | $l\mapsto[0,2]$
(a) | (c)
Figure 4: Computing the FPMFP solution for an example having overlapping MIPS.

We explicate the reasons for this imprecision below: we separate the data flow
values that reach along CFPs that contain a MIPS, however, a MIPS can overlap
with other MIPS in a way that both MIPS follow the same CFP resulting in the
same data flow values flowing through them. In such a case, at the end edge of
a MIPS, the data flow along that MIPS will be blocked but the flow along the
other overlapping MIPS will be allowed unless the edge is end edge of both the
MIPS. This leads to imprecision. Hence we need to handle the overlapping MIPS
case explicitly. For this purpose, we define a _contains-prefix-of_ relation
between MIPS below.

###### Definition 1

(Contains-prefix-of (CPO)) For a MIPS $\mu$ and an edge $e$ in $\mu$, let
_prefix_ $(\text{$\mu$},e)$ be the subsegment of $\mu$ from
$\emph{start}(\text{$\mu$})$ to $e$. Then, we say that MIPS $\mu_{1}$
contains-prefix-of MIPS $\mu_{2}$ at $e$, iff $\mu_{1}$ contains _prefix_
$(\text{$\mu_{2}$},e)$.

For example in Figure 4, the MIPS $\mu_{1}$ contains-prefix-of $\mu_{2}$ 444In
this case $\mu_{2}$ also contains-prefix-of $\mu_{1}$ at $e_{3}$ and $e_{4}$,
however in general contains-prefix-of may not be a symmetric relation. at
edges $e_{3}$ and $e_{4}$. For a MIPS $\mu_{1}$ and an edge $e$, all MIPS
$\mu_{2}$ that satisfy $\mu_{1}$ CPO $\mu_{2}$ are obtained as follows: let
$\mathcal{U}$ be the set of all MIPS in the CFG of the program.

$\text{\emph{cpo}}_{e}(\text{$\mu_{1}$})$
$\displaystyle=\\{\text{$\mu_{2}$}\mid\text{$\mu_{2}$}\in\text{$\mathcal{U}$},\
\text{$\mu_{1}$}\ \text{contains}\
\text{\emph{prefix}$(\text{$\mu_{2}$},e)$}\\}$ (1)

We observe the following property of
$\text{\emph{cpo}}_{e}(\text{$\mu_{1}$})$.

###### Observation 3.2

Because of the prefix relation, all MIPS in
$\text{\emph{cpo}}_{e}(\text{$\mu_{1}$})$ essentially follow the same control
flow path till edge $e$ although their start edges may appear at different
positions in the path. Next, the values along this path flow through each MIPS
in $\text{\emph{cpo}}_{e}(\text{$\mu_{1}$})$. Hence, these values should be
blocked at the end edge of every MIPS in
$\text{\emph{cpo}}_{e}(\text{$\mu_{1}$})$.

For an edge sequence $e\rightarrow e^{\prime}$,
$\text{\emph{cpo}}_{e}(\text{$\mu$})$ may be different from
$\text{\emph{cpo}}_{e^{\prime}}(\text{$\mu$})$ because all MIPS that reach $e$
may not reach $e^{\prime}$, and some new MIPS may start at $e^{\prime}$.
Hence, we define _ext_ function below that computes
$\text{\emph{cpo}}_{e^{\prime}}(\text{$\mu$})$ from
$\text{\emph{cpo}}_{e}(\text{$\mu$})$.

Let _edges_($\mu$) be the set of all edges in $\mu$, and
$\text{$\mathcal{S}$}=\text{$\text{\emph{cpo}}_{e}(\text{$\mu$})$}$ then

$\text{\emph{ext}}(\text{$\mathcal{S}$},e^{\prime})$
$\displaystyle=\\{\text{$\mu$}\mid\text{$\mu$}\in\text{$\mathcal{S}$},\,e^{\prime}\in\text{\emph{edges}(\text{$\mu$})}\\}\
\cup\ \\{\text{$\mu$}\mid\text{$\mu$}\in\text{$\mathcal{U}$},\
e^{\prime}\in\emph{start}(\text{$\mu$})\\}$ (2)

At an edge $e$ of MIPS $\mu$, we associate the data flow values that flow
through $\mu$ with $\text{\emph{cpo}}_{e}(\text{$\mu$})$ (instead of $\mu$).
These associations are abstractly illustrated in Figure 5a and instantiated to
an example in Figure 5b. We explain each of these below.

In Figure 5a, the data flow values $d,\,d^{\prime}\\!,\,d^{\prime\prime}$
reach edges $e,\,e^{\prime}\\!,\,e^{\prime\prime}$ respectively, along the
following CFP:
$\sigma:n_{0}\xrightarrow{e}n_{1}\xrightarrow{e^{\prime}}n_{2}\xrightarrow{e^{\prime\prime}}n_{3}$.
The data flow value $d^{\prime}=f_{n1}(d)$ and
$d^{\prime\prime}=f_{n2}(d^{\prime})$ where $f_{ni}(x)$ computes the effect of
node $n_{i}$ on input data flow value $x$. The corresponding associations with
sets of MIPS
$\text{$\mathcal{M}$},\,\text{$\mathcal{M}$}^{\prime},\,\text{$\mathcal{M}$}^{\prime\prime}$
are computed as follows:

$\mathcal{M}$ $\displaystyle=\text{$\text{\emph{ext}}(\\{\\},e)$}$
$\displaystyle\text{$\mathcal{M}$}^{\prime}$
$\displaystyle=\text{$\text{\emph{ext}}(\text{$\mathcal{M}$},e^{\prime})$}$
$\displaystyle\text{$\mathcal{M}$}^{\prime\prime}$
$\displaystyle=\text{$\text{\emph{ext}}(\text{$\mathcal{M}$}^{\prime},e^{\prime\prime})$}$

The idea is that a pair $\langle\text{$\mathcal{M}$},d\rangle$ at edge $e$
transforms into another pair
$\langle\text{$\mathcal{M}$}^{\prime},d^{\prime}\rangle$ at a successor edge
$e^{\prime}$ because

  * •

the CPO relation between MIPS at $e^{\prime}$ may be different from that at
$e$, and

  * •

$d^{\prime}$ is computed from $d$ as $d^{\prime}=f_{n1}(d)$.

In Figure 5b, the data flow values $l\mapsto[2,2]$ at edge $e_{1}$ is
associated with {} because no MIPS contains $e$. However, at edges
$e_{3},\,e_{4}$, the data flow value $l\mapsto[0,0]$ is associated with
$\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$ because $\mu_{1}$ CPO $\mu_{2}$ at
these edges i.e.,
$\text{$\text{\emph{ext}}(\text{$\\{\text{$\mu_{1}$}\\}$},e_{3})$}=\text{$\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$}$,
$\text{$\text{\emph{ext}}(\text{$\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$},e_{4})$}=\text{$\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$}$.
At $e_{5}$, $l\mapsto[0,0]$ is associated with $\\{\text{$\mu_{1}$}\\}$
because
$\text{$\text{\emph{ext}}(\text{$\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$},e_{5})$}=\text{$\\{\text{$\mu_{1}$}\\}$}$.
Since $e_{5}$ is end edge of $\mu_{1}$, $l\mapsto[0,0]$ is blocked at $e_{5}$.
Similarly, $l\mapsto[0,0]$ is blocked at $e_{8}$. Rest of the associations at
each edge are presented in Table 3.

|
$n_{0}$$n_{1}$$n_{2}$$n_{3}$$e$$\langle\text{$\mathcal{M}$},d\rangle$$e^{\prime}$$\langle\text{$\mathcal{M}$}^{\prime},d^{\prime}\rangle$$e^{\prime\prime}$$\langle\text{$\mathcal{M}$}^{\prime\prime},d^{\prime\prime}\rangle$
---
| $\begin{array}[]{@{}l@{}}\emph{l=2}\\\ \emph{input c}\\\
\emph{if$(p1>0)$}\end{array}$$\begin{array}[]{c}l=0\\\ c=0\end{array}$_print
l_ switch$(c)$$\begin{array}[]{c}assert\\\
(l!\\!=0)\end{array}$$\begin{array}[]{c}assert\\\
(l!\\!=0)\end{array}$_exit_[npos=.2,labelsep=.2]$e_{1}$[npos=.4,labelsep=.5]true
[npos=0.8]$\langle\\{\\},\text{$l\mapsto[2,2]$}\rangle$[npos=.2,labelsep=.2]false
[npos=.35,labelsep=.5]$e_{2}$[npos=.2,labelsep=.5]$e_{3}$[npos=.6,labelsep=-0.4]$\langle\text{$\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$},\text{$l\mapsto[0,0]$}\rangle$[npos=.6,labelsep=.5]$e_{4}$$\langle\text{$\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$},\text{$l\mapsto[0,0]$}\rangle$[npos=.4,labelsep=.1]$e_{5}$[npos=.75,labelsep=.1,nrot=0]case
1
[npos=0.4]$\langle\text{$\\{\text{$\mu_{1}$}\\}$},\text{\sout{\text{$l\mapsto[0,0]$}}}\rangle$[npos=.4,labelsep=.1]$e_{8}$[npos=.75,labelsep=.01,nrot=0]case
2
[npos=0.4]$\langle\text{$\\{\text{$\mu_{2}$}\\}$},\text{\sout{\text{$l\mapsto[0,0]$}}}\rangle$[npos=.7,labelsep=.5]$e_{7}$[npos=.45,labelsep=.5]
default [npos=.6,labelsep=.5]$e_{6}$[npos=.6,labelsep=.5]$e_{9}$
---
$\begin{array}[]{l}\text{(a) Generic view of }\\\ \text{data flow along a \text{CFP}.}\end{array}$ | $\begin{array}[]{l}\text{(b) Illustrating the flow of values for the example}\\\ \text{in Figure~{}\ref{fig:intersecting.mipsone}. For brevity, only values of variable $l$ }\\\ \text{are shown along \text{{CFP\/}s} that start at edge $e_{1}$.}\end{array}$
Figure 5: Computing the FPMFP solution Edges | Associations ($\langle\text{$\mathcal{M}$},d\rangle$) | FPMFP | MFP
---|---|---|---
$e_{1}$ | $\langle\\{\\},\text{$l\mapsto[2,2]$}\rangle$ | $l\mapsto[2,2]$ | $l\mapsto[2,2]$
$e_{2}$ | $\langle\\{\\},\text{$l\mapsto[2,2]$}\rangle$ | $l\mapsto[2,2]$ | $l\mapsto[2,2]$
$e_{3}$ | $\langle\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\},\text{$l\mapsto[0,0]$}\rangle$ | $l\mapsto[0,0]$ | $l\mapsto[0,0]$
$e_{4}$ | $\text{$\langle\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\},\text{$l\mapsto[0,0]$}\rangle$},\ \text{$\langle\\{\\},\text{$l\mapsto[2,2]$}\rangle$}$ | $l\mapsto[0,2]$ | $l\mapsto[0,2]$
$e_{5}$ | $\text{$\langle\\{\text{$\mu_{1}$}\\},\text{\sout{\text{$l\mapsto[0,0]$}}}\rangle$},\text{$\langle\\{\\},\text{$l\mapsto[2,2]$}\rangle$}$ | $l\mapsto[2,2]$ | $l\mapsto[0,2]$
$e_{7}$ | $\langle\\{\\},\text{$l\mapsto[0,2]$}\rangle$ | $l\mapsto[0,2]$ | $l\mapsto[0,2]$
$e_{8}$ | $\text{$\langle\\{\text{$\mu_{2}$}\\},\text{\sout{\text{$l\mapsto[0,0]$}}}\rangle$},\text{$\langle\\{\\},\text{$l\mapsto[2,2]$}\rangle$}$ | $l\mapsto[2,2]$ | $l\mapsto[0,2]$
Table 3: The FPMFP computation for example in Figure 4. A pair
$\langle\text{$\mathcal{M}$},d\rangle$ indicates that the data flow value $d$
flows through all MIPS in set of MIPS $\mathcal{M}$. The final FPMFP solution
is computed by taking meet of values over all pairs at each edge.

We now introduce the notations used in the FPMFP computation. We compute a set
of pairs of the form $\langle\text{$\mathcal{M}$},d\rangle$ at each edge $e$
where $\mathcal{M}$ is a _set of MIPS_, and $d$ is the data flow value that
flows through all MIPS in $\mathcal{M}$. For completeness, we have a pair
$\langle\text{$\mathcal{M}$}^{\prime},d\rangle$ corresponding to each possible
subset $\text{$\mathcal{M}$}^{\prime}$ of $\mathcal{U}$ at each edge $e$,
where $d=\top$ if the MIPS in $\text{$\mathcal{M}$}^{\prime}$ are not related
with each other by CPO relation i.e., there is no MIPS $\mu$ in
$\text{$\mathcal{M}$}^{\prime}$ such that
$\text{$\text{\emph{cpo}}_{e}(\text{$\mu$})$}=\text{$\mathcal{M}$}^{\prime}$.

At an edge $e$, presence of a pair
$\text{$\langle\text{$\mathcal{M}$},d\rangle$},\ d\not=\top$ indicates the
data flow value $d$ flows through each MIPS contained in $\mathcal{M}$, and
for some
$\text{$\mu$}\in\text{$\mathcal{M}$},\text{$\mathcal{M}$}=\text{$\text{\emph{cpo}}_{e}(\text{$\mu$})$}$.
Similarly, a pair $\langle\text{$\\{\\}$},d^{\prime}\rangle$ indicates that
the data flow value $d^{\prime}$ does not flow through any MIPS at edge $e$.

Example 1.  Figure 6 illustrates the FPMFP computation for the example in
Figure 2. Since $\mu$ is the only MIPS in the example, each data flow value
$d$ is mapped with either $\\{\text{$\mu$}\\}$ or $\\{\\}$. The data flow
value $a\mapsto[0,0]$ reaches the start edge ($e_{3}$) of $\mu$, hence, a pair
$\langle\\{\text{$\mu$}\\},\text{$a\mapsto[0,0]$}\rangle$ is created at
$e_{3}$. Similarly, at edge $e_{4}$, data flow value $a\mapsto[5,5]$ is mapped
with $\\{\\}$ i.e., a pair
$\langle\text{$\\{\\}$},\text{$a\mapsto[5,5]$}\rangle$ is created. Edge
$e_{6}$ is end edge of $\mu$, hence, the data flow value $a\mapsto[0,0]$ that
is mapped with $\mu$ in pair
$\langle\\{\text{$\mu$}\\},\text{$a\mapsto[0,0]$}\rangle$ is discarded i.e.,
replaced with $\top$ (the resulting pair
$\langle\\{\text{$\mu$}\\},\top\rangle$ at $e_{6}$ is not shown in figure for
brevity).

For a program containing $k$ MIPS, theoretically we need $2^{k}$ pairs 555In
Section 6.4, we prove that at any program point at most $k$ pairs can contain
the data flow values other than $\top$, where $k$ is the total number of input
MIPS. Further, our empirical evaluation shows that the number of such pairs to
be much smaller than $k$. Moreover, ignoring the pairs that contain $\top$
value does not affect the FPMFP solution (details are given in Section 6.3).
at each program point (one pair corresponding to each possible subset of _set
of all MIPS_ present in the program). The pairs computed in a FPMFP solution
satisfy the following property:

> At each program point, the meet of data flow values over all pairs gives at
> least as precise information as in MFP solution, and may give more precise
> information if some pairs contain information reaching from infeasible CFPs
> because such information is discarded. The precision is achieved only when
> the discarded information has weaker value or incomparable value compared to
> rest of the information reaching a node. Let $D_{n}$ be the data flow value
> in MFP solution at node $n$, and $\mathcal{S}_{n}$ be the set of pairs
> computed in FPMFP analysis at node $n$ then
>
> $\displaystyle
> D_{n}\sqsubseteq\bigsqcap_{\text{$\langle\text{$\mathcal{M}$},d\rangle$}\in\text{$\mathcal{S}_{n}$}}d$

Example 2.  In Figure 6, at the edge $e_{5}$ the meet of data flow values over
all pairs i.e., $\langle\\{\text{$\mu$}\\},\text{$a\mapsto[0,0]$}\rangle$ and
$\langle\text{$\\{\\}$},\text{$a\mapsto[5,5]$}\rangle$ is $a\mapsto[0,5]$
which is same as given by MFP solution in Figure 2; however, at the edge
$e_{6}$ the meet of data flow values over all pairs i.e.,
$\langle\\{\text{$\mu$}\\},\top\rangle$ and
$\langle\text{$\\{\\}$},\text{$a\mapsto[5,5]$}\rangle$ is $a\mapsto[5,5]$
which is more precise compared to $a\mapsto[0,5]$ given by MFP solution in
Figure 2.

###  3.4 Defining FPMFP solution

We now explain how these ideas are incorporated in a data flow analysis. We
compute the FPMFP solution in the following two steps.

  1. 1.

_Step 1_ : we lift a data flow analysis to an analysis that computes separate
data flow values for different MIPS (Equation 8 and 9 define the lifted
analysis). The lifted analysis blocks the data flow values associated with
each MIPS $\mu$ at the end edge of $\mu$.

  2. 2.

_Step 2_ : we merge the data flow values that are computed by the lifted
analysis (over all pairs at each program point) to obtain the FPMFP solution
(Equation 3 and 4 define the merging of data flow values).

We describe each of these steps in detail now. Let $\mathcal{L}$ denote the
lattice of data flow values of the underlying data flow analysis. Then the MFP
solution of the data flow analysis for a program is a set of values in
$\mathcal{L}$, represented by data flow variables
$\emph{In}_{n}/\emph{Out}_{n}$ (Equation 6 and 7) for every node $n$ of the
CFG of the program, when the equations are solved using $\top$ as the initial
value of $\emph{In}_{n}/\emph{Out}_{n}$. Assume we are given a set
$\mathcal{U}$ that contains all MIPS in the CFG of the program, then each
$\text{$\mathcal{M}$}\subseteq\text{$\mathcal{U}$}$ could be associated with
any data flow value $d$ in $\mathcal{L}$, if $d$ flows through each MIPS
contained in $\mathcal{M}$. These associations are represented by the elements
of the lattice
$\text{$\overline{\mathcal{L}}$}:\text{$\mathcal{P}(\text{$\mathcal{U}$})$}\rightarrow\text{$\mathcal{L}$}$,
where $\mathcal{P}(\text{$\mathcal{U}$})$ is the powerset of $\mathcal{U}$.

We lift the underlying analysis that computes values
$\emph{In}_{n}/\emph{Out}_{n}\in\text{$\mathcal{L}$}$ to an analysis that
computes
$\text{$\overline{\emph{In}}$}_{n}/\text{$\overline{\emph{Out}}$}_{n}\in\text{$\overline{\mathcal{L}}$}$.
Thus $\text{$\overline{\emph{In}}$}_{n}$, $\text{$\overline{\emph{Out}}$}_{n}$
are sets of pairs $\langle\text{$\mathcal{M}$},d\rangle$ such that
$\text{$\mathcal{M}$}\subseteq\text{$\mathcal{U}$}$,
$d\in\text{$\mathcal{L}$}$. Each of these sets represent a _function_ that
maps each value in $\mathcal{P}(\text{$\mathcal{U}$})$ to a value in
$\mathcal{L}$ i.e., $\emph{In}_{n}/\emph{Out}_{n}$ cannot contain two pairs
$\langle\text{$\mathcal{M}$},d\rangle$ and
$\langle\text{$\mathcal{M}$}^{\prime},d^{\prime}\rangle$ where
$\text{$\mathcal{M}$}=\text{$\mathcal{M}$}^{\prime}$ but $d\not=d^{\prime}$.
This collection of pairs gives us the distinctions required to achieve
precision by separating the data flow values along infeasible paths from those
along feasible paths.

For a data flow value $\text{$\overline{\emph{In}}$}_{n}$, the meaning of
association of a data flow value $d$ with a set of MIPS $\mathcal{M}$ is as
follows:

  * •

Pair
$\text{$\langle\text{$\mathcal{M}$},d\rangle$}\in\text{$\overline{\emph{In}}$}_{n}$,
indicates that the data flow value $d$ flows through all MIPS in
$\mathcal{M}$. If no such value exists at $n$, then $d=\top$.

  * •

Pair
$\text{$\langle\text{$\\{\\}$},d\rangle$}\in\text{$\overline{\emph{In}}$}_{n}$,
indicates that the data flow value $d$ does not flow through any MIPS at node
$n$. If no such value exists (i.e., every data flow value flows through some
or the other MIPS) then $d=\top$.

Example 1.  In Figure 6, the data flow value $a\mapsto[0,0]$ flows through
MIPS $\mu$ at edges $e_{3},\ e_{5},$ and $e_{6}$. On the other hand, the data
flow value $a\mapsto[5,5]$ does not flow through any MIPS. (Recall that flow
through a MIPS $\mu$ means flow along $\mu$ —from start edge of $\mu$ till end
edge of $\mu$).

Section 4 defines the data flow equations to compute
$\text{$\overline{\emph{In}}$}_{n}/\text{$\overline{\emph{Out}}$}_{n}$. The
FPMFP solution is a set of values in $\mathcal{L}$, represented by the data
flow variables
$\text{$\overline{\overline{\emph{In}}}$}_{n}/\text{$\overline{\overline{\emph{Out}}}$}_{n}$
(Equation 3 and 4) for every node $n$ in the CFG of the program. They are
computed from
$\text{$\overline{\emph{In}}$}_{n}/\text{$\overline{\emph{Out}}$}_{n}$ using
the following operations.

$\displaystyle\text{$\overline{\overline{\emph{In}}}$}_{n}$
$\displaystyle=\text{$\emph{fold}_{\sqcap}$}(\text{$\overline{\emph{In}}$}_{n})$
(3) $\displaystyle\text{$\overline{\overline{\emph{Out}}}$}_{n}$
$\displaystyle=\text{$\emph{fold}_{\sqcap}$}(\text{$\overline{\emph{Out}}$}_{n})$
(4) $\displaystyle where,\
\text{$\emph{fold}_{\sqcap}$}(\text{$\mathcal{S}$})$
$\displaystyle=\bigsqcap_{\text{$\langle\text{$\mathcal{M}$},d\rangle$}\in\text{$\mathcal{S}$}}d$
(5)

The
$\text{$\overline{\overline{\emph{In}}}$}_{n}/\text{$\overline{\overline{\emph{Out}}}$}_{n}$
values represent the FPMFP solution which represents the data flow information
reaching node $n$ along all CFPs excluding the ones that are known to be
infeasible CFPs and are given as input.

|  Paths and MIPS: • MIPS
$\text{$\mu$}\\!:n_{2}\xrightarrow{e_{3}}n_{4}\xrightarrow{e_{5}}n_{5}\xrightarrow{e6}n_{6}$
• $\emph{start}(\text{$\mu$})=\\{e_{3}\\}$ •
$\emph{inner}(\text{$\mu$})=\\{e_{5}\\}$ •
$\emph{end}(\text{$\mu$})=\\{e_{6}\\}$
Lattices and data flow values •
$\text{$\mathcal{L}$}=\begin{array}[t]{@{}l@{}l}\big{\\{}\\{&a\mapsto[i,j]\\}\mid\\\
&-\infty\leq i\leq j\leq+\infty\big{\\}}\end{array}$ •
$\top=\\{a\mapsto[+\infty,-\infty]\\}$ •
$\text{$\mathcal{U}$}=\\{\text{$\mu$}\\}$ •
$\text{$\overline{\mathcal{L}}$}:\text{$\mathcal{P}(\text{$\mathcal{U}$})$}\rightarrow\text{$\mathcal{L}$}$
•
$\text{$\overline{\emph{In}}$}_{n_{6}}=\big{\\{}\text{$\langle\text{$\\{\\}$},\text{$a\mapsto[5,5]$}\rangle$}\big{\\}}$
•
$\text{$\overline{\overline{\emph{In}}}$}_{n_{6}}=\\{\text{$a\mapsto[5,5]$}\\}$
• $\emph{In}_{n_{6}}=\text{$\\{a\\!\mapsto\\![0,5]\\}$}$ (Figure 2(b))
---
| $a=0$$n_{1}$if $(x\\!\geq\\!0)$$n_{2}$$a=a+5$$n_{3}$print $x$$n_{4}$if
$(x==5)$$n_{5}$assert $(a\ !\\!=0)$$n_{6}$print
x$n_{7}$$e_{1}$[npos=.5,labelsep=.5]{$\langle\text{$\\{\\}$},\text{$a\mapsto[0,0]$}\rangle$}[npos=.35,labelsep=.5]$e_{2}$[npos=.37,labelsep=1]true
[npos=.9,labelsep=.5]{$\langle\text{$\\{\\}$},\text{$a\mapsto[0,0]$}\rangle$}[npos=.3,labelsep=.5]$e_{3}$[npos=.15,labelsep=1]false
[npos=.5,labelsep=.5]{$\langle\\{\text{$\mu$}\\},\text{$a\mapsto[0,0]$}\rangle$}[npos=.6,labelsep=.5]$e_{4}$[npos=.3,labelsep=.5]{$\langle\text{$\\{\\}$},\text{$a\mapsto[5,5]$}\rangle$}[labelsep=1]$e_{5}$[npos=.5,labelsep=1]$\begin{array}[]{@{}l@{}}\big{\\{}\text{$\langle\text{$\\{\\}$},\text{$a\mapsto[5,5]$}\rangle$},\\\
\
\text{$\langle\\{\text{$\mu$}\\},\text{$a\mapsto[0,0]$}\rangle$}\big{\\}}\end{array}$[npos=.4,labelsep=.2]$e_{6}$[npos=.47,labelsep=1]true
[npos=.99,labelsep=.2]{$\langle\text{$\\{\\}$},\text{$a\mapsto[5,5]$}\rangle$}[npos=.4,labelsep=1]$e_{7}$[npos=.17,labelsep=1]false
[npos=.55,labelsep=.5]{$\langle\text{$\\{\\}$},\text{$a\mapsto[0,5]$}\rangle$}[npos=.6,labelsep=.5]$e_{8}$[npos=.25,labelsep=.5]{$\langle\text{$\\{\\}$},\text{$a\mapsto[5,5]$}\rangle$}
---
Figure 6: Computing FPMFP solution for the example of Figure 2. The lifted
data flow analysis computes a set of pairs
$\text{$\overline{\emph{In}}$}_{n}/\text{$\overline{\emph{Out}}$}_{n}$ at each
node $n$ such that a pair $\langle\text{$\mathcal{M}$},d\rangle$, indicates
$d$ flows through each MIPS $m\in\text{$\mathcal{M}$}$. if
$\text{$\mathcal{M}$}=\text{$\\{\\}$}$ then $d$ does not flow through any MIPS
at node $n$. Figure 2 contains single MIPS $\mu$, hence, two pairs are
computed (corresponding to $\\{\text{$\mu$}\\}$ and $\\{\\}$) at each program
point, for brevity, we have only shown pairs where $d\not=\top$.

##  4 Computing the FPMFP Solution

We now illustrate how the data flow equations for computing the FPMFP solution
are derived from that of the MFP specifications of a data flow analysis.
Section 4.1 explains this lifting by defining the data flow equations, node
flow functions, and the meet operator. A key enabler for this lifting is a set
of specially crafted edge flow functions666The edge flow function for an edge
$m\rightarrow n$ uses $\emph{Out}_{m}$ to compute $\emph{In}_{n}$ in a forward
analysis, and vice-versa in a backward analysis. (Section 4.2) that discard
data flow values that reach a program point from infeasible CFPs.

###  4.1 FPMFP Solution Specification

Let $\emph{In}_{n},\emph{Out}_{n}\in\text{$\mathcal{L}$}$ be the data flow
values computed by a data flow analysis at node $n$, where $\mathcal{L}$ is a
meet semi-lattice satisfying the descending chain condition. Additionally, it
contains a $\top$ element—we add an artificial $\top$ value, if there is no
natural $\top$.

Equations 6 and 7 (given below) represent the data flow equations for
computing MFP solution over the CFG of a procedure, say _p_. For simplicity we
assume a forward analysis. _BI_ represents the boundary information reaching
procedure _p_ from its callers. The meet operator $\;\sqcap\;$computes the
_glb_ (greatest lower bound) of elements in $\mathcal{L}$. Function _pred_
$(n)$ returns the predecessor nodes of node _n_ in the CFG of _p_. The node
flow function $\text{\em f}_{n}$ and edge flow function $\text{\em
g}_{\text{$m\rightarrow n$}}$ compute the effect of node $n$ and edge
$m\rightarrow n$ in the CFG respectively. Usually the edge flow functions are
identity.

$\displaystyle\emph{In}_{n}$
$\displaystyle=\begin{cases}\emph{BI}&n=Start_{p}\\\ \bigsqcap\limits_{m\in
pred(n)}\\!\\!\\!\\!\text{\em g}_{\text{$m\rightarrow
n$}}(\emph{Out}_{m})&otherwise\end{cases}$ (6) $\displaystyle\emph{Out}_{n}$
$\displaystyle=\text{\em f}_{n}(\emph{In}_{n})$ (7)

We lift Equations 6 and 7 to define a data flow analysis that computes data
flow variables
$\text{$\overline{\emph{In}}$}_{n},\text{$\overline{\emph{Out}}$}_{n}$ each of
which is a set of pairs of the form $\langle\text{$\mathcal{M}$},d\rangle$. As
explained in Section 3.4,
$\text{$\overline{\emph{In}}$}_{n},\text{$\overline{\emph{Out}}$}_{n}$ are
values in $\overline{\mathcal{L}}$, where
$\text{$\overline{\mathcal{L}}$}:\text{$\mathcal{P}(\text{$\mathcal{U}$})$}\rightarrow\text{$\mathcal{L}$}$
such that $\mathcal{U}$ is the _set of all MIPS_ in the program, and
$\mathcal{L}$ is the lattice of values computed by Equations 6 and 7.

$\displaystyle\text{$\overline{\emph{In}}$}_{n}$
$\displaystyle=\begin{cases}\text{$\overline{\emph{BI}}$}&n=Start_{p}\\\
\bigsqcap\limits_{m\in pred(n)}^{\text{\textemdash}}\overline{\text{\em
g}}_{\text{$m\rightarrow
n$}}(\text{$\overline{\emph{Out}}$}_{m})&otherwise\end{cases}$ (8)
$\displaystyle\text{$\overline{\emph{Out}}$}_{n}$
$\displaystyle=\text{$\overline{f}$}_{n}(\text{$\overline{\emph{In}}$}_{n})$
(9) $\overline{\emph{BI}}$
$\displaystyle=\big{\\{}\text{$\langle\text{$\\{\\}$},\emph{BI}\rangle$}\big{\\}}\
\cup\
\big{\\{}\text{$\langle\text{$\mathcal{M}$},\top\rangle$}\mid\text{$\mathcal{M}$}\not=\text{$\\{\\}$},\text{$\mathcal{M}$}\subseteq\text{$\mathcal{U}$}\big{\\}}$
(10)

The top value that is used for initialization is
$\big{\\{}\text{$\langle\text{$\mathcal{M}$},\top\rangle$}\mid\text{$\mathcal{M}$}\subseteq\text{$\mathcal{U}$}\big{\\}}$.
The node flow function ($\text{$\overline{f}$}_{n}$) is pointwise application
of $\text{\em f}_{n}$ to the pairs in the input set:

$\displaystyle\text{$\overline{f}$}_{n}(\text{$\mathcal{S}$})$
$\displaystyle=\\{\text{$\langle\text{$\mathcal{M}$},\text{\em
f}_{n}(d)\rangle$}\mid\text{$\langle\text{$\mathcal{M}$},d\rangle$}\in\text{$\mathcal{S}$}\\}$
(11)

The meet operator ( $\overline{\text{$\sqcap$}}$ ) is pointwise application of
$\sqcap$ to the pairs that contain the same set of MIPS i.e.,

$\displaystyle\text{$\mathcal{S}$}\text{\;$\overline{\text{$\sqcap$}}$\;}\text{$\mathcal{S}$}^{\prime}=\\{\text{$\langle\text{$\mathcal{M}$},d\text{$\;\sqcap\;$}d^{\prime}\rangle$}\mid\text{$\langle\text{$\mathcal{M}$},d\rangle$}\in\text{$\mathcal{S}$},\text{$\langle\text{$\mathcal{M}$},d^{\prime}\rangle$}\in\text{$\mathcal{S}$}^{\prime}\\}$
(12)

Note that  $\overline{\text{$\sqcap$}}$ is defined for all values in
$\overline{\emph{In}}$/$\overline{\emph{Out}}$ because
$\overline{\emph{In}}$/$\overline{\emph{Out}}$ each contain one pair
corresponding to each subset of $\mathcal{U}$.

If the partial order between elements in $\mathcal{L}$ is $\sqsubseteq$ then
the partial order between elements in $\overline{\mathcal{L}}$ is
$\overline{\sqsubseteq}$ and is given as follows.

$\displaystyle\text{$\mathcal{S}$}\text{$\overline{\sqsubseteq}$}\text{$\mathcal{S}$}^{\prime}\iff(\text{$\langle\text{$\mathcal{M}$},d\rangle$}\in\text{$\mathcal{S}$}\land\text{$\langle\text{$\mathcal{M}$},d^{\prime}\rangle$}\in\text{$\mathcal{S}$}^{\prime}\implies
d\sqsubseteq d^{\prime})$ (13)

###  4.2 Defining the Edge Flow Function

We now formally define the edge flow function $\overline{\text{\em
g}}(\text{$\mathcal{S}$})$. The edge flow function performs the following two
operations over an input pair $\langle\text{$\mathcal{M}$},d\rangle$ in
$\mathcal{S}$.

  1. 1.

If $e$ is end edge of some MIPS in $\mathcal{M}$, then the data flow value $d$
is blocked,

  2. 2.

Otherwise $d$ is associated with a set of MIPS $\mathcal{M}^{\prime}$ where
$\text{$\mathcal{M}^{\prime}$}=\text{$\text{\emph{ext}}(\text{$\mathcal{M}$},e)$}$
(described in Section 3).

The data flow value $d$ from multiple pairs in $\mathcal{S}$ can get
associated with the same set of MIPS $\mathcal{M}^{\prime}$. Hence in the
output pair $\langle\text{$\mathcal{M}$}^{\prime},d^{\prime}\rangle$,
$d^{\prime}$ is effectively computed by taking meet of values of $d$ from
individual pairs
$\text{$\langle\text{$\mathcal{M}$},d\rangle$}\in\text{$\mathcal{S}$}$ where
$\text{$\mathcal{M}^{\prime}$}=\text{$\text{\emph{ext}}(\text{$\mathcal{M}$},e)$}$,
as shown in Equation 15. Let the function _endof_ $(\text{$\mathcal{M}$},e)$
be a boolean function that denotes if $e$ is end edge of some MIPS in
$\mathcal{M}$ or not i.e.,

$\displaystyle\text{\emph{endof}$(\text{$\mathcal{M}$},e)$}=$
$\displaystyle(\exists\text{$\mu$}\in\text{$\mathcal{M}$}.\,e\in\emph{end}(\text{$\mu$}))$
(14)

The first term in the right hand side of the following edge flow function
corresponds to the Item (1) in the list above, while the second term
corresponds to the Item (2) of the list.

$\displaystyle\overline{\text{\em g}}_{e}(\text{$\mathcal{S}$})=$
$\displaystyle\Bigg{\\{}\text{$\langle\text{$\mathcal{M}$}^{\prime},\top\rangle$}\mid\text{$\mathcal{M}$}^{\prime}\subseteq\text{$\mathcal{U}$},\,\text{\emph{endof}$(\text{$\mathcal{M}$}^{\prime},e)$}\Bigg{\\}}$
(15) $\displaystyle\bigcup$
$\displaystyle\Bigg{\\{}\text{$\langle\text{$\mathcal{M}$}^{\prime},d^{\prime}\rangle$}\mid\text{$\mathcal{M}$}^{\prime}\subseteq\text{$\mathcal{U}$},\,\neg\text{\emph{endof}$(\text{$\mathcal{M}$}^{\prime},e)$},\,d^{\prime}=\bigsqcap_{\text{$\langle\text{$\mathcal{M}$},d\rangle$}\in\text{$\mathcal{S}$},\
\text{$\text{\emph{ext}}(\text{$\mathcal{M}$},e)$}=\text{$\mathcal{M}$}^{\prime}}\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!d\
\ \ \ \ \ \ \ \ \ \Bigg{\\}}$

Input Pair: $\langle\text{$\mathcal{M}$},d\rangle$, Output Pair:
$\langle\text{$\mathcal{M}$}^{\prime},d^{\prime}\rangle$$\begin{array}[]{c}$e$\text{
is end edge of some \text{MIPS} in}\\\
\text{$\text{\emph{ext}}(\text{$\mathcal{M}$},e)$}\end{array}$$\text{$\mathcal{M}$}^{\prime}=\text{$\text{\emph{ext}}(\text{$\mathcal{M}$},e)$},\
d^{\prime}=\top$$\text{$\mathcal{M}$}^{\prime}=\text{$\text{\emph{ext}}(\text{$\mathcal{M}$},e)$},\
d^{\prime}=d$[npos=0.9]True [npos=0.9]False  Figure 7: Computing output pair
$\langle\text{$\mathcal{M}$}^{\prime},d^{\prime}\rangle$ from input pair
$\langle\text{$\mathcal{M}$},d\rangle$ in edge flow function
$\overline{\text{\em g}}_{e}$

##  5 Extending the FPMFP Computation to the Inter-procedural Level

In this section, we explain the FPMFP computation for _inter-procedural data
flow analysis_ [21] by describing the call node handling. Specifically, we
formalize the FPMFP computation for the _functional approach_ [21] of inter-
procedural data flow analysis. First, we briefly explain the functional
approach below. Next, we describe the class of _inter-procedural MIPS_ (MIPS
that span across multiple procedures) that we admit for the FPMFP computation
(Section 5.1). Finally, we explain how FPMFP handles call nodes (Section 5.2).

The functional approach consists of two phases. The first phase computes
summaries of procedures in a program, by traversing the callgraph in a bottom-
up order (i.e., summaries for callee procedures are computed before computing
the summaries of the caller procedures). In this phase, a non-recursive
procedure is analyzed once, while a recursive procedure is analyzed multiple
times until a fix-point of procedure summaries is reached. After the summary
computation, a top-down traversal of the call-graph is performed to propagate
data flow values from callers to callees. In this phase, a procedure is
analyzed in an intra-procedural manner because the effect of call nodes is
represented by the summaries of the callee procedures. Therefore, explaining
call node handling and procedure summary computation is sufficient to extend
the FPMFP computation at the inter-procedural level using the functional
approach.

We first state the types of inter-procedural MIPS that we admit (Section 5.1),
followed by the description of call node handling (Section 5.2), and procedure
summary computation (Section 5.3).

###  5.1 Inter-procedural MIPS

An inter-procedural MIPS can span across multiple procedures, unlike an intra-
procedural MIPS that remains inside a single procedure. We allow all intra-
procedural MIPS as input for a FPMFP computation. Additionally, we allow a
specific class of inter-procedural MIPS in the FPMFP computation. We describe
this class of inter-procedural MIPS below.

We categorize an inter-procedural MIPS as shown in Figure 8. Here, we
distinguish between the two types of inter-procedural MIPS depending on if
they start and end in the same procedure or not. We admit a subclass of MIPS
that belong to the former type; this subclass is defined below. We refer these
MIPS as _balanced inter-procedural MIPS_, because each _call edge_ is matched
by a corresponding _call-return edge_.

All inter-procedural MIPS$\begin{array}[]{c}\text{\text{MIPS} that start and
end}\\\ \text{in different
procedures}\end{array}$$\begin{array}[]{c}\text{\text{MIPS} that start and
end}\\\ \text{in the same procedure}\end{array}$Balanced MIPSNon-balanced MIPS
Figure 8: Types of Inter-procedural MIPS

###### Definition 2

(Balanced Inter-procedural MIPS) Let a MIPS $\mu$ be an inter-procedural MIPS
and $\mathcal{V}$ be the set of variables present in the condition on the end
edge of $\mu$. We say $\mu$ is a balanced inter-procedural MIPS if it starts
and ends in the same procedure in a non-recursive manner777For each call edge
there is a corresponding call return edge in the MIPS., and the variables in
$\mathcal{V}$ are not modified inside the procedures called through the
intermediate nodes of $\mu$ 888In general, this may not hold for all inter-
procedural MIPS that start and end in the same procedure. Specifically, there
could exist an inter-procedural MIPS $\mu_{1}$ such that the variables in the
condition on the end edge of $\mu_{1}$ are modified along some paths inside
the procedures called from intermediate nodes of the MIPS..

| $l\\!=\\!2$$S_{p}$$a\\!=\\!0$$n_{1}$use
a$n_{2}$q()$n_{3}$$a\\!>\\!5$$n_{4}$use a$n_{5}$use a$E_{p}$use
a$S_{q}$$l\\!=\\!0$$q_{1}$use
a$E_{q}$[npos=0.5,labelsep=.5]$e_{0}$[npos=0.35,labelsep=0]$e_{2}$[npos=0.5,labelsep=.5]$e_{1}$[npos=0.5,labelsep=.5]$e_{3}$[npos=0.5,labelsep=.5]$e_{4}$[npos=0.5,labelsep=0.2]$e_{5}$[npos=0.7,labelsep=0.2]true[npos=0.53,labelsep=.2]$e_{6}$[npos=0.8,labelsep=.2]false[npos=0.53,labelsep=.2]$e_{7}$[npos=0.43,labelsep=.2]$C_{pq}$[npos=0.53,labelsep=.2]$e_{8}$[npos=0.53,labelsep=.2]$e_{9}$[npos=0.43,labelsep=.2]$R_{qp}$
---
|  |  | $\begin{array}[]{l}\bullet\ \text{MIPS}\ \text{$\mu$}_{1}:e_{2}\rightarrow e_{3}\rightarrow e_{4}\rightarrow e_{5}\end{array}$
---
| $\begin{array}[]{l}\text{The \text{FPMFP} solution}\end{array}$
---
|  Edges |  Sets of MIPS | FPMFP
---|---|---
{} |  {$\text{$\mu$}_{1}$} | $\sqcap$
$e_{3}$ | $l\mapsto[2,2]$ | $l\mapsto[2,2]$ | $l\mapsto[2,2]$
$e_{4}$ | $l\mapsto[0,0]$ | $l\mapsto[0,0]$ | $l\mapsto[0,0]$
$e_{8}$ | $l\mapsto[2,2]$ |  | $l\mapsto[2,2]$
$e_{9}$ | $l\mapsto[0,0]$ |  | $l\mapsto[0,0]$
(a) |  | (b)
Figure 9: Computing FPMFP solution using the functional approach of inter-
procedural analysis: $S,E$ represent the start and end nodes of a procedure
respectively. $C_{pq}$ represents the transfer of control from procedure $p$
to procedure $q$ at a call node and $R_{qp}$ represents the return of control
from $q$ to $p$.

For example in Figure 9, MIPS
$\text{$\mu$}_{1}:n_{1}\xrightarrow{e_{2}}n_{2}\xrightarrow{e_{3}}n_{3}\xrightarrow{e_{4}}n_{4}\xrightarrow{e_{5}}n_{5}$
is a balanced inter-procedural MIPS. A balanced MIPS has the following
interesting property.

> For a balanced MIPS $\mu$ that starts and ends in a procedure $p$, the
> control flow inside the procedures called from intermediate nodes of $\mu$
> can be abstracted out during the FPMFP computation of $p$.

Example 1.  In Figure 9, MIPS
$\text{$\mu$}_{1}:n_{1}\xrightarrow{e_{2}}n_{2}\xrightarrow{e_{3}}n_{3}\xrightarrow{e_{4}}n_{4}\xrightarrow{e_{5}}n_{5}$
goes through the call node $n_{3}$ that calls procedure $q$. However, the
control flow inside $q$ is abstracted out during a FPMFP computation of the
caller procedure $p$. In particular, the edges in procedure $q$ are not marked
as inner edges of $\text{$\mu$}_{1}$ (even though the call $q()$ is part of
$\mu_{1}$).

Henceforth, we assume all inter-procedural MIPS that are input to our analysis
are balanced. We now explain the handling of a call node followed by the
procedure summary computation for bit-vector frameworks.

###  5.2 Handling the Call Nodes

We now describe how the effect of a call node is incorporated in a FPMFP
computation. For this, we assume summaries of all procedures are already
computed. We explain the procedure summary computation for bit-vector
frameworks in Section 5.3.

Figure 10 shows an abstract view of the handling of a call node in a FPMFP
computation. At a a call node $q()$, the output pair
$\langle\text{$\mathcal{M}$}^{\prime},d^{\prime}\rangle$ corresponding to an
input pair $\langle\text{$\mathcal{M}$},d\rangle$ is computed as follows:

  * •

$\text{$\mathcal{M}$}^{\prime}=\text{$\text{\emph{ext}}(\text{$\mathcal{M}$},e_{4})$}$,
as explained in the edge flow function in Section 4.2.

  * •

$d^{\prime}$ is obtained by using $d$ and the procedure summary of $q$.

We now explain the complete effect of a procedure call on the caller and
callee procedures using the example in Figure 9 as running example.

q()Procedure $p$q()q()q()Procedure $q$q()q()$\begin{array}[]{l}\text{compute
$\text{\emph{exitVal}}$ using context $c_{1}$}\\\ \text{and summary of
procedure
$q$}\end{array}$[npos=0.5,labelsep=.5]$e_{1}$[npos=0.5,labelsep=.5]$\langle\text{$\mathcal{M}$},d\rangle$[npos=0.5,labelsep=.5]$e_{4}$[npos=0.5,labelsep=.5]$\langle\text{$\mathcal{M}$}^{\prime},d^{\prime}\rangle$[npos=0.43,labelsep=.2]$(C_{pq},\,d)$[npos=0.95,labelsep=.2]$\begin{array}[]{c}\big{\\{}\text{$\langle\\{\\},d\rangle$}\big{\\}}\cup\big{\\{}\text{$\langle\text{$\mathcal{M}$}_{i},\top\rangle$}\mid\text{$\mathcal{M}$}_{i}\not=\\{\\},\text{$\mathcal{M}$}_{i}\subseteq\text{$\mathcal{U}$}_{q}\big{\\}}\\\
(\text{Context}\
c_{1})\end{array}$[npos=0.53,labelsep=.2]$e_{2}$[npos=0.53,labelsep=.2]$e_{3}$[npos=0.63,labelsep=.2]$(R_{qp},\,d^{\prime})$[npos=0.02,labelsep=1.5]exitVal[npos=0.5,labelsep=.4]$d^{\prime}=\displaystyle\bigsqcap_{\text{$\langle\text{$\mathcal{M}$}_{j},d_{j}\rangle$}\in\emph{exitVal}}\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!d_{j}$
Figure 10: Generic view of call node handling in a FPMFP computation. $C_{pq}$
represents the transfer of control from procedure $p$ to procedure $q$ at a
call node and $R_{qp}$ represents the return of control from $q$ to $p$.
$\text{$\mathcal{U}$}_{q}$ is the set containing all i) intra-procedural MIPS
of q, and ii) balanced inter-procedural MIPS that start and end in $q$.

####  5.2.1 Effect of a Caller Procedure on its Callee Procedure

The boundary information ($\text{$\overline{\emph{BI}}$}_{q}$) for a callee
procedure $q$ is computed by taking the meet of data flow values present at
all call sites of $q$. Next, $\text{$\overline{\emph{BI}}$}_{q}$ is used for
solving the callee procedure $q$. If $C_{q}$ is the set of all call sites of
$q$, and $\text{$\mathcal{U}$}_{q}$ is the set containing 1) intra-procedural
MIPS of $q$, and 2) balanced inter-procedural MIPS that start and end in $q$
then $\text{$\overline{\emph{BI}}$}_{q}$ is computed as follows:

$\displaystyle\text{$\overline{\emph{BI}}$}_{q}$
$\displaystyle=\big{\\{}\text{$\langle\\{\\},x\rangle$}\big{\\}}\cup\big{\\{}\text{$\langle\text{$\mathcal{M}$},\top\rangle$}\mid\text{$\mathcal{M}$}\subseteq\text{$\mathcal{U}$}_{q},\text{$\mathcal{M}$}\not=\\{\\}\big{\\}}\
\text{,where }$ $\displaystyle x$ $\displaystyle=\bigsqcap_{n\in
C_{q}}\text{$\emph{fold}_{\sqcap}$}(\text{$\overline{\emph{In}}$}_{n})$

In Figure 9, the data flow information in $\text{$\overline{\emph{In}}$}_{n3}$
is used to compute the boundary information
($\text{$\overline{\emph{BI}}$}_{q}$) for procedure $q$ i.e.,
$\text{$\overline{\emph{BI}}$}_{q}=\big{\\{}\text{$\langle\\{\\},\text{$l\mapsto[2,2]$}\rangle$}\big{\\}}$.

Moreover, a single boundary is maintained for each procedure. If there is a
change in the data flow information at any call site of a procedure $q$ then
the new boundary $\text{$\overline{\emph{BI}}$}_{q}^{\prime}$ is merged with
the existing boundary information of $q$
($\text{$\overline{\emph{BI}}$}_{q}$). If this leads to a change in the
resulting boundary information of $q$, the procedure $q$ is added to the
worklist for solving. Later, the procedure is solved in an intra-procedural
manner using the new boundary information by the worklist algorithm [21].

####  5.2.2 Effect of a Callee Procedure on its Caller Procedure

The MFP computation (specified by equations 6 and 7 from Section 3.4) defines
the node flow functions ($f_{n}$) for all nodes —including nodes that call
other procedures. In the functional approach of inter-procedural analysis
[21], the call node flow functions are defined using summaries of the
corresponding callee procedures. We use these node flow functions to compute
the effect of a procedure call on the caller procedure using equation 11. For
example, in Figure 9 the MFP analysis defines the node flow function $f_{n3}$
which incorporates the effect of call $q()$ i.e., $q$ replaces the original
value of $l$ by 0. The FPMFP computation uses $f_{n3}$ to compute
$\text{$\overline{f}$}_{n3}$ using equation 11 as follows:

$\displaystyle\text{$\overline{f}$}_{n3}\big{(}\big{\\{}\text{$\langle\\{\\},\text{$l\mapsto[2,2]$}\rangle$},\text{$\langle\\{\text{$\mu$}_{1}\\},\text{$l\mapsto[2,2]$}\rangle$}\big{\\}}\big{)}$
$\displaystyle=\big{\\{}\text{$\langle\\{\\},f_{n3}(\text{$l\mapsto[2,2]$})\rangle$},\text{$\langle\\{\text{$\mu$}_{1}\\},f_{n3}(\text{$l\mapsto[2,2]$})\rangle$}\big{\\}}$
$\displaystyle=\big{\\{}\text{$\langle\\{\\},\text{$l\mapsto[0,0]$}\rangle$},\text{$\langle\\{\text{$\mu$}_{1}\\},\text{$l\mapsto[0,0]$}\rangle$}\big{\\}}$

We elaborate the procedure summary computation for bit-vector frameworks in
Section 5.3

###  5.3 Computing the feasible path GEN and KILL summaries for bit-vector
frameworks

In this section, we state the MFP specifications used for the computation of
procedure summaries for bit-vector frameworks [1]. Next, we lift these
specifications to the corresponding FPMFP specifications.

We use the standard notions of a procedure summary computation for bit-vector
frameworks from [1]. In these frameworks, the node flow functions are of the
following form $\displaystyle
f_{n}(\text{$X$})=(\text{$X$}-\text{$\text{KILL}_{n}$})\cup\text{$\text{GEN}_{n}$}$,
where $\text{GEN}_{n}$ and $\text{KILL}_{n}$ are constant for each node. Hence
the procedure summaries can be constructed by composing individual node flow
functions, independent of the calling context information.

The meet operator in bit-vector frameworks is either the set-union or set-
intersection. For simplicity of exposition, we explain the procedure summary
computation assuming the meet operator is union, henceforth we refer these
data flow problems as _union problems_. We explain the computation for forward
data flow analysis, a dual modeling exists for backward analysis (like live
variables analysis [1]).

Let $\text{GEN}_{n}$, $\text{KILL}_{n}$ be the constant GEN and KILL
information at a non-call node $n$ respectively. Then GEN and KILL summaries
for procedures are computed by solving corresponding GEN and KILL data flow
problems as described below.

Solving the KILL data flow problem. The kill summary for union problems is
computed using $\displaystyle\cap$ as the meet operator, indicating that a
value is added to the kill summary of a procedure iff the value is killed
along all CFPs that reach the exit of the procedure. Initially, kill summary
of all procedures is set to $\top$ which is the top value of the kill data
flow lattice. {} is used as the boundary value. The MFP specifications of a
KILL data flow problem for a procedure $p$ are as follows.

$\text{KIn}_{n}$ $\displaystyle=\begin{cases}\\{\\}&n=Start_{p}\\\
\bigcap\limits_{m\in pred(n)}\text{$\text{KOut}_{m}$}&otherwise\end{cases}$
(16) $\text{KOut}_{n}$
$\displaystyle=\text{$\text{KIn}_{n}$}\cup\text{$\text{\emph{nodekill}($n$)}$}$
(17) nodekill($n$) $\displaystyle=\begin{cases}\text{$\text{KILL}_{n}$}&\ \ \
\ \ \ \text{\emph{n is not a call node}}\\\
\text{$\text{KOut}_{\text{\emph{Exit}${}_{q}$}}$}&\ \ \ \ \ \ \text{\emph{n
calls a procequre q}}\end{cases}$ (18)

nodekill($n$) represents the kill information for the node $n$; the
information is constant if $n$ is not a call node. Otherwise, nodekill($n$) is
the information at the exit the procedure called from $n$. For simplicity of
exposition, we assume at most one procedure can be called from a node (in
practice, more than one procedures can be called from a node through function
pointers, in which case the kill summary of the node is computed by doing
intersection of kill information at exit of all procedures that can be called
from $n$).

Equations 16 to 18 are solved for each procedure chosen in a bottom up
traversal of the call graph of a program. In this, each non-recursive
procedure is solved once, while a recursive procedure is solved multiple times
until the data flow values at all points saturate.

The final value in KOut at the exit of a procedure $p$ is the KILL summary for
procedure $p$, as given by the MFP solution. This summary may include the KILL
information reaching from infeasible CFPs. Hence, to get a more precise
summary, we lift the MFP specifications to the FPMFP specifications for each
procedure $p$ in the program as follows. Let $\text{$\mathcal{U}$}_{p}$ be the
set containing 1) intra-procedural MIPS of $p$, and 2) balanced inter-
procedural MIPS that start and end in procedure $p$.

The FPMFP specifications (obtained by lifting MFP specifications from
equations 16 to 18):

$\overline{\text{KIn}}_{n}$
$\displaystyle=\begin{cases}\text{$\overline{\text{KILLBI}}$}&n=Start_{p}\\\
&\\\ \mathop{\overline{\bigsqcap}}\limits_{m\in pred(n)}\overline{\text{\em
g}}_{m\rightarrow
n}(\text{$\overline{\text{KOut}}_{m}$})&otherwise\end{cases}$ (19)
$\overline{\text{KILLBI}}$
$\displaystyle=\big{\\{}\text{$\langle\\{\\},\\{\\}\rangle$}\big{\\}}\cup\big{\\{}\text{$\langle\text{$\mathcal{M}$},\top\rangle$}\mid\text{$\mathcal{M}$}\subseteq\text{$\mathcal{U}$}_{p},\
\text{$\mathcal{M}$}\not=\\{\\}\big{\\}}$ (20) $\overline{\text{KOut}}_{n}$
$\displaystyle=\big{\\{}\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}\cup\text{$\text{$\overline{\text{\emph{nodekill}}}$}(n)$}\rangle$}\mid\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}\rangle$}\in\text{$\overline{\text{KIn}}_{n}$}\big{\\}}$
(21) $\text{$\overline{\text{\emph{nodekill}}}$}(n)$
$\displaystyle=\begin{cases}\text{$\text{KILL}_{n}$}&\ \ \ \ \ \ \text{\emph{n
is not a call node}}\\\ &\\\
\bigcap\limits_{\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}\rangle$}\in\text{$\overline{\text{KOut}}_{\text{\emph{Exit}${}_{q}$}}$}}\text{$\mathcal{D}$}&\
\ \ \ \ \ \text{\emph{n calls a procequre q}}\end{cases}$ (22)

The $\overline{\sqcap}$ does a point-wise intersection of the kill data flow
values in the input set of pairs as follows.

$\displaystyle\displaystyle\text{$\mathcal{S}_{1}$}\overline{\sqcap}\text{$\mathcal{S}_{2}$}$
$\displaystyle=\big{\\{}\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}_{1}\cap\text{$\mathcal{D}$}_{2}\rangle$}\mid\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}_{1}\rangle$}\in\text{$\mathcal{S}_{1}$},\
\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}_{2}\rangle$}\in\text{$\mathcal{S}_{2}$}\big{\\}}$
(23)

The final kill summary of a procedure $p$ is computed by doing intersection of
the data flow values at the exit of $p$ i.e.,

KSUMp
$\displaystyle=\bigcap\limits_{\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}\rangle$}\in\text{$\overline{\text{KOut}}_{\text{\emph{Exit}${}_{p}$}}$}}\text{$\mathcal{D}$}$
(24)

We now explain the GEN summary computation of a procedure below.

Solving the GEN data flow problem. The GEN summary for union problems is
computed using $\cup$ as the meet operator, indicating that a data flow value
is added to GEN summary if it is generated along atleast one CFP that reaches
the exit of the procedure. Next, $\\{\\}$ is used as the boundary value. The
corresponding MFP specifications are as follows.

The MFP specifications:

$\text{GIn}_{n}$ $\displaystyle=\begin{cases}\\{\\}&n=Start_{p}\\\ &\\\
\bigcup\limits_{m\in pred(n)}\text{$\text{GOut}_{m}$}&otherwise\end{cases}$
(25) $\text{GOut}_{n}$
$\displaystyle=(\text{$\text{GIn}_{n}$}-\text{$\text{\emph{nodekill}($n$)}$})\cup\text{$\text{\emph{nodegen}}(n)$}$
(26) $\text{\emph{nodegen}}(n)$
$\displaystyle=\begin{cases}\text{$\text{GEN}_{n}$}&\ \ \ \ \ \ \text{\emph{n
is not a call node}}\\\ \text{$\text{GOut}_{\text{\emph{Exit}${}_{q}$}}$}&\ \
\ \ \ \ \text{\emph{n calls a procedure q}}\end{cases}$ (27)

Based on these MFP specifications, we derive the FPMFP specifications for each
procedure $p$ in the program as follows. Let $\text{$\mathcal{U}$}_{p}$ be the
set containing 1) intra-procedural MIPS of $p$, and 2) balanced inter-
procedural MIPS that start and end in $p$.

The FPMFP specifications:

$\overline{\text{GIn}}_{n}$
$\displaystyle=\begin{cases}\big{\\{}\text{$\langle\text{$\mathcal{M}$},\\{\\}\rangle$}\mid\text{$\mathcal{M}$}\subseteq\text{$\mathcal{U}$}_{p}\big{\\}}&n=Start_{p}\\\
&\\\ \displaystyle\mathop{\overline{\bigsqcap}^{\prime}}\limits_{m\in
pred(n)}\overline{\text{\em g}}_{m\rightarrow
n}(\text{$\overline{\text{GOut}}_{m}$})&otherwise\end{cases}$ (28)
$\overline{\text{GOut}}_{n}$
$\displaystyle=\big{\\{}\text{$\langle\text{$\mathcal{M}$},(\text{$\mathcal{D}$}-\text{$\text{$\overline{\text{\emph{nodekill}}}$}(n)$})\cup\text{$\text{$\overline{\text{\emph{nodegen}}}$}(n)$}\rangle$}\mid\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}\rangle$}\in\text{$\overline{\text{GIn}}_{n}$}\big{\\}}$
(29) $\text{$\overline{\text{\emph{nodegen}}}$}(n)$
$\displaystyle=\begin{cases}\text{$\text{GEN}_{n}$}&\ \ \ \ \ \ \text{\emph{n
is not a call node}}\\\ &\\\
\displaystyle\bigcup_{\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}\rangle$}\in\text{$\overline{\text{GOut}}_{Exit_{q}}$}}\text{$\mathcal{D}$}&\
\ \ \ \ \ \text{\emph{n calls a procedure q}}\end{cases}$ (30)

$\overline{\sqcap}^{\prime}$ does a point-wise union of data flow values in
the set of input pairs as follows.

$\displaystyle\displaystyle\text{$\mathcal{S}_{1}$}\overline{\sqcap}^{\prime}\text{$\mathcal{S}_{2}$}$
$\displaystyle=\big{\\{}\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}_{1}\cup\text{$\mathcal{D}$}_{2}\rangle$}\mid\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}_{1}\rangle$}\in\text{$\mathcal{S}_{1}$},\
\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}_{2}\rangle$}\in\text{$\mathcal{S}_{2}$}\big{\\}}$
(31)

The final gen summary of a procedure $p$ is computed by doing the union of
data flow values at the exit of the procedure $p$ i.e.,

GSUMp
$\displaystyle=\bigcup_{\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}\rangle$}\in\text{$\overline{\text{GOut}}_{Exit_{p}}$}}\text{$\mathcal{D}$}$
(32)

Substituting GEN and KILL summaries to compute the effect of procedure calls.

The GEN and KILL summaries are computed for all procedures using the
corresponding constant boundary values. We call this summary computation
phase. Later, these GEN and KILL summaries are used to compute the effect of
procedure $p$ at all callsites of $p$ during the actual FPMFP computation
(using actual boundary values) as follows: Let $n:p()$ be a callsite of $p$
then

$\displaystyle
f_{n}(\text{$X$})=(\text{$X$}-\text{KSUM${}_{p}$})\cup\text{GSUM${}_{p}$}$
(33)
$\displaystyle\text{$\overline{f}$}_{n}(\text{$\mathcal{S}$})=\\{\text{$\langle\text{$\mathcal{M}$},f_{n}(\text{$\mathcal{D}$})\rangle$}\mid\text{$\langle\text{$\mathcal{M}$},\text{$\mathcal{D}$}\rangle$}\in\text{$\mathcal{S}$}\\}$
(34)

All Optimizations$\begin{array}[]{c}\text{Optimizations that involve}\\\
\text{ignoring a \text{pair}}\end{array}$$\begin{array}[]{c}\text{Optimization
3}\\\ \text{(Section 6.3)}\end{array}$$\begin{array}[]{c}\text{Optimizations
that involve}\\\ \text{merging
\text{pairs}}\end{array}$$\begin{array}[]{c}\text{Optimization 1}\\\
\text{(Section 6.1)}\end{array}$$\begin{array}[]{c}\text{Optimization 2}\\\
\text{(Section 6.2)}\end{array}$ Figure 11: Optimizations for scalability of
the FPMFP computation: The leaf nodes describe a particular optimization, and
rest of the nodes describe the type of the optimization.

##  6 Optimizations for Computing FPMFP Solutions

We now describe few optimizations that improve the scalability of a FPMFP
computation. First, we explicate a relation between efficiency of the FPMFP
computation and the number of pairs in the FPMFP computation. Next, we propose
ideas to reduce the number of pairs. Our empirical data shows the reduction
obtained is significant.

As evident from equations 8 to 15, the efficiency of a FPMFP computation is
inversely proportional to the number of pairs. Theoretically, the number of
pairs needed is exponential in the number of MIPS in $\mathcal{U}$ (set of all
MIPS) because a different pair is created corresponding to each subset of
$\mathcal{U}$. However, at any program point the number of pairs that are
evaluated is bounded by $|\text{$\mathcal{U}$}|+1$ (explained in Section 6.4).
Below, we describe the ideas to reduce the number of pairs by either merging
them or ignoring the ones that have no effect on the final FPMFP solution.
These optimizations are shown in Figure 11. We describe each of these
optimizations below.

###  6.1 Merging Pairs

We now describe an optimization that allows us to merge some of the pairs
present at a program point. We observed that a large class of MIPS found in
our benchmarks were satisfying the following property.

> $\mathcal{P}$: The condition on the end edge of a MIPS $\mu$ evaluates to
> _false_ at the start edge of $\mu$, and the variables present in the
> condition are not modified at the intermediate nodes of $\mu$.

We observe the following peculiarity of MIPS that satisfy $\mathcal{P}$.

###### Observation 6.1

We do not need to distinguish between MIPS that satisfy $\mathcal{P}$ and have
the same end edge, because the condition on the end edge does not hold at the
starts of these MIPS and data flow values associated with them are blocked at
the same end edge. Hence, the data flow values associated with them can be
merged.

We support Observation 6.1 with a proof in Section 10.4. Observation 6.1
allows us to merge pairs at a program point as described below.

|  |  Sets of MIPS | FPMFP
---|---|---|---
|  | {} | $\\{\text{$\mu$}_{1}\\}$ | $\\{\text{$\mu$}_{2}\\}$ | $\\{\text{$\mu$}_{1},\text{$\mu$}_{2}\\}$ | $\sqcap$
Edges | $e_{3}$ |  $z\mapsto[1,1]$ | $\top$ | $\top$ | $\top$ |  $z\mapsto[1,1]$
$e_{5}$ | $\top$ | $z\mapsto[0,0]$ | $\top$ | $\top$ | $z\mapsto[0,0]$
$e_{6}$ | $\top$ | $\top$ |  $z\mapsto[2,2]$ | $\top$ |  $z\mapsto[2,2]$
$e_{7}$ |  $z\mapsto[1,1]$ | $z\mapsto[0,0]$ |  $z\mapsto[2,2]$ | $\top$ |  $z\mapsto[0,2]$
| $e_{9}$ |  $z\mapsto[1,1]$ | $\top$ | $\top$ | $\top$ |  $z\mapsto[1,1]$
Table 4: The FPMFP solution for example in Figure 12a. For brevity, only
values of z are shown.

_Optimization 1._ We merge two pairs $\langle\text{$\mathcal{M}$},d\rangle$
and $\langle\text{$\mathcal{M}$}^{\prime},d^{\prime}\rangle$ into a single
pair $\langle\text{$\mathcal{M}$}\cup\text{$\mathcal{M}$}^{\prime},d\sqcap
d^{\prime}\rangle$ _iff_ the sets $\mathcal{M}$ and
$\text{$\mathcal{M}$}^{\prime}$ are _end edge equivalent_ (denoted by
$\overset{\mathrm{\emph{end}}}{=}\ $) as defined below:

$\displaystyle\text{$\mathcal{M}$}\overset{\mathrm{\emph{end}}}{=}\text{$\mathcal{M}$}^{\prime}\Leftrightarrow\bigcup_{\text{$\mu$}\in\text{$\mathcal{M}$}}\emph{end}(\text{$\mu$})=\bigcup_{\text{$\mu$}^{\prime}\in\text{$\mathcal{M}$}^{\prime}}\emph{end}(\text{$\mu$}^{\prime})$
(35)

The FPMFP computation for the example in Figure 12 is shown in Table 4. Four
pairs are computed at each edge corresponding to each subset of
$\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$. However, MIPS $\mu_{1}$, $\mu_{2}$
have the same end edge $e_{9}$ and hence the following sets are end edge
equivalent: $\\{\text{$\mu_{1}$}\\}$, $\\{\text{$\mu_{2}$}\\}$,
$\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$. We obtain the FPMFP solution by
merging these pairs as shown in Figure 12b where only two pairs are maintained
at each edge.

| _read a,b; z=1; d=1_ _$switch(b)$__a=3;z=0_ _a=5;z=2_ _print a_ _$a
>0$_return -1return $a/z$[labelsep=.2]$e_{1}$[labelsep=.2]case 2
[labelsep=.5]$e_{2}$[labelsep=.2] default
[npos=.6,labelsep=.5]$e_{3}$[labelsep=.2]case 1
[labelsep=.5]$e_{4}$[labelsep=.5]$e_{5}$[labelsep=.1]$e_{6}$[labelsep=.1]$e_{7}$[labelsep=.1]$e_{8}$true
[labelsep=.1]$e_{9}$false
---
|  | $\begin{array}[]{l}\text{Paths and \text{MIPS}:}\\\ \bullet\ \text{MIPS}\ \text{$\mu$}_{1}:e_{5}\rightarrow e_{7}\rightarrow e_{9}\\\ \bullet\ \text{MIPS}\ \text{$\mu$}_{2}:e_{6}\rightarrow e_{7}\rightarrow e_{9}\\\ \bullet\ \text{$\\{\text{$\mu_{1}$}\\}$}\overset{\mathrm{\emph{end}}}{=}\text{$\\{\text{$\mu_{2}$}\\}$}\overset{\mathrm{\emph{end}}}{=}\text{$\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$}\\\ \end{array}$
---
| $\begin{array}[]{l}\text{The \text{FPMFP} solution: \text{MIPS}
$\text{$\\{\text{$\mu_{1}$}\\}$}$, $\text{$\\{\text{$\mu_{2}$}\\}$}$, }\\\
\text{and \text{$\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$} are end edge
equivalent so the }\\\ \text{corresponding data flow values are associated
}\\\ \text{with $\text{$\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$}$ only. For
brevity, computation}\\\ \text{ of values for z is shown only. }\\\
\end{array}$
---
|  |  |  Sets of MIPS | FPMFP
---|---|---|---
|  | {} | $\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$ | $\sqcap$
Edges | $e_{3}$ |  $z\mapsto[1,1]$ | $\top$ |  $z\mapsto[1,1]$
$e_{5}$ | $\top$ | $z\mapsto[0,0]$ | $z\mapsto[0,0]$
$e_{6}$ | $\top$ |  $z\mapsto[2,2]$ |  $z\mapsto[2,2]$
$e_{7}$ |  $z\mapsto[1,1]$ |  $z\mapsto[0,2]$ |  $z\mapsto[0,2]$
$e_{9}$ |  $z\mapsto[1,1]$ | $\top$ |  $z\mapsto[1,1]$
(a) | (b)
Figure 12: Equivalent MIPS

###  6.2 Removing Duplicate Data Flow Values Across Pairs

In this section, we explain how the same data flow values can appear in more
than one pairs at a program point. Further, we propose an idea to remove this
duplication of values while retaining the precision and soundness of the FPMFP
solution. This optimization has helped us to improve the scalability of our
approach to 150KLOC, whereas without this optimization scalability was 73KLOC.

In a FPMFP computation, at an edge $e$, two pairs can contain the same data
flow value $d$ iff $d$ reaches $e$ along two or more CFPs (because in this
case $d$ may flow through two different MIPS which are not related by CPO
relation). In such case, if one of the CFP is a feasible CFP then the two
pairs can be merged into one as illustrated in Example 6.2 below.

Example 1.  For example in Figure 13, the data flow value $d\mapsto[1,1]$
flows through MIPS $\mu$, hence it is associated with $\\{\text{$\mu$}\\}$ at
edges in $\mu$ i.e., $e_{3},e_{5},e_{7}$. Next, the value associated with
$\\{\text{$\mu$}\\}$ is blocked at the end edge $e_{7}$ of $\mu$, because this
value is reaching along the infeasible CFP that contains $\mu$ i.e.,
$e_{0}\rightarrow e_{1}\rightarrow e_{3}\rightarrow e_{5}\rightarrow e_{7}$.
On the other hand, $d\mapsto[1,1]$ also reaches $e_{7}$ along the following
CFP that is not infeasible $\sigma:e_{0}\rightarrow e_{2}\rightarrow
e_{4}\rightarrow e_{6}\rightarrow e_{7}$, hence $d\mapsto[1,1]$ is also
associated with {}. Effectively, $d\mapsto[1,1]$ is included at $e_{7}$ in the
FPMFP solution. In such case, we can get the same FPMFP solution without
associating $d\mapsto[1,1]$ with $\\{\text{$\mu$}\\}$ at $e_{5},e_{7}$ as
shown in Table 5. Observe that the corresponding FPMFP solution is same to
that in Figure 13.

We use the following general criteria to treat the pairs that contain the same
data flow value at a program point.

> If a data flow value $d$ reaches the end edge of a MIPS $\mu$ along a
> feasible CFP then $d$ need not be associated with $\mu$, because even if $d$
> is blocked within $\mu$, it reaches along the feasible CFP and hence its
> association with $\mu$ is redundant.

|  | Sets of MIPS | FPMFP
---|---|---|---
|  | {} | {$\text{$\mu$}_{1}$} | $\sqcap$
Edges | $e_{3}$ | $\top$ | $d\mapsto[1,1]$ | $d\mapsto[1,1]$
$e_{5}$ | $d\mapsto[1,1]$ | $\top$ | $d\mapsto[1,1]$
$e_{6}$ | $d\mapsto[1,1]$ | $\top$ | $d\mapsto[1,1]$
$e_{7}$ | $d\mapsto[1,1]$ | $\top$ | $d\mapsto[1,1]$
Table 5: Removing Duplicates

To find out if a data flow value reaches the end edge of a MIPS along a
feasible CFP, we define the _contains-suffix-of_ relation below.

###### Definition 3

(Contains-suffix-of (CSO)) For a MIPS $\mu$ and an edge $e$ in $\mu$, let
_suffix_ $(\text{$\mu$},e)$ be the sub-segment of $\mu$ from $e$ to
$\emph{end}(\text{$\mu$})$. Then, we say that “MIPS $\mu_{1}$ contains-suffix-
of MIPS $\mu_{2}$ at $e$”, iff $\mu_{1}$ contains _suffix_
$(\text{$\mu_{2}$},e)$.

$\text{\emph{cso}}_{e}(\text{$\mu_{1}$})$
$\displaystyle=\\{\text{$\mu_{2}$}\mid\text{$\mu_{2}$}\in\text{$\mathcal{U}$},\
\text{$\mu_{1}$}\ \text{contains}\
\text{\emph{suffix}$(\text{$\mu_{2}$},e)$}\\}$ (36)

Observe that the CSO is a reflexive relation, and a dual of the CPO relation
defined in section 3.3 in the following sense: at an edge $e$, $\mu_{1}$ CPO
$\mu_{2}$ means $\mu_{1}$ and $\mu_{2}$ follow the same CFP till edge $e$
whereas, $\mu_{1}$ CSO $\mu_{2}$ means $\mu_{1}$ and $\mu_{2}$ follow the same
CFP after edge $e$ however they may or may not follow the same CFP before edge
$e$.

The CSO relation has the following properties.

  * •

_Property 1_ : if a MIPS $\mu_{1}$ contains suffix of a MIPS $\mu_{2}$ at an
edge $e$, then the data flow value associated with $\mu_{2}$ is blocked at or
before reaching the end of $\mu_{1}$ (because after $e$, $\mu_{1}$ and
$\mu_{2}$ follow the same CFP on which $\mu_{2}$ ends at or before the end of
$\mu_{1}$).

Example 2.  For example in Figure 14a, $\mu_{1}$ CSO $\mu_{2}$ at $e_{5}$.
Hence, $l\mapsto[0,0]$ is blocked at $e_{6}$ in pair
$\langle\\{\text{$\mu_{2}$}\\},\text{$l\mapsto[0,0]$}\rangle$ as well as at
$e_{7}$ in $\langle\\{\text{$\mu_{1}$}\\},\text{$l\mapsto[0,0]$}\rangle$. Thus
$l\mapsto[0,0]$ does not reach $e_{7}$.

  * •

_Property 2_ : if two pairs $\langle\text{$\mathcal{M}_{1}$},d\rangle$ and
$\langle\text{$\text{$\mathcal{M}$}_{2}$},d\rangle$ contain the same data flow
value $d$ at an edge $e$, and $d$ is not killed along a MIPS $\mu_{2}$ in
$\text{$\mathcal{M}$}_{2}$ then the following holds.

> $d$ reaches the end of $\mu_{2}$ along atleast one feasible CFP that passes
> through $e$, provided that $\mu_{2}$ does not contain suffix of any MIPS in
> $\mathcal{M}_{1}$ at e. Specifically in this case, the data flow value $d$
> from pair $\langle\text{$\mathcal{M}_{1}$},d\rangle$ reaches the end of
> $\mu_{2}$ (proof in Section 10.4). Hence the association of $d$ with
> $\mu_{2}$ can be discarded.

Example 3.  For example in Figure 14a, $\mu_{2}$ does not contain suffix of
$\mu_{1}$. Further, $l\mapsto[0,0]$ flows through $\mu_{1}$ and $\mu_{2}$ and
is blocked at corresponding end edges as shown in Figure 14b. However,
$l\mapsto[0,0]$ is included in the FPMFP solution at the end edge $e_{6}$ of
$\mu_{2}$ because it reaches along the following feasible CFP:
$e_{0}\rightarrow e_{3}\rightarrow e_{5}\rightarrow e_{6}\rightarrow e_{9}$.

In such case, we can get the same FPMFP solution without maintaining an
association with $\mu_{2}$.

Based on the above properties, we now formally describe the following criteria
to merge two pairs that have the same data flow value.

_Optimization 2._ At an edge e, we shift the common data flow value $d$ from
two pairs $\langle\text{$\mathcal{M}$}_{1},d\rangle$ and
$\langle\text{$\mathcal{M}$}_{2},d\rangle$ to a single pair
$\langle\text{$\mathcal{M}$}_{3},d\rangle$ where $\text{$\mathcal{M}$}_{3}$
contains only those MIPS in
$\text{$\mathcal{M}_{1}$}\cup\text{$\text{$\mathcal{M}$}_{2}$}$ that contain
suffix of at least one MIPS in $\mathcal{M}_{1}$ and at least one MIPS in
$\text{$\mathcal{M}$}_{2}$ 999Note that CSO is a reflexive relation, hence if
$\text{$\mu_{1}$}\in\text{$\mathcal{M}_{1}$}$ then “$\mu_{1}$ contains suffix
of at least one MIPS in $\mathcal{M}_{1}$” is trivially true. i.e.,

$\displaystyle\text{$\mathcal{M}$}_{3}=$
$\displaystyle\\{\text{$\mu_{1}$}\mid\text{$\mu_{1}$}\in\text{$\mathcal{M}$}_{1},\
\exists\text{$\mu_{2}$}\in\text{$\mathcal{M}$}_{2}.\,\text{$\mu_{1}$}\
\text{$\text{CSO}$}\ \text{$\mu_{2}$}\text{ at }e\\}$ $\displaystyle\cup$
$\displaystyle\\{\text{$\mu_{2}$}\mid\text{$\mu_{2}$}\in\text{$\mathcal{M}$}_{2},\
\exists\text{$\mu_{1}$}\in\text{$\mathcal{M}$}_{1}.\,\text{$\mu_{2}$}\
\text{$\text{CSO}$}\ \text{$\mu_{1}$}\text{ at }e\\}$

Example 4.  For example in Figure 14a, at edges $e_{5}$ and $e_{6}$ $\mu_{1}$
CSO $\mu_{2}$, hence we associate $l\mapsto[0,0]$ with $\mu_{1}$ only as shown
in Figure 14c. Observe the corresponding FPMFP solution is same as in Figure
14b.

d=1$c\\!>\\!5$$a\\!=\\!0$$b\\!>\\!5$read a$a\\!>\\!5$use ause
a[npos=0.4,labelsep=0]$e_{0}$[npos=0.85,labelsep=0.2]false[npos=0.4,labelsep=0]$e_{1}$[npos=0.45,labelsep=0.2]true[npos=0.2,labelsep=0]$e_{2}$[npos=0.8,labelsep=2]$\big{\\{}\text{$\langle\\{\\},\text{$d\mapsto[1,1]$}\rangle$}\big{\\}}$[doubleline=true,
npos=0.4,labelsep=.5]$e_{3}$[labelsep=1,npos=0.2]$\big{\\{}\text{$\langle\text{$\\{\text{$\mu$}\\}$},\text{$d\mapsto[1,1]$}\rangle$}\big{\\}}$[npos=0.4,labelsep=0]$e_{4}$[labelsep=1,npos=0.9]$\big{\\{}\text{$\langle\\{\\},\text{$d\mapsto[1,1]$}\rangle$}\big{\\}}$[npos=0.45,labelsep=0]$e_{6}$[labelsep=1,npos=0.4]$\big{\\{}\text{$\langle\\{\\},\text{$d\mapsto[1,1]$}\rangle$}\big{\\}}$[labelsep=1,npos=0.6]$\big{\\{}\text{$\langle\\{\\},\text{$d\mapsto[1,1]$}\rangle$},\
\text{$\langle\text{$\\{\text{$\mu$}\\}$},\text{$d\mapsto[1,1]$}\rangle$}\big{\\}}$[npos=0.3,labelsep=.5]$e_{5}$[npos=0.3,labelsep=.5]$e_{7}$[npos=0.85,labelsep=0.2]true[labelsep=2,npos=0.6]$\big{\\{}\text{$\langle\\{\\},\text{$d\mapsto[1,1]$}\rangle$},\
\text{$\langle\text{$\\{\text{$\mu$}\\}$},\text{\sout{\text{$d\mapsto[1,1]$}}}\rangle$}\big{\\}}$[npos=0.4,labelsep=0.2]$e_{8}$[npos=0.85,labelsep=0.2]false[labelsep=5,npos=0.6]$\big{\\{}\text{$\langle\\{\\},\text{$d\mapsto[1,1]$}\rangle$}\big{\\}}$
Figure 13: An example illustrating the FPMFP computation. The path segment
$\text{$\mu$}:e_{3}\rightarrow e_{5}\rightarrow e_{7}$ is a MIPS. For
simplicity, we have only shown value range of variable d, and pairs
$\langle\text{$\mathcal{M}$},x\rangle$ where $x\not=\top$.

Example 5.  For example in Figure 15a, the data flow value $l\mapsto[0,0]$
flows though two MIPS $\mu_{1}$ and $\mu_{2}$. Further neither $\mu_{1}$ CSO
$\mu_{2}$ nor $\mu_{2}$ CSO $\mu_{1}$, hence $l\mapsto[0,0]$ reaches
$\emph{end}(\text{$\mu_{1}$})$ and $\emph{end}(\text{$\mu_{2}$})$ along the
following feasible CFPs $\sigma_{1}$ and $\sigma_{2}$ respectively,
$\sigma_{1}:e_{0}\rightarrow e_{1}\rightarrow e_{3}\rightarrow
e_{4}\rightarrow e_{7}$, $\sigma_{2}:e_{0}\rightarrow e_{2}\rightarrow
e_{4}\rightarrow e_{5}$. Hence, $l\mapsto[0,0]$ is included in the FPMFP
solution at edges $e_{7}$ and $e_{5}$ as shown in Figure 15b. We obtain the
same FPMFP solution without associating $l\mapsto[0,0]$ with $\mu_{1}$ or
$\mu_{2}$ as shown in Figure 15c.

| _if $(l==0)$__if $(d==2)$__c=2, read d_ _print l_ _if $(c==0)$__if
$(d==2)$__print l_ _exit_[npos=.4,labelsep=.2]$e_{0}$[npos=.7,labelsep=.5]true
[npos=.5,labelsep=.2]$e_{1}$[npos=.6,labelsep=.5]false
[npos=.4,labelsep=.2]$e_{2}$[npos=.7,labelsep=.5]true
[npos=.5,labelsep=.2]false
[npos=.35,labelsep=.5]$e_{3}$[npos=.6,labelsep=.5]$e_{4}$[npos=.6,labelsep=.5]$e_{5}$[npos=.4,labelsep=.1]$e_{6}$[npos=.7,labelsep=.1]true
[npos=.3,labelsep=.1]$e_{7}$[npos=.45,labelsep=.01,nrot=0]true
[npos=.5,labelsep=.2]$e_{10}$[npos=.35,labelsep=.5]$e_{8}$[npos=.5,labelsep=.5]false
[npos=.45,labelsep=.5]$e_{9}$[npos=.5,labelsep=-1.5] false
---
|  | $\begin{array}[]{l}\text{Paths and \text{MIPS}:}\\\ \bullet\ \text{MIPS}\ \text{$\mu$}_{1}:e_{3}\rightarrow e_{5}\rightarrow e_{6}\rightarrow e_{7}(\text{marked in blue})\\\ \bullet\ \emph{start}(\text{$\mu$}_{1})=\\{e_{3}\\},\ \emph{inner}(\text{$\mu$}_{1})=\\{e_{5},e_{6}\\},\\\ \bullet\ \emph{end}(\text{$\mu$}_{1})=\\{e_{7}\\}\\\ \bullet\ \text{MIPS}\ \text{$\mu$}_{2}:e_{4}\rightarrow e_{5}\rightarrow e_{6}(\text{marked in red})\\\ \bullet\ \emph{start}(\text{$\mu$}_{2})=\\{e_{4}\\},\ \emph{inner}(\text{$\mu$}_{2})=\\{e_{5}\\},\ \emph{end}(\text{$\mu$}_{2})=\\{e_{6}\\}\\\ \bullet\ \text{At }e_{5}\text{ and }e_{6},\ \text{$\mu_{1}$}\ \text{$\text{CSO}$}\ \text{$\mu_{2}$}\end{array}$
---
|   Edges  |  Sets of MIPS | FPMFP
---|---|---
{} | $\\{\text{$\mu$}_{1}\\}$ | $\\{\text{$\mu$}_{2}\\}$ | $\\{\text{$\mu$}_{1},\text{$\mu$}_{2}\\}$ | $\sqcap$
$e_{1}$ | $l\mapsto[1,\infty]$ | $\top$ | $\top$ | $\top$ | $l\mapsto[1,\infty]$
$e_{3}$ | $\top$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $l\mapsto[0,0]$
$e_{4}$ | $\top$ | $\top$ | $l\mapsto[0,0]$ | $\top$ | $l\mapsto[0,0]$
$e_{5}$ | $l\mapsto[1,\infty]$ | $l\mapsto[0,0]$ | $l\mapsto[0,0]$ | $\top$ | $l\mapsto[0,\infty]$
$e_{6}$ | $l\mapsto[1,\infty]$ | $l\mapsto[0,0]$ | $l\mapsto[0,0]$ | $\top$ | $l\mapsto[0,\infty]$
$e_{7}$ | $l\mapsto[1,\infty]$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $l\mapsto[1,\infty]$
(b)
|   Edges  |  Sets of MIPS | FPMFP
---|---|---
{} | $\\{\text{$\mu$}_{1}\\}$ | $\\{\text{$\mu$}_{2}\\}$ | $\\{\text{$\mu$}_{1},\text{$\mu$}_{2}\\}$ | $\sqcap$
$e_{1}$ | $l\mapsto[1,\infty]$ | $\top$ | $\top$ | $\top$ | $l\mapsto[1,\infty]$
$e_{3}$ | $\top$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $l\mapsto[0,0]$
$e_{4}$ | $\top$ | $\top$ | $l\mapsto[0,0]$ | $\top$ | $l\mapsto[0,0]$
$e_{5}$ | $l\mapsto[1,\infty]$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $l\mapsto[0,\infty]$
$e_{6}$ | $l\mapsto[1,\infty]$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $l\mapsto[0,\infty]$
$e_{7}$ | $l\mapsto[1,\infty]$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $l\mapsto[1,\infty]$
(a) | (c)
Figure 14: Illustrating pairs that have the same data flow value and have CSO relation between constituent MIPS. Here $l$ is an unsigned int variable. | _if_ $(c\,!\\!=0)$_l=0_ _c=2_ _print l_ _if $(c==0)$__assert $(l!\\!=0)$__exit_[npos=.4,labelsep=.2]$e_{0}$[npos=.4,labelsep=.2]$e_{1}$[npos=.7,labelsep=.5]true [npos=.5,labelsep=.2]false [npos=.35,labelsep=.5]$e_{2}$[npos=.6,labelsep=.5]$e_{3}$[npos=.6,labelsep=.5]$e_{4}$[npos=.4,labelsep=.1]$e_{5}$[npos=.7,labelsep=.1]true [npos=.35,labelsep=.5]$e_{7}$[npos=.5,labelsep=.5]false [npos=.6,labelsep=.5]$e_{6}$
---
|  | $\begin{array}[]{l}\text{Paths and \text{MIPS}:}\\\ \bullet\ \text{MIPS}\ \text{$\mu$}_{1}:e_{2}\rightarrow e_{4}\rightarrow e_{7}\ (\text{marked in blue})\\\ \bullet\ \text{MIPS}\ \text{$\mu$}_{2}:e_{3}\rightarrow e_{4}\rightarrow e_{5}\ (\text{marked in red})\\\ \bullet\ \emph{start}(\text{$\mu$}_{1})=e_{2}\\\ \bullet\ \emph{start}(\text{$\mu$}_{2})=e_{3}\\\ \bullet\ \emph{inner}(\text{$\mu$}_{1})=\emph{inner}(\text{$\mu$}_{2})=e_{4}\\\ \bullet\ \emph{end}(\text{$\mu$}_{1})=e_{7},\emph{end}(\text{$\mu$}_{2})=e_{5}\\\ \end{array}$
---
|  Edges |  Sets of MIPS | FPMFP
---|---|---
{} | $\\{\text{$\mu$}_{1}\\}$ | $\\{\text{$\mu$}_{2}\\}$ | $\\{\text{$\mu$}_{1},\text{$\mu$}_{2}\\}$ | $\sqcap$
$e_{2}$ | $\top$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $l\mapsto[0,0]$
$e_{3}$ | $\top$ | $\top$ | $l\mapsto[0,0]$ | $\top$ | $l\mapsto[0,0]$
$e_{4}$ | $\top$ | $l\mapsto[0,0]$ | $l\mapsto[0,0]$ | $\top$ | $l\mapsto[0,0]$
$e_{5}$ | $l\mapsto[0,0]$ | $\top$ | $l\mapsto[0,0]$ | $\top$ | $l\mapsto[0,0]$
$e_{7}$ | $l\mapsto[0,0]$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $l\mapsto[0,0]$
(b)
|  Edges |  Sets of MIPS | FPMFP
---|---|---
{} | $\\{\text{$\mu$}_{1}\\}$ | $\\{\text{$\mu$}_{2}\\}$ | $\\{\text{$\mu$}_{1},\text{$\mu$}_{2}\\}$ | $\sqcap$
$e_{2}$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $\top$ | $l\mapsto[0,0]$
$e_{3}$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $\top$ | $l\mapsto[0,0]$
$e_{4}$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $\top$ | $l\mapsto[0,0]$
$e_{5}$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $\top$ | $l\mapsto[0,0]$
$e_{7}$ | $l\mapsto[0,0]$ | $\top$ | $\top$ | $\top$ | $l\mapsto[0,0]$
(a) | (c)
Figure 15: Illustrating pairs that have the same data flow value but do not
have CSO relation between constituent MIPS. $l\mapsto[0,0]$ reaches
$\emph{end}(\text{$\mu_{1}$})$ and $\emph{end}(\text{$\mu_{2}$})$ along the
following feasible CFPs $\sigma_{1}$ and $\sigma_{2}$ respectively,
$\sigma_{1}:e_{0}\rightarrow e_{1}\rightarrow e_{3}\rightarrow
e_{4}\rightarrow e_{7}$, $\sigma_{2}:e_{0}\rightarrow e_{2}\rightarrow
e_{4}\rightarrow e_{5}$.

###  6.3 Removing the pairs that contain $\top$ data flow value

In a pair $\langle\text{$\mathcal{M}$},d\rangle$ the data flow value $d$
remains $\top$ at edges that are outside a MIPS in $\mathcal{M}$. We use the
following observation to eliminate such pairs.

###### Observation 6.2

Ignoring the pairs that contain $\top$ as data flow value does not affect the
precision or the soundness of the FPMFP solution because the FPMFP solution is
computed by taking meet of the data flow values in each pair at a program
point.

_Optimization 3_. We eliminate the pairs that have $\top$ as the associated
data flow value, if the total number of remaining pairs at the program point
is more than one.

For example in Figure 12b, the pairs corresponding to {} at edges $e_{5}$ and
$e_{6}$ contain $\top$ value hence these pairs can be eliminated. Similarly,
pairs corresponding to $\\{\text{$\mu_{1}$},\text{$\mu_{2}$}\\}$ at edges
$e_{3}$ and $e_{9}$ can be eliminated.

With this modification the node and edge flow functions (Equations 11, 15)
remain same except that the meet operator (Equation 12) now assumes absence of
a pair corresponding to some
$\text{$\mathcal{M}$}\subseteq\text{$\mathcal{U}$}$ in the input sets as
presence of a pair $\langle\text{$\mathcal{M}$},\top\rangle$.

###  6.4 Complexity Analysis

The cost of the FPMFP computation is equivalent to computing $k+1$ parallel
MFP solutions, where $k$ is bounded by the maximum number of pairs at a
program point that do not contain $\top$ as the associated data flow value.

At an edge $e$, the maximum number of pairs that do not contain $\top$ value
is same as the maximum number of distinct sets given by
$\text{\emph{cpo}}_{e}(\text{$\mu$})$ over all MIPS $\mu$, plus 1 for the pair
corresponding to {}. In worst case, $\text{\emph{cpo}}_{e}(\text{$\mu$})$ set
for each $\mu$ is distinct. Hence the total number of such pairs (i.e., $k$
value from previous paragraph) is bounded by the number of MIPS in the CFG. In
practice we found the $k$ value to be much smaller where the FPMFP computation
time was $2.9\times$ of the MFP computation time on average. This is because
not all MIPS in a program overlap with each other.

##  7 Experiments and Results

In this section, we empirically compare FPMFP solution with MFP solution with
respect to the precision of the solutions and the efficiency of their
computation. Indeed, we did not find any other existing technique that is as
generic as the MFP computation, and eliminates the effect of infeasible paths
from exhaustive data flow analysis (existing techniques are explained in
Section 8).

The Section is organized as follows. First, we explain the experimental setup
and benchmark characteristics (Section 7.1). Next, we describe two client
analyses on which we compared precision of FPMFP and MFP solutions (Section
7.2), followed by comparing the performance of FPMFP and MFP solutions
(Section 7.5). Lastly, we discuss infeasible path patterns observed in our
benchmarks (Section 7.6)

###  7.1 Experimental Setup

We performed our experiments on a 64 bit machine with 16GB RAM running Windows
7 with Intel core i7-5600U processor having a clock speed of 2.6 GHz. We used
30 C programs of up to 150KLoC size which contained 7 SPEC CPU-2006
benchmarks, 5 industry codesets, and 18 open source codesets [25, 26, 27].
These programs were randomly chosen to cover a range of application areas with
different program characteristics. The number of distinct MIPS range from 17
for the _acpid_ benchmark to 2.1k for the _h264ref_ benchmark. In these
benchmarks, up to 61% (geomertic mean 29%) functions had at least one MIPS in
their CFG. On average 77% MIPS were overlapping with at least one other MIPS.

Table 6: Benchmark properties: three types of benchmarks that we used include
Open source [25, 26, 27], Industry, and SPEC CPU 2006 benchmarks.  Benchmark
Properties
---
Type | Name | KLOC |  #MIPS | $\begin{array}[]{c}\\#\text{Overlapping}\\\ \text{MIPS}\end{array}$ | $\begin{array}[]{c}\\#\text{Balanced}\\\ \text{MIPS}\end{array}$ | $\begin{array}[]{c}\%\text{Funcs}\\\ \text{Impacted}\end{array}$
Open Source | 1.acpid | 0.3 | 6 | 6 | 6 | 7
2.polymorph | 0.4 | 24 | 24 | 17 | 11
3.nlkain | 0.5 | 33 | 8 | 3 | 58
4.spell | 0.6 | 14 | 11 | 12 | 23
5.ncompress | 1 | 30 | 27 | 16 | 30
6.gzip | 1.3 | 49 | 46 | 40 | 25
7.stripcc | 2.1 | 107 | 97 | 74 | 30
8.barcode-nc | 2.3 | 60 | 49 | 22 | 25
9.barcode | 2.8 | 76 | 66 | 28 | 24
10.archimedes | 5 | 118 | 86 | 53 | 38
11.combine | 5.7 | 234 | 210 | 124 | 29
12.httpd | 5.7 | 226 | 211 | 88 | 16
13.sphinxbase | 6.6 | 213 | 199 | 109 | 16
14.chess | 7.5 | 262 | 186 | 112 | 39
15.antiword | 19.3 | 669 | 570 | 306 | 32
16.sendmail | 20.3 | 726 | 681 | 349 | 32
17.sudo | 45.8 | 250 | 223 | 148 | 15
18.ffmpeg | 80 | 1363 | 1201 | 891 | 9
SPEC | 19.mcf | 5.4 | 19 | 17 | 4 | 20
20.bzip2 | 16 | 501 | 485 | 184 | 40
21.hmmer | 16.5 | 595 | 522 | 270 | 20
22.sjeng | 27 | 438 | 379 | 198 | 33
23.milc | 30 | 497 | 375 | 141 | 38
24.h264ref | 35.9 | 2189 | 1696 | 526 | 31
445.gobmk | 150 | 1834 | 1435 | 756 | 13
Industry | 26.NZM | 2.6 | 52 | 43 | 34 | 43
27.IC | 3.7 | 50 | 29 | 13 | 15
28.AIS | 6 | 83 | 56 | 21 | 14
| 29.FRSC | 6 | 42 | 21 | 1 | 15
| 30.FX | 7.5 | 140 | 78 | 39 | 34

We used the iterative fix-point based data flow analysis algorithm [28, 1]
implemented in Java in a commercial static analysis tool _TCS Embedded Code
Analyzer_ [22] for our data flow analysis. Initially, the tool transforms the
source code to an intermediate representation, and constructs CFGs for
procedures in the program. Later, it runs some basic inbuilt analyses like
pointer analysis, alias analysis in flow sensitive and context insensitive
manner, followed by constructing the program call graph. Since FPMFP just
lifts the abstract operations given in the input MFP specification, it remains
oblivious to and respects the analysis specific choices like use of aliasing,
pointers, and field sensitivity. In our evaluation, we implemented the
functional approach of inter-procedural analysis (described in Section 5) for
computing MFP and FPMFP solutions for potentially uninitialized variable
analysis and reaching definitions analysis. The details of the same are
discussed in Section 7.2.

Table 7: Reduction in the number of potentially uninitialized variable Alarms Benchmarks | Uninitialized
---|---
Variable Alarms
MFP | FPMFP | reduction(%)
Open Source | 1.acpid | 1 | 1 | 0(0)
2.polymorph | 4 | 4 | 0(0)
3.nlkain | 4 | 0 | 4(100)
4.spell | 3 | 3 | 0(0)
5.ncompress | 7 | 7 | 0(0)
6.gzip | 0 | 0 | -
7.stripcc | 27 | 1 | 26(96.30)
8.barcode-nc | 0 | 0 | -
9.barcode | 2 | 0 | 2(100)
10.archimedes | 61 | 56 | 5(8.20)
11.combine | 63 | 63 | 0(0)
12.httpd | 117 | 117 | 0(0)
13.sphinxbase | 46 | 43 | 3(6.52)
14.chess | 16 | 16 | 0(0)
15.antiword | 18 | 18 | 0(0)
16.sendmail | 103 | 102 | 1(0.97)
| 17.sudo | 62 | 58 | 4(6.45)
| 18.ffmpeg | 124 | 112 | 12(9.68)
SPEC | 19.mcf | 5 | 5 | 0(0)
20.bzip2 | 72 | 35 | 37(51.39)
21.hmmer | 636 | 629 | 7(1.10)
22.sjeng | 19 | 19 | 0(0)
23.milc | 188 | 168 | 20(10.64)
24.h264ref | 52 | 48 | 4(7.69)
25.gobmk | 1216 | 1199 | 17(1.39)
Industry | 26.NZ | 3 | 0 | 3(100)
27.IC | 5 | 5 | 0(0)
28.AIS | 0 | 0 | -
29.FRSC | 3 | 3 | 0(0)
30.FX | 84 | 84 | 0(0)
Table 8: Reduction in the number of def-use pairs: 1) MFP (resp. FPMFP) column shows the sum of number of def-use pairs at all program nodes $n$ in the CFG of a program for global and local variables.  Benchmarks | Reaching Definition Analysis
---|---
Type | Name | #def-use pairs | reduction(%)
|  | MFP | FPMFP |
Open Source | 1.acpid | 156 | 156 | 0(0.00)
2.polymorph | 228 | 228 | 0(0.00)
3.nlkain | 1042 | 965 | 77(7.39)
4.spell | 516 | 515 | 1(0.19)
5.ncompress | 1201 | 1175 | 26(2.16)
6.gzip | 3423 | 3401 | 22(0.64)
7.stripcc | 2703 | 2645 | 58(2.15)
8.barcode-nc | 3051 | 3007 | 44(1.44)
9.barcode | 3709 | 3653 | 56(1.51)
10.archimedes | 44337 | 44216 | 121(0.27)
11.combine | 16618 | 15859 | 759(4.57)
12.httpd | 10475 | 10072 | 403(3.85)
13.sphinxbase | 9641 | 8482 | 1159(12.02)
14.chess | 31386 | 31303 | 83(0.26)
15.antiword | 68889 | 60144 | 8745(12.69)
16.sendmail | 102812 | 101470 | 1342(1.31)
17.sudo | 14391 | 14211 | 180(1.25)
18.ffmpeg | 89148 | 86607 | 2541(2.85)
SPEC | 19.mcf | 3570 | 3565 | 5(0.14)
20.bzip2 | 82548 | 77967 | 4581(5.55)
21.hmmer | 70597 | 70021 | 576(0.82)
22.sjeng | 77602 | 76959 | 643(0.83)
23.milc | 18133 | 17828 | 305(1.68)
24.h264ref | 426346 | 409325 | 17021(3.99)
25.gobmk | 213243 | 184142 | 29101(13.65)
Industry | 26.NZ | 2652 | 2651 | 1(0.04)
27.IC | 3111 | 3063 | 48(1.54)
28.AIS | 2475 | 2414 | 61(2.46)
| 29.FRSC | 1297 | 1295 | 2(0.15)
| 30.FX | 4971 | 4925 | 46(0.93)
Table 9: Comparing performance of MFP and FPMFP computation. _Prep._ represents the MIPS detection phase. Note the analysis times are not comparable with gcc or clang, because our implementation is in Java. Benchmarks | Analysis Time (Sec) | Memory Consumption (MB)
---|---|---
Prep | MFP | FPMFP | $\begin{array}[]{c}\text{Incre-}\\\ \text{ase(x)}\end{array}$ | Prep | MFP | FPMFP | $\begin{array}[]{c}\text{Incre-}\\\ \text{ase(x)}\end{array}$
Open Source | 1.acpid | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0
2.polymorph | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0
3.nlkain | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 0
4.spell | 0 | 0 | 0 | 0 | 1 | 1 | 0 | 0
5.ncompress | 1 | 0 | 1 | 1(1) | 2 | 1 | 4 | 2(2)
6.gzip | 1 | 1 | 5 | 4(4) | 5 | 10 | 24 | 14(1.4)
7.stripcc | 3 | 1 | 6 | 5(5) | 8 | 5 | 21 | 15(3)
8.barcode-nc | 2 | 1 | 2 | 1(1) | 6 | 8 | 6 | -1(-0.1)
9.barcode | 2 | 2 | 2 | 0 | 7 | 10 | 8 | -1(-0.1)
10.archimedes | 6 | 3 | 32 | 29(10) | 24 | 44 | 156 | 112(2.5)
11.combine | 5 | 3 | 5 | 2(0.6) | 16 | 23 | 19 | -3(-0.1)
12.httpd | 40 | 14 | 19 | 5(0.3) | 28 | 39 | 21 | -18(-0.46)
13.sphinxbase | 7 | 3 | 3 | 0 | 13 | 16 | 7 | -9(-0.56)
14.chess | 13 | 7 | 30 | 23(3) | 31 | 93 | 191 | 98(1)
15.antiword | 13 | 16 | 82 | 66(4) | 47 | 101 | 218 | 117(1)
16.sendmail | 110 | 142 | 2060 | 1918(13) | 81 | 340 | 1548 | 1208(3.5)
| 17.sudo | 15 | 9 | 17 | 8(1) | 35 | 71 | 19 | -52(-0.7)
| 18.ffmpeg | 234 | 51 | 80 | 29 (0.5) | 158 | 266 | 90 | -175(-0.6)
SPEC 2006 | 19.mcf | 1 | 1 | 1 | 0 | 0 | 3 | 3 | 0
20.bzip2 | 8 | 7 | 69 | 62 (9) | 28 | 44 | 90 | 46(1)
21.hmmer | 14 | 9 | 23 | 14(1.5) | 50 | 67 | 58 | -8(-0.1)
22.sjeng | 10 | 16 | 62 | 46(2.8) | 27 | 122 | 215 | 92(0.75)
23.milc | 6 | 4 | 7 | 3(0.7) | 25 | 25 | 14 | -11(-0.4)
24.h264ref | 60 | 115 | 451 | 336(2.9) | 131 | 1003 | 1644 | 640(0.6)
25.gobmk | 4218 | 1696 | 9818 | 8122(4.7) | 390 | 9365 | 17392 | 8032(0.85)
Industry | 26.NZM | 1 | 1 | 2 | 1(1) | 3 | 8 | 7 | -1(-0.1)
27.IC | 5 | 4 | 3 | -1(-0.25) | 11 | 20 | 9 | -11(-0.5)
28.FRSC | 3 | 2 | 1 | -1(-0.5) | -15 | 10 | 4 | -6(-0.6)
29.AIS | 4 | 3 | 4 | 1(0.3) | 9 | 20 | 16 | -4(-0.2)
30.FX | 7 | 3 | 7 | 4(1.3) | 20 | 35 | 47 | 11(0.3)
Table 10: Impact of Optimization 1 on the FPMFP computation (in Optimization 1, we consider two MIPS with the same end edge as equivalent, and subsequently merge the pairs that contain equivalent MIPS). Benchmarks |  Number of Distinct MIPS
---|---
Before and After Optimization 1
Before | After | Reduction(%)
Open Source | 1.acpid | 83 | 6 | 77(92.77)
2.polymorph 0.96 | 65 | 24 | 41(63.08)
3.nlkain | 35 | 33 | 2(5.71)
4.spell | 99 | 14 | 85(85.86)
5.ncompress | 14163 | 30 | 14133(99.79)
6.gzip | 23524624 | 49 | 23524575(99.99)
7.stripcc | 774751 | 107 | 774644(99.99)
8.barcode-nc | 208 | 60 | 148(71.15)
9.barcode | 3851 | 76 | 3775(98.03)
10.archimedes | 1054292 | 118 | 1054174(99.99)
11.combine | 27061 | 234 | 26827(99.14)
12.httpd | 76591463106 | 226 | 76591462880(99.99)
13.sphinxbase | 6463 | 213 | 6250(96.70)
14.chess | 19701157845 | 262 | 19701157583(99.99)
15.antiword | 1446759232593972 | 669 | 1446759232593303(99.99)
16.sendmail | 94082730655046 | 726 | 94082730654320(99.99)
| 17.sudo | 549565 | 250 | 549315(99.95)
| 18.ffmpeg | 5019442696182 | 1363 | 5019442694819(99.99)
SPEC 2006 | 19.mcf | 44 | 19 | 25(56.82)
20.bzip2 | 115451494 | 501 | 115450993(99.99)
21.hmmer | 8606721 | 595 | 8606126(99.99)
22.sjeng | 1508084297532741 | 438 | 1508084297532303(99.99)
23.milc | 2322 | 497 | 1825(78.60)
24.h264ref | 51269021916 | 2189 | 51269019727(99.99)
25.gobmk | $>2^{64}$ | 1834 |  $>2^{64}$(99.99)
Industry | 26.NZM | 1064 | 52 | 1012(95.11)
27.IC | 158 | 50 | 108(68.35)
28.AIS | 176 | 83 | 93(52.84)
29.FRSC | 89 | 42 | 47(52.81)
30.FX | 704 | 140 | 564(80.11)
Table 11: Impact of Optimization 2 on the FPMFP computation. Timeout indicates the analysis did not finish within 10K seconds. Benchmarks | Analysis Time (in Seconds)
---|---
Before and After Optimization 2
Before | After | Reduction(%)
Open Source | 1.acpid | 0 | 0 | 0
2.polymorph 0.96 | 0 | 0 | 0
3.nlkain | 0 | 0 | 0
4.spell | 0 | 0 | 0
5.ncompress | 3 | 1 | 2(66)
6.gzip | 22 | 5 | 17(77)
7.stripcc | 55 | 6 | 49(89)
8.barcode-nc | 2 | 2 | 0
9.barcode | 2 | 2 | 0
10.archimedes | 53 | 32 | 21(39)
11.combine | 19 | 5 | 14(73)
12.httpd | 290 | 19 | 271 (93)
13.sphinxbase | 4 | 3 | 1(25)
14.chess | 76 | 30 | 46(60)
15.antiword | 705 | 82 | 623(88)
16.sendmail | Timeout | 2060 | -
| 17.sudo | 64 | 17 | 47(73)
| 18.ffmpeg | Timeout | 80 | -
SPEC 2006 | 19.mcf | 1 | 1 | 0
20.bzip2 | 931 | 69 | 862 (92)
21.hmmer | 143 | 23 | 120(83)
22.sjeng | 501 | 62 | 439(87)
23.milc | 11 | 7 | 4(36)
24.h264ref | 2977 | 451 | 2526(84)
25.gobmk | Timeout | 9818 | -
Industry | 26.NZM | 4 | 2 | 2(50)
27.IC | 6 | 3 | 3(50))
28.AIS | 7 | 4 | 3(42)
29.FRSC | 3 | 1 | 2(66)
30.FX | 9 | 7 | 2(22)

###  7.2 Comparing the Precision of FPMFP and MFP Solutions

###  7.3 Reduction in the Number of Potentially Uninitialized Variable Alarms

A potentially uninitialized variable analysis reports the variables that are
used at a program point but are not initialized along at least one path that
reaches the program point. We computed the potentially uninitialized variables
as follows: first, we implemented the _must defined variables_ analysis that
computes the set of non-array variables that are defined along all CFPs
reaching a program point. Next, we take the complement of the _must defined_
data flow results to report the variables that are used at a program point $p$
but are not initialized along at least one CFP that reaches $p$. We call such
CFPs as _witness CFPs_.

As shown in Table 7, we computed two sets of potentially uninitialized
variable alarms corresponding to the MFP and FPMFP solutions of must defined
variable analysis. In particular, the potentially uninitialized variable
analysis that used the FPMFP solution of _must defined_ analysis reported up
to 100% (average 18.5%, geo. mean 3%) fewer alarms compared to when it used
the MFP solution. In the reduced alarm cases, all the witness CFPs were found
infeasible.

More specifically, in 14 out of 27 benchmarks the FPMFP solution helped
achieve positive reduction in the uninitialized variable alarms, while in 13
benchmarks there was no reduction in the alarms. In the latter case the
following two scenarios were observed: in the first scenario, the addresses of
uninitialized variables are passed as parameter to library functions whose
source code is not available and hence its behavior is conservatively
approximated (i.e, the analysis assumed that the variables are not initialized
inside the functions), and in the second scenario a variable is conditionally
initialized inside the callee procedure where the evaluation of the condition
depends on the calling context thereby necessitating a context sensitive
analysis to eliminate the false positive alarm (our implementation is context
insensitive).

###  7.4 Reduction in the Number of Def-Use Pairs

We implemented the classic reaching definitions analysis [28, 1] (non SSA
based) in which for each program point, we compute the set of definitions that
reach the point. We measured the effect of the reduction in the number of
reaching definitions on Def-Use pair computation, which is a client analysis
of the reaching definitions analysis. In this, we pair the definition of a
variable with its reachable use point.

In the FPMFP computation, the def and use points that are connected with each
other by only infeasible paths are eliminated. However, we found that most
def-use points are connected by at least one feasible CFP, and hence a 100%
reduction is not achievable by any technique.

As shown in Table 8, we found that up to 13.6% (average 2.87%, geometric mean
1.75%) fewer def-use pairs were reported when using FPMFP solution in place of
the MFP solution. In particular, in 28 out of 30 benchmarks the FPMFP solution
lead to fewer def-use pairs than the MFP solution. In general, we observed
that the precision increased with increase in the number of MIPS. For example,
the _gobmk_ benchmark contains a large number of MIPS (1.9k), consequently we
observed significant (13%) reduction in the number of def-use pairs. On the
other hand, the _acpid_ benchmark had only 17 MIPS, consequently we did not
see any reduction in the number of def-use pairs. As an outlier case, on the
_sphinxbase_ benchmark that had only 216 MIPS we observed 12% reduction in
def-use pairs. Here, we observed that the end edges of many MIPS are reachable
only along infeasible CFPs, hence in FPMFP computation the data flow along
these edges is completely blocked, thus all the corresponding def-use pairs
(at the program points pre-dominated by the end edges) are eliminated.

The def-use pairs have multifold applications; in particular, they are useful
for program slicing, program dependency graph creation, program debugging, and
test case generation. For example in program testing, some coverage criteria
mandate that each def-use pair should be covered by at least one test case.
Here, up to 13.6% fewer def-use pairs means fewer manual test cases need to be
written to cover these pairs, which is a significant reduction in the manual
time and efforts.

###  7.5 Comparing the Performance of FPMFP and MFP Computations

Computation of the FPMFP solution was less efficient than the corresponding
MFP solutions. The details of the relative memory and time consumption of both
the analyses for reaching definitions computation are presented in Table 9.
The _Prep._ column represents the time and memory consumption for infeasible
path detection phase. This is performed once for each program.

The FPMFP analysis took 2.9 times more time than MFP analysis on average (geo.
mean 1.6). In general, the analysis time increased with increase in the number
of MIPS in the program. Apart from this, the FPMFP analysis consumed 0.5 times
more memory than the MFP analysis on average. However, on 50% of the bechmarks
the FPMFP analysis consumed less memory than the MFP analysis because the
definitions reaching along infeasible CFPs are ignored during the analysis.

The effect of optimizations for scalability on analysis time

Table 10 shows the reduction in the number of distinct MIPS after applying
Optimization 1 (Section 6.1). Here, two MIPS are considered equivalent if they
have the same end edge, in this case we can merge two pairs if they contain
equivalent MIPS. We found that if we count MIPS with same end edge single
time, then the total number of MIPS reduces by up to 99%(average 85%,
geometric mean 78%). This leads to reduction in number of pairs at various
program points.

Table 11 shows the effectiveness of optimization 2 (Section 6.2) on top of
optimization 1. In particular, it shows the analysis time before and after
applying the optimization 2. We found that 3 out of 30 applications timed out
(i.e., did not finish within 10K seconds) when we disabled optimization 2.
Similarly, for remaining applications the analysis time increased by up to
99%(average 48.9%, geometric mean 19.8%) after disabling optimization 2.

| If(…){
---
A: $x=5$;
}
…
If($x<5$){
B: print(“%$d$”, &$x$)
}
| Const int $N=100$
---
A: $x=0$;
While($x<N$){
…
$x++$;
}
B:
| If($x<5$){
---
A:
}
…
If($x<5$){
…
}else{
B:
}
(a) | (b) | (c)
Figure 16: Illustrating the types of MIPS observed. In each of the example
above there is a MIPS going from point A to point B. The variable $x$ is not
modified in the code portion represented by three dots ($\ldots$) .

###  7.6 Types of MIPS Observed

In general case, knowing whether a path is infeasible or not is undecidable.
Nevertheless, a large number of infeasible paths in a program can be
identified using statically detectable correlations between two branch
conditions or between a branch condition and an assignment statement. Indeed,
in our work, we detected a large number of MIPS using Bodik’s approach
(described in Appendix A).

We observe that a lot of MIPS in our benchmarks belong to one of the following
two types resulting from correlation between an assignment statement and a
branch statement or two branch statements.

  1. 1.

The first type involves assignment of constant value to a variable along some
node in a path followed by the variable being used in some conditional
expression that performs either _equality_ or _less than_ or _greater than_
check on the variable later in the path. Two typical examples of this type are
shown Figure 16a and 16b. In the first example a variable is assigned a
constant value inside the if branch (point A) and subsequently used in other
branch condition that appears later in the path (point B). The second example
contains a loop that executes at least once hence the path that goes from
point A to point B without executing the loop is infeasible.

  2. 2.

The second type involves two syntactically same conditions used in two
branches at different places in a path and the variables in the conditions are
not modified along the path that connects the branches. For example in Figure
16c the path that goes from point A to point B is infeasible.

###  7.7 Summary of Empirical Observations

Previous empirical evidence [2] on linux kernel code shows 9-40% of
conditional statements contribute to at least one infeasible CFP. In our