UniTO/tesi/tesi_unicode.org

\begin{comment}
* TODO Scaletta [1/5]
  - [X] Abstract
  - [-] Background [40%]
    - [X] Ocaml
    - [ ] Lambda code [0%]
      - [ ] Compiler optimizations
      - [ ] other instructions
    - [X] Pattern matching 
    - [ ] Symbolic execution
    - [ ] Translation Validation
  - [ ] Translation validation of the Pattern Matching Compiler
    - [ ] Source translation
      - [ ] Formal Grammar
      - [ ] Compilation of source patterns
      - [ ] Rest?
    - [ ] Target translation
      - [ ] Formal Grammar
      - [ ] Symbolic execution of the lambda target
    - [ ] Equivalence between source and target
  - [ ] Proof of correctness
  - [ ] Practical results 
  
\end{comment}

#+TITLE:   Translation Verification of the OCaml pattern matching compiler
#+AUTHOR:   Francesco Mecca
#+EMAIL:    me@francescomecca.eu
#+DATE:

#+LANGUAGE: en
#+LaTeX_CLASS: article
#+LaTeX_HEADER: \usepackage{algorithm} 
#+LaTeX_HEADER: \usepackage{comment} 
#+LaTeX_HEADER: \usepackage{algpseudocode} 
#+LaTeX_HEADER: \usepackage{amsmath,amssymb,amsthm}
#+Latex_HEADER: \newtheorem{definition}{Definition}
#+LaTeX_HEADER: \usepackage{graphicx} 
#+LaTeX_HEADER: \usepackage{listings} 
#+LaTeX_HEADER: \usepackage{color} 
#+EXPORT_SELECT_TAGS: export
#+EXPORT_EXCLUDE_TAGS: noexport
#+OPTIONS: H:2 toc:nil \n:nil @:t ::t |:t ^:{} _:{} *:t TeX:t LaTeX:t
#+STARTUP: showall
\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}

* Background

** OCaml
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:
    - 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 lists of integers, lists of strings and in general
      lists 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 /principal type/.
      For example the principal type of the List.length function is "For any /a/, function from
      list of /a/ to /int/" and /a/ is called the /type parameter/.
    - 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.
    - Type Inference: the principal type of a well formed term can be inferred without any
      annotation or declaration.
    - 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 /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.
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.

** Lambda form compilation
\begin{comment}
https://dev.realworldocaml.org/compiler-backend.html
\end{comment}

OCaml provides compilation in form of a byecode executable with an
optionally embeddable interpreter and a native executable that could
be statically linked to provide a single file executable.

After the OCaml typechecker has proven that the program is type safe,
the OCaml compiler lower the code to /Lambda/, an s-expression based
language that assumes that its input has already been proved safe.
On the /Lambda/ representation of the source program, the compiler
performes a series of optimization passes before translating the
lambda form to assembly code.

*** OCaml datatypes

Most native data types in OCaml, such as integers, tuples, lists,
records, can be seen as instances of the following definition

#+BEGIN_SRC ocaml
type t = Nil | One of int | Cons of int * t 
#+END_SRC
that is a type /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. 

*** Lambda form types
A lambda form target file produced by the ocaml compiler consists of a
single s-expression. Every s-expression consist of /(/, a sequence of
elements separated by a whitespace and a closing /)/.
Elements of s-expressions are:
- Atoms: sequences of ascii letters, digits or symbols
- Variables
- Strings: enclosed in double quotes and possibly escaped
- S-expressions: allowing arbitrary nesting

There are several numeric types:
- integers: that us either 31 or 63 bit two's complement arithmetic
  depending on system word size, and also wrapping on overflow
- 32 bit and 64 bit integers: that use 32-bit and 64-bit two's complement arithmetic
  with wrap on overflow
- big integers: offer integers with arbitrary precision
- floats: that use IEEE754 double-precision (64-bit) arithmetic with
  the addition of the literals /infinity/, /neg_infinity/ and /nan/.

The are varios numeric operations defined:

- Arithmetic operations: +, -, *, /, % (modulo), neg (unary negation)
- Bitwise operations: &, |, ^, <<, >> (zero-shifting), a>> (sign extending)
- Numeric comparisons: <, >, <=, >=, ==

*** Functions

Functions are defined using the following syntax, and close over all
bindings in scope: (lambda (arg1 arg2 arg3) BODY)
and are applied using the following syntax: (apply FUNC ARG ARG ARG)
Evaluation is eager.

*** Bindings
The atom /let/ introduces a sequence of bindings:
(let BINDING BINDING BINDING ... BODY)

*** Other atoms
TODO: if, switch, stringswitch...
TODO: magari esempi


** Pattern matching

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 on the other hands express predicates through
syntactic templates that also allow to bind on data structures of
arbitrary shapes. One common example of pattern matching is the use of regular
expressions on strings. OCaml provides pattern matching on ADT and
primitive data types.
The result of a pattern matching operation is always one of:
- this value does not match this pattern”
- this value matches this pattern, resulting the following bindings of
  names to values and the jump to the expression pointed at the
  pattern.

#+BEGIN_SRC ocaml
type color = | Red | Blue | Green | Black | White

match color with
| Red -> print "red"
| Blue -> print "red"
| Green -> print "red"
| _ -> print "white or black"
#+END_SRC

OCaml provides tokens to express data destructoring.
For example we can examine the content of a list with patten matching

#+BEGIN_SRC ocaml

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_SRC

Parenthesized patterns, such as the third one in the previous example,
matches the same value as the pattern without parenthesis.

The same could be done with tuples
#+BEGIN_SRC ocaml

begin match tuple with
| (Some _, Some _) -> print "Pair of optional types"
| (Some _, None) | (None, Some _) -> print "Pair of optional types, one of which is null"
| (None, None) -> print "Pair of optional types, both null"
#+END_SRC

The pattern pattern₁ |  pattern₂ represents the logical "or" of the
two patterns pattern₁ and pattern₂. A value matches pattern₁ |
pattern₂ if it matches pattern₁ or pattern₂.

Pattern clauses can make the use of /guards/ to test predicates and
variables can captured (binded in scope).

#+BEGIN_SRC ocaml

begin match token_list with
| "switch"::var::"{"::rest -> ...
| "case"::":"::var::rest when is_int var -> ...
| "case"::":"::var::rest when is_string var -> ...
| "}"::[ ] -> ...
| "}"::rest -> error "syntax error: " rest

#+END_SRC

Moreover, the OCaml pattern matching compiler emits a warning when a
pattern is not exhaustive or some patterns are shadowed by precedent ones.

In general pattern matching on primitive and algebraic data types takes the
following form.

|match variable with
|\vert pattern₁ -> expr₁
|\vert pattern₂ when guard -> expr₂
|\vert pattern₃ as var -> expr₃ 
|⋮
|\vert pₙ -> exprₙ

It can be described more formally through a BNF grammar.

#+BEGIN_SRC bnf

pattern ::= value-name  
| _   ;; wildcard pattern
| constant  ;; matches a constant value
| pattern as  value-name  ;; binds to value-name
| ( pattern ) ;; parenthesized pattern
| pattern |  pattern ;; or-pattern 
| constr  pattern ;; variant pattern
| [ pattern  { ; pattern }  [ ; ] ] ;; list patterns 
| pattern ::  pattern   ;; lists patterns using cons operator (::)
| [| pattern  { ; pattern }  [ ; ] |] ;; array pattern 
| char-literal ..  char-literal   ;; match on a range of characters
| { field  [: typexpr]  [= pattern] { ; field  [: typexpr]  [= pattern] } \
  [; _ ] [ ; ] } ;; patterns that match on records

#+END_SRC

\begin{comment}
*** 1.2.1 Pattern matching compilation to lambda code

During compilation, patterns are in the form
| pattern         | type of pattern    |
|-----------------+---------------------|
| _               | wildcard            |
| x               | variable            |
| c(p₁,p₂,...,pₙ) | constructor pattern |
| (p₁\vert p₂)    | or-pattern          |

Expressions are compiled into lambda code and are referred as lambda
code actions.

The entire pattern matching code can be represented as a clause matrix
that associates rows of patterns (p_{i,1}, p_{i,2}, ..., p_{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*}

The pattern /p/ matches a value /v/, written as p ≼ v, when one of the
following rules apply

|--------------------+---+--------------------+-------------------------------------------|
| _                  | ≼ | v                  | ∀v                                        |
| x                  | ≼ | v                  | ∀v                                        |
| (p₁ \vert\ p₂)     | ≼ | v                  | iff p₁ ≼ v or p₂ ≼ v                      |
| c(p₁, p₂, ..., pₐ) | ≼ | c(v₁, v₂, ..., vₐ) | iff (p₁, p₂, ..., pₐ) ≼ (v₁, v₂, ..., vₐ) |
| (p₁, p₂, ..., pₐ)  | ≼ | (v₁, v₂, ..., vₐ)  | iff pᵢ ≼ vᵢ ∀i ∈ [1..a]                   |
|--------------------+---+--------------------+-------------------------------------------|

When a value /v/ matches pattern /p/ we say that /v/ is an /instance/ of /p/.

Considering the pattern matrix P we say that the value vector
$\vec{v}$ = (v₁, v₂, ..., vᵢ) matches the line number i in P  if and only if the following two
conditions are satisfied:
- p_{i,1}, p_{i,2}, \cdots, p_{i,n}  ≼ (v₁, v₂, ..., vᵢ)
- ∀j < i p_{j,1}, p_{j,2}, \cdots, p_{j,n} ⋠ (v₁, v₂, ..., vᵢ) 

We can define the following three relations with respect to patterns:
- Patter p is less precise than pattern q, written p ≼ q, when all
  instances of q are instances of p
- Pattern p and q are equivalent, written p ≡ q, when their instances
  are the same
- Patterns p and q are compatible when they share a common instance

**** Initial state of the compilation

Given a source of the following form:


|match variable with
|\vert pattern₁ -> e₁
|\vert pattern₂ -> e₂
|⋮
|\vert pₘ -> eₘ

the initial input of the algorithm C consists of a vector of variables
$\vec{x}$ = (x₁, x₂, ..., xₙ)  of size /n/ where /n/ is the arity of
the type of /x/ and a clause matrix P → L of width n and height m.
That is:

\begin{equation*}
C((\vec{x} = (x₁, x₂, ..., xₙ),
\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*}

The base case C₀ of the algorithm is the case in which the $\vec{x}$
is empty, that is $\vec{x}$ = (), then the result of the compilation
C₀ is l₁
\begin{equation*}
C₀((),
\begin{pmatrix}
→ l₁ \\
→ l₂ \\
→  \vdots \\
→ lₘ
\end{pmatrix})
) = l₁
\end{equation*}

When $\vec{x}$ ≠ () then the compilation advances using one of the
following four rules:

1) Variable rule: if all patterns of the first column of P are wildcard patterns or
   bind the value to a variable, then 

    \begin{equation*}
    C(\vec{x}, P → L) = C((x₂, x₃, ..., xₙ), P' → L')
    \end{equation*}
    where
    \begin{equation*}
    \begin{pmatrix}
    p_{1,2} & \cdots & p_{1,n} & → & (let & y₁ & x₁) & l₁ \\
    p_{2,2} & \cdots & p_{2,n} & → & (let & y₂ & x₁) & l₂ \\
    \vdots & \ddots & \vdots & →  & \vdots & \vdots & \vdots & \vdots \\
    p_{m,2} & \cdots & p_{m,n} & → & (let & yₘ & x₁) & lₘ
    \end{pmatrix}
    \end{equation*}

    That means in every lambda action lᵢ there is a binding of x₁ to the
    variable that appears on the pattern $p_{i,1}. Bindings are omitted
    for wildcard patterns and the lambda action lᵢ remains unchanged.

2) Constructor rule: if all patterns in the first column of P are
   constructors patterns of the form k(q₁, q₂, ..., qₙ) we define a
   new matrix, the specialized clause matrix S, by applying the
   following transformation on every row /p/:
    \begin{lstlisting}[mathescape,columns=fullflexible,basicstyle=\fontfamily{lmvtt}\selectfont,]
    for every c ∈ Set of constructors 
        for i ← 1 .. m 
            let kᵢ ← constructor_of($p_{i,1}$) 
            if kᵢ = c then 
                p ← $q_{i,1}$, $q_{i,2}$, ..., $q_{i,n'}$,  $p_{i,2}$, $p_{i,3}$, ..., $p_{i, n}$
    \end{lstlisting}
   Patterns of the form $q_{i,j}$ matches on the values of the
   constructor and we define new fresh variables y₁, y₂, ..., yₐ so
   that the lambda action lᵢ becomes

\begin{lstlisting}[mathescape,columns=fullflexible,basicstyle=\fontfamily{lmvtt}\selectfont,]
    (let (y₁ (field 0 x₁))
         (y₂ (field 1 x₁))
         ...
         (yₐ (field (a-1) x₁))
         lᵢ)
\end{lstlisting}

   and the result of the compilation for the set of constructors
   {c₁, c₂, ..., cₖ} is:

\begin{lstlisting}[mathescape,columns=fullflexible,basicstyle=\fontfamily{lmvtt}\selectfont,]
    switch x₁ with
    case c₁: l₁
    case c₂: l₂
    ...
    case cₖ: lₖ
    default: exit
\end{lstlisting}

3) Orpat rule: there are various strategies for dealing with
   or-patterns. The most naive one is to split the or-patterns.
   For example a row p containing an or-pattern:
   \begin{equation*}
   (p_{i,1}|q_{i,1}|r_{i,1}), p_{i,2}, ..., p_{i,m} → lᵢ
   \end{equation*}
   results in three rows added to the clause matrix
   \begin{equation*}
   p_{i,1}, p_{i,2}, ..., p_{i,m} → lᵢ \\
   \end{equation*}
   \begin{equation*}
   q_{i,1}, p_{i,2}, ..., p_{i,m} → lᵢ \\
   \end{equation*}
   \begin{equation*}
   r_{i,1}, p_{i,2}, ..., p_{i,m} → lᵢ 
   \end{equation*}
4) Mixture rule:
   When none of the previous rules apply the clause matrix P → L is
   splitted into two clause matrices, the first P₁ → L₁ that is the
   largest prefix matrix for which one of the three previous rules
   apply, and P₂ → L₂ containing the remaining rows. The algorithm is
   applied to both matrices.

\end{comment}

\begin{comment}
#+BEGIN_COMMENT
CITE paper?
#+END_COMMENT’ 
\end{comment}

** Symbolic execution

** Translation validation
Translators, such as translators and code generators, are huge pieces of
software usually consisting of multiple subsystem and
constructing an actual specification of a translator implementation for
formal validation is a very long task. Moreover, different
translators implement different algorithms, so the correctness proof of
a translator cannot be generalized and reused to prove another translator.
Translation validation is an alternative to the verification of
existing translators that consists of taking the source and the target
(compiled) program and proving /a posteriori/ their semantic equivalence.

- [ ] Techniques for translation validation
- [ ] What does semantically equivalent mean
- [ ] What happens when there is no semantic equivalence
- [ ] Translation validation through symbolic execution

** Translation validation of the Pattern Matching Compiler
    - [ ] Source translation
      - [ ] Formal Grammar
      - [ ] Compilation of source patterns
      - [ ] Rest?