Changeset 1752 for Deliverables

Ignore:
Timestamp:
Feb 24, 2012, 5:18:22 PM (8 years ago)
Message:

...

File:
1 edited

Legend:

Unmodified
 r1751 In the last section we finally present an estimation of the effort required for the certification in Matita of the compiler. for the certification in Matita of the compiler and we draw conclusions. \section{Front-end: Clight to RTLabs} \begin{displaymath} \mathtt{Value} ::= \bot \mid \mathtt{int(size)} \mid \mathtt{float} \mid \mathtt{null} \mid \mathtt{ptr} \quad\stackrel{\sigma}{\longrightarrow}\quad \mathtt{BEValue} ::= \bot \mid \mathtt{byte} \mid \mathtt{int}_i \mid \mathtt{ptr}_i \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}. \mathtt{Value} ::= \bot \mid \mathtt{int(size)} \mid \mathtt{float} \mid \mathtt{null} \mid \mathtt{ptr} \quad\stackrel{\sigma}{\longrightarrow}\quad \mathtt{BEValue} ::= \bot \mid \mathtt{byte} \mid \mathtt{null}_i \mid \mathtt{ptr}_i \end{displaymath} In the front-end, we have both integer and float values, where integer values are sized', along with null values and pointers. Some frontenv values are representables in a byte, but some others require more bits. In the back-end model all values are meant to be represented in a single byte. Values can thefore be undefined, be one byte long integers or be indexed fragments of a pointer, null or not. Floats values are no longer present, as floating point arithmetic is not supported by the CerCo compiler. The $\sigma$ map implements a one-to-many relation: a single front-end value is mapped to a sequence of back-end values when its size is more then one byte. We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}. Both kinds of memory can be thought as an instance of a generic \texttt{Mem} data type parameterized over the kind of values stored in memory. \begin{displaymath} \begin{displaymath} \mathtt{Block} ::= \mathtt{Region} \cup \mathtt{ID} \mathtt{Block} ::= \mathtt{Region} \times \mathtt{ID} \end{displaymath} In particular, the front-end stores integer values as a header, with size information, followed by a string of continuation' blocks, marking out the full representation of the value in memory. In contrast, the layout of sized integer values in the back-end memory model consists of a series of byte-sized chunks': \begin{center} \begin{picture}(2, 2) \put(-150,-20){\framebox(25,25)[c]{\texttt{v}}} \put(-125,-20){\framebox(25,25)[c]{\texttt{4}}} \put(-100,-20){\framebox(25,25)[c]{\texttt{cont}}} \put(-75,-20){\framebox(25,25)[c]{\texttt{cont}}} \put(-50,-20){\framebox(25,25)[c]{\texttt{cont}}} \put(-15,-10){\vector(1, 0){30}} \put(25,-20){\framebox(25,25)[c]{\texttt{\texttt{v1}}}} \put(50,-20){\framebox(25,25)[c]{\texttt{\texttt{v2}}}} \put(75,-20){\framebox(25,25)[c]{\texttt{\texttt{v3}}}} \put(100,-20){\framebox(25,25)[c]{\texttt{\texttt{v4}}}} \begin{picture}(0, 25) \put(-125,0){\framebox(25,25)[c]{\texttt{v,4}}} \put(-100,0){\framebox(25,25)[c]{\texttt{cont}}} \put(-75,0){\framebox(25,25)[c]{\texttt{cont}}} \put(-50,0){\framebox(25,25)[c]{\texttt{cont}}} \put(-15,10){\vector(1, 0){30}} \put(25,0){\framebox(25,25)[c]{\texttt{\texttt{v$_1$}}}} \put(50,0){\framebox(25,25)[c]{\texttt{\texttt{v$_2$}}}} \put(75,0){\framebox(25,25)[c]{\texttt{\texttt{v$_3$}}}} \put(100,0){\framebox(25,25)[c]{\texttt{\texttt{v$_4$}}}} \end{picture} \end{center} Chunks for pointers are pairs made of the original pointer and the index of the chunk. Therefore, when assembling the chunks together, we can always recognize if all chunks refer to the same value or if the operation is meaningless. The differing memory representations of values in the two memory models imply the need for a series of lemmas on the actions of \texttt{load} and \texttt{store} to ensure correctness. The first lemma required has the following statement: