From fcce4a97354069f911540c6a0d0a6b8554b94429 Mon Sep 17 00:00:00 2001 From: Tariq Kurd Date: Mon, 4 Nov 2024 17:01:54 +0100 Subject: [PATCH] apply ACPERM rules in order (#427) Also update table to clarify the SL value for GCPERM. Fixes https://github.com/riscv/riscv-cheri/issues/426 Fixes https://github.com/riscv/riscv-cheri/issues/428 Signed-off-by: Tariq Kurd Co-authored-by: Alexander Richardson --- src/cap-description.adoc | 2 +- src/insns/acperm_32bit.adoc | 58 ++++++++++++++++++++----------------- src/level-ext.adoc | 10 ++++--- 3 files changed, 38 insertions(+), 32 deletions(-) diff --git a/src/cap-description.adoc b/src/cap-description.adoc index bb57434f..4392828b 100644 --- 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 index 421d8001..c2cfdc88 100644 --- a/src/insns/acperm_32bit.adoc +++ b/src/insns/acperm_32bit.adoc @@ -29,9 +29,9 @@ 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 <> field in `cs1` could not have been produced by <> then -clear all AP permissions and the <>, and skip the next step +clear all AP permissions, and the <> 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 <>. +. Encode the AP permissions for RV32 according to <>. . 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. + @@ -39,31 +39,35 @@ Some combinations of permissions cannot be encoded for MXLEN=32, and are not use 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: - -. <> cannot be set without <> being set -.. Clear <> unless <> is set -. <> cannot be set without at least one of <> or <> being set. -.. Clear <> unless <> or <> are set. -. <> cannot be set without <> being set -.. Clear <> unless <> is set -. <> cannot be set without <> being set -.. Clear <> unless <> is set. -. <> cannot be set without <> being set -.. Zero <> unless <> is set. -. <> cannot be set without <> being set -.. Zero <> unless <> is set. - -NOTE: The combination of <> clear and <> set is reserved for future extensions. - -The MXLEN=32 additional rules are: - -. Clear <> unless _all_ other permissions are set -. Clear <> and <> if <> is not set -. Clear <> if <> _is_ set, but <> _is not_ set. -. Clear <> if <> and <> are set, and <> and <> are both clear. -. If removing <> results in unrepresentable permissions, then set <> and <> only. +The rules from <> 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) | <> | All other permissions are set. +| 2 | <> | <> or <> +| 3 (RV32 only) | <> | <> +| 4 (RV32 only) | <> | <> +| 5 (RV32 only) | <> | not(<>) or <> +| 6 (RV32 only) | <> | <> or <> +| 7 | <> | <> and <> +| 8 | <> | <> and <> +| 9 | <> | <> +| 10 (RV32 only) | <> | (<> and <> and <> and (<> == ∞)) or + + (not(<> and not(<>) and not(<>) and (<>==0)))^1^ +| 11 | <> | <> +| 12 | <> | <> +|=== + +^1^ All the listed permissions in the set are either minimum or maximum. + +The behaviour of currently illegal combinations from <> is to clear the permission if invalid (or in the case of <> 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 <>, or +<> if <> is implemented. .Capability permissions bit field [#acperm_bit_field] diff --git a/src/level-ext.adoc b/src/level-ext.adoc index 14e1dbb4..a17457e2 100644 --- a/src/level-ext.adoc +++ b/src/level-ext.adoc @@ -74,14 +74,14 @@ endif::[] 11+| bit[0] - <> ({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 <>) -| 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 <>) +| 3 | ✔ | | ✔ | | | 0^1^ | | | N/A | Data & Cap R0 (without <>) | 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 <>) @@ -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 <> to simplify the rules followed by <> + [#section_cap_level_change] === Changing capability levels and permissions While capability levels (<>) are conceptually a label on the capability rather than a permission granted by the capability, they are adjusted using the <> instruction.