# Changeset 1788 for Deliverables/D1.2

Ignore:
Timestamp:
Feb 28, 2012, 11:32:07 AM (9 years ago)
Message:

small modifications

File:
1 edited

### Legend:

Unmodified
 r1786 Given $LA:\mathtt{label}\to\mathtt{lattice}$ (where $\mathtt{lattice}$ is the type of sets of registers\footnote{More precisely, it is the lattice of pairs of sets of pseudo-registers and sets of hardware registers, $\mathtt{set}(\mathtt{register})\times \mathtt{set}(\mathtt{hdwregister})$, with pointwise operations.}), we also have have the following predicates: $$x\sim y \at \ell$$ to state that registers $x$ and $y$ are similar at $\ell$. The formal definition will be given next, but intuitively it means that those two registers \emph{must} have the same value at $\ell$. The analysis that produces this information can be of this relation's property will be given next, but intuitively it means that those two registers \emph{must} have the same value after $\ell$. The analysis that produces this information can be coarse: in our case, we just set two different registers to be similar at $\ell$ if at $\ell$ itself there is a move instruction between the two. \end{itemize} The overall effect is that if $T$ is an LTL state with $\ell(T)=\ell$ then we will have $T\to^+T'$ where $T'(\Colour(r_1))=T(\Colour(r_2))+T(\Colour(r_2))$. We skip over the details of correctly dealing with the stack and its size. then we will have $T\to^+T'$ where $T'(\Colour(r_1))=T(\Colour(r_2))+T(\Colour(r_2))$, while $T'(y)=T(y)$ for any $y$ \emph{in the image of $\Colour$} different from $\Colour(r_1)$. Some hardware registers that are used for book-keeping and which are explicitly excluded from colouring may have different values. We skip the details of correctly dealing with the stack and its size. \subsubsection{The relation between ERTL and LTL states} Given a state $S$ in ERTL, we abuse the notation by using $S$ as the underlying map