358 lines
12 KiB
TeX
358 lines
12 KiB
TeX
% Created 2020-02-24 Mon 14:37
|
|
% Intended LaTeX compiler: pdflatex
|
|
\documentclass[11pt]{article}
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage{graphicx}
|
|
\usepackage{grffile}
|
|
\usepackage{longtable}
|
|
\usepackage{wrapfig}
|
|
\usepackage{rotating}
|
|
\usepackage[normalem]{ulem}
|
|
\usepackage{amsmath}
|
|
\usepackage{textcomp}
|
|
\usepackage{amssymb}
|
|
\usepackage{capt-of}
|
|
\usepackage{hyperref}
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage{algorithm}
|
|
\usepackage{algpseudocode}
|
|
\usepackage{amsmath,amssymb,amsthm}
|
|
\newtheorem{definition}{Definition}
|
|
\usepackage{graphicx}
|
|
\usepackage{listings}
|
|
\usepackage{color}
|
|
\author{Francesco Mecca}
|
|
\date{}
|
|
\title{Translation Verification of the OCaml pattern matching compiler}
|
|
\hypersetup{
|
|
pdfauthor={Francesco Mecca},
|
|
pdftitle={Translation Verification of the OCaml pattern matching compiler},
|
|
pdfkeywords={},
|
|
pdfsubject={},
|
|
pdfcreator={Emacs 26.3 (Org mode 9.1.9)},
|
|
pdflang={English}}
|
|
\begin{document}
|
|
|
|
\maketitle
|
|
\section{{\bfseries\sffamily TODO} Scaletta [1/2]}
|
|
\label{sec:org8ebbc9e}
|
|
\begin{itemize}
|
|
\item[{$\boxtimes$}] Abstract
|
|
\item[{$\boxminus$}] Background [20\%]
|
|
\begin{itemize}
|
|
\item[{$\boxtimes$}] Ocaml
|
|
\item[{$\square$}] Lambda code [0\%]
|
|
\begin{itemize}
|
|
\item[{$\square$}] Untyped lambda form
|
|
\item[{$\square$}] OCaml specific instructions
|
|
\end{itemize}
|
|
\item[{$\boxminus$}] Pattern matching [50\%]
|
|
\begin{itemize}
|
|
\item[{$\boxtimes$}] Introduzione
|
|
\item[{$\square$}] Compilation to lambda form
|
|
\end{itemize}
|
|
\item[{$\square$}] Translation Verification
|
|
\item[{$\square$}] Symbolic execution
|
|
\end{itemize}
|
|
\item[{$\square$}] Translation verification of the Pattern Matching Compiler
|
|
\begin{itemize}
|
|
\item[{$\square$}] Source translation
|
|
\begin{itemize}
|
|
\item[{$\square$}] Formal Grammar
|
|
\item[{$\square$}] Compilation of source patterns
|
|
\end{itemize}
|
|
\item[{$\square$}] Target translation
|
|
\begin{itemize}
|
|
\item[{$\square$}] Formal Grammar
|
|
\item[{$\square$}] Symbolic execution of the lambda target
|
|
\end{itemize}
|
|
\item[{$\square$}] Equivalence between source and target
|
|
\end{itemize}
|
|
\begin{itemize}
|
|
\item[{$\square$}] Practical results
|
|
\end{itemize}
|
|
\end{itemize}
|
|
|
|
|
|
\begin{abstract}
|
|
|
|
This dissertation presents an algorithm for the translation validation of the OCaml
|
|
pattern matching compiler. Given the source representation of the target program and the
|
|
target program compiled in untyped lambda form, the algoritmhm is capable of modelling
|
|
the source program in terms of symbolic constraints on it's branches and apply symbolic
|
|
execution on the untyped lambda representation in order to validate wheter the compilation
|
|
produced a valid result.
|
|
In this context a valid result means that for every input in the domain of the source
|
|
program the untyped lambda translation produces the same output as the source program.
|
|
The input of the program is modelled in terms of symbolic constraints closely related to
|
|
the runtime representation of OCaml objects and the output consists of OCaml code
|
|
blackboxes that are not evaluated in the context of the verification.
|
|
|
|
\end{abstract}
|
|
|
|
\section{Background}
|
|
\label{sec:org73f49d4}
|
|
|
|
\subsection{OCaml}
|
|
\label{sec:orga0f2160}
|
|
Objective Caml (OCaml) is a dialect of the ML (Meta-Language) family of programming
|
|
languages.
|
|
OCaml shares many features with other dialects of ML, such as SML and Caml Light,
|
|
The main features of ML languages are the use of the Hindley-Milner type system that
|
|
provides many advantages with respect to static type systems of traditional imperative and object
|
|
oriented language such as C, C++ and Java, such as:
|
|
\begin{itemize}
|
|
\item Parametric polymorphism: in certain scenarios a function can accept more than one
|
|
type for the input parameters. For example a function that computes the lenght of a
|
|
list doesn't need to inspect the type of the elements of the list and for this reason
|
|
a List.length function can accept list of integers, list of strings and in general
|
|
list of any type. Such languages offer polymorphic functions through subtyping at
|
|
runtime only, while other languages such as C++ offer polymorphism through compile
|
|
time templates and function overloading.
|
|
With the Hindley-Milner type system each well typed function can have more than one
|
|
type but always has a unique best type, called the \emph{principal type}.
|
|
For example the principal type of the List.length function is "For any \emph{a}, function from
|
|
list of \emph{a} to \emph{int}" and \emph{a} is called the \emph{type parameter}.
|
|
\item Strong typing: Languages such as C and C++ allow the programmer to operate on data
|
|
without considering its type, mainly through pointers. Other languages such as C\#
|
|
and Go allow type erasure so at runtime the type of the data can't be queried.
|
|
In the case of programming languages using an Hindley-Milner type system the
|
|
programmer is not allowed to operate on data by ignoring or promoting its type.
|
|
\item Type Inference: the principal type of a well formed term can be inferred without any
|
|
annotation or declaration.
|
|
\item Algebraic data types: types that are modelled by the use of two
|
|
algebraic operations, sum and product.
|
|
A sum type is a type that can hold of many different types of
|
|
objects, but only one at a time. For example the sum type defined
|
|
as \emph{A + B} can hold at any moment a value of type A or a value of
|
|
type B. Sum types are also called tagged union or variants.
|
|
A product type is a type constructed as a direct product
|
|
of multiple types and contains at any moment one instance for
|
|
every type of its operands. Product types are also called tuples
|
|
or records. Algebraic data types can be recursive
|
|
in their definition and can be combined.
|
|
\end{itemize}
|
|
Moreover ML languages are functional, meaning that functions are
|
|
treated as first class citizens and variables are immutable,
|
|
although mutable statements and imperative constructs are permitted.
|
|
In addition to that OCaml features an object system, that provides
|
|
inheritance, subtyping and dynamic binding, and modules, that
|
|
provide a way to encapsulate definitions. Modules are checked
|
|
statically and can be reificated through functors.
|
|
|
|
\begin{enumerate}
|
|
\item {\bfseries\sffamily TODO} Pattern matching [37\%]
|
|
\label{sec:org8bcefd9}
|
|
\begin{itemize}
|
|
\item[{$\square$}] capisci come mettere gli esempi uno accanto all'altro
|
|
\end{itemize}
|
|
|
|
Pattern matching is a widely adopted mechanism to interact with ADT.
|
|
C family languages provide branching on predicates through the use of
|
|
if statements and switch statements.
|
|
Pattern matching is a mechanism for destructuring and analyzing data
|
|
structures for the presence of values simbolically represented as
|
|
tokens. One common example of pattern matching is the use of regular
|
|
expressions on strings. OCaml provides pattern matching on ADT,
|
|
primitive data types.
|
|
|
|
\begin{itemize}
|
|
\item[{$\boxtimes$}] Esempio enum, C e Ocaml
|
|
\end{itemize}
|
|
\begin{verbatim}
|
|
type color = | Red | Blue | Green
|
|
|
|
begin match color with
|
|
| Red -> print "red"
|
|
| Blue -> print "red"
|
|
| Green -> print "red"
|
|
|
|
\end{verbatim}
|
|
|
|
OCaml provides tokens to express data destructoring
|
|
|
|
|
|
\begin{itemize}
|
|
\item[{$\boxtimes$}] Esempio destructor list
|
|
\end{itemize}
|
|
\begin{verbatim}
|
|
|
|
begin match list with
|
|
| [ ] -> print "empty list"
|
|
| element1 :: [ ] -> print "one element"
|
|
| element1 :: element2 :: [ ] -> print "two elements"
|
|
| head :: tail-> print "head followed by many elements"
|
|
\end{verbatim}
|
|
|
|
\begin{itemize}
|
|
\item[{$\boxtimes$}] Esempio destructor tuples
|
|
\end{itemize}
|
|
\begin{verbatim}
|
|
|
|
begin match tuple with
|
|
| (Some _, Some _) -> print "Pair of optional types"
|
|
| (Some _, None) -> print "Pair of optional types, last null"
|
|
| (None, Some _) -> print "Pair of optional types, first null"
|
|
| (None, None) -> print "Pair of optional types, both null"
|
|
\end{verbatim}
|
|
|
|
Pattern clauses can make the use of \emph{guards} to test predicates and
|
|
variables can be binded in scope.
|
|
|
|
\begin{itemize}
|
|
\item[{$\square$}] Esempio binding e guards
|
|
\end{itemize}
|
|
\begin{verbatim}
|
|
|
|
begin match token_list with
|
|
| "switch"::var::"{"::rest ->
|
|
| "case"::":"::var::rest when is_int var ->
|
|
| "case"::":"::var::rest when is_string var ->
|
|
| "}"::[ ] -> stop ()
|
|
| "}"::rest -> error "syntax error: " rest
|
|
|
|
\end{verbatim}
|
|
|
|
\begin{itemize}
|
|
\item[{$\square$}] Un altro esempio con destructors e tutto i lresto
|
|
\end{itemize}
|
|
|
|
In general pattern matching on primitive and algebraic data types takes the
|
|
following form.
|
|
|
|
\begin{itemize}
|
|
\item[{$\square$}] Esempio informale
|
|
\end{itemize}
|
|
|
|
It can be described more formally through a BNF grammar.
|
|
|
|
\begin{itemize}
|
|
\item[{$\square$}] BNF
|
|
|
|
\item[{$\square$}] Come funziona il pattern matching?
|
|
\end{itemize}
|
|
|
|
\item {\bfseries\sffamily TODO} 1.2.1 Pattern matching compilation to lambda code
|
|
\label{sec:orgd51f0ff}
|
|
|
|
\begin{itemize}
|
|
\item[{$\square$}] Da tabella a matrice
|
|
\end{itemize}
|
|
|
|
Formally, pattern are defined as follows:
|
|
\begin{center}
|
|
\begin{tabular}{ll}
|
|
pattern & Patterns\\
|
|
\hline
|
|
\_ & wildcard\\
|
|
x & variable\\
|
|
c(p₁,p₂,\ldots{},pₙ) & constructor pattern\\
|
|
(p₁\(\vert{}\) p₂) & or-pattern\\
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
Values are defined as follows:
|
|
\begin{center}
|
|
\begin{tabular}{ll}
|
|
values & Values\\
|
|
\hline
|
|
c(v₁, v₂, \ldots{}, vₙ) & constructor value\\
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
The entire pattern matching code can be represented as a clause matrix
|
|
that associates rows of patterns (p\(_{\text{i,1}}\), p\(_{\text{i,2}}\), \ldots{}, p\(_{\text{i,n}}\)) to
|
|
lambda code action lⁱ
|
|
\begin{equation*}
|
|
(P → L) =
|
|
\begin{pmatrix}
|
|
p_{1,1} & p_{1,2} & \cdots & p_{1,n} & → l₁ \\
|
|
p_{2,1} & p_{2,2} & \cdots & p_{2,n} & → l₂ \\
|
|
\vdots & \vdots & \ddots & \vdots & → \vdots \\
|
|
p_{m,1} & p_{m,2} & \cdots & p_{m,n} & → lₘ
|
|
\end{pmatrix}
|
|
\end{equation*}
|
|
|
|
Most native data types in OCaml, such as integers, tuples, lists,
|
|
records, can be seen as instances of the following definition
|
|
|
|
\begin{verbatim}
|
|
type t = Nil | One of int | Cons of int * t
|
|
\end{verbatim}
|
|
that is a type \emph{t} with three constructors that define its complete
|
|
signature.
|
|
Every constructor has an arity. Nil, a constructor of arity 0, is
|
|
called a constant constructor.
|
|
|
|
The pattern \emph{p} matches a value \emph{v}, written as p ≼ v, when one of the
|
|
following rules apply
|
|
|
|
\begin{center}
|
|
\begin{tabular}{llll}
|
|
& & & \\
|
|
\hline
|
|
\_ & ≼ & v & ∀v\\
|
|
x & ≼ & v & ∀v\\
|
|
(p₁ \(\vert{}\)$\backslash$ p₂) & ≼ & v & iff p₁ ≼ v or p₂ ≼ v\\
|
|
c(p₁, p₂, \ldots{}, pₐ) & ≼ & c(v₁, v₂, \ldots{}, vₐ) & iff (p₁, p₂, \ldots{}, pₐ) ≼ (v₁, v₂, \ldots{}, vₐ)\\
|
|
(p₁, p₂, \ldots{}, pₐ) & ≼ & (v₁, v₂, \ldots{}, vₐ) & iff pᵢ ≼ vᵢ ∀i ∈ [1..a]\\
|
|
\hline
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
We can also say that \emph{v} is an \emph{instance} of \emph{p}.
|
|
|
|
When we consider the pattern matrix P we say that the value vector
|
|
\(\vec{v}\) = (v₁, v₂, \ldots{}, vᵢ) matches the line number i in P if and only if the following two
|
|
conditions are satisfied:
|
|
\begin{itemize}
|
|
\item p\(_{\text{i,1}}\), p\(_{\text{i,2}}\), \(\cdots{}\), p\(_{\text{i,n}}\) ≼ (v₁, v₂, \ldots{}, vᵢ)
|
|
\item ∀j < i p\(_{\text{j,1}}\), p\(_{\text{j,2}}\), \(\cdots{}\), p\(_{\text{j,n}}\) ⋠ (v₁, v₂, \ldots{}, vᵢ)
|
|
\end{itemize}
|
|
|
|
We can define the following three relations with respect to patterns:
|
|
\begin{itemize}
|
|
\item Patter p is less precise than pattern q, written p ≼ q, when all
|
|
instances of q are instances of p
|
|
\item Pattern p and q are equivalent, written p ≡ q, when their instances
|
|
are the same
|
|
\item Patterns p and q are compatible when they share a common instance
|
|
\end{itemize}
|
|
\end{enumerate}
|
|
|
|
\subsection{1.2.1.1 Initial state of the compilation}
|
|
\label{sec:org333d6ea}
|
|
|
|
Given a source of the following form:
|
|
|
|
\#+BEGIN\_SRC ocaml
|
|
match x with
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
p₁ -> e₁\\
|
|
p₂ -> e₂\\
|
|
\end{tabular}
|
|
\end{center}
|
|
\ldots{}
|
|
\begin{center}
|
|
\begin{tabular}{l}
|
|
pₘ -> eₘ\\
|
|
\end{tabular}
|
|
\end{center}
|
|
\#+END\_SRC ocaml
|
|
|
|
the initial input of the algorithm consists of a vector of variables
|
|
\(\vec{x}\) = (x₁, x₂, \ldots{}, xₙ) of size n
|
|
and a clause matrix P → L of width n and height m.
|
|
|
|
\begin{equation*}
|
|
(P → L) =
|
|
\begin{pmatrix}
|
|
p_{1,1} & p_{1,2} & \cdots & p_{1,n} → l₁ \\
|
|
p_{2,1} & p_{2,2} & \cdots & p_{2,n} → l₂ \\
|
|
\vdots & \vdots & \ddots \vdots → \vdots \\
|
|
p_{m,1} & p_{m,2} & \cdots & p_{m,n} → lₘ
|
|
\end{pmatrix}
|
|
\end{equation*}
|
|
\end{document}
|