|
|
|
|
@ -28,7 +28,7 @@
|
|
|
|
|
|
|
|
|
|
The additional arithmetic expressions' semantics are implemented in a similar manner as with the other.
|
|
|
|
|
|
|
|
|
|
The sematic of \texttt{for} is as follows:
|
|
|
|
|
The semantic of \texttt{for} is as follows:
|
|
|
|
|
|
|
|
|
|
\begin{center}
|
|
|
|
|
\inference[\texttt{for}]
|
|
|
|
|
@ -41,7 +41,7 @@
|
|
|
|
|
|
|
|
|
|
\begin{subsection}{MiniFun Semantics}
|
|
|
|
|
The semantic of the MiniFun language is implemented in the \href{../lib/miniFun/Semantics.mli}{Semantics.mli} and \href{../lib/miniFun/Semantics.ml}{Semantics.ml} file.
|
|
|
|
|
A \texttt{reduce} function is provided that transforms the AST into the avluated value or an error.
|
|
|
|
|
A \texttt{reduce} function is provided that transforms the AST into the evaluated value or an error.
|
|
|
|
|
The AST type is defined in \href{../lib/miniFun/Types.mli}{Types.mli} and in \href{../lib/miniFun/Types.ml}{Types.ml}.
|
|
|
|
|
|
|
|
|
|
A program \texttt{t} is defined as follows:
|
|
|
|
|
@ -67,7 +67,7 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\begin{section}{Types for MiniFun}
|
|
|
|
|
A type \(\tau\) is defined as either {\it int}, {\it bool}, a touple or a function.
|
|
|
|
|
A type \(\tau\) is defined as either {\it int}, {\it bool}, a tuple or a function.
|
|
|
|
|
|
|
|
|
|
\begin{equation*}
|
|
|
|
|
\tau \defeq {\it int\/}\ \vert\ {\it bool\/}\ \vert\ (\tau,\tau)\ \vert\ \tau \to \tau
|
|
|
|
|
@ -104,7 +104,7 @@
|
|
|
|
|
\begin{center}
|
|
|
|
|
\inference[\texttt{FunRec}]
|
|
|
|
|
{\Gamma[f \mapsto \tau \to \tau'; x \mapsto \tau] \vdash t_1 \triangleright \tau' & \Gamma[f \mapsto \tau \to \tau'] \vdash t_2 \triangleright \tau''} % chktex 1
|
|
|
|
|
{\Gamma \vdash \texttt{let rec} f x \texttt{:} \tau \to \tau' \texttt{ = } t_1 \texttt{ in } t_2 \triangleright \tau''} % chktex 1
|
|
|
|
|
{\Gamma \vdash \texttt{let rec } f\ x \texttt{:} \tau \to \tau' \texttt{ = } t_1 \texttt{ in } t_2 \triangleright \tau''} % chktex 1
|
|
|
|
|
\end{center}
|
|
|
|
|
|
|
|
|
|
In the files \href{../lib/miniFun/TypeChecker.mli}{TypeChecker.mli} and \href{../lib/miniFun/TypeChecker.ml}{TypeChecker.ml} there is the implementation of the deduction rules, but returns either the valid type of the expression or an error instead of simply the required option type of the valid type.
|
|
|
|
|
@ -112,6 +112,7 @@
|
|
|
|
|
|
|
|
|
|
\begin{section}{Parsing}
|
|
|
|
|
\begin{subsection}{MiniImp}
|
|
|
|
|
As seen in class, lexing and parsing is done with ocamellex and menhir in the files \href{../lib/miniImp/Lexer.mli}{Lexer.mli} and \href{../lib/miniImp/Parser.ml}{Parser.ml}.
|
|
|
|
|
Operators listed in order of precedence from highest to lowest:
|
|
|
|
|
|
|
|
|
|
\begin{center}
|
|
|
|
|
@ -127,14 +128,15 @@
|
|
|
|
|
\end{tblr}
|
|
|
|
|
\end{center}
|
|
|
|
|
|
|
|
|
|
The expressions \(c_1 \texttt{;} c_2\) and \(c_1 \texttt{;}\) are both recognized and give respectively \(\texttt{SEQUENCE(} c_1 \texttt{,} c_2 \texttt{)}\) % chktex 9
|
|
|
|
|
and \(c_1\), such that semicolons can be placed always at the end of a command.
|
|
|
|
|
The expressions \(c_1 \texttt{;} c_2\) and \(c_3 \texttt{;}\) are both recognized and give respectively \(\texttt{SEQUENCE(} c_1 \texttt{,} c_2 \texttt{)}\) % chktex 9
|
|
|
|
|
and \(c_3\), such that semicolons can be placed always at the end of a command.
|
|
|
|
|
|
|
|
|
|
Integers with a preceding minus sign can be interpreted as the opposite integer, with obviously lower precedence than the binary operator minus.
|
|
|
|
|
\end{subsection}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\begin{subsection}{MiniFun}
|
|
|
|
|
As seen in class, lexing and parsing is done with ocamellex and menhir in the files \href{../lib/miniFun/Lexer.mli}{Lexer.mli} and \href{../lib/miniFun/Parser.ml}{Parser.ml}.
|
|
|
|
|
A decision was made to interpret \texttt{\textbackslash}, \texttt{lambda} and \texttt{fun} all as the start of the definition of a function just for ease of typing. They are associated to the same token \texttt{LAMBDA}.
|
|
|
|
|
|
|
|
|
|
Operators listed in order of precedence from highest to lowest:
|
|
|
|
|
@ -157,7 +159,7 @@
|
|
|
|
|
\end{tblr}
|
|
|
|
|
\end{center}
|
|
|
|
|
|
|
|
|
|
Tuples require parentesis in their definition, but the tuple type does not since there is no ambiguity. The symbol \texttt{->} that defines the function type is right associative and has lowest precedence.
|
|
|
|
|
Tuples require parenthesis in their definition, but the tuple type does not since there is no ambiguity. The symbol \texttt{->} that defines the function type is right associative and has lowest precedence.
|
|
|
|
|
\end{subsection}
|
|
|
|
|
|
|
|
|
|
\begin{subsection}{Interpreters}
|
|
|
|
|
@ -175,11 +177,11 @@
|
|
|
|
|
|
|
|
|
|
The control flow structure is composed of a flag to know if it is empty or contains nodes and the set of all contained nodes.
|
|
|
|
|
Since each node can only have at maximum 2 nodes as next nodes, the data structure contains a map from each node to a tuple of the two nodes or to a node.
|
|
|
|
|
The structure also contains the back edges of each node implemented as a map from each node to a list of nodes, the input value, the variables that are the input and ouput, the initial node and the terminal node.
|
|
|
|
|
The structure also contains the back edges of each node implemented as a map from each node to a list of nodes, the input value, the variables that are the input and output, the initial node and the terminal node.
|
|
|
|
|
Finally there is a map from each node to a list of generic elements that in our case are simple statements.
|
|
|
|
|
|
|
|
|
|
\begin{subsection}{MiniImp Simple Statement}
|
|
|
|
|
MiniImp Simple Statements \(t\) is defined as follows:
|
|
|
|
|
MiniImp Simple Statements \(t\) is defined in the files \href{../lib/miniImp/CfgImp.ml}{CfgImp.ml} and \href{../lib/miniImp/CfgImp.mli}{CfgImp.mli} as follows:
|
|
|
|
|
|
|
|
|
|
\begin{grammar}
|
|
|
|
|
<t> \(\defeq\) skip | <x> `:=' <a> | <b> `{?}'
|
|
|
|
|
@ -191,9 +193,9 @@
|
|
|
|
|
\alt{} <a> `mod' <a> | <a> `^' <a> | `rand' <a>
|
|
|
|
|
\end{grammar}
|
|
|
|
|
|
|
|
|
|
The implemented cfg is neither minimal nor maximal, but can be either or both for some programs. In particular each node as associated a list of statements and sequence of statements in the AST is put, if possible, in the same node.
|
|
|
|
|
The implemented CFG is neither minimal nor maximal, but can be either or both for some programs. In particular each node as associated a list of statements and sequence of statements in the AST is put, if possible, in the same node.
|
|
|
|
|
|
|
|
|
|
\texttt{?} is only allowed as the last element of the list of statemets associated with a node and a node has associated a \texttt{?} if and only if they have two next nodes.
|
|
|
|
|
\texttt{?} is only allowed as the last element of the list of statements associated with a node and a node has associated a \texttt{?} if and only if they have two next nodes.
|
|
|
|
|
|
|
|
|
|
The for loop is translated as:
|
|
|
|
|
|
|
|
|
|
@ -339,7 +341,7 @@ while exp > 0 do (
|
|
|
|
|
\end{subsection}
|
|
|
|
|
|
|
|
|
|
\begin{subsection}{MiniRISC}
|
|
|
|
|
The MiniRISC CFG is finally tranlated into MiniRISC intermediate code by the function \texttt{convert} in the files \href{../lib/miniImp/RISC.ml}{RISC.ml} and \href{../lib/miniImp/RISC.mli}{RISC.mli}.
|
|
|
|
|
The MiniRISC CFG is finally translated into MiniRISC intermediate code by the function \texttt{convert} in the files \href{../lib/miniImp/RISC.ml}{RISC.ml} and \href{../lib/miniImp/RISC.mli}{RISC.mli}.
|
|
|
|
|
The grammar of MiniRISC is analogous to the one for \hyperref[grammar:MiniRISC]{MiniRISC Simple Statements}:
|
|
|
|
|
|
|
|
|
|
\begin{grammar}
|
|
|
|
|
@ -373,7 +375,7 @@ while exp > 0 do (
|
|
|
|
|
\end{section}
|
|
|
|
|
|
|
|
|
|
\begin{section}{Dataflow Analysis}
|
|
|
|
|
A refined CFG structure used for analysis is defined in \href{../lib/analysis/Dataflow.ml}{Dataflow.ml} and \href{../lib/analysis/Dataflow.mli}{Dataflow.mli}. The CFG is supplemented with a map from each node to the support structure that stores the list of defined variables or live variables. Since the CFG is not minimal, there is also a list for each simple statement. A fixed point function then applies the input fuction until the map does not change. Simple structural equality is not appropriate since order in the lists should not matter; an internal function for equality is used.
|
|
|
|
|
A refined CFG structure used for analysis is defined in \href{../lib/analysis/Dataflow.ml}{Dataflow.ml} and \href{../lib/analysis/Dataflow.mli}{Dataflow.mli}. The CFG is supplemented with a map from each node to the support structure that stores the list of defined variables or live variables. Since the CFG is not minimal, there is also a list for each simple statement. A fixed point function then applies the input function until the map does not change. Simple structural equality is not appropriate since order in the lists should not matter; an internal function for equality is used.
|
|
|
|
|
|
|
|
|
|
\begin{subsection}{Defined Variables}
|
|
|
|
|
In the files \href{../lib/miniImp/definedVariables.ml}{definedVariables.ml} and \href{../lib/miniImp/definedVariables.mli}{definedVariables.mli} three functions are defined: \texttt{compute_defined_variables}, \texttt{compute_cfg} and \texttt{check_undefined_variables}.
|
|
|
|
|
@ -382,7 +384,7 @@ while exp > 0 do (
|
|
|
|
|
\texttt{compute_cfg} returns the CFG from the analysis data structure; in the case of defined variables analysis the CFG returned is the same as the one in input of \texttt{compute_defined_variables}.
|
|
|
|
|
\texttt{check_undefined_variables} returns all variables that might be undefined at time of use.
|
|
|
|
|
|
|
|
|
|
Since the greatest fixed point is computed, first all variables are retrived from all code, then assigned to each input and ouput list of variables for each line of code.
|
|
|
|
|
Since the greatest fixed point is computed, first all variables are retrieved from all code, then assigned to each input and output list of variables for each line of code.
|
|
|
|
|
|
|
|
|
|
Since it is an approximation some behaviour might not be intuitive. For example:
|
|
|
|
|
|
|
|
|
|
@ -406,7 +408,7 @@ output := y;
|
|
|
|
|
\end{section}
|
|
|
|
|
|
|
|
|
|
\begin{section}{Target Code Generation}
|
|
|
|
|
In the files \href{../lib/miniImp/reduceRegisters.ml}{reduceRegisters.ml} and \href{../lib/miniImp/reduceRegisters.mli}{reduceRegisters.mli} the function \texttt{reduceregisters} reduces the number of used registers by counting the syntactic occurrence of each variable and partitioning the set keeping the most used as registers. All registers are either renamed or put into memory. It is allowed for the input or output registers to be put in memory, in the latter case some code is added at the end of the program to retrive the value and put into a register (register \texttt{2}).
|
|
|
|
|
In the files \href{../lib/miniImp/reduceRegisters.ml}{reduceRegisters.ml} and \href{../lib/miniImp/reduceRegisters.mli}{reduceRegisters.mli} the function \texttt{reduceregisters} reduces the number of used registers by counting the syntactic occurrence of each variable and partitioning the set keeping the most used as registers. All registers are either renamed or put into memory. It is allowed for the input or output registers to be put in memory, in the latter case some code is added at the end of the program to retrieve the value and put into a register (in particular register \texttt{2}).
|
|
|
|
|
|
|
|
|
|
\begin{subsection}{MiniImp to MiniRISC compiler}
|
|
|
|
|
The file \href{../bin/miniImpInterpreterReg.ml}{miniImpInterpreterReg.ml} compiles from MiniImp to MiniRISC or execute the MiniRISC code. It uses the package \href{https://opam.ocaml.org/packages/clap/}{Clap} to parse command line arguments and generate help pages.
|
|
|
|
|
@ -418,7 +420,11 @@ output := y;
|
|
|
|
|
\begin{section}{Running the code}
|
|
|
|
|
The project uses the following packages: \href{https://dune.build/}{Dune}, \href{https://gallium.inria.fr/~fpottier/menhir/}{Menhir} and \href{https://github.com/rbardou/clap}{Clap}. They can be installed via \href{https://opam.ocaml.org/}{Opam} with the command \texttt{opam install dune menhir clap}.
|
|
|
|
|
To compile the project simply run \texttt{dune build}. To run the test run \texttt{dune runtest}.
|
|
|
|
|
In order to execute one of the interpreters run \texttt{dune exec <interpreter> {-}{-} <flags and options>}. To see a list of all options run \texttt{dune exec <interpreter> {-}{-} -h}. A binary version of the executables can also be found in \href{./_build/default/bin/}{./_build/default/bin/}.
|
|
|
|
|
In order to execute one of the interpreters run \texttt{dune exec <interpreter> {-}{-} <flags and options>}.
|
|
|
|
|
|
|
|
|
|
For example: \texttt{dune exec miniImpInterpreterReg {-}{-} -i bin/sum.miniimp -r 4 -v 100 -e}.
|
|
|
|
|
|
|
|
|
|
To see a list of all options run \texttt{dune exec <interpreter> {-}{-} -h}. A binary version of the executables can also be found in the build directory: \href{./_build/default/bin/}{./\_build/default/bin/}.
|
|
|
|
|
\end{section}
|
|
|
|
|
%%% Local Variables:
|
|
|
|
|
%%% TeX-command-extra-options: "-shell-escape"
|
|
|
|
|
|
elvis