diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/examples/exn.sail | 20 | ||||
| -rw-r--r-- | doc/examples/list.sail | 1 | ||||
| -rw-r--r-- | doc/examples/my_replicate_bits.sail | 3 | ||||
| -rw-r--r-- | doc/examples/regref.sail | 17 | ||||
| -rw-r--r-- | doc/manual.tex | 7 | ||||
| -rw-r--r-- | doc/riscv.tex | 15 | ||||
| -rw-r--r-- | doc/tutorial.tex | 260 | ||||
| -rw-r--r-- | doc/types.tex | 2 | ||||
| -rw-r--r-- | doc/usage.tex | 44 |
9 files changed, 327 insertions, 42 deletions
diff --git a/doc/examples/exn.sail b/doc/examples/exn.sail new file mode 100644 index 00000000..de97e3f9 --- /dev/null +++ b/doc/examples/exn.sail @@ -0,0 +1,20 @@ +val print = {ocaml: "print_endline"} : string -> unit + +scattered union exception + +union clause exception = Epair : (range(0, 255), range(0, 255)) + +union clause exception = Eunknown : string + +function main() : unit -> unit = { + try { + throw(Eunknown("foo")) + } catch { + Eunknown(msg) => print(msg), + _ => exit() + } +} + +union clause exception = Eint : int + +end exception diff --git a/doc/examples/list.sail b/doc/examples/list.sail new file mode 100644 index 00000000..4eaeb67a --- /dev/null +++ b/doc/examples/list.sail @@ -0,0 +1 @@ +let l : list(int) = 1 :: 2 :: 3 :: [||]
\ No newline at end of file diff --git a/doc/examples/my_replicate_bits.sail b/doc/examples/my_replicate_bits.sail index bd45a32d..c9972cd6 100644 --- a/doc/examples/my_replicate_bits.sail +++ b/doc/examples/my_replicate_bits.sail @@ -11,7 +11,8 @@ val "shiftl" : forall 'm. (bits('m), int) -> bits('m) val operator >> = { ocaml: "shiftr_ocaml", c: "shiftr_c", - lem: "shiftr_lem" + lem: "shiftr_lem", + _: "shiftr" } : forall 'm. (bits('m), int) -> bits('m) val "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) diff --git a/doc/examples/regref.sail b/doc/examples/regref.sail new file mode 100644 index 00000000..268af295 --- /dev/null +++ b/doc/examples/regref.sail @@ -0,0 +1,17 @@ +default Order dec +$include <prelude.sail> + +register X0 : bits(8) +register X1 : bits(8) +register X2 : bits(8) + +let X : vector(3, dec, register(bits(8))) = [ref X2, ref X1, ref X0] + +function main() : unit -> unit = { + X0 = 0xFF; + assert(X0 == 0xFF); + (*X[0]) = 0x11; + assert(X0 == 0x11); + (*ref X0) = 0x00; + assert(X0 == 0x00) +}
\ No newline at end of file diff --git a/doc/manual.tex b/doc/manual.tex index a52600a5..3b75b26a 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -25,7 +25,7 @@ \lstdefinelanguage{sail} { morekeywords={val,function,cast,type,forall,overload,operator,enum,union,undefined,exit,and,assert,sizeof, scattered,register,inc,dec,if,then,else,effect,let,as,@,in,end,Type,Int,Order,match,clause,struct, - foreach,from,to,by,infix,infixl,infixr,bitfield,default}, + foreach,from,to,by,infix,infixl,infixr,bitfield,default,try,catch,throw}, keywordstyle={\bf\ttfamily\color{blue}}, morestring=[b]", stringstyle={\ttfamily\color{red}}, @@ -64,8 +64,9 @@ \title{The Sail instruction-set semantics specification language} -\author{Kathryn E. Gray \and Peter Sewell \and Christopher Pulte \and - Shaked Flur \and Robert Norton-Wright \and Alasdair Armstrong} +\author{Alasdair Armstrong \and Thomas Bauereiss \and Brian Campbell \and + Shaked Flur \and Kathryn E. Gray \and Robert Norton-Wright \and Christopher Pulte \and + Peter Sewell} \maketitle diff --git a/doc/riscv.tex b/doc/riscv.tex index e2aa3025..1e50c90c 100644 --- a/doc/riscv.tex +++ b/doc/riscv.tex @@ -63,14 +63,13 @@ register Xs : vector(32, dec, xlen_t) \sailX We also give a function \ll{MEMr} for reading memory, this function -just points at a builtin we have defined elsewhere \TODO{Section where - we talk about preludes, built-in type environment etc}. Note that functions in sail are -annotated with effects. This effect system is quite basic, but -indicates whether or not functions read or write registers (rreg and -wreg), read and write memory (rmem and wmem), as well as a host of -other concurrency model related effects. They also indicate whether a -function throws exceptions or has other non-local control flow (the -escape effect). +just points at a builtin we have defined elsewhere. Note that +functions in sail are annotated with effects. This effect system is +quite basic, but indicates whether or not functions read or write +registers (rreg and wreg), read and write memory (rmem and wmem), as +well as a host of other concurrency model related effects. They also +indicate whether a function throws exceptions or has other non-local +control flow (the escape effect). \sailMEMr \sailfnMEMr diff --git a/doc/tutorial.tex b/doc/tutorial.tex index 98a06710..34046e2b 100644 --- a/doc/tutorial.tex +++ b/doc/tutorial.tex @@ -60,6 +60,31 @@ does not make any distinction between expressions and statements, so since there is only a single line of code within the foreach block, we can drop it and simply write: \mrbfnmyreplicatebitsthree +\subsection{External Bindings} + +Rather than defining functions within Sail itself, they can be mapped +onto functions definition within the various backend targets supported +by Sail. This is primarily used to setup the primitive functions +defined in the Sail library. These declarations work like much FFI +bindings in many programming languages---in Sail we provide the +\ll{val} declaration, except rather than giving a function body we +supply a string used to identify the external operator in each +backend. For example, we could link the \ll{>>} operator with the +\verb|shiftl| primitive as \mrbzeightoperatorzzerozIzIznine If the +external function has the same name as the sail function, such as +\ll{shiftl = "shiftl"}, then we can use the shorthand syntax +\mrbshiftl + +We can map onto differently-named operations for different targets by +using a JSON-like \ll{key: "value"} notation, for example: +\mrbzeightoperatorzzerozKzKznine We can also omit backends---in which +case those targets will expect a definition written in Sail. Note that +no checking is done to ensure that the definition in the target +matches the type of the Sail function. Finally, the \ll{_} key used +above is a wildcard that will be used for any backend not otherwise +included. If we use the wildcard key, then we cannot omit specific +backends to force them to use a definition in Sail. + \subsection{Numeric Types} \label{sec:numeric} @@ -95,7 +120,9 @@ 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. +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} @@ -236,6 +263,12 @@ 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 saying that they are equivalent to +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} @@ -307,6 +340,17 @@ 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 @@ -443,10 +487,10 @@ assignment operator within a block. } \end{lstlisting} The assignment operator is the equality symbol, as in C and other -programming languages. Sail supports a rich language of -\emph{l-expression} 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 +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; @@ -473,23 +517,130 @@ the variable \ll{x}, so 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{l-expressions} +\subsubsection{Assignment and l-values} \label{sec:lexp} -Sail allows for setter functions to be declared in a very simple way: -\ll{f(x) = y} is sugar for \ll{f(x, y)}. This feature is commonly used -when setting +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[4 .. 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 +implictly 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} -\fbox{TODO} \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 +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 @@ -658,6 +809,7 @@ 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 @@ -736,14 +888,14 @@ so we can use this to define functions with optional arguments, e.g. \ll{sizeof}, see Section~\ref{sec:sizeof}) or we can provide it ourselves as an explicit argument. -\subsection{Getters and Setters} -\label{sec:getset} +%% \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. +%% 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} +%% \fbox{TODO} \subsection{Sizeof and Constraint} \label{sec:sizeof} @@ -793,8 +945,73 @@ 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 suprisingly 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-pseudocode's have varying naming conventions and @@ -834,4 +1051,7 @@ operations. These are listed below: 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} diff --git a/doc/types.tex b/doc/types.tex index 11037c91..a74cdea9 100644 --- a/doc/types.tex +++ b/doc/types.tex @@ -1,6 +1,8 @@ \section{Type System} \label{sec:types} +(This section is still a work in progress) + \newcommand{\tcheck}[3]{#1 \vdash #2 \Leftarrow #3} \newcommand{\tinfer}[3]{#1 \vdash #2 \Rightarrow #3} \newcommand{\msail}[1]{\text{\lstinline[mathescape]+#1+}} diff --git a/doc/usage.tex b/doc/usage.tex index 12095822..3b8eed5f 100644 --- a/doc/usage.tex +++ b/doc/usage.tex @@ -21,7 +21,7 @@ definitions used in the rest of the specification and then specification. For more complex projects, once can use \ll{$include} statments in -Sail source, for example: \TODO{use \# like C} +Sail source, for example: \begin{lstlisting} $include <library.sail> $include "file.sail" @@ -38,7 +38,7 @@ AST is parsed~\footnote{This can affect precedence declarations for custom user \subsection{OCaml compilation} -To compile a sail specification into OCaml, one calls Sail as +To compile a Sail specification into OCaml, one calls Sail as \begin{verbatim} sail -ocaml FILES \end{verbatim} @@ -76,25 +76,46 @@ specification. In particular \verb+elf.sail+ defines a function 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 instruments the -generated OCaml code with tracing information this option implies \verb+-ocaml+. +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} +%% \subsection{C compilation} -WIP but basically like OCaml +%% WIP but basically like OCaml -\subsection{Lem embedding} +\subsection{Lem and Isabelle} -\TODO{Document generating lem} +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} +\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 -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 -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 +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 +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 @@ -127,6 +148,9 @@ indicated by starting with the letter d. 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. |