# Changeset 1773

Ignore:
Timestamp:
Feb 27, 2012, 3:53:15 PM (7 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r1772 \subsection{Graph translations} RTLabs and most intermediate languages in the back-end have a graph representation: the code of each function is represented by a graph of instructions. The graph maps a set of labels (the names of the nodes) to the instruction stored at that label (the nodes of the graph). Instructions reference zero or more additional labels that are the immediate successors of the instruction: zero for return from functions; more than one for conditional jumps and calls; one in all other cases. The references from one instruction to its immediates are the arcs of the graph. Status of graph languages always have a program counter that holds a representation of a reference to the current instruction. A translation between two consecutive graph languages maps each instruction stored at location $l$ in the first graph and with immediate successors $\{l_1,\ldots,l_n\}$ to a subgraph of the output graph that has a single entry point at location $l$ and exit arcs to $\{l_1,\ldots,l_n\}$. Moreover, the labels of all non entry nodes in the subgraph are distinct from all the labels in the source graph. In order to simplify the translations and the relative proofs of forward simulation, after the release of D4.2 and D4.3, we have provided: \begin{itemize} \item a new data type (called \texttt{blist}) that represents a sequence of instructions to be added to the output graph. The b'' in the name stands for binder, since a \texttt{blist} is either empty, an extension of a \texttt{blist} with an instruction at the front, or the generation of a fresh quantity followed by a \texttt{blist}. The latter feature is used, for instance, to generate fresh register names. The instructions in the list are unlabelled and all of them but the last one are also sequential, like in a linear program. \item a new iterator (called \texttt{b\_graph\_translate}) of type \begin{displaymath} \mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist}) \rightarrow \mathtt{graph} \rightarrow \mathtt{graph} \end{displaymath} The iterator transform the input graph in the output graph by replacing each node with the graph that corresponds to the linear \texttt{blist} obtained by applying the function in input to the node label. \end{itemize} Using the iterator above, the code can be written in such a way that the programmer does not see any distinction between writing a transformation on linear or graph languages. In order to prove simulations for translations obtained using the iterator, we will prove the following theorem: \begin{align*} \mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\ & \forall  f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\ &       \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (next \ l \ G_i)\ G_{\sigma} \end{align*} Here \texttt{subgraph} is a computational predicate that given a \texttt{blist} $[i_1, \ldots, i_n]$, an entry label $l$, an exit label $l'$ and a graph $G$ expands to the fact that fetching from $G$ at address $l$ one retrieves a node $i_1$ with a successor $l_1$ that, when fetched, yields a node $i_2$ with a successor $l_2$ such that \ldots. The successor of $i_n$ is $l'$. Proving a forward simulation diagram of the following kind using the theorem above is now as simple as doing the same using standard small step operational semantics over linear languages. \begin{align*} \mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\ &       \forall s.  \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\ &       \mathtt{let}\ l := pc\ s\ \mathtt{in} \\ &       s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma \end{align*} Because of the fact that graph translation preserves entry and exit labels of translated statements, the state translation function $\sigma$ will simply preserve the value of the program counter. The program code, which is part of the state, is translated using the iterator. The proof is then roughly the following. Let $l$ be the program counter of the input state $s$. We proceed by cases on the current instruction of $s$. Let $[i_1, \ldots, i_n]$ be the \texttt{blist} associated to $l$ and $s$ by the translation function. The witness required for the existential statement is simply $n$. By applying the theorem above we know that the next $n$ instructions that will be fetched from $s\ \sigma$ will be $[i_1, \ldots, i_n]$ and it is now sufficient to prove that they simulate the original instruction. \subsection{The RTLabs to RTL translation} \end{diagram} \end{displaymath} \subsection{The RTL to ERTL translation} \label{subsect.rtl.ertl.translation} \begin{displaymath} \mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist'}) \rightarrow \mathtt{graph} \rightarrow \mathtt{graph} \end{displaymath} \begin{align*} \mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\ & \forall  f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\ &       \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (\mathtt{next}\ l\ G_{i})\ G_{\sigma} \end{align*} \begin{align*} \mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\ &       \forall s.  \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\ &       \mathtt{let}\ l := pc\ s\ \mathtt{in} \\ &       s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma \end{align*} \begin{align*}