Created
February 19, 2025 21:54
-
-
Save arichardson/a10e2188ba0b88739e546eab3b2be2ef to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| diff --git a/sail_latex_riscv/commands.tex b/sail_latex_riscv/commands.tex | |
| index 80a14033..6ddc4805 100644 | |
| --- a/sail_latex_riscv/commands.tex | |
| +++ b/sail_latex_riscv/commands.tex | |
| @@ -33,8 +33,7 @@ | |
| \newcommand{\sailRISCVvalundefinedUnit}{\saildoclabelled{sailRISCVzundefinedzyunit}{\saildocval{}{\lstinputlisting[language=sail]{sail_latex_riscv/valzundefined_unitd751910db26c6cf7ec5d02a503ad4f9e.tex}}}} | |
| -\newcommand{\sailRISCVvaledivInt}{\saildoclabelled{sailRISCVzedivzyint}{\saildocval{ Euclidean division | |
| - | |
| +\newcommand{\sailRISCVvaledivInt}{\saildoclabelled{sailRISCVzedivzyint}{\saildocval{Euclidean division | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzediv_int5aaf4d3d5a3d15a7aebaf90d3bfb6650.tex}}}} | |
| \newcommand{\sailRISCVvalemodInt}{\saildoclabelled{sailRISCVzemodzyint}{\saildocval{}{\lstinputlisting[language=sail]{sail_latex_riscv/valzemod_int8e3d74b3b6a72e24e6bd03570d8e21ba.tex}}}} | |
| @@ -141,12 +140,13 @@ | |
| \newcommand{\sailRISCVvalprerrInt}{\saildoclabelled{sailRISCVzprerrzyint}{\saildocval{}{\lstinputlisting[language=sail]{sail_latex_riscv/valzprerr_int00b48f715fbb32df5901801dff63b643.tex}}}} | |
| -\newcommand{\sailRISCVvalpowTwo}{\saildoclabelled{sailRISCVzpow2}{\saildocval{We have special support for raising values to the power of two. Any Sail expression \lstinline`2 ^ x` will be compiled to this builtin. | |
| +\newcommand{\sailRISCVvalpowTwo}{\saildoclabelled{sailRISCVzpow2}{\saildocval{ | |
| +We have special support for raising values to the power of two. Any Sail expression \lstinline`2 ^ x` will be compiled to this builtin. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzpow2e971ce2f9ebb899590551317286dfd1b.tex}}}} | |
| -\newcommand{\sailRISCVvalShlEight}{\saildoclabelled{sailRISCVzzyshl8}{\saildocval{A common idiom in asl is to take two bits of an opcode and convert in into a variable like | |
| - | |
| +\newcommand{\sailRISCVvalShlEight}{\saildoclabelled{sailRISCVzzyshl8}{\saildocval{ | |
| +A common idiom in asl is to take two bits of an opcode and convert in into a variable like | |
| \lstinputlisting[language=sail]{sail_latex_riscv/blocka2cd1c63e1ba9c2d625830f7e4de8f31.sail}\lstinline{pow2} ensures that in this case the typechecker knows that the end result will be a value in the set \lstinline`{8, 16, 32, 64}` | |
| Similarly, we define shifts of 32 and 1 (i.e., powers of two). | |
| @@ -177,16 +177,13 @@ The most general shift operations also allow negative shifts which go in the opp | |
| \newcommand{\sailRISCVoverloadAshrInt}{\saildoclabelled{sailRISCVoverloadAzshrzyint}{\saildocoverload{}{\lstinputlisting[language=sail]{sail_latex_riscv/overloadAzshr_int5f4032eb21b9c850a9e2a8de5872a2a2.tex}}}} | |
| -\newcommand{\sailRISCVvaltdivInt}{\saildoclabelled{sailRISCVztdivzyint}{\saildocval{ Truncating division (rounds towards zero) | |
| - | |
| +\newcommand{\sailRISCVvaltdivInt}{\saildoclabelled{sailRISCVztdivzyint}{\saildocval{Truncating division (rounds towards zero) | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valztdiv_int5e119ac7ab9ff04c8877846f345d1159.tex}}}} | |
| -\newcommand{\sailRISCVvalTmodInt}{\saildoclabelled{sailRISCVzzytmodzyint}{\saildocval{ Remainder for truncating division (has sign of dividend) | |
| - | |
| +\newcommand{\sailRISCVvalTmodInt}{\saildoclabelled{sailRISCVzzytmodzyint}{\saildocval{Remainder for truncating division (has sign of dividend) | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valz_tmod_inta2984ba6dbfa10758476d9b3b7f62560.tex}}}} | |
| -\newcommand{\sailRISCVvalTmodIntPositive}{\saildoclabelled{sailRISCVzzytmodzyintzypositive}{\saildocval{ If we know the second argument is positive, we know the result is positive | |
| - | |
| +\newcommand{\sailRISCVvalTmodIntPositive}{\saildoclabelled{sailRISCVzzytmodzyintzypositive}{\saildocval{If we know the second argument is positive, we know the result is positive | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valz_tmod_int_positive6f0621d972182279e90a43c082e50c10.tex}}}} | |
| \newcommand{\sailRISCVoverloadAtmodInt}{\saildoclabelled{sailRISCVoverloadAztmodzyint}{\saildocoverload{}{\lstinputlisting[language=sail]{sail_latex_riscv/overloadAztmod_int76b131b53b88df8b201279295eacebbe.tex}}}} | |
| @@ -251,7 +248,8 @@ The most general shift operations also allow negative shifts which go in the opp | |
| \newcommand{\sailRISCVfnnLeadingSpaces}{\saildoclabelled{sailRISCVfnznzyleadingzyspaces}{\saildocfn{}{\lstinputlisting[language=sail]{sail_latex_riscv/fnzn_leading_spaces05ea6c2f03435a60412f4bef062a912a.tex}}}} | |
| -\newcommand{\sailRISCVvalspc}{\saildoclabelled{sailRISCVzspc}{\saildocval{In a string mapping this is treated as \lstinline`[ ]+`, i.e one or more space | |
| +\newcommand{\sailRISCVvalspc}{\saildoclabelled{sailRISCVzspc}{\saildocval{ | |
| +In a string mapping this is treated as \lstinline`[ ]+`, i.e one or more space | |
| characters. It is printed as a single space \lstinline`" "`. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzspca574d99b4c3d28e08386a1f673633994.tex}}}} | |
| @@ -264,7 +262,8 @@ characters. It is printed as a single space \lstinline`" "`. | |
| \newcommand{\sailRISCVfnspcBackwardsMatches}{\saildoclabelled{sailRISCVfnzspczybackwardszymatches}{\saildocfn{}{\lstinputlisting[language=sail]{sail_latex_riscv/fnzspc_backwards_matches6b6357587b217ae24d7055f09204bd11.tex}}}} | |
| -\newcommand{\sailRISCVvaloptSpc}{\saildoclabelled{sailRISCVzoptzyspc}{\saildocval{In a string mapping this is treated as \lstinline`[ ]*`, \saildocabbrev{i.e.} zero or more space | |
| +\newcommand{\sailRISCVvaloptSpc}{\saildoclabelled{sailRISCVzoptzyspc}{\saildocval{ | |
| +In a string mapping this is treated as \lstinline`[ ]*`, i.e. zero or more space | |
| characters. It is printed as the empty string. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzopt_spc4aab1150dfed90f36fea1776963edbf0.tex}}}} | |
| @@ -277,7 +276,8 @@ characters. It is printed as the empty string. | |
| \newcommand{\sailRISCVfnoptSpcBackwardsMatches}{\saildoclabelled{sailRISCVfnzoptzyspczybackwardszymatches}{\saildocfn{}{\lstinputlisting[language=sail]{sail_latex_riscv/fnzopt_spc_backwards_matchesbc78b9c02b7156c6cfcb17a7d5067f87.tex}}}} | |
| -\newcommand{\sailRISCVvaldefSpc}{\saildoclabelled{sailRISCVzdefzyspc}{\saildocval{Like \lstinline`opt_spc`, in a string mapping this is treated as \lstinline`[ ]*`, \saildocabbrev{i.e.} zero or more space | |
| +\newcommand{\sailRISCVvaldefSpc}{\saildoclabelled{sailRISCVzdefzyspc}{\saildocval{ | |
| +Like \lstinline`opt_spc`, in a string mapping this is treated as \lstinline`[ ]*`, i.e. zero or more space | |
| characters. It differs however in that it is printed as a single space \lstinline`" "`. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzdef_spce04ebdaa1e0acd4aa4dd3326642e673e.tex}}}} | |
| @@ -324,11 +324,13 @@ characters. It differs however in that it is printed as a single space \lstinlin | |
| \newcommand{\sailRISCVvalsailZeroExtend}{\saildoclabelled{sailRISCVzsailzyzzerozyextend}{\saildocval{}{\lstinputlisting[language=sail]{sail_latex_riscv/valzsail_zzero_extend411875c18d3b332113845d17151890c2.tex}}}} | |
| -\newcommand{\sailRISCVvaltruncate}{\saildoclabelled{sailRISCVztruncate}{\saildocval{\lstinline{sail_zero_extend}\lstinline`(v, n)` truncates \lstinline`v`, keeping only the \emph{least} significant \lstinline`n` bits. | |
| +\newcommand{\sailRISCVvaltruncate}{\saildoclabelled{sailRISCVztruncate}{\saildocval{ | |
| +\lstinline{sail_zero_extend}\lstinline`(v, n)` truncates \lstinline`v`, keeping only the \emph{least} significant \lstinline`n` bits. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valztruncatea666e28ae0c8ca7327a2b3fcd1ed4ec7.tex}}}} | |
| -\newcommand{\sailRISCVvaltruncateLSB}{\saildoclabelled{sailRISCVztruncateLSB}{\saildocval{\lstinline{truncate}\lstinline`(v, n)` truncates \lstinline`v`, keeping only the \emph{most} significant \lstinline`n` bits. | |
| +\newcommand{\sailRISCVvaltruncateLSB}{\saildoclabelled{sailRISCVztruncateLSB}{\saildocval{ | |
| +\lstinline{truncate}\lstinline`(v, n)` truncates \lstinline`v`, keeping only the \emph{most} significant \lstinline`n` bits. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valztruncatelsb4d124c6ec672453343dc0b20d295e82d.tex}}}} | |
| @@ -410,11 +412,13 @@ characters. It differs however in that it is printed as a single space \lstinlin | |
| \newcommand{\sailRISCVvalsetSliceBits}{\saildoclabelled{sailRISCVzsetzyslicezybits}{\saildocval{}{\lstinputlisting[language=sail]{sail_latex_riscv/valzset_slice_bits5956200094c551f35973411fcc90a521.tex}}}} | |
| -\newcommand{\sailRISCVvalunsigned}{\saildoclabelled{sailRISCVzunsigned}{\saildocval{converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$. | |
| +\newcommand{\sailRISCVvalunsigned}{\saildoclabelled{sailRISCVzunsigned}{\saildocval{ | |
| +converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzunsigned1010eda2cdd2666cd8fd0ddf82ac526f.tex}}}} | |
| -\newcommand{\sailRISCVvalsigned}{\saildoclabelled{sailRISCVzsigned}{\saildocval{converts a bit vector of length $n$ to an integer in the range $-2^{n-1}$ to $2^{n-1} - 1$ using twos-complement. | |
| +\newcommand{\sailRISCVvalsigned}{\saildoclabelled{sailRISCVzsigned}{\saildocval{ | |
| +converts a bit vector of length $n$ to an integer in the range $-2^{n-1}$ to $2^{n-1} - 1$ using twos-complement. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzsigned36d2317f34f1dacb4e465e6e56b185e6.tex}}}} | |
| @@ -1058,7 +1062,7 @@ characters. It differs however in that it is printed as a single space \lstinlin | |
| \newcommand{\sailRISCVletcapResetT}{\saildoclabelled{sailRISCVletzcapzyresetzyT}{\saildoclet{}{\lstinputlisting[language=sail]{sail_latex_riscv/letzcap_reset_t56aac6ecd6f934ba784056463b1e3b8b.tex}}}} | |
| -\newcommand{\sailRISCVtypeCapability}{\saildoclabelled{sailRISCVtypezCapability}{\saildoctype{ A partially decompressed version of a capability -- E, B, T, | |
| +\newcommand{\sailRISCVtypeCapability}{\saildoclabelled{sailRISCVtypezCapability}{\saildoctype{A partially decompressed version of a capability -- E, B, T, | |
| lenMSB, sealed and otype fields are not present in all formats and are | |
| populated by capBitsToCapability. | |
| @@ -1122,13 +1126,15 @@ populated by capBitsToCapability. | |
| \newcommand{\sailRISCVfnsetCapPerms}{\saildoclabelled{sailRISCVfnzsetCapPerms}{\saildocfn{}{\lstinputlisting[language=sail]{sail_latex_riscv/fnzsetcappermsbb03905a9ed7e94e44018326fd80a0d0.tex}}}} | |
| -\newcommand{\sailRISCVvalgetCapFlags}{\saildoclabelled{sailRISCVzgetCapFlags}{\saildocval{Gets the architecture specific capability flags for given capability. | |
| +\newcommand{\sailRISCVvalgetCapFlags}{\saildoclabelled{sailRISCVzgetCapFlags}{\saildocval{ | |
| +Gets the architecture specific capability flags for given capability. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzgetcapflags06024d55b7e2cd94f99830e3c12d9adf.tex}}}} | |
| \newcommand{\sailRISCVfngetCapFlags}{\saildoclabelled{sailRISCVfnzgetCapFlags}{\saildocfn{}{\lstinputlisting[language=sail]{sail_latex_riscv/fnzgetcapflags06024d55b7e2cd94f99830e3c12d9adf.tex}}}} | |
| -\newcommand{\sailRISCVvalsetCapFlags}{\saildoclabelled{sailRISCVzsetCapFlags}{\saildocval{\lstinline{getCapFlags}\lstinline`(cap, flags)` sets the architecture specific capability flags on \lstinline`cap` | |
| +\newcommand{\sailRISCVvalsetCapFlags}{\saildoclabelled{sailRISCVzsetCapFlags}{\saildocval{ | |
| +\lstinline{getCapFlags}\lstinline`(cap, flags)` sets the architecture specific capability flags on \lstinline`cap` | |
| to \lstinline`flags` and returns the result as new capability. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzsetcapflags1cebd5e15eac27fc3dbd3e6dc534158a.tex}}}} | |
| @@ -1139,8 +1145,9 @@ to \lstinline`flags` and returns the result as new capability. | |
| \newcommand{\sailRISCVfnisCapSealed}{\saildoclabelled{sailRISCVfnzisCapSealed}{\saildocfn{}{\lstinputlisting[language=sail]{sail_latex_riscv/fnziscapsealeda9077bc28a9d2efcd12e42755a4de536.tex}}}} | |
| -\newcommand{\sailRISCVvalhasReservedOType}{\saildoclabelled{sailRISCVzhasReservedOType}{\saildocval{Tests whether the capability has a reserved otype (larger than \hyperref[sailRISCVzcapzymaxzyotype]{\lstinline{cap_max_otype}}). | |
| -Note that this includes both sealed (\saildocabbrev{e.g.} sentry) and unsealed (all ones) | |
| +\newcommand{\sailRISCVvalhasReservedOType}{\saildoclabelled{sailRISCVzhasReservedOType}{\saildocval{ | |
| +Tests whether the capability has a reserved otype (larger than \hyperref[sailRISCVzcapzymaxzyotype]{\lstinline{cap_max_otype}}). | |
| +Note that this includes both sealed (e.g. sentry) and unsealed (all ones) | |
| otypes. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzhasreservedotypee1cbb5365f130582a0df82f04b53cb52.tex}}}} | |
| @@ -1453,7 +1460,8 @@ otypes. | |
| \newcommand{\sailRISCVfnprivLevelToBits}{\saildoclabelled{sailRISCVfnzprivLevelzytozybits}{\saildocfn{}{\lstinputlisting[language=sail]{sail_latex_riscv/fnzprivlevel_to_bits4b6f72dec94db401093759e81957be6b.tex}}}} | |
| -\newcommand{\sailRISCVvalprivLevelOfBits}{\saildoclabelled{sailRISCVzprivLevelzyofzybits}{\saildocval{Converts the given 2-bit privilege level code to the \hyperref[sailRISCVzPrivilege]{\lstinline{Privilege}} enum. | |
| +\newcommand{\sailRISCVvalprivLevelOfBits}{\saildoclabelled{sailRISCVzprivLevelzyofzybits}{\saildocval{ | |
| +Converts the given 2-bit privilege level code to the \hyperref[sailRISCVzPrivilege]{\lstinline{Privilege}} enum. | |
| Calling with a reserved code will result in an internal error. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzprivlevel_of_bitsf8754d7aa9d9aeada7d193ecf64e148c.tex}}}} | |
| @@ -1860,7 +1868,8 @@ Calling with a reserved code will result in an internal error. | |
| \newcommand{\sailRISCVfnwordWidthBytes}{\saildoclabelled{sailRISCVfnzwordzywidthzybytes}{\saildocfn{}{\lstinputlisting[language=sail]{sail_latex_riscv/fnzword_width_bytes3499487c0f03a80d8659fa504a62261f.tex}}}} | |
| -\newcommand{\sailRISCVvalreportInvalidWidth}{\saildoclabelled{sailRISCVzreportzyinvalidzywidth}{\saildocval{Raise an internal error reporting that width w is invalid for access kind, k, | |
| +\newcommand{\sailRISCVvalreportInvalidWidth}{\saildoclabelled{sailRISCVzreportzyinvalidzywidth}{\saildocval{ | |
| +Raise an internal error reporting that width w is invalid for access kind, k, | |
| and current xlen. The file name and line number should be passed in as the | |
| first two arguments using the \textbf{FILE} and \textbf{LINE} built-in macros. | |
| This is mainly used to supress Sail warnings about incomplete matches and | |
| @@ -2939,7 +2948,8 @@ and https://github.com/riscv/sail-riscv/pull/197 . | |
| \newcommand{\sailRISCVfnextInitRegs}{\saildoclabelled{sailRISCVfnzextzyinitzyregs}{\saildocfn{}{\lstinputlisting[language=sail]{sail_latex_riscv/fnzext_init_regs1d9ff00ce58fd5712eb26190e338015a.tex}}}} | |
| -\newcommand{\sailRISCVvalextRvfiInit}{\saildoclabelled{sailRISCVzextzyrvfizyinit}{\saildocval{This function is called after above when running rvfi and allows the model | |
| +\newcommand{\sailRISCVvalextRvfiInit}{\saildoclabelled{sailRISCVzextzyrvfizyinit}{\saildocval{ | |
| +This function is called after above when running rvfi and allows the model | |
| to be initialised differently. For RVFI we initialise cap regs to default | |
| instead of null. | |
| @@ -4895,15 +4905,17 @@ instead of null. | |
| \newcommand{\sailRISCVtypeExtPhysAddrCheck}{\saildoclabelled{sailRISCVtypezExtzyPhysAddrzyCheck}{\saildoctype{}{\lstinputlisting[language=sail]{sail_latex_riscv/typezext_physaddr_checkc3760f9b4fda909a0f48ead90fcc3bf3.tex}}}} | |
| -\newcommand{\sailRISCVvalextCheckPhysMemRead}{\saildoclabelled{sailRISCVzextzycheckzyphyszymemzyread}{\saildocval{Validate a read from physical memory. | |
| -\lstinline{Ext_PhysAddr_Check}(access\_type, paddr, size, aquire, release, reserved, read\_meta) should | |
| +\newcommand{\sailRISCVvalextCheckPhysMemRead}{\saildoclabelled{sailRISCVzextzycheckzyphyszymemzyread}{\saildocval{ | |
| +Validate a read from physical memory. | |
| +\lstinline{Ext_PhysAddr_Check}(access_type, paddr, size, aquire, release, reserved, read_meta) should | |
| return Some(exception) to abort the read or None to allow it to proceed. The | |
| check is performed after PMP checks and does not apply to MMIO memory. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzext_check_phys_mem_readf999b4bc39f7274e42391ca653d8762d.tex}}}} | |
| -\newcommand{\sailRISCVvalextCheckPhysMemWrite}{\saildoclabelled{sailRISCVzextzycheckzyphyszymemzywrite}{\saildocval{Validate a write to physical memory. | |
| -\lstinline{ext_check_phys_mem_read}(write\_kind, paddr, size, data, metadata) should return Some(exception) | |
| +\newcommand{\sailRISCVvalextCheckPhysMemWrite}{\saildoclabelled{sailRISCVzextzycheckzyphyszymemzywrite}{\saildocval{ | |
| +Validate a write to physical memory. | |
| +\lstinline{ext_check_phys_mem_read}(write_kind, paddr, size, data, metadata) should return Some(exception) | |
| to abort the write or None to allow it to proceed. The check is performed | |
| after PMP checks and does not apply to MMIO memory. | |
| @@ -4913,7 +4925,8 @@ after PMP checks and does not apply to MMIO memory. | |
| \newcommand{\sailRISCVfnhandleCheriCapException}{\saildoclabelled{sailRISCVfnzhandlezycherizycapzyexception}{\saildocfn{}{\lstinputlisting[language=sail]{sail_latex_riscv/fnzhandle_cheri_cap_exceptionc1ff083ca6d0a739fb48243e22ff4898.tex}}}} | |
| -\newcommand{\sailRISCVvalhandleCheriRegException}{\saildoclabelled{sailRISCVzhandlezycherizyregzyexception}{\saildocval{Causes the processor to raise a capability exception by writing the given | |
| +\newcommand{\sailRISCVvalhandleCheriRegException}{\saildoclabelled{sailRISCVzhandlezycherizyregzyexception}{\saildocval{ | |
| +Causes the processor to raise a capability exception by writing the given | |
| capability exception cause and register number to the xtval register then | |
| signalling an exception. | |
| @@ -4921,7 +4934,8 @@ signalling an exception. | |
| \newcommand{\sailRISCVfnhandleCheriRegException}{\saildoclabelled{sailRISCVfnzhandlezycherizyregzyexception}{\saildocfn{}{\lstinputlisting[language=sail]{sail_latex_riscv/fnzhandle_cheri_reg_exceptionfad1b48ae08f4eb90d02a5d75771c894.tex}}}} | |
| -\newcommand{\sailRISCVvalhandleCheriPccException}{\saildoclabelled{sailRISCVzhandlezycherizypcczyexception}{\saildocval{Is as \hyperref[sailRISCVzhandlezycherizycapzyexception]{\lstinline{handle_cheri_cap_exception}} except that the capability register | |
| +\newcommand{\sailRISCVvalhandleCheriPccException}{\saildoclabelled{sailRISCVzhandlezycherizypcczyexception}{\saildocval{ | |
| +Is as \hyperref[sailRISCVzhandlezycherizycapzyexception]{\lstinline{handle_cheri_cap_exception}} except that the capability register | |
| number uses the special value 0x10 indicating the PCC register. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzhandle_cheri_pcc_exception3ca0178a61c5394ac2c49197cedda1c1.tex}}}} | |
| @@ -4958,15 +4972,17 @@ number uses the special value 0x10 indicating the PCC register. | |
| \newcommand{\sailRISCVtypeextDataAddrError}{\saildoclabelled{sailRISCVtypezextzydatazyaddrzyerror}{\saildoctype{}{\lstinputlisting[language=sail]{sail_latex_riscv/typezext_data_addr_errora4f74a5b44e1f0d7e46bc0f33c466dea.tex}}}} | |
| -\newcommand{\sailRISCVvalddcAndResultingAddr}{\saildoclabelled{sailRISCVzddczyandzyresultingzyaddr}{\saildocval{Returns the current value of DDC (for subsequent access checks) as well as | |
| +\newcommand{\sailRISCVvalddcAndResultingAddr}{\saildoclabelled{sailRISCVzddczyandzyresultingzyaddr}{\saildocval{ | |
| +Returns the current value of DDC (for subsequent access checks) as well as | |
| the resulting address for a non-CHERI integer-based memory access. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzddc_and_resulting_addr0f0e2d5c6123a71667b35ed17c44868e.tex}}}} | |
| \newcommand{\sailRISCVfnddcAndResultingAddr}{\saildoclabelled{sailRISCVfnzddczyandzyresultingzyaddr}{\saildocfn{}{\lstinputlisting[language=sail]{sail_latex_riscv/fnzddc_and_resulting_addr0f0e2d5c6123a71667b35ed17c44868e.tex}}}} | |
| -\newcommand{\sailRISCVvalgetCheriModeCapAddr}{\saildoclabelled{sailRISCVzgetzycherizymodezycapzyaddr}{\saildocval{For given base register and offset returns, depending on current capability | |
| -mode flag, a bounding capability, effective address, and capreg\_idx (for use | |
| +\newcommand{\sailRISCVvalgetCheriModeCapAddr}{\saildoclabelled{sailRISCVzgetzycherizymodezycapzyaddr}{\saildocval{ | |
| +For given base register and offset returns, depending on current capability | |
| +mode flag, a bounding capability, effective address, and capreg_idx (for use | |
| in cap cause). | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/valzget_cheri_mode_cap_addr267a231c94a9ae3cf08d67cb43590a2e.tex}}}} | |
| @@ -6159,51 +6175,49 @@ in cap cause). | |
| \newcommand{\sailRISCVfclZBSUnderscoreRTYPEexecute}{\saildoclabelled{sailRISCVfclZBSUnderscoreRTYPEzexecute}{\saildocfcl{}{\lstinputlisting[language=sail]{sail_latex_riscv/fclZBSUnderscoreRTYPEzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclAUIPCCexecute}{\saildoclabelled{sailRISCVfclAUIPCCzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of \textbf{PCC}, with the | |
| +\newcommand{\sailRISCVfclAUIPCCexecute}{\saildoclabelled{sailRISCVfclAUIPCCzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with the contents of \textbf{PCC}, with the | |
| \textbf{address} replaced with \textbf{PCC}.\textbf{address} $+$ \emph{imm} $\times$ 4096. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclAUIPCCzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCJALexecute}{\saildoclabelled{sailRISCVfclCJALzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the next instruction's \textbf{PCC} and | |
| +\newcommand{\sailRISCVfclCJALexecute}{\saildoclabelled{sailRISCVfclCJALzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with the next instruction's \textbf{PCC} and | |
| sealed as a sentry. \textbf{PCC}.\textbf{address} is incremented by \emph{imm}. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \textbf{PCC}.\textbf{address} $+$ \emph{imm} $\lt$ \textbf{PCC}.\textbf{base}. | |
| -\item \textbf{PCC}.\textbf{address} $+$ \emph{imm} $+$ min\_instruction\_bytes $\gt$ \textbf{PCC}.\textbf{top}. | |
| +\item \textbf{PCC}.\textbf{address} $+$ \emph{imm} $+$ min_instruction_bytes $\gt$ \textbf{PCC}.\textbf{top}. | |
| \item \textbf{PCC}.\textbf{address} $+$ \emph{imm} is unaligned, ignoring bit 0. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCJALzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCJALRexecute}{\saildoclabelled{sailRISCVfclCJALRzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the next instruction's \textbf{PCC} and | |
| +\newcommand{\sailRISCVfclCJALRexecute}{\saildoclabelled{sailRISCVfclCJALRzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with the next instruction's \textbf{PCC} and | |
| sealed as a sentry. \textbf{PCC} is replaced with the value of capability | |
| register \emph{cs1} with its \textbf{address} incremented by \emph{imm} and the 0th bit of | |
| its \textbf{address} set to 0, and is unsealed if it is a sentry. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \emph{cs1}.\textbf{tag} is not set. | |
| \item \emph{cs1} is sealed and is not a sentry. | |
| \item \emph{cs1} is a sentry and \emph{imm} $\ne$ 0. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Execute}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Execute}. | |
| \item \emph{cs1}.\textbf{address} $+$ \emph{imm} $\lt$ \emph{cs1}.\textbf{base}. | |
| -\item \emph{cs1}.\textbf{address} $+$ \emph{imm} $+$ min\_instruction\_bytes $\gt$ \emph{cs1}.\textbf{top}. | |
| +\item \emph{cs1}.\textbf{address} $+$ \emph{imm} $+$ min_instruction_bytes $\gt$ \emph{cs1}.\textbf{top}. | |
| \item \emph{cs1}.\textbf{base} is unaligned (only possible if PCC relocation is enabled). | |
| \item \emph{cs1}.\textbf{address} $+$ \emph{imm} is unaligned, ignoring bit 0. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCJALRzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCGetPermexecute}{\saildoclabelled{sailRISCVfclCGetPermzexecute}{\saildocfcl{The least significant \hyperref[sailRISCVzcapzyhpermszywidth]{\lstinline{cap_hperms_width}} bits of integer register \emph{rd} are | |
| +\newcommand{\sailRISCVfclCGetPermexecute}{\saildoclabelled{sailRISCVfclCGetPermzexecute}{\saildocfcl{ | |
| +The least significant \hyperref[sailRISCVzcapzyhpermszywidth]{\lstinline{cap_hperms_width}} bits of integer register \emph{rd} are | |
| set equal to the \textbf{perms} field of capability register \emph{cs1}; bits | |
| \hyperref[sailRISCVzcapzyupermszyshift]{\lstinline{cap_uperms_shift}} to \hyperref[sailRISCVzcapzyupermszyshift]{\lstinline{cap_uperms_shift}}+\hyperref[sailRISCVzcapzyupermszywidth]{\lstinline{cap_uperms_width}}-1 of \emph{rd} are set | |
| equal to the \textbf{uperms} field of \emph{cs1}. | |
| @@ -6211,27 +6225,32 @@ The other bits of \emph{rd} are set to zero. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetPermzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCGetFlagsexecute}{\saildoclabelled{sailRISCVfclCGetFlagszexecute}{\saildocfcl{Integer register \emph{rd} is set equal to the zero-extended \textbf{flags} field of | |
| +\newcommand{\sailRISCVfclCGetFlagsexecute}{\saildoclabelled{sailRISCVfclCGetFlagszexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set equal to the zero-extended \textbf{flags} field of | |
| capability register \emph{cs1}. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetFlagszexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCGetTypeexecute}{\saildoclabelled{sailRISCVfclCGetTypezexecute}{\saildocfcl{Integer register \emph{rd} is set equal to the \textbf{otype} field of capability | |
| +\newcommand{\sailRISCVfclCGetTypeexecute}{\saildoclabelled{sailRISCVfclCGetTypezexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set equal to the \textbf{otype} field of capability | |
| register \emph{cs1}. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetTypezexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCGetBaseexecute}{\saildoclabelled{sailRISCVfclCGetBasezexecute}{\saildocfcl{Integer register \emph{rd} is set equal to the \textbf{base} field of capability | |
| +\newcommand{\sailRISCVfclCGetBaseexecute}{\saildoclabelled{sailRISCVfclCGetBasezexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set equal to the \textbf{base} field of capability | |
| register \emph{cs1}. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetBasezexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCGetOffsetexecute}{\saildoclabelled{sailRISCVfclCGetOffsetzexecute}{\saildocfcl{Integer register \emph{rd} is set equal to the \textbf{offset} field of capability | |
| +\newcommand{\sailRISCVfclCGetOffsetexecute}{\saildoclabelled{sailRISCVfclCGetOffsetzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set equal to the \textbf{offset} field of capability | |
| register \emph{cs1}. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetOffsetzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCGetHighexecute}{\saildoclabelled{sailRISCVfclCGetHighzexecute}{\saildocfcl{Integer register \emph{rd} is set equal to the \textbf{high half} of capability | |
| +\newcommand{\sailRISCVfclCGetHighexecute}{\saildoclabelled{sailRISCVfclCGetHighzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set equal to the \textbf{high half} of capability | |
| register \emph{cs1}. | |
| The bits returned here are of the \textbf{in-memory} form of the capability, which | |
| @@ -6244,7 +6263,8 @@ capability is interpreted as a twice-\textbf{XLEN}-bit integer). | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetHighzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCSetHighexecute}{\saildoclabelled{sailRISCVfclCSetHighzexecute}{\saildocfcl{Capability register \emph{cd} comes to hold the capability from \emph{cs1} with its | |
| +\newcommand{\sailRISCVfclCSetHighexecute}{\saildoclabelled{sailRISCVfclCSetHighzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} comes to hold the capability from \emph{cs1} with its | |
| high bits replaced with the value in the integer register \emph{rs2}. The tag | |
| of \emph{cd} is cleared. | |
| @@ -6253,85 +6273,83 @@ instruction yields the same result as writing \emph{cs1} out to memory, | |
| overwriting the high word with \emph{rs2}, and loading that capability-sized | |
| granule into \emph{cd}, although without the memory mutation side-effects. | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSetHighzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCGetLenexecute}{\saildoclabelled{sailRISCVfclCGetLenzexecute}{\saildocfcl{Integer register \emph{rd} is set equal to the \textbf{length} field of capability | |
| +\newcommand{\sailRISCVfclCGetLenexecute}{\saildoclabelled{sailRISCVfclCGetLenzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set equal to the \textbf{length} field of capability | |
| register \emph{cs1}. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item Due to the compressed representation of capabilities, the actual length | |
| - of capabilities can be $2^{\hyperref[sailRISCVzxlen]{{xlen}}}$; \hyperref[sailRISCVzCGetLen]{\lstinline{CGetLen}} will return the | |
| - maximum value of $2^{\hyperref[sailRISCVzxlen]{{xlen}}}-1$ in this case. | |
| - | |
| +of capabilities can be $2^{\hyperref[sailRISCVzxlen]{\lstinline{{xlen}}}}$; \hyperref[sailRISCVzCGetLen]{\lstinline{CGetLen}} will return the | |
| +maximum value of $2^{\hyperref[sailRISCVzxlen]{\lstinline{{xlen}}}}-1$ in this case. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetLenzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCGetTopexecute}{\saildoclabelled{sailRISCVfclCGetTopzexecute}{\saildocfcl{Integer register \emph{rd} is set equal to the \textbf{top} field (\saildocabbrev{i.e.} one past the | |
| +\newcommand{\sailRISCVfclCGetTopexecute}{\saildoclabelled{sailRISCVfclCGetTopzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set equal to the \textbf{top} field (i.e. one past the | |
| last addressable byte) of capability register \emph{cs1}. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item Due to the compressed representation of capabilities, the actual top | |
| - of capabilities can be $2^{\hyperref[sailRISCVzxlen]{{xlen}}}$; \hyperref[sailRISCVzCGetTop]{\lstinline{CGetTop}} will return the | |
| - maximum value of $2^{\hyperref[sailRISCVzxlen]{{xlen}}}-1$ in this case. | |
| - | |
| +of capabilities can be $2^{\hyperref[sailRISCVzxlen]{\lstinline{{xlen}}}}$; \hyperref[sailRISCVzCGetTop]{\lstinline{CGetTop}} will return the | |
| +maximum value of $2^{\hyperref[sailRISCVzxlen]{\lstinline{{xlen}}}}-1$ in this case. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetTopzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCGetTagexecute}{\saildoclabelled{sailRISCVfclCGetTagzexecute}{\saildocfcl{The low bit of integer register \emph{rd} is set to the \textbf{tag} field of \emph{cs1}. | |
| +\newcommand{\sailRISCVfclCGetTagexecute}{\saildoclabelled{sailRISCVfclCGetTagzexecute}{\saildocfcl{ | |
| +The low bit of integer register \emph{rd} is set to the \textbf{tag} field of \emph{cs1}. | |
| All other bits of \emph{rd} are cleared. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetTagzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCGetSealedexecute}{\saildoclabelled{sailRISCVfclCGetSealedzexecute}{\saildocfcl{The low bit of integer register \emph{rd} is set to 0 if \emph{cs1} is unsealed | |
| +\newcommand{\sailRISCVfclCGetSealedexecute}{\saildoclabelled{sailRISCVfclCGetSealedzexecute}{\saildocfcl{ | |
| +The low bit of integer register \emph{rd} is set to 0 if \emph{cs1} is unsealed | |
| and to 1 otherwise. | |
| All other bits of \emph{rd} are cleared. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetSealedzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCGetAddrexecute}{\saildoclabelled{sailRISCVfclCGetAddrzexecute}{\saildocfcl{Integer register \emph{rd} is set equal to the \textbf{address} field of capability | |
| +\newcommand{\sailRISCVfclCGetAddrexecute}{\saildoclabelled{sailRISCVfclCGetAddrzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set equal to the \textbf{address} field of capability | |
| register \emph{cs1}. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetAddrzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCSpecialRWexecute}{\saildoclabelled{sailRISCVfclCSpecialRWzexecute}{\saildocfcl{Capability register \emph{cd} is set equal to special capability register \emph{scr}, | |
| +\newcommand{\sailRISCVfclCSpecialRWexecute}{\saildoclabelled{sailRISCVfclCSpecialRWzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is set equal to special capability register \emph{scr}, | |
| and \emph{scr} is set equal to capability register \emph{cs1} if \emph{cs1} is not \textbf{C0}. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \emph{scr} does not exist. | |
| \item \emph{scr} is read-only and \emph{cs1} is not \textbf{C0}. | |
| \item \emph{scr} is only accessible to a higher privilege mode. | |
| -\item \emph{scr} requires \textbf{Permit\_Access\_System\_Registers} and that is not | |
| - granted by \textbf{PCC}.\textbf{perms}. | |
| +\item \emph{scr} requires \textbf{Permit_Access_System_Registers} and that is not | |
| +granted by \textbf{PCC}.\textbf{perms}. | |
| \end{itemize} | |
| - | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item Writing \textbf{NULL} to a special capability register cannot be done with \textbf{C0} | |
| - as that only performs a read. An alternative implementation would allocate | |
| - a separate two-operand CSpecialR instruction and interpret \emph{cs1} being | |
| - \textbf{C0} as a write of \textbf{NULL} if the need to use a temporary capability | |
| - register proves to be overly problematic for software. For U-mode | |
| - transitions to domains without \textbf{Permit\_Access\_System\_Registers} only | |
| - \textbf{DDC} should need clearing, which can be done with \hyperref[sailRISCVzCClear]{\lstinline{CClear}}. | |
| - | |
| +as that only performs a read. An alternative implementation would allocate | |
| +a separate two-operand CSpecialR instruction and interpret \emph{cs1} being | |
| +\textbf{C0} as a write of \textbf{NULL} if the need to use a temporary capability | |
| +register proves to be overly problematic for software. For U-mode | |
| +transitions to domains without \textbf{Permit_Access_System_Registers} only | |
| +\textbf{DDC} should need clearing, which can be done with \hyperref[sailRISCVzCClear]{\lstinline{CClear}}. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSpecialRWzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCAndPermexecute}{\saildoclabelled{sailRISCVfclCAndPermzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability | |
| +\newcommand{\sailRISCVfclCAndPermexecute}{\saildoclabelled{sailRISCVfclCAndPermzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with the contents of capability | |
| register \emph{cs1} with the \textbf{perms} field set to the bitwise and of its | |
| previous value and bits 0 to \hyperref[sailRISCVzcapzyhpermszywidth]{\lstinline{cap_hperms_width}}-1 of integer register \emph{rs2} | |
| and the \textbf{uperms} field set to the bitwise and of its previous value and | |
| @@ -6340,31 +6358,33 @@ If \emph{cs1} was sealed then \emph{cd}.\textbf{tag} is cleared. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCAndPermzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCSetFlagsexecute}{\saildoclabelled{sailRISCVfclCSetFlagszexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability | |
| +\newcommand{\sailRISCVfclCSetFlagsexecute}{\saildoclabelled{sailRISCVfclCSetFlagszexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with the contents of capability | |
| register \emph{cs1} with the \textbf{flags} field set to bits 0 to \hyperref[sailRISCVzcapzyflagszywidth]{\lstinline{cap_flags_width}}-1 | |
| of integer register \emph{rs2}. If \emph{cs1} was sealed then \emph{cd}.\textbf{tag} is cleared. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSetFlagszexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCToPtrexecute}{\saildoclabelled{sailRISCVfclCToPtrzexecute}{\saildocfcl{If the \textbf{tag} field of capability register \emph{cs1} is not set, integer | |
| +\newcommand{\sailRISCVfclCToPtrexecute}{\saildoclabelled{sailRISCVfclCToPtrzexecute}{\saildocfcl{ | |
| +If the \textbf{tag} field of capability register \emph{cs1} is not set, integer | |
| register \emph{rd} is set to 0, otherwise integer register \emph{rd} is set to | |
| \emph{cs1}.\textbf{address} $-$ \emph{cs2}.\textbf{base}. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item \emph{cs2} being sealed will not set \emph{rd} to 0. This is for further study. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCToPtrzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCSubexecute}{\saildoclabelled{sailRISCVfclCSubzexecute}{\saildocfcl{Integer register \emph{rd} is set equal to (\emph{cs1}.\textbf{address} $-$ | |
| -\emph{cs2}.\textbf{address}) $\bmod~2^{\hyperref[sailRISCVzxlen]{{xlen}}}$. | |
| +\newcommand{\sailRISCVfclCSubexecute}{\saildoclabelled{sailRISCVfclCSubzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set equal to (\emph{cs1}.\textbf{address} $-$ | |
| +\emph{cs2}.\textbf{address}) $\bmod~2^{\hyperref[sailRISCVzxlen]{\lstinline{{xlen}}}}$. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSubzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCIncOffsetexecute}{\saildoclabelled{sailRISCVfclCIncOffsetzexecute}{\saildocfcl{Capability register \emph{cd} is set equal to capability register \emph{cs1} with its | |
| +\newcommand{\sailRISCVfclCIncOffsetexecute}{\saildoclabelled{sailRISCVfclCIncOffsetzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is set equal to capability register \emph{cs1} with its | |
| \textbf{address} replaced with \emph{cs1}.\textbf{address} $+$ \emph{rs2}. | |
| If the resulting capability cannot be represented exactly, or if \emph{cs1} was | |
| sealed, then \emph{cd}.\textbf{tag} is cleared. The remaining capability fields are | |
| @@ -6373,7 +6393,8 @@ set to what the in-memory representation of \emph{cs1} with the address set to | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCIncOffsetzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCIncOffsetImmediateexecute}{\saildoclabelled{sailRISCVfclCIncOffsetImmediatezexecute}{\saildocfcl{Capability register \emph{cd} is set equal to capability register \emph{cs1} with its | |
| +\newcommand{\sailRISCVfclCIncOffsetImmediateexecute}{\saildoclabelled{sailRISCVfclCIncOffsetImmediatezexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is set equal to capability register \emph{cs1} with its | |
| \textbf{address} replaced with \emph{cs1}.\textbf{address} $+$ \emph{imm}. | |
| If the resulting capability cannot be represented exactly, or if \emph{cs1} was | |
| sealed, then \emph{cd}.\textbf{tag} is cleared. The remaining capability fields are | |
| @@ -6382,7 +6403,8 @@ set to what the in-memory representation of \emph{cs1} with the address set to | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCIncOffsetImmediatezexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCSetOffsetexecute}{\saildoclabelled{sailRISCVfclCSetOffsetzexecute}{\saildocfcl{Capability register \emph{cd} is set equal to capability register \emph{cs1} with its | |
| +\newcommand{\sailRISCVfclCSetOffsetexecute}{\saildoclabelled{sailRISCVfclCSetOffsetzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is set equal to capability register \emph{cs1} with its | |
| \textbf{address} replaced with \emph{cs1}.\textbf{base} $+$ \emph{rs2}. | |
| If the resulting capability cannot be represented exactly, or if \emph{cs1} was | |
| sealed, then \emph{cd}.\textbf{tag} is cleared. The remaining capability fields are | |
| @@ -6391,7 +6413,8 @@ set to what the in-memory representation of \emph{cs1} with the address set to | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSetOffsetzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCSetAddrexecute}{\saildoclabelled{sailRISCVfclCSetAddrzexecute}{\saildocfcl{Capability register \emph{cd} is set equal to capability register \emph{cs1} with its | |
| +\newcommand{\sailRISCVfclCSetAddrexecute}{\saildoclabelled{sailRISCVfclCSetAddrzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is set equal to capability register \emph{cs1} with its | |
| \textbf{address} replaced with \emph{rs2}. | |
| If the resulting capability cannot be represented exactly, or if \emph{cs1} was | |
| sealed, then \emph{cd}.\textbf{tag} is cleared. The remaining capability fields are | |
| @@ -6400,7 +6423,8 @@ set to what the in-memory representation of \emph{cs1} with the address set to | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSetAddrzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCSetBoundsexecute}{\saildoclabelled{sailRISCVfclCSetBoundszexecute}{\saildocfcl{Capability register \emph{cd} is set to capability register \emph{cs1} with its | |
| +\newcommand{\sailRISCVfclCSetBoundsexecute}{\saildoclabelled{sailRISCVfclCSetBoundszexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is set to capability register \emph{cs1} with its | |
| \textbf{base} field replaced with \emph{cs1}.\textbf{address} and its \textbf{length} field | |
| replaced with integer register \emph{rs2}. If the resulting capability cannot be | |
| represented exactly the \textbf{base} will be rounded down and the \textbf{length} | |
| @@ -6411,7 +6435,8 @@ is cleared if the bounds of the result exceed the bounds of \emph{cs1}, or if | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSetBoundszexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCSetBoundsImmediateexecute}{\saildoclabelled{sailRISCVfclCSetBoundsImmediatezexecute}{\saildocfcl{Capability register \emph{cd} is set to capability register \emph{cs1} with its | |
| +\newcommand{\sailRISCVfclCSetBoundsImmediateexecute}{\saildoclabelled{sailRISCVfclCSetBoundsImmediatezexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is set to capability register \emph{cs1} with its | |
| \textbf{base} field replaced with \emph{cs1}.\textbf{address} and its \textbf{length} field | |
| replaced with \emph{uimm}. If the resulting capability cannot be represented | |
| exactly the \textbf{base} will be rounded down and the \textbf{length} will be rounded | |
| @@ -6421,7 +6446,8 @@ bounds of the result exceed the bounds of \emph{cs1}, or if \emph{cs1} was seale | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSetBoundsImmediatezexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCSetBoundsExactexecute}{\saildoclabelled{sailRISCVfclCSetBoundsExactzexecute}{\saildocfcl{Capability register \emph{cd} is set to capability register \emph{cs1} with its | |
| +\newcommand{\sailRISCVfclCSetBoundsExactexecute}{\saildoclabelled{sailRISCVfclCSetBoundsExactzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is set to capability register \emph{cs1} with its | |
| \textbf{base} field replaced with \emph{cs1}.\textbf{address} and its \textbf{length} field | |
| replaced with integer register \emph{rs2}. If the resulting capability cannot be | |
| represented exactly, the \textbf{tag} field will be cleared (unlike | |
| @@ -6433,55 +6459,54 @@ sealed. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSetBoundsExactzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCClearTagexecute}{\saildoclabelled{sailRISCVfclCClearTagzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of \emph{cs1}, with | |
| +\newcommand{\sailRISCVfclCClearTagexecute}{\saildoclabelled{sailRISCVfclCClearTagzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with the contents of \emph{cs1}, with | |
| the \textbf{tag} field cleared. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCClearTagzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCMoveexecute}{\saildoclabelled{sailRISCVfclCMovezexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of \emph{cs1}. | |
| +\newcommand{\sailRISCVfclCMoveexecute}{\saildoclabelled{sailRISCVfclCMovezexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with the contents of \emph{cs1}. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCMovezexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCClearexecute}{\saildoclabelled{sailRISCVfclCClearzexecute}{\saildocfcl{Capability registers 8 $\times$ \emph{q} $+$ \emph{i} are each set to \textbf{NULL} if the | |
| +\newcommand{\sailRISCVfclCClearexecute}{\saildoclabelled{sailRISCVfclCClearzexecute}{\saildocfcl{ | |
| +Capability registers 8 $\times$ \emph{q} $+$ \emph{i} are each set to \textbf{NULL} if the | |
| \emph{i}th bit of \emph{m} is set, with the exception that the 0th bit of \emph{m} refers | |
| to \textbf{DDC} when \emph{q} is 0, rather than \textbf{C0}. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item This instruction is designed to accelerate the register clearing that is | |
| - required for secure domain transitions. It is expected that it can be | |
| - implemented efficiently in hardware using a single `valid' bit per | |
| - register that is cleared by this instruction and set on any subsequent | |
| - write to the register. | |
| - | |
| +required for secure domain transitions. It is expected that it can be | |
| +implemented efficiently in hardware using a single `valid' bit per | |
| +register that is cleared by this instruction and set on any subsequent | |
| +write to the register. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCClearzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclFPClearexecute}{\saildoclabelled{sailRISCVfclFPClearzexecute}{\saildocfcl{Floating-point registers 8 $\times$ \emph{q} $+$ \emph{i} are each set to 0 if the | |
| +\newcommand{\sailRISCVfclFPClearexecute}{\saildoclabelled{sailRISCVfclFPClearzexecute}{\saildocfcl{ | |
| +Floating-point registers 8 $\times$ \emph{q} $+$ \emph{i} are each set to 0 if the | |
| \emph{i}th bit of \emph{m} is set. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item This instruction is designed to accelerate the register clearing that is | |
| - required for secure domain transitions. It is expected that it can be | |
| - implemented efficiently in hardware using a single `valid' bit per | |
| - register that is cleared by this instruction and set on any subsequent | |
| - write to the register. | |
| - | |
| +required for secure domain transitions. It is expected that it can be | |
| +implemented efficiently in hardware using a single `valid' bit per | |
| +register that is cleared by this instruction and set on any subsequent | |
| +write to the register. | |
| \item The 0 value written is FLEN bits wide, the largest supported by the | |
| - implementation, such that the in-memory representation of the register is | |
| - 0, rather than a NaN-boxed narrower value. | |
| - | |
| - | |
| +implementation, such that the in-memory representation of the register is | |
| +0, rather than a NaN-boxed narrower value. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclFPClearzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCFromPtrexecute}{\saildoclabelled{sailRISCVfclCFromPtrzexecute}{\saildocfcl{If the value of integer register \emph{rs2} is 0 then capability register \emph{cd} is | |
| +\newcommand{\sailRISCVfclCFromPtrexecute}{\saildoclabelled{sailRISCVfclCFromPtrzexecute}{\saildocfcl{ | |
| +If the value of integer register \emph{rs2} is 0 then capability register \emph{cd} is | |
| set to \textbf{NULL}. Otherwise capability register \emph{cd} is set to capability | |
| register \emph{cs1} with its \textbf{offset} replaced with \emph{rs2}. If the resulting | |
| capability cannot be represented exactly, or if \emph{cs1} was sealed, then | |
| @@ -6491,7 +6516,8 @@ decodes to. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCFromPtrzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCBuildCapexecute}{\saildoclabelled{sailRISCVfclCBuildCapzexecute}{\saildocfcl{Capability register \emph{cd} is set equal to capability register \emph{cs1} with its | |
| +\newcommand{\sailRISCVfclCBuildCapexecute}{\saildoclabelled{sailRISCVfclCBuildCapzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is set equal to capability register \emph{cs1} with its | |
| \textbf{base}, \textbf{length}, \textbf{address}, \textbf{perms}, \textbf{uperms} and \textbf{flags} | |
| replaced with the corresponding fields in capability register \emph{cs2}. If | |
| \emph{cs2} is a sentry then \emph{cd} is also sealed as a sentry. If the resulting | |
| @@ -6500,80 +6526,79 @@ legally derivable capability, or if \emph{cs1} did not have its \textbf{tag} fie | |
| set, or if \emph{cs1} was sealed, \emph{cd} is replaced with \emph{cs2} with its \textbf{tag} | |
| field cleared. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item Implementations may instead choose to set \emph{cd} to \emph{cs2} with its \textbf{tag} | |
| - set after performing all checks, but the specification derives the result | |
| - from \emph{cs1} in order to convey the provenance associated with this | |
| - operation. | |
| - | |
| +set after performing all checks, but the specification derives the result | |
| +from \emph{cs1} in order to convey the provenance associated with this | |
| +operation. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCBuildCapzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCCopyTypeexecute}{\saildoclabelled{sailRISCVfclCCopyTypezexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability | |
| +\newcommand{\sailRISCVfclCCopyTypeexecute}{\saildoclabelled{sailRISCVfclCCopyTypezexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with the contents of capability | |
| register \emph{cs1} with the \textbf{address} set to \emph{cs2}.\textbf{otype} and the | |
| \textbf{tag} field cleared if \emph{cs2} has a reserved \textbf{otype} or if \emph{cs1} | |
| was sealed. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item Reserved otypes always result in untagged capabilities, as, at the | |
| - moment, all reserved otypes are constructed using ambiently-available | |
| - actions. \hyperref[sailRISCVzCCSeal]{\lstinline{CCSeal}} knows how to work with these. | |
| - | |
| +moment, all reserved otypes are constructed using ambiently-available | |
| +actions. \hyperref[sailRISCVzCCSeal]{\lstinline{CCSeal}} knows how to work with these. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCCopyTypezexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCRRLexecute}{\saildoclabelled{sailRISCVfclCRRLzexecute}{\saildocfcl{Integer register \emph{rd} is set to the smallest value greater or equal to \emph{rs1} | |
| +\newcommand{\sailRISCVfclCRRLexecute}{\saildoclabelled{sailRISCVfclCRRLzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set to the smallest value greater or equal to \emph{rs1} | |
| that can be used as a length to set exact bounds on a capability that has a | |
| suitably aligned base (as obtained with the help of \hyperref[sailRISCVzCRAM]{\lstinline{CRAM}}). | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCRRLzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCRAMexecute}{\saildoclabelled{sailRISCVfclCRAMzexecute}{\saildocfcl{Integer register \emph{rd} is set to a mask that can be used to round addresses | |
| +\newcommand{\sailRISCVfclCRAMexecute}{\saildoclabelled{sailRISCVfclCRAMzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set to a mask that can be used to round addresses | |
| down to to a value that is sufficiently aligned to set exact bounds for the | |
| nearest representable length of \emph{rs1} (as obtained by \hyperref[sailRISCVzCRRL]{\lstinline{CRRL}}). | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCRAMzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCTestSubsetexecute}{\saildoclabelled{sailRISCVfclCTestSubsetzexecute}{\saildocfcl{Integer register \emph{rd} is set to 1 if the \textbf{tag} fields of capability | |
| +\newcommand{\sailRISCVfclCTestSubsetexecute}{\saildoclabelled{sailRISCVfclCTestSubsetzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set to 1 if the \textbf{tag} fields of capability | |
| registers \emph{cs1} and \emph{cs2} are the same and the bounds and permissions of | |
| \emph{cs2} are a subset of those of \emph{cs1}. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item The operand order for this instruction is reversed compared with the | |
| - normal RISC-V comparison instructions, but this may be changed in future. | |
| - | |
| +normal RISC-V comparison instructions, but this may be changed in future. | |
| \item The \textbf{otype} field is ignored for this instruction, but an alternative | |
| - implementation might wish to consider capabilities with distinct | |
| - \textbf{otype}s as unordered as is done for the \textbf{tag} field. | |
| - | |
| - | |
| +implementation might wish to consider capabilities with distinct | |
| +\textbf{otype}s as unordered as is done for the \textbf{tag} field. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCTestSubsetzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCSEQXexecute}{\saildoclabelled{sailRISCVfclCSEQXzexecute}{\saildocfcl{Integer register \emph{rd} is set to 1 if the \textbf{tag} fields and in-memory | |
| +\newcommand{\sailRISCVfclCSEQXexecute}{\saildoclabelled{sailRISCVfclCSEQXzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is set to 1 if the \textbf{tag} fields and in-memory | |
| representations of capability registers \emph{cs1} and \emph{cs2} are identical, | |
| including any reserved encoding bits, otherwise it is set to 0. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSEQXzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCSealexecute}{\saildoclabelled{sailRISCVfclCSealzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with capability register \emph{cs1}, and is | |
| +\newcommand{\sailRISCVfclCSealexecute}{\saildoclabelled{sailRISCVfclCSealzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with capability register \emph{cs1}, and is | |
| sealed with \textbf{otype} equal to the \textbf{address} field of capability register | |
| \emph{cs2}. If \emph{cs2} is unable to authorize the sealing, or if \emph{cs1} was already | |
| sealed, then the \textbf{tag} field of \emph{cd} is cleared. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSealzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCCSealexecute}{\saildoclabelled{sailRISCVfclCCSealzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with capability register \emph{cs1}, and is | |
| +\newcommand{\sailRISCVfclCCSealexecute}{\saildoclabelled{sailRISCVfclCCSealzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with capability register \emph{cs1}, and is | |
| conditionally sealed with \textbf{otype} equal to the \textbf{address} field of | |
| capability register \emph{cs2}. The conditions under which the input is passed | |
| through unaltered are intended to permit a fast branchless rederivation | |
| @@ -6582,40 +6607,35 @@ set of \hyperref[sailRISCVzCCopyType]{\lstinline{CCopyType}} and \hyperref[sailR | |
| disk. Other than these conditions, if \emph{cs2} is unable to authorize the | |
| sealing, the \textbf{tag} field of \emph{cd} is cleared. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item The intent is that this is used for rederiving swapped-out capabilities, | |
| - so the expectation is that this whole sequence is guarded by a check on | |
| - whether the \textbf{tag} field of the capability was valid. | |
| - | |
| +so the expectation is that this whole sequence is guarded by a check on | |
| +whether the \textbf{tag} field of the capability was valid. | |
| \item If the input to be conditionally sealed is already sealed it is passed | |
| - through before any futher checks are made. This allows multiple \hyperref[sailRISCVzCCSeal]{\lstinline{CCSeal}}s | |
| - in a chain, any of which can be the one to seal the initial input. The | |
| - intent is that all of these \hyperref[sailRISCVzCCSeal]{\lstinline{CCSeal}}s' authorities will have been produced | |
| - by \hyperref[sailRISCVzCCopyType]{\lstinline{CCopyType}}s of the same input (i.e., they will all attempt to seal to | |
| - the same type), but that's not, strictly, required. Sealed capabilities | |
| - with a reserved \textbf{otype} are also constructed directly by \hyperref[sailRISCVzCBuildCap]{\lstinline{CBuildCap}}. | |
| - | |
| +through before any futher checks are made. This allows multiple \hyperref[sailRISCVzCCSeal]{\lstinline{CCSeal}}s | |
| +in a chain, any of which can be the one to seal the initial input. The | |
| +intent is that all of these \hyperref[sailRISCVzCCSeal]{\lstinline{CCSeal}}s' authorities will have been produced | |
| +by \hyperref[sailRISCVzCCopyType]{\lstinline{CCopyType}}s of the same input (i.e., they will all attempt to seal to | |
| +the same type), but that's not, strictly, required. Sealed capabilities | |
| +with a reserved \textbf{otype} are also constructed directly by \hyperref[sailRISCVzCBuildCap]{\lstinline{CBuildCap}}. | |
| \item To avoid the need to branch on whether the original capability was sealed, | |
| - attempts to seal with the reserved unsealed \textbf{otype} will leave the | |
| - capability unmodified rather than trap. | |
| - | |
| +attempts to seal with the reserved unsealed \textbf{otype} will leave the | |
| +capability unmodified rather than trap. | |
| \item To avoid the need to check which is the correct authority, any sealing | |
| - request where the \textbf{address} of capability register \emph{cs2} is out of | |
| - bounds will leave the capability unmodified rather than trap, as will | |
| - attempts to seal with an invalid capability since it may have become | |
| - unrepresentable but be within its reinterpreted bounds. | |
| - | |
| - | |
| +request where the \textbf{address} of capability register \emph{cs2} is out of | |
| +bounds will leave the capability unmodified rather than trap, as will | |
| +attempts to seal with an invalid capability since it may have become | |
| +unrepresentable but be within its reinterpreted bounds. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCCSealzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCUnsealexecute}{\saildoclabelled{sailRISCVfclCUnsealzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with capability register \emph{cs1} and is | |
| +\newcommand{\sailRISCVfclCUnsealexecute}{\saildoclabelled{sailRISCVfclCUnsealzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with capability register \emph{cs1} and is | |
| unsealed, using capability register \emph{cs2} as the authority for the unsealing | |
| operation. If \emph{cs2}.\textbf{perms} does not grant \textbf{Global} then \emph{cd}.\textbf{perms} | |
| is stripped of \textbf{Global}. If \emph{cs2} is unable to authorize the unsealing, | |
| @@ -6623,12 +6643,14 @@ the \textbf{tag} field of \emph{cd} is cleared. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnsealzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCSealEntryexecute}{\saildoclabelled{sailRISCVfclCSealEntryzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with capability register \emph{cs1} and | |
| +\newcommand{\sailRISCVfclCSealEntryexecute}{\saildoclabelled{sailRISCVfclCSealEntryzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with capability register \emph{cs1} and | |
| sealed as a sentry. | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSealEntryzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCInvokeexecute}{\saildoclabelled{sailRISCVfclCInvokezexecute}{\saildocfcl{\textbf{PCC} is set equal to capability register \emph{cs1} and unsealed with the 0th | |
| +\newcommand{\sailRISCVfclCInvokeexecute}{\saildoclabelled{sailRISCVfclCInvokezexecute}{\saildocfcl{ | |
| +\textbf{PCC} is set equal to capability register \emph{cs1} and unsealed with the 0th | |
| bit of its \textbf{address} set to 0, whilst \textbf{C31} is set equal to capability | |
| register \emph{cs2} and unsealed. This provides a constrained form of | |
| non-monotonicity, allowing for fast jumps between protection domains, with | |
| @@ -6636,162 +6658,145 @@ non-monotonicity, allowing for fast jumps between protection domains, with | |
| domain's data. The capabilities must have a matching \textbf{otype} to ensure the | |
| right data is provided for the given jump target. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \emph{cs1}.\textbf{tag} is not set. | |
| \item \emph{cs2}.\textbf{tag} is not set. | |
| \item \emph{cs1}.\textbf{otype} is reserved. | |
| \item \emph{cs2}.\textbf{otype} is reserved. | |
| \item \emph{cs1}.\textbf{otype} $\ne$ \emph{cs2}.\textbf{otype}. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_CInvoke}. | |
| -\item \emph{cs2}.\textbf{perms} does not grant \textbf{Permit\_CInvoke}. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Execute}. | |
| -\item \emph{cs2}.\textbf{perms} grants \textbf{Permit\_Execute}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_CInvoke}. | |
| +\item \emph{cs2}.\textbf{perms} does not grant \textbf{Permit_CInvoke}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Execute}. | |
| +\item \emph{cs2}.\textbf{perms} grants \textbf{Permit_Execute}. | |
| \item \emph{cs1}.\textbf{address} $\lt$ \emph{cs1}.\textbf{base}. | |
| -\item \emph{cs1}.\textbf{address} $+$ min\_instruction\_bytes $\gt$ \emph{cs1}.\textbf{top}. | |
| +\item \emph{cs1}.\textbf{address} $+$ min_instruction_bytes $\gt$ \emph{cs1}.\textbf{top}. | |
| \item \emph{cs1}.\textbf{base} is unaligned (only possible if PCC relocation is enabled). | |
| \item \emph{cs1}.\textbf{address} is unaligned, ignoring bit 0. | |
| \end{itemize} | |
| - | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item From the point of view of security, this needs to be an atomic operation | |
| - (i.e. the caller cannot decide to just do some of it, because partial | |
| - execution could put the system into an insecure state). From a hardware | |
| - perspective, more complex domain-transition implementations (e.g., to | |
| - implement function-call semantics or message passing) may need to perform | |
| - multiple memory reads and writes, which might take multiple cycles and | |
| - complicate control logic. | |
| - | |
| +(i.e. the caller cannot decide to just do some of it, because partial | |
| +execution could put the system into an insecure state). From a hardware | |
| +perspective, more complex domain-transition implementations (e.g., to | |
| +implement function-call semantics or message passing) may need to perform | |
| +multiple memory reads and writes, which might take multiple cycles and | |
| +complicate control logic. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCInvokezexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclJALRUnderscoreCAPexecute}{\saildoclabelled{sailRISCVfclJALRUnderscoreCAPzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the next instruction's \textbf{PCC} and | |
| +\newcommand{\sailRISCVfclJALRUnderscoreCAPexecute}{\saildoclabelled{sailRISCVfclJALRUnderscoreCAPzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with the next instruction's \textbf{PCC} and | |
| sealed as a sentry. \textbf{PCC} is replaced with the value of capability | |
| register \emph{cs1} with the 0th bit of its \textbf{address} set to 0 and is unsealed | |
| if it is a sentry. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \emph{cs1}.\textbf{tag} is not set. | |
| \item \emph{cs1} is sealed and is not a sentry. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Execute}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Execute}. | |
| \item \emph{cs1}.\textbf{address} $\lt$ \emph{cs1}.\textbf{base}. | |
| -\item \emph{cs1}.\textbf{address} $+$ min\_instruction\_bytes $\gt$ \emph{cs1}.\textbf{top}. | |
| +\item \emph{cs1}.\textbf{address} $+$ min_instruction_bytes $\gt$ \emph{cs1}.\textbf{top}. | |
| \item \emph{cs1}.\textbf{base} is unaligned (only possible if PCC relocation is enabled). | |
| \item \emph{cs1}.\textbf{address} is unaligned, ignoring bit 0. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclJALRUnderscoreCAPzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclJALRUnderscorePCCexecute}{\saildoclabelled{sailRISCVfclJALRUnderscorePCCzexecute}{\saildocfcl{Integer register \emph{rd} is replaced with the next instruction's | |
| +\newcommand{\sailRISCVfclJALRUnderscorePCCexecute}{\saildoclabelled{sailRISCVfclJALRUnderscorePCCzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is replaced with the next instruction's | |
| \textbf{PCC}.\textbf{offset}. \textbf{PCC}.\textbf{offset} is replaced with the value of | |
| register \emph{rs1} with the 0th bit set to 0. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \textbf{PCC}.\textbf{address} $+$ \emph{rs1} $\lt$ \textbf{PCC}.\textbf{base}. | |
| -\item \textbf{PCC}.\textbf{address} $+$ \emph{rs1} $+$ min\_instruction\_bytes $\gt$ \textbf{PCC}.\textbf{top}. | |
| +\item \textbf{PCC}.\textbf{address} $+$ \emph{rs1} $+$ min_instruction_bytes $\gt$ \textbf{PCC}.\textbf{top}. | |
| \item \textbf{PCC}.\textbf{address} $+$ \emph{rs1} is unaligned, ignoring bit 0. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclJALRUnderscorePCCzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclLoadDataDDCexecute}{\saildoclabelled{sailRISCVfclLoadDataDDCzexecute}{\saildocfcl{Integer register \emph{rd} is replaced with the signed or unsigned byte, | |
| +\newcommand{\sailRISCVfclLoadDataDDCexecute}{\saildoclabelled{sailRISCVfclLoadDataDDCzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is replaced with the signed or unsigned byte, | |
| halfword, word or doubleword located in memory at \textbf{DDC}.\textbf{address} $+$ | |
| \emph{rs1}. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \textbf{DDC}.\textbf{tag} is not set. | |
| \item \textbf{DDC} is sealed. | |
| -\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit\_Load}. | |
| +\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit_Load}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $\lt$ \textbf{DDC}.\textbf{base}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $+$ \emph{size} $\gt$ \textbf{DDC}.\textbf{top}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclLoadDataDDCzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclLoadDataCapexecute}{\saildoclabelled{sailRISCVfclLoadDataCapzexecute}{\saildocfcl{Integer register \emph{rd} is replaced with the signed or unsigned byte, | |
| +\newcommand{\sailRISCVfclLoadDataCapexecute}{\saildoclabelled{sailRISCVfclLoadDataCapzexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is replaced with the signed or unsigned byte, | |
| halfword, word or doubleword located in memory at \emph{cs1}.\textbf{address}. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \emph{cs1}.\textbf{tag} is not set. | |
| \item \emph{cs1} is sealed. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Load}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Load}. | |
| \item \emph{cs1}.\textbf{address} $\lt$ \emph{cs1}.\textbf{base}. | |
| \item \emph{cs1}.\textbf{address} $+$ \emph{size} $\gt$ \emph{cs1}.\textbf{top}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclLoadDataCapzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclLoadCapDDCexecute}{\saildoclabelled{sailRISCVfclLoadCapDDCzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the capability located in memory | |
| +\newcommand{\sailRISCVfclLoadCapDDCexecute}{\saildoclabelled{sailRISCVfclLoadCapDDCzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with the capability located in memory | |
| at \textbf{DDC}.\textbf{address} $+$ \emph{rs1}, and if \textbf{DDC}.\textbf{perms} does not grant | |
| -\textbf{Permit\_Load\_Capability} then \emph{cd}.\textbf{tag} is cleared. | |
| - | |
| -\subsection*{Exceptions} | |
| - | |
| +\textbf{Permit_Load_Capability} then \emph{cd}.\textbf{tag} is cleared. | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \textbf{DDC}.\textbf{tag} is not set. | |
| \item \textbf{DDC} is sealed. | |
| -\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit\_Load}. | |
| +\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit_Load}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $\lt$ \textbf{DDC}.\textbf{base}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $+$ \textbf{CLEN} $/$ 8 $\gt$ \textbf{DDC}.\textbf{top}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} is unaligned, regardless of whether the | |
| - implementation supports unaligned data accesses. | |
| - | |
| +implementation supports unaligned data accesses. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclLoadCapDDCzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclLoadCapCapexecute}{\saildoclabelled{sailRISCVfclLoadCapCapzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the capability located in memory | |
| +\newcommand{\sailRISCVfclLoadCapCapexecute}{\saildoclabelled{sailRISCVfclLoadCapCapzexecute}{\saildocfcl{ | |
| +Capability register \emph{cd} is replaced with the capability located in memory | |
| at \emph{cs1}.\textbf{address}, and if \emph{cs1}.\textbf{perms} does not grant | |
| -\textbf{Permit\_Load\_Capability} then \emph{cd}.\textbf{tag} is cleared. | |
| - | |
| -\subsection*{Exceptions} | |
| - | |
| +\textbf{Permit_Load_Capability} then \emph{cd}.\textbf{tag} is cleared. | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \emph{cs1}.\textbf{tag} is not set. | |
| \item \emph{cs1} is sealed. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Load}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Load}. | |
| \item \emph{cs1}.\textbf{address} $\lt$ \emph{cs1}.\textbf{base}. | |
| \item \emph{cs1}.\textbf{address} $+$ \textbf{CLEN} $/$ 8 $\gt$ \emph{cs1}.\textbf{top}. | |
| \item \emph{cs1}.\textbf{address} is unaligned, regardless of whether the implementation | |
| - supports unaligned data accesses. | |
| - | |
| +supports unaligned data accesses. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclLoadCapCapzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCLoadTagsexecute}{\saildoclabelled{sailRISCVfclCLoadTagszexecute}{\saildocfcl{Integer register \emph{rd} is replaced with the tags of the capabilities located | |
| +\newcommand{\sailRISCVfclCLoadTagsexecute}{\saildoclabelled{sailRISCVfclCLoadTagszexecute}{\saildocfcl{ | |
| +Integer register \emph{rd} is replaced with the tags of the capabilities located | |
| in memory at and above \emph{cs1}.\textbf{address}. The 0th bit corresponds to the | |
| first capability in memory. The result is coherent with other processors, as | |
| if the corresponding data words had also been loaded. The number of tags | |
| @@ -6800,52 +6805,42 @@ return the tags held in an L1 cache line, and so we use the constant | |
| \hyperref[sailRISCVzcapszyperzycachezyline]{\lstinline{caps_per_cache_line}}. The number of tags loaded must be a power of two, at | |
| least 1, and no more than \textbf{XLEN}. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \emph{cs1}.\textbf{tag} is not set. | |
| \item \emph{cs1} is sealed. | |
| -\item \emph{cs1}.\textbf{perms} does not grant both \textbf{Permit\_Load} and | |
| - \textbf{Permit\_Load\_Capability}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant both \textbf{Permit_Load} and | |
| +\textbf{Permit_Load_Capability}. | |
| \item \emph{cs1}.\textbf{address} $\lt$ \emph{cs1}.\textbf{base}. | |
| \item \emph{cs1}.\textbf{address} $+$ \hyperref[sailRISCVzcapszyperzycachezyline]{\lstinline{caps_per_cache_line}} $\times$ \textbf{CLEN} $/$ 8 | |
| - $\gt$ \emph{cs1}.\textbf{top}. | |
| +$\gt$ \emph{cs1}.\textbf{top}. | |
| \item \emph{cs1}.\textbf{address} is unaligned. | |
| \item The page table entry for \emph{cs1}.\textbf{address} would cause the tag to be | |
| - cleared. | |
| +cleared. | |
| \end{itemize} | |
| - | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item In order to reduce DRAM traffic, implementations may choose to load only | |
| - the tags and not the corresponding data, and may wish to not evict other | |
| - cache lines by treating it as a non-temporal/streaming load. | |
| - | |
| +the tags and not the corresponding data, and may wish to not evict other | |
| +cache lines by treating it as a non-temporal/streaming load. | |
| \item Software can easily discover the number of tags loaded by an | |
| - implementation by storing a series of \textbf{XLEN} capabilities to an aligned | |
| - array and performing a \hyperref[sailRISCVzCLoadTags]{\lstinline{CLoadTags}} operation. This need only be done once. | |
| - | |
| +implementation by storing a series of \textbf{XLEN} capabilities to an aligned | |
| +array and performing a \hyperref[sailRISCVzCLoadTags]{\lstinline{CLoadTags}} operation. This need only be done once. | |
| \item For heterogeneous multi-core or multi-processor systems, all cores must | |
| - return the same number of tags, which will often be based on the smallest | |
| - cache line size in the system. | |
| - | |
| - | |
| -\item Unlike \hyperref[sailRISCVzLoadCapImm]{CLC}, this instruction traps if tags will always be | |
| - unset due to lacking \textbf{Permit\_Load\_Capability} or page table entry | |
| - permissions, since that is likely indicative of a software bug that could | |
| - lead to temporal safety vulnerabilities if capabilities are erroneously | |
| - missed. | |
| - | |
| - | |
| +return the same number of tags, which will often be based on the smallest | |
| +cache line size in the system. | |
| + | |
| +\item Unlike \hyperref[sailRISCVzLoadCapImm]{\lstinline{CLC}}, this instruction traps if tags will always be | |
| +unset due to lacking \textbf{Permit_Load_Capability} or page table entry | |
| +permissions, since that is likely indicative of a software bug that could | |
| +lead to temporal safety vulnerabilities if capabilities are erroneously | |
| +missed. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCLoadTagszexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| \newcommand{\sailRISCVfclLoadResDataDDCexecute}{\saildoclabelled{sailRISCVfclLoadResDataDDCzexecute}{\saildocfcl{}{\lstinputlisting[language=sail]{sail_latex_riscv/fclLoadResDataDDCzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| @@ -6858,163 +6853,147 @@ An exception is raised if: | |
| \newcommand{\sailRISCVfclLoadResCapModeexecute}{\saildoclabelled{sailRISCVfclLoadResCapModezexecute}{\saildocfcl{}{\lstinputlisting[language=sail]{sail_latex_riscv/fclLoadResCapModezexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclStoreDataDDCexecute}{\saildoclabelled{sailRISCVfclStoreDataDDCzexecute}{\saildocfcl{The byte, halfword, word or doubleword located in memory at | |
| +\newcommand{\sailRISCVfclStoreDataDDCexecute}{\saildoclabelled{sailRISCVfclStoreDataDDCzexecute}{\saildocfcl{ | |
| +The byte, halfword, word or doubleword located in memory at | |
| \textbf{DDC}.\textbf{address} $+$ \emph{rs1} is replaced with integer register \emph{rs2}. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \textbf{DDC}.\textbf{tag} is not set. | |
| \item \textbf{DDC} is sealed. | |
| -\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit\_Store}. | |
| +\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit_Store}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $\lt$ \textbf{DDC}.\textbf{base}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $+$ \emph{size} $\gt$ \textbf{DDC}.\textbf{top}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclStoreDataDDCzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclStoreDataCapexecute}{\saildoclabelled{sailRISCVfclStoreDataCapzexecute}{\saildocfcl{The byte, halfword, word or doubleword located in memory at | |
| +\newcommand{\sailRISCVfclStoreDataCapexecute}{\saildoclabelled{sailRISCVfclStoreDataCapzexecute}{\saildocfcl{ | |
| +The byte, halfword, word or doubleword located in memory at | |
| \emph{cs1}.\textbf{address} is replaced with integer register \emph{rs2}. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \emph{cs1}.\textbf{tag} is not set. | |
| \item \emph{cs1} is sealed. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Store}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Store}. | |
| \item \emph{cs1}.\textbf{address} $\lt$ \emph{cs1}.\textbf{base}. | |
| \item \emph{cs1}.\textbf{address} $+$ \emph{size} $\gt$ \emph{cs1}.\textbf{top}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclStoreDataCapzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclStoreCapDDCexecute}{\saildoclabelled{sailRISCVfclStoreCapDDCzexecute}{\saildocfcl{The capability located in memory at \textbf{DDC}.\textbf{address} $+$ \emph{rs1} is | |
| +\newcommand{\sailRISCVfclStoreCapDDCexecute}{\saildoclabelled{sailRISCVfclStoreCapDDCzexecute}{\saildocfcl{ | |
| +The capability located in memory at \textbf{DDC}.\textbf{address} $+$ \emph{rs1} is | |
| replaced with capability register \emph{cs2}. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \textbf{DDC}.\textbf{tag} is not set. | |
| \item \textbf{DDC} is sealed. | |
| -\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit\_Store}. | |
| -\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit\_Store\_Capability} and | |
| - \emph{cs2}.\textbf{tag} is set. | |
| -\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit\_Store\_Local\_Capability}, | |
| - \emph{cs2}.\textbf{tag} is set and \emph{cs2}.\textbf{perms} does not grant \textbf{Global}. | |
| +\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit_Store}. | |
| +\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit_Store_Capability} and | |
| +\emph{cs2}.\textbf{tag} is set. | |
| +\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit_Store_Local_Capability}, | |
| +\emph{cs2}.\textbf{tag} is set and \emph{cs2}.\textbf{perms} does not grant \textbf{Global}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $\lt$ \textbf{DDC}.\textbf{base}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $+$ \textbf{CLEN} $/$ 8 $\gt$ \textbf{DDC}.\textbf{top}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclStoreCapDDCzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclStoreCapCapexecute}{\saildoclabelled{sailRISCVfclStoreCapCapzexecute}{\saildocfcl{The capability located in memory at \emph{cs1}.\textbf{address} is replaced with | |
| +\newcommand{\sailRISCVfclStoreCapCapexecute}{\saildoclabelled{sailRISCVfclStoreCapCapzexecute}{\saildocfcl{ | |
| +The capability located in memory at \emph{cs1}.\textbf{address} is replaced with | |
| capability register \emph{cs2}. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| An exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \emph{cs1}.\textbf{tag} is not set. | |
| \item \emph{cs1} is sealed. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Store}. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Store\_Capability} and | |
| - \emph{cs2}.\textbf{tag} is set. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Store\_Local\_Capability}, | |
| - \emph{cs2}.\textbf{tag} is set and \emph{cs2}.\textbf{perms} does not grant \textbf{Global}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Store}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Store_Capability} and | |
| +\emph{cs2}.\textbf{tag} is set. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Store_Local_Capability}, | |
| +\emph{cs2}.\textbf{tag} is set and \emph{cs2}.\textbf{perms} does not grant \textbf{Global}. | |
| \item \emph{cs1}.\textbf{address} $\lt$ \emph{cs1}.\textbf{base}. | |
| \item \emph{cs1}.\textbf{address} $+$ \textbf{CLEN} $\gt$ \emph{cs1}.\textbf{top}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclStoreCapCapzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclLoadCapImmexecute}{\saildoclabelled{sailRISCVfclLoadCapImmzexecute}{\saildocfcl{In integer mode, capability register \emph{cd} is replaced with the capability | |
| +\newcommand{\sailRISCVfclLoadCapImmexecute}{\saildoclabelled{sailRISCVfclLoadCapImmzexecute}{\saildocfcl{ | |
| +In integer mode, capability register \emph{cd} is replaced with the capability | |
| located in memory at \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $+$ \emph{imm}, and if | |
| -\textbf{DDC}.\textbf{perms} does not grant \textbf{Permit\_Load\_Capability} then | |
| +\textbf{DDC}.\textbf{perms} does not grant \textbf{Permit_Load_Capability} then | |
| \emph{cd}.\textbf{tag} is cleared. In capability mode, capability register \emph{cd} is | |
| replaced with the capability located in memory at \emph{cs1}.\textbf{address} $+$ | |
| -\emph{imm}, and if \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Load\_Capability} then | |
| +\emph{imm}, and if \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Load_Capability} then | |
| \emph{cd}.\textbf{tag} is cleared. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| In integer mode, an exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \textbf{DDC}.\textbf{tag} is not set. | |
| \item \textbf{DDC} is sealed. | |
| -\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit\_Load}. | |
| +\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit_Load}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $+$ \emph{imm} $\lt$ \textbf{DDC}.\textbf{base}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $+$ \emph{imm} $+$ \textbf{CLEN} $/$ 8 $\gt$ | |
| - \textbf{DDC}.\textbf{top}. | |
| +\textbf{DDC}.\textbf{top}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $+$ \emph{imm} is unaligned, regardless of | |
| - whether the implementation supports unaligned data accesses. | |
| +whether the implementation supports unaligned data accesses. | |
| \end{itemize} | |
| - | |
| In capability mode, an exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \emph{cs1}.\textbf{tag} is not set. | |
| \item \emph{cs1} is sealed. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Load}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Load}. | |
| \item \emph{cs1}.\textbf{address} $+$ \emph{imm} $\lt$ \emph{cs1}.\textbf{base}. | |
| \item \emph{cs1}.\textbf{address} $+$ \emph{imm} $+$ \textbf{CLEN} $/$ 8 $\gt$ \emph{cs1}.\textbf{top}. | |
| \item \emph{cs1}.\textbf{address} $+$ \emph{imm} is unaligned, regardless of whether the | |
| - implementation supports unaligned data accesses. | |
| - | |
| +implementation supports unaligned data accesses. | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclLoadCapImmzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclStoreCapImmexecute}{\saildoclabelled{sailRISCVfclStoreCapImmzexecute}{\saildocfcl{In integer mode, the capability located in memory at \textbf{DDC}.\textbf{address} $+$ | |
| +\newcommand{\sailRISCVfclStoreCapImmexecute}{\saildoclabelled{sailRISCVfclStoreCapImmzexecute}{\saildocfcl{ | |
| +In integer mode, the capability located in memory at \textbf{DDC}.\textbf{address} $+$ | |
| \emph{rs1} $+$ \emph{imm} is replaced with capability register \emph{cs2}. In capability | |
| mode, the capability located in memory at \emph{cs1}.\textbf{address} $+$ \emph{imm} is | |
| replaced with capability register \emph{cs2}. | |
| -\subsection*{Exceptions} | |
| - | |
| - | |
| +\subsection*{Exceptions\n | |
| In integer mode, an exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \textbf{DDC}.\textbf{tag} is not set. | |
| \item \textbf{DDC} is sealed. | |
| -\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit\_Store}. | |
| -\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit\_Store\_Capability} and | |
| - \emph{cs2}.\textbf{tag} is set. | |
| -\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit\_Store\_Local\_Capability}, | |
| - \emph{cs2}.\textbf{tag} is set and \emph{cs2}.\textbf{perms} does not grant \textbf{Global}. | |
| +\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit_Store}. | |
| +\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit_Store_Capability} and | |
| +\emph{cs2}.\textbf{tag} is set. | |
| +\item \textbf{DDC}.\textbf{perms} does not grant \textbf{Permit_Store_Local_Capability}, | |
| +\emph{cs2}.\textbf{tag} is set and \emph{cs2}.\textbf{perms} does not grant \textbf{Global}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $+$ \emph{imm} $\lt$ \textbf{DDC}.\textbf{base}. | |
| \item \textbf{DDC}.\textbf{address} $+$ \emph{rs1} $+$ \emph{imm} $+$ \textbf{CLEN} $/$ 8 $\gt$ | |
| - \textbf{DDC}.\textbf{top}. | |
| +\textbf{DDC}.\textbf{top}. | |
| \end{itemize} | |
| - | |
| In capability mode, an exception is raised if: | |
| - | |
| \begin{itemize} | |
| \item \emph{cs1}.\textbf{tag} is not set. | |
| \item \emph{cs1} is sealed. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Store}. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Store\_Capability} and | |
| - \emph{cs2}.\textbf{tag} is set. | |
| -\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit\_Store\_Local\_Capability}, | |
| - \emph{cs2}.\textbf{tag} is set and \emph{cs2}.\textbf{perms} does not grant \textbf{Global}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Store}. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Store_Capability} and | |
| +\emph{cs2}.\textbf{tag} is set. | |
| +\item \emph{cs1}.\textbf{perms} does not grant \textbf{Permit_Store_Local_Capability}, | |
| +\emph{cs2}.\textbf{tag} is set and \emph{cs2}.\textbf{perms} does not grant \textbf{Global}. | |
| \item \emph{cs1}.\textbf{address} $+$ \emph{imm} $\lt$ \emph{cs1}.\textbf{base}. | |
| \item \emph{cs1}.\textbf{address} $+$ \emph{imm} $+$ \textbf{CLEN} $/$ 8 $\gt$ \emph{cs1}.\textbf{top}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclStoreCapImmzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| \newcommand{\sailRISCVfclStoreCondDataDDCexecute}{\saildoclabelled{sailRISCVfclStoreCondDataDDCzexecute}{\saildocfcl{}{\lstinputlisting[language=sail]{sail_latex_riscv/fclStoreCondDataDDCzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| @@ -7029,120 +7008,111 @@ In capability mode, an exception is raised if: | |
| \newcommand{\sailRISCVfclAMOSwapCapexecute}{\saildoclabelled{sailRISCVfclAMOSwapCapzexecute}{\saildocfcl{}{\lstinputlisting[language=sail]{sail_latex_riscv/fclAMOSwapCapzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCUnderscoreCLCexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCLCzexecute}{\saildocfcl{Compressed 16-bit encoding for \hyperref[sailRISCVzLoadCapImm]{CLC}. | |
| - | |
| -\subsection*{Notes} | |
| - | |
| +\newcommand{\sailRISCVfclCUnderscoreCLCexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCLCzexecute}{\saildocfcl{ | |
| +Compressed 16-bit encoding for \hyperref[sailRISCVzLoadCapImm]{\lstinline{CLC}}. | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item This instruction is only available in capability encoding mode. | |
| \item For RV32 this replaces the encoding of \hyperref[sailRISCVzCzEFLW]{\lstinline{C.FLW}}, RV64 uses \hyperref[sailRISCVzCzEFLD]{\lstinline{C.FLD}}. | |
| - | |
| \end{itemize} | |
| -}{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnderscoreCLCzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCUnderscoreCLCSPexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCLCSPzexecute}{\saildocfcl{Compressed 16-bit encoding for a stack-pointer-relative \hyperref[sailRISCVzLoadCapImm]{CLC}. | |
| - | |
| -\subsection*{Notes} | |
| +}{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnderscoreCLCzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| +\newcommand{\sailRISCVfclCUnderscoreCLCSPexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCLCSPzexecute}{\saildocfcl{ | |
| +Compressed 16-bit encoding for a stack-pointer-relative \hyperref[sailRISCVzLoadCapImm]{\lstinline{CLC}}. | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item This instruction is only available in capability encoding mode. | |
| \item For RV32 this replaces the encoding of \hyperref[sailRISCVzCzEFLWSP]{\lstinline{C.FLWSP}}, RV64 uses \hyperref[sailRISCVzCzEFLDSP]{\lstinline{C.FLDSP}}. | |
| \item The encoding with \lstinline`cd == 0` is reserved and will raise an illegal | |
| - instruction trap. | |
| - | |
| +instruction trap. | |
| \end{itemize} | |
| -}{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnderscoreCLCSPzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| - | |
| -\newcommand{\sailRISCVfclCUnderscoreCSCexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCSCzexecute}{\saildocfcl{Compressed 16-bit encoding for \hyperref[sailRISCVzStoreCapImm]{CSC}. | |
| -\subsection*{Notes} | |
| +}{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnderscoreCLCSPzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| +\newcommand{\sailRISCVfclCUnderscoreCSCexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCSCzexecute}{\saildocfcl{ | |
| +Compressed 16-bit encoding for \hyperref[sailRISCVzStoreCapImm]{\lstinline{CSC}}. | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item This instruction is only available in capability encoding mode. | |
| \item For RV32 this replaces the encoding of \hyperref[sailRISCVzCzEFSW]{\lstinline{C.FSW}}, RV64 uses \hyperref[sailRISCVzCzEFSD]{\lstinline{C.FSD}}. | |
| - | |
| \end{itemize} | |
| -}{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnderscoreCSCzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| - | |
| -\newcommand{\sailRISCVfclCUnderscoreCSCSPexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCSCSPzexecute}{\saildocfcl{Compressed 16-bit encoding for a stack-pointer-relative \hyperref[sailRISCVzStoreCapImm]{CSC}. | |
| -\subsection*{Notes} | |
| +}{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnderscoreCSCzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| +\newcommand{\sailRISCVfclCUnderscoreCSCSPexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCSCSPzexecute}{\saildocfcl{ | |
| +Compressed 16-bit encoding for a stack-pointer-relative \hyperref[sailRISCVzStoreCapImm]{\lstinline{CSC}}. | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item This instruction is only available in capability encoding mode. | |
| \item For RV32 this replaces the encoding of \hyperref[sailRISCVzCzEFSWSP]{\lstinline{C.FSWSP}}, RV64 uses \hyperref[sailRISCVzCzEFSDSP]{\lstinline{C.FSDSP}}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnderscoreCSCSPzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCUnderscoreCIncOffsetOneSixCSPexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCIncOffsetOneSixCSPzexecute}{\saildocfcl{Compressed 16-bit encoding for \hyperref[sailRISCVzCIncOffsetImmediate]{\lstinline{CIncOffsetImmediate}} with source and | |
| +\newcommand{\sailRISCVfclCUnderscoreCIncOffsetOneSixCSPexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCIncOffsetOneSixCSPzexecute}{\saildocfcl{ | |
| +Compressed 16-bit encoding for \hyperref[sailRISCVzCIncOffsetImmediate]{\lstinline{CIncOffsetImmediate}} with source and | |
| destination registers set to \lstinline`csp` and an immediate scaled by 16. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item This instruction is only available in capability encoding mode. | |
| \item This instruction replaces the encoding of \hyperref[sailRISCVzCzEADDI16SP]{\lstinline{C.ADDI16SP}}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnderscoreCIncOffsetOneSixCSPzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCUnderscoreCIncOffsetFourCSPNexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCIncOffsetFourCSPNzexecute}{\saildocfcl{Compressed 16-bit encoding for \hyperref[sailRISCVzCIncOffsetImmediate]{\lstinline{CIncOffsetImmediate}} with the source register | |
| +\newcommand{\sailRISCVfclCUnderscoreCIncOffsetFourCSPNexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCIncOffsetFourCSPNzexecute}{\saildocfcl{ | |
| +Compressed 16-bit encoding for \hyperref[sailRISCVzCIncOffsetImmediate]{\lstinline{CIncOffsetImmediate}} with the source register | |
| set to \lstinline`csp` and an immediate scaled by 4. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item This instruction is only available in capability encoding mode. | |
| \item This instruction replaces the encoding of \hyperref[sailRISCVzCzEADDI4SPN]{\lstinline{C.ADDI4SPN}}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnderscoreCIncOffsetFourCSPNzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCUnderscoreCJALRexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCJALRzexecute}{\saildocfcl{Compressed 16-bit encoding for \hyperref[sailRISCVzCJALR]{\lstinline{CJALR}} with the destination register set | |
| +\newcommand{\sailRISCVfclCUnderscoreCJALRexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCJALRzexecute}{\saildocfcl{ | |
| +Compressed 16-bit encoding for \hyperref[sailRISCVzCJALR]{\lstinline{CJALR}} with the destination register set | |
| to \lstinline`cra`. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item This instruction is only available in capability encoding mode. | |
| \item This instruction replaces the encoding of \hyperref[sailRISCVzCzEJALR]{\lstinline{C.JALR}}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnderscoreCJALRzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCUnderscoreCJRexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCJRzexecute}{\saildocfcl{Compressed 16-bit encoding for \hyperref[sailRISCVzCJALR]{\lstinline{CJALR}} with the source register set to | |
| +\newcommand{\sailRISCVfclCUnderscoreCJRexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCJRzexecute}{\saildocfcl{ | |
| +Compressed 16-bit encoding for \hyperref[sailRISCVzCJALR]{\lstinline{CJALR}} with the source register set to | |
| \lstinline`cnull` and destination register set to \lstinline`cra`. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item This instruction is only available in capability encoding mode. | |
| \item This instruction replaces the encoding of \hyperref[sailRISCVzCzEJR]{\lstinline{C.JR}}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnderscoreCJRzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| -\newcommand{\sailRISCVfclCUnderscoreCJALexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCJALzexecute}{\saildocfcl{Compressed 16-bit encoding for \hyperref[sailRISCVzCJAL]{\lstinline{CJAL}} with the destination register set | |
| +\newcommand{\sailRISCVfclCUnderscoreCJALexecute}{\saildoclabelled{sailRISCVfclCUnderscoreCJALzexecute}{\saildocfcl{ | |
| +Compressed 16-bit encoding for \hyperref[sailRISCVzCJAL]{\lstinline{CJAL}} with the destination register set | |
| to \lstinline`cra`. | |
| -\subsection*{Notes} | |
| - | |
| - | |
| +\subsection*{Notes\n | |
| \begin{itemize} | |
| \item This instruction is only available in capability encoding mode. | |
| \item This instruction is only available in RV32. | |
| \item This instruction replaces the encoding of \hyperref[sailRISCVzCzEJAL]{\lstinline{C.JAL}}. | |
| - | |
| \end{itemize} | |
| + | |
| }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCUnderscoreCJALzexecute33a689e3a631b9b905b85461d3814943.tex}}}} | |
| \newcommand{\sailRISCVfclNOTUnderscoreCAPMODEexecute}{\saildoclabelled{sailRISCVfclNOTUnderscoreCAPMODEzexecute}{\saildocfcl{}{\lstinputlisting[language=sail]{sail_latex_riscv/fclNOTUnderscoreCAPMODEzexecute33a689e3a631b9b905b85461d3814943.tex}}}} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment