path: root/doc/usage.tex

\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 translated C is by default printed to stdout, but one can also use
the \verb+-o+ option to output to a file, so
\begin{verbatim}
sail -c FILES -o out
\end{verbatim}
will generate a file called \verb+out.c+. 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, Isabelle \& HOL4}

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{\LaTeX\ Generation}

Sail can be used to generate latex for inclusion in documentation as:
\begin{verbatim}
sail -o DIRECTORY -latex FILES
\end{verbatim}
The list of \verb+FILES+ is a list of Sail files to produce latex for,
and \verb+DIRECTORY+ is the directory where the generated latex will
be placed. The list of files must be a valid type-checkable series of
Sail files. The intention behind this latex generation is for it to be
included within existing ISA manuals written in Latex, as such the
latex output generates a list of commands for each top-level Sail
declaration in \verb+DIRECTORY/commands.tex+. The rest of this section
discusses the stable features of the latex generation process---there
are additional features for including markdown doc-comments in Sail
code and formatting them into latex for inclusion id documentation,
among other things, but these features are not completely stable
yet. This manual itself makes use of the Sail latex generation, so
\verb+doc/manual.tex+, and \verb+doc/Makefile+ can be used to see how
the process is set up.


\paragraph{Requirements} The generated latex uses the \emph{listings} package for formatting
source code, uses the macros in the \emph{etoolbox} package for the
generated commands, and relies on the \emph{hyperref} package for
cross-referencing. These packages are available in most TeX
distributions, and are available as part of thetexlive packages for
Ubuntu.

\paragraph{Usage} Due to the oddities of latex verbatim environments each Sail
declaration must be placed in it's own file then the command in
\verb+commands.tex+ includes in with \verb+\lstinputlisting+. To
include the generated Sail in a document one would do something like:
\begin{lstlisting}[language=TeX]
  \input{commands.tex}
  \sailval{my_function}
  \sailfn{my_function}
\end{lstlisting}
which would enclude the type declaration (\verb+\sailval+) for
\verb+my_function+ as well as type body of that function
(\verb+\sailfn+).

It is sometimes useful to include multiple versions of the same Sail
definitions in a latex document. In this case the \verb+-latex_prefix+
option can be used. For example if we used \verb+-latex_prefix prefix+
then the above example would become:
\begin{lstlisting}[language=TeX]
  \input{commands.tex}
  \prefixval{my_function}
  \prefixfn{my_function}
\end{lstlisting}

The generated definitions are created wrapped in customisable macros
that can be overridden to change the formatting of the Sail code. For
\verb+\sailfn+ there is a macro \verb+\saildocfn+ that must be defined,
and similarly for the other Sail toplevel types.

\paragraph{Cross-referencing} For each macro \verb+\sail+\emph{X}\verb+{id}+ there is a macro
\verb+\sailref+\emph{X}\verb+{id}{text}+ which creates a
hyper-reference to the original definition. This requires the
hyper-ref package.

\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}