248 lines
7.9 KiB
TeX
248 lines
7.9 KiB
TeX
\documentclass{beamer}
|
|
\usepackage{listings}
|
|
\lstset{
|
|
basicstyle=\ttfamily,
|
|
columns=fullflexible,
|
|
frame=single,
|
|
breaklines=true,
|
|
}
|
|
\usepackage{tikz}
|
|
|
|
\usetikzlibrary{positioning}
|
|
\usetheme{Darmstadt}
|
|
|
|
\begin{document}
|
|
|
|
\title{Presentation of our Lustre-to-C compiler}
|
|
\subtitle{github.com/Benjamin-Loison/Synchronous-reactive-systems}
|
|
\date{16 December 2022}
|
|
\author{Benjamin Loison, Arnaud Daby-Seesaram, Antoine Grimod}
|
|
|
|
\frame{\titlepage}
|
|
|
|
\section{Structure of the compiler}
|
|
\begin{frame}{Main ideas}
|
|
\begin{figure}
|
|
\begin{tikzpicture}
|
|
\node (sf) {Source file};
|
|
\node[right =2cm of sf] (ast) {Typed AST};
|
|
\node[right =2cm of ast] (C) {C program};
|
|
\draw
|
|
(sf) edge[->] node[above] {parser} (ast)
|
|
(ast) edge[->] node[above] {compiler} (C);
|
|
\end{tikzpicture}
|
|
\caption{Structure of the compiler}
|
|
\end{figure}
|
|
\end{frame}
|
|
|
|
\begin{frame}{Testing}
|
|
\begin{block}{Passes}
|
|
The passes can be split into:
|
|
\begin{itemize}
|
|
\item those checking the program validity
|
|
\item those modifying the AST of the program
|
|
\end{itemize}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
\section{Typed AST}
|
|
\subsection{First attempt using GADTs}
|
|
\begin{frame}
|
|
\begin{block}{Main idea}
|
|
Using GADTs to represent nodes and expressions allows to ensure the
|
|
well-typedness of a program.
|
|
\end{block}
|
|
\begin{figure}
|
|
\centering
|
|
\includegraphics[width=.75\textwidth]{imgs/gadt.png}
|
|
\end{figure}
|
|
\end{frame}
|
|
\begin{frame}
|
|
\begin{block}{Pros of using GADTs}
|
|
\begin{itemize}
|
|
\item Any term of the GADT represents a well-typed program
|
|
\item Extending the language to support more types consists of adding
|
|
constructors to variables and constants
|
|
\item The types are easy to read and understand
|
|
\end{itemize}
|
|
\end {block}
|
|
|
|
\begin{block}{Cons of using GADTs}
|
|
\begin{itemize}
|
|
\item
|
|
They cannot be dynamically generated (hence it is impossible to
|
|
implement a parser that gives back a GADT)
|
|
\item
|
|
One should think about the isomorphism between
|
|
\texttt{a $\ast$ (b $\ast$ c)} and \texttt{(a $\ast$ b) $\ast$ c}.
|
|
\end{itemize}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
\subsection{Second attempt: using explicit types in the variables, expressions,
|
|
\dots{} constructors}
|
|
\begin{frame}
|
|
\begin{block}{Idea}
|
|
Explicitly collect typing information while parsing.
|
|
\end{block}
|
|
\begin{figure}
|
|
\centering
|
|
\includegraphics[width=.6\textwidth]{imgs/explicit_types.png}
|
|
\end{figure}
|
|
\end{frame}
|
|
|
|
\begin{frame}
|
|
\begin{block}{Pros of using explicit types}
|
|
\begin{itemize}
|
|
\item Programs can be built dynamically, hence a parser can be
|
|
written
|
|
\item While parsing, the parser has all the required information on
|
|
the sub-variables/nodes/expressions to check the well-typedness
|
|
\end{itemize}
|
|
\end{block}
|
|
\begin{block}{Cons of these definitions}
|
|
\begin{itemize}
|
|
\item The typing information on terms is very redundant.
|
|
\item The rejection of ill-typed programs depends on the correctness
|
|
of the parser
|
|
\end{itemize}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
\section{Passes}
|
|
\begin{frame}{}
|
|
\begin{block}{Classification}
|
|
\begin{itemize}
|
|
\item node-passes: for all nodes, do \texttt{P: t\_node -> t\_node
|
|
option}
|
|
\pause
|
|
\item equation-passes: for all equations of all nodes, do
|
|
\texttt{P: t\_equation -> t\_equation option}
|
|
(the definition uses the node-passes constructor)
|
|
\pause
|
|
\item expression-passes: for all expression of all equations, do
|
|
\texttt{P: t\_expression -> t\_expression option}
|
|
(the definition uses the equation-passes constructor)
|
|
\end{itemize}
|
|
\end{block}
|
|
\end{frame}
|
|
\begin{frame}{Implemented Passes}
|
|
\begin{block}{Sanity checks}
|
|
\begin{itemize}
|
|
\item Check the well-typedness of a program
|
|
\pause
|
|
\item Check that there are no assignment conflicts in a programs
|
|
(node-pass)
|
|
\pause
|
|
\end{itemize}
|
|
\end{block}
|
|
\begin{block}{AST modification}
|
|
\begin{itemize}
|
|
\item Rewrite automata into \texttt{if-then-else} constructs
|
|
(node-pass)
|
|
\pause
|
|
\item Linearization of the equations:
|
|
\begin{itemize}
|
|
\item for all, \texttt{pre e} add a, intermediate variable
|
|
\item \texttt{v1, v2, v3 = f(i), e3;} is rewritten into
|
|
\texttt{v1, v2 = f(i); v3 = e3;}
|
|
\end{itemize}
|
|
(node-pass)
|
|
\pause
|
|
\item (no longer required) Push the \texttt{pre} to variables
|
|
(expression-pass)
|
|
\end{itemize}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]{Translation of automaton}
|
|
\only<1>{\lstinputlisting[language=ml, firstline=1, lastline=7]{code/example_automaton.lus}}
|
|
\only<2>{\lstinputlisting[language=ml, firstline=9, lastline=14]{code/example_automaton.lus}}
|
|
\end{frame}
|
|
\begin{frame}{Restriction on automaton}
|
|
The patterns that appears on the left of equations must be the
|
|
same in all branches
|
|
|
|
\only<2>{\lstinputlisting[language=ml, firstline=16, lastline=22]{code/example_automaton.lus}}
|
|
\end{frame}
|
|
|
|
\begin{frame}{Clock unification}
|
|
|
|
Derived from the rules provided in \emph{Clock-directed Modular Code Generation for Synchronous
|
|
Data-flow Languages}
|
|
\end{frame}
|
|
|
|
\section{Translation to C}
|
|
\begin{frame}
|
|
|
|
\texttt{ast\_to\_c.ml} architecture similar to Arnaud's AST pretty-printer.
|
|
|
|
\pause
|
|
|
|
For instance, go from \texttt{counting.lus} to \texttt{counting.c}.
|
|
|
|
\pause
|
|
|
|
Use of three tricks, as our compiler only manages \texttt{bool}s, \texttt{int}s and \texttt{float}s:
|
|
\begin{enumerate}
|
|
\item \texttt{0} can be interpreted as a \texttt{bool}, an \texttt{int} and a \texttt{float}
|
|
\pause
|
|
\item A \texttt{float} correctly encode \texttt{bool}s (\texttt{true} and \texttt{false}) and \texttt{int}s (between $[-2^{24} + 1; 2^{24} + 1]$)
|
|
\pause
|
|
\item To run an assignment of \texttt{value} to \texttt{variable} within the condition of a \texttt{if} and also make the cases of the \texttt{if} depends on a condition \texttt{condition}, we can do \texttt{if(((variable = value) \&\& false) || condition)}\\
|
|
\pause
|
|
We can also use this trick to execute an assignment and \textit{return} a value \texttt{value\_to\_return} without using any \texttt{;}, by using \texttt{((variable = value) || true) ? value\_to\_return : 0} (thanks to the first trick)
|
|
\end{enumerate}
|
|
\end{frame}
|
|
|
|
\begin{frame}
|
|
\begin{itemize}
|
|
\item
|
|
\begin{itemize}
|
|
\item \texttt{pp\_varlist (Base | Arg | Dec)}
|
|
\item \texttt{pp\_retvarlist}
|
|
\item \texttt{pp\_prevarlist}
|
|
\item \texttt{pp\_asnprevarlist}
|
|
\end{itemize}
|
|
\pause
|
|
\item \texttt{when} implementation error: division by zero for instance, so used the first trick (\texttt{when\_merge.node})
|
|
\pause
|
|
\item \texttt{->}: use global variable \texttt{init\_\{NODE\_NAME\}}\\
|
|
\texttt{1 -> 2 -> 3} returns \texttt{0} on first run and only \texttt{3} on the following ones, correct? (\texttt{arrow.node})
|
|
\pause
|
|
\item \texttt{pre}
|
|
\pause
|
|
\item \texttt{reset}% (\texttt{reset})
|
|
\pause
|
|
\item Functions returning tuples thanks to Arnaud's linearization only have to deal with \texttt{(a0, a1, ..., an) = return\_tuple\_a0\_a1\_dots\_an(0)} (\texttt{function\_returning\_tuple.node})
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\section{Tests}
|
|
\begin{frame}{Tests}
|
|
\begin{block}{testing methods}
|
|
We thought of three testing methods:
|
|
\begin{itemize}
|
|
\item manual testing of our functionalities
|
|
\item run the sanity-checks-passes after any AST-altering pass
|
|
\item simulation of the nodes (aborted)
|
|
\end{itemize}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
\section{Possible improvements}
|
|
\begin{frame}{Improvements}
|
|
\begin{itemize}
|
|
\item Increase the expressivity of the accepted programs
|
|
\item Improve the complexity of the different passes
|
|
\begin{itemize}
|
|
\item Group neighbour passes of the same type (node-, expression or
|
|
equation-pass).
|
|
\end{itemize}
|
|
\item \dots{}
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\end{document}
|
|
|