Sail Desc
References:
Sail is a domain specific imperative language designed for describing processor architectures.
Sail in RISC-V instr. descriptions
Constant Definitions
Constants for 64-bit ISA with 128 bit capability:
type xlen : Int = 64
type cap_addr_width : Int = xlen
type cap_len_width : Int = cap_addr_width + 1
type cap_size : Int = 16
type cap_mantissa_width : Int = 14
type cap_hperms_width : Int = 12
type cap_uperms_width : Int = 4
type cap_uperms_shift : Int = 15
type cap_flags_width : Int = 1
type cap_otype_width : Int = 18
let cap_max_otype = MAX(cap_otype_width) - reserved_otypesFunction Definitions
Functions for integer and bit vector manipulation
func 1:
unsigned : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
This converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$.
func 2:
signed : forall ’n, ’n > 0. bits(’n) -> range(- (2 ^ (’n - 1)), 2 ^ (’n - 1) - 1)
This converts a bit vector of length $n$ to an integer in the range $-2^{n-1}$ to $2^{n-1} - 1$ using twos-complement.
func 3:
to_bits : forall ’l, ’l >= 0. (int(’l), int) -> bits(’l)
func 4⁄5:
bool_to_bit : bool -> bit
bool_to_bits : bool -> bits(1)
func 6:
truncate : forall 'm 'n, ('m >= 0 & 'm <= 'n). (bits('n), int('m)) -> bits('m)
truncate(v,n) truncates v, keeping only the least significant n bits.
func 7:
pow2 : forall 'n. int('n) -> int(2^'n)
func 8⁄9:
EXTZ: Addes zeros in most significant bits of vector to obtain a vector of desired length.
EXTS: Extends the most significant bits of vector preserving the sign bit.
func 10⁄11:
zeros: Produces a bit vector of all zeros
ones: Produces a bit vector of all ones
Types used in function defs
Source code, common Source code, rv64
type CapBits = bits(8 * cap_size)
type CapAddrBits = bits(cap_addr_width)
type CapLenBits = bits(cap_len_width)
type CapPermsBits = bits(cap_perms_width)
struct Capability = {...}
Functions to convert Compressed Cap
capBitsToCapability : (bool, CapBits) -> Capability
capToBits : Capability -> CapBits
Functions for reading and writing regs and mem
C(n) : regno -> Capability
C(n) : (regno, Capability) -> unit
The overloaded function C(n) is used to read or write capability register n.
X(n) : regno -> xlenbits
X(n) : (regno, xlenbits) -> unit
The overloaded function X(n) is used to read or write integer register n.
F(n) : regno -> xlenbits
F(n) : (regno, xlenbits) -> unit
The overloaded function F(n) is used to read or write floating-point register n.
memBitsToCapability : (bool, CapBits) -> Capability
capToMemBits : Capability -> CapBits
int_to_cap : CapAddrBits -> Capability
get_cheri_mode_cap_addr : (regidx, xlenbits) -> (Capability, xlenbits, capreg_idx)
handle_load_cap_via_cap : (regidx, capreg_idx, Capability, xlenbits) -> Retired
handle_load_data_via_cap : (regidx, capreg_idx, Capability, xlenbits, bool, word_width) -> Retired
handle_store_cap_via_cap : (regidx, capreg_idx, Capability, xlenbits) -> Retired
handle_store_data_via_cap : (regidx, capreg_idx, Capability, xlenbits, word_width) ->
Retired
Functions for ISA exception behavior
handle_exception : ExceptionType -> unit
handle_illegal : unit -> unit
handle_mem_exception : (xlenbits, ExceptionType) -> unit
handle_cheri_cap_exception : (CapEx, capreg_idx) -> unit
handle_cheri_reg_exception : (CapEx, regidx) -> unit
/* Is as `handle_cheri_cap_exception` except that the capability register number uses the special value 0x10 indicating the PCC register. */
handle_cheri_pcc_exception : CapEx -> unit
pcc_access_system_regs : unit -> bool
privLevel_to_bits : Privilege -> priv_level
min_instruction_bytes : unit -> CapAddrInt
legalize_epcc : Capability -> Capability
legalize_tcc : (Capability, Capability) -> Capability
Functions for Manipulating Capabilities
The address of a capability has a range as below (the base is the first byte of the range, and top is one greater than last byte):
{ $a\in N | base \le a \lt top$ }
Note: for 64-bit arch, the top can be $2^{64}$, meaning that the entire 64-bit address space can be addressed.
getCapBounds : Capability -> (CapAddrInt, CapLen) /* return base and top */
getCapBaseBits : Capability -> CapAddrBits
getCapTop : Capability -> CapLen
getCapLength : Capability -> CapLen
inCapBounds : (Capability, CapAddrBits, CapLen) -> bool /* check addr and addr+size is in Cap */
cursor: the Capability’s address;
offset: relative to base.
$base + offset$ $mod$ $2^{64}$ = $cursor$
getCapCursor : Capability -> CapAddrInt
getCapOffsetBits : Capability -> CapAddrBits
Adjust the bounds and offsets of capabilities. Not all combinations of bounds and offset are representable, so these functions return a boolean value indicating whether the requested operation was successfull. Even in the case of failure a capability is still returned, although it may not preserve the bounds of the original capability.
setCapBounds : (Capability, CapAddrBits, CapLenBits) -> (bool, Capability)
setCapAddr : (Capability, CapAddrBits) -> (bool, Capability)
setCapOffset : (Capability, CapAddrBits) -> (bool, Capability)
incCapOffset : (Capability, CapAddrBits) -> (bool, Capability)
Adjust the tag:
clearTag : Capability -> Capability
clearTagIf : (Capability, bool) -> Capability
clearTagIfSealed : Capability -> Capability
About the compression ability:
getRepresentableAlignmentMask : xlenbits -> xlenbits
getRepresentableLength : xlenbits -> xlenbits
Operation on sealing:
sealCap : (Capability, bits(cap_otype_width)) -> Capability
unsealCap : Capability -> Capability
isCapSealed : Capability -> bool
Operation on Object Types:
hasReservedOType : Capability -> bool
Operations on permissions and flags:
getCapPerms : Capability -> CapPermsBits
setCapPerms : (Capability, CapPermsBits) -> Capability
/*
* Get the architecture specific capability flags for given capability.
*/
getCapFlags : Capability -> CapFlagsBits
/*
* setCapFlags(cap, flags):
* Set the architecture specific capability flags on `cap` to `flags`
* and returns the result as new capability.
*/
setCapFlags : (Capability, CapFlagsBits) -> Capability
Checking ISA features
haveRVC : unit -> bool
haveFExt : unit -> bool
haveNExt : unit -> bool
haveSupMode : unit -> bool
Instruction Definitions
Instructions dependent on encoding modes
More
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?