Changeset 1346
 Timestamp:
 Oct 10, 2011, 6:18:10 PM (9 years ago)
 Location:
 Deliverables
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.2/Report/report.tex
r1317 r1346 99 99 \vspace*{7cm} 100 100 \paragraph{Abstract} 101 We describe the translation of the front 101 We describe the translation of the frontend of the \cerco{} compiler from the 102 102 \ocaml{} prototype to the Calculus of Inductive Constructions (CIC) in the 103 103 \matita{} proof assistant. This transforms programs in the Clike … … 110 110 will assist in future work proving correctness properties. 111 111 112 This work was Task~3.2 of the \cerco{} project, translating the prototype 113 described in Deliverable~2.2~\cite{d2.2} into CIC using the intermediate languages 114 formalized in Deliverables~3.1~\cite{d3.1} and~3.3. It will feed into the frontend 115 correctness proofs in Task~3.4 and is a counterpart to the backend 116 formalization in Task~4.2. 117 112 118 \newpage 113 119 … … 115 121 116 122 % TODO: clear up any ize vs ise 117 % TODO: clear up any "front end" vs "frontend" 118 % TODO: clear up any mentions of languages that aren't textsf'd. 119 % TODO: fix unicode in listings 120 % TODO: make it clear that our correctness is intended to go beyond compcert's 121 % TODO: capitalise deliverable/task? 123 % CHECK: clear up any "front end" vs "frontend" 124 % CHECK: clear up any mentions of languages that aren't textsf'd. 125 % CHECK: fix unicode in listings 126 % CHEKC: capitalise deliverable/task when referring to a particular one 122 127 123 128 \section{Introduction} … … 154 159 \> $\downarrow$ \> transform to RTL graph\\ 155 160 \textsf{RTLabs}\\ 156 \> $\downarrow$ \> start of target specific back end\\161 \> $\downarrow$ \> start of target specific backend\\ 157 162 \>\quad \vdots 158 163 \end{tabbing} … … 170 175 171 176 \item[\textsf{RTLabs}]  a language in the form of a control flow graph 172 which retains the values and front 177 which retains the values and frontend operations from \textsf{Cminor} 173 178 \end{description} 174 179 More details on the formalisation of the syntax and semantics of these 175 languages can be found in the accompanying deliverable 3.4.180 languages can be found in the accompanying Deliverable 3.4. 176 181 Development of the formalized frontend was conducted in concert with the 177 182 development of these intermediate languages to facilitate testing. … … 205 210 \end{itemize} 206 211 207 This document describes the formalized front 212 This document describes the formalized frontend after these changes. 208 213 209 214 \section{\textsf{Clight} phases} … … 243 248 This has been implemented in \matita. We have also performed a few proofs that 244 249 the arithmetic behind these changes is correct to gain confidence in the 245 technique. During task 3.4 we will extend these proofs to cover more250 technique. During Task 3.4 we will extend these proofs to cover more 246 251 operations and show that the semantics of the expressions are equivalent, not 247 252 just the underlying arithmetic. … … 252 257 simple recursive definition, and was straightforward to port to \matita. The 253 258 generation of cost labels was handled by our generic identifiers code, 254 described in the accompanying deliverable 3.3 on intermediate languages.259 described in the accompanying Deliverable 3.3 on intermediate languages. 255 260 256 261 \subsection{Runtime functions} … … 275 280 \textsf{Clight} abstract syntax trees directly. 276 281 277 \subsection{Conversion to Cminor}282 \subsection{Conversion to \textsf{Cminor}} 278 283 279 284 The conversion to \textsf{Cminor} performs two essential tasks. First, it … … 346 351 formed early in the compilation process. 347 352 348 This work overlaps with deliverable 3.3 (where more details of the additions353 This work overlaps with Deliverable 3.3 (where more details of the additions 349 354 to the syntax and semantics of the intermediate languages can be found) and 350 task 3.4 on the correctness of the compiler. Thus this work is experimental351 in nature, and will evolve during task 3.4.355 Task 3.4 on the correctness of the compiler. Thus this work is experimental 356 in nature, and will evolve during Task 3.4. 352 357 353 358 The use of the invariants follows a common pattern. Each language embeds … … 428 433 429 434 To provide some early testing and bug fixing of this code we constructed it in 430 concert with the executable semantics described in deliverable 3.3, and435 concert with the executable semantics described in Deliverable 3.3, and 431 436 \matita{} term pretty printers in the prototype compiler. Using these, we 432 437 were able to test the phases individually and together by running programs … … 439 444 proof assistant, and shown that invariants can be added to the intermediate 440 445 languages to help show properties of it. This work provides a solid basis for 441 the compiler correctness proofs in task 3.4.446 the compiler correctness proofs in Task 3.4. 442 447 443 448 \bibliographystyle{plain} 
Deliverables/D3.3/Report/report.tex
r1317 r1346 68 68 \bf 69 69 Report n. D3.3\\ 70 Executable Formal Semantics of front 70 Executable Formal Semantics of frontend intermediate languages\\ 71 71 \end{LARGE} 72 72 \end{center} … … 99 99 \vspace*{7cm} 100 100 \paragraph{Abstract} 101 We report on the formalization of the front 101 We report on the formalization of the frontend intermediate languages for the 102 102 \cerco{} project's compiler using executable semantics in the \matita{} proof 103 103 assistant. This includes common definitions for fresh identifier handling, 104 $n$bit arithmetic and operations and testing of the s meantics. We also104 $n$bit arithmetic and operations and testing of the semantics. We also 105 105 consider embedding invariants into the semantics for showing correctness 106 106 properties. 107 107 108 This work was Task~3.3 of the \cerco{} project and the languages that were 109 formalized were first described in Deliverable~2.1~\cite{d2.1}. They are used 110 by the formalized frontend in Task~3.2 to provide the syntax for the 111 transformations, and to test them by animating programs in the executable 112 semantics. It will also be a crucial part of the specifications for the 113 correctness results in Task~3.4. 114 108 115 \newpage 109 116 110 117 \tableofcontents 111 118 112 % TODO: clear up any ize vs ise113 % TODO: clear up any "front end" vs "frontend"114 % TODO: clear up any mentions of languages that aren't textsf'd.115 % TODO: fix unicode in listings119 % CHECK: clear up any ize vs ise 120 % CHECK: clear up any "front end" vs "frontend" 121 % CHECK: clear up any mentions of languages that aren't textsf'd. 122 % CHECK: fix unicode in listings 116 123 117 124 \section{Introduction} 118 125 119 This work formalizes the front 126 This work formalizes the frontend intermediate languages from the \cerco{} 120 127 prototype compiler, described in previous deliverables~\cite{d2.1,d2.2}. The 121 front 128 frontend of the compiler is summarized in Figure~\ref{fig:summary} including 122 129 the intermediate languages and the compiler passes described in the 123 accompanying deliverable 3.2. We have also refined parts of the formal130 accompanying Deliverable 3.2. We have also refined parts of the formal 124 131 development that are used for several of the languages in the compiler. 125 132 126 The input language to the formalized front 133 The input language to the formalized frontend is the \textsf{Clight} 127 134 language. The executable semantics for this language were presented in a 128 135 previous deliverable~\cite{d3.1}. Here we will report on some … … 134 141 done in the Calculus of Inductive Constructions (CIC), as implemented in the 135 142 \matita{} proof assistant. These definitions will be essential for the 136 correctness proofs of the compiler in task 3.4.143 correctness proofs of the compiler in Task 3.4. 137 144 138 145 Finally, we will report on work to add several invariants to the 139 languages. This activity overlaps with task 3.4 on the correctness of the140 compiler front 146 languages. This activity overlaps with Task 3.4 on the correctness of the 147 compiler frontend. However, the use of dependent types mean that this work 141 148 is tied closely to the definition of the languages and the transformations of 142 the front end in task 3.2. By considering it now we can experiment with and149 the frontend in Task 3.2. By considering it now we can experiment with and 143 150 judge its impact on the formal semantics, and how feasible retrofitting such 144 151 invariants is. … … 158 165 simplification\\ 159 166 \textsf{Cminor}\\ 160 \> $\downarrow$ \> generate global variable initiali sation code\\167 \> $\downarrow$ \> generate global variable initialization code\\ 161 168 \> $\downarrow$ \> transform to RTL graph\\ 162 169 \textsf{RTLabs}\\ 163 \> $\downarrow$ \> start of target specific back end\\170 \> $\downarrow$ \> start of target specific backend\\ 164 171 \>\quad \vdots 165 172 \end{tabbing} 166 173 \end{minipage} 167 174 \end{center} 168 \caption{Front 175 \caption{Frontend languages and transformations} 169 176 \label{fig:summary} 170 177 \end{figure} … … 189 196 a monad for encapsulating failure and I/O (using resumptions). The executable 190 197 memory model was ported from CompCert as part of the work on \textsf{Clight} 191 and was reused for the front 198 and was reused for the frontend languages\footnote{However, it is likely that 192 199 we will revise the memory model to make it better suited for describing the 193 200 backend of our compiler.}. The failure and I/O monad was introduced in the … … 234 241 235 242 The bit vectors in~\cite{d4.1} also came equipped with some basic arithmetic 236 for the target semantics. The front 243 for the target semantics. The frontend required these operations to be 237 244 generalized and extended. In particular, we required operations such as zero 238 245 and sign extension and translation between bit vectors and full integers. It … … 242 249 frontend semantics. 243 250 244 \subsection{Front 245 246 The two front 251 \subsection{Frontend operations} 252 253 The two frontend intermediate languages, \textsf{Cminor} and \textsf{RTLabs}, 247 254 share the same set of operations on values. They differ from 248 255 \textsf{Clight}'s operations by incorporating casts and by having a separate … … 274 281 is similar to the prototype, except that the types attached to expressions are 275 282 restricted so that some corner cases are ruled out in the \textsf{Cminor} to 276 \textsf{RTLabs} stage (see the accompanying deliverable 3.2 for details):283 \textsf{RTLabs} stage (see the accompanying Deliverable 3.2 for details): 277 284 \begin{lstlisting} 278 285 inductive expr : typ $\rightarrow$ Type[0] ≝ … … 289 296 In principle we could extend this to statically ensure that only welltyped 290 297 \textsf{Cminor} expressions are considered, and we will consider this as part 291 of the work on correctness in task 3.4.298 of the work on correctness in Task 3.4. 292 299 293 300 We also provide a variant of the syntax where the only initialization data is … … 311 318 prototype compiler. Some of the syntax is shown below, including the type of 312 319 the control flow graphs. The same common elements are used as for \textsf{Cminor}, 313 including the front 320 including the frontend operations mentioned above. 314 321 315 322 \begin{lstlisting}[language=matita] … … 339 346 340 347 To provide some assurance that the semantics were properly implemented, and to 341 support the testing described in the accompanying deliverable 3.2, we have348 support the testing described in the accompanying Deliverable 3.2, we have 342 349 adapted the pretty printers in the prototype compiler to produce \matita{} 343 350 terms for the syntax of each language described above. 344 351 345 352 A few common definitions were added for animating the small step semantics 346 definitions for any of the front 353 definitions for any of the frontend languages in \matita. We then used a 347 354 small selection of test cases to ensure basic functionality. However, this is 348 355 still a time consuming process, so more testing will carried out once the … … 362 369 involves manipulating the syntax and semantics of the intermediate languages 363 370 (the present work), the encoding of the frontend compiler phases in \matita{} 364 ( task 3.2) and the correctness of the frontend (task 3.4). Thus this work is371 (Task 3.2) and the correctness of the frontend (Task 3.4). Thus this work is 365 372 rather experimental; it is being carried out on branches in our source code 366 repository and the final form will be decided and merged in during task 3.4.373 repository and the final form will be decided and merged in during Task 3.4. 367 374 368 375 So far we have tried adding two forms of invariant  one using dependent … … 474 481 475 482 The \textsf{Clight} semantics can be amended to use these invariants, although 476 the main benefit is for the compiler stages (see the accompanying deliverable483 the main benefit is for the compiler stages (see the accompanying Deliverable 477 484 3.2 for details). The semantics require the invariants to be added to the 478 485 state and continuations. It was convenient to split the continuations between … … 491 498 presence of proof terms and more dependent pattern matching in the semantics 492 499 will have on the complexity of future correctness proofs. We plan to examine 493 this issue during task 3.4.500 this issue during Task 3.4. 494 501 495 502 We use a similar method to specify the invariant that the \textsf{RTLabs} … … 503 510 We have developed executable semantics for each of the frontend languages of 504 511 the \cerco{} compiler. These will form the basis of the correctness 505 statements for each stage of the compiler in task 3.4. We have also shown512 statements for each stage of the compiler in Task 3.4. We have also shown 506 513 that useful invariants can be added as dependent types, and intend to use 507 514 these in subsequent work.
Note: See TracChangeset
for help on using the changeset viewer.