summaryrefslogtreecommitdiff
path: root/cheri
diff options
context:
space:
mode:
Diffstat (limited to 'cheri')
-rw-r--r--cheri/cheri_insts.sail85
-rw-r--r--cheri/cheri_prelude_128.sail46
-rw-r--r--cheri/cheri_prelude_256.sail15
-rw-r--r--cheri/cheri_prelude_common.sail24
4 files changed, 100 insertions, 70 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 0a286070..101414f8 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -73,7 +73,7 @@ function clause execute (CGetType(rd, cb)) =
let capVal = readCapReg(cb) in
wGPR(rd) := if (capVal.sealed)
then EXTZ(capVal.otype)
- else -1
+ else (bitone ^^ 64)
(* END_CGetType *)
}
@@ -110,8 +110,9 @@ function clause execute (CGetLen(rd, cb)) =
else
let capVal = readCapReg(cb) in
let len65 = getCapLength(capVal) in
- let len64 = (if len65 > MAX_U64 then MAX_U64 else len65) in
- wGPR(rd) := (bit[64]) len64;
+ wGPR(rd) := (if len65 > MAX_U64 then MAX_U64 else len65);
+ (*let (uint64) len64 = (if len65 > MAX_U64 then MAX_U64 else len65) in
+ wGPR(rd) := (bit[64]) len64;*)
(* END_CGetLen *)
}
@@ -123,7 +124,7 @@ function clause execute (CGetTag(rd, cb)) =
raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
else
let capVal = readCapReg(cb) in
- wGPR(rd) := EXTZ(capVal.tag);
+ wGPR(rd) := EXTZ([capVal.tag]);
(* END_CGetTag *)
}
@@ -135,7 +136,7 @@ function clause execute (CGetSealed(rd, cb)) =
raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
else
let capVal = readCapReg(cb) in
- wGPR(rd) := EXTZ(capVal.sealed);
+ wGPR(rd) := EXTZ([capVal.sealed]);
(* END_CGetSealed *)
}
@@ -150,7 +151,7 @@ function clause execute (CGetPCC(cd)) =
else
let pcc = (capRegToCapStruct(PCC)) in
let (success, pcc2) = setCapOffset(pcc, PC) in
- {assert (success, None); (* guaranteed to be in-bounds *)
+ {assert (success, ""); (* guaranteed to be in-bounds *)
writeCapReg(cd, pcc2)};
(* END_CGetPCC *)
}
@@ -279,7 +280,7 @@ function clause execute(CSub(rd, cb, ct)) =
raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
else
{
- wGPR(rd) := (bit[64])(getCapCursor(cb_val) - getCapCursor(ct_val))
+ wGPR(rd) := (bit[64])(to_svec(getCapCursor(cb_val) - getCapCursor(ct_val)))
}
(* END_CSub *)
}
@@ -325,7 +326,7 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
ltu := (cursor1 < cursor2);
lts := (((bit[64])cursor1) <_s ((bit[64])cursor2));
};
- wGPR(rd) := EXTZ(switch (op) {
+ wGPR(rd) := EXTZ ((bool[1]) (switch (op) {
case CEQ -> [equal]
case CNE -> [not (equal)]
case CLT -> [lts]
@@ -334,7 +335,7 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
case CLEU -> [ltu | equal]
case CEXEQ -> [cb_val == ct_val]
case CNEXEQ -> [cb_val != ct_val]
- })
+ }))
}
(* END_CPtrCmp *)
}
@@ -574,8 +575,8 @@ function clause execute (CBuildCap(cd, cb, ct)) =
let (representable, cd2) = setCapOffset(cd1, (bit[64]) ct_offset) in
let cd3 = setCapPerms(cd2, ct_perms) in
{
- assert(exact, None); (* base and top came from ct originally so will be exact *)
- assert(representable, None); (* similarly offset should be representable XXX except for fastRepCheck *)
+ assert(exact, ""); (* base and top came from ct originally so will be exact *)
+ assert(representable, ""); (* similarly offset should be representable XXX except for fastRepCheck *)
writeCapReg(cd, cd3);
}
(* END_CBuildCap *)
@@ -609,11 +610,11 @@ function clause execute (CCopyType(cd, cb, ct)) =
raise_c2_exception(CapEx_LengthViolation, cb)
else
let (success, cap) = setCapOffset(cb_val, (bit[64]) (ct_otype - cb_base)) in {
- assert(success, None); (* offset is in bounds so must succeed *)
+ assert(success, ""); (* offset is in bounds so must succeed *)
writeCapReg(cd, cap);
}
} else
- writeCapReg(cd, int_to_cap(-1))
+ writeCapReg(cd, int_to_cap(bitone ^^ 64))
(* END_CCopyType *)
}
@@ -624,7 +625,7 @@ function clause execute (CCheckPerm(cs, rt)) =
(* START_CCheckPerm *)
checkCP2usable();
cs_val := readCapReg(cs);
- cs_perms := EXTZ(getCapPerms(cs_val));
+ cs_perms := (bit[64]) (EXTZ(getCapPerms(cs_val)));
rt_perms := rGPR(rt);
if (register_inaccessible(cs)) then
raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
@@ -725,7 +726,7 @@ function clause execute (CCSeal(cd, cs, ct)) =
raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
else if not (cs_val.tag) then
raise_c2_exception(CapEx_TagViolation, cs)
- else if (not (ct_val.tag)) | (getCapCursor(ct_val) == -1) then
+ else if (not (ct_val.tag)) | (getCapCursor(ct_val) == unsigned(bitone ^^ 64)) then
writeCapReg(cd, cs_val)
else if (cs_val.sealed) then
raise_c2_exception(CapEx_SealViolation, cs)
@@ -939,7 +940,7 @@ function clause execute(CJALR(cd, cb, link)) =
if (success) then
writeCapReg(cd, linkCap)
else
- assert(false, None);
+ assert(false, "");
delayedPC := (bit[64]) (getCapOffset(cb_val));
delayedPCC := capStructToCapReg(cb_val);
branchPending := 1;
@@ -982,7 +983,7 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
size := wordWidthBytes(width);
cursor := getCapCursor(cb_val);
vAddr := cursor + unsigned(rGPR(rt)) + (size*signed(offset));
- vAddr64:= (bit[64]) vAddr;
+ vAddr64:= (bit[64]) (to_svec(vAddr));
if ((vAddr + size) > getCapTop(cb_val)) then
raise_c2_exception(CapEx_LengthViolation, cb)
else if (vAddr < getCapBase(cb_val)) then
@@ -993,18 +994,23 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
{
pAddr := (TLBTranslate(vAddr64, LoadData));
widthBytes := wordWidthBytes(width);
- memResult := if (linked) then
+ (bit[64]) memResult := if (linked) then
{
CP0LLBit := 0b1;
CP0LLAddr := pAddr;
- MEMr_reserve_wrapper(pAddr, widthBytes);
+ if widthBytes == 1 then extendLoad(MEMr_reserve_wrapper(pAddr, 1), signext)
+ else if widthBytes == 2 then extendLoad(MEMr_reserve_wrapper(pAddr, 2), signext)
+ else if widthBytes == 4 then extendLoad(MEMr_reserve_wrapper(pAddr, 4), signext)
+ else extendLoad(MEMr_reserve_wrapper(pAddr, 8), signext)
}
else
- MEMr_wrapper(pAddr, widthBytes);
- if (signext) then
- wGPR(rd) := EXTS(memResult)
- else
- wGPR(rd) := EXTZ(memResult)
+ {
+ if widthBytes == 1 then extendLoad(MEMr_wrapper(pAddr, 1), signext)
+ else if widthBytes == 2 then extendLoad(MEMr_wrapper(pAddr, 2), signext)
+ else if widthBytes == 4 then extendLoad(MEMr_wrapper(pAddr, 4), signext)
+ else extendLoad(MEMr_wrapper(pAddr, 8), signext)
+ };
+ wGPR(rd) := memResult;
}
}
(* END_CLoad *)
@@ -1039,7 +1045,7 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
size := wordWidthBytes(width);
cursor := getCapCursor(cb_val);
vAddr := cursor + unsigned(rGPR(rt)) + (size * signed(offset));
- vAddr64:= (bit[64]) vAddr;
+ vAddr64:= (bit[64]) (to_svec(vAddr));
if ((vAddr + size) > getCapTop(cb_val)) then
raise_c2_exception(CapEx_LengthViolation, cb)
else if (vAddr < getCapBase(cb_val)) then
@@ -1052,7 +1058,7 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
rs_val := rGPR(rs);
if (conditional) then
{
- success := if (CP0LLBit[0]) then
+ (bool) success := if (CP0LLBit[0]) then
switch(width)
{
case B -> MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0])
@@ -1102,7 +1108,7 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
{
cursor := getCapCursor(cb_val);
vAddr := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset));
- vAddr64:= (bit[64]) vAddr;
+ vAddr64:= (bit[64]) (to_svec(vAddr));
if ((vAddr + cap_size) > getCapTop(cb_val)) then
raise_c2_exception(CapEx_LengthViolation, cb)
else if (vAddr < getCapBase(cb_val)) then
@@ -1149,7 +1155,7 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
{
cursor := getCapCursor(cb_val);
vAddr := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset));
- vAddr64:= (bit[64]) vAddr;
+ vAddr64:= (bit[64]) (to_svec(vAddr));
if ((vAddr + cap_size) > getCapTop(cb_val)) then
raise_c2_exception(CapEx_LengthViolation, cb)
else if (vAddr < getCapBase(cb_val)) then
@@ -1159,17 +1165,18 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
else
{
let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in
- let (tag, mem) = (if (linked)
- then
- {
- CP0LLBit := 0b1;
- CP0LLAddr := pAddr;
- MEMr_tagged_reserve(pAddr);
- }
- else
- (MEMr_tagged(pAddr)))
- in
- (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & not (suppressTag), mem);
+ if (linked) then
+ {
+ CP0LLBit := 0b1;
+ CP0LLAddr := pAddr;
+ let (tag, mem) = MEMr_tagged_reserve(pAddr) in
+ (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem);
+ }
+ else
+ {
+ let (tag, mem) = MEMr_tagged(pAddr) in
+ (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem);
+ }
}
}
(* END_CLC *)
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index 98b0a40c..f1f33a56 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -35,6 +35,14 @@
(* 128 bit cap + tag *)
typedef CapReg = bit[129]
+val cast bool -> bit effect pure cast_bool_bit
+val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec
+val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec
+function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v)
+val extern bool -> bool effect pure not
+
+typedef uint64 = range<0, (2** 64) - 1>
+
typedef CapStruct = const struct {
bool tag;
bit[4] uperms;
@@ -85,9 +93,9 @@ def Nat cap_size_t = 16 (* cap size in bytes *)
let ([:cap_size_t:]) cap_size = 16
function CapStruct capRegToCapStruct((CapReg) c) =
- let (bool) s = c[104] in
- let (bit[20]) B = if s then c[103..96] : 0x000 else c[103..84] in
- let (bit[20]) T = if s then c[83..76] : 0x000 else c[83..64] in
+ let (bool) s = c[104] in
+ let (bit[20]) Bc = if s then c[103..96] : 0x000 else c[103..84] in
+ let (bit[20]) Tc = if s then c[83..76] : 0x000 else c[83..64] in
let (bit[24]) otype = if s then c[95..84] : c[75..64] else 0 in
{
tag = c[128];
@@ -106,8 +114,8 @@ function CapStruct capRegToCapStruct((CapReg) c) =
reserved = c[112..111];
E = c[110..105] ^ 0b110000;
sealed = s;
- B = B;
- T = T;
+ B = Bc;
+ T = Tc;
otype = otype;
address = c[63..0];
}
@@ -175,30 +183,30 @@ function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) =
(false, cap (* was undefined but ocaml shallow embedding can't handle it *) )
function [|-1:1|] a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) =
- switch (a_mid <_u R, bound <_u R) {
- case (bitzero, bitzero) -> 0
- case (bitzero, bitone) -> 1
- case (bitone, bitzero) -> -1
- case (bitone, bitone) -> 0
+ switch (a_mid < R, bound < R) {
+ case (false, false) -> 0
+ case (false, true) -> 1
+ case (true, false) -> -1
+ case (true, true) -> 0
}
function uint64 getCapBase((CapStruct) c) =
let ([|45|]) E = min(unsigned(c.E), 45) in
- let (bit[20]) B = c.B in
+ let (bit[20]) Bc = c.B in
let (bit[65]) a = EXTZ(c.address) in
- let (bit[20]) R = B - 0x01000 in (* wraps *)
+ let (bit[20]) R = Bc - 0x01000 in (* wraps *)
let (bit[20]) a_mid = a[(E + 19)..E] in
- let correction = a_top_correction(a_mid, R, B) in
+ let correction = a_top_correction(a_mid, R, Bc) in
let a_top = a >> (E+20) in
- let (bit[64]) base = EXTZ((a_top + correction) : B) << E in
+ let (bit[64]) base = EXTZ((a_top + correction) : Bc) << E in
unsigned(base)
function CapLen getCapTop ((CapStruct) c) =
let ([|45|]) E = min(unsigned(c.E), 45) in
- let (bit[20]) B = c.B in
+ let (bit[20]) Bc = c.B in
let (bit[20]) T = c.T in
let (bit[65]) a = EXTZ(c.address) in
- let (bit[20]) R = B - 0x01000 in (* wraps *)
+ let (bit[20]) R = Bc - 0x01000 in (* wraps *)
let (bit[20]) a_mid = a[(E + 19)..E] in
let correction = a_top_correction(a_mid, R, T) in
let a_top = a >> (E+20) in
@@ -283,10 +291,10 @@ function [|48|] computeE ((bit[65]) rlength) =
function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) =
(* {cap with base=base; length=(bit[64]) length; offset=0} *)
let ([|48|]) e = computeE(top - (0b0 : base)) in
- let (bit[20]) B = base[(19+e)..e] in
- let (bit[20]) T = top[(19+e)..e] in
+ let (bit[20]) Bc = base[19+e..e] in
+ let (bit[20]) T = top[19+e..e] in
let (bit[20]) T2 = T + if (top[(e - 1)..0] == 0) then 0 else 1 in
- let newCap = {cap with E=(bit[6]) e; B=B; T=T2} in
+ let newCap = {cap with E=(bit[6]) e; B=Bc; T=T2} in
let newBase = getCapBase(newCap) in
let newTop = getCapTop(newCap) in
let exact = (base == newBase) & (top == newTop) in
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index ee9a91ac..7cf3d69c 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -36,7 +36,10 @@
typedef CapReg = bit[257]
val cast bool -> bit effect pure cast_bool_bit
-val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_bool_vec
+val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec
+val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec
+function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v)
+val extern bool -> bool effect pure not
typedef uint64 = range<0, (2** 64) - 1>
@@ -188,13 +191,13 @@ function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) =
function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) =
(true, {cap with sealed=true; otype=otype})
-function uint64 getCapBase((CapStruct) c) = unsigned(c.base)
-function CapLen getCapTop((CapStruct) c) = unsigned(c.base) + unsigned(c.length)
-function uint64 getCapOffset((CapStruct) c) = unsigned(c.offset)
-function CapLen getCapLength((CapStruct) c) = unsigned(c.length)
+function bit[64] getCapBase((CapStruct) c) = c.base
+function [|0:2**65 - 2|] getCapTop((CapStruct) c) = unsigned(c.base) + unsigned(c.length)
+function bit[64] getCapOffset((CapStruct) c) = c.offset
+function CapLen getCapLength((CapStruct) c) = unsigned(c.length)
function uint64 getCapCursor((CapStruct) cap) =
- (unsigned(cap.base) + unsigned(cap.offset)) mod (2 ** 64)
+ (unsigned(cap.base) + unsigned(cap.offset)) mod (pow2(64))
function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) =
(true, {c with offset=offset})
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index dcb56d01..f5fcd095 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -32,6 +32,16 @@
(* SUCH DAMAGE. *)
(*========================================================================*)
+
+scattered typedef ast = const union
+
+val ast -> unit effect {barr, eamem, escape, rmem, rmemt, rreg, undef, wmvt, wreg} execute
+scattered function unit execute
+
+val bit[32] -> option<ast> effect pure decode
+scattered function option<ast> decode
+
+
register CapReg PCC
register CapReg nextPCC
register CapReg delayedPCC
@@ -74,7 +84,7 @@ let (vector <0, 32, inc, (register<CapReg>)>) CapRegs =
C21, C22, C23, C24, C25, C26, C27, C28, C29, C30, C31
]
-let (nat) max_otype = 0xffffff
+let max_otype = MAX(24) (*0xffffff*)
let have_cp2 = true
function (CapStruct) readCapReg((regno) n) =
@@ -204,7 +214,7 @@ function bool pcc_access_system_regs () =
(pcc.access_system_regs)
function bool register_inaccessible((regno) r) =
- let is_sys_reg = switch(r) {
+ let (bool) is_sys_reg = switch(r) {
case 0b11011 -> true
case 0b11100 -> true
case 0b11101 -> true
@@ -249,7 +259,8 @@ function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_
MEMval_tag_conditional(addr, cap_size, tag, reverse_endianness(data));
}
-function unit effect {wmem} MEMw_wrapper(addr, size, data) =
+val forall Nat 'n, 'n >= 1. (bit[64], [:'n:], bit[8 * 'n]) -> unit effect {wmvt, wreg, eamem} MEMw_wrapper
+function unit effect {wmvt, wreg, eamem} MEMw_wrapper(addr, size, data) =
let ledata = reverse_endianness(data) in
if (addr == 0x000000007f000000) then
{
@@ -263,7 +274,8 @@ function unit effect {wmem} MEMw_wrapper(addr, size, data) =
MEMval_tag(addr, size, false, ledata);
}
-function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
+val forall Nat 'n, 'n >= 1. (bit[64], [:'n:], bit[8 * 'n]) -> bool effect {wmvt, eamem} MEMw_conditional_wrapper
+function bool effect {wmvt, eamem} MEMw_conditional_wrapper(addr, size, data) =
{
(* On cheri non-capability writes must clear the corresponding tag*)
MEMea_conditional(addr, size);
@@ -293,7 +305,7 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy
else if (vAddr < (base)) then
(raise_c2_exception(CapEx_LengthViolation, capno))
else
- (bit[64]) vAddr; (* XXX vAddr not truncated because top <= 2^64 and size > 0 *)
+ (bit[64]) (to_vec(vAddr)); (* XXX vAddr not truncated because top <= 2^64 and size > 0 *)
}
function (bit[64]) TranslatePC ((bit[64]) vAddr) = {
@@ -311,7 +323,7 @@ function (bit[64]) TranslatePC ((bit[64]) vAddr) = {
}
function unit checkCP2usable () =
- if not ((CP0Status.CU)[2]) then
+ if not ((norm_dec (CP0Status.CU))[2]) then
{
(CP0Cause.CE) := 0b10;
(SignalException(CpU));
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 22:44:02 +0000