tutorial.tex

\section{Sail Language}

\subsection{Functions}
\label{sec:functions}

\input{code_myreplicatebits}

In Sail, functions are declared in two parts. First we write the type
signature for the function using the \ll{val} keyword, then define the
body of the function via the \ll{function} keyword. In this
Subsection, we will write our own version of the \ll{replicate_bits}
function from the Sail library. This function takes a number $n$ and a
bitvector, and copies that bitvector $n$ times.

\mrbval{my_replicate_bits}

\noindent The general syntax for a function type in Sail is as follows:
\begin{center}
  \ll{val} \textit{name} \ll{:} \ll{forall} \textit{type variables} \ll{,} \textit{constraint} \ll{. (} \textit{type$_1$} \ll{,} $\ldots$ \ll{,} \textit{type$_2$} \ll{)} \ll{->} \textit{return type}
\end{center}
An implementation for the \ll{replicate_bits} function would be
follows \mrbfn{my_replicate_bits}

The general syntax for a function declaration is:
\begin{center}
  \ll{function} \textit{name} \ll{(} \textit{argument$_1$} \ll{,} $\ldots$ \ll{,} \textit{argument$_n$} \ll{)} \ll{=} \textit{expression}
\end{center}

Code for this example can be found in
the Sail repository in \verb|doc/examples/my_replicate_bits.sail|. To
test it, we can invoke Sail interactively using the \verb|-i| option,
passing the above file on the command line. Typing
\verb|my_replicate_bits(3, 0xA)| will step through the execution of the
above function, and eventually return the result \verb|0xAAA|. Typing
\verb|:run| in the interactive interpreter will cause the expression
to be evaluated fully, rather than stepping through the execution.

Sail allows type variables to be used directly within expressions, so
the above could be re-written as \mrbfn{my_replicate_bits_2} This
notation can be succinct, but should be used with caution. What
happens is that Sail will try to re-write the type variables using
expressions of the appropriate size that are available within the
surrounding scope, in this case \ll{n} and \ll{length(xs)}. If no
suitable expressions are found to trivially rewrite these type
variables, then additional function parameters will be automatically
added to pass around this information at run-time.

Functions may also have implicit parameters, e.g. we can implement a
zero extension function that implicitly picks up its result length
from the calling context as follows:
\mrbval{extz}
\mrbfn{extz}

Implicit parameters are always integers, and they must appear first
before any other parameters in the function type signature.

\subsection{Mappings}
\label{sec:mappings}

Mappings are a feature of Sail that allow concise expression of
bidirectional relationships between values that are common in ISA
specifications: for example, bit-representations of an enum type or
assembly-language string representations of an instruction AST.

They are defined similarly to functions, with a \verb|val|-spec and a
definition. Currently, they only work for monomorphic types.

\begin{center}
  \ll{val} \textit{name} \ll{:}  \textit{type$_1$} \ll{<->} \textit{type$_2$}
\end{center}

\begin{center}
  \ll{mapping} \textit{name} \ll{=} \verb|{|
     \textit{pattern} \ll{<->} \textit{pattern} \ll{,}
     \textit{pattern} \ll{<->} \textit{pattern} \ll{,}
     $\ldots$
  \verb|}|
\end{center}

All the functionality of pattern matching, described below, is
available, including guarded patterns: but note that guards apply only
to one side. This sometimes leads to unavoidable duplicated code.

As a shorthand, you can also specify a mapping and its type
simultaneously.

\begin{center}
   \ll{mapping} \textit{name} \ll{:} \textit{type$_1$} \ll{<->} \textit{type$_2$} \ll{=} \verb|{|
     \textit{pattern} \ll{<->} \textit{pattern} \ll{,}
     \textit{pattern} \ll{<->} \textit{pattern} \ll{,}
     $\ldots$
  \verb|}|
\end{center}

A simple example from our RISC-V model:

\begin{lstlisting}
mapping size_bits : word_width <-> bits(2) = {
  BYTE   <-> 0b00,
  HALF   <-> 0b01,
  WORD   <-> 0b10,
  DOUBLE <-> 0b11
}
\end{lstlisting}

Mappings are used simply by calling them as if they were functions:
type inference will determine in which direction the mapping
runs. (This gives rise to the restriction that the types on either
side of a mapping must be different.)

\begin{lstlisting}
  let width : word_width = size_bits(0b00);
  let width : bits(2) = size_bits(BYTE);
\end{lstlisting}

Mappings are implemented by transforming them at compile time into a
forwards and a backwards function, along with some auxiliary
functions. Once a mapping is declared with a \verb|val|-spec, it can
be implemented by defining these functions manually instead of
defining the mapping as above. These functions and their types are:

\begin{lstlisting}
  val name_forwards : type_1 -> type_2
  val name_backwards : type_2 -> type_1
  val name_forwards_matches : type_1 -> bool
  val name_backwards_matches : type_2 -> bool
\end{lstlisting}

\subsection{Numeric Types}
\label{sec:numeric}

Sail has three basic numeric types, \ll{int}, \ll{nat}, and
\ll{range}. The type \ll{int} is an arbitrary precision mathematical
integer, and likewise \ll{nat} is an arbitrary precision natural
number. The type \ll{range('n,'m)} is an inclusive range between the
\ll{Int}-kinded type variables \ll{'n} and \ll{'m}. The type
\ll{int('o)} is an integer exactly equal to the \ll{Int}-kinded type
variable \ll{'n}, i.e. \ll{int('o)} $=$ \ll{range('o,'o)}. These types
can be used interchangeably provided the rules summarised in the below
diagram are satisfied (via constraint solving).

\begin{center}
\begin{tikzpicture}
  [type/.style={rectangle},auto,>=stealth',semithick]
  \node[type] (int) at (0, 3) {\ll{int}};
  \node[type] (nat) at (3, 0) {\ll{nat}};
  \node[type] (range) at (-3, 0) {\ll{range('n,'m)}};
  \node[type] (atom) at (0, -3) {\ll{int('o)}};

  \draw[->] (nat) -- (int);
  \draw[->] (range) -- (int);
  \draw[->] (atom) to [bend left=10] node {} (int);
  \draw[->] (range) to node {\ll{'n} $\ge$ \ll{0}} (nat);
  \draw[->] (atom) to node {\ll{'o} $\ge$ \ll{0}} (nat);
  \draw[->] (atom) to [bend right=35] node {\ll{'n} $\le$ \ll{'o} $\le$ \ll{'m}} (range);
  \draw[->] (range) to [bend right=35] node [swap] {\ll{'n} $=$ \ll{'m} $=$ \ll{'o}} (atom);
\end{tikzpicture}
\end{center}

Note that \ll{bit} isn't a numeric type (i.e. it's not
\ll{range(0,1)}. This is intentional, as otherwise it would be
possible to write expressions like \ll{(1 : bit) + 5} which would end
up being equal to \ll{6 : range(5, 6)}. This kind of implicit casting
from bits to other numeric types would be highly undesirable. The
\ll{bit} type itself is a two-element type with members \ll{bitzero} and
\ll{bitone}.

\subsection{Vector Type}
\label{sec:vec}

Sail has the built-in type \ll{vector}, which is a polymorphic type for
fixed-length vectors. For example, we could define a vector \ll{v} of
three integers as follows:
\begin{lstlisting}
let v : vector(3, dec, int) = [1, 2, 3]
\end{lstlisting}
The first argument of the vector type is a numeric expression
representing the length of the vector, and the last is the type of the
vector's elements. But what is the second argument? Sail allows two
different types of vector orderings---increasing (\ll{inc}) and
decreasing (\ll{dec}). These two orderings are shown for the bitvector
0b10110000 below.

\begin{center}
\begin{tikzpicture}[scale=0.7]
  \draw (0,0) rectangle (1,1) node[pos=.5] {1};
  \draw (1,0) rectangle (2,1) node[pos=.5] {0};
  \draw (2,0) rectangle (3,1) node[pos=.5] {1};
  \draw (3,0) rectangle (4,1) node[pos=.5] {1};
  \draw (4,0) rectangle (5,1) node[pos=.5] {0};
  \draw (5,0) rectangle (6,1) node[pos=.5] {0};
  \draw (6,0) rectangle (7,1) node[pos=.5] {0};
  \draw (7,0) rectangle (8,1) node[pos=.5] {0};

  \node at (.5,1.5) {0};
  \node at (7.5,1.5) {7};
  \draw[->] (1.5,1.5) -- (6.5,1.5);
  \node at (.5,-0.5) {MSB};
  \node at (7.5,-0.5) {LSB};
  \node at (4,2) {\ll{inc}};
\end{tikzpicture}
\qquad
\begin{tikzpicture}[scale=0.7]
  \draw (0,0) rectangle (1,1) node[pos=.5] {1};
  \draw (1,0) rectangle (2,1) node[pos=.5] {0};
  \draw (2,0) rectangle (3,1) node[pos=.5] {1};
  \draw (3,0) rectangle (4,1) node[pos=.5] {1};
  \draw (4,0) rectangle (5,1) node[pos=.5] {0};
  \draw (5,0) rectangle (6,1) node[pos=.5] {0};
  \draw (6,0) rectangle (7,1) node[pos=.5] {0};
  \draw (7,0) rectangle (8,1) node[pos=.5] {0};

  \node at (.5,1.5) {7};
  \node at (7.5,1.5) {0};
  \draw[->] (1.5,1.5) -- (6.5,1.5);
  \node at (.5,-0.5) {MSB};
  \node at (7.5,-0.5) {LSB};
  \node at (4,2) {\ll{dec}};
\end{tikzpicture}
\end{center}

For increasing (bit)vectors, the 0 index is the most significant bit
and the indexing increases towards the least significant bit. Whereas
for decreasing (bit)vectors the least significant bit is 0 indexed,
and the indexing decreases from the most significant to the least
significant bit. For this reason, increasing indexing is sometimes
called `most significant bit is zero' or MSB0, while decreasing
indexing is sometimes called `least significant bit is zero' or
LSB0. While this vector ordering makes most sense for bitvectors (it
is usually called bit-ordering), in Sail it applies to all
vectors. A default ordering can be set using
\begin{lstlisting}
default Order dec
\end{lstlisting}
and this should usually be done right at the beginning of a
specification. Most architectures stick to either convention or the
other, but Sail also allows functions which are polymorphic over
vector order, like so:
\begin{lstlisting}
val foo : forall ('a : Order). vector(8, 'a, bit) -> vector(8, 'a, bit)
\end{lstlisting}

\paragraph{Bitvector Literals}

Bitvector literals in Sail are written as either
\lstinline[mathescape]{0x$\textit{hex string}$} or
\lstinline[mathescape]{0b$\textit{binary string}$}, for example
\ll{0x12FE} or \ll{0b1010100}. The length of a hex literal is always
four times the number of digits, and the length of binary string is
always the exact number of digits, so \ll{0x12FE} has length 16, while
\ll{0b1010100} has length 7.

\paragraph{Accessing and Updating Vectors}

A vector can be indexed by using the
\lstinline[mathescape]{$\textit{vector}$[$\textit{index}$]}
notation. So, in the following code:
\begin{lstlisting}
  let v : vector(4, dec, int) = [1, 2, 3, 4]
  let a = v[0]
  let b = v[3]
\end{lstlisting}
\ll{a} will be \ll{4}, and \ll{b} will be \ll{1} (note that \ll{v} is
\ll{dec}). By default, Sail will statically check for out of bounds
errors, and will raise a type error if it cannot prove that all such
vector accesses are valid.

Vectors can be sliced using the
%
\lstinline[mathescape]{$\textit{vector}$[$\textit{index}_{msb}$ .. $\textit{index}_{lsb}$]}
%
notation. The indexes are always supplied with the index closest to
the MSB being given first, so we would take the bottom 32-bits of a
decreasing bitvector \ll{v} as \ll{v[31 .. 0]}, and the upper 32-bits
of an increasing bitvector as \ll{v[0 .. 31]}, i.e. the indexing order
for decreasing vectors decreases, and the indexing order for
increasing vectors increases.

A vector index can be updated using
\lstinline[mathescape]{[$\textit{vector}$ with $\textit{index}$ = $\textit{expression}$]}
notation.
%
Similarly, a sub-range of a vector can be updated using
%
\lstinline[mathescape]{[$\textit{vector}$ with $\textit{index}_{msb}$ .. $\textit{index}_{lsb}$ = $\textit{expression}$]},
%
where the order of the indexes is the same as described above for
increasing and decreasing vectors.

These expressions are actually just syntactic sugar for several
built-in functions, namely \ll{vector_access}, \ll{vector_subrange},
\ll{vector_update}, and \ll{vector_update_subrange}.

\subsection{List Type}

In addition to vectors, Sail also has \ll{list} as a built-in type. For
example:
\begin{lstlisting}
let l : list(int) = [|1, 2, 3|]
\end{lstlisting}
The cons operator is \ll{::}, so we could equally write:
\lstinputlisting{examples/list.sail}
Pattern matching can be used to destructure lists, see Section~\ref{sec:pat}.

\subsection{Other Types}

Sail also has a \ll{string} type, and a \ll{real} type. The \ll{real}
type is used to model arbitrary real numbers, so floating point
instructions could be specified by mapping the floating point inputs
to real numbers, performing the arithmetic operation on the real
numbers, and then mapping back to a floating point value of the
appropriate precision.

\subsection{Pattern Matching}
\label{sec:pat}

Like most functional languages, Sail supports pattern matching via the
\ll{match} keyword. For example:
\begin{lstlisting}
let n : int = f();
match n {
  1 => print("1"),
  2 => print("2"),
  3 => print("3"),
  _ => print("wildcard")
}
\end{lstlisting}
The \ll{match} keyword takes an expression and then branches using a
pattern based on its value. Each case in the match expression takes
the form \lstinline[mathescape]{$\textit{pattern}$ => $\textit{expression}$},
separated by commas. The cases are checked sequentially from top to
bottom, and when the first pattern matches its expression will be
evaluated.

\ll{match} in Sail is not currently checked for exhaustiveness---after
all we could have arbitrary constraints on a numeric variable being
matched upon, which would restrict the possible cases in ways that we
could not determine with just a simple syntactic check. However, there
is a simple exhaustiveness checker which runs and gives warnings (not
errors) if it cannot tell that the pattern match is exhaustive, but
this check can give false positives. It can be turned off with the
\verb+-no_warn+ flag.

When we match on numeric literals, the type of the variable we are
matching on will be adjusted. In the above example in the
\ll{print("1")} case, $n$ will have the type \ll{int('e)}, where
\ll{'e} is some fresh type variable, and there will be a constraint
that \ll{'e} is equal to one.

We can also have guards on patterns, for example we could modify the
above code to have an additional guarded case like so:
\begin{lstlisting}
let n : int = f();
match n {
  1 => print("1"),
  2 => print("2"),
  3 => print("3"),
  m if m <= 10 => print("n is less than or equal to 10"),
  _ => print("wildcard")
}
\end{lstlisting}
The variable pattern m will match against anything, and the guard can
refer to variables bound by the pattern.

\paragraph{Matching on enums}

Match can be used to match on possible values of an enum, like so:
\begin{lstlisting}
enum E = A | B | C

match x {
  A => print("A"),
  B => print("B"),
  C => print("C")
}
\end{lstlisting}
Note that because Sail places no restrictions on the lexical structure
of enumeration elements to differentiate them from ordinary
identifiers, pattern matches on variables and enum elements can be
somewhat ambiguous. This is the primary reason why we have the basic,
but incomplete, pattern exhaustiveness check mentioned above---it can
warn you if removing an enum constructor breaks a pattern match.

\paragraph{Matching on tuples}

We use match to destructure tuple types, for example:
\begin{lstlisting}
let x : (int, int) = (2, 3) in
match x {
  (y, z) => print("y = 2 and z = 3")
}

\end{lstlisting}

\paragraph{Matching on unions}

Match can also be used to destructure union constructors, for example
using the option type from Section~\ref{sec:union}:
\begin{lstlisting}
match option {
  Some(x) => foo(x),
  None()  => print("matched None()")
}
\end{lstlisting}
Note that like how calling a function with a unit argument can be done
as \ll{f()} rather than \ll{f(())}, matching on a constructor \ll{C}
with a unit type can be achieved by using \ll{C()} rather than
\ll{C(())}.

\paragraph{Matching on bit vectors}

Sail allows numerous ways to match on bitvectors, for example:
\begin{lstlisting}
match v {
  0xFF => print("hex match"),
  0b0000_0001 => print("binary match"),
  0xF @ v : bits(4) => print("vector concatenation pattern"),
  0xF @ [bitone, _, b1, b0] => print("vector pattern"),
  _ : bits(4) @ v : bits(4) => print("annotated wildcard pattern")
}
\end{lstlisting}
We can match on bitvector literals in either hex or binary forms. We
also have vector concatenation patterns, of the form
\lstinline[mathescape]{$\mathit{pattern}$ @ $\ldots$ @ $\mathit{pattern}$}.
We must be able to infer the length of all the sub-patterns in a vector
concatenation pattern, hence why in the example above all the
wildcard and variable patterns beneath vector concatenation patterns
have type annotations. In the context of a pattern the \ll{:} operator
binds tighter than the \ll{@} operator (as it does elsewhere).

We also have vector patterns, which for bitvectors match on individual
bits. In the above example, \ll{b0} and \ll{b1} will have type
\ll{bit}. The pattern \ll{bitone} is a bit literal, with \ll{bitzero}
being the other bit literal pattern.

Note that because vectors in Sail are type-polymorphic, we can also
use both vector concatenation patterns and vector patterns to match
against non-bit vectors.

\paragraph{Matching on lists}

Sail allows lists to be destructured using patterns. There are two
types of patterns for lists, cons patterns and list literal patterns.

\begin{lstlisting}
match ys {
  x :: xs => print("cons pattern"),
  [||]    => print("empty list")
}
\end{lstlisting}

\begin{lstlisting}
match ys {
  [|1, 2, 3|] => print("list pattern"),
  _           => print("wildcard")
}
\end{lstlisting}

\paragraph{Matching on strings}

Unusually, Sail allows strings and concatenations of strings to be
used in pattern-matching. The match operates in a simple left-to-right
fashion.

\begin{lstlisting}
  match s {
    "hello" ^ " " ^ "world" => print("matched hello world"),
    _ => print("wildcard")
  }
\end{lstlisting}

Note that a string match is always greedy, so

\begin{lstlisting}
  match s {
    "hello" ^ s ^ "world" => print("matched hello" ^ s ^ "world"),
    "hello" ^ s => print("matched hello" ^ s),
    _ => print("wildcard")
  }
\end{lstlisting}

while syntactically valid, will never match the first case.

String matching is most often used with \emph{mappings}, covered
above, to allow parsing of strings containing, for example, integers:

\begin{lstlisting}
  match s {
    "int=" ^ int(x) ^ ";" => x
    _ => -1
  }
\end{lstlisting}

This is intended to be used to parse assembly languages.


\paragraph{As patterns}

Like OCaml, Sail also supports naming parts of patterns using the
\ll{as} keyword. For example, in the above list pattern we could bind
the entire list as zs as follows:
\begin{lstlisting}
match ys {
  x :: xs as zs => print("cons with as pattern"),
  [||]          => print("empty list")
}
\end{lstlisting}
The as pattern has lower precedence than any other keyword or operator
in a pattern, so in this example zs will refer to \ll{x :: xs}.

\subsection{Mutable and Immutable Variables}

Local immutable bindings can be introduced via the \ll{let} keyword,
which has the following form
\begin{center}
  \ll{let} \textit{pattern} \ll{=} \textit{expression} \ll{in} \textit{expression}
\end{center}
The pattern is matched against the first expression, binding any
identifiers in that pattern. The pattern can have any form, as in the
branches of a match statement, but it should be complete (i.e. it
should not fail to match)\footnote{although this is not checked right
  now}.

When used in a block, we allow a variant of the let statement, where
it can be terminated by a semicolon rather than the in keyword.
\begin{lstlisting}[mathescape]
{
  let $\textit{pattern}$ = $\textit{expression}_0$;
  $\textit{expression}_1$;
  $\vdots$
  $\textit{expression}_n$
}
\end{lstlisting}
This is equivalent to the following
\begin{lstlisting}[mathescape]
{
  let $\textit{pattern}$ = $\textit{expression}_0$ in {
    $\textit{expression}_1$;
    $\vdots$
    $\textit{expression}_n$
  }
}
\end{lstlisting}
If we were to write
\begin{lstlisting}[mathescape]
{
  let $\textit{pattern}$ = $\textit{expression}_0$ in
  $\textit{expression}_1$;
  $\vdots$
  $\textit{expression}_n$ // pattern not visible
}
\end{lstlisting}
instead, then \textit{pattern} would only be bound within
$\textit{expression}_1$ and not any further expressions. In general
the block-form of let statements terminated with a semicolon should
always be preferred within blocks.

Variables bound within function arguments, match statement, and
let-bindings are always immutable, but Sail also allows mutable
variables. Mutable variables are bound implicitly by using the
assignment operator within a block.
\begin{lstlisting}
{
  x : int = 3 // Create a new mutable variable x initialised to 3
  x = 2       // Rebind it to the value 2
}
\end{lstlisting}
The assignment operator is the equality symbol, as in C and other
programming languages. Sail supports a rich language of \emph{l-value}
forms, which can appear on the left of an assignment. These will be
described in Subsection~\ref{sec:lexp}. Note that we could have
written
\begin{lstlisting}
{
  x = 3;
  x = 2
}
\end{lstlisting}
but it would not have type-checked. The reason for this is if a
mutable variable is declared without a type, Sail will try to infer
the most specific type from the right hand side of the
expression. However, in this case Sail will infer the type as
\ll{int(3)} and will therefore complain when we try to reassign it to
\ll{2}, as the type \ll{int(2)} is not a subtype of \ll{int(3)}. We
therefore declare it as an \ll{int} which as mentioned in
Section~\ref{sec:numeric} is a supertype of all numeric types. Sail
will not allow us to change the type of a variable once it has been
created with a specific type. We could have a more specific type for
the variable \ll{x}, so
\begin{lstlisting}
{
  x : {|2, 3|} = 3;
  x = 2
}
\end{lstlisting}
would allow \ll{x} to be either 2 or 3, but not any other value. The
\lstinline+{|2, 3|}+ syntax is equivalent to \lstinline+{'n, 'n in {2, 3}. int('n)}+.

\subsubsection{Assignment and l-values}
\label{sec:lexp}

It is common in ISA specifications to assign to complex l-values,
e.g.~to a subvector or named field of a bitvector register, or to an
l-value computed with some auxiliary function, e.g.~to select the
appropriate register for the current execution model.

We have l-values that allow us to write to individual elements of a
vector:
\begin{lstlisting}
{
  v : bits(8) = 0xFF;
  v[0] = bitzero;
  assert(v == 0xFE)
}
\end{lstlisting}
as well as sub ranges of a vector:
\begin{lstlisting}
{
  v : bits(8) = 0xFF;
  v[3 .. 0] = 0x0; // assume default Order dec
  assert(v == 0xF0)
}
\end{lstlisting}
We also have vector concatenation l-values, which work much like
vector concatenation patterns
\begin{lstlisting}
{
  v1 : bits(4) = 0xF;
  v2 : bits(4) = 0xF;
  v1 @ v2 = 0xAB;
  assert(v1 == 0xA & v2 == 0xB)
}
\end{lstlisting}
For structs we can write to an individual struct field as
\begin{lstlisting}
{
  s : S = struct { field = 0xFF }
  s.field = 0x00
}
\end{lstlisting}
assume we have a struct type \ll{S}, with a field simply called
\ll{field}. We can do multiple assignment using tuples, e.g.
\begin{lstlisting}
{
  (x, y) = (2, 3);
  assert(x == 2 & x == 3)
}
\end{lstlisting}

Finally, we allow functions to appear in l-values. This is a very
simple way to declare `setter' functions that look like custom
l-values, for example:
\begin{lstlisting}
{
  memory(addr) = 0x0F
}
\end{lstlisting}
This works because \ll{f(x) = y} is sugar for \ll{f(x, y)}. This
feature is commonly used when setting registers or memory that has
additional semantics for when they are read or written. We commonly
use the overloading feature to declare what appear to be getter/setter
pairs, so the above example we could implement a \ll{read_memory}
function and a \ll{write_memory} function and overload them both as
\ll{memory} to allow us to write memory using \ll{memory(addr) = data}
and read memory as \ll{data = memory(addr)}, as so:
\begin{lstlisting}
val read_memory : bits(64) -> bits(8)
val write_memory : (bits(64), bits(8)) -> unit

overload memory = {read_memory, write_memory}
\end{lstlisting}
For more details on operator and function overloading see
Section~\ref{sec:overload}.

\subsection{Registers}

Registers can be declared with a top level
\begin{center}
  \ll{register} \textit{name} \ll{:} \textit{type}
\end{center}
declaration. Registers are essentially top-level global variables and
can be set with the previously discussed l-expression forms. There is
currently no restriction on the type of a register in
Sail.\footnote{We may at some point want to enforce that they can be
  mapped to bitvectors.}

Registers differ from ordinary mutable variables as we can pass around
references to them by name. A reference to a register \ll{R} is
created as \ll{ref R}. If the register \ll{R} has the type \ll{A},
then the type of \ll{ref R} will be \ll{register(A)}. There is a
dereferencing l-value operator \ll{*} for assigning to a register
reference. One use for register references is to create a list of
general purpose registers, so they can be indexed using numeric
variables. For example:
\lstinputlisting{examples/regref.sail}

We can dereference register references using the \ll{"reg_deref"}
builtin (see Section~\ref{sec:prelude}), which is set up like so:
\begin{lstlisting}
val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
\end{lstlisting}
Currently there is no built-in syntactic sugar for dereferencing
registers in expressions.

Unlike previous versions of Sail, referencing and de-referencing
registers is done explicitly, although we can use an automatic cast to
implicitly dereference registers if that semantics is desired for a
specific specification that makes heavy use of register references,
like so:
\begin{lstlisting}
val cast auto_reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
\end{lstlisting}


\subsection{Type declarations}

\subsubsection{Enumerations}

Enumerations can be defined in either a Haskell-like syntax (useful
for smaller enums) or a more traditional C-like syntax, which is often
more readable for enumerations with more members. There are no lexical
constraints on the identifiers that can be part of an
enumeration. There are also no restrictions on the name of a
enumeration type, other than it must be a valid identifier. For
example, the following shows two ways to define the enumeration
\ll{Foo} with three members, \ll{Bar}, \ll{Baz}, and \ll{quux}:

\lstinputlisting{examples/enum1.sail}
\lstinputlisting{examples/enum2.sail}

For every enumeration type $E$ sail generates a
\lstinline[mathescape]{num_of_$E$} function and a
\lstinline[mathescape]{$E$_of_num} function, which for \ll{Foo} above
will have the following definitions\footnote{It will ensure that the
  generated function name \ll{arg} does not clash with any enumeration
  constructor.}:
\begin{lstlisting}
val Foo_of_num : forall 'e, 0 <= 'e <= 2. int('e) -> Foo
function Foo_of_num(arg) = match arg {
  0 => Bar,
  1 => Baz,
  _ => quux
}

val num_of_Foo : Foo -> {'e, 0 <= 'e <= 2. int('e)}
function num_of_Foo(arg) = match arg {
  Bar  => 0,
  Baz  => 1,
  quux => 2
}
\end{lstlisting}
Note that these functions are not automatically made into implicit
casts.

\subsubsection{Structs}

Structs are defined using the struct keyword like so:
\lstinputlisting{examples/struct.sail}

If we have a struct \ll{foo : Foo}, its fields can be accessed by
\ll{foo.bar}, and set as \ll{foo.bar = 0xF}. It can also be updated in
a purely functional fashion using the construct \ll{\{foo with bar =
  0xF\}}. A new struct value can be created with
\ll{struct \{foo = 0xF, baz = 42, quux = 3\}}. There is no lexical
restriction on the name of a struct or the names of its fields.
Pattern matching on structs is not possible.

\subsubsection{Unions}
\label{sec:union}

As an example, the \ll{maybe} type \`{a} la Haskell could be defined
in Sail as follows:
\begin{lstlisting}
union maybe ('a : Type) = {
  Just : 'a,
  None : unit
}
\end{lstlisting}
Constructors, such as \ll{Just} are called like functions, as in
\ll{Just(3) : maybe(int)}. The \ll{None} constructor is also called in
this way, as \ll{None()}. Notice that unlike in other languages, every
constructor must be associated with a type---there are no nullary
constructors. As with structs there are no lexical restrictions on the
names of either the constructors nor the type itself, other than they
must be valid identifiers.

\subsubsection{Bitfields}
\label{sec:bitfield}

The following example creates a bitfield type called \ll{cr} and a
register \ll{CR} of that type.

\lstinputlisting{examples/bitfield.sail}

A bitfield definition creates a wrapper around a bit vector type, and
generates getters and setters for the fields. For the setters, it is
assumed that they are being used to set registers with the bitfield
type\footnote{This functionality was originally called \emph{register
    types} for this reason, but this was confusing because types of
  registers are not always register types.}. If the bitvector is
decreasing then indexes for the fields must also be in decreasing
order, and vice-versa for an increasing vector. For the above example,
the bitfield wrapper type will be the following:

\begin{lstlisting}
struct cr = {bits : bitvector(8, dec)}
\end{lstlisting}

The complete vector can be accessed as \ll{CR.bits()}, and a register
of type \ll{cr} can be set like \ll{CR->bits() = 0xFF}. Getting and
setting individual fields can be done similarly, as \ll{CR.CR0()} and
\ll{CR->CR0() = 0xF}. Internally, the bitfield definition will
generate a \lstinline[mathescape]{_get_$F$} and
\lstinline[mathescape]{_set_$F$} function for each field
\lstinline[mathescape]{$F$}, and then overload them as
\lstinline[mathescape]{_mod_$F$} for the accessor syntax. The setter
takes the bitfield as a reference to a register, hence why we use the
\ll{->} notation. For pure updates of values of type \ll{cr} a
function \lstinline[mathescape]{update_$F$} is also defined. For more
details on getters and setters, see Section~\ref{sec:lexp}. A
singleton bit in a bitfield definition, such as \ll{LT : 7} will be
defined as a bitvector of length one, and not as a value of type
\ll{bit}, which mirrors the behaviour of ARM's ASL language.

\subsection{Operators}

Valid operators in Sail are sequences of the following non
alpha-numeric characters: \verb#!%&*+-./:<>=@^|#. Additionally, any
such sequence may be suffixed by an underscore followed by any valid
identifier, so \verb#<=_u# or even \verb#<=_unsigned# are valid
operator names. Operators may be left, right, or non-associative, and
there are 10 different precedence levels, ranging from 0 to 9, with 9
binding the tightest. To declare the precedence of an operator, we use a fixity declaration like:
\begin{lstlisting}
infix 4 <=_u
\end{lstlisting}
For left or right associative operators, we'd use the keywords
\ll{infixl} or \ll{infixr} respectively. An operator can be used
anywhere a normal identifier could be used via the \ll{operator}
keyword. As such, the \verb#<=_u# operator can be defined as:
\begin{lstlisting}
val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool
function operator <=_u(x, y) = unsigned(x) <= unsigned(y)
\end{lstlisting}

\paragraph{Builtin precedences}
The precedence of several common operators are built into Sail. These
include all the operators that are used in type-level numeric
expressions, as well as several common operations such as equality,
division, and modulus. The precedences for these operators are
summarised in Table~\ref{tbl:operators}.

\begin{table}[hbt]
  \center
  \begin{tabular}{| c || l | l | l |}
    \hline
    Precedence & Left associative & Non-associative & Right associative\\
    \hline
    9 & & &\\
    \hline
    8 & & & \ll{^}\\
    \hline
    7 & \ll{*}, \ll{/}, \ll{\%} & &\\
    \hline
    6 & \ll{+}, \ll{-} & &\\
    \hline
    5 & & &\\
    \hline
    4 & & \ll{<}, \ll{<=}, \ll{>}, \ll{>=}, \ll{!=}, \ll{=}, \ll{==} &\\
    \hline
    3 & & & \ll{&}\\
    \hline
    2 & & & \ll{|}\\
    \hline
    1 & & &\\
    \hline
    0 & & &\\
    \hline
  \end{tabular}
  \caption{Default Sail operator precedences}
  \label{tbl:operators}
\end{table}

\paragraph{Type operators}
Sail allows operators to be used at the type level. For example, we
could define a synonym for the built-in \ll{range} type as:
\lstinputlisting{examples/type_operator.sail} Note that we can't use
\ll{..} as an operator name, because that is reserved syntax for
vector slicing. Operators used in types always share precedence with
identically named operators at the expression level.

\subsection{Ad-hoc Overloading}
\label{sec:overload}

Sail has a flexible overloading mechanism using the \ll{overload}
keyword
\begin{center}
  \ll{overload} \textit{name} \ll{=} \lstinline+{+ \textit{name}$_1$ \ll{,} \ldots \ll{,} \textit{name}$_n$ \lstinline+}+
\end{center}
This takes an identifier name, and a list of other identifier names to
overload that name with. When the overloaded name is seen in a Sail
definition, the type-checker will try each of the overloads in order
from left to right (i.e. from $\textit{name}_1$ to $\textit{name}_n$).
until it finds one that causes the resulting expression to type-check
correctly.

Multiple \ll{overload} declarations are permitted for the same
identifier, with each overload declaration after the first adding its
list of identifier names to the right of the overload list (so earlier
overload declarations take precedence over later ones). As such, we
could split every identifier from above syntax example into its own
line like so:
\begin{center}
  \ll{overload} \textit{name} \ll{=} \lstinline+{+ \textit{name}$_1$ \lstinline+}+\\
  $\vdots$\\
  \ll{overload} \textit{name} \ll{=} \lstinline+{+ \textit{name}$_n$ \lstinline+}+
\end{center}

As an example for how overloaded functions can be used, consider the
following example, where we define a function \ll{print_int} and a
function \ll{print_string} for printing integers and strings
respectively. We overload \ll{print} as either \ll{print_int} or
\ll{print_string}, so we can print either number such as 4, or strings
like \ll{"Hello, World!"} in the following \ll{main} function
definition.

\lstinputlisting{examples/overload.sail}

We can see that the overloading has had the desired effect by dumping
the type-checked AST to stdout using the following command
\verb+sail -ddump_tc_ast examples/overload.sail+. This will print the
following, which shows how the overloading has been resolved
\begin{lstlisting}
function main () : unit = {
  print_string("Hello, World!");
  print_int(4)
}
\end{lstlisting}
This option can be quite useful for testing how overloading has been
resolved. Since the overloadings are done in the order they are listed
in the source file, it can be important to ensure that this order is
correct. A common idiom in the standard library is to have versions of
functions that guarantee more constraints about their output be
overloaded with functions that accept more inputs but guarantee less
about their results. For example, we might have two division functions:
\begin{lstlisting}
val div1 : forall 'm 'n, 'n >= 0 & 'm > 0. (int('n), int('m)) -> {'o, 'o >= 0. int('o)}

val div2 : (int, int) -> option(int)
\end{lstlisting}
The first guarantees that if the first argument is greater than or
equal to zero, and the second argument is greater than zero, then the
result will be greater than or equal to zero. If we overload these
definitions as
\begin{lstlisting}
overload operator / = {div1, div2}
\end{lstlisting}
Then the first will be applied when the constraints on its inputs can
be resolved, and therefore the guarantees on its output can be
guaranteed, but the second will be used when this is not the case, and
indeed, we will need to manually check for the division by zero case
due to the option type. Note that the return type can be very
different between different cases in the overload.

The amount of arguments overloaded functions can have can also vary,
so we can use this to define functions with optional arguments, e.g.
\lstinputlisting{examples/zeros.sail} In this example, we can call
\ll{zero_extend} and the return length is implicit (likely using
\ll{sizeof}, see Section~\ref{sec:sizeof}) or we can provide it
ourselves as an explicit argument.

%% \subsection{Getters and Setters}
%% \label{sec:getset}

%% We have already seen some examples of getters and setters in
%% Subsection~\ref{sec:bitfield}, but they can be used in many other
%% contexts.

%% \fbox{TODO}

\subsection{Sizeof and Constraint}
\label{sec:sizeof}

As already mentioned in Section~\ref{sec:functions}, Sail allows for
arbitrary type variables to be included within expressions. However,
we can go slightly further than this, and include both arbitrary
(type-level) numeric expressions in code, as well as type
constraints. For example, if we have a function that takes two
bitvectors as arguments, then there are several ways we could compute
the sum of their lengths.
\begin{lstlisting}
val f : forall 'n 'm. (bits('n), bits('m)) -> unit

function f(xs, ys) = {
  let len = length(xs) + length(ys);
  let len = 'n + 'm;
  let len = sizeof('n + 'm);
  ()
}
\end{lstlisting}
Note that the second line is equivalent to
\begin{lstlisting}
  let len = sizeof('n) + sizeof('n)
\end{lstlisting}

There is also the \ll{constraint} keyword, which takes a type-level constraint and allows it to be used as a boolean expression, so we could write:
\begin{lstlisting}
function f(xs, ys) = {
  if constraint('n <= 'm) {
    // Do something
  }
}
\end{lstlisting}
rather than the equivalent test \ll{length(xs) <= length(ys)}. This way
of writing expressions can be succinct, and can also make it very
explicit what constraints will be generated during flow
typing. However, all the constraint and sizeof definitions must be
re-written to produce executable code, which can result in the
generated theorem prover output diverging (in appearance) somewhat
from the source input. In general, it is probably best to use
\ll{sizeof} and \ll{constraint} sparingly.

However, as previously mentioned both \ll{sizeof} and \ll{constraint}
can refer to type variables that only appear in the output or are
otherwise not accessible at runtime, and so can be used to implement
implicit arguments, as was seen for \ll{replicate_bits} in
Section~\ref{sec:functions}.

\subsection{Scattered Definitions}
\label{sec:scattered}
In a Sail specification, sometimes it is desirable to collect together
the definitions relating to each machine instruction (or group
thereof), e.g.~grouping the clauses of an AST type with the associated
clauses of decode and execute functions, as in
Section~\ref{sec:riscv}. Sail permits this with syntactic sugar for
`scattered' definitions. Either functions or union types can be
scattered.

One begins a scattered definition by declaring the name and kind
(either function or union) of the scattered definition, e.g.
\begin{lstlisting}
scattered function foo

scattered union bar
\end{lstlisting}
This is then followed by a list of clauses for either the union or the
function, which can be freely interleaved with other definitions (such
as \ll{E} in the below code)
\begin{lstlisting}[mathescape]
union clause bar : Baz(int, int)

function clause foo(Baz(x, y)) = $\ldots$

enum E = A | B | C

union clause bar : Quux(string)

function clause foo(Quux(str)) = print(str)
\end{lstlisting}
Finally the scattered definition is ended with the \ll{end} keyword, like so:
\begin{lstlisting}
end foo

end bar
\end{lstlisting}

Semantically, scattered definitions of union types appear at the start
of their definition, and scattered definitions of functions appear at
the end. A scattered function definition can be recursive, but
mutually recursive scattered function definitions should be avoided.

\subsection{Exceptions}
\label{sec:exn}

Perhaps surprisingly for a specification language, Sail has exception
support. This is because exceptions as a language feature do sometimes
appear in vendor ISA pseudocode, and such code would be very difficult
to translate into Sail if Sail did not itself support exceptions. We
already translate Sail to monadic theorem prover code, so working with
a monad that supports exceptions there is fairly natural.

For exceptions we have two language features: \ll{throw} statements
and \ll{try}-\ll{catch} blocks. The throw keyword takes a value of
type \ll{exception} as an argument, which can be any user defined type
with that name. There is no builtin exception type, so to use
exceptions one must be set up on a per-project basis. Usually the
exception type will be a union, often a scattered union, which allows
for the exceptions to be declared throughout the specification as they
would be in OCaml, for example: \lstinputlisting{examples/exn.sail}
Note how the use of the scattered type allows additional exceptions to
be declared even after they are used.

\subsection{Preludes and Default Environment}
\label{sec:prelude}

By default Sail has almost no built-in types or functions, except for
the primitive types described in this Chapter. This is because
different vendor-pseudocodes have varying naming conventions and
styles for even the most basic operators, so we aim to provide
flexibility and avoid committing to any particular naming convention or
set of built-ins. However, each Sail backend typically implements
specific external names, so for a PowerPC ISA description one might
have:
\begin{lstlisting}[mathescape]
val EXTZ = "zero_extend" : $\ldots$
\end{lstlisting}
while for ARM, one would have
\begin{lstlisting}[mathescape]
val ZeroExtend = "zero_extend" : $\ldots$
\end{lstlisting}
where each backend knows about the \ll{"zero_extend"} external name,
but the actual Sail functions are named appropriately for each
vendor's pseudocode. As such each Sail ISA spec tends to have its own
prelude.

However, the \verb+lib+ directory in the Sail repository contains some
files that can be included into any ISA specification for some basic
operations. These are listed below:
\begin{description}
  \item[flow.sail] Contains basic definitions required for flow
    typing to work correctly.
  \item[arith.sail] Contains simple arithmetic operations for
    integers.
  \item[vector\_dec.sail] Contains operations on decreasing
    (\ll{dec}) indexed vectors, see Section~\ref{sec:vec}.
  \item[vector\_inc.sail] Like \verb+vector_dec.sail+, except
    for increasing (\ll{inc}) indexed vectors.
  \item[option.sail] Contains the definition of the option
    type, and some related utility functions.
  \item[prelude.sail] Contains all the above files, and chooses
    between \verb+vector_dec.sail+ and \verb+vector_inc.sail+ based on
    the default order (which must be set before including this file).
  \item[smt.sail] Defines operators allowing div, mod, and abs
    to be used in types by exposing them to the Z3 SMT solver.
  \item[exception\_basic.sail] Defines a trivial exception type, for
    situations where you don't want to declare your own (see
    Section~\ref{sec:exn}).
\end{description}