Changeset 1750


Ignore:
Timestamp:
Feb 24, 2012, 5:02:06 PM (8 years ago)
Author:
tranquil
Message:

start of ERTL to LTL

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1749 r1750  
    1515\usepackage{skull}
    1616\usepackage{stmaryrd}
     17\usepackage{array}
     18\newcolumntype{b}{@{}>{{}}}
     19\newcolumntype{B}{@{}>{{}}c<{{}}@{}}
     20\newcolumntype{h}[1]{@{\hspace{#1}}}
     21\newcolumntype{L}{>{$}l<{$}}
     22\newcolumntype{C}{>{$}c<{$}}
     23\newcolumntype{R}{>{$}r<{$}}
     24\newcolumntype{S}{>{$(}r<{)$}}
     25\newcolumntype{n}{@{}}
    1726\usepackage{wasysym}
     27
    1828
    1929\lstdefinelanguage{matita-ocaml} {
     
    543553\mathrm{RTL\ status} & \ \ \mathrm{ERTL\ status} \\
    544554\mathtt{sp} & = \mathtt{spl} / \mathtt{sph} \\
    545 \mathtt{graph} & \mapsto \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
     555\mathtt{graph} & \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
    546556& \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\
    547557\end{align*}
     
    588598\subsection{The ERTL to LTL translation}
    589599\label{subsect.ertl.ltl.translation}
    590 
     600\newcommand{\declsf}[1]{\expandafter\newcommand\expandafter{\csname #1\endcsname}{\mathop{\mathsf{#1}}\nolimits}}
     601\declsf{Livebefore}
     602\declsf{Liveafter}
     603\declsf{Defined}
     604\declsf{Used}
     605\declsf{Eliminable}
     606\declsf{StatementSem}
     607For the liveness analysis, we aim at a map
     608$\ell \in \mathtt{label} \mapsto $ live registers at $\ell$.
     609We define the following operators on ERTL statements.
     610$$
     611\begin{array}{lL>{(ex. $}L<{)$}}
     612\Defined(s) & registers defined at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_1,C\}, \mathtt{CALL}id\mapsto \text{caller-save}
     613\\
     614\Used(s) & registers used at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_2,r_3\}, \mathtt{CALL}id\mapsto \text{parameters}
     615\end{array}
     616$$
     617Given $LA:\mathtt{label}\to\mathtt{lattice}$ (where $\mathtt{lattice}$
     618is the type of sets of registers\footnote{More precisely, it is thethe lattice
     619of pairs of sets of pseudo-registers and sets of hardware registers,
     620with pointwise operations.}, we also have have the following
     621predicates:
     622$$
     623\begin{array}{lL}
     624\Eliminable_{LA}(\ell) & iff $s(\ell)$ has side-effects only on $r\notin LA(\ell)$
     625\\&
     626(ex.\ $\ell : r_1\leftarrow r_2+r_3 \mapsto (\{r_1,C\}\cap LA(\ell)\neq\emptyset,
     627  \mathtt{CALL}id\mapsto \text{never}$)
     628\\
     629\Livebefore_{LA}(\ell) &$:=
     630  \begin{cases}
     631    LA(\ell) &\text{if $\Eliminable_{LA}(\ell)$,}\\
     632    (LA(\ell)\setminus \Defined(s(\ell)))\cup \Used(s(\ell) &\text{otherwise}.
     633  \end{cases}$
     634\end{array}
     635$$
     636In particular, $\Livebefore$ has type $(\mathtt{label}\to\mathtt{lattice})\to
     637\mathtt{label}\to\mathtt{lattice}$.
     638
     639The equation on which we build the fixpoint is then
     640$$\Liveafter(\ell) \doteq \bigcup_{\ell' >_1 \ell} \Livebefore_{\Liveafter}(\ell')$$
     641where $\ell' >_1 \ell$ denotes that $\ell'$ is an immediate successor of $\ell$
     642in the graph. We do not require the fixpoint to be the least one, so the hypothesis
     643on $\Liveafter$ that we require is
     644$$\Liveafter(\ell) \supseteq \bigcup_{\ell' >_1 \ell} \Livebefore(\ell')$$
     645(for shortness we drop the subscript from $\Livebefore$).
    591646\subsection{The LTL to LIN translation}
    592647\label{subsect.ltl.lin.translation}
Note: See TracChangeset for help on using the changeset viewer.