Changeset 1277


Ignore:
Timestamp:
Sep 26, 2011, 6:58:43 PM (8 years ago)
Author:
campbell
Message:

Runtime functions and conclusion for D3.2.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.2/Report/report.tex

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