Changeset 1007

Ignore:
Timestamp:
Jun 20, 2011, 5:57:32 PM (9 years ago)
Message:

 r1005 Policies do not exist in only a limited number of circumstances: namely, if a pseudoinstruction attempts to jump to a label that does not exist, or the program is too large to fit in code memory even after shrinking jumps according to the best policy. The first case is an example of compiler error because of ill-formedness of the input. It does not count for the compiler completeness. We plan to employ dependent types in CerCo to restrict the domain of the compiler to those programs that are semantically correct and should be compiled. In particular, in CerCo we are also interested in completeness of compilation whereas previous formalizations only focused on correctness. best policy. The first circumstance is an example of a serious compiler error, as an ill-formed assembly program was generated. It does not count against the completeness of the assembler. We plan to employ dependent types in CerCo in order to restrict the domain of the compiler to those programs that are semantically correct' and should be compiled. In particular, in CerCo we are also interested in the completeness of the compilation process, whereas previous formalisations only focused on correctness. The rest of this paper is a detailed description of this proof. We leave extending this tracking of memory addresses throughout the whole of the MCS-51's address spaces as future work. It is interesting to compare our work to an industrial grade' assembler for the MCS-51: SDCC~\cite{sdcc:2011}. SDCC is the only open source C compiler available that targets the MCS-51 instruction set. It appears that all pseudojumps in SDCC assembly are expanded to \texttt{LJMP} instructions, the worst possible jump expansion policy from an efficiency point of view. Note that this policy is the only possible policy that can preserve the semantics of an assembly program during the assembly process. However, this comes at the expense of assembler completeness: the generated program may be too large to fit into code memory. In this respect, there is a fundamental trade-off between the completeness of the assembler and the efficiency of the assembled program. The definition and proof of an complete, optimal (in the sense that jump pseudoinstructions are expanded to the smallest possible opcode) and correct jump expansion policy is ongoing work. Aside from their application in verified compiler projects such as CerCo and CompCert, verified assemblers such as ours could also be applied to the verification of operating system kernels. Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009,klein:sel4:2010}. In essence, the work presented in this publication is one part of CerCo's extension over CompCert. \subsection{Source code} \label{subsect.source.code} \subsection{Resources} \label{subsect.resources} All files relating to our formalisation effort can be found online at~\url{http://cerco.cs.unibo.it}.