From 546635b6971deaa02a705dee77880c804ffb63cd Mon Sep 17 00:00:00 2001 From: Tariq Kurd Date: Tue, 23 Jan 2024 14:45:51 +0100 Subject: [PATCH 1/3] minor clarifications --- src/cap-description.adoc | 6 ++++++ src/riscv-integration.adoc | 2 ++ src/tables.adoc | 2 ++ 3 files changed, 10 insertions(+) diff --git a/src/cap-description.adoc b/src/cap-description.adoc index 94f22d10..fd4491c4 100644 --- a/src/cap-description.adoc +++ b/src/cap-description.adoc @@ -349,6 +349,12 @@ Decoding the bounds: top: t = { a[XLENMAX - 1:E + MW] + ct, T[MW - 1:0] , {E{1'b0}} } base: b = { a[XLENMAX - 1:E + MW] + cb, B[MW - 1:0] , {E{1'b0}} } ``` +NOTE: The representable range + is defined by the space beneath the bottom address bit (`a[E + MW]`) + in the expression above. If the capability address changes causing that address bit + to change, then the representable range is violated and so the tag will be cleared + by an instruction such as <>. This is represented by a range + of `s=2^E+MW^` in xref:cap_bounds_map[xrefstyle=short]. The corrections c~t~ and c~b~ are calculated as as shown below using the definitions in xref:cap_encoding_ct[xrefstyle=short] and diff --git a/src/riscv-integration.adoc b/src/riscv-integration.adoc index 9d55bd77..1fb5a035 100644 --- a/src/riscv-integration.adoc +++ b/src/riscv-integration.adoc @@ -1013,6 +1013,8 @@ Unlike machine and supervisor level CSRs, {cheri_base_ext_name} does not require The <> is made visible in a CSR. This provides access to an <> capability while in debug mode without executing <>. +<> resets to the <> with the address field set to the core boot address. + NOTE: It is common for implementations to not allow executing *pc* relative instructions, such as <> or <>, in debug mode. diff --git a/src/tables.adoc b/src/tables.adoc index 53d86e60..7276481b 100644 --- a/src/tables.adoc +++ b/src/tables.adoc @@ -99,6 +99,8 @@ include::generated/csr_alias_action_table_body.adoc[] in within bounds of the capability written to `Xtvecc`. The check on writing must include the lowest (0 offset) and highest possible offset (e.g. 64 * XLENMAX bits where HICAUSE=16). +NOTE: _XLEN writing_ is only available if {cheri_mode_ext_name} is implemented. + NOTE: Implementations which allow misa.C to be writable need to legalise *Xepcc* on _reading_ if the misa.C value has changed since the value was written as this can cause the read value of bit [1] to change state. From f863793d9f9faacf2f8e3a93048397830ea2260d Mon Sep 17 00:00:00 2001 From: Tariq Kurd Date: Wed, 24 Jan 2024 14:21:50 +0100 Subject: [PATCH 2/3] overhaul representable region description --- src/cap-description.adoc | 75 ++++++++++++++++++++++----------- src/insns/auipcc_32bit.adoc | 2 +- src/insns/cincoffset_32bit.adoc | 2 +- src/insns/csetaddr_32bit.adoc | 2 +- src/riscv-integration.adoc | 10 ++--- 5 files changed, 58 insertions(+), 33 deletions(-) diff --git a/src/cap-description.adoc b/src/cap-description.adoc index fd4491c4..f6254023 100644 --- a/src/cap-description.adoc +++ b/src/cap-description.adoc @@ -349,13 +349,6 @@ Decoding the bounds: top: t = { a[XLENMAX - 1:E + MW] + ct, T[MW - 1:0] , {E{1'b0}} } base: b = { a[XLENMAX - 1:E + MW] + cb, B[MW - 1:0] , {E{1'b0}} } ``` -NOTE: The representable range - is defined by the space beneath the bottom address bit (`a[E + MW]`) - in the expression above. If the capability address changes causing that address bit - to change, then the representable range is violated and so the tag will be cleared - by an instruction such as <>. This is represented by a range - of `s=2^E+MW^` in xref:cap_bounds_map[xrefstyle=short]. - The corrections c~t~ and c~b~ are calculated as as shown below using the definitions in xref:cap_encoding_ct[xrefstyle=short] and xref:cap_encoding_cb[xrefstyle=short]. @@ -423,7 +416,7 @@ A capability whose bounds cover the entire address space has 0 base and top equals 2^XLENMAX^, i.e. _t_ is a XLENMAX + 1 bit value. However, _b_ is a XLENMAX bit value and the size mismatch introduces additional complications when decoding, so the following condition is required to correct _t_ for -capabilities whose representable region wraps the edge of the address +capabilities whose <> wraps the edge of the address space: ``` @@ -484,28 +477,60 @@ or 'root' capability. | Address | zeros | Capability address |============================================================================== -[#section_cap_representable_check] -=== Representable Limit Check +[#section_cap_representable_check, reftext="Representable Range"] +=== Representable Range Check + +The new address, after updating the address of a capability, is within the +_representable range_ if decompressing the capability's bounds with the +original and new addresses yields the same base and top addresses. -Pointer arithmetic on capabilities must be checked to ensure that the new -address is within the capability's representable region described in -xref:section_cap_encoding[xrefstyle=short]. The new address, after pointer -arithmetic, is within the representable region if decompressing the -capability's bounds with the original and new addresses yields the same base -and top addresses. In other words, given a capability with address _a_ and the +In other words, given a capability with address _a_ and the new address `a' = a + x`, the bounds _b_ and _t_ are decoded using _a_ and the new bounds _b'_ and _t'_ are decoded using _a'_. The new address is within the -capability's representable region if `b == b' && t == t'`. +capability's _representable range_ if `b == b' && t == t'`. + +Changing a capability's address to a value outside the _representable range_ +unconditionally clears the capability's tag. Examples are: + +* Instructions such as <> which include pointer arithmetic. +* The <> instruction which updates the capability address field. -Changing a capability's address to a value outside the representable region -unconditionally clears the capability's tag. +==== Practical Information -NOTE: The encoding of the bounds depends upon the leading 1 of the address -which is used to determine the exponent. If the leading 1 of the address moves -then the bounds will need to be recalculated. Instructions like <> -and <> update the address field but do not recalculate the bounds. -Therefore, if the leading 1 moves relative to when the bounds were calculated -then the tag is cleared on the result as the encoding has been invalidated. +In the bounds encoding in this specification, the top and bottom capability +bounds are formed of two or three sections: + +* Upper bits from the address +* Middle bits from T and B decoded from the metadata +* Lower bits are set to zero +** This is only if there is an embedded exponent (EF=0) + +.Composition of address bounds +[#comp_addr_bounds,options=header,align="center"] +|============================================================================== +| Configuration | Upper section | Middle Section | Lower section +| EF=0, E varies | address[XLENMAX-1:E + MW] + ct | T[MW - 1:0] | {E{1'b0}} +| EF=1, i.e. E=0 | address[XLENMAX:MW] + ct 2+| T[MW - 1:0] +|============================================================================== + +The _representable range_ defines the range of addresses which do not corrupt +the bounds encoding. The encoding was first introduced in +xref:section_cap_encoding[xrefstyle=short], and is repeated in a different +form in xref:comp_addr_bounds[xrefstyle=short] to aid this description. + +For the address to be valid for the current bounds encoding, the address +bits in the _Upper Section_ of xref:comp_addr_bounds[xrefstyle=short] _must +not change_ as this will change the meaning of the bounds. + +This gives a range of `s=2^E+MW^`, which as shown in +xref:cap_bounds_map[xrefstyle=short]. + +The gap between the bounds of the representable range is always guaranteed +to be at least 1/8 of `s`. This is represented by `R = Bc - 1` in +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 diff --git a/src/insns/auipcc_32bit.adoc b/src/insns/auipcc_32bit.adoc index df3eb60b..f26daa7b 100644 --- a/src/insns/auipcc_32bit.adoc +++ b/src/insns/auipcc_32bit.adoc @@ -25,7 +25,7 @@ Form a 32-bit offset from the 20-bit immediate filling the lowest 12 bits with zeros. Increment the address of the <> instruction's <> by the 32-bit offset, then write the output capability to `cd`. The tag bit of the output capability is 0 if the incremented address is outside the <>'s -representable region. +<>. Legacy Mode Description:: Form a 32-bit offset from the immediate, filling in the lowest 12 bits with diff --git a/src/insns/cincoffset_32bit.adoc b/src/insns/cincoffset_32bit.adoc index 47de686d..6ae8dadb 100644 --- a/src/insns/cincoffset_32bit.adoc +++ b/src/insns/cincoffset_32bit.adoc @@ -31,7 +31,7 @@ cleared by <>. Description:: Increment the address field of the capability `cs1` and write the result to `cd` . The tag bit of the output capability is 0 if `cs1` did not have its tag -set to 1, the incremented address is outside `cs1` 's representable region or +set to 1, the incremented address is outside `cs1` 's <> or `cs1` is sealed. + For <>, the address is incremented by the value in `rs2` . + diff --git a/src/insns/csetaddr_32bit.adoc b/src/insns/csetaddr_32bit.adoc index 2a39a4f5..df546a30 100644 --- a/src/insns/csetaddr_32bit.adoc +++ b/src/insns/csetaddr_32bit.adoc @@ -17,7 +17,7 @@ include::wavedrom/csetaddr.adoc[] Description:: Set the address field of capability `cs1` to `rs2` and write the output capability to `cd`. The tag bit of the output capability is 0 if `cs1` did not -have its tag set to 1, `rs1` is outside the representable range of `cs1` +have its tag set to 1, `rs1` is outside the <> of `cs1` or if `cs1` is sealed. Prerequisites:: diff --git a/src/riscv-integration.adoc b/src/riscv-integration.adoc index 1fb5a035..a4de06ca 100644 --- a/src/riscv-integration.adoc +++ b/src/riscv-integration.adoc @@ -24,8 +24,8 @@ data they protect. The memory address space is circular, so the byte at address 2^XLEN^ - 1 is adjacent to the byte at address zero. A capability's -representable region described in xref:section_cap_encoding[xrefstyle=short] is -also circular, so address 0 is within the representable region of a capability +<> described in xref:section_cap_encoding[xrefstyle=short] is +also circular, so address 0 is within the <> of a capability where address 2^XLENMAX^ - 1 is within the bounds. [#section_riscv_programmers_model] @@ -207,7 +207,7 @@ build <>-relative capabilities. <> forms a 32-bit offset from the 2 immediate and filling the lowest 12 bits with zeros. The <> address is then incremented by the offset and a representability check is performed so the capability's tag is cleared if the new address is outside the <>'s -representable region. The resulting CLEN value along with the new tag are +<>. The resulting CLEN value along with the new tag are written to a *c* register. ==== Control Transfer Instructions @@ -298,7 +298,7 @@ xref:csr-numbers-section[xrefstyle=short]. Reading or writing any part of a CLEN-bit CSR may cause side-effects. For example, the CSR's tag bit may be cleared if a new address -is outside the representable region of a CSR capability being written. +is outside the <> of a CSR capability being written. This section describes how the CSR instructions operate on these CSRs in {cheri_base_ext_name}. @@ -564,7 +564,7 @@ Capabilities written to <> must be legalised by implicitly zeroing bit either 16 or 32, then whenever IALIGN=32, the capability read from <> must be legalised by implicitly zeroing bit **mepcc[1]**. Therefore, the capability read or written has its tag bit cleared if the legalised address is -not within the representable region. +not within the <>. NOTE: When reading or writing a sealed capability in <>, the tag is not cleared if the original address equals the legalized From cbdb693486b2db082ba8684f61a7b7ed99c5e501 Mon Sep 17 00:00:00 2001 From: Tariq Kurd Date: Wed, 24 Jan 2024 15:48:48 +0100 Subject: [PATCH 3/3] fix comments --- src/cap-description.adoc | 2 +- src/riscv-integration.adoc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cap-description.adoc b/src/cap-description.adoc index f6254023..b53acc8b 100644 --- a/src/cap-description.adoc +++ b/src/cap-description.adoc @@ -509,7 +509,7 @@ bounds are formed of two or three sections: [#comp_addr_bounds,options=header,align="center"] |============================================================================== | Configuration | Upper section | Middle Section | Lower section -| EF=0, E varies | address[XLENMAX-1:E + MW] + ct | T[MW - 1:0] | {E{1'b0}} +| EF=0, i.e. E>0 | address[XLENMAX-1:E + MW] + ct | T[MW - 1:0] | {E{1'b0}} | EF=1, i.e. E=0 | address[XLENMAX:MW] + ct 2+| T[MW - 1:0] |============================================================================== diff --git a/src/riscv-integration.adoc b/src/riscv-integration.adoc index a4de06ca..38e61195 100644 --- a/src/riscv-integration.adoc +++ b/src/riscv-integration.adoc @@ -1013,7 +1013,7 @@ Unlike machine and supervisor level CSRs, {cheri_base_ext_name} does not require The <> is made visible in a CSR. This provides access to an <> capability while in debug mode without executing <>. -<> resets to the <> with the address field set to the core boot address. +<> resets to the <> capability with the address field set to the core boot address. NOTE: It is common for implementations to not allow executing *pc* relative instructions, such as <> or <>, in debug mode.