diff options
| -rw-r--r-- | cheri/cheri_prelude_128.sail | 4 | ||||
| -rw-r--r-- | cheri/cheri_prelude_256.sail | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail index ffd986a4..263dae43 100644 --- a/cheri/cheri_prelude_128.sail +++ b/cheri/cheri_prelude_128.sail @@ -126,7 +126,7 @@ function capRegToCapStruct(c) : CapReg -> CapStruct = permit_execute = c[114], global = c[113], reserved = c[112..111], - E = c[110..105] ^ 0b110000, + E = c[110..105], sealed = s, B = Bc, T = Tc, @@ -153,7 +153,7 @@ function capStructToMemBits128(cap) : CapStruct -> bits(128) = ( cap.uperms @ getCapHardPerms(cap) @ cap.reserved - @ cap.E ^ 0b110000 + @ cap.E @ cap.sealed @ b @ t diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail index ba8a5d16..5590bbb8 100644 --- a/cheri/cheri_prelude_256.sail +++ b/cheri/cheri_prelude_256.sail @@ -165,12 +165,12 @@ function capStructToMemBits256(cap) : CapStruct -> bits(256) = this ensures that canonical null_cap is always all-zeros in memory even though it may have bits set logically (e.g. length or exponent) */ +let null_cap_bits : bits(256) = capStructToMemBits256(null_cap) + function capStructToMemBits(cap) : CapStruct -> bits(256)= - let null_cap_bits : bits(256) = capStructToMemBits256(null_cap) in capStructToMemBits256(cap) ^ null_cap_bits function memBitsToCapBits(tag, b) : (bool, bits(256)) -> bits(257) = - let null_cap_bits : bits(256) = capStructToMemBits256(null_cap) in tag @ (b ^ null_cap_bits) function capStructToCapReg(cap) : CapStruct -> CapReg = cap.tag @ capStructToMemBits256(cap) |