\section{Using Sail}
\label{sec:usage}

In its most basic use-case Sail is a command-line tool, analogous to
a compiler: one gives it a list of input Sail files; it type-checks
them and provides translated output.

To simply typecheck Sail files, one can pass them on the command line
with no other options, so for our \riscv\ spec:
\begin{verbatim}
sail prelude.sail riscv_types.sail riscv_mem.sail riscv_sys.sail riscv_vmem.sail riscv.sail
\end{verbatim}
The sail files passed on the command line are simply treated as if
they are one large file concatenated together, although the parser
will keep track of locations on a per-file basis for
error-reporting. As can be seen, this specification is split into
several logical components. \verb+prelude.sail+ defines the initial
type environment and builtins, \verb+riscv_types.sail+ gives type
definitions used in the rest of the specification, \verb+riscv_mem.sail+
and \verb+riscv_vmem.sail+ describe the physical and virtual memory
interaction, and then \verb+riscv_sys.sail+ and \verb+riscv.sail+
implement most of the specification.

For more complex projects, one can use \ll{$include} statements in
Sail source, for example:
\begin{lstlisting}
$include <library.sail>
$include "file.sail"
\end{lstlisting}

Here, Sail will look for \verb+library.sail+ in the
\verb+$SAIL_DIR/lib+, where \verb+$SAIL_DIR+ is usually the root of
the sail repository. It will search for \verb+file.sail+ relative to
the location of the file containing the \ll{$include}. The space after
the \ll{$include} is mandatory. Sail also supports \ll{$define},
\ll{$ifdef}, and \ll{$ifndef}. These are things that are understood by
Sail itself, not a separate preprocessor, and are handled after the
AST is parsed~\footnote{This can affect precedence declarations for custom user defined operators---the precedence must be redeclared in the file you are including the operator into.}.

\subsection{OCaml compilation}

To compile a Sail specification into OCaml, one calls Sail as
\begin{verbatim}
sail -ocaml FILES
\end{verbatim}
This will produce a version of the specification translated into
OCaml, which is placed into a directory called \verb+_sbuild+, similar
to ocamlbuild's \verb+_build+ directory. The generated OCaml is
intended to be fairly close to the original Sail source, and currently
we do not attempt to do much optimisation on this output.

The contents of the \verb+_sbuild+ directory are set up as an
ocamlbuild project, so one can simply switch into that directory and run
\begin{verbatim}
ocamlbuild -use-ocamlfind out.cmx
\end{verbatim}
to compile the generated model. Currently the OCaml compilation
requires that lem, linksem, and zarith are available as ocamlfind
findable libraries, and also that the environment variable
\verb+$SAIL_DIR+ is set to the root of the Sail repository.

If the Sail specification contains a \ll{main} function with type
\ll{unit -> unit} that implements a fetch/decode/execute loop then the
OCaml backend can produce a working executable, by running
\begin{verbatim}
sail -o out -ocaml FILES
\end{verbatim}
Then one can run
\begin{verbatim}
./out ELF_FILE
\end{verbatim}
to simulate an ELF file on the specification. One can do \ll{$include
  <elf.sail>} to gain access to some useful functions for accessing
information about the loaded ELF file from within the Sail
specification. In particular \verb+elf.sail+ defines a function
\ll{elf_entry : unit -> int} which can be used to set the PC to the
correct location. ELF loading is done by the linksem
library\footnote{\url{https://github.com/rems-project/linksem}}.

There is also an \verb+-ocaml_trace+ option which is the same as
\verb+-ocaml+ except it instruments the generated OCaml code with
tracing information.

\subsection{C compilation}

To compile Sail into C, the \verb+-c+ option is used, like so:
\begin{verbatim}
sail -c FILES 1> out.c
\end{verbatim}
The transated C is currently printed to stdout, so this should be
redirected to a file as above. To produce an executable this needs to
be compiled and linked with the C files in the \verb+sail/lib+
directory:
\begin{verbatim}
gcc out.c $SAIL_DIR/lib/*.c -lgmp -lz -I $SAIL_DIR/lib/ -o out
\end{verbatim}
The C output requires the GMP library for arbitrary precision
arithmetic, as well as zlib for working with compressed ELF binaries.

There are several Sail options that affect the C output:
\begin{itemize}
  \item \verb+-O+ turns on optimisations. The generated C code will be
    quite slow unless this flag is set.
  \item \verb+-Oconstant_fold+ apply constant folding optimisations.
  \item \verb+-c_include+ Supply additional header files to be
    included in the generated C.
  \item \verb+-c_no_main+ Do not generate a \verb+main()+ function.
  \item \verb+-static+ Mark generated C functions as static where
    possible. This is useful for measuring code coverage.
\end{itemize}

The generated executable for the Sail specification (provided a main
function is generated) supports several options for loading ELF files
and binary data into the specification memory.
\begin{itemize}
\item \verb+-e/--elf+ Loads an ELF file into memory. Currently only
  AArch64 and RISC-V ELF files are supported.

\item \verb+-b/--binary+ Loads raw binary data into the
  specification's memory. It is used like so:
\begin{verbatim}
./out --binary=0xADDRESS,FILE
./out -b 0xADDRESS,FILE
\end{verbatim}
The contents of the supplied file will be placed in memory starting at
the given address, which must be given as a hexadecimal number.

\item \verb+-i/--image+ For ELF files that are not loadable via the
  \verb+--elf+ flag, they can be pre-processed by Sail using linksem
  into a special image file that can be loaded via this flag. This is
  done like so:
\begin{verbatim}
sail -elf ELF_FILE -o image.bin
./out --image=image.bin
\end{verbatim}
The advantage of this flag is that it uses Linksem to process the ELF
file, so it can handle any ELF file that linksem is able to
understand. This also guarantees that the contents of the ELF binary
loaded into memory is exactly the same as for the OCaml backend and
the interpreter as they both also use Linksem internally to load ELF
files.
\item \verb+-n/--entry+ sets a custom entry point returned by the
  \ll{elf_entry} function. Must be a hexadecimal address prefixed by
  \verb+0x+.
\item \verb+-l/--cyclelimit+ run the simulation until a set number of
  cycles have been reached. The main loop of the specification must
  call the \ll{cycle_count} function for this to work.
\end{itemize}

\subsection{Lem and Isabelle}

We have a separate document detailing how to generate Isabelle
theories from Sail models, and how to work with those models in
Isabelle, see:
\begin{center}
\anonymise{\url{https://github.com/rems-project/sail/raw/sail2/snapshots/isabelle/Manual.pdf}}
\end{center}
Currently there are generated Isabelle snapshots for some of our
models in \verb+snapshots/isabelle+ in the Sail repository. These
snapshots are provided for convenience, and are not guaranteed to be
up-to-date.

In order to open a theory of one of the specifications in Isabelle,
use the \verb+-l Sail+ command-line flag to load the session containing the
Sail library. Snapshots of the Sail and Lem libraries are in the
\verb+lib/sail+ and \verb+lib/lem+ directories, respectively. You can
tell Isabelle where to find them using the \verb+-d+ flag, as in
\begin{verbatim}
isabelle jedit -l Sail -d lib/lem -d lib/sail riscv/Riscv.thy
\end{verbatim}
When run from the \verb+snapshots/isabelle+ directory this will open
the RISC-V specification.

\subsection{Interactive mode}

Compiling Sail with
\begin{verbatim}
make isail
\end{verbatim}
builds it with a GHCi-style interactive interpreter. This can be used
by starting Sail with \verb+sail -i+. If Sail is not compiled with
interactive support the \verb+-i+ flag does nothing. Sail will still
handle any other command line arguments as per usual, including
compiling to OCaml or Lem. One can also pass a list of commands to the
interpreter by using the \verb+-is+ flag, as
\begin{verbatim}
sail -is FILE
\end{verbatim}
where \verb+FILE+ contains a list of commands. Once inside the interactive
mode, a list of commands can be accessed by typing \verb+:commands+,
while \verb+:help+ can be used to provide some documentation for each
command.

\subsection{Other options}

Here we summarize most of the other options available for
Sail. Debugging options (usually for debugging Sail itself) are
indicated by starting with the letter \verb+d+.

\begin{itemize}
\item {\verb+-v+} Print the Sail version.

\item {\verb+-help+} Print a list of options.

\item {\verb+-no_warn+} Turn off warnings.

\item {\verb+-enum_casts+} Allow elements of enumerations to be
  automatically cast to numbers.

\item \verb+-memo_z3+ Memoize calls to the Z3 solver. This can greatly
  improve typechecking times if you are repeatedly typechecking the
  same specification while developing it.

\item \verb+-no_lexp_bounds_check+ Turn off bounds checking in the left
  hand side of assignments.

\item \verb+-no_effects+ Turn off effect checking. May break some
  backends that assume effects are properly checked.

\item \verb+-undefined_gen+ Generate functions that create undefined
  values of user-defined types. Every type \ll{T} will get a
  \ll{undefined_T} function created for it. This flag is set
  automatically by some backends that want to re-write \ll{undefined}.

\item \verb+-just_check+ Force Sail to terminate immediately after
  typechecking.

\item \verb+-dno_cast+ Force Sail to never perform type coercions
  under any circumstances.

\item \verb+-dtc_verbose <verbosity>+ Make the typechecker print a
  trace of typing judgements. If the verbosity level is 1, then this
  should only include fairly readable judgements about checking and
  inference rules. If verbosity is 2 then it will include a large
  amount of debugging information. This option can be useful to
  diagnose tricky type-errors, especially if the error message isn't
  very good.

\item \verb+-ddump_tc_ast+ Write the typechecked AST to stdout after
  typechecking

\item \verb+-ddump_rewrite_ast <prefix>+ Write the AST out after each
  re-writing pass. The output from each pass is placed in a file
  starting with \verb+prefix+.

\item \verb+-dsanity+ Perform extra sanity checks on the AST.

\item \verb+-dmagic_hash+ Allow the \# symbol in identifiers. It's
  currently used as a magic symbol to separate generated identifiers
  from those the user can write, so this option allows for the output
  of the various other debugging options to be fed back into Sail.
\end{itemize}