Changeset 1752 for Deliverables/D1.2/CompilerProofOutline
- Timestamp:
- Feb 24, 2012, 5:18:22 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/CompilerProofOutline/outline.tex
r1751 r1752 61 61 62 62 In the last section we finally present an estimation of the effort required 63 for the certification in Matita of the compiler .63 for the certification in Matita of the compiler and we draw conclusions. 64 64 65 65 \section{Front-end: Clight to RTLabs} … … 321 321 322 322 \begin{displaymath} 323 \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 324 \end{displaymath} 325 326 In the front-end, we have both integer and float values, where integer values are `sized, along with null values and pointers. 327 In the back-end memory model, floats values are no longer present, as floating point arithmetic is not supported by the CerCo compiler. 328 However, the back-end memory model introduces an undefined value ($\bot$) and sized pointer values. 329 330 We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}. 323 \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 324 \end{displaymath} 325 326 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 327 representables in a byte, but some others require more bits. 328 329 In the back-end model all values are meant to be represented in a single byte. 330 Values can thefore be undefined, be one byte long integers or be indexed 331 fragments of a pointer, null or not. Floats values are no longer present, as floating point arithmetic is not supported by the CerCo compiler. 332 333 The $\sigma$ map implements a one-to-many relation: a single front-end value 334 is mapped to a sequence of back-end values when its size is more then one byte. 335 336 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 337 thought as an instance of a generic \texttt{Mem} data type parameterized over 338 the kind of values stored in memory. 331 339 332 340 \begin{displaymath} … … 337 345 338 346 \begin{displaymath} 339 \mathtt{Block} ::= \mathtt{Region} \ cup\mathtt{ID}347 \mathtt{Block} ::= \mathtt{Region} \times \mathtt{ID} 340 348 \end{displaymath} 341 349 … … 356 364 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. 357 365 In contrast, the layout of sized integer values in the back-end memory model consists of a series of byte-sized `chunks': 366 358 367 \begin{center} 359 \begin{picture}(2, 2) 360 \put(-150,-20){\framebox(25,25)[c]{\texttt{v}}} 361 \put(-125,-20){\framebox(25,25)[c]{\texttt{4}}} 362 \put(-100,-20){\framebox(25,25)[c]{\texttt{cont}}} 363 \put(-75,-20){\framebox(25,25)[c]{\texttt{cont}}} 364 \put(-50,-20){\framebox(25,25)[c]{\texttt{cont}}} 365 \put(-15,-10){\vector(1, 0){30}} 366 \put(25,-20){\framebox(25,25)[c]{\texttt{\texttt{v1}}}} 367 \put(50,-20){\framebox(25,25)[c]{\texttt{\texttt{v2}}}} 368 \put(75,-20){\framebox(25,25)[c]{\texttt{\texttt{v3}}}} 369 \put(100,-20){\framebox(25,25)[c]{\texttt{\texttt{v4}}}} 368 \begin{picture}(0, 25) 369 \put(-125,0){\framebox(25,25)[c]{\texttt{v,4}}} 370 \put(-100,0){\framebox(25,25)[c]{\texttt{cont}}} 371 \put(-75,0){\framebox(25,25)[c]{\texttt{cont}}} 372 \put(-50,0){\framebox(25,25)[c]{\texttt{cont}}} 373 \put(-15,10){\vector(1, 0){30}} 374 \put(25,0){\framebox(25,25)[c]{\texttt{\texttt{v$_1$}}}} 375 \put(50,0){\framebox(25,25)[c]{\texttt{\texttt{v$_2$}}}} 376 \put(75,0){\framebox(25,25)[c]{\texttt{\texttt{v$_3$}}}} 377 \put(100,0){\framebox(25,25)[c]{\texttt{\texttt{v$_4$}}}} 370 378 \end{picture} 371 379 \end{center} 380 381 Chunks for pointers are pairs made of the original pointer and the index of 382 the chunk. Therefore, when assembling the chunks together, we can always 383 recognize if all chunks refer to the same value or if the operation is 384 meaningless. 385 372 386 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. 373 387 The first lemma required has the following statement:
Note: See TracChangeset
for help on using the changeset viewer.