Merge branch 'main' into 202410-reserve-ls-c0

Signed-off-by: Tariq Kurd <[email protected]>

Makefile

@@ -18,7 +18,7 @@ GEN_SCRIPT   = $(SCRIPTS_DIR)/generate_tables.py
 
 # Version and date
 DATE    ?= $(shell date +%Y-%m-%d)
-VERSION ?= v0.8.3
+VERSION ?= v0.9.0
 REVMARK ?= Draft
 
 # URLs for downloaded CSV files

src/attributes.adoc

@@ -46,6 +46,8 @@ endif::[]
 :cheri_default_ext_name:   Zcherihybrid
 // Extension for CHERI PTE bits
 :cheri_pte_ext_name:       Zcheripte
+// Extension for capability levels (flow control)
+:cheri_levels_ext_name:             Zcherilevels
 // Extension for thread identification
 :tid_ext_name:             Zstid
 
@@ -77,7 +79,10 @@ endif::[]
 :cap_rv32_mw_width:    10
 :cap_rv64_mw_width:    14
 :cap_rv32_perms_width:  5
+//including Zcherilevels, 6 without
 :cap_rv64_perms_width:  6
+//CL is not a permission, so 8 not 9
+:cap_rv64_perms_levels_width:  8
 :cap_rv32_addr_width:  32
 :cap_rv64_addr_width:  64
 :cap_rv32_exp_width:    5

src/cap-description.adoc

@@ -60,6 +60,8 @@ Reserved bits are available for future extensions to {cheri_base_ext_name}.
 
 NOTE: Reserved bits must be 0 in tagged capabilities.
 
+NOTE: The CL field is only present if {cheri_levels_ext_name} is implemented, otherwise it is reserved.
+
 === Components of a Capability
 
 Capabilities contain the software accessible fields described in this section.
@@ -102,6 +104,7 @@ The byte-address of a memory location is encoded as MXLEN integer value.
 ifdef::cheri_v9_annotations[]
 WARNING: *CHERI v9 Note:* The permissions are encoded differently in this
 specification.
+Additionally, this specification incorporates permissions that were present in Morello and/or CHERIoT but not CHERI v9.
 endif::[]
 
 This field encodes architecturally defined permissions of the capability.
@@ -166,6 +169,8 @@ Therefore, it is only possible to encode a subset of all combinations.
 ^| 64    | {cap_rv64_perms_width} | Separate bits for each architectural permission.
 |==============================================================================
 
+NOTE: if {cheri_levels_ext_name} is supported then there are {cap_rv64_perms_levels_width} architectural permission bits.
+
 For MXLEN=32, the permissions encoding is split into four quadrants.
 The quadrant is taken from bits [4:3] of the permissions encoding.
 The meaning for bits [2:0] are shown in <<cap_perms_encoding32>> for each quadrant.
@@ -222,8 +227,8 @@ reserved values as if it were 0b00000 (no permissions). Future extensions may as
 meanings to the reserved bit patterns, in which case <<GCPERM>> is allowed to report a
 non-zero value.
 
-A {cap_rv64_perms_width}-bit vector encodes the permissions when MXLEN=64. In
-this case, there is a bit per permission as shown in
+A {cap_rv64_perms_width}-bit vector encodes the permissions when MXLEN=64 ({cap_rv64_perms_levels_width}-bit if {cheri_levels_ext_name} is supported).
+In this case, there is a bit per permission as shown in
 xref:cap_perms_encoding64[xrefstyle=short]. A permission is granted if its
 corresponding bit is set, otherwise the capability does not grant that
 permission.
@@ -240,8 +245,10 @@ permission.
 | 3   | <<x_perm>>
 | 4   | <<asr_perm>>
 | 5   | <<lm_perm>>
-//| 6   | <<m_bit>>
+| 6   | <<el_perm>>^1^
+| 7   | <<sl_perm>>^1^
 |==============================================================================
+^1^ This permission is only supported if the implementation supports <<section_ext_cheri_levels,{cheri_levels_ext_name}>>.
 
 The <<m_bit>> is only assigned meaning when the
 implementation supports {cheri_default_ext_name} _and_ <<x_perm>> is set.
@@ -617,8 +624,9 @@ or 'root' capability.
 | SDP           | ones  | Grants all permissions
 | AP (MXLEN=32) | 0x8/0x9^1^  (see xref:cap_perms_encoding32[xrefstyle=short])
                         | Grants all permissions
-| AP (MXLEN=64) | 0x3F (see xref:cap_perms_encoding64[xrefstyle=short])
+| AP (MXLEN=64) | 0xFF (see xref:cap_perms_encoding64[xrefstyle=short])
                         | Grants all permissions
+| CL            | one^2^| _Global_
 | CT            | zero  | Unsealed
 | EF            | zero  | Internal exponent format
 | L~8~          | zero  | Top address reconstruction bit (MXLEN=32 only)
@@ -636,6 +644,8 @@ or 'root' capability.
 * For MXLEN=32, the <<m_bit>> is set to {INT_MODE_VALUE} in the AP field, giving the value 0x9
 * For MXLEN=64, the <<m_bit>> is set to {INT_MODE_VALUE} in a separate M field which is _not shown_ in the table above.
 
+^2^ This field only exists if {cheri_levels_ext_name} is implemented.
+
 [#section_cap_representable_check, reftext="Representable Range"]
 === Representable Range Check
 

src/csv/CHERI_ISA.csv

@@ -52,8 +52,8 @@
 "GCTYPE","✔","✔","","","","✔","✔","Both","","","","","","","","","","","","","","","","","OP","1-src 1-dst","","","Get capability type","","","","","","","",""
 "SCMODE","✔","✔","","","","✔","","Both","","","","","","","","","","","","","","","","","OP","1-src 1-dst","","","Set the mode bit of a capability, no permissions required","","","","","","","",""
 "GCMODE","✔","✔","","","","✔","","Both","","","","","","","","","","","","","","","","","OP","1-src 1-dst","","","Get the mode bit of a capability, no permissions required","","","","","","","",""
-"MODESW","✔","✔","","","","✔","","Both","","","","","","","","","","","","","","","","","OP","no operands","","","Directly switch mode ({cheri_int_mode_name}/ {cheri_cap_mode_name})","mode==D (optional)","","","","","","",""
-"C.MODESW","✔","✔","","","","✔","","Both","","","","","","","","","","","","","","","","","C1","no operands","","","Directly switch mode ({cheri_int_mode_name}/ {cheri_cap_mode_name})","mode==D (optional)","","","","","","",""
+"MODESW.CAP","✔","✔","","","","✔","","Both","","","","","","","","","","","","","","","","","OP","no operands","","","Directly switch mode into {cheri_cap_mode_name}","","","","","","","",""
+"MODESW.INT","✔","✔","","","","✔","","Both","","","","","","","","","","","","","","","","","OP","no operands","","","Directly switch mode into {cheri_int_mode_name}","","","","","","","",""
 "C.ADDI16SP","✔","✔","","","","✔","✔","Both","","","","✔","","","","","","","","","","","","","C0","","","","ADD immediate to stack pointer, CADD in Capability Mode","","","","","","","",""
 "C.ADDI4SPN","✔","✔","","","","✔","✔","Both","","","","✔","","","","","","","","","","","","","C0","","","","ADD immediate to stack pointer, CADDI in Capability Mode","","","","","","","",""
 "C.MV","✔","✔","","","","✔","✔","Both","","","","✔","","","","","","","","","","","","","C2","","","","Register Move, cap reg move in Capability Mode","","","","","","","",""

src/debug-integration.adoc

@@ -108,8 +108,8 @@ include::img/dpccreg.edn[]
 Upon entry to debug mode, cite:[riscv-debug-spec], does not specify how to
 update the PC, and says PC relative instructions may be illegal. This concept
 is extended to include any instruction which reads or updates <<pcc>>, which refers to
-all jumps, conditional branches and <<AUIPC>>. The exception is <<MODESW>>
-which _is_ supported if {cheri_default_ext_name} is implemented, see <<dinfc>>
+all jumps, conditional branches and <<AUIPC>>. The exceptions are <<MODESW_CAP>> and <<MODESW_INT>>
+which _are_ supported if {cheri_default_ext_name} is implemented, see <<dinfc>>
 for details.
 
 As a result, the value of <<pcc>> is UNSPECIFIED in debug mode according
@@ -180,13 +180,12 @@ The reset value is the <<infinite-cap>> capability.
 If {cheri_default_ext_name} is implemented:
 
 * The <<m_bit>> is reset to {cheri_int_mode_name} ({INT_MODE_VALUE}).
-* The debugger can set the <<m_bit>> to {cheri_cap_mode_name} ({CAP_MODE_VALUE}) by executing <<MODESW>> from the program buffer
-** if <<MODESW>> is not supported in debug mode then the same can be done by reading the CSR, using <<SCMODE>> and then writing the CSR.
-** This only needs doing once after resetting the core.
-* The <<m_bit>> is used on debug mode entry to determine which CHERI execution mode to enter.
+* The debugger can set the <<m_bit>> to {cheri_cap_mode_name} ({CAP_MODE_VALUE}) by executing <<MODESW_CAP>> from the program buffer.
+** Executing <<MODESW_CAP>> causes subsequent instruction execution from the program buffer, starting from the next instruction, to be executed in {cheri_cap_mode_name}. It also sets the CHERI execution mode to {cheri_cap_mode_name} on future entry into debug mode.
+** Therefore to enable use of a CHERI debugger, a single <<MODESW_CAP>> only needs to be executed once from the program buffer after resetting the core.
+** The debugger can also execute <<MODESW_INT>> to change the mode back to {cheri_int_mode_name}, which also affects the execution of the next instruction in the program buffer, updates the <<m_bit>> of <<dinfc>> and controls which CHERI execution mode to enter on the next entry into debug mode.
 
-The <<m_bit>> is the only writeable field in <<dinfc>>.
-Therefore if {cheri_default_ext_name} is not implemented then it is read-write with no writeable fields.
+The <<m_bit>> of <<dinfc>> is _only_ updated by executing <<MODESW_CAP>> or <<MODESW_INT>> from the program buffer.
 
 NOTE: A future version of this specification may add writeable fields to allow creation
  of other capabilities, if, for example, a future extension requires multiple formats for

src/img/acperm_bit_field.edn

@@ -6,7 +6,7 @@
 (def left-margin 100)
 (def right-margin 100)
 (def boxes-per-row 32)
-(draw-column-headers {:height 20 :font-size 18 :labels (reverse ["0" "1" "2" "" "4" "5" "6" "" "" "SDPLEN+5" "" "" "" "" "" "15" "16" "17" "18" "19" "" "" "" "" "" "" "" "" "" "" "" "XLEN-1"])})
+(draw-column-headers {:height 20 :font-size 18 :labels (reverse ["0" "1" "2" "3" "4" "5" "6" "" "" "SDPLEN+5" "" "" "" "" "" "15" "16" "17" "18" "19" "" "" "" "" "" "" "" "" "" "" "" "XLEN-1"])})
 
 (draw-box "Reserved" {:span 13})
 (draw-box "R"        {:span 1})
@@ -15,18 +15,22 @@
 (draw-box "Reserved" {:span 6})
 (draw-box "SDP"      {:span 4})
 (draw-box "C"        {:span 1})
-(draw-box "Reserved" {:span 3})
+(draw-box "CL"       {:span 1})
+(draw-box "SL"       {:span 1})
+(draw-box "EL"       {:span 1})
 (draw-box "LM"       {:span 1})
 (draw-box "W"        {:span 1})
 
 (draw-box "XLEN-19"   {:span 13 :borders {}})
 (draw-box "1"         {:span 1 :borders {}})
 (draw-box "1"         {:span 1 :borders {}})
 (draw-box "1"         {:span 1 :borders {}})
-(draw-box "8"         {:span 6 :borders {}})
+(draw-box "10-SDPLEN" {:span 6 :borders {}})
 (draw-box "SDPLEN"    {:span 4 :borders {}})
 (draw-box "1"         {:span 1 :borders {}})
-(draw-box "3"         {:span 3 :borders {}})
+(draw-box "1"         {:span 1 :borders {}})
+(draw-box "1"         {:span 1 :borders {}})
+(draw-box "1"         {:span 1 :borders {}})
 (draw-box "1"         {:span 1 :borders {}})
 (draw-box "1"         {:span 1 :borders {}})
 ----

src/img/cap-encoding-xlen32.edn

@@ -6,11 +6,12 @@
 (def left-margin 100)
 (def right-margin 100)
 (def boxes-per-row 32)
-(draw-column-headers {:height 50 :font-size 22 :labels (reverse ["0" "1" "2" "" "" "" "" "" "" "9" "10" "11" "12" "" "" "" "" "17" "18" "19" "20" "21" "" "" "24" "25" "" "" "" "29" "30" "31"])})
+(draw-column-headers {:height 50 :font-size 22 :labels (reverse ["0" "1" "2" "" "" "" "" "" "" "9" "10" "11" "12" "" "" "" "" "17" "18" "19" "20" "21" "" "23" "24" "25" "" "" "" "29" "30" "31"])})
 
 (draw-box "SDP"         {:span 2})
 (draw-box "AP, M"       {:span 5})
-(draw-box "Reserved"    {:span 4})
+(draw-box "CL"          {:span 1})
+(draw-box "Reserved"    {:span 3})
 (draw-box "CT"          {:span 1})
 (draw-box "EF"          {:span 1})
 (draw-box "L8"          {:span 1})

src/img/cap-encoding-xlen64.edn

@@ -6,13 +6,14 @@
 (def left-margin 100)
 (def right-margin 100)
 (def boxes-per-row 32)
-(draw-column-headers {:height 50 :font-size 22 :labels (reverse ["0" "2" "3" "" "" "" "13" "14" "16" "17" "" "" "25" "26" "27" "28" "" "" "" "" "45" "46" "" "" "51" "52" "53" "56" "57" "" "" "63"])})
+(draw-column-headers {:height 50 :font-size 22 :labels (reverse ["0" "2" "3" "" "" "" "13" "14" "16" "17" "" "" "25" "26" "27" "28" "" "42" "43" "44" "" "" "" "" "51" "52" "53" "56" "57" "" "" "63"])})
 
 (draw-box "Reserved"    {:span 4})
 (draw-box "SDP"         {:span 2})
 (draw-box "M"           {:span 1})
-(draw-box "AP"          {:span 4})
-(draw-box "Reserved"    {:span 6})
+(draw-box "AP"          {:span 6})
+(draw-box "CL"          {:span 1})
+(draw-box "Reserved"    {:span 3})
 (draw-box "CT"          {:span 1})
 (draw-box "EF"          {:span 1})
 (draw-box "T[11:3]"     {:span 4})

src/img/htval2reg.edn

@@ -8,9 +8,9 @@
 (def boxes-per-row 32)
 (draw-column-headers {:height 20 :font-size 18 :labels (reverse ["0" "" "" "3" "4" "" "" "" "" "" "" "" "" "" "" "15" "16" "" "" "19" "20" "" "" "" "" "" "" "" "" "" "" "HSXLEN-1"])})
 
-(draw-box "Reserved"   {:span 12})
+(draw-box "WPRI"       {:span 12})
 (draw-box "TYPE"       {:span 4})
-(draw-box "Reserved"   {:span 12})
+(draw-box "WPRI"       {:span 12})
 (draw-box "CAUSE"      {:span 4})
 
 (draw-box "HSXLEN-20" {:span 12 :borders {}})

src/img/mtval2reg.edn

@@ -8,9 +8,9 @@
 (def boxes-per-row 32)
 (draw-column-headers {:height 20 :font-size 18 :labels (reverse ["0" "" "" "3" "4" "" "" "" "" "" "" "" "" "" "" "15" "16" "" "" "19" "20" "" "" "" "" "" "" "" "" "" "" "MXLEN-1"])})
 
-(draw-box "Reserved"   {:span 12})
+(draw-box "WPRI"       {:span 12})
 (draw-box "TYPE"       {:span 4})
-(draw-box "Reserved"   {:span 12})
+(draw-box "WPRI"       {:span 12})
 (draw-box "CAUSE"      {:span 4})
 
 (draw-box "MXLEN-20" {:span 12 :borders {}})

src/img/stval2reg.edn

@@ -8,9 +8,9 @@
 (def boxes-per-row 32)
 (draw-column-headers {:height 20 :font-size 18 :labels (reverse ["0" "" "" "3" "4" "" "" "" "" "" "" "" "" "" "" "15" "16" "" "" "19" "20" "" "" "" "" "" "" "" "" "" "" "SXLEN-1"])})
 
-(draw-box "Reserved"   {:span 12})
+(draw-box "WPRI"       {:span 12})
 (draw-box "TYPE"       {:span 4})
-(draw-box "Reserved"   {:span 12})
+(draw-box "WPRI"       {:span 12})
 (draw-box "CAUSE"      {:span 4})
 
 (draw-box "SXLEN-20" {:span 12 :borders {}})

src/img/vstval2reg.edn

@@ -8,9 +8,9 @@
 (def boxes-per-row 32)
 (draw-column-headers {:height 20 :font-size 18 :labels (reverse ["0" "" "" "3" "4" "" "" "" "" "" "" "" "" "" "" "15" "16" "" "" "19" "20" "" "" "" "" "" "" "" "" "" "" "VSXLEN-1"])})
 
-(draw-box "Reserved"   {:span 12})
+(draw-box "WPRI"       {:span 12})
 (draw-box "TYPE"       {:span 4})
-(draw-box "Reserved"   {:span 12})
+(draw-box "WPRI"       {:span 12})
 (draw-box "CAUSE"      {:span 4})
 
 (draw-box "VSXLEN-20" {:span 12 :borders {}})

src/insns/acperm_32bit.adoc

@@ -50,6 +50,10 @@ The common rules are:
 .. Clear <<m_bit>> unless <<x_perm>> is set
 . <<lm_perm>> cannot be set without <<c_perm>> being set
 .. Clear <<lm_perm>> unless <<c_perm>> is set.
+. <<sl_perm>> cannot be set without <<c_perm>> being set
+.. Zero <<sl_perm>> unless <<c_perm>> is set.
+. <<el_perm>> cannot be set without <<c_perm>> being set
+.. Zero <<sl_perm>> unless <<c_perm>> is set.
 
 NOTE: The combination of <<x_perm>> clear and <<m_bit>> set is reserved for future extensions.
 
@@ -64,6 +68,10 @@ The MXLEN=32 additional rules are:
 [#acperm_bit_field]
 include::../img/acperm_bit_field.edn[]
 
+NOTE: The <<el_perm,EL>>, <<sl_perm,SL>> and <<section_cap_level,CL>> fields are only defined if the implementation supports <<section_ext_cheri_levels,{cheri_levels_ext_name}>>.
+
+NOTE: Even though being included here <<section_cap_level,CL>> is not considered an architectural permission.
+
 Exceptions::
 include::require_cre.adoc[]
 

src/insns/atomic_exceptions.adoc

@@ -6,7 +6,9 @@ Requires <<r_perm>> and <<w_perm>> in the authorising capability.
 +
 If <<c_perm>> is not granted then store the memory tag as zero, and load `cd.tag` as zero.
 +
-If the authorizing capability does not grant <<lm_perm>>, and the tag of `cd` is 1 and `cd` is not sealed, then an implicit <<ACPERM>> clearing <<w_perm>> and <<lm_perm>> is performed to obtain the final permissions on `cd` (see <<LC>>).
+If the authorizing capability does not grant <<lm_perm>>, and the tag of `cd` is 1 and `cd` is not sealed, then an implicit <<ACPERM>> clearing <<w_perm>> and <<lm_perm>> is performed to obtain the intermediate permissions on `cd` (see <<LC>>).
++
+If the authorizing capability does not grant <<el_perm>>, and the tag of `cd` is 1, then an implicit <<ACPERM>> clearing <<el_perm>> and restricting <<section_cap_level>> to the level of the authorizing capability is performed to obtain the final permissions on `cd` (see <<LC>>).
 +
 endif::[]
 ifndef::cap_atomic[]

src/insns/auipc_32bit.adoc

@@ -6,6 +6,8 @@
 Synopsis::
 Add upper immediate to *pc*/<<pcc>>
 
+NOTE: CHERI extensions which use an alternative capability format may choose to redefine the handling of the immediate operand for this instruction in {cheri_cap_mode_name}.
+
 {cheri_cap_mode_name} Mnemonic::
 `auipc cd, imm`
 

src/insns/hypv-virt-loadx.adoc

@@ -5,21 +5,19 @@
 
 See <<HLVX_WU>>.
 
-<<<
-
 [#HLVX_WU,reftext="HLVX.WU"]
 ==== HLVX.WU
 
 Synopsis::
 Hypervisor virtual machine load from executable memory
 
 {cheri_cap_mode_name} Mnemonics::
-`hlv.hu rd, cs1` +
-`hlv.wu rd, cs1`
+`hlvx.hu rd, cs1` +
+`hlvx.wu rd, cs1`
 
 {cheri_int_mode_name} Mnemonics::
-`hlv.hu rd, rs1` +
-`hlv.wu rd, rs1`
+`hlvx.hu rd, rs1` +
+`hlvx.wu rd, rs1`
 
 Encoding::
 include::wavedrom/hypv-virt-loadx.adoc[]

src/insns/hypv-virt-store-cap.adoc

@@ -19,19 +19,17 @@ include::wavedrom/hypv-virt-store-cap.adoc[]
 Store a CLEN+1 bit value in `cs2` to memory as though V=1; i.e., with the
 address translation and protection, and endianness, that apply to memory
 accesses in either VS-mode or VU-mode. The effective address is the address of
-`cs1`. The authorising capability for the operation is `cs1`. The capability
-written to memory has the tag set to 0 if the tag of `cs2` is 0 or `cs1` does
-not grant <<c_perm>>.
+`cs1`. The authorising capability for the operation is `cs1`.
 +
 include::load_store_c0.adoc[]
 
 {cheri_int_mode_name} Description::
 Store a CLEN+1 bit value in `cs2` to memory as though V=1; i.e., with the
 address translation and protection, and endianness, that apply to memory
 accesses in either VS-mode or VU-mode. The effective address is the `rs1`. The
-authorising capability for the operation is <<ddc>>. The capability written to
-memory has the tag set to 0 if the tag of `cs2` is 0 or <<ddc>> does not grant
-<<c_perm>>.
+authorising capability for the operation is <<ddc>>.
+
+include::store_tag_perms.adoc[]
 
 include::malformed_no_check.adoc[]
 

src/insns/load_tag_perms.adoc

@@ -2,9 +2,14 @@ Resulting value of `cd`::
 The tag value written to `cd` is 0 if the tag of the memory location loaded is
 0 or the authorizing capability (<<ddc>> or `cs1`) does not grant <<c_perm>>.
 +
-If the authorizing capability does not grant <<lm_perm>>, and the tag of `cd` is 1 and `cd` is not sealed, then an implicit <<ACPERM>> clearing <<w_perm>> and <<lm_perm>> is performed to obtain the final permissions on `cd`.
+If the authorizing capability does not grant <<lm_perm>>, and the tag of `cd` is 1 and `cd` is not sealed, then an implicit <<ACPERM>> clearing <<w_perm>> and <<lm_perm>> is performed to obtain the intermediate permissions on `cd`.
++
+If the authorizing capability does not grant <<el_perm>>, and the tag of `cd` is 1, then an implicit <<ACPERM>> clearing <<el_perm>> and restricting <<section_cap_level>> to the level of the authorizing capability is performed to obtain the final permissions on `cd`.
 
 NOTE: Missing <<lm_perm>> does not affect untagged values since this could result in surprising bit patterns when copying non-capability data.
 Similarly, sealed capabilities are not modified as they are not directly dereferenceable.
 
+NOTE: Missing <<el_perm>> also affects the level of sealed capabilities since notionally the <<section_cap_level>> of a capability is not a permission but rather a data flow label attached to the loaded value.
+However, untagged values are not affected by <<el_perm>>.
+
 NOTE: While the implicit <<ACPERM>> introduces a dependency on the loaded data, microarchitectures can avoid this by deferring the actual masking of permissions until the loaded capability is dereferenced or the metadata bits are inspected using <<GCPERM>> or <<GCHI>>.