Changeset 1277 for Deliverables/D3.2/Report/report.tex
- Timestamp:
- Sep 26, 2011, 6:58:43 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.2/Report/report.tex
r1261 r1277 255 255 256 256 \subsection{Runtime functions} 257 % TODO: this hasn't been implemented yet 257 258 Some operations on integers do not have a simple translation to the target 259 machine code. In particular, we need to replace operations for 16 and 32-bit 260 division and most bitwise shifts with calls to runtime functions. These 261 functions need to be added to the program at an early stage because of their 262 impact on execution time: any loops must be available to our labelling 263 mechanism so that we can report on how long the resulting machine code will 264 take to execute. 265 266 We follow the prototype in replacing the affected expressions, which requires 267 us to break up expressions into multiple statements because function calls are 268 not permitted in \textsf{Clight} expressions. We may investigate moving these 269 substitutions to a later stage of the compiler if they prove difficult to 270 reason about. However, this would also require adjusting the semantics so 271 that the costs still appear in the evaluation of \textsf{Clight} programs. 272 273 The prototype adds the functions themselves by generating C code as text and 274 reparsing the program. This is unsuitable for formalization, so we generate 275 \textsf{Clight} abstract syntax trees directly. 258 276 259 277 \subsection{Conversion to Cminor} … … 418 436 \section{Conclusion} 419 437 438 We have formalized the front-end of the \cerco{} compiler in the \matita{} 439 proof assistant, and shown that invariants can be added to the intermediate 440 languages to help show properties of it. This work provides a solid basis for 441 the compiler correctness proofs in task 3.4. 442 420 443 \bibliographystyle{plain} 421 444 \bibliography{report}
Note: See TracChangeset
for help on using the changeset viewer.