Changeset 1748

Ignore:
Timestamp:
Feb 24, 2012, 4:53:07 PM (8 years ago)
Message:

commit to avoid conflicts

File:
1 edited

Legend:

Unmodified
 r1747 \> $\downarrow$ \> copy propagation\footnote{\label{lab:opt}To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation) \\ \> $\downarrow$ \> instruction selection\\ \> $\downarrow$ \> change of memory models in compiler\\ \textsf{RTL}\\ \> $\downarrow$ \> constant propagation$^{\mbox{\scriptsize \ref{lab:opt}}}$ (an endo-transformation) \\ \label{subsect.rtlabs.rtl.translation} % dpm: type system and casting load (???) We require a map, $\sigma$, between \texttt{Values} of the front-end memory model to lists of \texttt{BEValues} of the back-end memory model: The RTLabs to RTL translation pass marks the frontier between the two memory models used in the CerCo project. As a result, we require some method of translating between the values that the two memory models permit. Suppose we have such a translation, $\sigma$. Then the translation between values of the two memory models may be pictured with: \begin{displaymath} \end{displaymath} In the front-end, we have both integer and float values, where integer values are sized, along with null values and pointers. In the back-end memory model, floats values are no longer present, as floating point arithmetic is not supported by the CerCo compiler. However, the back-end memory model introduces an undefined value ($\bot$) and sized pointer values. We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}. \end{displaymath} where Here, \texttt{Block} consists of a \texttt{Region} paired with an identifier. \begin{displaymath} \end{displaymath} \begin{displaymath} \mathtt{BEMem} = \mathtt{Mem} \mathtt{Value} \end{displaymath} We now have what we need for defining what is meant by the memory' in the backend memory model. Namely, we instantiate the previously defined \texttt{Mem} type with the type of back-end memory values. \begin{displaymath} \mathtt{BEMem} = \mathtt{Mem} \mathtt{BEValue} \end{displaymath} Memory addresses consist of a pair of back-end memory values: \begin{displaymath} \mathtt{Address} = \mathtt{BEValue} \times  \mathtt{BEValue} \\ \end{displaymath} \begin{displaymath} \mathtt{Mem} = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \mathtt{Cont} \mid \mathtt{Value} \times \mathtt{Size} \mid \mathtt{null}) \end{displaymath}