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:
Functions may also have implicit parameters, e.g. we can implement a zero extension function that implicitly picks up its result length from the calling context as follows:
Sail will also ensure that the output of our function has precisely the length bits('n * 'm) for all possible inputs (hence why the keyword uses the mathematical forall quantifier).
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 therefore be a bitvector of length 'n * 'm . We can also add constraints on these types. Here we require that we are replicating the input bitvector at least once with the 'n >= 1 constraint, and that the input bitvector length is at least one with the 'm >= 1 constraint. Sail will check that all callers of this function are guaranteed to satisfy these constraints.
This signature shows how Sail can track the length of bitvectors and the value of integer variables in type signatures, using type variables. Type variables are written with a leading 'tick', so 'n and 'm are the type variables in the above signature.
In Sail, we often define functions in two parts. First we can write the type signature for the function using the val keyword, then define the body of the function using the function keyword. In this Subsection, we will write our own version of the replicate_bits function from the Sail library. This function takes a number n and a bitvector, and creates a new bitvector containing that bitvector copied n times.
You may have noticed that in the definition of my_replicate_bits above, there was no return keyword. This is because unlike languages such as C and C++, and more similar to languages like OCaml and Rust, everything in Sail is an expression which evaluates to a value. A block in Sail is simply a sequence of expressions surrounded by curly braces { and } , and separated by semicolons. The value returned by a block is the value returned by the last expressions, and likewise the type of a block is determined by it’s final expressions, so { A; B; C } , will evaluate to the value of C after evaluating A and B in order. The expressions other than the final expression in the block must have type unit , which is discussed in the following section. Within blocks we can declare immutable variables using let , and mutable variables using var , for example:
The wikipedia page for the unit type , goes into further details on the difference between unit and void.
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 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 Tuples ).
In addition, we can write a numeric type that only contains a fixed set of integers. The type {32, 64} is a type that can only contain the values 32 and 64 .
Note that bit isn’t a numeric type (i.e. it’s not range(0, 1) ). This is intentional, as otherwise it would be possible to write expressions like (1 : bit) + 5 which would end up being equivalent to 6 : range(5, 6) . This kind of implicit casting from bits to other numeric types would be highly undesirable. The bit type itself is a two-element type with members bitzero and bitone .
Sail has three basic numeric types, int , nat , and range . The type int which we have already seen above is an arbitrary precision mathematical integer. Likewise, nat is an arbitrary precision natural number. The type range('n, 'm) is an inclusive range between type variables 'n and 'm . For both int and nat we can specify a type variable that constrains elements of the type to be equal to the value of that type variable. In other words, the values of type int('n) are integers equal to 'n . So 5 : int(5) and similarly for any integer constant. These types can often be used interchangeably provided certain constraints are satisfied. For example, int('n) is equivalent to range('n, 'n) and range('n, 'm) can be converted into int('n) when 'n == 'm .
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.
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!
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
Sail allows two different types of bitvector orderings---increasing ( inc ) and decreasing ( dec ). These two orderings are shown for the bitvector 0b10110000 below.
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.
Bitvector literals in Sail are written as either 0x followed by a sequence of hexadecimal digits (as in 0x12FE ) or 0b followed by a sequence of binary digits (as in 0b1010100 ). The bit length of a hex literal is always four times the number of hexadecimal digits, and the bit length of binary literal is always the exact number of binary digits. So, 0x12FE has bit length 16, and 0b1010100 has bit length 7. To ensure bitvector logic in specifications is precisely 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. Underscores can be used in bitvector literals to separate groups, where each group is typically 16 bits. For example:
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.
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:
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:
A vector v can have an index index using [v with index = expression] . Similarly, a sub-range of v can be updated using [v with n .. m = expression] where the order of the indexes is the same as described above for increasing and decreasing vectors.
A vector v can be sliced using the v[n .. 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 .. 0] , and the upper 32-bits of an increasing bitvector as v[0 .. 31] , i.e. the indexing order for decreasing vectors decreases, and the indexing order for increasing vectors increases.
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.
For those unfamiliar the word, 'cons' is derived from Lisp dialects, and has become standard functional programming jargon for such an operator — see en.wikipedia.org/wiki/Cons for more details.
Note that while the function type (A, B) -> 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:
Sail has tuple types which represent heterogeneous sequences containing values of different types. A tuple type (T1, T2, …) has values (x1, x2, …) where x1 : T1 , x2 : T2 and so on. A tuple must have 2 or more elements. Some examples of tuples would be:
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:
Behind the scenes, Sail will just generate separate struct definitions, so we use this type in exactly the same was as we did previously.
In our shape example, we defined rectangle and circle as two separate structs, but if we wanted we could declare those structs inline
Constructors in Sail always have a single argument. If we want a constructor in a union type to contain no information, then we can use the unit type. For a constructor with multiple arguments we can use a tuple type. We provide some syntax sugar that allows writing constructor applications with either tuple or unit argument types as if they were functions with multiple arguments or no arguments respectively.
To destructure unions, we typically use pattern matching to handle each case in the union separately. This will be discussed in detail in Pattern matching .
This defines a type with two constructors Rectangle and Circle . Constructors are used like functions with a single argument, as so:
defines a type rectangle that has both a width and a height. The other logical way to combine data is if we want to say we have some data or some other data, like if we wanted to represent a shape that could be a circle or a rectangle. In Sail, we use a union for this.
If the names of the generated functions are not ideal, then custom names can be provided using the enum_number_conversions attribute.
This style is better when the enumeration is short and has few constructors, however specification authors may prefer to use the first style exclusively for consistency.
The above style is best when there are a lot of elements in the enumeration. We allow enums to be defined in a style similar to Haskell, where the identifiers are separated by a vertical bar | character, like so:
Sail enumerations are also much like their C counterparts. An enum is declared using the enum keyword followed by the name of the enumeration type. The members of the enumeration are specified as a comma-separated list of identifiers between curly braces, like so:
The struct can then be instantiated with any length of bitvector for the a_bitvector field, and any data type for the something field, including another struct like the My_struct type we defined earlier.
We can then construct struct values by using the struct keyword and providing values for all the fields. The individual fields can be accessed using the . operator. If the struct is mutable, we can also the . operator on the left-hand side of an assignment to assign to the struct field. For immutable structs, we can update them using the with keyword, which will create a new struct value with some fields changed.
The following example struct defines three fields. The first contains a bitvector of length 5 and is called field1 . The second, field2 contains an integer. The third, field3 contains a string.
Like in C, structs are used to hold multiple values. Structs are created using the struct keyword followed by the name of the struct. The data the struct contains is then defined following the = symbol. Each piece of data stored in a struct is called a field , and each is given a unique name that identifies that piece of data, and can have a different type.
Type synonyms are completely transparent to the Sail type-checker, so a type synonym can be used exactly the same as the original type.
Sail types also include numbers, as in bits(32) above. We can therefore write a type synonym for just such a number:
For example, if we have an architecture with 32 general purpose registers, we might want to index them using a 5-bit type. Rather than using bits(5) directly, we create a synonym:
We have now described all the various types available in Sail. However, in order to create more descriptive and self-documenting specifications, we might want to give types new names that better inform the reader of the intent behind the types. We can do this using type synonyms, which are created with the type keyword.
but in practice we don’t need to do this, as Sail has kind-inference to avoid us having to think about this particular detail.
Which we could use as the type foo(32, string) , or foo(16, int) . What stops us from writing foo(string, int) or even range(int, int) or list(3) however? Those should clearly be type errors, and if they are type errors does that mean types have types? The answer to this is yes, and we call the types of types kinds. Sail has three different kinds of types, which we denote as Int , Bool , and Type . The Int kind is for type-level integers, Bool is for type-level (boolean) constraints, and Type is for ordinary types. Type constructors therefore have types much like functions, with list having the type Type → Type and range having the type (Int, Int) → Type .
Throughout the previous section we have seen many different types. For example we could have a type like list(int) , or a type like range(2, 5) . The range type takes two numbers as an arguments, whereas list takes a type as an argument. We’ve also seen polymorphic user-defined types like:
This warning should be heeded, and the match simplified otherwise the generated theorem prover definitions produced by Sail may be rejected by the prover.
Here the 0b1 literal in the (Some(0b1), _) case would need to be replaced for an exhaustiveness checker without bitvector literals to check the case where x and y are both Some , but this would change the behavior when x is Some and y is None , hence a wildcard cannot be inserted.
Most targets that check pattern exhaustiveness share the same limitation as Sail — they only check match arms without guards, so they would not see that this match is complete. To avoid this, Sail will attempt to replace literal patterns with wildcards when possible, so the above will be rewritten to:
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:
The as pattern has lower precedence than any other keyword or operator in a pattern, so in this example the pattern brackets as (x :: xs) as zs
Like OCaml, Sail also supports naming parts of patterns using the as keyword. For example, in the above cons pattern example we could bind the entire matched list to the zs variable:
Finally, if we want to create a variable with the same name as a field, rather than typing struct { field_name = field_name, _ } , we can shorten this to just struct { field_name, _ } , So the above example is equivalent to:
We can omit fields from the match by using a wildcard _ in place of some of the fields:
Sail allows lists to be destructured using patterns. There are two types of patterns for lists, cons patterns and list literal patterns. The cons pattern destructures lists into the first element (the head) and the rest of the list (the tail).
Note that like how calling a function with a unit argument can be done as f() rather than f(()) , matching on a constructor C with a unit type can be achieved by using C() rather than C(()) .
Match can also be used to destructure tagged union constructors, for example using the option type from the Sail library.
Note that because Sail places no restrictions on the lexical structure of enumeration elements to differentiate them from ordinary identifiers, pattern matches on variables and enum elements can be somewhat ambiguous. Issues with this are usually caught by the exhaustiveness checker — it can warn you if removing an enum constructor breaks a pattern match.
Match can be used to match on possible values of an enum, like so:
First, and as we have already seen, we can match on literal values. These literal values can be () , bitvectors, the boolean values true and false , numbers, and strings.
You may wonder — why not write z if z < 0 for the final case? Here we run into one of the limitations of the exhaustiveness checker mentioned above. Sail can only check the exhaustiveness of unguarded clauses, meaning that the checker only considers cases without an if guard. The z pattern by itself is exhaustive, so the checker is happy, but if we added a if z < 0 guard the checker would complain that there are no unguarded patterns for it to look at. This may seem suprising for such a simple case (we can easily see the three guards would cover all cases!), however each guard clause could contain arbitrarily complex logic potentially abstracted behind arbitrary function calls, which the completeness checker cannot reason about.
What if we need to switch based on more complex logic than just the structure and values of the expressions we are matching on? For this matches in Sail support guards. A guard allows us to combine the behavior of a match expression and the boolean logic of an if expression — and the syntax is reflective of this, as we can use the if keyword to add extra logic to each match arm:
Sail will check match statements for exhaustiveness (meaning that the patterns in the match cover every possible value), and prints a warning if the overall match statement is not exhaustive. There are some limitations on the exhaustiveness checker which we will discuss further below.
These features can be combined, so if we had a pattern (first, 3) in the above example, the expression for that pattern would be executed when the second element of the pair is equal to 3, and the first element would be bound to the variable first .
Finally, we can use patterns to destructure values — breaking them apart into their constituent parts. For example if we have a pair expression we can break it apart into the first value in the pair and the second, which can then be used as individual variables:
However the pattern in a match statement can also bind variables. In the following example we match on a numeric expression x + y , and if it is equal to 1 we execute the first match arm. However, if that is not the case the value of x + y is bound to a new immutable variable z .
The concrete match statement syntax in Sail is inspired by the syntax used in Rust — but programmers coming from languages with no pattern matching features may be unfamiliar with the concept. One can think of the match statement like a super-powered switch statement in C. At its most basic level a match statement can function like a switch statement (except without any fall-through). As in the above example we can use match to compare an expression against a sequence of values like so:
The match keyword takes an expression and then branches by comparing the matched value with a pattern. Each case in the match expression takes the form => , separated by commas (a trailing comma is allowed). The cases are checked sequentially from top to bottom, and when the first pattern matches its expression will be evaluated.
Like most functional languages, and an increasing number of imperative languages like Rust, Sail supports pattern matching via the match keyword. For example:
The match statement isn’t the only place we can use patterns. We can also use patterns in function arguments and with let , for example:
Here we can use xlen within the function as both a regular variable xlen and as a type variable 'xlen .
If we want to give the variable xlen and the type variable 'n the same name, we could go further and simplify to:
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:
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.
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:
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 .
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:
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.
This functions identically, just without the keyword. We consider this deprecated and strongly encourage the use of the var keyword going forwards.
Technically, unless the --strict-var option is used Sail also allows mutable variables to be implicitly declared, like so:
Bindings made using let are always immutable, but Sail also allows mutable variables. Mutable variables are created by using the var keyword within a block.
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) = data and read memory as data = memory(addr) , for example:
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:
It is common in ISA specifications to assign to complex l-values, e.g. to a subvector or named field of a bitvector register, or to an l-value computed with some auxiliary function, e.g. to select the appropriate register for the current execution model.
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.
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:
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:
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:
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.
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.
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.
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:
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:
Ad-hoc overloading
Sail has a flexible overloading mechanism using the overload keyword. For example:
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:
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' definitions 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.
val print_int : int -> unit val print_string : string -> unit overload print = { print_int , print_string } function main () : unit -> unit = { print ( "Hello, World!" ); print ( 4 ) }
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
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:
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
overload operator / = { div1 , div2 }