diff --git a/THIRD_PARTY_FILES.md b/THIRD_PARTY_FILES.md index 136cf353a..87765e8c6 100644 --- a/THIRD_PARTY_FILES.md +++ b/THIRD_PARTY_FILES.md @@ -7,6 +7,13 @@ CIL https://github.com/cil-project/cil | BSD 3-Clause | src/lib/visitor.ml | ASLi/CIL | | BSD 3-Clause | src/lib/jib_visitor.ml | ASLi | +The following file is from Asciidoctor +https://github.com/asciidoctor/asciidoctor + +| License | Files | Source | +| ------------ | ----------------------- | ----------- | +| MIT | doc/asciidoc/manual.css | Asciidoctor | + CIL === @@ -78,3 +85,31 @@ CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ``` + +Asciidoctor +=========== + +``` +MIT License + +Copyright (C) 2012-present Dan Allen, Sarah White, Ryan Waldron, and the +individual contributors to Asciidoctor. + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. +``` diff --git a/doc/asciidoc/Makefile b/doc/asciidoc/Makefile index 90fd4b09c..e8b7c2c25 100644 --- a/doc/asciidoc/Makefile +++ b/doc/asciidoc/Makefile @@ -3,33 +3,73 @@ SAIL_PLUGIN ?= asciidoctor-sail SAIL_DOCS = sail_doc/riscv_duopod.json SAIL_DOCS += sail_doc/pattern_matching.json SAIL_DOCS += sail_doc/my_replicate_bits.json +SAIL_DOCS += sail_doc/bitfield.json SAIL_DOCS += sail_doc/exn.json +SAIL_DOCS += sail_doc/mapping.json +SAIL_DOCS += sail_doc/scattered.json +SAIL_DOCS += sail_doc/tuples.json +SAIL_DOCS += sail_doc/string.json +SAIL_DOCS += module_sail_doc/simple_mod.json +SAIL_DOCS += module_sail_doc/simple_mod_err.error +SAIL_DOCS += module_sail_doc/cond.rigging +SAIL_DOCS += custom_sail_doc/cannot_wildcard.json +SAIL_DOCS += lib_sail_doc/concurrency_interface/read_write.json -CUSTOM_SAIL_DOCS = custom_sail_doc/cannot_wildcard.json +TIKZ_FIGURES = ordering-tikz.png -LIB_SAIL_DOCS = lib_sail_doc/concurrency_interface/read_write.json +EXTRAS = ../examples/simple_mod.rigging default: manual.pdf sail_doc/%.json: ../examples/%.sail mkdir -p sail_doc - sail -doc $< -doc_file $< -doc_embed plain -doc_bundle $(notdir $@) + sail -doc -doc_file $< -doc_embed plain -doc_bundle $(notdir $@) $< lib_sail_doc/%.json: ../../lib/%.sail mkdir -p lib_sail_doc mkdir -p lib_sail_doc/concurrency_interface - sail -doc $< -doc_file $< -doc_embed plain -doc_bundle $(patsubst lib_sail_doc/%,%,$@) -o lib_sail_doc + sail -doc -doc_file $< -doc_embed plain -doc_bundle $(patsubst lib_sail_doc/%,%,$@) -o lib_sail_doc $< + +.SECONDEXPANSION: + +module_sail_doc/%.json: ../examples/%.rigging $$(shell sail ../examples/%.rigging -list_files) + mkdir -p module_sail_doc + sail -doc $(addprefix -doc_file ,$(shell sail $< -list_files)) -doc_embed plain -doc_bundle $(notdir $@) -o module_sail_doc $< + +module_sail_doc/%.error: ../examples/%.rigging $$(shell sail ../examples/%.rigging -list_files) + mkdir -p module_sail_doc + -sail -no_color $< 2> $@ + +module_sail_doc/%.rigging: ../examples/%.rigging + mkdir -p module_sail_doc + sail $< -list_files + cp $< $@ custom_sail_doc/cannot_wildcard.json: ../examples/cannot_wildcard.sail mkdir -p custom_sail_doc - sail -no_color -doc $< -doc_file $< -doc_embed plain -doc_bundle $(notdir $@) -o custom_sail_doc 2> custom_sail_doc/cannot_wildcard_warning + sail -no_color -doc -doc_file $< -doc_embed plain -doc_bundle $(notdir $@) -o custom_sail_doc 2> custom_sail_doc/cannot_wildcard_warning $< + +ordering-tikz.pdf: latex/ordering.tex + pdflatex --jobname=ordering-tikz $< + +%.png: %.pdf + pdftoppm -r 300 -png $< > $@ + +parser.txt: ../../src/lib/parser.mly parser.sed + obelisk -i $< | tr '\n' '+' | sed 's/+[ ][ ]*\([^| ]\)/ \1/g' | tr '+' '\n' > $@ + sed -i.bak -f parser.sed $@ -manual.pdf: *.adoc $(SAIL_DOCS) $(LIB_SAIL_DOCS) $(CUSTOM_SAIL_DOCS) +manual.pdf: *.adoc $(SAIL_DOCS) $(EXTRAS) $(TIKZ_FIGURES) parser.txt asciidoctor-pdf manual.adoc -r $(SAIL_PLUGIN) -r asciidoctor-bibtex -manual.html: *.adoc $(SAIL_DOCS) $(LIB_SAIL_DOCS) $(CUSTOM_SAIL_DOCS) +manual.html: *.adoc $(SAIL_DOCS) $(EXTRAS) $(TIKZ_FIGURES) parser.txt manual.css asciidoctor manual.adoc -r $(SAIL_PLUGIN) -r asciidoctor-bibtex +.PHONY: clean clean: - -rm manual.pdf + -rm *.pdf + -rm *.png + -rm *.log + -rm *.aux + -rm parser.txt -rm manual.html diff --git a/doc/asciidoc/docinfo.html b/doc/asciidoc/docinfo.html new file mode 100644 index 000000000..959aa39f9 --- /dev/null +++ b/doc/asciidoc/docinfo.html @@ -0,0 +1,23 @@ + + + diff --git a/doc/asciidoc/grammar.adoc b/doc/asciidoc/grammar.adoc new file mode 100644 index 000000000..038d37df3 --- /dev/null +++ b/doc/asciidoc/grammar.adoc @@ -0,0 +1,41 @@ +This appendix contains a grammar for the Sail language that is +automatically generated from the +https://gallium.inria.fr/~fpottier/menhir[Menhir] parser definition. + +NOTE: This means that the grammar is stated in such a way that the +parser generator can see it is free of LR shift/reduce and +reduce/reduce conflicts, rather than being optimised for human +readability. + +First, we need some lexical conventions: + +* `ID` is any valid Sail identifier + +* `OPERATOR` is any valid Sail operator, as defined in <>. + +* `TYPE_VARIABLE` is a valid Sail identifier with a leading single quote `'`. + +* `NUMBER` is a non-empty sequence of decimal digits `[0-9]+`. + +* `HEXADECIMAL_LITERAL` is `0x[A-Ba-f0-9_]+` + +* `BINARY_LITERAL` is `0b[0-1_]+` + +* `STRING_LITERAL` is a Sail string literal. + +`$[ATTRIBUTE]` and `$LINE_DIRECTIVE` represent attributes and single +line directives. Examples of line directives would be things like +`$include`, `$ifdef` and so on. These start with a leading `$`, are +followed by the directive name (which follows the same lexical rules +as a Sail identifier), is followed by one or more spaces, then +proceeds to the end of the line, with everything between the +identifier and the line ending being the line directive's argument +(with leading and trailing whitespace removed). An attribute starts +with `$[` and ends with `]`, and in between consists of an attribute +name, followed by at least one whitespace character, then any +arbitrary sequence of characters that does not contain `]`. + +[source,sail] +---- +include::parser.txt[] +---- diff --git a/doc/asciidoc/language.adoc b/doc/asciidoc/language.adoc index 91b9378d7..b6b5cfac2 100644 --- a/doc/asciidoc/language.adoc +++ b/doc/asciidoc/language.adoc @@ -17,9 +17,10 @@ variables_. Type variables are written with a leading 'tick', so `'n` and `'m` are the type variables in the above signature. NOTE: The leading tick is a convention derived from Standard ML, and -other functional languages derived from Standard ML, such as -OCaml. Readers who are familiar with Rust will also recognise this -naming convention from lifetime variables in Rust types. +other functional languages derived from Standard ML, such as OCaml. +Readers who are familiar with Rust will also recognise this naming +convention from lifetime variables in Rust types. The `val` keyword to +declare functions is also taken from OCaml. The type `bits('m)` is a bitvector of length `'m`, and `int('n)` is an integer with the value `'n`. The result of this function will @@ -50,11 +51,29 @@ include::sail:extz[from=mrb] ---- Implicit parameters are always integers, and they must appear first -before any other parameters in the function type signature. The first argument can then just be omitted when calling the function, like so: +before any other parameters in the function type signature. The first +argument can then just be omitted when calling the function, like so: sail::extz_usage[from=mrb,part=body,dedent] -=== Numeric types +=== The unit type + +The simplest type in Sail is the _unit type_ `unit`. It is a type with +a single member `()`. Rather than have functions that takes zero +arguments, we have functions that take a single `unit` argument. +Similarly, rather than having functions that return no results, a +function with no meaningful return value can return `()`. The `()` +notation reflects the fact that the unit type can be thought of as an +empty tuple (see <>). + +In Sail `unit` plays a similar role to void in C and C++, except +unlike void it is an ordinary type and can appear anywhere and be used +in generic functions. + +The https://en.wikipedia.org/wiki/Unit_type[wikipedia page for the unit type], +goes into further details on the difference between unit and void. + +=== Numeric types and bits Sail has three basic numeric types, `int`, `nat`, and `range`. The type `int` which we have already seen above is an arbitrary precision @@ -81,18 +100,219 @@ which would end up being equivalent to bits to other numeric types would be highly undesirable. The `bit` type itself is a two-element type with members `bitzero` and `bitone`. +In addition, we can write a numeric type that only contains a fixed +set of integers. The type `{32,{nbsp}64}` is a type that can only +contain the values `32` and `64`. + +NOTE: In older Sail versions the numeric set type would have been +denoted `{|32, 64|}`. + === Bitvector Literals Bitvector literals in Sail are written as either `0x` followed by a sequence of hexadecimal digits or `0b` followed by a sequence of -binary digits, for example `0x12FE or `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 `0x12FE` has +binary digits, for example `0x12FE` or `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 `0x12FE` has length 16, while `0b1010100` has length 7. To ensure bitvector logic -in specifications is precisly specified, we do not do any kind of +in specifications is precisly specified, we do not allow any kind of implicit widening or truncation as might occur in C. To change the length of a bitvector, explicit zero/sign extension and truncation -functions must be used. +functions must be used. Underscores can be used in bitvector literals +to separate groups of bits (typically in groups of 16), for example: + +[source,sail] +---- +let large_bitvector : bits(64) = 0xFFFF_0000_1234_0000 +---- + +We can make bitvectors as large as we need: + +[source,sail] +---- +let even_larger_bitvector : bits(192) = + 0xFFFF_FFFF_FFFF_FFFF_0000_0000_0000_0000_ABCD_ABCD_ABCD_ABCD +---- + +We can also write bitvectors very verbosely using `bitzero` and +`bitone`, like: + +[source,sail] +---- +let v : bits(2) = [bitzero, bitzero] +---- + +The `@` operator is used to concatenate bitvectors, for example: + +[source,sail] +---- +let x = 0xFFFF; +let y = 0x0000; +assert(x @ y == 0xFFFF_0000); +---- + +For historical reasons the `bit` type is not equal to `bits(1)`, and +while this does simplify naively mapping the bits type into a (very +inefficient!) representation like `bit list` in Isabelle or OCaml, it +might be something we reconsider in the future. + +Sail allows two different types of bitvector orderings---increasing +(`inc`) and decreasing (`dec`). These two orderings are shown for the +bitvector 0b10110000 below. + +image::ordering-tikz.png[width=70%,align=center,pdfwidth=80%] + +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 + +[source,sail] +---- +default Order dec +---- + +and this should usually be done right at the beginning of a +specification. This setting is global, and increasing and decreasing +bitvectors can therefore never be mixed within the same specification! + +In practice decreasing order is the almost universal standard and only +POWER uses increasing order. All currently maintained Sail +specifications use decreasing. You may run into issues with increasing +bitvectors as the code to support these is effectively never exercised +as a result. + +=== Vectors + +Sail has the built-in type `vector`, which is a polymorphic type for +fixed-length vectors. For example, we could define a vector `v` of +three integers as follows: + +[source,sail] +---- +let v : vector(3, int) = [3, 2, 1] +---- + +The first argument of the vector type is a numeric expression +representing the length of the vector, and the second is the type of +the vector's elements. As mentioned in the bitvector section, the +ordering of bitvectors and vectors is always the same, so: + +[source,sail] +---- +let a_generic_vector : vector(3, bit) = [bitzero, bitzero, bitone] +let a_bit_vector : bits(3) = [bitzero, bitzero, bitone] // 0b001 + +assert(a_generic_vector[0] == bitone) +assert(a_bitvector_vector[0] == bitone) +---- + +Note that a generic vector of bits and a bitvector are not the same +type, despite us being able to write them using the same syntax. This +means you cannot write a function that is polymorphic over both +generic vectors and bitvectors). This is because we typically want +these types to have very different representations in our various Sail +backends, and we don't want to be forced into a compilation strategy +that requires monomorphising such functions. + +=== Accessing and Updating Vectors + +A (bit)vector can be indexed by using the _vector index_ notation. So, +in the following code: + +[source,sail] +---- +let v : vector(4, int) = [1, 2, 3, 4] +let a = v[0] +let b = v[3] +---- +`a` will be `4`, and `b` will be `1` (we assume `default Order dec` +here). 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. + +A vector `v` can be sliced using the `v[n{nbsp}..{nbsp}m]` 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 `v` as `v[31{nbsp}..{nbsp}0]`, and the upper 32-bits of an +increasing bitvector as `v[0{nbsp}..{nbsp}31]`, i.e. the indexing +order for decreasing vectors decreases, and the indexing order for +increasing vectors increases. + +A vector `v` can have an index index using +`[v{nbsp}with{nbsp}index{nbsp}={nbsp}expression]`. Similarly, a +sub-range of v can be updated using +`[v{nbsp}with{nbsp}n{nbsp}..{nbsp}m{nbsp}={nbsp}expression]` where the +order of the indexes is the same as described above for increasing and +decreasing vectors. + +=== Tuples +:tuples: sail_doc/tuples.json + +Sail has tuple types which represent heterogenous sequences containing +values of different types. A tuple type `(T1,{nbsp}T2,{nbsp}...)` has +values `(x1,{nbsp}x2,{nbsp}...)` where `x1{nbsp}:{nbsp}T1`, +`x2{nbsp}:{nbsp}T2` and so on. A tuple must have 2 or more elements. +Some examples of tuples would be: + +sail::TUPLES[from=tuples,type=span] + +Note that while the function type `(A,{nbsp}B){nbsp}\->{nbsp}C` might +look like a function taking a single tuple argument, it is in fact a +function taking two arguments. If we wanted to write a function taking +a single tuple argument, we would instead write: + +[source,sail] +---- +include::sail:single_tuple_argument[from=tuples,type=val] + +include::sail:single_tuple_argument[from=tuples,type=function] +---- + +which would be called as + +sail::caller[from=tuples,type=function,part=body,dedent] + +NOTE: This is because in Sail the function type is denoted +`(A,{nbsp}B,{nbsp}...){nbsp}\->{nbsp}C`, but we allow the brackets to +be elided when the function has a single non-tuple argument so we can +write `A{nbsp}\->{nbsp}B` rather than `(A){nbsp}\->{nbsp}B`. + +=== Strings +:strings: sail_doc/string.json + +Sail has a `string` type, which is primarily used for error reporting +and debugging. + +CAUTION: Sail is not a language designed for working with strings, and +the semantics of ISA specifications should not depend on any logic +involving strings. If you find yourself using strings for reasons +other than printing or logging errors in a Sail specification, you +should probably reconsider. + +A Sail string is any sequence of ASCII characters between double +quotes. Backslash is used to introduce escape sequences, and the +following escape sequences are supported: + +* `\\` -- Backslash +* `\n` -- Newline character +* `\t` -- Tab character +* `\b` -- Backspace character +* `\r` -- Carriage return +* `\'` -- Single quote (somewhat unnecessary, as single quotes are allowed in Sail strings) +* `\"` -- Double quote +* `\DDD` -- The character with decimal ASCII code `DDD` +* `\xHH` -- The character with hexadecimal ASCII code `HH` + +Multi-line strings can be written by escaping the newline character at the end of a line: + +sail::multi_line[from=strings,type=function,part=body,dedent] === Pattern Matching :pattern-match: sail_doc/pattern_matching.json @@ -165,7 +385,7 @@ We now describe all the things that can be matched on in Sail ==== Matching on literals First, and as we have already seen, we can match on literal -values. These literal values can be bitvectors, the boolean values +values. These literal values can be `()`, bitvectors, the boolean values `true` and `false`, numbers, and strings. ==== Matching on enumerations @@ -190,7 +410,7 @@ sail::match_tuple[from=pattern-match,part=body,dedent] ==== Matching on unions Match can also be used to destructure tagged union constructors, for example -using the option type from Section~\ref{sec:union}: +using the option type from the Sail library. [source,sail] ---- include::sail:OPTION[from=pattern-match,type=span] @@ -245,11 +465,11 @@ operator in a pattern, so in this example the pattern brackets as ==== Automatic wildcard insertion -The various theorem provers Sail can produce definitions for are -strict, and _require_ patterns to be exhaustive. However, their -pattern exhaustiveness checkers do not understand bitvectors in the -same way Sail does. For example, Sail can tell that the following -match is complete: +The various theorem provers that Sail can produce definitions for are +often strict, and enforce that pattern matches are exhaustive. +However, their pattern exhaustiveness checkers do not understand +bitvectors in the same way Sail does. For example, Sail can tell that +the following match is complete: sail::match_wildcard_remove[from=pattern-match,part=body,dedent] @@ -270,6 +490,517 @@ This warning should be heeded, and the match simplified otherwise the generated theorem prover definitions produced by Sail may be rejected by the prover. +=== Type patterns + +In the previous section we saw as patterns, which allowed us bind +additional variables for subpatterns. However, as patterns can also be +used to bind type variables. For example: + +[source,sail] +---- +// Some function that returns either 32 or 64 at runtime +val get_current_xlen : unit -> {32, 64} + +register R : bits(32) + +val example : int -> unit + +function example() = { + let xlen as int('n) = get_current_xlen() + + // Create a bitvector of length xlen + let bv : bits('n) = zero_extend(xlen, *R); + + print_bits("bv = ", bv) +} +---- + +You can think of the `as int('n)` as matching on the return type of +the `get_current_xlen` rather than the value, and binding it's length +to a new type variable `'n`, which we can subsequently use in types +later in our function. Note that even though we only know if xlen will +be 32 or 64 at runtime after the call to get_current_xlen, Sail is +still able to statically check all our bitvector accesses. + +If a type only contains a single type variable (as `int('n)` does), +then we allow omitting the type name and just using a variable as the +type pattern, for example the following would be equivalent to the +first line of example above: + +[source,sail] +---- +let xlen as 'n = get_current_xlen(); +---- + +If we want to give the variable `xlen` and the type variable `'n` the +same name, we could go further and simplify to: + +[source,sail] +---- +function example() = { + let 'xlen = get_current_xlen() + + // Create a bitvector of length xlen + let bv : bits('xlen) = zero_extend(xlen, *R); + + print_bits("bv = ", bv) +} +---- + +Here we can use xlen within the function as both a regular variable +`xlen` and as a type variable `'xlen`. + +=== Mutable variables + +Bindings made using let are always immutable, but Sail also allows mutable +variables. Mutable variables are bound implicitly by using the +var keyword within a block. + +[source,sail] +---- +{ + var x : int = 3; // Create a new mutable variable x initialised to 3 + x = 2 // Rebind it to the value 2 +} +---- + +Like let-bound variables, mutable variables are lexically scoped, so +they only exist within the block that declared them. + +Technically, unless the `-strict_var` option is used Sail also allows +mutable variables to be implicitly declared, like so: + +[source,sail] +---- +{ + x : int = 3 // Create a new mutable variable x initialised to 3 + x = 2 // Rebind it to the value 2 +} +---- + +This functions identically, just without the keyword. We consider this +deprecated and strongly encourage the use of the `var` keyword going +forwards. + +The assignment operator is the equality symbol, as in C and other +programming languages. Sail supports a rich language of _l-value_ +forms, which can appear on the left of an assignment. These will be +described in the next section. + +One important thing to note is that Sail always infers the most +specific type it can for variables, and in the presence of integer +types with constraints, these types can be _very_ specific. This is +not a problem for immutable bindings, but can cause issues for mutable +variables when explicit types are omitted. The following will not +typecheck: + +[source,sail] +---- +{ + var x = 3; + x = 2; +} +---- + +The reason is that Sail (correctly) infers that `x` has the type 'the +integer equal to 3', and therefore refuses to allow us to assign `2` +to it (as it well should), because two is not equal to three. To avoid +this we must give an annotation with a less specific type like `int`. + +=== Assignment and l-values + +It is common in ISA specifications to assign to complex l-values, +e.g.{nbsp}to a subvector or named field of a bitvector register, or to +an l-value computed with some auxiliary function, e.g.{nbsp}to select +the appropriate register for the current execution model. + +Sail has l-values that allow writing to individual elements of a +(bit)vector: + +[source,sail] +---- +var v : bits(8) = 0xFF; +v[0] = bitzero; +assert(v == 0xFE) +---- + +As well as sub-ranges of a (bit)vector: + +[source,sail] +---- +var v : bits(8) = 0xFF; +v[3 .. 0] = 0x0; // assume default Order dec +assert(v == 0xF0) +---- + +We also have vector concatenation l-values, which work much like +vector concatenation patterns + +[source,sail] +---- +var v1 : bits(4) = 0xF; +var v2 : bits(4) = 0xF; +v1 @ v2 = 0xAB; +assert(v1 == 0xA & v2 == 0xB) +---- + +For structs we can write to an individual struct field as + +[source,sail] +---- +// Assume S is a struct type with a single bits(8) field (called field) +var s : S = struct { field = 0xFF }; +s.field = 0x00; +assert(s.field == 0x00) +---- + +We can also do multiple assignment using tuples, for example: + +[source,sail] +---- +var (x, y) = (2, 3); +assert(x == 2 & x == 3) +// swap values +(y, x) = (x, y) +assert(x == 3 & x == 2) +---- + +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: + +[source,sail] +---- +memory(addr) = 0x0F +// is just syntactic sugar for +memory(addr, 0x0F) +---- + +This feature is commonly used when setting registers or memory that +have some additional semantics when they are read or written. We +commonly use the ad-hoc overloading feature to declare what appear to +be getter/setter pairs, so for the above example we could implement a +`read_memory` function and a `write_memory` function and overload them +both as `memory` to allow us to write memory using +`memory(addr){nbsp}={nbsp}data` and read memory as +`data{nbsp}={nbsp}memory(addr)`, for example: + +[source,sail] +---- +val read_memory : bits(64) -> bits(8) +val write_memory : (bits(64), bits(8)) -> unit + +overload memory = {read_memory, write_memory} +---- + +=== Bitfields +:bitf: sail_doc/bitfield.json + +The following example creates a bitfield type called `cr_type` and a +register `CR` of that type. The underlying bitvector type (in this +case `bits(8)`) must be specified as part of the bitfield declaration. + +NOTE: The underlying bitvector type can be specified using a type +synonym, like `xlenbits` in sail-riscv. + +[source,sail] +---- +include::sail:BITFIELD[from=bitf,type=span] +---- + +If the bitvector is decreasing then indexes for the fields must also +be in decreasing order, and vice-versa for an increasing vector. The +field definitions can be overlapping and do not need to be contiguous. + +A bitfield generates a type that is simply a struct wrapper around the +underlying bitvector, with a single field called `bits` containing +that bitvector. For the above example, this will be: + +[source,sail] +---- +struct cr_type = { + bits : bits(8) +} +---- + +This representation is guaranteed, so it is expected that Sail code +will use the `bits` field to access the underlying bits of the +bitfield as needed. The following function shows how the bits +contained in a bitfield can be accessed: + +sail::bitfield_access_example[from=bitf,type=function] + +Similarly, bitfields can be updated much like regular vectors just +using the field names rather than numeric indices: + +sail::bitfield_update_example[from=bitf,type=function] + +Older versions of Sail did not guarantee the underlying representation +of the bitfield (because it tried to do clever things to optimise +them). This meant that bitfields had to be accessed using getter and +setter functions, like so: + +sail::legacy_bitfields[from=bitf,type=function] + +The method like accessor syntax was (overly sweet) syntactic sugar for +getter and setter functions following a specific naming convention +that was generated by the bitfield. These functions are still +generated for backwards compatibility, but we would advise against +using them. + +NOTE: Except perhaps for the `Mk_cr_type` function or equivalent for +other bitfields, which is still quite useful for creating bitfields. + +=== Operators + +Valid operators in Sail are sequences of the following non +alpha-numeric characters: `!%&*+-./:<>=@^|#`. Additionally, any such +sequence may be suffixed by an underscore followed by any valid +identifier, so `\<=_u` or even `\<=_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: + +[source,sail] +---- +infix 4 <=_u +---- + +For left or right associative operators, we'd use the keywords +`infixl` or `infixr` respectively. An operator can be used anywhere a +normal identifier could be used via the `operator` keyword. As such, +the `\<=_u` operator can be defined as: + +[source,sail] +---- +val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool +function operator <=_u(x, y) = unsigned(x) <= unsigned(y) +---- + +==== 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 the following table. + +.Default Sail operator precedences +[cols="1,2m,2m,2m",width=80%] +|=== +| Precedence | Left associative | Non-associative | Right associative + +| 9 | | | +| 8 | | | ^ +| 7 | *, \, % | | +| 6 | +, - | | +| 4 | | <, <=, >, >=, !=, =, == | +| 3 | | | & +| 2 | | | \| +| 1 | | | +| 0 | | | +|=== + +=== Ad-hoc Overloading + +Sail has a flexible overloading mechanism using the overload keyword. For example: + +[source,sail] +---- +overload foo = {bar, baz} +---- + +It 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 (that are +in scope) in order from left to right until it finds one that causes +the resulting expression to type-check correctly. + +Multiple `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 example into its own +line like so: +[source,sail] +---- +overload foo = {bar} +overload foo = {baz} +---- + +Note that if an overload is defined in module `B` using identifiers +provided by another module `A`, then a module `C` that requires only +`B` will not see any of the identifiers from `A`, unless it also +requires `A`. See the section on modules for details. Note that this +means an overload cannot be used to 're-export' defintions provided by +another module. + +As an example for how overloaded functions can be used, consider the +following example, where we define a function `print_int` and a +function `print_string` for printing integers and strings +respectively. We overload `print` as either `print_int` or +`print_string`, so we can print either number such as 4, or strings +like `"Hello, World!"` in the following `main` function definition. + +[source,sail] +---- +include::../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 +`sail -ddump_tc_ast examples/overload.sail`. This will print the +following, which shows how the overloading has been resolved + +[source,sail] +---- +function main () : unit = { + print_string("Hello, World!"); + print_int(4) +} +---- + +This option can sometimes be quite useful for observing how +overloading has been resolved. Since the overloadings are done in the +order they are defined, 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: + +[source,sail] +---- +val div1 : forall 'm 'n, 'n >= 0 & 'm > 0. (int('n), int('m)) -> {'o, 'o >= 0. int('o)} + +val div2 : (int, int) -> option(int) +---- + +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 + +[source,sail] +---- +overload operator / = {div1, div2} +---- + +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. Notice that the return type can be different +between different cases in the overload. + +=== Mappings +:maps: sail_doc/mapping.json + +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 +the encoding-decoding of instructions. + +They are defined similarly to functions, with a `val` keyword to +specify the type and a definition, using a bidirectional arrow `+<->+` +rather than a function arrow `+->+`, and a separate `mapping` +definition. + +[source,sail] +---- +include::sail:size_bits[from=maps,type=val] + +include::sail:M1[from=maps,type=span] +---- + +As a shorthand, you can also specify a mapping and its type +simultaneously: + +sail::M2[from=maps,type=span] + +Mappings are used simply by calling them as if they were functions: +type inference will determine in which direction the mapping is +applied. (This gives rise to the restriction that the types on either +side of a mapping must be different.) + +[source,sail] +---- +include::sail:example[from=maps,part=body,dedent] +---- + +Sometimes, because the subset of Sail allowed in bidirectional mapping +clauses is quite restrictive, it can be useful to specify the forwards +and backwards part of a mapping separately: + +sail::M3[from=maps,type=span] + +=== Sizeof and Constraint + +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. + +[source,sail] +---- +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); + () +} +---- + +Note that the second line is equivalent to + +[source,sail] +---- + let len = sizeof('n) + sizeof('n) +---- + +There is also the `constraint` keyword, which takes a type-level +constraint and allows it to be used as a boolean expression, so we +could write: + +[source,sail] +---- +function f(xs, ys) = { + if constraint('n <= 'm) { + // Do something + } +} +---- + +rather than the equivalent test `length(xs){nbsp}\<={nbsp}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 `sizeof` and +`constraint` sparingly on type variables. + +One common use for sizeof however, is to lower type-level integers +down to the value level, for example: + +[source,sail] +---- +// xlen is a type of kind 'Int' +type xlen : Int = 64 + +val f : int -> unit + +function xlen_example() = { + let v = sizeof(xlen); + f(v) +} +---- + === Exceptions :exn: sail_doc/exn.json @@ -279,7 +1010,9 @@ appear in vendor ISA pseudocode (they are a feature in Arm's ASL language), 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 is fairly natural. +supports exceptions is fairly natural. In practice Sail language-level +exceptions end up being quite a nice tool for implementing processor +exceptions in ISA specifications. For exceptions we have two language features: `throw` statements and `try`--`catch` blocks. The throw keyword takes a value of @@ -293,3 +1026,72 @@ would be in OCaml, for example: ---- include::sail:EXN[from=exn,type=span] ---- + +=== Scattered Definitions +:sdef: sail_doc/scattered.json + +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 +the <> section. +Sail permits this with syntactic sugar for `scattered' definitions. +Functions, mappings, unions, and enums can be scattered. + +One begins a scattered definition by declaring the name and kind +(either function or union) of the scattered definition, e.g. + +sail::DECS[type=span,from=sdef] + +This is then followed by _clauses_ for either, which can be freely +interleaved with other definitions. It is common to define both a +scattered type (either union or enum), with a scattered function that +operates on newly defined clauses of that type, as is shown below: + +sail::CLAUSES[type=span,from=sdef] + +Finally the scattered definitions are ended with the `end` keyword, like so: + +sail::ENDS[type=span,from=sdef] + +Technically the `end` keyword is not required, but it is good practice +to include it as it informs Sail that the clauses are now complete, +which forbids new clauses and means subsequent pattern completeness +checks no longer have to require extra wildcards to account for new +clauses being added. + +Semantically, scattered definitions for types appear at the start of +their definition (note however, that this does not mean that a module +that requires just the start `scattered union` definition can access +any constructors of a union defined in modules it does not require). +Scattered definitions for functions and mappings appear at the +end. A scattered function definition can be recursive, but mutually +recursive scattered function definitions should be avoided. + +=== Preludes and Default Environment + +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: + +[source,sail] +---- +val EXTZ = "zero_extend" : ... +---- + +while for ARM, to mimic ASL, one would have + +[source,sail] +---- +val ZeroExtend = "zero_extend" : ... +---- + +where each backend knows about the `"zero_extend"` external name, but +the actual Sail functions are named appropriately for each vendor's +pseudocode. As such each ISA spec written in Sail tends to have its +own prelude. diff --git a/doc/asciidoc/latex/ordering.tex b/doc/asciidoc/latex/ordering.tex new file mode 100644 index 000000000..81fc90e0a --- /dev/null +++ b/doc/asciidoc/latex/ordering.tex @@ -0,0 +1,48 @@ +\documentclass{article} + +\usepackage{graphics} +\usepackage{tikz} +\pgfrealjobname{ordering} +\usetikzlibrary{arrows} + +\begin{document} + +\beginpgfgraphicnamed{ordering-tikz} +\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) {\texttt{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) {\texttt{dec}}; +\end{tikzpicture} +\endpgfgraphicnamed + +\end{document} diff --git a/doc/asciidoc/manual.adoc b/doc/asciidoc/manual.adoc index 6dca997b1..bec99dcb6 100644 --- a/doc/asciidoc/manual.adoc +++ b/doc/asciidoc/manual.adoc @@ -6,7 +6,9 @@ = The Sail instruction-set semantics specification language Alasdair Armstrong; Thomas Bauereiss; Brian Campbell; Shaked Flur; Kathryn E. Gray; Robert Norton-Wright; Christopher Pulte; Peter Sewell :title-logo-image: image:../../etc/logo/sail_logo_square.svg[top=25%,align=center,pdfwidth=2in] -:toc: +:docinfo: shared +:toc: left +:stylesheet: manual.css == Introduction @@ -24,6 +26,14 @@ include::usage.adoc[] include::language.adoc[] +== Modular Sail Specifications + +include::modules.adoc[] + +== The Sail Grammar + +include::grammar.adoc[] + == References bibliography::[] diff --git a/doc/asciidoc/manual.css b/doc/asciidoc/manual.css new file mode 100644 index 000000000..09f8b4044 --- /dev/null +++ b/doc/asciidoc/manual.css @@ -0,0 +1,2421 @@ +/*! Asciidoctor default stylesheet | MIT License | https://asciidoctor.org */ +/* Uncomment the following line when using as a custom stylesheet */ +@import "https://fonts.googleapis.com/css?family=Open+Sans:300,300italic,400,400italic,600,600italic%7CNoto+Serif:400,400italic,700,700italic%7CDroid+Sans+Mono:400,700"; +html { + font-family: sans-serif; + -webkit-text-size-adjust: 100%; +} + +a { + background: none; +} + +a:focus { + outline: thin dotted; +} + +a:active, +a:hover { + outline: 0; +} + +h1 { + font-size: 1em; + margin: 0.67em 0; +} + +b, +strong { + font-weight: bold; +} + +abbr { + font-size: 0.9em; +} + +abbr[title] { + cursor: help; + border-bottom: 1px dotted #dddddf; + text-decoration: none; +} + +dfn { + font-style: italic; +} + +hr { + height: 0; +} + +mark { + background: #ff0; + color: #000; +} + +code, +kbd, +pre, +samp { + font-family: monospace; + font-size: 1em; +} + +pre { + white-space: pre-wrap; +} + +q { + quotes: "\201C" "\201D" "\2018" "\2019"; +} + +small { + font-size: 80%; +} + +sub, +sup { + font-size: 75%; + line-height: 0; + position: relative; + vertical-align: baseline; +} + +sup { + top: -0.5em; +} + +sub { + bottom: -0.25em; +} + +img { + border: 0; +} + +svg:not(:root) { + overflow: hidden; +} + +figure { + margin: 0; +} + +audio, +video { + display: inline-block; +} + +audio:not([controls]) { + display: none; + height: 0; +} + +fieldset { + border: 1px solid silver; + margin: 0 2px; + padding: 0.35em 0.625em 0.75em; +} + +legend { + border: 0; + padding: 0; +} + +button, +input, +select, +textarea { + font-family: inherit; + font-size: 100%; + margin: 0; +} + +button, +input { + line-height: normal; +} + +button, +select { + text-transform: none; +} + +button, +html input[type=button], +input[type=reset], +input[type=submit] { + -webkit-appearance: button; + cursor: pointer; +} + +button[disabled], +html input[disabled] { + cursor: default; +} + +input[type=checkbox], +input[type=radio] { + padding: 0; +} + +button::-moz-focus-inner, +input::-moz-focus-inner { + border: 0; + padding: 0; +} + +textarea { + overflow: auto; + vertical-align: top; +} + +table { + border-collapse: collapse; + border-spacing: 0; +} + +*, +::before, +::after { + box-sizing: border-box; +} + +html, +body { + font-size: 100%; +} + +body { + background: #fff; + color: rgba(0, 0, 0, 0.8); + padding: 0; + margin: 0; + font-family: "Noto Serif", "DejaVu Serif", serif; + line-height: 1; + position: relative; + cursor: auto; + tab-size: 4; + word-wrap: anywhere; + -moz-osx-font-smoothing: grayscale; + -webkit-font-smoothing: antialiased; +} + +a:hover { + cursor: pointer; +} + +img, +object, +embed { + max-width: 100%; + height: auto; +} + +object, +embed { + height: 100%; +} + +img { + -ms-interpolation-mode: bicubic; +} + +.left { + float: left !important; +} + +.right { + float: right !important; +} + +.text-left { + text-align: left !important; +} + +.text-right { + text-align: right !important; +} + +.text-center { + text-align: center !important; +} + +.text-justify { + text-align: justify !important; +} + +.hide { + display: none; +} + +img, +object, +svg { + display: inline-block; + vertical-align: middle; +} + +textarea { + height: auto; + min-height: 50px; +} + +select { + width: 100%; +} + +.subheader, +.admonitionblock td.content > .title, +.audioblock > .title, +.exampleblock > .title, +.imageblock > .title, +.listingblock > .title, +.literalblock > .title, +.stemblock > .title, +.openblock > .title, +.paragraph > .title, +.quoteblock > .title, +table.tableblock > .title, +.verseblock > .title, +.videoblock > .title, +.dlist > .title, +.olist > .title, +.ulist > .title, +.qlist > .title, +.hdlist > .title { + line-height: 1.45; + color: #7a2518; + font-weight: 400; + margin-top: 0; + margin-bottom: 0.25em; +} + +div, +dl, +dt, +dd, +ul, +ol, +li, +h1, +h2, +h3, +#toctitle, +.sidebarblock > .content > .title, +h4, +h5, +h6, +pre, +form, +p, +blockquote, +th, +td { + margin: 0; + padding: 0; +} + +a { + color: #2156a5; + text-decoration: underline; + line-height: inherit; +} + +a:hover, +a:focus { + color: #1d4b8f; +} + +a img { + border: 0; +} + +p { + line-height: 1.6; + margin-bottom: 1.25em; + text-rendering: optimizeLegibility; +} + +p aside { + font-size: 0.875em; + line-height: 1.35; + font-style: italic; +} + +h1, +h2, +h3, +#toctitle, +.sidebarblock > .content > .title, +h4, +h5, +h6 { + font-family: "Open Sans", "DejaVu Sans", sans-serif; + font-weight: 400; + font-style: normal; + color: #733700; + text-rendering: optimizeLegibility; + margin-top: 1em; + margin-bottom: 0.5em; + line-height: 1.0125em; +} + +h1 small, +h2 small, +h3 small, +#toctitle small, +.sidebarblock > .content > .title small, +h4 small, +h5 small, +h6 small { + font-size: 60%; + color: #e99b8f; + line-height: 0; +} + +h1 { + font-size: 2.125em; +} + +h2 { + font-size: 1.6875em; +} + +h3, +#toctitle, +.sidebarblock > .content > .title { + font-size: 1.375em; +} + +h4, +h5 { + font-size: 1.125em; +} + +h6 { + font-size: 1em; +} + +hr { + border: solid #dddddf; + border-width: 1px 0 0; + clear: both; + margin: 1.25em 0 1.1875em; +} + +em, +i { + font-style: italic; + line-height: inherit; +} + +strong, +b { + font-weight: bold; + line-height: inherit; +} + +small { + font-size: 60%; + line-height: inherit; +} + +code { + font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace; + font-weight: 400; + color: rgba(0, 0, 0, 0.9); +} + +ul, +ol, +dl { + line-height: 1.6; + margin-bottom: 1.25em; + list-style-position: outside; + font-family: inherit; +} + +ul, +ol { + margin-left: 1.5em; +} + +ul li ul, +ul li ol { + margin-left: 1.25em; + margin-bottom: 0; +} + +ul.circle { + list-style-type: circle; +} + +ul.disc { + list-style-type: disc; +} + +ul.square { + list-style-type: square; +} + +ul.circle ul:not([class]), +ul.disc ul:not([class]), +ul.square ul:not([class]) { + list-style: inherit; +} + +ol li ul, +ol li ol { + margin-left: 1.25em; + margin-bottom: 0; +} + +dl dt { + margin-bottom: 0.3125em; + font-weight: bold; +} + +dl dd { + margin-bottom: 1.25em; +} + +blockquote { + margin: 0 0 1.25em; + padding: 0.5625em 1.25em 0 1.1875em; + border-left: 1px solid #ddd; +} + +blockquote, +blockquote p { + line-height: 1.6; + color: rgba(0, 0, 0, 0.85); +} + +@media screen and (min-width: 768px) { + h1, + h2, + h3, + #toctitle, + .sidebarblock > .content > .title, + h4, + h5, + h6 { + line-height: 1.2; + } + + h1 { + font-size: 2.3em; + } + + h2 { + font-size: 2.3125em; + } + + h3, + #toctitle, + .sidebarblock > .content > .title { + font-size: 1.6875em; + } + + h4 { + font-size: 1.4375em; + } +} + +table { + background: #fff; + margin-bottom: 1.25em; + border: 1px solid #dedede; + word-wrap: normal; +} + +table thead, +table tfoot { + background: #f7f8f7; +} + +table thead tr th, +table thead tr td, +table tfoot tr th, +table tfoot tr td { + padding: 0.5em 0.625em 0.625em; + font-size: inherit; + color: rgba(0, 0, 0, 0.8); + text-align: left; +} + +table tr th, +table tr td { + padding: 0.5625em 0.625em; + font-size: inherit; + color: rgba(0, 0, 0, 0.8); +} + +table tr.even, +table tr.alt { + background: #f8f8f7; +} + +table thead tr th, +table tfoot tr th, +table tbody tr td, +table tr td, +table tfoot tr td { + line-height: 1.6; +} + +h1, +h2, +h3, +#toctitle, +.sidebarblock > .content > .title, +h4, +h5, +h6 { + line-height: 1.2; + word-spacing: -0.05em; +} + +h1 strong, +h2 strong, +h3 strong, +#toctitle strong, +.sidebarblock > .content > .title strong, +h4 strong, +h5 strong, +h6 strong { + font-weight: 400; +} + +.center { + margin-left: auto; + margin-right: auto; +} + +.stretch { + width: 100%; +} + +.clearfix::before, +.clearfix::after, +.float-group::before, +.float-group::after { + content: " "; + display: table; +} + +.clearfix::after, +.float-group::after { + clear: both; +} + +:not(pre).nobreak { + word-wrap: normal; +} + +:not(pre).nowrap { + white-space: nowrap; +} + +:not(pre).pre-wrap { + white-space: pre-wrap; +} + +:not(pre):not([class^=L]) > code { + font-size: 0.9375em; + font-style: normal !important; + letter-spacing: 0; + padding: 0.1em 0.5ex; + word-spacing: -0.15em; + background: #f7f7f8; + border-radius: 4px; + line-height: 1.45; + text-rendering: optimizeSpeed; +} + +pre { + color: rgba(0, 0, 0, 0.9); + font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace; + line-height: 1.45; + text-rendering: optimizeSpeed; +} + +pre code, +pre pre { + color: inherit; + font-size: inherit; + line-height: inherit; +} + +pre > code { + display: block; +} + +pre.nowrap, +pre.nowrap pre { + white-space: pre; + word-wrap: normal; +} + +em em { + font-style: normal; +} + +strong strong { + font-weight: 400; +} + +.keyseq { + color: rgba(51, 51, 51, 0.8); +} + +kbd { + font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace; + display: inline-block; + color: rgba(0, 0, 0, 0.8); + font-size: 0.65em; + line-height: 1.45; + background: #f7f7f7; + border: 1px solid #ccc; + border-radius: 3px; + box-shadow: 0 1px 0 rgba(0, 0, 0, 0.2), 0 0 0 0.1em #fff inset; + margin: 0 0.15em; + padding: 0.2em 0.5em; + vertical-align: middle; + position: relative; + top: -0.1em; + white-space: nowrap; +} + +.keyseq kbd:first-child { + margin-left: 0; +} + +.keyseq kbd:last-child { + margin-right: 0; +} + +.menuseq, +.menuref { + color: #000; +} + +.menuseq b:not(.caret), +.menuref { + font-weight: inherit; +} + +.menuseq { + word-spacing: -0.02em; +} + +.menuseq b.caret { + font-size: 1.25em; + line-height: 0.8; +} + +.menuseq i.caret { + font-weight: bold; + text-align: center; + width: 0.45em; +} + +b.button::before, +b.button::after { + position: relative; + top: -1px; + font-weight: 400; +} + +b.button::before { + content: "["; + padding: 0 3px 0 2px; +} + +b.button::after { + content: "]"; + padding: 0 2px 0 3px; +} + +p a > code:hover { + color: rgba(0, 0, 0, 0.9); +} + +#header, +#content, +#footnotes, +#footer { + width: 100%; + margin: 0 auto; + max-width: 62.5em; + *zoom: 1; + position: relative; + padding-left: 0.9375em; + padding-right: 0.9375em; +} + +#header::before, +#header::after, +#content::before, +#content::after, +#footnotes::before, +#footnotes::after, +#footer::before, +#footer::after { + content: " "; + display: table; +} + +#header::after, +#content::after, +#footnotes::after, +#footer::after { + clear: both; +} + +#content { + margin-top: 1.25em; +} + +#content::before { + content: none; +} + +#header > h1:first-child { + color: rgba(0, 0, 0, 0.85); + margin-top: 2.25rem; + margin-bottom: 0; +} + +#header > h1:first-child + #toc { + margin-top: 8px; + border-top: 1px solid #dddddf; +} + +#header > h1:only-child, +body.toc2 #header > h1:nth-last-child(2) { + border-bottom: 1px solid #dddddf; + padding-bottom: 8px; +} + +#header .details { + border-bottom: 1px solid #dddddf; + line-height: 1.45; + padding-top: 0.25em; + padding-bottom: 0.25em; + padding-left: 0.25em; + color: rgba(0, 0, 0, 0.6); + display: flex; + flex-flow: row wrap; +} + +#header .details span:first-child { + margin-left: -0.125em; +} + +#header .details span.email a { + color: rgba(0, 0, 0, 0.85); +} + +#header .details br { + display: none; +} + +#header .details br + span::before { + content: "\00a0\2013\00a0"; +} + +#header .details br + span.author::before { + content: "\00a0\22c5\00a0"; + color: rgba(0, 0, 0, 0.85); +} + +#header .details br + span#revremark::before { + content: "\00a0|\00a0"; +} + +#header #revnumber { + text-transform: capitalize; +} + +#header #revnumber::after { + content: "\00a0"; +} + +#content > h1:first-child:not([class]) { + color: rgba(0, 0, 0, 0.85); + border-bottom: 1px solid #dddddf; + padding-bottom: 8px; + margin-top: 0; + padding-top: 1rem; + margin-bottom: 1.25rem; +} + +#toc { + border-bottom: 1px solid #e7e7e9; + padding-bottom: 0.5em; +} + +#toc > ul { + margin-left: 0.125em; +} + +#toc ul.sectlevel0 > li > a { + font-style: italic; +} + +#toc ul.sectlevel0 ul.sectlevel1 { + margin: 0.5em 0; +} + +#toc ul { + font-family: "Open Sans", "DejaVu Sans", sans-serif; + list-style-type: none; +} + +#toc li { + line-height: 1.3334; + margin-top: 0.3334em; +} + +#toc a { + text-decoration: none; + color: #FFFFFF; +} + +#toc a:active { + text-decoration: underline; +} + +#toctitle { + color: #FFEBCC; + font-size: 1.3em; +} + +@media screen and (min-width: 768px) { + #toctitle { + font-size: 1.375em; + } + + body.toc2 { + padding-left: 15em; + padding-right: 0; + } + + #toc.toc2 { + margin-top: 0 !important; + background: #239DD5; + position: fixed; + width: 15em; + left: 0; + top: 0; + border-right: 1px solid #e7e7e9; + border-top-width: 0 !important; + border-bottom-width: 0 !important; + z-index: 1000; + padding: 1.25em 1em; + height: 100%; + overflow: auto; + } + + #toc.toc2 #toctitle { + margin-top: 0; + margin-bottom: 0.8rem; + font-size: 1.2em; + } + + #toc.toc2 > ul { + font-size: 0.9em; + margin-bottom: 0; + } + + #toc.toc2 ul ul { + margin-left: 0; + padding-left: 1em; + } + + #toc.toc2 ul.sectlevel0 ul.sectlevel1 { + padding-left: 0; + margin-top: 0.5em; + margin-bottom: 0.5em; + } + + body.toc2.toc-right { + padding-left: 0; + padding-right: 15em; + } + + body.toc2.toc-right #toc.toc2 { + border-right-width: 0; + border-left: 1px solid #e7e7e9; + left: auto; + right: 0; + } +} + +@media screen and (min-width: 1280px) { + body.toc2 { + padding-left: 20em; + padding-right: 0; + } + + #toc.toc2 { + width: 20em; + } + + #toc.toc2 #toctitle { + font-size: 1.375em; + } + + #toc.toc2 > ul { + font-size: 0.95em; + } + + #toc.toc2 ul ul { + padding-left: 1.25em; + } + + body.toc2.toc-right { + padding-left: 0; + padding-right: 20em; + } +} + +#content #toc { + border: 1px solid #e0e0dc; + margin-bottom: 1.25em; + padding: 1.25em; + background: #f8f8f7; + border-radius: 4px; +} + +#content #toc > :first-child { + margin-top: 0; +} + +#content #toc > :last-child { + margin-bottom: 0; +} + +#footer { + max-width: none; + background: rgba(0, 0, 0, 0.8); + padding: 1.25em; +} + +#footer-text { + color: rgba(255, 255, 255, 0.8); + line-height: 1.44; +} + +#content { + margin-bottom: 0.625em; +} + +.sect1 { + padding-bottom: 0.625em; +} + +@media screen and (min-width: 768px) { + #content { + margin-bottom: 1.25em; + } + + .sect1 { + padding-bottom: 1.25em; + } +} + +.sect1:last-child { + padding-bottom: 0; +} + +.sect1 + .sect1 { + border-top: 1px solid #e7e7e9; +} + +#content h1 > a.anchor, +h2 > a.anchor, +h3 > a.anchor, +#toctitle > a.anchor, +.sidebarblock > .content > .title > a.anchor, +h4 > a.anchor, +h5 > a.anchor, +h6 > a.anchor { + position: absolute; + z-index: 1001; + width: 1.5ex; + margin-left: -1.5ex; + display: block; + text-decoration: none !important; + visibility: hidden; + text-align: center; + font-weight: 400; +} + +#content h1 > a.anchor::before, +h2 > a.anchor::before, +h3 > a.anchor::before, +#toctitle > a.anchor::before, +.sidebarblock > .content > .title > a.anchor::before, +h4 > a.anchor::before, +h5 > a.anchor::before, +h6 > a.anchor::before { + content: "\00A7"; + font-size: 0.85em; + display: block; + padding-top: 0.1em; +} + +#content h1:hover > a.anchor, +#content h1 > a.anchor:hover, +h2:hover > a.anchor, +h2 > a.anchor:hover, +h3:hover > a.anchor, +#toctitle:hover > a.anchor, +.sidebarblock > .content > .title:hover > a.anchor, +h3 > a.anchor:hover, +#toctitle > a.anchor:hover, +.sidebarblock > .content > .title > a.anchor:hover, +h4:hover > a.anchor, +h4 > a.anchor:hover, +h5:hover > a.anchor, +h5 > a.anchor:hover, +h6:hover > a.anchor, +h6 > a.anchor:hover { + visibility: visible; +} + +#content h1 > a.link, +h2 > a.link, +h3 > a.link, +#toctitle > a.link, +.sidebarblock > .content > .title > a.link, +h4 > a.link, +h5 > a.link, +h6 > a.link { + color: #ba3925; + text-decoration: none; +} + +#content h1 > a.link:hover, +h2 > a.link:hover, +h3 > a.link:hover, +#toctitle > a.link:hover, +.sidebarblock > .content > .title > a.link:hover, +h4 > a.link:hover, +h5 > a.link:hover, +h6 > a.link:hover { + color: #a53221; +} + +details, +.audioblock, +.imageblock, +.literalblock, +.listingblock, +.stemblock, +.videoblock { + margin-bottom: 1.25em; +} + +details { + margin-left: 1.25rem; +} + +details > summary { + cursor: pointer; + display: block; + position: relative; + line-height: 1.6; + margin-bottom: 0.625rem; + outline: none; + -webkit-tap-highlight-color: transparent; +} + +details > summary::-webkit-details-marker { + display: none; +} + +details > summary::before { + content: ""; + border: solid transparent; + border-left-color: currentColor; + border-width: 0.3em 0 0.3em 0.5em; + position: absolute; + top: 0.5em; + left: -1.25rem; + transform: translateX(15%); +} + +details[open] > summary::before { + border: solid transparent; + border-top-color: currentColor; + border-width: 0.5em 0.3em 0; + transform: translateY(15%); +} + +details > summary::after { + content: ""; + width: 1.25rem; + height: 1em; + position: absolute; + top: 0.3em; + left: -1.25rem; +} + +.admonitionblock td.content > .title, +.audioblock > .title, +.exampleblock > .title, +.imageblock > .title, +.listingblock > .title, +.literalblock > .title, +.stemblock > .title, +.openblock > .title, +.paragraph > .title, +.quoteblock > .title, +table.tableblock > .title, +.verseblock > .title, +.videoblock > .title, +.dlist > .title, +.olist > .title, +.ulist > .title, +.qlist > .title, +.hdlist > .title { + text-rendering: optimizeLegibility; + text-align: left; + font-family: "Noto Serif", "DejaVu Serif", serif; + font-size: 1rem; + font-style: italic; +} + +table.tableblock.fit-content > caption.title { + white-space: nowrap; + width: 0; +} + +.paragraph.lead > p, +#preamble > .sectionbody > [class=paragraph]:first-of-type p { + font-size: 1.21875em; + line-height: 1.6; + color: rgba(0, 0, 0, 0.85); +} + +.admonitionblock > table { + border-collapse: separate; + border: 0; + background: none; + width: 100%; +} + +.admonitionblock > table td.icon { + text-align: center; + width: 80px; +} + +.admonitionblock > table td.icon img { + max-width: none; +} + +.admonitionblock > table td.icon .title { + font-weight: bold; + font-family: "Open Sans", "DejaVu Sans", sans-serif; + text-transform: uppercase; +} + +.admonitionblock > table td.content { + padding-left: 1.125em; + padding-right: 1.25em; + border-left: 1px solid #dddddf; + color: rgba(0, 0, 0, 0.6); + word-wrap: anywhere; +} + +.admonitionblock > table td.content > :last-child > :last-child { + margin-bottom: 0; +} + +.exampleblock > .content { + border: 1px solid #e6e6e6; + margin-bottom: 1.25em; + padding: 1.25em; + background: #fff; + border-radius: 4px; +} + +.sidebarblock { + border: 1px solid #dbdbd6; + margin-bottom: 1.25em; + padding: 1.25em; + background: #f3f3f2; + border-radius: 4px; +} + +.sidebarblock > .content > .title { + color: #7a2518; + margin-top: 0; + text-align: center; +} + +.exampleblock > .content > :first-child, +.sidebarblock > .content > :first-child { + margin-top: 0; +} + +.exampleblock > .content > :last-child, +.exampleblock > .content > :last-child > :last-child, +.exampleblock > .content .olist > ol > li:last-child > :last-child, +.exampleblock > .content .ulist > ul > li:last-child > :last-child, +.exampleblock > .content .qlist > ol > li:last-child > :last-child, +.sidebarblock > .content > :last-child, +.sidebarblock > .content > :last-child > :last-child, +.sidebarblock > .content .olist > ol > li:last-child > :last-child, +.sidebarblock > .content .ulist > ul > li:last-child > :last-child, +.sidebarblock > .content .qlist > ol > li:last-child > :last-child { + margin-bottom: 0; +} + +.literalblock pre, +.listingblock > .content > pre { + border-radius: 4px; + overflow-x: auto; + padding: 1em; + font-size: 0.8125em; +} + +@media screen and (min-width: 768px) { + .literalblock pre, + .listingblock > .content > pre { + font-size: 0.90625em; + } +} + +@media screen and (min-width: 1280px) { + .literalblock pre, + .listingblock > .content > pre { + font-size: 1em; + } +} + +.literalblock pre, +.listingblock > .content > pre:not(.highlight), +.listingblock > .content > pre[class=highlight], +.listingblock > .content > pre[class^="highlight "] { + background: #f7f7f8; +} + +.literalblock.output pre { + color: #f7f7f8; + background: rgba(0, 0, 0, 0.9); +} + +.listingblock > .content { + position: relative; +} + +.listingblock code[data-lang]::before { + display: none; + content: attr(data-lang); + position: absolute; + font-size: 0.75em; + top: 0.425rem; + right: 0.5rem; + line-height: 1; + text-transform: uppercase; + color: inherit; + opacity: 0.5; +} + +.listingblock:hover code[data-lang]::before { + display: block; +} + +.listingblock.terminal pre .command::before { + content: attr(data-prompt); + padding-right: 0.5em; + color: inherit; + opacity: 0.5; +} + +.listingblock.terminal pre .command:not([data-prompt])::before { + content: "$"; +} + +.listingblock pre.highlightjs { + padding: 0; +} + +.listingblock pre.highlightjs > code { + padding: 1em; + border-radius: 4px; +} + +.listingblock pre.prettyprint { + border-width: 0; +} + +.prettyprint { + background: #f7f7f8; +} + +pre.prettyprint .linenums { + line-height: 1.45; + margin-left: 2em; +} + +pre.prettyprint li { + background: none; + list-style-type: inherit; + padding-left: 0; +} + +pre.prettyprint li code[data-lang]::before { + opacity: 1; +} + +pre.prettyprint li:not(:first-child) code[data-lang]::before { + display: none; +} + +table.linenotable { + border-collapse: separate; + border: 0; + margin-bottom: 0; + background: none; +} + +table.linenotable td[class] { + color: inherit; + vertical-align: top; + padding: 0; + line-height: inherit; + white-space: normal; +} + +table.linenotable td.code { + padding-left: 0.75em; +} + +table.linenotable td.linenos, +pre.pygments .linenos { + border-right: 1px solid; + opacity: 0.35; + padding-right: 0.5em; + user-select: none; +} + +pre.pygments span.linenos { + display: inline-block; + margin-right: 0.75em; +} + +.quoteblock { + margin: 0 1em 1.25em 1.5em; + display: table; +} + +.quoteblock:not(.excerpt) > .title { + margin-left: -1.5em; + margin-bottom: 0.75em; +} + +.quoteblock blockquote, +.quoteblock p { + color: rgba(0, 0, 0, 0.85); + font-size: 1.15rem; + line-height: 1.75; + word-spacing: 0.1em; + letter-spacing: 0; + font-style: italic; + text-align: justify; +} + +.quoteblock blockquote { + margin: 0; + padding: 0; + border: 0; +} + +.quoteblock blockquote::before { + content: "\201c"; + float: left; + font-size: 2.75em; + font-weight: bold; + line-height: 0.6em; + margin-left: -0.6em; + color: #7a2518; + text-shadow: 0 1px 2px rgba(0, 0, 0, 0.1); +} + +.quoteblock blockquote > .paragraph:last-child p { + margin-bottom: 0; +} + +.quoteblock .attribution { + margin-top: 0.75em; + margin-right: 0.5ex; + text-align: right; +} + +.verseblock { + margin: 0 1em 1.25em; +} + +.verseblock pre { + font-family: "Open Sans", "DejaVu Sans", sans-serif; + font-size: 1.15rem; + color: rgba(0, 0, 0, 0.85); + font-weight: 300; + text-rendering: optimizeLegibility; +} + +.verseblock pre strong { + font-weight: 400; +} + +.verseblock .attribution { + margin-top: 1.25rem; + margin-left: 0.5ex; +} + +.quoteblock .attribution, +.verseblock .attribution { + font-size: 0.9375em; + line-height: 1.45; + font-style: italic; +} + +.quoteblock .attribution br, +.verseblock .attribution br { + display: none; +} + +.quoteblock .attribution cite, +.verseblock .attribution cite { + display: block; + letter-spacing: -0.025em; + color: rgba(0, 0, 0, 0.6); +} + +.quoteblock.abstract blockquote::before, +.quoteblock.excerpt blockquote::before, +.quoteblock .quoteblock blockquote::before { + display: none; +} + +.quoteblock.abstract blockquote, +.quoteblock.abstract p, +.quoteblock.excerpt blockquote, +.quoteblock.excerpt p, +.quoteblock .quoteblock blockquote, +.quoteblock .quoteblock p { + line-height: 1.6; + word-spacing: 0; +} + +.quoteblock.abstract { + margin: 0 1em 1.25em; + display: block; +} + +.quoteblock.abstract > .title { + margin: 0 0 0.375em; + font-size: 1.15em; + text-align: center; +} + +.quoteblock.excerpt > blockquote, +.quoteblock .quoteblock { + padding: 0 0 0.25em 1em; + border-left: 0.25em solid #dddddf; +} + +.quoteblock.excerpt, +.quoteblock .quoteblock { + margin-left: 0; +} + +.quoteblock.excerpt blockquote, +.quoteblock.excerpt p, +.quoteblock .quoteblock blockquote, +.quoteblock .quoteblock p { + color: inherit; + font-size: 1.0625rem; +} + +.quoteblock.excerpt .attribution, +.quoteblock .quoteblock .attribution { + color: inherit; + font-size: 0.85rem; + text-align: left; + margin-right: 0; +} + +p.tableblock:last-child { + margin-bottom: 0; +} + +td.tableblock > .content { + margin-bottom: 1.25em; + word-wrap: anywhere; +} + +td.tableblock > .content > :last-child { + margin-bottom: -1.25em; +} + +table.tableblock, +th.tableblock, +td.tableblock { + border: 0 solid #dedede; +} + +table.grid-all > * > tr > * { + border-width: 1px; +} + +table.grid-cols > * > tr > * { + border-width: 0 1px; +} + +table.grid-rows > * > tr > * { + border-width: 1px 0; +} + +table.frame-all { + border-width: 1px; +} + +table.frame-ends { + border-width: 1px 0; +} + +table.frame-sides { + border-width: 0 1px; +} + +table.frame-none > colgroup + * > :first-child > *, +table.frame-sides > colgroup + * > :first-child > * { + border-top-width: 0; +} + +table.frame-none > :last-child > :last-child > *, +table.frame-sides > :last-child > :last-child > * { + border-bottom-width: 0; +} + +table.frame-none > * > tr > :first-child, +table.frame-ends > * > tr > :first-child { + border-left-width: 0; +} + +table.frame-none > * > tr > :last-child, +table.frame-ends > * > tr > :last-child { + border-right-width: 0; +} + +table.stripes-all > * > tr, +table.stripes-odd > * > tr:nth-of-type(odd), +table.stripes-even > * > tr:nth-of-type(even), +table.stripes-hover > * > tr:hover { + background: #f8f8f7; +} + +th.halign-left, +td.halign-left { + text-align: left; +} + +th.halign-right, +td.halign-right { + text-align: right; +} + +th.halign-center, +td.halign-center { + text-align: center; +} + +th.valign-top, +td.valign-top { + vertical-align: top; +} + +th.valign-bottom, +td.valign-bottom { + vertical-align: bottom; +} + +th.valign-middle, +td.valign-middle { + vertical-align: middle; +} + +table thead th, +table tfoot th { + font-weight: bold; +} + +tbody tr th { + background: #f7f8f7; +} + +tbody tr th, +tbody tr th p, +tfoot tr th, +tfoot tr th p { + color: rgba(0, 0, 0, 0.8); + font-weight: bold; +} + +p.tableblock > code:only-child { + background: none; + padding: 0; +} + +p.tableblock { + font-size: 1em; +} + +ol { + margin-left: 1.75em; +} + +ul li ol { + margin-left: 1.5em; +} + +dl dd { + margin-left: 1.125em; +} + +dl dd:last-child, +dl dd:last-child > :last-child { + margin-bottom: 0; +} + +li p, +ul dd, +ol dd, +.olist .olist, +.ulist .ulist, +.ulist .olist, +.olist .ulist { + margin-bottom: 0.625em; +} + +ul.checklist, +ul.none, +ol.none, +ul.no-bullet, +ol.no-bullet, +ol.unnumbered, +ul.unstyled, +ol.unstyled { + list-style-type: none; +} + +ul.no-bullet, +ol.no-bullet, +ol.unnumbered { + margin-left: 0.625em; +} + +ul.unstyled, +ol.unstyled { + margin-left: 0; +} + +li > p:empty:only-child::before { + content: ""; + display: inline-block; +} + +ul.checklist > li > p:first-child { + margin-left: -1em; +} + +ul.checklist > li > p:first-child > .fa-square-o:first-child, +ul.checklist > li > p:first-child > .fa-check-square-o:first-child { + width: 1.25em; + font-size: 0.8em; + position: relative; + bottom: 0.125em; +} + +ul.checklist > li > p:first-child > input[type=checkbox]:first-child { + margin-right: 0.25em; +} + +ul.inline { + display: flex; + flex-flow: row wrap; + list-style: none; + margin: 0 0 0.625em -1.25em; +} + +ul.inline > li { + margin-left: 1.25em; +} + +.unstyled dl dt { + font-weight: 400; + font-style: normal; +} + +ol.arabic { + list-style-type: decimal; +} + +ol.decimal { + list-style-type: decimal-leading-zero; +} + +ol.loweralpha { + list-style-type: lower-alpha; +} + +ol.upperalpha { + list-style-type: upper-alpha; +} + +ol.lowerroman { + list-style-type: lower-roman; +} + +ol.upperroman { + list-style-type: upper-roman; +} + +ol.lowergreek { + list-style-type: lower-greek; +} + +.hdlist > table, +.colist > table { + border: 0; + background: none; +} + +.hdlist > table > tbody > tr, +.colist > table > tbody > tr { + background: none; +} + +td.hdlist1, +td.hdlist2 { + vertical-align: top; + padding: 0 0.625em; +} + +td.hdlist1 { + font-weight: bold; + padding-bottom: 1.25em; +} + +td.hdlist2 { + word-wrap: anywhere; +} + +.literalblock + .colist, +.listingblock + .colist { + margin-top: -0.5em; +} + +.colist td:not([class]):first-child { + padding: 0.4em 0.75em 0; + line-height: 1; + vertical-align: top; +} + +.colist td:not([class]):first-child img { + max-width: none; +} + +.colist td:not([class]):last-child { + padding: 0.25em 0; +} + +.thumb, +.th { + line-height: 0; + display: inline-block; + border: 4px solid #fff; + box-shadow: 0 0 0 1px #ddd; +} + +.imageblock.left { + margin: 0.25em 0.625em 1.25em 0; +} + +.imageblock.right { + margin: 0.25em 0 1.25em 0.625em; +} + +.imageblock > .title { + margin-bottom: 0; +} + +.imageblock.thumb, +.imageblock.th { + border-width: 6px; +} + +.imageblock.thumb > .title, +.imageblock.th > .title { + padding: 0 0.125em; +} + +.image.left, +.image.right { + margin-top: 0.25em; + margin-bottom: 0.25em; + display: inline-block; + line-height: 0; +} + +.image.left { + margin-right: 0.625em; +} + +.image.right { + margin-left: 0.625em; +} + +a.image { + text-decoration: none; + display: inline-block; +} + +a.image object { + pointer-events: none; +} + +sup.footnote, +sup.footnoteref { + font-size: 0.875em; + position: static; + vertical-align: super; +} + +sup.footnote a, +sup.footnoteref a { + text-decoration: none; +} + +sup.footnote a:active, +sup.footnoteref a:active { + text-decoration: underline; +} + +#footnotes { + padding-top: 0.75em; + padding-bottom: 0.75em; + margin-bottom: 0.625em; +} + +#footnotes hr { + width: 20%; + min-width: 6.25em; + margin: -0.25em 0 0.75em; + border-width: 1px 0 0; +} + +#footnotes .footnote { + padding: 0 0.375em 0 0.225em; + line-height: 1.3334; + font-size: 0.875em; + margin-left: 1.2em; + margin-bottom: 0.2em; +} + +#footnotes .footnote a:first-of-type { + font-weight: bold; + text-decoration: none; + margin-left: -1.05em; +} + +#footnotes .footnote:last-of-type { + margin-bottom: 0; +} + +#content #footnotes { + margin-top: -0.625em; + margin-bottom: 0; + padding: 0.75em 0; +} + +div.unbreakable { + page-break-inside: avoid; +} + +.big { + font-size: larger; +} + +.small { + font-size: smaller; +} + +.underline { + text-decoration: underline; +} + +.overline { + text-decoration: overline; +} + +.line-through { + text-decoration: line-through; +} + +.aqua { + color: #00bfbf; +} + +.aqua-background { + background: #00fafa; +} + +.black { + color: #000; +} + +.black-background { + background: #000; +} + +.blue { + color: #0000bf; +} + +.blue-background { + background: #0000fa; +} + +.fuchsia { + color: #bf00bf; +} + +.fuchsia-background { + background: #fa00fa; +} + +.gray { + color: #606060; +} + +.gray-background { + background: #7d7d7d; +} + +.green { + color: #006000; +} + +.green-background { + background: #007d00; +} + +.lime { + color: #00bf00; +} + +.lime-background { + background: #00fa00; +} + +.maroon { + color: #600000; +} + +.maroon-background { + background: #7d0000; +} + +.navy { + color: #000060; +} + +.navy-background { + background: #00007d; +} + +.olive { + color: #606000; +} + +.olive-background { + background: #7d7d00; +} + +.purple { + color: #600060; +} + +.purple-background { + background: #7d007d; +} + +.red { + color: #bf0000; +} + +.red-background { + background: #fa0000; +} + +.silver { + color: #909090; +} + +.silver-background { + background: #bcbcbc; +} + +.teal { + color: #006060; +} + +.teal-background { + background: #007d7d; +} + +.white { + color: #bfbfbf; +} + +.white-background { + background: #fafafa; +} + +.yellow { + color: #bfbf00; +} + +.yellow-background { + background: #fafa00; +} + +span.icon > .fa { + cursor: default; +} + +a span.icon > .fa { + cursor: inherit; +} + +.admonitionblock td.icon [class^="fa icon-"] { + font-size: 2.5em; + text-shadow: 1px 1px 2px rgba(0, 0, 0, 0.5); + cursor: default; +} + +.admonitionblock td.icon .icon-note::before { + content: "\f05a"; + color: #19407c; +} + +.admonitionblock td.icon .icon-tip::before { + content: "\f0eb"; + text-shadow: 1px 1px 2px rgba(155, 155, 0, 0.8); + color: #111; +} + +.admonitionblock td.icon .icon-warning::before { + content: "\f071"; + color: #bf6900; +} + +.admonitionblock td.icon .icon-caution::before { + content: "\f06d"; + color: #bf3400; +} + +.admonitionblock td.icon .icon-important::before { + content: "\f06a"; + color: #bf0000; +} + +.conum[data-value] { + display: inline-block; + color: #fff !important; + background: rgba(0, 0, 0, 0.8); + border-radius: 50%; + text-align: center; + font-size: 0.75em; + width: 1.67em; + height: 1.67em; + line-height: 1.67em; + font-family: "Open Sans", "DejaVu Sans", sans-serif; + font-style: normal; + font-weight: bold; +} + +.conum[data-value] * { + color: #fff !important; +} + +.conum[data-value] + b { + display: none; +} + +.conum[data-value]::after { + content: attr(data-value); +} + +pre .conum[data-value] { + position: relative; + top: -0.125em; +} + +b.conum * { + color: inherit !important; +} + +.conum:not([data-value]):empty { + display: none; +} + +dt, +th.tableblock, +td.content, +div.footnote { + text-rendering: optimizeLegibility; +} + +h1, +h2, +p, +td.content, +span.alt, +summary { + letter-spacing: -0.01em; +} + +p strong, +td.content strong, +div.footnote strong { + letter-spacing: -0.005em; +} + +p, +blockquote, +dt, +td.content, +td.hdlist1, +span.alt, +summary { + font-size: 1.0625rem; +} + +p { + margin-bottom: 1.25rem; +} + +.sidebarblock p, +.sidebarblock dt, +.sidebarblock td.content, +p.tableblock { + font-size: 1em; +} + +.exampleblock > .content { + background: #fffef7; + border-color: #e0e0dc; + box-shadow: 0 1px 4px #e0e0dc; +} + +.print-only { + display: none !important; +} + +@page { + margin: 1.25cm 0.75cm; +} + +@media print { + * { + box-shadow: none !important; + text-shadow: none !important; + } + + html { + font-size: 80%; + } + + a { + color: inherit !important; + text-decoration: underline !important; + } + + a.bare, + a[href^="#"], + a[href^="mailto:"] { + text-decoration: none !important; + } + + a[href^="http:"]:not(.bare)::after, + a[href^="https:"]:not(.bare)::after { + content: "(" attr(href) ")"; + display: inline-block; + font-size: 0.875em; + padding-left: 0.25em; + } + + abbr[title] { + border-bottom: 1px dotted; + } + + abbr[title]::after { + content: " (" attr(title) ")"; + } + + pre, + blockquote, + tr, + img, + object, + svg { + page-break-inside: avoid; + } + + thead { + display: table-header-group; + } + + svg { + max-width: 100%; + } + + p, + blockquote, + dt, + td.content { + font-size: 1em; + orphans: 3; + widows: 3; + } + + h2, + h3, + #toctitle, + .sidebarblock > .content > .title { + page-break-after: avoid; + } + + #header, + #content, + #footnotes, + #footer { + max-width: none; + } + + #toc, + .sidebarblock, + .exampleblock > .content { + background: none !important; + } + + #toc { + border-bottom: 1px solid #dddddf !important; + padding-bottom: 0 !important; + } + + body.book #header { + text-align: center; + } + + body.book #header > h1:first-child { + border: 0 !important; + margin: 2.5em 0 1em; + } + + body.book #header .details { + border: 0 !important; + display: block; + padding: 0 !important; + } + + body.book #header .details span:first-child { + margin-left: 0 !important; + } + + body.book #header .details br { + display: block; + } + + body.book #header .details br + span::before { + content: none !important; + } + + body.book #toc { + border: 0 !important; + text-align: left !important; + padding: 0 !important; + margin: 0 !important; + } + + body.book #toc, + body.book #preamble, + body.book h1.sect0, + body.book .sect1 > h2 { + page-break-before: always; + } + + .listingblock code[data-lang]::before { + display: block; + } + + #footer { + padding: 0 0.9375em; + } + + .hide-on-print { + display: none !important; + } + + .print-only { + display: block !important; + } + + .hide-for-print { + display: none !important; + } + + .show-for-print { + display: inherit !important; + } +} + +@media amzn-kf8, print { + #header > h1:first-child { + margin-top: 1.25rem; + } + + .sect1 { + padding: 0 !important; + } + + .sect1 + .sect1 { + border: 0; + } + + #footer { + background: none; + } + + #footer-text { + color: rgba(0, 0, 0, 0.6); + font-size: 0.9em; + } +} + +@media amzn-kf8 { + #header, + #content, + #footnotes, + #footer { + padding: 0; + } +} diff --git a/doc/asciidoc/modules.adoc b/doc/asciidoc/modules.adoc new file mode 100644 index 000000000..149a61d6e --- /dev/null +++ b/doc/asciidoc/modules.adoc @@ -0,0 +1,156 @@ +=== Modules +:simplemod: sail_doc/simple_mod.json + +Sail provides support for organizing large specifications into +_modules_. Modules provide an access control mechanism, meaning a Sail +definition in one module cannot access or use definitions provided by +another module unless it explicitly _requires_ the other module. + +The module structure of a Sail specification is specified in a +separate `.rigging` file (so named because +https://en.wikipedia.org/wiki/Rigging[rigging] is what supports and +organizes the sails on a ship). + +For a simple example, let's assume we have two Sail files `amod.sail` and +`bmod.sail`: + +.`amod.sail` +[source,sail] +---- +include::sail:ALFA[from=simplemod,type=span] +---- + +.`bmod.sail` +[source,sail] +---- +include::sail:BRAVO[from=simplemod,type=span] +---- +We can use the following rigging file: + +.`simple_mod.rigging` +[source] +---- +include::../examples/simple_mod.rigging[] +---- +This file defines two modules `A` and `B`, with module `A` containing +the file `amod.sail` and module B containing the file `bmod.sail`. +Module `B` requires module `A`, so it can use the `alfa` function +defined in `A`. What would happen if we removed the requires line? We +would get the following error: + +[source] +---- +include::module_sail_doc/simple_mod_err.error[] +---- + +This error tells us that `alfa` is not in scope, but Sail knows it +exists as it has already checked module `A`, so it points us at the +definition and suggests how we could resolve the error by adding the +requires line we just removed. + +When using a rigging file we do not have to pass all the files on the +command line, so we can invoke Sail simply as + +[source,shell] +---- +sail simple_mod.rigging +---- + +and it will know where to find `amod.sail` and `bmod.sail` relative to +the location of the rigging file. + +A module can have more than one Sail file. These files are processed +sequentially in the order they are listed. This is exactly like what +happens when we pass multiple Sail files on the command line without a +rigging file to define the module structure. A module can therefore be +thought of as a sequence of Sail files that is treated as a single +logical unit. As an example, we could add a third module to our above +file, which is comprised of three Sail files and depends on A and B. + +[source] +---- +C { + requires A, B + files + foo.sail, + bar.sail, + baz.sail +} +---- + +Note that comments and trailing commas are allowed, and we could optionally delimit +the lists using `[` and `]`, like so: + +[source] +---- +C { + // Require both our previous modules + requires [A, B] + /* Both types of Sail comments are allowed! */ + files [ + foo.sail, + bar.sail, + baz.sail, + ] +} +---- + +If we wanted to we could define `C` in a separate file, rather than +adding it to our previous file, and pass multiple rigging files to +Sail like so: + +[source,shell] +---- +sail simple_mod.rigging new_file_with_C.rigging +---- + +These will be treated together as a single large rigging file. A use +case might be if you were defining an out-of-tree extension `Xfoo` for +sail-riscv, you could do something like: + +[source,shell] +---- +sail sail-riscv/riscv.rigging src/Xfoo.rigging +---- + +and the modules you define in `Xfoo.rigging` can require modules from +`riscv.rigging` (and technically also vice-versa, although it makes +less sense in this example). + +=== Working with Makefiles + +The `-list_files` option can be used to list all the files within a +rigging file, which allows them to be used in a Makefile prerequisite. +As an example, to build the module examples in this very manual, we +use the rule below to generate documentation indexes (which our +Asciidoctor plugin consumes) for every `.sail` file within a rigging +file. + +[%nowrap,make] +---- +.SECONDEXPANSION: + +module_sail_doc/%.json: ../examples/%.rigging $$(shell sail ../examples/%.rigging -list_files) + mkdir -p module_sail_doc + sail -doc $(addprefix -doc_file ,$(shell sail $< -list_files)) -doc_embed plain -doc_bundle $(notdir $@) -o module_sail_doc $< +---- + +=== Conditional compilation within modules + +We can use _variables_ in our rigging files to control either file +inclusion within a module or to control whether a module requires +another or not. A variable can even contain a sequence of modules, +that can then be used in a require statement, as shown in the +following example: + +[source] +---- +include::module_sail_doc/cond.rigging[] +---- + +=== Optional and default modules + +Modules can be marked as either `optional` or `default`. Default +modules are those that form the base part of a specification, whereas +optional modules are intended to implement extensions which may or may +not be present. Default modules cannot require optional modules. diff --git a/doc/asciidoc/parser.sed b/doc/asciidoc/parser.sed new file mode 100644 index 000000000..88b328790 --- /dev/null +++ b/doc/asciidoc/parser.sed @@ -0,0 +1,121 @@ +/Assert/d +/Exit/d +/Configuration/d +/Eof/d +/Real/d +/Internal/d +/Newtype/d +/Outcome/d +/Doc/d +/Cast/d +/Mutual/d +/Impl/d +/LcurlyBar/d + +s/Pragma/$LINE_DIRECTIVE/g +s/Fixity/FIXITY_DEF/g +s/Overload/overload/g +s/Clause/clause/g +s/Forwards/forwards/g +s/Backwards/backwards/g +s/End/end/g +s/Default/default/g +s/Scattered/scattered/g +s/Monadic/monadic/g +s/Typedef/type/g +s/Enum/enum/g +s/With/with/g +s/Union/union/g +s/Bitfield/bitfield/g +s/Function_/function/g +s/Mapping/mapping/g +s/TYPE/Type/g +s/TyVar/TYPE_VARIABLE/g +s/And/and/g +s/As/as/g +s/Attribute/$[ATTRIBUTE]/g +s/Bidir/<->/g +s/Forall/forall/g +s/Bitzero/bitzero/g +s/Bitone/bitone/g +s/Effect/effect/g +s/Constant/constant/g +s/Struct/struct/g +s/Bin/BINARY_LITERAL/g +s/Hex/HEXADECIMAL_LITERAL/g +s/String/STRING_LITERAL/g +s/Unit/()/g +s/Undefined/undefined/g +s/Sizeof/sizeof/g +s/Constraint/constraint/g +s/Let_/let/g +s/True/true/g +s/False/false/g +s/Ref/ref/g +s/Foreach/foreach/g +s/Repeat/repeat/g +s/While/while/g +s/Until/until/g +s/Try/try/g +s/Throw/throw/g +s/Catch/catch/g +s/Return/return/g +s/Sizeof/sizeof/g +s/Constraint/constraint/g +s/Configuration/configuration/g +s/TerminationMeasure/termination_measure/g +s/Register/register/g +s/Match/match/g +s/Comma/,/g +s/Under/_/g +s/LsquareBar/[|/g +s/RsquareBar/|]/g +s/Lparen/(/g +s/Rparen/)/g +s/Lcurly/{/g +s/Rcurly/}/g +s/Lsquare/[/g +s/Rsquare/]/g +s/By/by/g +s/If_/if/g +s/Then/then/g +s/Else/else/g +s/Semi/;/g +s/At/@/g +s/TwoCaret/2^/g +s/Caret/^/g +s/Dot/./g +s/Do/do/g +s/OpId/OPERATOR/g +s/Id/ID/g +s/Op/operator/g +s/Colon/:/g +s/Minus/-/g +s/Gt/>/g +s/Lt///g +s///g + +/effect /d +/ match /d +/register /d +//d +/ : -> /d + +s///g +s///g diff --git a/doc/asciidoc/riscv.adoc b/doc/asciidoc/riscv.adoc index 3cb32eae1..6d5c254c8 100644 --- a/doc/asciidoc/riscv.adoc +++ b/doc/asciidoc/riscv.adoc @@ -2,7 +2,7 @@ We introduce the basic features of Sail via a small example from our RISC-V model that includes just two instructions: add immediate and -load double. We start by defining the default order (see \ref{sec:vec} +load double. We start by defining the default order (see <> for details), and including the Sail prelude: sail::PREAMBLE[from=riscv-code,type=span,trim] diff --git a/doc/asciidoc/usage.adoc b/doc/asciidoc/usage.adoc index 41a0a5023..57145d98d 100644 --- a/doc/asciidoc/usage.adoc +++ b/doc/asciidoc/usage.adoc @@ -19,8 +19,8 @@ and `riscv_vmem.sail` describe the physical and virtual memory interaction, and then `riscv_sys.sail` and `riscv.sail` implement most of the specification. -For more complex projects, one can use `$include` statements in -Sail source, for example: +One can use also use `$include` directives in Sail source, for +example: [source,sail] ---- $include @@ -35,9 +35,23 @@ file containing the `$include`. The space after the `$include` before the filename is mandatory. Sail also supports `$define`, `$ifdef`, and `$ifndef` for basic conditional compilation. These are things that are understood by Sail itself, not a separate preprocessor, and are -handled after the AST is parsed{blank}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.]. +handled after the AST is parsed. + +For more complex projects, a module hierarchy can be defined. See the +<> section for details. + +=== Sail options + +For command line arguments, by default Sail accepts arguments of +the form `‑long_opt`, i.e. leading with a single `-` and words +separated by `_`. For those who find this departure from standard +convention distasteful, you can define the `SAIL_NEW_CLI` environment +variable, and all such options will be formatted as +`‑‑long‑opt` (short opts like `‑o` will remain +unchanged). For backwards compatibility reasons, this default is hard +to change. + +For a list of all options, one can call Sail as `sail -help`. <<< === C compilation @@ -72,12 +86,50 @@ There are several Sail options that affect the C output: * `-c_include` Supply additional header files to be included in the generated C. - + * `-c_no_main` Do not generate a `main()` function. * `-static` Mark generated C functions as static where possible. This is useful for measuring code coverage. +<<< +=== SystemVerilog compilation (Experimental) + +CAUTION: This feature is new and experimental, so it is not guaranteed +to provide working SystemVerilog. Furthermore, it is intended for +hardware model checking against a hand-written design. Sail is not a +hardware description language! + +To compile Sail into SystemVerilog, the `-sv` option is used. The `-o` +option provides a prefix that is used on the various generated files. + +There are several options for the SystemVerilog output: + +* `-sv_output_dir` Generate all files in the specified directory + +* `-sv_include` Add an include directive to the generated SystemVerilog + +* `-sv_verilate` Can be used as either `-sv_verilate run` or + `-sv_verilate compile`. If used Sail will automatically invoke + https://www.veripool.org/verilator/[verilator] on the generated + SystemVerilog + + +* `-sv_lines` Output SystemVerilog `line directives to aid debugging. + +* `-sv_int_size` Set the maximum integer size allowed in the specification. + +* `-sv_bits_size` Bound the maximum bitvector width on the generated SystemVerilog. + +* `-sv_specialize` The `-sv_specialize n` option will perform `n` + rounds of specialisation on the Sail code before generating + SystemVerilog. This will make bitvectors more monomorphic, but at + the cost of code duplication. + +The are various other options that control various minutae about the +generated SystemVerilog, see `sail -help` for more details. + + <<< === Automatic formatting (Experimental) diff --git a/doc/examples/amod.sail b/doc/examples/amod.sail new file mode 100644 index 000000000..3288c2030 --- /dev/null +++ b/doc/examples/amod.sail @@ -0,0 +1,9 @@ +default Order dec + +$include + +$span start ALFA +val alfa : unit -> int + +function alfa() = 3 +$span end diff --git a/doc/examples/bitfield.sail b/doc/examples/bitfield.sail index 6729bc5dd..cda66b0eb 100644 --- a/doc/examples/bitfield.sail +++ b/doc/examples/bitfield.sail @@ -1,8 +1,67 @@ -bitfield cr : bitvector(8,dec) = { +default Order dec + +$include + +$span start BITFIELD + +bitfield cr_type : bits(8) = { CR0 : 7 .. 4, LT : 7, GT : 6, CR1 : 3 .. 2, CR3 : 1 .. 0 } -register CR : cr + +register CR : cr_type + +$span end + +val bitfield_access_example : unit -> unit + +function bitfield_access_example() = { + // Rather than using numeric indices, the bitfield names are used + let cr0_field : bits(4) = CR[CR0]; + + // Bitfield accessors always return bitvector results + let lt_field : bits(1) = CR[LT]; // Note 'bits(1)' not 'bit' + + // Can access the underlying bitvector using the bits field + let some_bits : bits(7) = CR.bits[6 .. 0]; +} + +val bitfield_update_example : unit -> unit + +function bitfield_update_example() = { + // We can set fields on the CR register using their field names + CR[CR3] = 0b01; + + // If we want to set the underlying bits + CR.bits[1 .. 0] = 0b01; + + // We can even use vector update notation! + CR = [CR with CR3 = 0b01, LT = 0b1]; + + // Because of the representation, we could set the whole thing like: + CR = (struct { bits = 0x00 } : cr_type); +} + +val legacy_bitfields : unit -> unit + +function legacy_bitfields() = { + // Assigning to a field of a bitfield register + CR->CR3() = 0b01; + // '->' notation just means the setter takes the register by reference: + (ref CR).CR3() = 0b01; + + // Assigning all the bits (now just 'CR.bits = 0x00') + CR->bits() = 0x00; + + // Accessing a field + let cr0_field : bits(4) = CR.CR0(); + + // Updating a field + CR = update_CR3(CR, 0b01); // now '[ CR with CR3 = 0b01 ]' + + // Construct a new CR bitfield + CR = Mk_cr_type(0x00); +} diff --git a/doc/examples/bmod.sail b/doc/examples/bmod.sail new file mode 100644 index 000000000..c74dfc92a --- /dev/null +++ b/doc/examples/bmod.sail @@ -0,0 +1,9 @@ + +$span start BRAVO +val bravo : unit -> unit + +function bravo() = { + let x = alfa(); + print_int("alfa returned: ", x) +} +$span end diff --git a/doc/examples/cond.rigging b/doc/examples/cond.rigging new file mode 100644 index 000000000..b35d6d894 --- /dev/null +++ b/doc/examples/cond.rigging @@ -0,0 +1,30 @@ +variable ARCH = A64 +variable ARCH_MODULES = if ARCH == A64 then arch64_only else [] + +arch_prelude { + files + prelude.sail, + if $ARCH == A32 then arch_xlen32.sail + else if $ARCH == A64 then [ + arch_xlen64.sail, + arch_xlen64_helpers.sail + ] else error("Invalid value for ARCH") +} + +arch64_only { + requires arch_prelude + files + instructions64.sail +} + +arch_instructions { + requires arch_prelude + files + instructions.sail +} + +arch_end { + requires arch_instructions, $ARCH_MODULES + files + end.sail +} diff --git a/doc/examples/mapping.sail b/doc/examples/mapping.sail new file mode 100644 index 000000000..1f4ad8160 --- /dev/null +++ b/doc/examples/mapping.sail @@ -0,0 +1,39 @@ +default Order dec +$include + +enum word_width = {BYTE, HALF, WORD, DOUBLE} + +val size_bits : word_width <-> bits(2) + +$span start M1 +mapping size_bits = { + BYTE <-> 0b00, + HALF <-> 0b01, + WORD <-> 0b10, + DOUBLE <-> 0b11 +} +$span end + +$span start M2 +mapping size_bits2 : word_width <-> bits(2) = { + BYTE <-> 0b00, + HALF <-> 0b01, + WORD <-> 0b10, + DOUBLE <-> 0b11 +} +$span end + +function example() -> unit = { + let width : word_width = size_bits(0b00); + let width : bits(2) = size_bits(BYTE); +} + +$span start M3 +mapping size_bits3 : word_width <-> bits(2) = { + BYTE <-> 0b00, + HALF <-> 0b01, + WORD <-> 0b10, + forwards DOUBLE => 0b11, // forwards is left-to-right + backwards 0b11 => DOUBLE, // backwards is right-to-left +} +$span end diff --git a/doc/examples/pattern_matching.sail b/doc/examples/pattern_matching.sail index 26f254ee6..6a6bc165d 100644 --- a/doc/examples/pattern_matching.sail +++ b/doc/examples/pattern_matching.sail @@ -7,7 +7,7 @@ val f : unit -> int val example : unit -> unit function example() = { - let n: int = f(); + let n : int = f(); match n { 1 => print_endline("1"), 2 => print_endline("2"), @@ -16,7 +16,7 @@ function example() = { } } -function match_switch(expression: int) -> unit = { +function match_switch(expression : int) -> unit = { match expression { 1 => print_endline("expression == 1"), 2 => { @@ -29,7 +29,7 @@ function match_switch(expression: int) -> unit = { } } -function match_bind(x: int, y: int) -> unit = { +function match_bind(x : int, y : int) -> unit = { match x + y { 1 => print_endline("x + y == 1"), z => { @@ -40,7 +40,7 @@ function match_bind(x: int, y: int) -> unit = { } } -function match_destruct(pair: (int, int)) -> unit = { +function match_destruct(pair : (int, int)) -> unit = { match pair : (int, int) { (first, second) => { // here we have split a pair into two variables first and second @@ -55,7 +55,7 @@ struct my_struct = { field2 : int, } -function match_struct(value: my_struct) -> unit = { +function match_struct(value : my_struct) -> unit = { match value { // match against literals in the struct fields struct { field1 = 0x0000, field2 = 3 } => (), @@ -68,7 +68,7 @@ function match_struct(value: my_struct) -> unit = { } } -function match_struct2(value: my_struct) -> unit = { +function match_struct2(value : my_struct) -> unit = { match value { struct { field1 = x, _ } => { print_bits("value.field1 = ", x) diff --git a/doc/examples/scattered.sail b/doc/examples/scattered.sail new file mode 100644 index 000000000..753d07ace --- /dev/null +++ b/doc/examples/scattered.sail @@ -0,0 +1,39 @@ +default Order dec + +$include + +$span start DECS +// We can declare scattered types, for either unions or enums +scattered union U + +scattered enum E + +// For scattered functions and mappings, we have to provide a type signature with val +val foo : U -> bits(64) + +scattered function foo + +val bar : E <-> string + +scattered mapping bar +$span end + +$span start CLAUSES +enum clause E = E_one + +union clause U = U_one : bits(64) + +function clause foo(U_one(x)) = x + +mapping clause bar = E_one <-> "first member of E" +$span end + +$span start ENDS +end E + +end U + +end foo + +end bar +$span end diff --git a/doc/examples/simple_mod.rigging b/doc/examples/simple_mod.rigging new file mode 100644 index 000000000..f60838ddc --- /dev/null +++ b/doc/examples/simple_mod.rigging @@ -0,0 +1,8 @@ +A { + files amod.sail +} + +B { + requires A + files bmod.sail +} diff --git a/doc/examples/simple_mod_err.rigging b/doc/examples/simple_mod_err.rigging new file mode 100644 index 000000000..e8f578eb4 --- /dev/null +++ b/doc/examples/simple_mod_err.rigging @@ -0,0 +1,7 @@ +A { + files amod.sail +} + +B { + files bmod.sail +} diff --git a/doc/examples/string.sail b/doc/examples/string.sail new file mode 100644 index 000000000..3c6857565 --- /dev/null +++ b/doc/examples/string.sail @@ -0,0 +1,19 @@ +default Order dec + +$include + +val multi_line : unit -> unit + +function multi_line() = { + print_endline("Hello, \ + World!"); + // Is equivalent to + print_endline("Hello, World!") +} + +val test : unit -> unit + +function test() = { + print_endline("\'"); + print_endline("'") +} diff --git a/doc/examples/tuples.sail b/doc/examples/tuples.sail new file mode 100644 index 000000000..ddfcb1c09 --- /dev/null +++ b/doc/examples/tuples.sail @@ -0,0 +1,21 @@ +default Order dec + +$include + +$span start TUPLES +let tuple1 : (string, int) = ("Hello, World!", 3) + +let tuple2 : (nat, nat, nat) = (1, 2, 3) +$span end + +val single_tuple_argument : ((int, int)) -> unit + +function single_tuple_argument(tuple) = { + let (x, y) = tuple; + print_int("x = ", x); + print_int("y = ", y); +} + +function caller() -> unit = { + single_tuple_argument((1, 2)) +} \ No newline at end of file diff --git a/doc/tutorial.tex b/doc/tutorial.tex index 1d66a02de..947d0c7c6 100644 --- a/doc/tutorial.tex +++ b/doc/tutorial.tex @@ -790,7 +790,17 @@ \subsubsection{Bitfields} The following example creates a bitfield type called \ll{cr} and a register \ll{CR} of that type. -\lstinputlisting{examples/bitfield.sail} +\begin{lstlisting} +bitfield cr : bitvector(8,dec) = { + CR0 : 7 .. 4, + LT : 7, + GT : 6, + CR1 : 3 .. 2, + CR3 : 1 .. 0 +} + +register CR : cr +\end{lstlisting} A bitfield definition creates a wrapper around a bit vector type, and generates getters and setters for the fields. For the setters, it is diff --git a/src/sail_doc_backend/docinfo.ml b/src/sail_doc_backend/docinfo.ml index 6988a9f9d..2f04b397a 100644 --- a/src/sail_doc_backend/docinfo.ml +++ b/src/sail_doc_backend/docinfo.ml @@ -677,6 +677,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct | DEF_pragma ("span", arg, _) when arg = "end" -> begin match !current_span with | Some (name, start_l) -> + current_span := None; let end_l = def_annot.loc in begin match (Reporting.simp_loc start_l, Reporting.simp_loc end_l) with