# Changeset 1370

Ignore:
Timestamp:
Oct 14, 2011, 10:56:50 AM (8 years ago)
Message:

D3.3: Added a subsection on the SmallstepExec?.ma definitions, plus a few related
 r1346 The semantics for many of the languages in the compiler share some core parts: the memory model, environments, runtime values, definitions of operations and a monad for encapsulating failure and I/O (using resumptions).  The executable the memory model, environments, runtime values, definitions of operations, a monad for encapsulating failure and I/O (using resumptions), and a common abstraction for small-step executable semantics.  The executable memory model was ported from CompCert as part of the work on \textsf{Clight} and was reused for the front-end languages\footnote{However, it is likely that we will revise the memory model to make it better suited for describing the back-end of our compiler.}.  The failure and I/O monad was introduced in the we will revise the memory model to make it better suited for describing all of our compiler, not just the front-end.}.  The failure and I/O monad was introduced in the previous deliverable on \textsf{Clight}~\cite[\S4.2]{d3.1}.  In all of the languages except \textsf{Clight} we have a basic form of type, \lstinline'typ' A common semantics is given for these operations in the form of simple CIC functions on the operation and runtime values. \subsection{Presentation of small-step executable semantics} \label{sec:smallstepexec} Each language's semantics is described by an instantiation of two records for defining transition systems.  We already use these to animate the semantics of the languages for testing, but they will also be used to state the simulation properties we will prove in Tasks~3.4 and~4.4. First we describe suitable transition systems, \begin{lstlisting} record trans_system (outty:Type[0]) (inty:outty $\rightarrow$ Type[0]) : Type[2] := { global : Type[1] ; state  : global $\rightarrow$ Type[0] ; is_final : $\forall$g. state g $\rightarrow$ option int ; step : $\forall$g. state g $\rightarrow$ IO outty inty (trace$\times$(state g)) }. \end{lstlisting} where we have some type of \lstinline'global' data that remains fixed throughout evaluation (typically used for the global environment), a type for states, a function to detect a final successful state and a step function which can also return an error or request for I/O.  The type of states may depend on the fixed data so that we will be able to add invariants asserting that (for example) all the global variables referenced by the program state exist. We also define a coinductive description of executions and a cofixpoint to produce them.  The second record extends the transition system with a type of programs and functions to initialise the transition system: \begin{lstlisting} record fullexec (outty:Type[0]) (inty:outty $\rightarrow$ Type[0]) : Type[2] := { program : Type[0] ; es1 :> trans_system outty inty ; make_global : program $\rightarrow$ global ?? es1 ; make_initial_state : $\forall$p:program. res (state ?? es1 (make_global p)) }. \end{lstlisting} Finally another function is given which uses them to produce a full execution starting from the program alone. \section{\textsf{Clight} modifications} The definition of the semantics is routine: a functional definition of a single small step of the machine is given, reusing the memory model, single small-step of the machine is given, reusing the memory model, environments, arithmetic and operations mentioned above. terms for the syntax of each language described above. A few common definitions were added for animating the small step semantics definitions for any of the front-end languages in \matita.  We then used a small selection of test cases to ensure basic functionality.  However, this is still a time consuming process, so more testing will carried out once the extraction of CIC terms to \ocaml{} programs is implemented in \matita. A few common definitions were added for animating the small-step semantics of any of the front-end languages in \matita{}, given a bound on the number of steps to execute and any input required.  These use the definitions described in Section~\ref{sec:smallstepexec} to perform the actual execution.  We then used a small selection of test cases to ensure basic functionality.  However, this is still a time consuming process, so more testing will carried out once the extraction of CIC terms to \ocaml{} programs is implemented in \matita. \section{Embedding invariants}