From 14bd397ca72a8553b32126e68fb5da692d88d39b Mon Sep 17 00:00:00 2001 From: Franz Fuchs Date: Tue, 23 Jan 2024 15:39:12 +0000 Subject: [PATCH 1/2] made clear that ddc is not used when cs1 == 0 in cbuildcap and ctestsubset --- src/insns/cbuildcap_32bit.adoc | 12 +++++++++--- src/insns/ctestsubset_32bit.adoc | 8 +++++++- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/src/insns/cbuildcap_32bit.adoc b/src/insns/cbuildcap_32bit.adoc index 23c3e924..13f879d1 100644 --- a/src/insns/cbuildcap_32bit.adoc +++ b/src/insns/cbuildcap_32bit.adoc @@ -3,6 +3,10 @@ [#CBUILDCAP,reftext="CBUILDCAP"] ==== CBUILDCAP +ifdef::cheri_v9_annotations[] +NOTE: *CHERI v9 Note:* cbuildcap does not use ddc if cs1==0 +endif::[] + include::new_encoding_note.adoc[] Synopsis:: @@ -20,7 +24,9 @@ sealed, `cs1` 's permissions and bounds are equal or a superset of `cs2` 's, `cs2` 's bounds are not malformed (see xref:section_cap_malformed[xrefstyle=short]), and all reserved bits in `cs2` 's metadata are 0. <> is typically used alongside <> to build -capabilities from integer values. +capabilities from integer values. The case `cs1 == 0` trivially leads to cd being +assigned the zero capability. This was chosen to be the case for clean architecture +design. Prerequisites:: {cheri_base_ext_name} @@ -28,11 +34,11 @@ Prerequisites:: Simplified Operation TODO #not debugged much easier to read than the existing SAIL# :: [source,SAIL,subs="verbatim,quotes"] -- -let cs1_val = if unsigned(cs1) == 0 then DDC else C(cs1); +let cs1_val = C(cs1); let cs2_val = C(cs2) [with tag=1]; //isCapSubset includes derivability checks on both operands let subset = isCapSubset(cs1_val, cs2_val); -//Clear cd.tag if cs1 isn't a subset of cs1, or if +//Clear cd.tag if cs2 isn't a subset of cs1, or if //cs1 is untagged or sealed, or if either is underivable C(cd) = clearTagIf(cs2_val, not(subset) | not(cs1_val.tag) | diff --git a/src/insns/ctestsubset_32bit.adoc b/src/insns/ctestsubset_32bit.adoc index d0f992f5..5c3efd96 100644 --- a/src/insns/ctestsubset_32bit.adoc +++ b/src/insns/ctestsubset_32bit.adoc @@ -3,6 +3,10 @@ [#CTESTSUBSET,reftext="CTESTSUBSET"] ==== CTESTSUBSET +ifdef::cheri_v9_annotations[] +NOTE: *CHERI v9 Note:* ctestsubset does not use ddc if cs1==0 +endif::[] + include::new_encoding_note.adoc[] Synopsis:: @@ -16,7 +20,9 @@ include::wavedrom/ctestsubset.adoc[] Description:: `rd` is set to 1 if the tag of capabilities `cs1` and `cs2` are equal and the -bounds and permissions of `cs2` are a subset of those of `cs1` . +bounds and permissions of `cs2` are a subset of those of `cs1`. The case +`cs1 == 0` is trivally no subset and was chosen to be that for clean architecture +design. NOTE: The implementation of this instruction is similar to <>, although <> does not include the sealed bit in the check. From 1c1e158a20986d2cf8d9857b9c5d6bb1a3abab51 Mon Sep 17 00:00:00 2001 From: Franz Fuchs Date: Thu, 1 Feb 2024 15:08:36 +0000 Subject: [PATCH 2/2] Minor fixes for cbuildcap and ctestsubset --- src/insns/cbuildcap_32bit.adoc | 5 ++--- src/insns/ctestsubset_32bit.adoc | 4 +--- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/src/insns/cbuildcap_32bit.adoc b/src/insns/cbuildcap_32bit.adoc index 13f879d1..cfac455d 100644 --- a/src/insns/cbuildcap_32bit.adoc +++ b/src/insns/cbuildcap_32bit.adoc @@ -24,9 +24,8 @@ sealed, `cs1` 's permissions and bounds are equal or a superset of `cs2` 's, `cs2` 's bounds are not malformed (see xref:section_cap_malformed[xrefstyle=short]), and all reserved bits in `cs2` 's metadata are 0. <> is typically used alongside <> to build -capabilities from integer values. The case `cs1 == 0` trivially leads to cd being -assigned the zero capability. This was chosen to be the case for clean architecture -design. +capabilities from integer values. The case `cs1 == 0` trivially leads to the tag +of `cd` being stripped. Prerequisites:: {cheri_base_ext_name} diff --git a/src/insns/ctestsubset_32bit.adoc b/src/insns/ctestsubset_32bit.adoc index 5c3efd96..753a5017 100644 --- a/src/insns/ctestsubset_32bit.adoc +++ b/src/insns/ctestsubset_32bit.adoc @@ -20,9 +20,7 @@ include::wavedrom/ctestsubset.adoc[] Description:: `rd` is set to 1 if the tag of capabilities `cs1` and `cs2` are equal and the -bounds and permissions of `cs2` are a subset of those of `cs1`. The case -`cs1 == 0` is trivally no subset and was chosen to be that for clean architecture -design. +bounds and permissions of `cs2` are a subset of those of `cs1`. NOTE: The implementation of this instruction is similar to <>, although <> does not include the sealed bit in the check.