Skip to content

Commit

Permalink
getCapBounds now returns all three: base, length and top. fixed the s…
Browse files Browse the repository at this point in the history 
…ource of error in pdf (PDF is still inconsitent with sail spec)
  • Loading branch information
@vmurali
vmurali committed Oct 10, 2024
1 parent a9b51ec commit b43baea
Show file tree
Hide file tree
Showing 4 changed files with 31 additions and 38 deletions.
2 changes: 1 addition & 1 deletion archdoc/chap-isaref-riscv.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
21 changes: 7 additions & 14 deletions properties/props.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 --> (
Expand All @@ -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
Expand All @@ -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;
Expand Down Expand Up @@ -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
Expand All @@ -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 */
Expand Down
32 changes: 16 additions & 16 deletions src/cheri_cap_common.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -404,20 +404,21 @@ 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);
let a_hi = if a_mid <_u c.B then 1 else 0;
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) = {
Expand Down Expand Up @@ -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 =
Expand All @@ -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)

/*!
Expand All @@ -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 =
Expand Down Expand Up @@ -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)

/*!
Expand Down Expand Up @@ -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 ")
Expand Down
14 changes: 7 additions & 7 deletions src/cheri_insts.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -661,16 +661,16 @@ 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);

let result = if cs1_val.tag != cs2_val.tag then
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
Expand Down Expand Up @@ -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
Expand All @@ -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);
Expand All @@ -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));
Expand Down

0 comments on commit b43baea

Please sign in to comment.