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.

Sign up for GitHub

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

Cbuildcap and ctestsubset do not use DDC #82

Merged
merged 3 commits into from
Feb 7, 2024
Merged

Cbuildcap and ctestsubset do not use DDC #82

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
14bd397
made clear that ddc is not used when cs1 == 0 in cbuildcap and ctests…
francislaus Jan 23, 2024
1c1e158
Minor fixes for cbuildcap and ctestsubset
francislaus Feb 1, 2024
248c2b9
Merge branch 'ddc_cbuildcap_ctestsubset'
francislaus Feb 1, 2024
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
11 changes: 8 additions & 3 deletions src/insns/cbuildcap_32bit.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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::
Expand All @@ -20,19 +24,20 @@ 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. <<CBUILDCAP>> is typically used alongside <<CSETHIGH>> to build
capabilities from integer values.
capabilities from integer values. The case `cs1 == 0` trivially leads to the tag
andresag01 marked this conversation as resolved.
Show resolved Hide resolved
of `cd` being stripped.

Prerequisites::
{cheri_base_ext_name}

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) |
Expand Down
6 changes: 5 additions & 1 deletion src/insns/ctestsubset_32bit.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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::
Expand All @@ -16,7 +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` .
bounds and permissions of `cs2` are a subset of those of `cs1`.

NOTE: The implementation of this instruction is similar to <<CBUILDCAP>>, although
<<CTESTSUBSET>> does not include the sealed bit in the check.
Expand Down
Loading