# Changeset 3656

Ignore:
Timestamp:
Mar 16, 2017, 12:17:13 PM (9 months ago)
Message:

cannibalising bits of project report for compiler proof section

Location:
Papers/jar-cerco-2017
Files:
2 edited

### Legend:

Unmodified
 r3615 \section{Compiler proof} \label{sect.compiler.proof} \subsection{A brief overview of the backend compilation chain} \label{subsect.brief.overview.backend.compilation.chain} The Matita compiler's backend consists of five distinct intermediate languages: RTL, RTLntl, ERTL, LTL and LIN. A sixth language, RTLabs, serves as the entry point of the backend and the exit point of the frontend. RTL, RTLntl, ERTL and LTL are control flow graph based' languages, whereas LIN is a linearised language, the final language before translation to assembly. We now briefly discuss the properties of the intermediate languages, and discuss the various transformations that take place during the translation process: \paragraph{RTLabs ((Abstract) Register Transfer Language)} As mentioned, this is the final language of the compiler's frontend and the entry point for the backend. This language uses pseudoregisters, not hardware registers.\footnote{There are an unbounded number of pseudoregisters.  Pseudoregisters are converted to hardware registers or stack positions during register allocation.} Functions still use stackframes, where arguments are passed on the stack and results are stored in addresses. During the pass to RTL instruction selection is carried out. \paragraph{RTL (Register Transfer Language)} This language uses pseudoregisters, not hardware registers. Tailcall elimination is carried out during the translation from RTL to RTLntl. \paragraph{RTLntl (Register Transfer Language --- No Tailcalls)} This language is a pseudoregister, graph based language where all tailcalls are eliminated. RTLntl is not present in the O'Caml compiler, the RTL language is reused for this purpose. \paragraph{ERTL (Explicit Register Transfer Language)} This is a language very similar to RTLntl. However, the calling convention is made explicit, in that functions no longer receive and return inputs and outputs via a high-level mechanism, but rather use stack slots or hadware registers. The ERTL to LTL pass performs the following transformations: liveness analysis, register colouring and register/stack slot allocation. \paragraph{LTL (Linearisable Transfer Language)} Another graph based language, but uses hardware registers instead of pseudoregisters. Tunnelling (branch compression) should be implemented here. \paragraph{LIN (Linearised)} This is a linearised form of the LTL language; function graphs have been linearised into lists of statements. All registers have been translated into hardware registers or stack addresses. This is the final stage of compilation before translating directly into assembly language. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% % SECTION.                                                                    % %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \section{The backend intermediate languages in Matita} \label{sect.backend.intermediate.languages.matita} We now discuss the encoding of the compiler backend languages in the Calculus of Constructions proper. We pay particular heed to changes that we made from the O'Caml prototype. In particular, many aspects of the backend languages have been unified into a single joint' language. We have also made heavy use of dependent types to reduce spurious partiality' and to encode invariants. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% % SECTION.                                                                    % %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \subsection{Abstracting related languages} \label{subsect.abstracting.related.languages} The O'Caml compiler is written in the following manner. Each intermediate language has its own dedicated syntax, notions of internal function, and so on. Here, we make a distinction between internal functions'---other functions that are explicitly written by the programmer---and external functions', which belong to external library and require explictly linking. In particular, IO can be seen as a special case of the external function' mechanism. Internal functions are represented as a record consisting of a sequential structure of statements, entry and exit points to this structure, and other book keeping devices. This sequential structure can either be a control flow graph or a linearised list of statements, depending on the language. Translations between intermediate language map syntaxes to syntaxes, and internal function representations to internal function representations explicitly. This is a perfectly valid way to write a compiler, where everything is made explicit, but writing a \emph{verified} compiler poses new challenges. In particular, we must look ahead to see how our choice of encodings will affect the size and complexity of the forthcoming proofs of correctness. We now discuss some abstractions, introduced in the Matita code, which we hope will make our proofs shorter, amongst other benefits. \paragraph{Changes between languages made explicit} Due to the bureaucracy inherent in explicating each intermediate language's syntax in the O'Caml compiler, it can often be hard to see exactly what changes between each successive intermediate language. By abstracting the syntax of the RTL, ERTL, LTL and LIN intermediate languages, we make these changes much clearer. Our abstraction takes the following form: \begin{lstlisting} inductive joint_instruction (p: params__) (globals: list ident): Type[0] := | COMMENT: String $\rightarrow$ joint_instruction p globals ... | INT: generic_reg p $\rightarrow$ Byte $\rightarrow$ joint_instruction p globals ... | OP1: Op1 $ightarrow$ acc_a_reg p $ightarrow$ acc_a_reg p $ightarrow$ joint_instruction p globals ... | extension: extend_statements p $\rightarrow$ joint_instruction p globals. \end{lstlisting} We first note that for the majority of intermediate languages, many instructions are shared. However, these instructions expect different register types (either a pseudoregister or a hardware register) as arguments. We must therefore parameterise the joint syntax with a record of parameters that will be specialised to each intermediate language. In the type above, this parameterisation is realised with the \texttt{params\_\_} record. As a result of this parameterisation, we have also added a degree of type safety' to the intermediate languages' syntaxes. In particular, we note that the \texttt{OP1} constructor expects quite a specific type, in that the two register arguments must both be what passes for the accumulator A in that language. In some languages, for example LIN, this is the hardware accumulator, whilst in others this is any pseudoregister. Contrast this with the \texttt{INT} constructor, which expects a \texttt{generic\_reg}, corresponding to an arbitrary' register type. Further, we note that some intermediate languages have language specific instructions (i.e. the instructions that change between languages). We therefore add a new constructor to the syntax, \texttt{extension}, which expects a value of type \texttt{extend\_statements p}. As \texttt{p} varies between intermediate languages, we can provide language specific extensions to the syntax of the joint language. For example, ERTL's extended syntax consists of the following extra statements: \begin{lstlisting} inductive ertl_statement_extension: Type[0] := | ertl_st_ext_new_frame: ertl_statement_extension | ertl_st_ext_del_frame: ertl_statement_extension | ertl_st_ext_frame_size: register $\rightarrow$ ertl_statement_extension. \end{lstlisting} These are further packaged into an ERTL specific instance of \texttt{params\_\_} as follows: \begin{lstlisting} definition ertl_params__: params__ := mk_params__ register register ... ertl_statement_extension. \end{lstlisting} \paragraph{Shared code, reduced proofs} Many features of individual backend intermediate languages are shared with other intermediate languages. For instance, RTLabs, RTL, ERTL and LTL are all graph based languages, where functions are represented as a control flow graph of statements that form their bodies. Functions for adding statements to a graph, searching the graph, and so on, are remarkably similar across all languages, but are duplicated in the O'Caml code. As a result, we chose to abstract the representation of internal functions for the RTL, ERTL, LTL and LIN intermediate languages into a joint' representation. This representation is parameterised by a record that dictates the layout of the function body for each intermediate language. For instance, in RTL, the layout is graph like, whereas in LIN, the layout is a linearised list of statements. Further, a generalised way of accessing the successor statement to the one currently under consideration is needed, and so forth. Our joint internal function record looks like so: \begin{lstlisting} record joint_internal_function (globals: list ident) (p:params globals) : Type[0] := { ... joint_if_params   : paramsT p; joint_if_locals   : localsT p; ... joint_if_code     : codeT ... p; ... }. \end{lstlisting} In particular, everything that can vary between differing intermediate languages has been parameterised. Here, we see the location where to fetch parameters, the listing of local variables, and the internal code representation has been parameterised. Other particulars are also parameterised, though here omitted. Hopefully this abstraction process will reduce the number of proofs that need to be written, dealing with internal functions of different languages characterised by parameters. \paragraph{Dependency on instruction selection} We note that the backend languages are all essentially post instruction selection languages'. The joint' syntax makes this especially clear. For instance, in the definition: \begin{lstlisting} inductive joint_instruction (p:params__) (globals: list ident): Type[0] := ... | INT: generic_reg p $\rightarrow$ Byte $\rightarrow$ joint_instruction p globals | MOVE: pair_reg p $\rightarrow$ joint_instruction p globals ... | PUSH: acc_a_reg p $\rightarrow$ joint_instruction p globals ... | extension: extend_statements p $\rightarrow$ joint_instruction p globals. \end{lstlisting} The capitalised constructors---\texttt{INT}, \texttt{MOVE}, and so on---are all machine specific instructions. Retargetting the compiler to another microprocessor, improving instruction selection, or simply enlarging the subset of the machine language that the compiler can use, would entail replacing these constructors with constructors that correspond to the instructions of the new target. We feel that this makes which instructions are target dependent, and which are not (i.e. those language specific instructions that fall inside the \texttt{extension} constructor) much more explicit. In the long term, we would really like to try to directly embed the target language in the syntax, in order to reuse the target language's semantics. \paragraph{Independent development and testing} We have essentially modularised the intermediate languages in the compiler backend. As with any form of modularisation, we reap benefits in the ability to independently test and develop each intermediate language separately, with the benefit of fixing bugs just once. \paragraph{Future reuse for other compiler projects} Another advantage of our modularisation scheme is the ability to quickly use and reuse intermediate languages for other compiler projects. For instance, in creating a cost-preserving compiler for a functional language, we may choose to target a linearised version of RTL directly. Adding such an intermediate language would involve the addition of just a few lines of code. \paragraph{Easy addition of new compiler passes} Under our modularisation and abstraction scheme, new compiler passes can easily be injected into the backend. We have a concrete example of this in the RTLntl language, an intermediate language that was not present in the original O'Caml code. To specify a new intermediate language we must simply specify, through the use of the statement extension mechanism, what differs in the new intermediate language from the joint' language, and configure a new notion of internal function record, by specialising parameters, to the new language. As generic code for the joint' language exists, for example to add statements to control flow graphs, this code can be reused for the new intermediate language. \paragraph{Possible commutations of translation passes} The backend translation passes of the CerCo compiler differ quite a bit from the CompCert compiler. In the CompCert compiler, linearisation occurs much earlier in the compilation chain, and passes such as register colouring and allocation are carried out on a linearised form of program. Contrast this with our own approach, where the code is represented as a graph for much longer. Similarly, in CompCert the calling conventions are enforced after register allocation, whereas we do register allocation before enforcing the calling convention. However, by abstracting the representation of intermediate functions, we are now much more free to reorder translation passes as we see fit. The linearisation process, for instance, now no longer cares about the specific representation of code in the source and target languages. It just relies on a common interface. We are therefore, in theory, free to pick where we wish to linearise our representation. This adds an unusual flexibility into the compilation process, and allows us to freely experiment with different orderings of translation passes. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% % SECTION.                                                                    % %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \subsection{Use of dependent types} \label{subsect.use.of.dependent.types} We see several potential ways in which a compiler can fail to compile a program: \begin{enumerate} \item The program is malformed, and there is no hope of making sense of the program. \item The compiler is buggy, or an invariant in the compiler is invalidated. \item An incomplete heuristic in the compiler fails. \item The compiled code exhausts some bounded resource, for instance the processor's code memory. \end{enumerate} Standard compilers can fail for all the above reasons. Certified compilers are only required to rule out the second class of failures, but they can still fail for all the remaining reasons. In particular, a compiler that systematically refuses to compile any well formed program is a sound compiler. On the contrary, we would like our certified compiler to fail only in the fourth case. We plan to achieve this with the following strategy. First, the compiler is abstracted over all incomplete heuristics, seen as total functions. To obtain executable code, the compiler is eventually composed with implementations of the abstracted strategies, with the composition taking care of any potential failure of the heuristics in finding a solution. Second, we reject all malformed programs using dependent types: only well-formed programs should typecheck and the compiler can be applied only to well-typed programs. Finally, exhaustion of bounded resources can be checked only at the very end of compilation. Therefore, all intermediate compilation steps are now total functions that cannot diverge, nor fail: these properties are directly guaranteed by the type system of Matita. Presently, the plan is not yet fulfilled. However, we are improving the implemented code according to our plan. We are doing this by progressively strenghthening the code through the use of dependent types. We detail the different ways in which dependent types have been used so far. First, we encode informal invariants, or uses of \texttt{assert false} in the O'Caml code, with dependent types, converting partial functions into total functions. There are numerous examples of this throughout the backend. For example, in the \texttt{RTLabs} to \texttt{RTL} transformation pass, many functions only make sense' when lists of registers passed to them as arguments conform to some specific length. For instance, the \texttt{translate\_negint} function, which translates a negative integer constant: \begin{lstlisting} definition translate_negint := $\lambda$globals: list ident. $\lambda$destrs: list register. $\lambda$srcrs: list register. $\lambda$start_lbl: label. $\lambda$dest_lbl: label. $\lambda$def: rtl_internal_function globals. $\lambda$prf: |destrs| = |srcrs|. (* assert here *) ... \end{lstlisting} The last argument to the function, \texttt{prf}, is a proof that the lengths of the lists of source and destination registers are the same. This was an assertion in the O'Caml code. Secondly, we make use of dependent types to make the Matita code correct by construction, and eventually the proofs of correctness for the compiler easier to write. For instance, many intermediate languages in the backend of the compiler, from RTLabs to LTL, are graph based languages. Here, function definitions consist of a graph (i.e. a map from labels to statements) and a pair of labels denoting the entry and exit points of this graph. Practically, we would always like to ensure that the entry and exit labels are present in the statement graph. We ensure that this is so with a dependent sum type in the \texttt{joint\_internal\_function} record, which all graph based languages specialise to obtain their own internal function representation: \begin{lstlisting} record joint_internal_function (globals: list ident) (p: params globals): Type[0] := { ... joint_if_code     : codeT $\ldots$ p; joint_if_entry    : $\Sigma$l: label. lookup $\ldots$ joint_if_code l $\neq$ None $\ldots$; ... }. \end{lstlisting} Here, \texttt{codeT} is a parameterised type representing the structure' of the function's body (a graph in graph based languages, and a list in the linearised LIN language). Specifically, the \texttt{joint\_if\_entry} is a dependent pair consisting of a label and a proof that the label in question is a vertex in the function's graph. A similar device exists for the exit label. We make use of dependent types also for another reason: experimentation. Namely, CompCert makes little use of dependent types to encode invariants. In contrast, we wish to make as much use of dependent types as possible, both to experiment with different ways of encoding compilers in a proof assistant, but also as a way of stress testing' Matita's support for dependent types. Moreover, at the moment we make practically no use of inductive predicates to specify compiler invariants and to describe the semantics of intermediate languages. On the contrary, all predicates are computable functions. Therefore, the proof style that we will adopt will be necessarily significantly different from, say, CompCert's one. At the moment, in Matita Russell-'-style reasoning (in the sense of~\cite{sozeau:subset:2006}) seems to be the best solution for working with computable functions. This style is heavily based on the idea that all computable functions should be specified using dependent types to describe their pre- and post-conditions. As a consequence, it is natural to add dependent types almost everywhere in the Matita compiler's codebase. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% % SECTION.                                                                    % %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \subsection{What we do not implement} \label{subsect.what.we.do.not.implement} There are several classes of functionality that we have chosen not to implement in the backend languages: \begin{itemize} \item \textbf{Datatypes and functions over these datatypes that are not supported by the compiler.} In particular, the compiler does not support the floating point datatype, nor accompanying functions over that datatype. At the moment, frontend languages within the compiler possess constructors corresponding to floating point code. These are removed during instruction selection (in the RTLabs to RTL transformation) using a daemon.\footnote{A Girardism.  An axiom of type \texttt{False}, from which we can prove anything.} However, at some point, we would like the front end of the compiler to recognise programs that use floating point code and reject them as being invalid. \item \textbf{Axiomatised components that will be implemented using external oracles.} Several large, complex pieces of compiler infrastructure, most noticably register colouring and fixed point calculation during liveness analysis have been axiomatised. This was already agreed upon before the start of the project, and is clearly marked in the project proposal, following comments by those involved with the CompCert project about the difficulty in formalising register colouring in that project. Instead, these components are axiomatised, along with the properties that they need to satisfy in order for the rest of the compilation chain to be correct. These axiomatised components are found in the ERTL to LTL pass. It should be noted that these axiomatised components fall into the following pattern: whilst their implementation is complex, and their proof of correctness is difficult, we are able to quickly and easily verify that any answer that they provide is correct. Therefore, we plan to provide implementations in OCaml only, and to provide certified verifiers in Matita. At the moment, the implementation of the certified verifiers is left as future work. \item \textbf{A few non-computational proof obligations.} A few difficult-to-close, but non-computational (i.e. they do not prevent us from executing the compiler inside Matita), proof obligations have been closed using daemons in the backend. These proof obligations originate with our use of dependent types for expressing invariants in the compiler. However, here, it should be mentioned that many open proof obligations are simply impossible to close until we start to obtain stronger invariants from the proof of correctness for the compiler proper. In particular, in the RTLabs to RTL pass, several proof obligations relating to lists of registers stored in a local environment' appear to fall into this pattern. \item \textbf{Branch compression (tunnelling).} This was a feature of the O'Caml compiler. It is not yet currently implemented in the Matita compiler. This feature is only an optimisation, and will not affect the correctness of the compiler. \item \textbf{Real' tailcalls} For the time being, tailcalls in the backend are translated to vanilla' function calls during the ERTL to LTL pass. This follows the O'Caml compiler, which did not implement tailcalls, and did this simplification step. Real' tailcalls are being implemented in the O'Caml compiler, and when this implementation is complete, we aim to port this code to the Matita compiler. \end{itemize} %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% % SECTION.                                                                    % %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \section{Associated changes to O'Caml compiler} \label{sect.associated.changes.to.ocaml.compiler} At the moment, only bugfixes, but no architectural changes we have made in the Matita backend have made their way back into the O'Caml compiler. We do not see the heavy process of modularisation and abstraction as making its way back into the O'Caml codebase, as this is a significant rewrite of the backend code that is supposed to yield the same code after instantiating parameters, anyway. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% % SECTION.                                                                    % %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \section{Future work} \label{sect.future.work} As mentioned in Section~\ref{subsect.what.we.do.not.implement}, there are several unimplemented features in the compiler, and several aspects of the Matita code that can be improved in order to make currently partial functions total. We summarise this future work here: \begin{itemize} \item We plan to make use of dependent types to identify floating point' free programs and make all functions total over such programs. This will remove a swathe of uses of daemons. This should be routine. \item We plan to move expansion of integer modulus, and other related functions, into the instruction selection (RTLabs to RTL) phase. This will also help to remove a swathe of uses of daemons, as well as potentially introduce new opportunities for optimisations that we currently miss in expanding these instructions at the C-light level. \item We plan to close all existing proof obligations that are closed using daemons, arising from our use of dependent types in the backend. However, many may not be closable until we have completed Deliverable D4.4, the certification of the whole compiler, as we may not have invariants strong enough at the present time. \item We plan to port the O'Caml compiler's implementation of tailcalls when this is completed, and eventually port the branch compression code currently in the O'Caml compiler to the Matita implementation. This should not cause any major problems. \item We plan to validate the backend translations, removing any obvious bugs, by executing the translation inside Matita on small C programs. This is not critical, as the certification process will find all bugs anyway. \item We plan to provide certified validators for all results provided by external oracles written in OCaml. At the moment, we have axiomatized oracles for computing least fixpoints during liveness analysis, for colouring registers and for branch displacement in the assembler code. \end{itemize} \section{The back-end intermediate languages' semantics in Matita} \label{sect.backend.intermediate.languages.semantics.matita} %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% % SECTION.                                                                    % %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \subsection{Abstracting related languages} \label{subsect.abstracting.related.languages} As mentioned in the report for Deliverable D4.2, a systematic process of abstraction, over the OCaml code, has taken place in the Matita encoding. In particular, we have merged many of the syntaxes of the intermediate languages (i.e. RTL, ERTL, LTL and LIN) into a single joint' syntax, which is parameterised by various types. Equivalent intermediate languages to those present in the OCaml code can be recovered by specialising this joint structure. As mentioned in the report for Deliverable D4.2, there are a number of advantages that this process of abstraction brings, from code reuse to allowing us to get a clearer view of the intermediate languages and their structure. However, the semantics of the intermediate languages allow us to concretely demonstrate this improvement in clarity, by noting that the semantics of the LTL and the semantics of the LIN languages are identical. In particular, the semantics of both LTL and LIN are implemented in exactly the same way. The only difference between the two languages is how the next instruction to be interpreted is fetched. In LTL, this involves looking up in a graph, whereas in LTL, this involves fetching from a list of instructions. As a result, we see that the semantics of LIN and LTL are both instances of a single, more general language that is parametric in how the next instruction is fetched. Furthermore, any prospective proof that the semantics of LTL and LIN are identical is now almost trivial, saving a deal of work in Deliverable D4.4. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% % SECTION.                                                                    % %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \subsection{Type parameters, and their purpose} \label{subsect.type.parameters.their.purpose} We mentioned in the Deliverable D4.2 report that all joint languages are parameterised by a number of types, which are later specialised to each distinct intermediate language. As this parameterisation process is also dependent on designs decisions in the language semantics, we have so far held off summarising the role of each parameter. We begin the abstraction process with the \texttt{params\_\_} record. This holds the types of the representations of the different register varieties in the intermediate languages: \begin{lstlisting} record params__: Type[1] := { acc_a_reg: Type[0]; acc_b_reg: Type[0]; dpl_reg: Type[0]; dph_reg: Type[0]; pair_reg: Type[0]; generic_reg: Type[0]; call_args: Type[0]; call_dest: Type[0]; extend_statements: Type[0] }. \end{lstlisting} We summarise what these types mean, and how they are used in both the semantics and the translation process: \begin{center} \begin{tabular*}{\textwidth}{p{4cm}p{11cm}} Type & Explanation \\ \hline \texttt{acc\_a\_reg} & The type of the accumulator A register.  In some languages this is implemented as the hardware accumulator, whereas in others this is a pseudoregister.\\ \texttt{acc\_b\_reg} & Similar to the accumulator A field, but for the processor's auxilliary accumulator, B. \\ \texttt{dpl\_reg} & The type of the representation of the low eight bit register of the MCS-51's single 16 bit register, DPL.  Can be either a pseudoregister or the hardware DPL register. \\ \texttt{dph\_reg} & Similar to the DPL register but for the eight high bits of the 16-bit register. \\ \texttt{pair\_reg} & Various different move' instructions have been merged into a single move instruction in the joint language.  A value can either be moved to or from the accumulator in some languages, or moved to and from an arbitrary pseudoregister in others.  This type encodes how we should move data around the registers and accumulators. \\ \texttt{generic\_reg} & The representation of generic registers (i.e. those that are not devoted to a specific task). \\ \texttt{call\_args} & The actual arguments passed to a function.  For some languages this is simply the number of arguments passed to the function. \\ \texttt{call\_dest} & The destination of the function call. \\ \texttt{extend\_statements} & Instructions that are specific to a particular intermediate language, and which cannot be abstracted into the joint language. \end{tabular*} \end{center} As mentioned in the report for Deliverable D4.2, the record \texttt{params\_\_} is enough to be able to specify the instructions of the joint languages: \begin{lstlisting} inductive joint_instruction (p: params__) (globals: list ident): Type[0] := | COMMENT: String $\rightarrow$ joint_instruction p globals | COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals ... | OP1: Op1 $\rightarrow$ acc_a_reg p $\rightarrow$ acc_a_reg p $\rightarrow$ joint_instruction p globals | COND: acc_a_reg p $\rightarrow$ label $\rightarrow$ joint_instruction p globals ... \end{lstlisting} Here, we see that the instruction \texttt{OP1} (a unary operation on the accumulator A) can be given quite a specific type, through the use of the \texttt{params\_\_} data structure. Joint statements can be split into two subclasses: those who simply pass the flow of control onto their successor statement, and those that jump to a potentially remote location in the program. Naturally, as some intermediate languages are graph based, and others linearised, the passing act of passing control on to the successor' instruction can either be the act of following a graph edge in a control flow graph, or incrementing an index into a list. We make a distinction between instructions that pass control onto their immediate successors, and those that jump elsewhere in the program, through the use of \texttt{succ}, denoting the immediate successor of the current instruction, in the \texttt{params\_} record described below. \begin{lstlisting} record params_: Type[1] := { pars__ :> params__; succ: Type[0] }. \end{lstlisting} The type \texttt{succ} corresponds to labels, in the case of control flow graph based languages, or is instantiated to the unit type for the linearised language, LIN. Using \texttt{param\_} we can define statements of the joint language: \begin{lstlisting} inductive joint_statement (p:params_) (globals: list ident): Type[0] := | sequential: joint_instruction p globals $\rightarrow$ succ p $\rightarrow$ joint_statement p globals | GOTO: label $\rightarrow$ joint_statement p globals | RETURN: joint_statement p globals. \end{lstlisting} Note that in the joint language, instructions are linear', in that they have an immediate successor. Statements, on the other hand, consist of either a linear instruction, or a \texttt{GOTO} or \texttt{RETURN} statement, both of which can jump to an arbitrary place in the program. The conditional jump instruction COND is linear', since it has an immediate successor, but it also takes an arbitrary location (a label) to jump to. For the semantics, we need further parametererised types. In particular, we parameterise the result and parameter type of an internal function call in \texttt{params0}: \begin{lstlisting} record params0: Type[1] := { pars__' :> params__; resultT: Type[0]; paramsT: Type[0] }. \end{lstlisting} Here, \texttt{paramsT} and \texttt{resultT} typically are the (pseudo)registers that store the parameters and result of a function. We further extend \texttt{params0} with a type for local variables in internal function calls: \begin{lstlisting} record params1 : Type[1] := { pars0 :> params0; localsT: Type[0] }. \end{lstlisting} Again, we expand our parameters with types corresponding to the code representation (either a control flow graph or a list of statements). Further, we hypothesise a generic method for looking up the next instruction in the graph, called \texttt{lookup}. Note that \texttt{lookup} may fail, and returns an \texttt{option} type: \begin{lstlisting} record params (globals: list ident): Type[1] := { succ_ : Type[0]; pars1 :> params1; codeT : Type[0]; lookup: codeT $\rightarrow$ label $\rightarrow$ option (joint_statement (mk_params_ pars1 succ_) globals) }. \end{lstlisting} We now have what we need to define internal functions for the joint language. The first two universe' fields are only used in the compilation process, for generating fresh names, and do not affect the semantics. The rest of the fields affect both compilation and semantics. In particular, we have a description of the result, parameters and the local variables of a function. Note also that we have lifted the hypothesised \texttt{lookup} function from \texttt{params} into a dependent sigma type, which combines a label (the entry and exit points of the control flow graph or list) combined with a proof that the label is in the graph structure: \begin{lstlisting} record joint_internal_function (globals: list ident) (p:params globals) : Type[0] := { joint_if_luniverse: universe LabelTag; joint_if_runiverse: universe RegisterTag; joint_if_result   : resultT p; joint_if_params   : paramsT p; joint_if_locals   : localsT p; joint_if_stacksize: nat; joint_if_code     : codeT ... p; joint_if_entry    : $\Sigma$l: label. lookup ... joint_if_code l $\neq$ None ?; joint_if_exit     : $\Sigma$l: label. lookup ... joint_if_code l $\neq$ None ? }. \end{lstlisting} Naturally, a question arises as to why we have chosen to split up the parameterisation into so many intermediate records, each slightly extending earlier ones. The reason is because some intermediate languages share a host of parameters, and only differ on some others. For instance, in instantiating the ERTL language, certain parameters are shared with RTL, whilst others are ERTL specific: \begin{lstlisting} ... definition ertl_params__: params__ := mk_params__ register register register register (move_registers $\times$ move_registers) register nat unit ertl_statement_extension. ... definition ertl_params1: params1 := rtl_ertl_params1 ertl_params0. definition ertl_params: ∀globals. params globals := rtl_ertl_params ertl_params0. ... definition ertl_statement := joint_statement ertl_params_. definition ertl_internal_function := $\lambda$globals.joint_internal_function ... (ertl_params globals). \end{lstlisting} Here, \texttt{rtl\_ertl\_params1} are the common parameters of the ERTL and RTL languages: \begin{lstlisting} definition rtl_ertl_params1 := $\lambda$pars0. mk_params1 pars0 (list register). \end{lstlisting} The record \texttt{more\_sem\_params} bundles together functions that store and retrieve values in various forms of register: \begin{lstlisting} record more_sem_params (p:params_): Type[1] := { framesT: Type[0]; empty_framesT: framesT; regsT: Type[0]; empty_regsT: regsT; call_args_for_main: call_args p; call_dest_for_main: call_dest p; greg_store_: generic_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT; greg_retrieve_: regsT $\rightarrow$ generic_reg p $\rightarrow$ res beval; acca_store_: acc_a_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT; acca_retrieve_: regsT $\rightarrow$ acc_a_reg p $\rightarrow$ res beval; ... dpl_store_: dpl_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT; dpl_retrieve_: regsT $\rightarrow$ dpl_reg p $\rightarrow$ res beval; ... pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT; }. \end{lstlisting} Here, the fields \texttt{empty\_framesT}, \texttt{empty\_regsT}, \texttt{call\_args\_for\_main} and \texttt{call\_dest\_for\_main} are used for state initialisation. The fields \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively. Similarly, \texttt{pair\_reg\_move} implements the generic move instruction of the joint language. Here \texttt{framesT} is the type of stack frames, with \texttt{empty\_framesT} an empty stack frame. The two hypothesised values \texttt{call\_args\_for\_main} and \texttt{call\_dest\_for\_main} deal with problems with the \texttt{main} function of the program, and how it is handled. In particular, we need to know when the \texttt{main} function has finished executing. But this is complicated, in C, by the fact that the \texttt{main} function is explicitly allowed to be recursive (disallowed in C++). Therefore, to understand whether the exiting \texttt{main} function is really exiting, or just recursively calling itself, we need to remember the address to which \texttt{main} will return control once the initial call to \texttt{main} has finished executing. This is done with \texttt{call\_dest\_for\_main}, whereas \texttt{call\_args\_for\_main} holds the \texttt{main} function's arguments. We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}: \begin{lstlisting} record more_sem_params1 (globals: list ident) (p: params globals) : Type[1] := { more_sparams1 :> more_sem_params p; succ_pc: succ p $\rightarrow$ address $\rightarrow$ res address; pointer_of_label: genv ... p $\rightarrow$ pointer $\rightarrow$ label $\rightarrow$ res ($\Sigma$p:pointer. ptype p = Code); ... fetch_statement: genv ... p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$ res (joint_statement (mk_sem_params ... more_sparams1) globals); ... save_frame: address $\rightarrow$ nat $\rightarrow$ paramsT ... p $\rightarrow$ call_args p $\rightarrow$ call_dest p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$ res (state (mk_sem_params ... more_sparams1)); pop_frame: genv globals p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$ res ((state (mk_sem_params ... more_sparams1))); ... set_result: list val $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$ res (state (mk_sem_params ... more_sparams1)); exec_extended: genv globals p $\rightarrow$ extend_statements (mk_sem_params ... more_sparams1) $\rightarrow$ succ p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$ IO io_out io_in (trace $\times$ (state (mk_sem_params ... more_sparams1))) }. \end{lstlisting} The field \texttt{succ\_pc} takes an address, and a successor' label, and returns the address of the instruction immediately succeeding the one at hand. Here, \texttt{fetch\_statement} fetches the next statement to be executed. The fields \texttt{save\_frame} and \texttt{pop\_frame} manipulate stack frames. In particular, \texttt{save\_frame} creates a new stack frame on the top of the stack, saving the destination and parameters of a function, and returning an updated state. The field \texttt{pop\_frame} destructively pops a stack frame from the stack, returning an updated state. Further, \texttt{set\_result} saves the result of the function computation, and \texttt{exec\_extended} is a function that executes the extended statements, peculiar to each individual intermediate language. We bundle \texttt{params} and \texttt{sem\_params} together into a single record. This will be used in the function \texttt{eval\_statement} which executes a single statement of the joint language: \begin{lstlisting} record sem_params2 (globals: list ident): Type[1] := { p2 :> params globals; more_sparams2 :> more_sem_params2 globals p2 }. \end{lstlisting} \noindent The \texttt{state} record holds the current state of the interpreter: \begin{lstlisting} record state (p: sem_params): Type[0] := { st_frms: framesT ? p; pc: address; sp: pointer; isp: pointer; carry: beval; regs: regsT ? p; m: bemem }. \end{lstlisting} Here \texttt{st\_frms} represent stack frames, \texttt{pc} the program counter, \texttt{sp} the stack pointer, \texttt{isp} the internal stack pointer, \texttt{carry} the carry flag, \texttt{regs} the registers (hardware and pseudoregisters) and \texttt{m} external RAM. Note that we have two stack pointers, as we have two stacks: the physical stack of the MCS-51 microprocessor, and an emulated stack in external RAM. The MCS-51's own stack is minuscule, therefore it is usual to emulate a much larger, more useful stack in external RAM. We require two stack pointers as the MCS-51's \texttt{PUSH} and \texttt{POP} instructions manipulate the physical stack, and not the emulated one. We use the function \texttt{eval\_statement} to evaluate a single joint statement: \begin{lstlisting} definition eval_statement: $\forall$globals: list ident.$\forall$p:sem_params2 globals. genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) := ... \end{lstlisting} We examine the type of this function. Note that it returns a monadic action, \texttt{IO}, denoting that it may have an IO \emph{side effect}, where the program reads or writes to some external device or memory address. Monads and their use are further discussed in Subsection~\ref{subsect.use.of.monads}. Further, the function returns a new state, updated by the single step of execution of the program. Finally, a \emph{trace} is also returned, which records externally observable events', such as the calling of external functions and the emission of cost labels. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% % SECTION.                                                                    % %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \subsection{Use of monads} \label{subsect.use.of.monads} Monads are a categorical notion that have recently gained an amount of traction in functional programming circles. In particular, it was noted by Moggi that monads could be used to sequence \emph{effectful} computations in a pure manner. Here, effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state. A monad can be characterised by the following: \begin{itemize} \item A data type, $M$. For instance, the \texttt{option} type in OCaml or Matita. \item A way to inject' or lift' pure values into this data type (usually called \texttt{return}). We call this function \texttt{return} and say that it must have type $\alpha \rightarrow M \alpha$, where $M$ is the name of the monad. In our example, the lifting' function for the \texttt{option} monad can be implemented as: \begin{lstlisting} let return x = Some x \end{lstlisting} \item A way to sequence' monadic functions together, to form another monadic function, usually called \texttt{bind}. Bind has type $M \alpha \rightarrow (\alpha \rightarrow M \beta) \rightarrow M \beta$. We can see that bind unpacks' a monadic value, applies a function after unpacking, and repacks' the new value in the monad. In our example, the sequencing function for the \texttt{option} monad can be implemented as: \begin{lstlisting} let bind o f = match o with None -> None Some s -> f s \end{lstlisting} \item A series of algebraic laws that relate \texttt{return} and \texttt{bind}, ensuring that the sequencing operation does the right thing' by retaining the order of effects. These \emph{monad laws} should also be useful in reasoning about monadic computations in the proof of correctness of the compiler. \end{itemize} In the semantics of both front and back-end intermediate languages, we make use of monads. This monadic infrastructure is shared between the front-end and back-end languages. In particular, an IO' monad, signalling the emission of a cost label, or the calling of an external function, is heavily used in the semantics of the intermediate languages. Here, the monad's sequencing operation ensures that cost label emissions and function calls are maintained in the correct order. We have already seen how the \texttt{eval\_statement} function of the joint language is monadic, with type: \begin{lstlisting} definition eval_statement: $\forall$globals: list ident.$\forall$p:sem_params2 globals. genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) := ... \end{lstlisting} If we examine the body of \texttt{eval\_statement}, we may also see how the monad sequences effects. For instance, in the case for the \texttt{LOAD} statement, we have the following: \begin{lstlisting} definition eval_statement: $\forall$globals: list ident. $\forall$p:sem_params2 globals. genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) := $\lambda$globals, p, ge, st. ... match s with | LOAD dst addrl addrh ⇒ ! vaddrh $\leftarrow$ dph_retrieve ... st addrh; ! vaddrl $\leftarrow$ dpl_retrieve ... st addrl; ! vaddr $\leftarrow$ pointer_of_address $\langle$vaddrl,vaddrh$\rangle$; ! v $\leftarrow$ opt_to_res ... (msg FailedLoad) (beloadv (m ... st) vaddr); ! st $\leftarrow$ acca_store p ... dst v st; ! st $\leftarrow$ next ... l st ; ret ? $\langle$E0, st$\rangle$ \end{lstlisting} Here, we employ a certain degree of syntactic sugaring. The syntax \begin{lstlisting} ... ! vaddrh $\leftarrow$ dph_retrieve ... st addrh; ! vaddrl $\leftarrow$ dpl_retrieve ... st addrl; ... \end{lstlisting} is sugaring for the \texttt{IO} monad's binding operation. We can expand this sugaring to the following much more verbose code: \begin{lstlisting} ... bind (dph_retrieve ... st addrh) ($\lambda$vaddrh. bind (dpl_retrieve ... st addrl) ($\lambda$vaddrl. ...)) \end{lstlisting} Note also that the function \texttt{ret} is implementing the lifting', or return function of the \texttt{IO} monad. We believe the sugaring for the monadic bind operation makes the program much more readable, and therefore easier to reason about. In particular, note that the functions \texttt{dph\_retrieve}, \texttt{pointer\_of\_address}, \texttt{acca\_store} and \texttt{next} are all monadic. Note, however, that inside this monadic code, there is also another monad hiding. The \texttt{res} monad signals failure, along with an error message. The monad's sequencing operation ensures the order of error messages does not get rearranged. The function \texttt{opt\_to\_res} lifts an option type into this monad, with an error message to be used in case of failure. The \texttt{res} monad is then coerced into the \texttt{IO} monad, ensuring the whole code snippet typechecks. \subsection{Memory models} \label{subsect.memory.models} Currently, the semantics of the front and back-end intermediate languages are built around two distinct memory models. The front-end languages reuse the CompCert 1.6 memory model, whereas the back-end languages employ a version tailored to their needs. This split between the memory models reflects the fact that the front-end and back-end languages have different requirements from their memory models. In particular, the CompCert 1.6 memory model places quite heavy restrictions on where in memory one can read from. To read a value in this memory model, you must supply an address, complete with the size of chunk' to read following that address. The read is only successful if you attempt to read at a genuine value boundary', and read the appropriate amount of memory for that value. As a result, with that memory model you are unable to read the third byte of a 32-bit integer value directly from memory, for instance. This has some consequences for the compiler, namely an inability to write a \texttt{memcpy} routine. However, the CerCo memory model operates differently, as we need to move data piecemeal' between stacks in the back-end of the compiler. As a result, the back-end memory model allows one to read data at any memory location, not just on value boundaries. This has the advantage that we can successfully give a semantics to a \texttt{memcpy} routine in the back-end of the CerCo compiler (remembering that \texttt{memcpy} is nothing more than read a byte, copy a byte' repeated in a loop), an advantage over CompCert.  However, the front-end of CerCo cannot because its memory model and values are the similar to CompCert 1.6. More recent versions of CompCert's memory model have evolved in a similar direction, with a byte-by-byte representation of memory blocks.  However, there remains an important difference in the handling of pointer values in the rest of the formalisation.  In particular, in CompCert 1.10 only complete pointer values can be loaded in all of the languages in the compiler, whereas in CerCo we need to represent individual bytes of a pointer in the back-end to support our 8-bit target architecture. Right now, the two memory models are interfaced during the translation from RTLabs to RTL. It is an open question whether we will unify the two memory models, using only the back-end, bespoke memory model throughout the compiler, as the CompCert memory model seems to work fine for the front-end, where such byte-by-byte copying is not needed. However, should we decide to port the front-end to the new memory model, it has been written in such an abstract way that doing so would be relatively straightforward.