Cheri-research/cheri-cap-lib
1
0
Fork 0
Code Issues 1 Pull Requests Actions Packages Projects Releases Wiki Activity

Extend forallCap to include almightyCap

Browse Source
This commit is contained in:
Peter Rugg
2025-03-04 14:43:05 +00:00
parent 7c9559524b
commit 199e3c9f7f
1 changed files with 14 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

21
CHERICapProps.bsv
View File

@@ -49,12 +49,18 @@ function Bool implies(Bool x, Bool y) = !x || y;
function Bool forallBaseAndLen(CapAddr base, CapAddr len,
function Bool prop(CapPipe cap));
Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
return baseCap.exact && implies
( boundedCap.exact
, prop(boundedCap.value)
);
Bool ret = ?;
if (base == 0 && ~len == 0) begin
ret = prop(almightyCap);
end else begin
Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
ret = baseCap.exact && implies
( boundedCap.exact
, prop(boundedCap.value)
);
end
return ret;
endfunction
// Furthermore, every valid capability can be reached by calling setAddr on
@@ -137,7 +143,8 @@ endfunction
(* noinline *)
function Bool prop_getTop(CapAddr base, CapAddr len, CapAddr addr);
function prop(cap) = getTop(cap) == zeroExtend(base) + zeroExtend(len);
Bool reqAlmighty = ~len == 0;
function prop(cap) = getTop(cap) == zeroExtend(base) + (reqAlmighty ? {1'b1, 0} : zeroExtend(len));
return forallCap(base, len, addr, prop);
endfunction