From b3804688533e771075f1d76b10dfcb6cd3dd9f10 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 25 Jan 2024 17:18:39 +0100 Subject: [PATCH] reorder capability chapter Show the encoding first so it is easier to find. Signed-off-by: Axel Heider --- src/cap-description.adoc | 139 ++++++++++++++++++++------------------- 1 file changed, 71 insertions(+), 68 deletions(-) diff --git a/src/cap-description.adoc b/src/cap-description.adoc index c89d783c..854ab200 100644 --- a/src/cap-description.adoc +++ b/src/cap-description.adoc @@ -14,6 +14,37 @@ define XLENMAX to be widest XLEN that the implementation supports. XLENMAX without including the tag bit. The value of CLEN is always calculated based on XLENMAX regardless of the effective XLEN value. +[#section_cap_encoding] +=== Capability Encoding + +ifdef::cheri_v9_annotations[] +NOTE: *CHERI v9 Note:* The encoding changes eliminate the concept of the +in-memory format, and also increase precision for RV32. When EF=0, T and B +are now shifted right rather than left within the address. Also, the bounds +decoding for XLENMAX=32 uses a trick (see bit T8) to save one bit when encoding +the exponent. +endif::[] + +The components of a capability except the tag are encoded as shown in +xref:cap_encoding_xlen32[xrefstyle=short] for XLENMAX=32 and +xref:cap_encoding_xlen64[xrefstyle=short] for XLENMAX=64. Each memory location +or register able to hold a capability must also store the tag as out of band +information that software cannot directly set or clear. The capability metadata +is held in the most significant bits and the address is held in the least +significant bits. + +.Capability encoding for XLENMAX=32 +[#cap_encoding_xlen32] +include::img/cap-encoding-xlen32.edn[] + +.Capability encoding for XLENMAX=64 +[#cap_encoding_xlen64] +include::img/cap-encoding-xlen64.edn[] + +Reserved bits are available for future extensions to {cheri_base_ext_name}. + +NOTE: Reserved bits must be 0 in valid capabilities. + === Components of a Capability Capabilities contain the software accessible fields described in this section. @@ -39,6 +70,8 @@ _capability_ wide in this specification. [#section_cap_perms] ==== Architectural Permissions (AP) +===== Description + ifdef::cheri_v9_annotations[] WARNING: *CHERI v9 Note:* The permissions are encoded differently in this specification. @@ -74,7 +107,7 @@ Execute Permission (X):: Allow instruction execution. [#asr_perm,reftext="ASR-permission"] Access System Registers Permission (ASR):: Allow access to privileged CSRs. -===== Permission Encoding +===== Encoding The bit width of the permissions field depends on the value of XLENMAX as shown in xref:perms_bit_width[xrefstyle=short]. A {cap_rv32_perms_width}-bit vector @@ -191,7 +224,9 @@ also seals the return address capability (if any) since it is the entry point to the caller function. [#section_cap_bounds] -==== Bounds +==== Bounds (EF, T, TE, B, BE) + +===== Concept ifdef::cheri_v9_annotations[] NOTE: *CHERI v9 Note:* The bounds mantissa width is different in XLENMAX=32. @@ -261,52 +296,8 @@ xref:exp_bit_width[xrefstyle=short]. NOTE: The address and bounds must be representable in valid capabilities i.e. when the tag is set (see xref:section_cap_malformed[xrefstyle=short]). -==== Address - -XLENMAX integer value that encodes the byte-address of a memory location. - -.Address widths depending on XLENMAX -[#address_bit_width,options=header,align="center",width="55%"] -|============================================================================== -^| XLENMAX ^| Address width -^| 32 ^| {cap_rv32_addr_width} -^| 64 ^| {cap_rv64_addr_width} -|============================================================================== - -==== Reserved Bits - -Reserved bits available for future extensions to {cheri_base_ext_name}. - -NOTE: Reserved bits must be 0 in valid capabilities. - -[#section_cap_encoding] -=== Capability Encoding - -ifdef::cheri_v9_annotations[] -NOTE: *CHERI v9 Note:* The encoding changes eliminate the concept of the -in-memory format, and also increase precision for RV32. When EF=0, T and B -are now shifted right rather than left within the address. Also, the bounds -decoding for XLENMAX=32 uses a trick (see bit T8) to save one bit when encoding -the exponent. -endif::[] - -The components of a capability are encoded as shown in -xref:cap_encoding_xlen32[xrefstyle=short] and -xref:cap_encoding_xlen64[xrefstyle=short] when XLENMAX=32 and XLENMAX=64 -respectively. - -.Capability encoding when XLENMAX=32 -[#cap_encoding_xlen32] -include::img/cap-encoding-xlen32.edn[] - -.Capability encoding when XLENMAX=64 -[#cap_encoding_xlen64] -include::img/cap-encoding-xlen64.edn[] - -Each memory location or register able to hold a capability must also store the -tag as out of band information that software cannot directly set or clear. The -capability metadata is held in the most significant bits and the address -is held in the least significant bits. +[#section_cap_bounds_decoding] +===== Decoding The metadata is encoded in a compressed format cite:[woodruff2019cheri]. It uses a floating point representation to encode the bounds relative to the @@ -425,6 +416,38 @@ if ( (E < (CAP_MAX_E - 1)) & (t[XLENMAX: XLENMAX - 1] - b[XLENMAX - 1] > 1) ) That is, invert the most significant bit of _t_ if the decoded length of the capability is larger than E. +[#section_cap_malformed] +===== Malformed Bounds + +A capability is _malformed_ if its encoding does not describe a valid +capability because its bounds cannot be correctly decoded. The following check +indicates whether a capability is malformed. + +``` +malformedMSB = (E == CAP_MAX_E && B[MW - 1:MW - 2] != 0) + || (E == CAP_MAX_E - 1 && B[MW - 1] != 0) +malformedLSB = (E < 0) +malformed = !EF && (malformedMSB || malformedLSB) +``` + +NOTE: The check is for malformed _bounds_, so it does not include reserved +bits! + +Capabilities with malformed bounds are always invalid anywhere in the system +i.e. their tags are always 0. + +==== Address + +XLENMAX integer value that encodes the byte-address of a memory location. + +.Address widths depending on XLENMAX +[#address_bit_width,options=header,align="center",width="55%"] +|============================================================================== +^| XLENMAX ^| Address width +^| 32 ^| {cap_rv32_addr_width} +^| 64 ^| {cap_rv64_addr_width} +|============================================================================== + [#section_special_caps] === Special Capabilities @@ -539,23 +562,3 @@ xref:section_cap_encoding[xrefstyle=short]. This gives useful guarantees, such that if an executed instruction is in <> bounds, then it is also guaranteed that the next linear instruction is _representable_. - -[#section_cap_malformed] -=== Malformed Capability Bounds - -A capability is _malformed_ if its encoding does not describe a valid -capability because its bounds cannot be correctly decoded. The following check -indicates whether a capability is malformed. - -``` -malformedMSB = (E == CAP_MAX_E && B[MW - 1:MW - 2] != 0) - || (E == CAP_MAX_E - 1 && B[MW - 1] != 0) -malformedLSB = (E < 0) -malformed = !EF && (malformedMSB || malformedLSB) -``` - -NOTE: The check is for malformed _bounds_, so it does not include reserved -bits! - -Capabilities with malformed bounds are always invalid anywhere in the system -i.e. their tags are always 0.