Skip to content

Commit 276f2ea

Browse files
author
Axel Heider
committed
reorder capability chapter
Show the encoding first so it is easier to find. Signed-off-by: Axel Heider <[email protected]>
1 parent e9f968f commit 276f2ea

File tree

1 file changed

+71
-68
lines changed

1 file changed

+71
-68
lines changed

src/cap-description.adoc

+71-68
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,37 @@ define XLENMAX to be widest XLEN that the implementation supports.
1414
XLENMAX without including the tag bit. The value of CLEN is always calculated
1515
based on XLENMAX regardless of the effective XLEN value.
1616

17+
[#section_cap_encoding]
18+
=== Capability Encoding
19+
20+
ifdef::cheri_v9_annotations[]
21+
NOTE: *CHERI v9 Note:* The encoding changes eliminate the concept of the
22+
in-memory format, and also increase precision for RV32. When EF=0, T and B
23+
are now shifted right rather than left within the address. Also, the bounds
24+
decoding for XLENMAX=32 uses a trick (see bit T8) to save one bit when encoding
25+
the exponent.
26+
endif::[]
27+
28+
The components of a capability except the tag are encoded as shown in
29+
xref:cap_encoding_xlen32[xrefstyle=short] for XLENMAX=32 and
30+
xref:cap_encoding_xlen64[xrefstyle=short] for XLENMAX=64. Each memory location
31+
or register able to hold a capability must also store the tag as out of band
32+
information that software cannot directly set or clear. The capability metadata
33+
is held in the most significant bits and the address is held in the least
34+
significant bits.
35+
36+
.Capability encoding for XLENMAX=32
37+
[#cap_encoding_xlen32]
38+
include::img/cap-encoding-xlen32.edn[]
39+
40+
.Capability encoding for XLENMAX=64
41+
[#cap_encoding_xlen64]
42+
include::img/cap-encoding-xlen64.edn[]
43+
44+
Reserved bits are available for future extensions to {cheri_base_ext_name}.
45+
46+
NOTE: Reserved bits must be 0 in valid capabilities.
47+
1748
=== Components of a Capability
1849

1950
Capabilities contain the software accessible fields described in this section.
@@ -39,6 +70,8 @@ _capability_ wide in this specification.
3970
[#section_cap_perms]
4071
==== Architectural Permissions (AP)
4172

73+
===== Description
74+
4275
ifdef::cheri_v9_annotations[]
4376
WARNING: *CHERI v9 Note:* The permissions are encoded differently in this
4477
specification.
@@ -74,7 +107,7 @@ Execute Permission (X):: Allow instruction execution.
74107
[#asr_perm,reftext="ASR-permission"]
75108
Access System Registers Permission (ASR):: Allow access to privileged CSRs.
76109

77-
===== Permission Encoding
110+
===== Encoding
78111

79112
The bit width of the permissions field depends on the value of XLENMAX as shown
80113
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
191224
to the caller function.
192225

193226
[#section_cap_bounds]
194-
==== Bounds
227+
==== Bounds (EF, T, TE, B, BE)
228+
229+
===== Concept
195230

196231
ifdef::cheri_v9_annotations[]
197232
NOTE: *CHERI v9 Note:* The bounds mantissa width is different in XLENMAX=32.
@@ -261,52 +296,8 @@ xref:exp_bit_width[xrefstyle=short].
261296
NOTE: The address and bounds must be representable in valid capabilities i.e.
262297
when the tag is set (see xref:section_cap_malformed[xrefstyle=short]).
263298

264-
==== Address
265-
266-
XLENMAX integer value that encodes the byte-address of a memory location.
267-
268-
.Address widths depending on XLENMAX
269-
[#address_bit_width,options=header,align="center",width="55%"]
270-
|==============================================================================
271-
^| XLENMAX ^| Address width
272-
^| 32 ^| {cap_rv32_addr_width}
273-
^| 64 ^| {cap_rv64_addr_width}
274-
|==============================================================================
275-
276-
==== Reserved Bits
277-
278-
Reserved bits available for future extensions to {cheri_base_ext_name}.
279-
280-
NOTE: Reserved bits must be 0 in valid capabilities.
281-
282-
[#section_cap_encoding]
283-
=== Capability Encoding
284-
285-
ifdef::cheri_v9_annotations[]
286-
NOTE: *CHERI v9 Note:* The encoding changes eliminate the concept of the
287-
in-memory format, and also increase precision for RV32. When EF=0, T and B
288-
are now shifted right rather than left within the address. Also, the bounds
289-
decoding for XLENMAX=32 uses a trick (see bit T8) to save one bit when encoding
290-
the exponent.
291-
endif::[]
292-
293-
The components of a capability are encoded as shown in
294-
xref:cap_encoding_xlen32[xrefstyle=short] and
295-
xref:cap_encoding_xlen64[xrefstyle=short] when XLENMAX=32 and XLENMAX=64
296-
respectively.
297-
298-
.Capability encoding when XLENMAX=32
299-
[#cap_encoding_xlen32]
300-
include::img/cap-encoding-xlen32.edn[]
301-
302-
.Capability encoding when XLENMAX=64
303-
[#cap_encoding_xlen64]
304-
include::img/cap-encoding-xlen64.edn[]
305-
306-
Each memory location or register able to hold a capability must also store the
307-
tag as out of band information that software cannot directly set or clear. The
308-
capability metadata is held in the most significant bits and the address
309-
is held in the least significant bits.
299+
[#section_cap_bounds_decoding]
300+
===== Decoding
310301

311302
The metadata is encoded in a compressed format cite:[woodruff2019cheri]. It
312303
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) )
425416
That is, invert the most significant bit of _t_ if the decoded length of the
426417
capability is larger than E.
427418

419+
[#section_cap_malformed]
420+
===== Malformed Bounds
421+
422+
A capability is _malformed_ if its encoding does not describe a valid
423+
capability because its bounds cannot be correctly decoded. The following check
424+
indicates whether a capability is malformed.
425+
426+
```
427+
malformedMSB = (E == CAP_MAX_E && B[MW - 1:MW - 2] != 0)
428+
|| (E == CAP_MAX_E - 1 && B[MW - 1] != 0)
429+
malformedLSB = (E < 0)
430+
malformed = !EF && (malformedMSB || malformedLSB)
431+
```
432+
433+
NOTE: The check is for malformed _bounds_, so it does not include reserved
434+
bits!
435+
436+
Capabilities with malformed bounds are always invalid anywhere in the system
437+
i.e. their tags are always 0.
438+
439+
==== Address
440+
441+
XLENMAX integer value that encodes the byte-address of a memory location.
442+
443+
.Address widths depending on XLENMAX
444+
[#address_bit_width,options=header,align="center",width="55%"]
445+
|==============================================================================
446+
^| XLENMAX ^| Address width
447+
^| 32 ^| {cap_rv32_addr_width}
448+
^| 64 ^| {cap_rv64_addr_width}
449+
|==============================================================================
450+
428451
[#section_special_caps]
429452
=== Special Capabilities
430453

@@ -539,23 +562,3 @@ xref:section_cap_encoding[xrefstyle=short].
539562
This gives useful guarantees, such that if an executed instruction is in
540563
<<pcc>> bounds, then it is also guaranteed that the next linear instruction
541564
is _representable_.
542-
543-
[#section_cap_malformed]
544-
=== Malformed Capability Bounds
545-
546-
A capability is _malformed_ if its encoding does not describe a valid
547-
capability because its bounds cannot be correctly decoded. The following check
548-
indicates whether a capability is malformed.
549-
550-
```
551-
malformedMSB = (E == CAP_MAX_E && B[MW - 1:MW - 2] != 0)
552-
|| (E == CAP_MAX_E - 1 && B[MW - 1] != 0)
553-
malformedLSB = (E < 0)
554-
malformed = !EF && (malformedMSB || malformedLSB)
555-
```
556-
557-
NOTE: The check is for malformed _bounds_, so it does not include reserved
558-
bits!
559-
560-
Capabilities with malformed bounds are always invalid anywhere in the system
561-
i.e. their tags are always 0.

0 commit comments

Comments
 (0)