apply ACPERM rules in order (#427)

Also update table to clarify the SL value for GCPERM. Fixes #426 Fixes #428 Signed-off-by: Tariq Kurd <[email protected]> Co-authored-by: Alexander Richardson <[email protected]>
riscv · Nov 4, 2024 · fcce4a9 · fcce4a9
1 parent 9561fff
commit fcce4a9
Show file tree

Hide file tree

Showing 3 changed files with 38 additions and 32 deletions.
diff --git a/src/cap-description.adoc b/src/cap-description.adoc
@@ -30,7 +30,7 @@ specifications must provide key primitives, such as permissions and bounds,
 from this specification while using a different encoding that, for example,
 changes the granularity of bounds or adds new features. For simplicity of
 expression, the text is written as if this was the only possible capability
-encoding possible for CHERI RISC-V.
+encoding for CHERI RISC-V.
 
 [#section_cap_encoding]
 === Capability Encoding

diff --git a/src/insns/acperm_32bit.adoc b/src/insns/acperm_32bit.adoc
@@ -29,41 +29,45 @@ ACPERM performs the following operations:
 format shown in xref:acperm_bit_field[xrefstyle=short].
 . Calculate the bitwise AND of the bit field with the mask `rs2`.
 . If the AP and <<m_bit>> field in `cs1` could not have been produced by <<ACPERM>> then
-clear all AP permissions and the <<m_bit>>, and skip the next step
+clear all AP permissions, and the <<m_bit>> to {CAP_MODE_VALUE}. Skip the next step.
 . Clear AP permissions as required to meet the rules below.
-. Encode the AP permissions for MXLEN=32 according to <<cap_perms_encoding32>>.
+. Encode the AP permissions for RV32 according to <<cap_perms_encoding32>>.
 . Copy `cs1` to `cd`, and update the AP and SDP fields with the newly calculated versions.
 . Set `cd.tag=0` if `cs1` is sealed or if any reserved fields of `cs1` are set.
 +
 Some combinations of permissions cannot be encoded for MXLEN=32, and are not useful when MXLEN=64.
 These cases are defined to return useful minimal sets of permissions, which may be no permissions.
 +
 NOTE: Future extensions may allow more combinations of permissions, especially for MXLEN=64.
-
-The common rules are:
-
-. <<asr_perm>> cannot be set without <<x_perm>> being set
-.. Clear <<asr_perm>> unless <<x_perm>> is set
-. <<c_perm>> cannot be set without at least one of <<r_perm>> or <<w_perm>> being set.
-.. Clear <<c_perm>> unless <<r_perm>> or <<w_perm>> are set.
-. <<m_bit>> cannot be set without <<x_perm>> being set
-.. 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 <<el_perm>> unless <<c_perm>> is set.
-
-NOTE: The combination of <<x_perm>> clear and <<m_bit>> set is reserved for future extensions.
-
-The MXLEN=32 additional rules are:
-
-. Clear <<asr_perm>> unless _all_ other permissions are set
-. Clear <<c_perm>> and <<x_perm>> if <<r_perm>> is not set
-. Clear <<w_perm>> if <<c_perm>> _is_ set, but <<lm_perm>> _is not_ set.
-. Clear <<x_perm>> if <<x_perm>> and <<r_perm>> are set, and <<c_perm>> and <<w_perm>> are both clear.
-. If removing <<lm_perm>> results in unrepresentable permissions, then set <<r_perm>> and <<c_perm>> only.
+The rules from <<acperm_rules>> must be followed when removing permissions.
+
+[#acperm_rules]
+.ACPERM common rules
+[float="center",align="center",cols="2,2,4",options="header"]
+|===
+| Rule            | Permission   | Only valid if
+|  1  (RV32 only) | <<asr_perm>> | All other permissions are set.
+|  2              | <<c_perm>>   | <<r_perm>> or <<w_perm>>
+|  3  (RV32 only) | <<c_perm>>   | <<r_perm>>
+|  4  (RV32 only) | <<x_perm>>   | <<r_perm>>
+|  5  (RV32 only) | <<w_perm>>   | not(<<c_perm>>) or <<lm_perm>>
+|  6  (RV32 only) | <<x_perm>>   | <<w_perm>> or <<c_perm>>
+|  7              | <<el_perm>>  | <<c_perm>> and <<r_perm>>
+|  8              | <<lm_perm>>  | <<c_perm>> and <<r_perm>>
+|  9              | <<sl_perm>>  | <<c_perm>>
+| 10  (RV32 only) | <<x_perm>>   | (<<c_perm>> and <<lm_perm>> and <<el_perm>> and (<<sl_perm>> == ∞)) or +
+                                   (not(<<c_perm>> and not(<<lm_perm>>) and not(<<el_perm>>) and (<<sl_perm>>==0)))^1^
+| 11              | <<asr_perm>> | <<x_perm>>
+| 12              | <<m_bit>>    | <<x_perm>>
+|===
+
+^1^ All the listed permissions in the set are either minimum or maximum.
+
+The behaviour of currently illegal combinations from <<acperm_rules>> is to clear the permission if invalid (or in the case of <<sl_perm>> set it to 0 (_local_)).
+
+* For RV64 all such combinations may be redefined by future extensions.
+* The RV32 only rules are added because they remove combinations which do not meet the encoding requirements for <<cap_perms_encoding32>>, or
+<<cap_perms_encoding_levels32>> if <<cheri_levels_ext,{cheri_levels_ext_name}>> is implemented.
 
 .Capability permissions bit field
 [#acperm_bit_field]

diff --git a/src/level-ext.adoc b/src/level-ext.adoc
@@ -74,14 +74,14 @@ endif::[]
 11+| bit[0] - <<m_bit>> ({CAP_MODE_VALUE}-{cheri_cap_mode_name}, {INT_MODE_VALUE}-{cheri_int_mode_name})
 |Bits[4:3]| R | W | C | LM | EL | SL  | X | ASR | Mode^1^ |
 | 0-1   | ✔ | ✔ | ✔ | ✔  | ✔  | ∞   | ✔ |  ✔  | Mode^1^  | Execute + ASR (see <<infinite-cap>>)
-| 2-3   | ✔ |   | ✔ | ✔  | ✔  | ∞   | ✔ |     | Mode^1^  | Execute + Data & Cap RO
+| 2-3   | ✔ |   | ✔ | ✔  | ✔  | ∞^1^| ✔ |     | Mode^1^  | Execute + Data & Cap RO
 | 4-5   | ✔ | ✔ | ✔ | ✔  | ✔  | ∞   | ✔ |     | Mode^1^  | Execute + Data & Cap RW
-| 6-7   | ✔ | ✔ |   |    |    | N/A | ✔ |     | Mode^1^  | Execute + Data RW
+| 6-7   | ✔ | ✔ |   |    |    | 0^1^| ✔ |     | Mode^1^  | Execute + Data RW
 11+| *Quadrant 2: Restricted capability data read/write*
 11+| bit[2] = write, bit[1:0] = store level. R and C implicitly granted, LM dependent on W permission.
 |Bits[4:3]| R | W | C | LM | EL | SL    | X | ASR | Mode^1^ |
 | 0-2   10+| reserved
-| 3       | ✔ |   | ✔ |    |    | N/A   |   |     | N/A | Data & Cap R0 (without <<lm_perm>>)
+| 3       | ✔ |   | ✔ |    |    | 0^1^  |   |     | N/A | Data & Cap R0 (without <<lm_perm>>)
 | 4       | ✔ | ✔ | ✔ | ✔  |    | _(3)_ |   |     | N/A | Reserved for `LVLBITS=2`
 | 5       | ✔ | ✔ | ✔ | ✔  |    | _(2)_ |   |     | N/A | Reserved for `LVLBITS=2`
 | 6       | ✔ | ✔ | ✔ | ✔  |    | 1     |   |     | N/A | Data & Cap RW (with store _local_, no <<el_perm>>)
@@ -91,13 +91,15 @@ endif::[]
 11+| _Reserved bits for future extensions must be 1 so they are implicitly granted_
 |Bits[4:3]| R | W | C | LM | EL | SL    | X | ASR | Mode^1^ |
 | 0-2   10+| reserved
-| 3       | ✔ |   | ✔ | ✔  | ✔  | N/A   |   |     | N/A | Data & Cap R0
+| 3       | ✔ |   | ✔ | ✔  | ✔  | 0^1^  |   |     | N/A | Data & Cap R0
 | 4       | ✔ | ✔ | ✔ | ✔  | ✔  | _(3)_ |   |     | N/A | Reserved for `LVLBITS=2`
 | 5       | ✔ | ✔ | ✔ | ✔  | ✔  | _(2)_ |   |     | N/A | Reserved for `LVLBITS=2`
 | 6       | ✔ | ✔ | ✔ | ✔  | ✔  | 1     |   |     | N/A | Data & Cap RW (with store _local_)
 | 7       | ✔ | ✔ | ✔ | ✔  | ✔  | 0     |   |     | N/A | Data & Cap RW (no store _local_)
 |==============================================================================
 
+^1^ SL isn't applicable in these cases, but this value is reported by <<GCPERM>> to simplify the rules followed by <<ACPERM>>
+
 [#section_cap_level_change]
 === Changing capability levels and permissions
 While capability levels (<<section_cap_level,CL>>) are conceptually a label on the capability rather than a permission granted by the capability, they are adjusted using the <<ACPERM>> instruction.