Optimization Under the Perspective of Soundness, Completeness, and Reusability - Correct System Design: Recent Insights and Advances - page 291

treatment of this phenomenon requires to implicitly mimic the run-time stack on
the analysis side. In [28] this was rst achieved by introducing a so-called DFA
stack on the analysis side. Intuitively, its entries mimic the activation records of
the corresponding run-time stack. In addition to data-flow facts and data-flow
functions dening an intraprocedural DFA problem, the specication of an inter-
procedural DFA problem requires a third component, so-called return functions
for handling the return from (recursive) procedure calls. Intuitively, the eect of
a (recursive) procedure call on global variables must be maintained, while the
one on local variables must be reset to the state valid immediately before the
call. Return functions realize this by conflating the two top-most entries of the
DFA stack storing the data-flow facts valid when calling the procedure under
consideration, and the data-flow fact valid immediately before leaving it to the
data-flow fact representing the valid data-flow information after nishing the
call.
Based on this extension, the interprocedural variant of the MFP -approach,

the -approach, proceeds almost as in the intraprocedural case. In addition

to the intraprocedural setting, however, it relies on a preprocess for computing
the global abstract semantics of procedures. This is a second-order approach
operating on data-flow fact transformers representing the global semantics of
procedures instead of single data-flow facts. The transformers computed by the
preprocess can then be used to compute the algorithmic solution of the problem
under consideration almost as in the intraprocedural setting. The details of the
complete process, which denes the interprocedural version of the

IMFP

MFP -solution,

the -solution, have originally been given in [28], and for a more general

setting in [14]. Similar to its intraprocedural counterpart, the

IMFP

-solution
denes the algorithmic solution of an interprocedural DFA problem. It can ef-
fectively be computed, whenever the function lattice of the lattice of data-flow
facts is of nite height, and the data-flow functions and return functions dening
the abstract semantics of elementary statements are monotonic.

IMFP

Sound and Complete Interprocedural Analyses. Similar to its intrapro-
cedural counterpart, soundness and completeness of the -approach are

dened with respect to an operational globalization of the abstract semantics
underlying it. For the purposes of this article, it is sucient to note the sim-
ilarity of the denition of the interprocedural

IMFP

MOP -solution, in symbols the

IMOP -solution, and its intraprocedural counterpart. The details are indeed not

necessary. Thus, we only remark that newstack is a function, which yields a
DFA stack containing its argument as single entry, and that IP [ ] denotes

the set of so-called interprocedurally valid paths connecting two nodes

m; n

m and

n . Intuitively, interprocedurally valid paths respect the call/return-behaviour of

procedure calls (cf. [44]). The meet-operation, nally, occurring in the denition
of the

IMOP

-solution is the ordinary meet on the lattice under consideration
applied to the top-components of the argument stacks.

The IMOP -Solution:

u f [[ p ]] ( newstack ( c 0 )) j p 2 IP [ s ;n ] g

8 c 0 2C8n2N: IMOP ( n )( c 0 )=