diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile | 11 | ||||
| -rw-r--r-- | doc/internals.md | 8 | ||||
| -rw-r--r-- | doc/manual.tex | 3 | ||||
| -rw-r--r-- | doc/pandocfix.sed | 2 | ||||
| -rw-r--r-- | doc/riscv.tex | 97 | ||||
| -rw-r--r-- | doc/tutorial.tex | 2 | ||||
| -rw-r--r-- | doc/usage.tex | 2 |
7 files changed, 58 insertions, 67 deletions
diff --git a/doc/Makefile b/doc/Makefile index 7afebdf2..315eaaaa 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -58,8 +58,8 @@ all: manual.pdf .PHONY: clean -code_riscv.tex: ${SAIL_RISCV}/model/prelude.sail ${SAIL_RISCV}/model/riscv_duopod.sail - sail -o code_riscv -latex -latex_full_valspecs ${SAIL_RISCV}/model/prelude.sail ${SAIL_RISCV}/model/riscv_duopod.sail +code_riscv.tex: ${SAIL_RISCV}/model/riscv_duopod.sail + sail -o code_riscv -latex -latex_full_valspecs $^ cp code_riscv/commands.tex code_riscv.tex code_myreplicatebits.tex: examples/my_replicate_bits.sail @@ -69,8 +69,12 @@ code_myreplicatebits.tex: examples/my_replicate_bits.sail grammar.tex: ../language/sail.ott ott -pp_grammar -tex_wrap false -tex_suppress_category I -tex_suppress_category D -tex_suppress_ntr terminals -tex_suppress_ntr formula -tex_suppress_ntr judgement -tex_suppress_ntr user_syntax -tex_suppress_ntr dec_comm -sort false -generate_aux_rules false -picky_multiple_parses true -i ../language/sail.ott -o grammar.tex +internals.tex: internals.md + pandoc $< -f markdown -t latex --listings -o $@ + sed -i.bak -f pandocfix.sed $@ + LATEXARG=manual.tex -manual.pdf: grammar.tex introduction.tex usage.tex types.tex code_riscv.tex riscv.tex manual.tex manual.bib tutorial.tex code_myreplicatebits.tex +manual.pdf: grammar.tex introduction.tex usage.tex types.tex code_riscv.tex riscv.tex manual.tex manual.bib tutorial.tex internals.tex code_myreplicatebits.tex pdflatex ${LATEXARG} bibtex manual pdflatex ${LATEXARG} @@ -83,6 +87,7 @@ clean: -rm manual.pdf -rm -rf code_riscv/ -rm -f code_riscv.tex + -rm -f internals.tex -rm -rf code_myreplicatebits/ -rm -f code_myreplicatebits.tex -rm -f *.aux diff --git a/doc/internals.md b/doc/internals.md index 6ba60fa6..6422f227 100644 --- a/doc/internals.md +++ b/doc/internals.md @@ -10,7 +10,7 @@ by [Lem](https://github.com/rems-project/lem), which allows the Sail OCaml source to seamlessly interoperate with parts written in Lem. Although we do not make much use of this, in principle it allows us to implement parts of Sail in Lem, which would enable them to be -verified in Isabelle or HOL. +verified in Isabelle or HOL4. The Sail AST looks something like: @@ -35,13 +35,13 @@ which attaches an annotation to each node in the AST, consisting of an arbitrary type that parameterises the AST, and a location identifying the position of the AST node in the source code: -``` +```OCaml type 'a annot = l * 'a ``` There are various types of locations: -``` +```OCaml type l = | Unknown | Unique of int * l @@ -184,7 +184,7 @@ which invokes the backend for each target, e.g. for OCaml: ``` There is also a `Sail.prover_regstate` function that allows the -register state to be Set up in a prover-agnostic way for each of the +register state to be set up in a prover-agnostic way for each of the theorem-prover targets. ## Type Checker diff --git a/doc/manual.tex b/doc/manual.tex index 38b14322..f3578784 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -105,6 +105,9 @@ \include{tutorial} +\lstset{language={},escapechar=\`} +\include{internals} + % Remove for now since incomplete %\include{types} diff --git a/doc/pandocfix.sed b/doc/pandocfix.sed new file mode 100644 index 00000000..1b6f2688 --- /dev/null +++ b/doc/pandocfix.sed @@ -0,0 +1,2 @@ +s/https:\/\/github.com\/rems-project\/sail\/blob\/sail2\/doc\/// +s/\\includegraphics/\\includegraphics[scale=0.35]/
\ No newline at end of file diff --git a/doc/riscv.tex b/doc/riscv.tex index ee0c07e1..ca2b9dfe 100644 --- a/doc/riscv.tex +++ b/doc/riscv.tex @@ -3,38 +3,35 @@ We introduce the basic features of Sail via a small example from our \riscv\ model that includes just two instructions: add immediate and -load double. - -We start with some basic type synonyms. We create a type \ll{xlen_t} -for bitvectors of length 64, then we define a type \ll{regno}, which -is a type synonym for the builtin type \ll{atom}. The type -\ll{atom('n)} is a number which is exactly equal to the type variable -\ll{atom('n)}. Type variables are syntactically marked with single -quotes, as in ML. A \emph{constraint} can be attached to this type -synonym---ensuring that it is only used where we can guarantee that -its value will be between 0 and 31. Sail supports a rich variety of -numeric types, including range types, which are statically checked. We -then define a synonym \ll{regbits} for \ll{bits(5)}. We don't want to -manually convert between \ll{regbits} and \ll{regno} all the time, so -we define a function that maps between them and declare it as a -\emph{cast}, which allows the type-checker to insert it where -needed. By default, we do not do any automatic casting (except between -basic numeric types when safe), but to allow idioms in ISA vendor -description documents we support flexible user defined casts. To ensure -that the constraint on the \ll{regno} type synonym is satisfied, we -return an existentially quantified type \ll{\{'n, 0 <= 'n < - 32. regno('n)\}}. - -\sailtype{xlen_t} -\sailtype{regno} +load double. We start by including two files from the main sail-riscv +development: + +\begin{lstlisting} +$include "prelude.sail" +$include "riscv_xlen64.sail" +\end{lstlisting} + +The prelude sets up basic definitions we will use, it can vary on a +per-architecture basis to account for stylistic differences in ISA +specifications. \texttt{riscv\_xlen64.sail} introduces some type +synonyms. It creates a integer type xlen, which is 64. Sail supports +definitions which are generic over both regular types, and integers +(think const generics in C++, but more expressive). We also create a +type \ll{xlenbits} for bitvectors of length \ll{xlen}. + +\sailtype{xlen} +\sailtype{xlen_bytes} +\sailtype{xlenbits} + +For the purpose of this example, we also introduce a type synonym for +bitvectors of length 5, which represent registers. + \sailtype{regbits} -\sailval{regbits_to_regno} -\sailfn{regbits_to_regno} We now set up some basic architectural state. First creating a -register of type \ll{xlen_t} for both the program counter \ll{PC}, and +register of type \ll{xlenbits} for both the program counter \ll{PC}, and the next program counter, \ll{nextPC}. We define the general purpose -registers as a vector of 32 \ll{xlen_t} bitvectors. The \ll{dec} +registers as a vector of 32 \ll{xlenbits} bitvectors. The \ll{dec} keyword isn't important in this example, but Sail supports two different numbering schemes for (bit)vectors \ll{inc}, for most significant bit is zero, and \ll{dec} for least significant bit is @@ -48,20 +45,18 @@ overloading, and has an expressive l-value language in assignments, with the aim of allowing pseudo-code like definitions. \begin{lstlisting} -register PC : xlen_t -register nextPC : xlen_t +register PC : xlenbits +register nextPC : xlenbits -register Xs : vector(32, dec, xlen_t) +register Xs : vector(32, dec, xlenbits) \end{lstlisting} \sailval{rX} -% TODO: Fix funcl commands -\sailfclrX -\sailfclMMMrX +\sailfn{rX} \sailval{wX} \sailfn{wX} -\sailoverloadIIX +\sailoverloadUUX We also give a function \ll{MEMr} for reading memory, this function just points at a builtin we have defined elsewhere. Note that @@ -83,8 +78,7 @@ desirable to group the relevant parts of these functions and datatypes together in one place, as they would usually be found in an architecture reference manual. To support this Sail supports \emph{scattered} definitions. First we give types for the execute and -decode functions, and declare them as scattered functions, as well as -the \ll{ast} union. +decode functions, as well as the \ll{ast} union. \sailtype{iop} @@ -92,10 +86,8 @@ the \ll{ast} union. scattered union ast val decode : bits(32) -> option(ast) effect pure -scattered function decode val execute : ast -> unit effect {rmem, rreg, wreg} -scattered function execute \end{lstlisting} Now we provide the clauses for the add-immediate \ll{ast} type, as @@ -111,8 +103,8 @@ its argument. union clause ast = ITYPE : (bits(12), regbits, regbits, iop) \end{lstlisting} -%\sailfndecodeSomeITYPE -%\sailfnexecuteITYPE +\sailfclITYPEdecode +\sailfclITYPEexecute \noindent Now we do the same thing for the load-double instruction: @@ -120,22 +112,11 @@ union clause ast = ITYPE : (bits(12), regbits, regbits, iop) union clause ast = LOAD : (bits(12), regbits, regbits) \end{lstlisting} -%\sailfndecodeSomeLOAD -%\sailfnexecuteLOAD - -Finally we define the fallthrough case for the decode function, and -end all our scattered definitions. Note that the clauses in a -scattered function will be matched in the order they appear in the -file. - -%\sailfndecodeNone - -\begin{lstlisting} -end ast -end decode -end execute -\end{lstlisting} +\sailfclLOADdecode +\sailfclLOADexecute -The actual code for this example, as well as our more complete -\riscv\ specification can be found on our github at +Finally we define the fallthrough case for the decode function. Note +that the clauses in a scattered function will be matched in the order +they appear in the file. The actual code for this example, as well as +our more complete \riscv\ specification can be found on our github at \anonymise{\url{https://github.com/rems-project/sail-riscv/blob/master/model/riscv_duopod.sail}}. diff --git a/doc/tutorial.tex b/doc/tutorial.tex index b9901fc9..c60edf69 100644 --- a/doc/tutorial.tex +++ b/doc/tutorial.tex @@ -58,7 +58,7 @@ check. This is another feature that must be used carefully, because too many implicit casts can quickly result in unreadable code. Sail 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: \mrbfn{my_replicate_bits_three} +can drop it and simply write: \mrbfn{my_replicate_bits_3} %\subsection{External Bindings} diff --git a/doc/usage.tex b/doc/usage.tex index a7532ddf..68ca76d6 100644 --- a/doc/usage.tex +++ b/doc/usage.tex @@ -87,7 +87,7 @@ 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 by default printed to stdout, but one can also use +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 |