diff --git a/archdoc/chap-isaref-riscv.tex b/archdoc/chap-isaref-riscv.tex index ea921d6..74d195b 100644 --- a/archdoc/chap-isaref-riscv.tex +++ b/archdoc/chap-isaref-riscv.tex @@ -120,7 +120,7 @@ \section{Constant Definitions} \sailRISCVtype{cap\_cE\_width} \sailRISCVtype{cap\_max\_E} \sailRISCVtypecapSizze{} -\sailRISCVtypecapMantissaWidth{} +\sailRISCVtypecapBWidth{} \sailRISCVtype{cap\_perms\_width} \sailRISCVtype{cap\_cperms\_width} \sailRISCVtype{cap\_otype\_width} diff --git a/properties/props.sail b/properties/props.sail index 48c531a..6c95c71 100644 --- a/properties/props.sail +++ b/properties/props.sail @@ -94,8 +94,7 @@ $property function prop_setbounds(reqBase : CapAddrBits, reqLen : CapAddrBits) -> bool = { let (exact, c) = setCapBounds(root_cap_mem, reqBase, reqLen); let encodable = capEncodable(c); - let (b2, l2) = getCapBoundsBits(c); - let t2 = (0b0 @ b2) + l2; + let (b2, l2, t2) = getCapBoundsBits(c); let reqTop = (0b0 @ reqBase) + (0b0 @ reqLen); let saneTop = reqTop <=_u 0b1@0x00000000; saneTop --> ( @@ -122,15 +121,13 @@ function prop_setbounds_monotonic( reqBase1 : CapAddrBits, reqLen1 : CapAddrBits, reqBase2 : CapAddrBits, reqLen2 : CapAddrBits) -> bool = { let (exact1, c1) = setCapBounds(root_cap_mem, reqBase1, reqLen1); - let (b1, l1) = getCapBoundsBits(c1); - let t1 = (0b0 @ b1) + l1; + let (b1, l1, t1) = getCapBoundsBits(c1); let reqTop1 = (0b0 @ reqBase1) + (0b0 @ reqLen1); let saneTop1 = reqTop1 <=_u 0b1@0x00000000; let reqTop2 = (0b0 @ reqBase2) + (0b0 @ reqLen2); let saneTop2 = reqTop2 <=_u 0b1@0x00000000; let (exact2, c2) = setCapBounds(c1, reqBase2, reqLen2); - let (b2, l2) = getCapBoundsBits(c2); - let t2 = (0b0 @ b2) + l2; + let (b2, l2, t2) = getCapBoundsBits(c2); let requestMonotonic = (b1 <=_u reqBase2) & (reqTop2 <=_u t1); let resultMonotonic = (b1 <=_u b2) & (t2 <=_u t1); (saneTop1 & saneTop2 & requestMonotonic) --> resultMonotonic @@ -145,12 +142,10 @@ $property function prop_setbounds_precise(reqBase1 : CapAddrBits, reqLen1 : CapAddrBits, c2 : CapBits) -> bool = { let (exact, c1) = setCapBounds(root_cap_mem, reqBase1, reqLen1); - let (b1, l1) = getCapBoundsBits(c1); - let t1 = (0b0 @ b1) + l1; + let (b1, l1, t1) = getCapBoundsBits(c1); let reqTop1 = (0b0 @ reqBase1) + (0b0 @ reqLen1); let saneTop1 = reqTop1 <=_u 0b1@0x00000000; - let (b2, l2) = getCapBoundsBits(capBitsToCapability(false, c2)); - let t2 = (0b0 @ b2) + l2; + let (b2, l2, t2) = getCapBoundsBits(capBitsToCapability(false, c2)); let validBase = b2 <=_u reqBase1; let betterBase = b1 <_u b2; let validTop = reqTop1 <=_u t2; @@ -182,8 +177,7 @@ function prop_repbounds_c(reqBase : CapAddrBits, reqLen : CapAddrBits, newAddr : let (exact, c) = setCapBounds(root_cap_mem, reqBase, reqLen); let reqTop = (0b0 @ reqBase) + (0b0 @ reqLen); let saneTop = reqTop <=_u 0b1@0x00000000; - let (b, l) = getCapBoundsBits(c); - let t = (0b0 @ b) + l; + let (b, l, t) = getCapBoundsBits(c); let (representable, newCap) = setCapAddr(c, newAddr); let inCBounds = (b <=_u newAddr) & ((0b0 @ newAddr) <=_u t); (saneTop & inCBounds) --> representable @@ -198,8 +192,7 @@ function prop_repbounds(reqBase : CapAddrBits, reqLen : CapAddrBits, newAddr : C let (exact, c) = setCapBounds(root_cap_mem, reqBase, reqLen); let reqTop = (0b0 @ reqBase) + (0b0 @ reqLen); let saneTop = reqTop <=_u 0b1@0x00000000; - let (b, l) = getCapBoundsBits(c); - let t = (0b0 @ b) + l; + let (b, l, t) = getCapBoundsBits(c); let (representable, newCap) = setCapAddr(c, newAddr); let repTop = (0b0 @ b) + ((to_bits(33,1) << unsigned(c.E)) << 9); /* The representable bounds check: either E is max or address is in range */ diff --git a/qtest/qtest.ml b/qtest/qtest.ml index c2975fa..b595731 100644 --- a/qtest/qtest.ml +++ b/qtest/qtest.ml @@ -12,13 +12,13 @@ let gen_sailbits_geom n s = let test_cap_decode capbits = let cap = Cheri_cc.zcapBitsToCapability(false, capbits) in - let (bot, length)= Cheri_cc.zgetCapBounds(cap) in + let (bot, length, top)= Cheri_cc.zgetCapBounds(cap) in begin print (Cheri_cc.string_of_zbits capbits); print (",0x"); print (Z.format "08x" bot); print (",0x"); - print (Z.format "09x" length); + print (Z.format "09x" top); print ","; print (Cheri_cc.string_of_zbits (Cheri_cc.zgetCapPerms cap)); print (","); diff --git a/src/cheri_cap_common.sail b/src/cheri_cap_common.sail index 69fe2b6..8bad237 100644 --- a/src/cheri_cap_common.sail +++ b/src/cheri_cap_common.sail @@ -404,7 +404,7 @@ let null_cap_bits : CapBits = capToBits(null_cap) /*! * Returns the decoded base and top of the given Capability. */ -function getCapBoundsBits(c) : Capability -> (CapAddrBits, CapLenBits) = { +function getCapBoundsBits(c) : Capability -> (CapAddrBits, CapLenBits, CapLenBits) = { let E = if c.E >=_u cap_max_E_bits then cap_max_E_bits else c.E; let a : CapAddrBits = c.address; let a_mid = truncate(a >> E, cap_B_width); @@ -412,12 +412,13 @@ function getCapBoundsBits(c) : Capability -> (CapAddrBits, CapLenBits) = { let a_top = a >> (E + cap_B_width); let base : CapAddrBits = truncate(((a_top - a_hi) @ c.B) << E, cap_addr_width); let length : CapLenBits = truncate((zeros(24) @ c.M) << E, cap_len_width); - (base, length) + let top : CapLenBits = (0b0 @ base) + length; + (base, length, top) } -function getCapBounds(cap) : Capability -> (CapAddrInt, CapLen) = - let (base : CapAddrBits, length : CapLenBits) = getCapBoundsBits(cap) in - (unsigned(base), unsigned(length)) +function getCapBounds(cap) : Capability -> (CapAddrInt, CapLen, CapLen) = + let (base : CapAddrBits, length: CapLenBits, top : CapLenBits) = getCapBoundsBits(cap) in + (unsigned(base), unsigned(length), unsigned(top)) val count_ones : forall 'ni 'no, 'no >= 1. (int('no), bits('ni)) -> bits('no) function count_ones (no, x) = { @@ -565,15 +566,15 @@ function unsealCap(cap) : Capability -> Capability = {cap with otype=to_bits(cap_otype_width, otype_unsealed)} function getCapBaseBits(c) : Capability -> CapAddrBits = - let (base, _) = getCapBoundsBits(c) in + let (base, _, _) = getCapBoundsBits(c) in base function getCapBase(c) : Capability -> CapAddrInt = unsigned(getCapBaseBits(c)) function getCapTopBits(c) : Capability -> CapLenBits = - let (base, length) = getCapBoundsBits(c) in { - zero_extend(base) + length + let (_, _, top) = getCapBoundsBits(c) in { + top } function getCapTop (c) : Capability -> CapLen = @@ -587,7 +588,7 @@ function getCapOffset(c) : Capability -> CapAddrInt = unsigned(getCapOffsetBits(c)) function getCapLength(c) : Capability -> CapLen = - let (base, length) = getCapBoundsBits(c) in + let (_, length, _) = getCapBoundsBits(c) in unsigned(length) /*! @@ -598,9 +599,9 @@ function getCapLength(c) : Capability -> CapLen = */ val inCapBounds : (Capability, CapAddrBits, CapLen) -> bool function inCapBounds (cap, addr, size) = { - let (base, length) = getCapBounds(cap); + let (base, length, top) = getCapBounds(cap); let a = unsigned(addr); - (a >= base) & (size <= length) + (a >= base) & (a + size <= top) } function int_to_cap (offset) : CapAddrBits -> Capability = @@ -630,8 +631,8 @@ function clearTag(cap) : Capability -> Capability = clearTagIf(cap, true) function capBoundsEqual (c1, c2) : (Capability, Capability) -> bool = - let (base1, length1) = getCapBounds(c1) in - let (base2, length2) = getCapBounds(c2) in + let (base1, length1, _) = getCapBounds(c1) in + let (base2, length2, _) = getCapBounds(c2) in (base1 == base2) & (length1 == length2) /*! @@ -688,9 +689,8 @@ function incCapAddr(c, delta) = val capToString : (Capability) -> string function capToString (cap) = { - let top = getCapTop(cap); - let top_str = BitStr(to_bits(cap_len_width + 3, top)); - let (base, length) = getCapBoundsBits(cap); + let (base, length, top) = getCapBoundsBits(cap); + let top_str = BitStr(0b000 @ top); let len_str = BitStr(0b000 @ length); BitStr(cap.address) ^ " (v:" ^ (if cap.tag then "1 " else "0 ") diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index a0d4df4..1eca78b 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -661,8 +661,8 @@ function clause execute (CTestSubset(rd, cs1, cs2)) = { let cs1_val = C(cs1); let cs2_val = C(cs2); - let (cs2_base, cs2_length) = getCapBounds(cs2_val); - let (cs1_base, cs1_length) = getCapBounds(cs1_val); + let (cs2_base, cs2_length, cs2_top) = getCapBounds(cs2_val); + let (cs1_base, cs1_length, cs1_top) = getCapBounds(cs1_val); let cs2_perms = getCapPerms(cs2_val); let cs1_perms = getCapPerms(cs1_val); @@ -670,7 +670,7 @@ function clause execute (CTestSubset(rd, cs1, cs2)) = { 0b0 else if cs2_base < cs1_base then 0b0 - else if cs2_base + cs2_length > cs1_base + cs1_length then + else if cs2_top > cs1_top then 0b0 else if (cs2_perms & cs1_perms) != cs2_perms then 0b0 @@ -706,7 +706,7 @@ function clause execute (CSeal(cd, cs1, cs2)) = { let cs2_val = C(cs2); let cs2_addr = unsigned(cs2_val.address); - let (cs2_base, cs2_length) = getCapBounds(cs2_val); + let (cs2_base, cs2_length, cs2_top) = getCapBounds(cs2_val); let isPermittedOtype : bool = if cs1_val.permit_execute then @@ -728,7 +728,7 @@ function clause execute (CSeal(cd, cs1, cs2)) = { & not(isCapSealed(cs2_val)) & cs2_val.permit_seal & (cs2_addr >= cs2_base) - & (cs2_addr < cs2_base + cs2_length) + & (cs2_addr < cs2_top) & isPermittedOtype; let inCap = clearTagIfSealed(cs1_val); @@ -750,14 +750,14 @@ function clause execute (CUnseal(cd, cs1, cs2)) = { let cs1_val = C(cs1); let cs2_val = C(cs2); let cs2_addr = unsigned(cs2_val.address); - let (cs2_base, cs2_length) = getCapBounds(cs2_val); + let (cs2_base, cs2_length, cs2_top) = getCapBounds(cs2_val); let permitted = cs2_val.tag & isCapSealed(cs1_val) & not(isCapSealed(cs2_val)) & (cs2_addr == unsigned(cs1_val.otype)) & cs2_val.permit_unseal & (cs2_addr >= cs2_base) - & (cs2_addr < cs2_base + cs2_length); + & (cs2_addr < cs2_top); let new_global = cs1_val.global & cs2_val.global; let newCap = {unsealCap(cs1_val) with global=new_global}; C(cd) = clearTagIf(newCap, not(permitted));