Next: Transformation Up: But Mom, I don't Previous: Recasting the Problem in

Analysis

The analysis computes an approximation of return continuations of each known function. We present a very simple linear-time analysis that uses the term labels to represent abstract continuations. The analysis uses a simple notion of escaping function - if a function name is mentioned in a non-application rôle, it is regarded as escaping and we define its return continuation to be $\top$ .

We define an abstract domain of return continuations:

$\begin{displaymath}\rho \in \mathsf{RCont} = \mathsf{Label} \cup \{ \bot, \top \} \end{displaymath}$

$\begin{displaymath}\sqsubseteq = \bigcup_{l \in \mathsf{Label}} \{ (\bot, l), (l, \top) \} \end{displaymath}$

$\begin{displaymath}\sqcup = \mbox{lub under $\sqsubseteq$} \end{displaymath}$

Given an expression and its abstract continuation, the analysis computes a map $\Gamma$ from variables (in particular, function names) to abstract continuations:

$\begin{displaymath}\Gamma' \in \mathsf{REnv} = \mathsf{Var} \rightharpoonup \mathsf{RCont} \end{displaymath}$

$\begin{displaymath}\Gamma(x) = \left\{ \begin{array}{ccc} \Gamma'(x) & & x \in ... ... \bot & & x \not\in \mathrm{dom}(\Gamma') \end{array} \right. \end{displaymath}$

$\begin{displaymath}\Gamma_1 \uplus \Gamma_2 = \{ x \mapsto \Gamma_1(x) \sqcup \Gamma_2(x) \end{displaymath}$

The analysis itself is defined as follows:

$\begin{displaymath}\mathcal{R} : \mathsf{Exp} \rightarrow \mathsf{RCont} \rightarrow \mathsf{REnv} \end{displaymath}$

$\begin{displaymath}\begin{array}{rcl} \mathcal{R}[\![ l : x ]\!]\rho & = & \{ x... ... \mapsto \rho \} \uplus \{ \vec{x}\mapsto \top \} \end{array} \end{displaymath}$

The analysis for a whole program is defined as follows:

$\begin{displaymath}\mathcal{A} : \mathsf{Exp} \rightarrow \mathsf{REnv} \end{displaymath}$

$\begin{displaymath}\mathcal{A}[\![ e ]\!] = \mathcal{R}[\![ e ]\!]\top \end{displaymath}$

So, for our example, we have:

$\begin{displaymath}\mathcal{A}[\![ \ldots ]\!] = \{ \mbox{\texttt{lp\_i}} \map... ... \mapsto \top, \mbox{\texttt{applyf}} \mapsto \bot, \ldots \} \end{displaymath}$

Next: Transformation Up: But Mom, I don't Previous: Recasting the Problem in

Matthew Fluet 2002-02-22