source: Deliverables/D1.2/Presentations/WP3.tex @ 2097

\documentclass[nopanel]{beamer}
\usepackage{graphicx,color}

\usetheme{Frankfurt}
\logo{\includegraphics[height=1.0cm]{fetopen.png}}

\usepackage[english]{babel}
%\usepackage{inputenc}


%\documentclass[nopanel,ucs]{beamer}
\usepackage[utf8x]{inputenc}
%\usepackage[T1,OT1]{fontenc}
%\usepackage{pifont}
%\usepackage{aeguill}
% using aeguill forces us to T1 everywhere, resulting in horribleness
%  \def\selectguillfont{\fontencoding{T1}\fontfamily{cmtt}\selectfont}%
%\def\guillemotleft{{\selectguillfont\symbol{19}}}%
%\def\guillemotright{{\selectguillfont\symbol{20}}}%
%\SetUnicodeOption{postscript}
%\usepackage{hyperref}
\usepackage{latexsym}
\usepackage{listings}

\def\cerco{CerCo}
\def\ocaml{OCaml}

\newcommand{\red}[1]{\textcolor{red}{#1}}
\newcommand{\blue}[1]{\textcolor{blue}{#1}}
\definecolor{darkgreen}{rgb}{0,0.4,0}
\newcommand{\green}[1]{\textcolor{darkgreen}{#1}}
\newcommand{\gray}[1]{\textcolor{gray}{#1}}

%\setbeamertemplate{footline}[page number]
%\setbeamertemplate{sidebar right}{}
\setbeamertemplate{navigation symbols}{}

\lstdefinelanguage{coq}
  {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record},
   morekeywords={[2]if,then,else},
  }

\lstdefinelanguage{matita}
  {keywords={definition,lemma,theorem,remark,inductive,record,qed,let,rec,match,with,Type,and,on,return},
   morekeywords={[2]whd,normalize,elim,cases,destruct},
   mathescape=true,
   morecomment=[n]{(*}{*)},
  }

\lstset{language=matita,basicstyle=\small\tt,columns=flexible,breaklines=false,
        keywordstyle=\color{red}\bfseries,
        keywordstyle=[2]\color{blue},
        commentstyle=\color{darkgreen},
        stringstyle=\color{blue},
        showspaces=false,showstringspaces=false}

\lstset{extendedchars=false}
\lstset{inputencoding=utf8x}
\DeclareUnicodeCharacter{8797}{:=}
\DeclareUnicodeCharacter{10746}{++}
\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}


\begin{document}

\title{CerCo Work Package 3\\
Verified Compiler --- Front-end}
\author{Brian Campbell\\ \scriptsize\smallskip
\href{mailto:Brian.Campbell@ed.ac.uk}{\texttt{Brian.Campbell@ed.ac.uk}}}
\institute{Laboratory for Foundations of Computer Science\\
The University of Edinburgh}
\date{March 16, 2011}
\frame{\titlepage}


\frame{
\frametitle{Achievements in period 2}

\begin{description}[T3.2]
\item[T3.2] \alert{Completed}: Matita encoding of compiler front-end
\item[T3.3] \alert{Completed}: Executable semantics for intermediate  languages
\item[T3.4] \alert{In progress}: Correctness proofs
\end{description}

\bigskip
Deliverables D3.2 and D3.3 submitted.

\bigskip
This talk is an interleaved presentation of these results.


}


\frame{
\frametitle{Outline}

\begin{itemize}
\item Shared definitions
%\item The front-end:
%\end{itemize}
%\vspace{-3ex}
\item \begin{tabbing}
\quad \= $\downarrow$ \quad \= \kill
\gray{\textsf{C} (unformalized)}\\
\> \gray{$\downarrow$} \> \gray{CIL parser (unformalized \ocaml)}\\
\textsf{Clight}\\
\> $\downarrow$ \> cast removal\\
\> \gray{$\downarrow$} \> \gray{add runtime functions}\\
\> $\downarrow$ \> cost labelling\\
\> $\downarrow$ \> stack variable allocation and control structure
 simplification\\
\textsf{Cminor}\\
\> $\downarrow$ \> generate global variable initialisation code\\
\> $\downarrow$ \> transform to RTL graph\\
\textsf{RTLabs}\\
\> \,\gray{\vdots} \> \gray{start of target specific back-end}
\end{tabbing}
%\vspace{-3ex}
%\begin{itemize}
\item Structured traces
\end{itemize}

}

\section{Shared}

\begin{frame}[fragile]
\frametitle{Shared definitions}

Identifiers: variables, cost labels, CFG labels, \dots

\begin{itemize}
\item Represented by arbitrarily large binary numbers and trees
\begin{itemize}
\item D3.3 `lazy failure' approach reusing existing structures
\item Invariant's types may depend on success of name generation
%\item Use this CompCert-like system instead
\end{itemize}
\item Tags for some type safety:
\begin{lstlisting}[language=matita]
inductive identifier (tag:String) : Type[0] ≝
  an_identifier : Word $\rightarrow$ identifier tag.
\end{lstlisting}
\end{itemize}

Memory, global environments from D3.1\\
Bit vector based arithmetic from D4.1
  \begin{itemize}
  \item added extra operations, increased efficiency
  \end{itemize}
%Common record type for small-step executable semantics
%  \begin{itemize}
%  \item used for animation
%  \item intended to be used when defining simulations
%  \end{itemize}



\textsf{Cminor} and \textsf{RTLabs} share operations on values.


\end{frame}

\section{Clight}
\frame{
\frametitle{Clight: syntax and semantics}

Modest evolution from D3.1:

\medskip
\begin{itemize}
\item use precise bit vectors instead of integer and range proof
\item adapting to changes in common definitions
\item added function to produce fresh name generator
\begin{itemize}
\item used for adding temporary variables
\item works by finding largest existing identifier
\item have shown necessary freshness proof
\end{itemize}
\end{itemize}
}

\begin{frame}[fragile]
\frametitle{Clight: cast simplification}

C insists on arithmetic promotion
\begin{itemize}
\item CIL-based \ocaml{} parser adds suitable casts
\item bad for our target (32-bit ops instead of 8-bit)
\end{itemize}

\medskip
Prototype recognises fixed patterns to simplify:
\[ (t)((t_1)e_1\ op\ (t_2)e_2) \]
\vspace{-4ex}
\begin{itemize}
\item Deep pattern matching is awkward in Matita
\item Misses (e.g.) \lstinline[language=C]'(char)((int)a+(int)b+(int)c)'
\end{itemize}

\medskip
\red{Instead}: recursive `coerce to desired type' approach.

Have done some preliminary proofs that this
works.
% (Doesn't get some things,
% e.g., \lstinline'==')
\end{frame}

\frame{
\frametitle{Clight: cost labelling}

Adds cost labels to Clight program.

\begin{itemize}
\item a simple recursive function, like prototype
\item uses common identifiers definition to produce fresh cost labels
\end{itemize}

The cost labelling is sound and precise, so we will be able to prove
some syntactic properties required later:
\begin{enumerate}
\item every function starts with a cost label
\item every branching instruction is followed by a cost label
\item the head of every loop (including \lstinline'goto's) is a cost label
\end{enumerate}

}

\section{Cminor}
\begin{frame}[fragile]
\frametitle{Cminor syntax and semantics}

Similar to CompCert's --- but developed from prototype.

\begin{itemize}
\item Some type enforcement for expressions:
\end{itemize}

\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
inductive expr : typ $\rightarrow$ Type[0] ≝
| Id : $\forall$t. ident $\rightarrow$ expr t
| Cst : $\forall$t. constant $\rightarrow$ expr t
| Op1 : $\forall$t,t'. unary_operation t t' $\rightarrow$ expr t $\rightarrow$ expr t'
| Op2 : $\forall$t1,t2,t'. binary_operation $\rightarrow$ expr t1 $\rightarrow$ expr t2 $\rightarrow$ expr t'
| Mem : $\forall$t,r. memory_chunk $\rightarrow$ expr (ASTptr r) $\rightarrow$ expr t
| Cond : $\forall$sz,sg,t. expr (ASTint sz sg) $\rightarrow$ expr t $\rightarrow$ expr t $\rightarrow$ expr t
| Ecost : $\forall$t. costlabel $\rightarrow$ expr t $\rightarrow$ expr t.
\end{lstlisting}
\begin{itemize}
%\item enforces some checking during production
\item indirectly forces checking that temporaries are fresh
\item[$\star$] reduces failure cases in translation to RTLabs
\end{itemize}

Semantics unexciting small-step function.
\end{frame}

\begin{frame}
\frametitle{Adding invariants}

Lots of sources of failure in front-end due to badly formed programs:
\begin{itemize}
\item missing variables, graph nodes, \dots
\item badly structured programs
\end{itemize}

\bigskip
Have been refining the intermediate languages to rule these out:
\begin{enumerate}
\item \gray{Indexing Cminor syntax by nesting depth}
\item adding type constraints
\item adding invariants asserting presence of variables, etc.
\end{enumerate}

\end{frame}

\begin{frame}[fragile]
\frametitle{Invariants for identifiers}


Invariants change between languages and compilation:

\begin{description}
\item[syntax] constraints between parts of function body and other information
about the function
\item[compilation] constraints between statements and expressions and data structures in the translation
\end{description}

When using or creating function definitions have proved that we can switch between
invariants:
\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
lemma populates_env : $\forall$l,e,u,l',e',u'.
  distinct_env ?? l $\rightarrow$                    (* distinct names in l *)
  populate_env e u l = $\langle$l',e',u'$\rangle$ $\rightarrow$ (* build register mapping *)
  $\forall$i,t. Exists ? ($\lambda$x.x = $\langle$i,t$\rangle$) l $\rightarrow$ (* Anything in the environment... *)
      Env_has e' i t.      (* maps to something of the correct type *)
\end{lstlisting}

\vfill
\end{frame}

\begin{frame}[fragile]
\frametitle{Invariants in Cminor}

Embedded invariant in the function record:
\begin{lstlisting}[language=matita,basicstyle=\scriptsize\tt,morekeywords=f_inv]
record internal_function : Type[0] ≝
{ f_return     : option typ
; f_params     : list (ident $\times$ typ)
; f_vars       : list (ident $\times$ typ)
; f_stacksize : nat
; f_body       : stmt
; f_inv        :
  stmt_P ($\lambda$s.
    stmt_vars   ($\lambda$i,t.Exists ? ($\lambda$x. x = $\langle$i,t$\rangle$) (f_params @ f_vars)) s $\wedge$
    stmt_labels ($\lambda$l.Exists ? ($\lambda$l'.l' = l) (labels_of f_body))     s)
  f_body
}.
\end{lstlisting}
\begin{enumerate}
\item All variables are in the parameters or locals lists\\
\quad --- with the correct type
\item All \lstinline'goto' labels mentioned are defined in the body
\end{enumerate}

\end{frame}


\section{Clight to Cminor}

\begin{frame}
\frametitle{Clight to Cminor}

Two main jobs:
\begin{enumerate}
\item make memory allocation of variables explicit
\item use simpler control structures
\end{enumerate}
Again, based on prototype rather than CompCert.

\bigskip
Added type checking:
\begin{itemize}
\item satisfies the restrictions for Cminor expressions
\item could separate out, have a `nice Clight' language
\end{itemize}
Similarly, code checks
\begin{itemize}
\item variable environments are well-formed
\item all \lstinline'goto' labels are translated
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Clight to Cminor proofs}

Beyond the invariants already shown, we will prove:

\medskip
\begin{enumerate}
\item a simulation relation
  \begin{itemize}
  \item between statement and continuation pairs
  \item using memory injection (similar to CompCert)
  \end{itemize}
\item syntactic cost labelling properties are preserved
  \begin{itemize}
  \item structural induction on function body
  \end{itemize}
\end{enumerate}
\end{frame}

\section{Initialisation}
\begin{frame}
\frametitle{Cminor: initialization}

Replace initialization data by code in the initial function.

\begin{itemize}
\item straightforward to define
\item instantiate a slightly different version of the semantics for it
\begin{itemize}
\item Can't accidentally forget the pass
\end{itemize}
\end{itemize}

\bigskip
Correctness should follow because the state after the initialisation will
be the same as the initial state of the original.
\end{frame}

\section{RTLabs}
\begin{frame}[fragile]
\frametitle{RTLabs: syntax and semantics}

Register Transfer Language with front-end operations.

Control flow graph implemented by generic identifiers map:

\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt]
definition label := identifier LabelTag.
definition graph : Type[0] $\rightarrow$ Type[0] := identifier_map LabelTag.

inductive statement : Type[0] ≝
| St_skip : label $\rightarrow$ statement
| St_const : register $\rightarrow$ constant $\rightarrow$ label $\rightarrow$ statement
| St_op1 : $\forall$t,t'. unary_operation t' t $\rightarrow$ register
   $\rightarrow$ register $\rightarrow$ label $\rightarrow$ statement
...
\end{lstlisting}
\vspace{-1.5ex}
\begin{itemize}
\item Shares basic operations (including semantics) with Cminor.
\item Tags prevent confusion of labels (graph vs.~goto vs.~cost).
\end{itemize}

Semantics straightforward interpretation of statements.
\end{frame}

\begin{frame}[fragile]
\frametitle{RTLabs: syntax and semantics}

\begin{lstlisting}[language=matita]
record internal_function : Type[0] ≝
{ f_labgen    : universe LabelTag
; f_reggen    : universe RegisterTag
...
; f_graph     : graph statement
; f_closed    : graph_closed f_graph
; f_typed     : graph_typed (f_locals @ f_params) f_graph
...
\end{lstlisting}

Enforce that
\begin{itemize}
\item every statement's successor labels are present in the CFG
\item every statement should be well-typed (for limited type system)
\end{itemize}

\end{frame}

\section{Cminor to RTLabs}
\begin{frame}
\frametitle{Cminor to RTLabs}

Break down statements and expressions into RTL graph.

\begin{itemize}
\item Incrementally build function backwards
\item all state is in function record, like prototype
\end{itemize}

%\bigskip
%May investigate whether a state monad makes invariant management easier.

\bigskip
Showing graph closure requires
\begin{itemize}
\item monotonicity of graph construction
\item eventual insertion of all \lstinline'goto' destinations
\end{itemize}

Carry these along in the partially built function record.

\end{frame}

% \begin{frame}[fragile]
% \frametitle{Cminor nesting depth}

% Want to prevent
% \begin{lstlisting}[language=C]
% void f() {
%   block { loop { exit 5; } }
% }
% \end{lstlisting}

% Index statements by block depth
% \begin{lstlisting}[language=matita]
% inductive stmt : $\forall$blockdepth:nat. Type[0] ≝
% | St_skip : $\forall$n. stmt n
% ...
% | St_block : $\forall$n. stmt (S n) $\rightarrow$ stmt n
% | St_exit : $\forall$n. Fin n $\rightarrow$ stmt n
% ...
% \end{lstlisting}

% \begin{itemize}
% \item In semantics index continuations too
% \item Use \lstinline[language=matita]'Fin n' to make \lstinline'k_exit'
% a total function
% \end{itemize}

% (May be able to remove entirely if we redo \lstinline[language=C]{switch}?)
% \end{frame}

\begin{frame}[fragile]
\frametitle{Establishing RTLabs invariants}

Use dependent pairs to show invariant along with results.

\begin{lstlisting}[language=matita,basicstyle=\footnotesize\tt,escapechar=\%]
let rec add_expr ... (e:expr ty)
   (Env:expr_vars ty e (present ?? env))   %\quad%  (* invariant *)
   (f:partial_fn le)
 on e: $\Sigma$f':partial_fn le. fn_graph_included le f f' ≝

match e return
   $\lambda$ty,e.expr_vars ty e (present ?? env) $\rightarrow$ ... with
[ ...
| Cst _ c $\Rightarrow$ $\lambda$_. %\guillemotleft%add_fresh_to_graph ? (St_const dst c) f ?, ?%\guillemotright%
...
\end{lstlisting}

Continually appeal to monotonicity (\lstinline'fn_graph_included').\\
Use unification hints to simplify stepping back.

\end{frame}

\frame{
\frametitle{Cminor to RTLabs: cost labels}

Two cost label properties are the same, the third will require more
work:
\begin{enumerate}
\item cost label at head of function
\item cost label after branching instructions
\item cost labels at the head of each loop / \lstinline'goto' destination
\end{enumerate}

No simple notion of the head of a loop or \lstinline'goto' any more.

\medskip
Instead: will prove in \alert{Cminor} that after following a finite
number of instructions we reach either
\begin{itemize}
\item a cost label, or
\item the end of the function
\end{itemize}

}

\section{Structured traces}
\frame{
\frametitle{RTLabs structured traces}

Front-end only uses flat traces consisting of single steps.

\bigskip
The back-end will need the function call structure and the labelling
properties in order to show that the generated costs are correct.

\begin{itemize}
\item Traces are structured in sections from cost label to cost label,
\item the entire execution of function calls nested as a single `step',
\item a coinductive definition presents non-terminating traces, using the
  inductive definition for all terminating function calls
\end{itemize}

\bigskip
RTLabs chosen because it is the first languages where statements:
\begin{itemize}
\item take one step each (modulo function calls)
\item have individual `addresses'
\end{itemize}
}

\frame{
\frametitle{RTLabs structured traces}
Have already established the existence of such traces
\begin{itemize}
\item termination decided classically
\item syntactic labelling properties used to build semantic structure
\item show stack preservation to ensure that function calls \texttt{return}
  to the correct location
\item tricky to establish guardedness of definitions
\end{itemize}

\bigskip
Next, prove that flattening these traces yields the original.
}

\frame{
\frametitle{Conclusion}

Syntax, semantics and translations of prototype now implemented in Matita.

\bigskip
Have defined and established
\begin{itemize}
\item invariants regarding variables, typing and program structure
\item a rich form of execution trace to pass to the back-end
\end{itemize}

\medskip
Work in progress:
\begin{itemize}
\item showing functional correctness of the front-end
\item proving that cost labelling is appropriate, and preserved
\end{itemize}

Finally, \alert{end-to-end} functional and cost correctness results.

}

\end{document}