implement new permit_unseal used for CUnseal instead of permit_seal.

4 files changed, 18 insertions, 16 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index fb3b370d..2066826a 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -1044,8 +1044,8 @@ function clause execute (CUnseal(cd, cs, ct)) =
     raise_c2_exception(CapEx_SealViolation, ct)
   else if (ct_cursor != unsigned(cs_val.otype)) then
     raise_c2_exception(CapEx_TypeViolation, ct)
-  else if not (ct_val.permit_seal) then
-    raise_c2_exception(CapEx_PermitSealViolation, ct)
+  else if not (ct_val.permit_unseal) then
+    raise_c2_exception(CapEx_PermitUnsealViolation, ct)
   else if (ct_cursor <  getCapBase(ct_val)) then
     raise_c2_exception(CapEx_LengthViolation, ct)
   else if (ct_cursor >= getCapTop(ct_val)) then
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index d1129147..32393fe8 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -47,7 +47,7 @@ struct CapStruct = {
   tag                    : bool    ,
   uperms                 : bits(4) ,
   access_system_regs     : bool    ,
-  perm_reserved9         : bool    ,
+  permit_unseal          : bool    ,
   permit_ccall           : bool    ,
   permit_seal            : bool    ,
   permit_store_local_cap : bool    ,
@@ -70,7 +70,7 @@ let null_cap : CapStruct = struct {
   tag                    = false,
   uperms                 = zeros(),
   access_system_regs     = false,
-  perm_reserved9         = false,
+  permit_unseal          = false,
   permit_ccall           = false,
   permit_seal            = false,
   permit_store_local_cap = false,
@@ -93,7 +93,7 @@ let default_cap : CapStruct = struct {
   tag                    = true,
   uperms                 = ones(),
   access_system_regs     = true,
-  perm_reserved9         = true,
+  permit_unseal          = true,
   permit_ccall           = true,
   permit_seal            = true,
   permit_store_local_cap = true,
@@ -123,7 +123,7 @@ function capRegToCapStruct(c) : CapReg -> CapStruct =
     tag                    = c[128],
     uperms                 = c[127..124],
     access_system_regs     = c[123],
-    perm_reserved9         = c[122],
+    permit_unseal          = c[122],
     permit_ccall           = c[121],
     permit_seal            = c[120],
     permit_store_local_cap = c[119],
@@ -144,7 +144,7 @@ function capRegToCapStruct(c) : CapReg -> CapStruct =
 
 function getCapHardPerms(cap) : CapStruct -> bits(11) =
    (cap.access_system_regs
-  @ cap.perm_reserved9
+  @ cap.permit_unseal
   @ cap.permit_ccall
   @ cap.permit_seal
   @ cap.permit_store_local_cap
@@ -198,7 +198,7 @@ function setCapPerms(cap, perms) : (CapStruct, bits(31)) -> CapStruct =
       uperms                 = perms[18..15],
       /* 14..11 reserved -- ignore */
       access_system_regs     = perms[10],
-      perm_reserved9         = perms[9],
+      permit_unseal          = perms[9],
       permit_ccall           = perms[8],
       permit_seal            = perms[7],
       permit_store_local_cap = perms[6],
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index 8e4a14f8..f09fe608 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -49,7 +49,7 @@ struct CapStruct = {
   uperms                  : bits(16),
   perm_reserved11_14      : bits(4) ,
   access_system_regs      : bool    ,
-  perm_reserved9          : bool    ,
+  permit_unseal           : bool    ,
   permit_ccall            : bool    ,
   permit_seal             : bool    ,
   permit_store_local_cap  : bool    ,
@@ -72,7 +72,7 @@ let null_cap : CapStruct = struct {
   uperms = zeros(),
   perm_reserved11_14 = zeros(),
   access_system_regs = false,
-  perm_reserved9 = false,
+  permit_unseal = false,
   permit_ccall = false,
   permit_seal = false,
   permit_store_local_cap = false,
@@ -95,7 +95,7 @@ let default_cap : CapStruct = struct {
   uperms = ones(),
   perm_reserved11_14 = ones(),
   access_system_regs = true,
-  perm_reserved9 = true,
+  permit_unseal = true,
   permit_ccall = true,
   permit_seal = true,
   permit_store_local_cap = true,
@@ -121,7 +121,7 @@ function capRegToCapStruct(capReg) : CapReg -> CapStruct =
     uperms                     = capReg[223..208],
     perm_reserved11_14         = capReg[207..204],
     access_system_regs         = capReg[203],
-    perm_reserved9             = capReg[202],
+    permit_unseal              = capReg[202],
     permit_ccall               = capReg[201],
     permit_seal                = capReg[200],
     permit_store_local_cap     = capReg[199],
@@ -142,7 +142,7 @@ function getCapPerms(cap) : CapStruct -> bits(31) =
     cap.uperms
       @ cap.perm_reserved11_14
       @ cap.access_system_regs
-      @ cap.perm_reserved9
+      @ cap.permit_unseal
       @ cap.permit_ccall
       @ cap.permit_seal
       @ cap.permit_store_local_cap
@@ -207,7 +207,7 @@ function setCapPerms(cap, perms) : (CapStruct, bits(31)) -> CapStruct =
       uperms                 = perms[30..15],
       perm_reserved11_14     = perms[14..11],
       access_system_regs     = perms[10],
-      perm_reserved9         = perms[9],
+      permit_unseal          = perms[9],
       permit_ccall           = perms[8],
       permit_seal            = perms[7],
       permit_store_local_cap = perms[6],
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index c2fb9c24..ecb98ef8 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -158,7 +158,8 @@ enum CapEx = {
   CapEx_PermitSealViolation,
   CapEx_AccessSystemRegsViolation,
   CapEx_PermitCCallViolation,
-  CapEx_AccessCCallIDCViolation
+  CapEx_AccessCCallIDCViolation,
+  CapEx_PermitUnsealViolation
 }
 
 function CapExCode(ex) : CapEx -> bits(8)=
@@ -184,7 +185,8 @@ function CapExCode(ex) : CapEx -> bits(8)=
     CapEx_PermitSealViolation           => 0x17,
     CapEx_AccessSystemRegsViolation     => 0x18,
     CapEx_PermitCCallViolation          => 0x19,
-    CapEx_AccessCCallIDCViolation       => 0x1a
+    CapEx_AccessCCallIDCViolation       => 0x1a,
+    CapEx_PermitUnsealViolation         => 0x1b
   }
 
 bitfield CapCauseReg : bits(16) = {