diff --git a/src/insns/atomic_exceptions.adoc b/src/insns/atomic_exceptions.adoc index 0e1f8031..6ffde29a 100644 --- a/src/insns/atomic_exceptions.adoc +++ b/src/insns/atomic_exceptions.adoc @@ -8,7 +8,8 @@ If <> is not granted then store the memory tag as zero, and load `cd.tag + If the authorizing capability does not grant <>, and the tag of `cd` is 1 and `cd` is not sealed, then an implicit <> clearing <> and <> is performed to obtain the intermediate permissions on `cd` (see <>). + -If the authorizing capability does not grant <>, and the tag of `cd` is 1, then an implicit <> clearing <> and restricting the <> to the level of the authorizing capability is performed to obtain the final permissions on `cd` (see <>). +If the authorizing capability does not grant <>, and the tag of `cd` is 1, then an implicit <> restricting the <> to the level of the authorizing capability is performed. +If `cd` is not sealed, this implicit <> also clears <> to obtain the final permissions on `cd` (see <>). + The stored tag is also set to zero if the authorizing capability does not have <> set but the stored data has a <> of 0 (see <>). endif::[] diff --git a/src/insns/load_tag_perms.adoc b/src/insns/load_tag_perms.adoc index db1323f0..5d1c5e00 100644 --- a/src/insns/load_tag_perms.adoc +++ b/src/insns/load_tag_perms.adoc @@ -5,6 +5,8 @@ The tag value written to `cd` is 0 if the tag of the memory location loaded is If the authorizing capability does not grant <>, and the tag of `cd` is 1 and `cd` is not sealed, then an implicit <> clearing <> and <> is performed to obtain the intermediate permissions on `cd`. + If the authorizing capability does not grant <>, and the tag of `cd` is 1, then an implicit <> clearing <> and restricting the <> to the level of the authorizing capability is performed to obtain the final permissions on `cd`. +If the authorizing capability does not grant <>, and the tag of `cd` is 1, then an implicit <> restricting the <> to the level of the authorizing capability is performed. +If `cd` is not sealed, this implicit <> also clears <> to obtain the final permissions on `cd`. NOTE: Missing <> does not affect untagged values since this could result in surprising bit patterns when copying non-capability data. Similarly, sealed capabilities are not modified as they are not directly dereferenceable. diff --git a/src/level-ext.adoc b/src/level-ext.adoc index e8711721..af240727 100644 --- a/src/level-ext.adoc +++ b/src/level-ext.adoc @@ -123,15 +123,15 @@ NOTE: A capability with <>=1 is _global_ and with <