Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

detection of out of range top #521

Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ GEN_SCRIPT = $(SCRIPTS_DIR)/generate_tables.py

# Version and date
DATE ?= $(shell date +%Y-%m-%d)
VERSION ?= v0.9.3
VERSION ?= v0.9.4
REVMARK ?= Draft

# Directories and files
Expand Down
6 changes: 5 additions & 1 deletion readme.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,13 @@ For guidelines on how to contribute, refer to the link:CONTRIBUTING.md[CONTRIBUT
To build the document, you'll need the following tools installed on your system:

* Make
* asciiDoctor-pdf, asciidoctor-bibtex, asciidoctor-diagram, and asciidoctor-mathematical
* Docker

If you want to build outside of Docker, you'll need some more tools:
* Python3
* asciiDoctor-pdf, asciidoctor-bibtex, asciidoctor-diagram, asciidoctor-mathematical and asciidoctor-sail
* bytefield-svg
* wavedrom-cli

=== Cloning the Repository

Expand Down
15 changes: 10 additions & 5 deletions src/cap-description.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -445,12 +445,17 @@ Reconstituting the top two bits of T:
T[MW - 1:MW - 2] = B[MW - 1:MW - 2] + LCout + LMSB
```

Decoding the bounds:
The bounds are decoded as shown in xref:top_bound_dec[xrefstyle=short] and
xref:base_bound_dec[xrefstyle=short].

.Decoding of the MXLEN+1 wide top (_t_) bound
[#top_bound_dec]
include::img/top-bound-dec.edn[]

.Decoding of the MXLEN wide base (_b_) bound
[#base_bound_dec]
include::img/base-bound-dec.edn[]

```
top: t = { {1'b0, a[MXLEN - 1:E + MW]} + ct, T[MW - 1:0], {E{1'b0}} }
base: b = { a[MXLEN - 1:E + MW] + cb, B[MW - 1:0], {E{1'b0}} }
```
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].
Expand Down
7 changes: 3 additions & 4 deletions src/cheri-pte-ext.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,9 @@ The CW bit indicates whether reading or writing capabilities with the tag set to
the virtual page is permitted. When the CW bit is set, capabilities are written
as usual, and capability reads are controlled by the CRG bit.

NOTE: The tag bit of the stored capability is checked _after_ it is potentially
cleared <<tags_cleared_by_permissions,due to lack of permissions>>.

If the CW bit is clear then:

* When a capability load or AMO instruction is executed, the implementation
Expand All @@ -115,10 +118,6 @@ If the CW bit is clear then:
is raised when a capability store or AMO instruction is executed and the tag bit
of the capability being written is set.
* When CRG is set, the "pre-CW state", two schemes are permitted (also see <<section_hardware_pte_updates>>):
NOTE: The tag bit of the stored capability is checked _after_ it is potentially
cleared <<tags_cleared_by_permissions,due to lack of permissions>>.

** The same behavior as when CRG is clear, allowing software interpretation
of this state.
** When a capability store or AMO instruction is executed
Expand Down
3 changes: 0 additions & 3 deletions src/csv/CHERI_CSR.csv
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,6 @@ direct write if address didn't change","✔","","","","Zcmt","Jump Vector Table
"dddc","0x7bc","","D","DRW","tag=0, otherwise undefined","Apply <<section_invalid_addr_conv>>.
Always update the CSR with <<SCADDR>> even if the address didn't change.","Apply <<section_invalid_addr_conv>> and update the CSR with the result if the address changed,
direct write if address didn't change","","✔","","","{cheri_default_ext_name}, Sdext","Debug Default Data Capability (saved/restored on debug mode entry/exit)","","","","","","","","","","","","","","","","","","","","",""
"mtdc","0x74c","","M","MRW, <<asr_perm>>","tag=0, otherwise undefined","Update the CSR using <<SCADDR>>.","direct write","","","","","{cheri_default_ext_name}, M-mode","Machine Trap Data Capability (scratch register)","","","","","","","","","","","","","","","","","","","","",""
"stdc","0x163","","S","SRW, <<asr_perm>>","tag=0, otherwise undefined","Update the CSR using <<SCADDR>>.","direct write","","","","","{cheri_default_ext_name}, S-mode","Supervisor Trap Data Capability (scratch register)","","","","","","","","","","","","","","","","","","","","",""
"vstdc","0x245","","VS","HRW, <<asr_perm>>","tag=0, otherwise undefined","Update the CSR using <<SCADDR>>.","direct write","","","","","{cheri_default_ext_name}, H","Virtual Supervisor Trap Data Capability (scratch register)","","","","","","","","","","","","","","","","","","","","",""
"ddc","0x416","","U","URW","<<infinite-cap>>","Apply <<section_invalid_addr_conv>>.
Always update the CSR with <<SCADDR>> even if the address didn't change.","Apply <<section_invalid_addr_conv>> and update the CSR with the result if the address changed,
direct write if address didn't change","","✔","","","{cheri_default_ext_name}","User Default Data Capability","","","","","","","","","","","","","","","","","","","","",""
Expand Down
20 changes: 3 additions & 17 deletions src/hypervisor-integration.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -146,22 +146,6 @@ The <<vscause>> register is as defined in cite:[riscv-priv-spec]. It must
additionally support the new exception code for CHERI exceptions that
<<scause>> supports.

[#vstdc,reftext="vstdc"]
=== Virtual Supervisor Trap Default Capability Register (vstdc)

The <<vstdc>> register is a capability width read/write register that is
VS-mode's version of supervisor register <<stdc>>. This register is only
present when the implementation supports {cheri_default_ext_name}.

{TAG_RESET_CSR}

{REQUIRE_CRE_CSR}

{REQUIRE_HYBRID_CSR}

.Virtual supervisor trap default capability register
include::img/vstdcreg.edn[]

[#vstval,reftext="vstval"]
=== Virtual Supervisor Trap Value Register (vstval)

Expand All @@ -182,7 +166,9 @@ part of {cheri_base_ext_name} when the hypervisor extension is supported. Its
CSR address is 0x24b.

<<vstval2>> is updated following the same rules as <<mtval2>> for CHERI exceptions
which are taken in VS-mode.
and <<cheri_pte_ext,CHERI PTE page faults>> which are delegated to VS-mode.
It is written to zero for all other exceptions, except as listed otherwise by other
future extensions.

The fields are identical to <<mtval2>> for CHERI exceptions.

Expand Down
16 changes: 16 additions & 0 deletions src/img/base-bound-dec.edn
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
[bytefield]
----
(defattrs :plain [:plain {:font-family "M+ 1p Fallback" :font-size 25}])
(def row-height 80)
(def row-header-fn nil)
(def left-margin 100)
(def right-margin 100)
(def boxes-per-row 32)
(draw-column-headers {:height 50 :font-size 22 :labels (reverse ["0" "" "" "" "" "" "" "" "" "" "E" "" "" "" "" "" "" "" "" "" "E+MW" "" "" "" "" "" "" "" "" "" "" "MXLEN-1"])})

(draw-box "a[MXLEN - 1:E + MW] + cb" {:span 12})
(draw-box "B[MW - 1:0]" {:span 10})
(draw-box "0" {:span 10})

(draw-box "MXLEN" {:span 32 :borders {}})
----
22 changes: 0 additions & 22 deletions src/img/mtdcreg.edn

This file was deleted.

22 changes: 0 additions & 22 deletions src/img/stdcreg.edn

This file was deleted.

16 changes: 16 additions & 0 deletions src/img/top-bound-dec.edn
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
[bytefield]
----
(defattrs :plain [:plain {:font-family "M+ 1p Fallback" :font-size 25}])
(def row-height 80)
(def row-header-fn nil)
(def left-margin 100)
(def right-margin 100)
(def boxes-per-row 32)
(draw-column-headers {:height 50 :font-size 22 :labels (reverse ["0" "" "" "" "" "" "" "" "" "" "E" "" "" "" "" "" "" "" "" "" "E+MW" "" "" "" "" "" "" "" "" "" "" "MXLEN"])})

(draw-box "{1'b0, a[MXLEN - 1:E + MW]} + ct" {:span 12})
(draw-box "T[MW - 1:0]" {:span 10})
(draw-box "0" {:span 10})

(draw-box "MXLEN+1" {:span 32 :borders {}})
----
22 changes: 0 additions & 22 deletions src/img/vstdcreg.edn

This file was deleted.

2 changes: 2 additions & 0 deletions src/insns/addi16sp_16bit.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@ include::wavedrom/c-int-reg-immed.adoc[]
Add the non-zero sign-extended 6-bit immediate to the value in the stack pointer (`csp=c2`), where the immediate is scaled to represent multiples of 16 in the range (-512,496). Clear the tag if the resulting capability is
unrepresentable or `csp` is sealed.

include::malformed_clear_tag_csp.adoc[]

{cheri_int_mode_name} Description::

Add the non-zero sign-extended 6-bit immediate to the value in the stack pointer (`sp=x2`), where the immediate is scaled to represent multiples of 16 in the range (-512,496).
Expand Down
2 changes: 2 additions & 0 deletions src/insns/addi4spn_16bit.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,8 @@ include::wavedrom/c-ciw.adoc[]

Add a zero-extended non-zero immediate, scaled by 4, to the stack pointer, `csp`, and writes the result to `cd'`. This instruction is used to generate pointers to stack-allocated variables. Clear the tag if the resulting capability is unrepresentable or `csp` is sealed.

include::malformed_clear_tag_csp.adoc[]

{cheri_int_mode_name} Description::

Add a zero-extended non-zero immediate, scaled by 4, to the stack pointer, `sp`, and writes the result to `rd'`. This instruction is used to generate pointers to stack-allocated variables.
Expand Down
2 changes: 1 addition & 1 deletion src/insns/atomic_exceptions.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ All misaligned atomics cause a store/AMO address misaligned exception to allow s
+
When these instructions cause CHERI exceptions, _CHERI data fault_
is reported in the TYPE field and the following codes may be
reported in the CAUSE field of <<mtval2>> or <<stval2>>:
reported in the CAUSE field of <<mtval2>>, <<stval2>> or <<vstval2>>:

<<<

Expand Down
5 changes: 2 additions & 3 deletions src/insns/cbo_exceptions.adoc
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
Exceptions::
CHERI fault exceptions occur when the authorizing capability fails one of the checks
listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>> or
<<stval2>> TYPE field and the corresponding code is written to CAUSE.
listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>>,
<<stval2>> or <<vstval2>> TYPE field and the corresponding code is written to CAUSE.
+
ifdef::cbo_inval[]
The CBIE bit in <<menvcfg>> and <<senvcfg>> indicates whether
Expand Down Expand Up @@ -33,7 +33,6 @@ ifdef::cbo_inval[]
endif::[]
| Invalid address violation | The effective address is invalid according to xref:section_invalid_addr_conv[xrefstyle=short]
| Bounds violation | None of the bytes accessed are within the bounds, or the capability has <<section_cap_malformed,malformed>> bounds

|==============================================================================


Expand Down
2 changes: 1 addition & 1 deletion src/insns/condbr_common.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,4 @@ Exceptions::
When the target address is not within the <<pcc>>'s bounds, and the branch is taken,
a _CHERI jump or
branch fault_ is reported in the TYPE field and Bounds violation is reported in
the CAUSE field of <<mtval2>> or <<stval2>>:
the CAUSE field of <<mtval2>>, <<stval2>> or <<vstval2>>:
4 changes: 2 additions & 2 deletions src/insns/hypv-virt-loadx.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,8 @@ to `rd`.

Exceptions::
CHERI fault exceptions occur when the authorizing capability fails one of the checks
listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>> or
<<stval2>> TYPE field and the corresponding code is written to CAUSE.
listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>>,
<<stval2>> or <<vstval2>>> TYPE field and the corresponding code is written to CAUSE.
+
[%autowidth,options=header,align=center]
|==============================================================================
Expand Down
2 changes: 1 addition & 1 deletion src/insns/jalr_32bit.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ instruction following the jump is written to `rd`.
Exceptions::
When these instructions cause CHERI exceptions, _CHERI jump or branch fault_
is reported in the TYPE field and the following codes may be
reported in the CAUSE field of <<mtval2>> or <<stval2>>:
reported in the CAUSE field of <<mtval2>>, <<stval2>> or <<vstval2>>:

[%autowidth,options=header,align=center]
|==============================================================================
Expand Down
7 changes: 3 additions & 4 deletions src/insns/load_exceptions.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ to CLEN/8.
+
endif::[]
CHERI fault exceptions occur when the authorizing capability fails one of the checks
listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>> or
<<stval2>> TYPE field and the corresponding code is written to CAUSE.
listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>>,
<<stval2>> or <<vstval2>> TYPE field and the corresponding code is written to CAUSE.
+
[%autowidth,options=header,align=center]
|==============================================================================
Expand All @@ -20,12 +20,11 @@ listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>> or
| Permission violation | Authority capability does not grant <<r_perm>>, or the AP field could not have been produced by <<ACPERM>>
| Invalid address violation | The effective address is invalid according to xref:section_invalid_addr_conv[xrefstyle=short]
| Bounds violation | At least one byte accessed is outside the authority capability bounds, or the capability has <<section_cap_malformed,malformed>> bounds

|==============================================================================
+
If virtual memory is enabled, then the state of <<cheri_pte_ext,PTE>>.CW,
and, if {cheri_pte_ext_name} is implemented, <<cheri_pte_ext,PTE>>.CRG, <<cheri_pte_ext,PTE>>.U and <<sstatusreg_pte,sstatus>>.UCRG,
may cause a CHERI <<cheri_pte_ext,PTE>> page fault exception in addition to a normal RISC-V page fault exception.
may cause a <<cheri_pte_ext,CHERI PTE page fault>> exception in addition to a normal RISC-V page fault exception.
See <<mtval2-page-fault>> for the exception reporting in this case.
+
:!load_res:
Expand Down
2 changes: 2 additions & 0 deletions src/insns/malformed_clear_tag_csp.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
NOTE: This instruction sets `cd.tag=0` if `csp` 's bounds are <<section_cap_malformed,malformed>>,
or if any of the reserved fields are set.
2 changes: 2 additions & 0 deletions src/insns/malformed_top_range_clear_tag.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
NOTE: This instruction sets `cd.tag=0` if `cs1` 's bounds are <<section_cap_malformed,malformed>>
or if any of the reserved fields are set.
4 changes: 2 additions & 2 deletions src/insns/mret_sret.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,8 @@ Exceptions::
CHERI fault exceptions occur when <<pcc>> does not grant <<asr_perm>> because
<<MRET>> and <<SRET>> require access to privileged CSRs. When that exception
occurs, _CHERI instruction fetch fault_ is reported in the TYPE field and the
Permission violation code is reported in the CAUSE field of <<mtval>> or
<<stval>>.
Permission violation code is reported in the CAUSE field of <<mtval2>>,
<<stval2>> or <<vstval2>>.

Operation::
[source,SAIL,subs="verbatim,quotes"]
Expand Down
6 changes: 3 additions & 3 deletions src/insns/store_exceptions.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ to CLEN/8.
+
endif::[]
CHERI fault exceptions occur when the authorizing capability fails one of the checks
listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>> or
<<stval2>> TYPE field and the corresponding code is written to CAUSE.
listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>>,
<<stval2>> or <<vstval2>> TYPE field and the corresponding code is written to CAUSE.
+
[%autowidth,options=header,align=center]
|==============================================================================
Expand All @@ -24,7 +24,7 @@ listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>> or
+
If {cheri_pte_ext_name} is implemented, and virtual memory is enabled, then the state of
<<cheri_pte_ext,PTE>>.CW and <<cheri_pte_ext,PTE>>.CRG from the current virtual memory page may
cause a CHERI <<cheri_pte_ext,PTE>> page fault exception in addition to a normal RISC-V page fault
cause a <<cheri_pte_ext,CHERI PTE page fault>> exception in addition to a normal RISC-V page fault
when operating in user mode.
See <<mtval2-page-fault>> for the exception reporting in this case.
+
Expand Down
2 changes: 1 addition & 1 deletion src/insns/zcmt_cmjalt.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ Requires <<jvtc>> to be tagged, not sealed, have <<x_perm>> and for the full XLE
{cheri_cap_mode_name} Exceptions::
When these instructions cause CHERI exceptions, _CHERI instruction fetch fault_
is reported in the TYPE field and the following codes may be
reported in the CAUSE field of <<mtval2>> or <<stval2>>:
reported in the CAUSE field of <<mtval2>>, <<stval2>> or <<vstval2>>:

[width="50%",options=header,cols="2,^1",align=center]
|==============================================================================
Expand Down
2 changes: 1 addition & 1 deletion src/insns/zcmt_cmjt.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ Requires <<jvtc>> to be tagged, not sealed, have <<x_perm>> and for the full XLE
{cheri_cap_mode_name} Exceptions::
When these instructions cause CHERI exceptions, _CHERI instruction fetch fault_
is reported in the TYPE field and the following codes may be
reported in the CAUSE field of <<mtval2>> or <<stval2>>:
reported in the CAUSE field of <<mtval2>>, <<stval2>> or <<vstval2>>:

[width="50%",options=header,cols="2,^1",align=center]
|==============================================================================
Expand Down
Loading
Loading