Fully apply implicit acperm, including tag clear

model/cheri/cheri_cap_common.sail

@@ -536,7 +536,22 @@ function clearTagIf(cap : Capability, cond : bool) -> Capability =
 function clearTag(cap : Capability) -> Capability =
   {cap with tag = false}
 
-function legalizeLoadedArchPerms(loaded_cap : Capability, auth_cap : Capability) -> Capability = {
+function clearTagAcperm(cap : Capability) -> Capability =
+  clearTagIf(cap, capIsSealed(cap) | not(capReservedValid(cap)))
+
+// Implementations are allowed to retain invalid capability permissions loaded from memory
+// instead of following the ACPERM behaviour of reducing them to no permissions.
+let sys_legalize_malformed_permission_on_load = false
+
+function legalizeLoadedPermissions(loaded_cap : Capability, auth_cap : Capability) -> Capability = {
+  // Any unsealed capability with its tag set to 1 that is loaded from memory has
+  // ... its Capability Level (CL) restricted to the
+  // authorizing capability’s Capability Level (CL) if the authorizing capability
+  // does not grant EL-permission. If sealed, then only CL is modified ...
+  // CL is not a permission so it is legalized even if permissions are malformed.
+  let restrictCL = loaded_cap.tag & not(canEL(auth_cap));
+  let loaded_cap = if restrictCL then {loaded_cap with cl = auth_cap.cl & loaded_cap.cl} else loaded_cap;
+
   // If a capability grants R-permission and C-permission, but no LM-permission, then
   // a capability loaded via this authorizing capability will have W-permission and
   // LM-permission removed provided that the loaded capability has its tag set and
@@ -546,58 +561,38 @@ function legalizeLoadedArchPerms(loaded_cap : Capability, auth_cap : Capability)
   // Any unsealed capability with its tag set to 1 that is loaded from memory has
   // its EL-permission cleared ... if the authorizing capability does not grant EL-permission.
 
-  let tagged_and_unsealed = loaded_cap.tag & not(capIsSealed(loaded_cap));
-  let clearWLM = tagged_and_unsealed & not(canLM(auth_cap));
-  let clearEL = tagged_and_unsealed & not(canEL(auth_cap));
+  // Malformed permissions are optionally legalized.
 
-  if clearWLM | clearEL then {
+  let legalize_perms = loaded_cap.tag & not(capIsSealed(loaded_cap)) &
+                       (not(permsMalformed(loaded_cap)) | sys_legalize_malformed_permission_on_load);
+  let clearWLM = legalize_perms & not(canLM(auth_cap));
+  let clearEL = legalize_perms & not(canEL(auth_cap));
+
+  let loaded_cap = if clearWLM | clearEL then {
     let perms = getArchPermsLegalized(loaded_cap);
     let perms = { perms with
       W = perms.W & not(clearWLM),
       LM = perms.LM & not(clearWLM),
       EL = perms.EL & not(clearEL),
     };
     setArchPerms(loaded_cap, perms)
-  } else loaded_cap
-}
-
-function restrictLoadedCL(loaded_cap : Capability, auth_cap : Capability) -> Capability = {
-  // Any unsealed capability with its tag set to 1 that is loaded from memory has
-  // ... its Capability Level (CL) restricted to the
-  // authorizing capability’s Capability Level (CL) if the authorizing capability
-  // does not grant EL-permission. If sealed, then only CL is modified ...
+  } else loaded_cap;
 
-  let restrictCL = loaded_cap.tag & not(canEL(auth_cap));
-  if restrictCL then {loaded_cap with cl = auth_cap.cl & loaded_cap.cl} else loaded_cap
+  if restrictCL | clearWLM | clearEL then {
+    clearTagAcperm(loaded_cap)
+  } else {
+    loaded_cap
+  }
 }
 
-function legalizeSL(stored_cap : Capability, auth_cap : Capability) -> Capability = {
+function legalizeStoredPermissions(stored_cap : Capability, auth_cap : Capability) -> Capability = {
   // When storing a capability, if the authorizing capability does not grant SL-perm
   // and the stored cap has CL == 0 clear the tag of the stored capability,
   // otherwise store the cap data unmodified.
   let cond = not(canSL(auth_cap)) & stored_cap.cl == zeros();
   clearTagIf(stored_cap, cond)
 }
 
-// Implementations are allowed to retain invalid capability permissions loaded from memory
-// instead of following the ACPERM behaviour of reducing them to no permissions.
-let sys_legalize_malformed_permission_on_load = false
-
-function legalizeLoadedPermissions(loaded_cap : Capability, auth_cap : Capability) -> Capability = {
-  // CL is not a permission so it is always legalized.
-  let loaded_cap = restrictLoadedCL(loaded_cap, auth_cap);
-
-  // Malformed permissions are optionally legalized.
-  if not(permsMalformed(loaded_cap)) | sys_legalize_malformed_permission_on_load then {
-    legalizeLoadedArchPerms(loaded_cap, auth_cap)
-  } else {
-    loaded_cap
-  }
-}
-
-function legalizeStoredPermissions(stored_cap : Capability, auth_cap : Capability) -> Capability = {
-  legalizeSL(stored_cap, auth_cap)
-}
 
 function capBoundsEqual (c1 : Capability, c2 : Capability) -> bool =
   match (getCapBounds(c1), getCapBounds(c2)) {

model/cheri/cheri_insts.sail

@@ -270,8 +270,7 @@ function clause execute(ACPERM(cd, cs1, rs2)) = {
   let cs1_val = C(cs1);
   let rs2_val = X(rs2);
 
-  let cond = capIsSealed(cs1_val) | not(capReservedValid(cs1_val));
-  let inCap = clearTagIf(cs1_val, cond);
+  let inCap = clearTagAcperm(cs1_val);
 
   let old_perms = packPerms(getArchPermsLegalized(inCap), inCap.cl, inCap.sd_perms).bits;
 

model/cheri/test_main_ext.sail

@@ -583,6 +583,28 @@ function test_cheri_enables() -> unit = {
     test_cheri_mcre(false);
 }
 
+
+function test_cheri_ls_perm_clearing() -> unit = {
+    let no_LM_EL_W_perms = {getArchPermsLegalized(infinite_cap) with LM=false, EL=false, W=false};
+    let no_LM_EL_W_CL_cap = setArchPerms({infinite_cap with cl=zeros()}, no_LM_EL_W_perms);
+
+    // Untagged loaded caps never have permissions cleared
+    assert(legalizeLoadedPermissions({infinite_cap with tag=false}, no_LM_EL_W_CL_cap) == {infinite_cap with tag=false});
+
+    // Infinite auth cap never changes loaded cap
+    assert(legalizeLoadedPermissions({infinite_cap with sealed=true}, infinite_cap) == {infinite_cap with sealed=true});
+    assert(legalizeLoadedPermissions({infinite_cap with reserved_0=ones()}, infinite_cap) == {infinite_cap with reserved_0=ones()});
+
+    // Clear EL, LM, W, CL as normal
+    assert(legalizeLoadedPermissions(infinite_cap, no_LM_EL_W_CL_cap) == no_LM_EL_W_CL_cap);
+
+    // Clear CL as normal, don't clear EL/LM/W due to sealed, clear tag due to sealed
+    assert(legalizeLoadedPermissions({infinite_cap with sealed=true}, no_LM_EL_W_CL_cap) == {infinite_cap with sealed=true, cl=zeros(), tag=false});
+
+    // Clear EL, LM, W, CL as normal, clear tag due to nonzero reserved bits
+    assert(legalizeLoadedPermissions({infinite_cap with reserved_0=ones()}, no_LM_EL_W_CL_cap) == {no_LM_EL_W_CL_cap with reserved_0=ones(), tag=false});
+}
+
 function test_main_ext() -> unit = {
     // Enable CHERI
     set_mseccfg(update_CRE(mseccfg, 0b1).bits);
@@ -607,4 +629,5 @@ function test_main_ext() -> unit = {
     test_cheri_malformed();
     test_cheri_invalid_addr();
     test_cheri_enables();
+    test_cheri_ls_perm_clearing();
 }