summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--cheri/cheri_insts.sail236
-rw-r--r--cheri/cheri_prelude.sail30
-rw-r--r--mips/mips_epilogue.sail2
-rw-r--r--mips/mips_insts.sail36
-rw-r--r--mips/mips_prelude.sail25
-rw-r--r--mips/mips_wrappers.sail2
-rw-r--r--src/lem_interp/run_interp_model.ml4
7 files changed, 170 insertions, 165 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index b084faa0..39453fd5 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -49,7 +49,7 @@ function clause execute (CGetX(op, rd, cb)) =
(* START_CGetX *)
checkCP2usable();
if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else
{
cbval := CapRegs[cb];
@@ -73,7 +73,7 @@ function clause execute (CGetPCC(cd)) =
(* START_CGetPCC *)
checkCP2usable();
if (register_inaccessible(cd)) then
- exit (raise_c2_exception_v(cd))
+ raise_c2_exception_v(cd)
else
let pcc = (capRegToCapStruct(PCC)) in
writeCapReg(cd, {pcc with offset = PC})
@@ -87,7 +87,7 @@ function clause execute (CGetPCCSetOffset(cd, rs)) =
(* START_CGetPCCSetOffset *)
checkCP2usable();
if (register_inaccessible(cd)) then
- exit (raise_c2_exception_v(cd))
+ raise_c2_exception_v(cd)
else
let pcc = (capRegToCapStruct(PCC)) in
let rs_val = rGPR(rs) in
@@ -104,7 +104,7 @@ function clause execute (CGetCause(rd)) =
(* START_CGetCause *)
checkCP2usable();
if not (PCC.access_EPCC) then
- exit (raise_c2_exception_noreg(CapEx_AccessEPCCViolation))
+ raise_c2_exception_noreg(CapEx_AccessEPCCViolation)
else
wGPR(rd) := EXTZ(CapCause)
(* END_CGetCause *)
@@ -117,7 +117,7 @@ function clause execute (CSetCause((regno) rt)) =
(* START_CSetCause *)
checkCP2usable();
if not (PCC.access_EPCC) then
- exit (raise_c2_exception_noreg(CapEx_AccessEPCCViolation))
+ raise_c2_exception_noreg(CapEx_AccessEPCCViolation)
else
{
(bit[64]) rt_val := rGPR(rt);
@@ -136,13 +136,13 @@ function clause execute(CAndPerm(cd, cb, rt)) =
cb_val := readCapReg(cb);
rt_val := rGPR(rt);
if (register_inaccessible(cd)) then
- exit (raise_c2_exception_v(cd))
+ raise_c2_exception_v(cd)
else if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if not (cb_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cb))
+ raise_c2_exception(CapEx_TagViolation, cb)
else if (cb_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cb))
+ raise_c2_exception(CapEx_SealViolation, cb)
else
writeCapReg(cd, {cb_val with
sw_perms = (cb_val.sw_perms & (rt_val[30..15]));
@@ -174,11 +174,11 @@ function clause execute(CToPtr(rd, cb, ct)) =
ct_val := readCapReg(ct);
cb_val := readCapReg(cb);
if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if (register_inaccessible(ct)) then
- exit (raise_c2_exception_v(ct))
+ raise_c2_exception_v(ct)
else if not (ct_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, ct))
+ raise_c2_exception(CapEx_TagViolation, ct)
else
{
wGPR(rd) := if not (cb_val.tag) then
@@ -198,9 +198,9 @@ function clause execute(CSub(rd, cb, ct)) =
ct_val := readCapReg(ct);
cb_val := readCapReg(cb);
if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if (register_inaccessible(ct)) then
- exit (raise_c2_exception_v(ct))
+ raise_c2_exception_v(ct)
else
{
wGPR(rd) := (bit[64])(getCapCursor(cb_val) - getCapCursor(ct_val))
@@ -222,9 +222,9 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
(* START_CPtrCmp *)
checkCP2usable();
if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if (register_inaccessible(ct)) then
- exit (raise_c2_exception_v(ct))
+ raise_c2_exception_v(ct)
else
{
cb_val := readCapReg(cb);
@@ -270,11 +270,11 @@ function clause execute (CIncOffset(cd, cb, rt)) =
cb_val := readCapReg(cb);
rt_val := rGPR(rt);
if (register_inaccessible(cd)) then
- exit (raise_c2_exception_v(cd))
+ raise_c2_exception_v(cd)
else if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if ((cb_val.tag) & (cb_val.sealed) & (rt_val != 0x0000000000000000)) then
- exit (raise_c2_exception(CapEx_SealViolation, cb))
+ raise_c2_exception(CapEx_SealViolation, cb)
else
writeCapReg(cd, {cb_val with offset=cb_val.offset+rt_val})
(* END_CIncOffset *)
@@ -289,11 +289,11 @@ function clause execute (CSetOffset(cd, cb, rt)) =
cb_val := readCapReg(cb);
rt_val := rGPR(rt);
if (register_inaccessible(cd)) then
- exit (raise_c2_exception_v(cd))
+ raise_c2_exception_v(cd)
else if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if ((cb_val.tag) & (cb_val.sealed)) then
- exit (raise_c2_exception(CapEx_SealViolation, cb))
+ raise_c2_exception(CapEx_SealViolation, cb)
else
writeCapReg(cd, {cb_val with offset=rt_val})
(* END_CSetOffset *)
@@ -309,17 +309,17 @@ function clause execute (CSetBounds(cd, cb, rt)) =
(nat) rt_val := rGPR(rt);
(nat) cursor := getCapCursor(cb_val);
if (register_inaccessible(cd)) then
- exit (raise_c2_exception_v(cd))
+ raise_c2_exception_v(cd)
else if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if not (cb_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cb))
+ raise_c2_exception(CapEx_TagViolation, cb)
else if (cb_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cb))
+ raise_c2_exception(CapEx_SealViolation, cb)
else if (cursor < ((nat)(cb_val.base))) then
- exit (raise_c2_exception(CapEx_LengthViolation, cb))
+ raise_c2_exception(CapEx_LengthViolation, cb)
else if ((cursor + rt_val) > ((nat)(cb_val.base) + (nat)(cb_val.length))) then
- exit (raise_c2_exception(CapEx_LengthViolation, cb))
+ raise_c2_exception(CapEx_LengthViolation, cb)
else
writeCapReg(cd, {cb_val with base=(bit[64])cursor; length=(bit[64])rt_val; offset=0})
(* END_CSetBounds *)
@@ -332,9 +332,9 @@ function clause execute (CClearTag(cd, cb)) =
(* START_CClearTag *)
checkCP2usable();
if (register_inaccessible(cd)) then
- exit (raise_c2_exception_v(cd))
+ raise_c2_exception_v(cd)
else if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else
{
cb_val := readCapReg(cb);
@@ -357,7 +357,7 @@ function clause execute (ClearRegs(regset, mask)) =
foreach (i from 0 to 15)
let r = ((bit[5]) (i+16)) in
if (mask[i] & register_inaccessible(r)) then
- exit (raise_c2_exception_v(r));
+ raise_c2_exception_v(r);
foreach (i from 0 to 15)
if (mask[i]) then
switch (regset) {
@@ -378,15 +378,15 @@ function clause execute (CFromPtr(cd, cb, rt)) =
cb_val := readCapReg(cb);
rt_val := rGPR(rt);
if (register_inaccessible(cd)) then
- exit (raise_c2_exception_v(cd))
+ raise_c2_exception_v(cd)
else if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if (rt == 0) then
writeCapReg(cd, null_cap)
else if not (cb_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cb))
+ raise_c2_exception(CapEx_TagViolation, cb)
else if (cb_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cb))
+ raise_c2_exception(CapEx_SealViolation, cb)
else
writeCapReg(cd, {cb_val with offset = rt_val});
(* END_CFromPtr *)
@@ -402,11 +402,11 @@ function clause execute (CCheckPerm(cs, rt)) =
cs_perms := capPermsToVec(cs_val);
rt_perms := (rGPR(rt))[30..0];
if (register_inaccessible(cs)) then
- exit (raise_c2_exception_v(cs))
+ raise_c2_exception_v(cs)
else if not (cs_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cs))
+ raise_c2_exception(CapEx_TagViolation, cs)
else if ((cs_perms & rt_perms) != rt_perms) then
- exit (raise_c2_exception(CapEx_UserDefViolation, cs))
+ raise_c2_exception(CapEx_UserDefViolation, cs)
else
()
(* END_CCheckPerm *)
@@ -421,19 +421,19 @@ function clause execute (CCheckType(cs, cb)) =
cs_val := readCapReg(cs);
cb_val := readCapReg(cb);
if (register_inaccessible(cs)) then
- exit (raise_c2_exception_v(cs))
+ raise_c2_exception_v(cs)
else if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if not (cs_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cs))
+ raise_c2_exception(CapEx_TagViolation, cs)
else if not (cb_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cb))
+ raise_c2_exception(CapEx_TagViolation, cb)
else if not (cs_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cs))
+ raise_c2_exception(CapEx_SealViolation, cs)
else if not (cb_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cb))
+ raise_c2_exception(CapEx_SealViolation, cb)
else if ((cs_val.otype) != (cb_val.otype)) then
- exit (raise_c2_exception(CapEx_TypeViolation, cs))
+ raise_c2_exception(CapEx_TypeViolation, cs)
else
()
(* END_CCheckType *)
@@ -449,25 +449,25 @@ function clause execute (CSeal(cd, cs, ct)) =
ct_val := readCapReg(ct);
(nat) ct_cursor := ((nat)(ct_val.base) + (nat)(ct_val.offset));
if (register_inaccessible(cd)) then
- exit (raise_c2_exception_v(cd))
+ raise_c2_exception_v(cd)
else if (register_inaccessible(cs)) then
- exit (raise_c2_exception_v(cs))
+ raise_c2_exception_v(cs)
else if (register_inaccessible(ct)) then
- exit (raise_c2_exception_v(ct))
+ raise_c2_exception_v(ct)
else if not (cs_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cs))
+ raise_c2_exception(CapEx_TagViolation, cs)
else if not (ct_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, ct))
+ raise_c2_exception(CapEx_TagViolation, ct)
else if (cs_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cs))
+ raise_c2_exception(CapEx_SealViolation, cs)
else if (ct_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, ct))
+ raise_c2_exception(CapEx_SealViolation, ct)
else if not (ct_val.permit_seal) then
- exit (raise_c2_exception(CapEx_PermitSealViolation, ct))
+ raise_c2_exception(CapEx_PermitSealViolation, ct)
else if ((nat)(ct_val.offset) >= (nat)(ct_val.length)) then
- exit (raise_c2_exception(CapEx_LengthViolation, ct))
+ raise_c2_exception(CapEx_LengthViolation, ct)
else if (ct_cursor > max_otype) then
- exit (raise_c2_exception(CapEx_LengthViolation, ct))
+ raise_c2_exception(CapEx_LengthViolation, ct)
else
writeCapReg(cd, {cs_val with sealed=true; otype=((bit[24])ct_cursor)})
(* END_CSeal *)
@@ -483,25 +483,25 @@ function clause execute (CUnseal(cd, cs, ct)) =
ct_val := readCapReg(ct);
(nat) ct_cursor := ((nat)(ct_val.base) + (nat)(ct_val.offset));
if (register_inaccessible(cd)) then
- exit (raise_c2_exception_v(cd))
+ raise_c2_exception_v(cd)
else if (register_inaccessible(cs)) then
- exit (raise_c2_exception_v(cs))
+ raise_c2_exception_v(cs)
else if (register_inaccessible(ct)) then
- exit (raise_c2_exception_v(ct))
+ raise_c2_exception_v(ct)
else if not (cs_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cs))
+ raise_c2_exception(CapEx_TagViolation, cs)
else if not (ct_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, ct))
+ raise_c2_exception(CapEx_TagViolation, ct)
else if not (cs_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cs))
+ raise_c2_exception(CapEx_SealViolation, cs)
else if (ct_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, ct))
+ raise_c2_exception(CapEx_SealViolation, ct)
else if (ct_cursor != ((nat)(cs_val.otype))) then
- exit (raise_c2_exception(CapEx_TypeViolation, ct))
+ raise_c2_exception(CapEx_TypeViolation, ct)
else if not (ct_val.permit_seal) then
- exit (raise_c2_exception(CapEx_PermitSealViolation, ct))
+ raise_c2_exception(CapEx_PermitSealViolation, ct)
else if (unsigned(ct_val.offset) >= unsigned(ct_val.length)) then
- exit (raise_c2_exception(CapEx_LengthViolation, ct))
+ raise_c2_exception(CapEx_LengthViolation, ct)
else
writeCapReg(cd, {cs_val with
sealed=false;
@@ -521,27 +521,27 @@ function clause execute (CCall(cs, cb)) =
cs_val := readCapReg(cs);
cb_val := readCapReg(cb);
if (register_inaccessible(cs)) then
- exit (raise_c2_exception_v(cs))
+ raise_c2_exception_v(cs)
else if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if not (cs_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cs))
+ raise_c2_exception(CapEx_TagViolation, cs)
else if not (cb_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cb))
+ raise_c2_exception(CapEx_TagViolation, cb)
else if not (cs_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cs))
+ raise_c2_exception(CapEx_SealViolation, cs)
else if not (cb_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cb))
+ raise_c2_exception(CapEx_SealViolation, cb)
else if ((cs_val.otype) != (cb_val.otype)) then
- exit (raise_c2_exception(CapEx_TypeViolation, cs))
+ raise_c2_exception(CapEx_TypeViolation, cs)
else if not (cs_val.permit_execute) then
- exit (raise_c2_exception(CapEx_PermitExecuteViolation, cs))
+ raise_c2_exception(CapEx_PermitExecuteViolation, cs)
else if (cb_val.permit_execute) then
- exit (raise_c2_exception(CapEx_PermitExecuteViolation, cb))
+ raise_c2_exception(CapEx_PermitExecuteViolation, cb)
else if (cs_val.offset >= cs_val.length) then
- exit (raise_c2_exception(CapEx_LengthViolation, cs))
+ raise_c2_exception(CapEx_LengthViolation, cs)
else
- exit (raise_c2_exception(CapEx_CallTrap, cs));
+ raise_c2_exception(CapEx_CallTrap, cs);
(* END_CCall *)
}
@@ -551,7 +551,7 @@ function clause execute (CReturn) =
{
(* START_CReturn *)
checkCP2usable();
- exit (raise_c2_exception_noreg(CapEx_ReturnTrap))
+ raise_c2_exception_noreg(CapEx_ReturnTrap)
(* END_CReturn *)
}
@@ -564,7 +564,7 @@ function clause execute (CBX(cb, imm, invert)) =
(* START_CBx *)
checkCP2usable();
if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if (((CapRegs[cb]).tag) ^ invert) then
{
let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in
@@ -583,21 +583,21 @@ function clause execute(CJALR(cd, cb, link)) =
checkCP2usable();
cb_val := readCapReg(cb);
if (link & register_inaccessible(cd)) then
- exit (raise_c2_exception_v(cd))
+ raise_c2_exception_v(cd)
else if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if not (cb_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cb))
+ raise_c2_exception(CapEx_TagViolation, cb)
else if (cb_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cb))
+ raise_c2_exception(CapEx_SealViolation, cb)
else if not (cb_val.permit_execute) then
- exit (raise_c2_exception(CapEx_PermitExecuteViolation, cb))
+ raise_c2_exception(CapEx_PermitExecuteViolation, cb)
else if not (cb_val.global) then
- exit (raise_c2_exception(CapEx_GlobalViolation, cb))
+ raise_c2_exception(CapEx_GlobalViolation, cb)
else if (((nat)(cb_val.offset)) + 4 > ((nat) (cb_val.length))) then
- exit (raise_c2_exception(CapEx_LengthViolation, cb))
+ raise_c2_exception(CapEx_LengthViolation, cb)
else if (((cb_val.base+cb_val.offset)[1..0]) != 0b00) then
- exit (SignalException(AdEL))
+ SignalException(AdEL)
else
{
if (link) then
@@ -632,13 +632,13 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
checkCP2usable();
cb_val := readCapReg(cb);
if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if not (cb_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cb))
+ raise_c2_exception(CapEx_TagViolation, cb)
else if (cb_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cb))
+ raise_c2_exception(CapEx_SealViolation, cb)
else if not (cb_val.permit_load) then
- exit (raise_c2_exception(CapEx_PermitLoadViolation, cb))
+ raise_c2_exception(CapEx_PermitLoadViolation, cb)
else
{
size := wordWidthBytes(width);
@@ -646,11 +646,11 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
vAddr := cursor + unsigned(rGPR(rt)) + (size*signed(offset));
vAddr64:= (bit[64]) vAddr;
if ((vAddr + size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
- exit (raise_c2_exception(CapEx_LengthViolation, cb))
+ raise_c2_exception(CapEx_LengthViolation, cb)
else if (vAddr < ((nat) (cb_val.base))) then
- exit (raise_c2_exception(CapEx_LengthViolation, cb))
+ raise_c2_exception(CapEx_LengthViolation, cb)
else if not (isAddressAligned(vAddr64, width)) then
- exit (SignalExceptionBadAddr(AdEL, vAddr64))
+ SignalExceptionBadAddr(AdEL, vAddr64)
else
{
pAddr := (TLBTranslate(vAddr64, LoadData));
@@ -689,13 +689,13 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
checkCP2usable();
cb_val := readCapReg(cb);
if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if not (cb_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cb))
+ raise_c2_exception(CapEx_TagViolation, cb)
else if (cb_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cb))
+ raise_c2_exception(CapEx_SealViolation, cb)
else if not (cb_val.permit_store) then
- exit (raise_c2_exception(CapEx_PermitStoreViolation, cb))
+ raise_c2_exception(CapEx_PermitStoreViolation, cb)
else
{
size := wordWidthBytes(width);
@@ -703,11 +703,11 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
vAddr := cursor + unsigned(rGPR(rt)) + (size * signed(offset));
vAddr64:= (bit[64]) vAddr;
if ((vAddr + size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
- exit (raise_c2_exception(CapEx_LengthViolation, cb))
+ raise_c2_exception(CapEx_LengthViolation, cb)
else if (vAddr < ((nat) (cb_val.base))) then
- exit (raise_c2_exception(CapEx_LengthViolation, cb))
+ raise_c2_exception(CapEx_LengthViolation, cb)
else if not (isAddressAligned(vAddr64, width)) then
- exit (SignalExceptionBadAddr(AdES, vAddr64))
+ SignalExceptionBadAddr(AdES, vAddr64)
else
{
pAddr := (TLBTranslate(vAddr64, StoreData));
@@ -749,33 +749,33 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
cs_val := readCapReg(cs);
cb_val := readCapReg(cb);
if (register_inaccessible(cs)) then
- exit (raise_c2_exception_v(cs))
+ raise_c2_exception_v(cs)
else if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if not (cb_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cb))
+ raise_c2_exception(CapEx_TagViolation, cb)
else if (cb_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cb))
+ raise_c2_exception(CapEx_SealViolation, cb)
else if not (cb_val.permit_store_cap) then
- exit (raise_c2_exception(CapEx_PermitStoreCapViolation, cb))
+ raise_c2_exception(CapEx_PermitStoreCapViolation, cb)
else if not (cb_val.permit_store_local_cap) & (cs_val.tag) & not (cs_val.global) then
- exit (raise_c2_exception(CapEx_PermitStoreLocalCapViolation, cb))
+ raise_c2_exception(CapEx_PermitStoreLocalCapViolation, cb)
else
{
cursor := getCapCursor(cb_val);
vAddr := cursor + unsigned(rGPR(rt)) + (16 * signed(offset));
vAddr64:= (bit[64]) vAddr;
if ((vAddr + cap_size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
- exit (raise_c2_exception(CapEx_LengthViolation, cb))
+ raise_c2_exception(CapEx_LengthViolation, cb)
else if (vAddr < ((nat) (cb_val.base))) then
- exit (raise_c2_exception(CapEx_LengthViolation, cb))
+ raise_c2_exception(CapEx_LengthViolation, cb)
else if (vAddr64[4..0] != 0b00000) then
- exit (SignalExceptionBadAddr(AdES, vAddr64))
+ SignalExceptionBadAddr(AdES, vAddr64)
else
{
let (pAddr, noStoreCap) = (TLBTranslateC(vAddr64, StoreData)) in
if (cs_val.tag & noStoreCap) then
- exit (raise_c2_exception(CapEx_TLBNoStoreCap, cs))
+ raise_c2_exception(CapEx_TLBNoStoreCap, cs)
else if (conditional) then
{
success := if (CP0LLBit[0]) then
@@ -800,26 +800,26 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
checkCP2usable();
cb_val := readCapReg(cb);
if (register_inaccessible(cd)) then
- exit (raise_c2_exception_v(cd))
+ raise_c2_exception_v(cd)
else if (register_inaccessible(cb)) then
- exit (raise_c2_exception_v(cb))
+ raise_c2_exception_v(cb)
else if not (cb_val.tag) then
- exit (raise_c2_exception(CapEx_TagViolation, cb))
+ raise_c2_exception(CapEx_TagViolation, cb)
else if (cb_val.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, cb))
+ raise_c2_exception(CapEx_SealViolation, cb)
else if not (cb_val.permit_load_cap) then
- exit (raise_c2_exception(CapEx_PermitLoadCapViolation, cb))
+ raise_c2_exception(CapEx_PermitLoadCapViolation, cb)
else
{
cursor := getCapCursor(cb_val);
vAddr := cursor + unsigned(rGPR(rt)) + (16*signed(offset));
vAddr64:= (bit[64]) vAddr;
if ((vAddr + cap_size) > ((nat) (cb_val.base) + ((nat) (cb_val.length)))) then
- exit (raise_c2_exception(CapEx_LengthViolation, cb))
+ raise_c2_exception(CapEx_LengthViolation, cb)
else if (vAddr < ((nat) (cb_val.base))) then
- exit (raise_c2_exception(CapEx_LengthViolation, cb))
+ raise_c2_exception(CapEx_LengthViolation, cb)
else if (vAddr64[4..0] != 0b00000) then
- exit (SignalExceptionBadAddr(AdEL, vAddr64))
+ SignalExceptionBadAddr(AdEL, vAddr64)
else
{
let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in
diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail
index 23973782..66115d1a 100644
--- a/cheri/cheri_prelude.sail
+++ b/cheri/cheri_prelude.sail
@@ -342,7 +342,7 @@ typedef CapCauseReg = register bits [15:0] {
register CapCauseReg CapCause
-function unit SignalException ((Exception) ex) =
+function forall Type 'o . 'o SignalException ((Exception) ex) =
{
C31 := PCC;
C31.offset := PC;
@@ -359,7 +359,7 @@ function unit ERETHook() =
that non-capability branches don't override PCC *)
}
-function unit raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) =
+function forall Type 'o . 'o raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) =
{
(CapCause.ExcCode) := CapExCode(capEx);
(CapCause.RegNum) := regnum;
@@ -369,10 +369,10 @@ function unit raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) =
SignalException(mipsEx);
}
-function unit raise_c2_exception((CapEx) capEx, (regno) regnum) =
+function forall Type 'o . 'o raise_c2_exception((CapEx) capEx, (regno) regnum) =
raise_c2_exception8(capEx, 0b000 : regnum)
-function unit raise_c2_exception_v((regno) regnum) =
+function forall Type 'o . 'o raise_c2_exception_v((regno) regnum) =
switch(regnum) {
case 0b11011 -> raise_c2_exception(CapEx_AccessKR1CViolation, regnum)
case 0b11100 -> raise_c2_exception(CapEx_AccessKR2CViolation, regnum)
@@ -382,7 +382,7 @@ function unit raise_c2_exception_v((regno) regnum) =
case _ -> assert(false, Some("should only call for cap reg violation"))
}
-function unit raise_c2_exception_noreg((CapEx) capEx) =
+function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) =
raise_c2_exception8(capEx, 0xff)
function bool register_inaccessible((regno) r) =
@@ -457,22 +457,22 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy
capno := 0b00000;
cap := readCapReg(capno);
if (~(cap.tag)) then
- exit (raise_c2_exception(CapEx_TagViolation, capno))
+ (raise_c2_exception(CapEx_TagViolation, capno))
else if (cap.sealed) then
- exit (raise_c2_exception(CapEx_SealViolation, capno));
+ (raise_c2_exception(CapEx_SealViolation, capno));
switch (accessType) {
- case Instruction -> if (~(cap.permit_execute)) then exit (raise_c2_exception(CapEx_PermitExecuteViolation, capno))
- case LoadData -> if (~(cap.permit_load)) then exit (raise_c2_exception(CapEx_PermitLoadViolation, capno))
- case StoreData -> if (~(cap.permit_store)) then exit (raise_c2_exception(CapEx_PermitStoreViolation, capno))
+ case Instruction -> if (~(cap.permit_execute)) then (raise_c2_exception(CapEx_PermitExecuteViolation, capno))
+ case LoadData -> if (~(cap.permit_load)) then (raise_c2_exception(CapEx_PermitLoadViolation, capno))
+ case StoreData -> if (~(cap.permit_store)) then (raise_c2_exception(CapEx_PermitStoreViolation, capno))
};
cursor := getCapCursor(cap);
vAddr := cursor + unsigned(addr);
vAddr64:= (bit[64]) vAddr;
size := wordWidthBytes(width);
if ((vAddr + size) > ((nat) (cap.base) + ((nat) (cap.length)))) then
- exit (raise_c2_exception(CapEx_LengthViolation, capno))
+ (raise_c2_exception(CapEx_LengthViolation, capno))
else if (vAddr < ((nat) (cap.base))) then
- exit (raise_c2_exception(CapEx_LengthViolation, capno));
+ (raise_c2_exception(CapEx_LengthViolation, capno));
vAddr64;
}
@@ -482,9 +482,9 @@ function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType
let (bit[64]) length = PCC.length in
let (bit[64]) absPC = (base + vAddr) in
if (absPC[1..0] != 0b00) then (* bad PC alignment *)
- exit (SignalExceptionBadAddr(AdEL, absPC))
+ (SignalExceptionBadAddr(AdEL, absPC))
else if ((unsigned(vAddr) + 4) > unsigned(length)) then
- exit (raise_c2_exception_noreg(CapEx_LengthViolation))
+ (raise_c2_exception_noreg(CapEx_LengthViolation))
else
TLBTranslate(absPC, accessType)
}
@@ -494,7 +494,7 @@ function unit checkCP2usable () =
if (~((CP0Status.CU)[2])) then
{
(CP0Cause.CE) := 0b10;
- exit (SignalException(CpU));
+ (SignalException(CpU));
}
}
diff --git a/mips/mips_epilogue.sail b/mips/mips_epilogue.sail
index 6b789639..1b8d64f7 100644
--- a/mips/mips_epilogue.sail
+++ b/mips/mips_epilogue.sail
@@ -37,7 +37,7 @@
union ast member unit RI
function clause decode _ = Some(RI)
function clause execute (RI) =
- exit (SignalException (ResI))
+ SignalException (ResI)
end decode
end execute
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index 6e1f0a06..fac2aa52 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -85,7 +85,7 @@ function clause execute (DADDI (rs, rt, imm)) =
let (bit[65]) sum65 = (EXTS(rGPR(rs)) + EXTS(imm)) in
{
if (sum65[64] != sum65[63]) then
- exit (SignalException(Ov))
+ (SignalException(Ov))
else
wGPR(rt) := sum65[63..0]
}
@@ -104,7 +104,7 @@ function clause execute (DADD (rs, rt, rd)) =
let (bit[65]) sum65 = (EXTS(rGPR(rs)) + EXTS(rGPR(rt))) in
{
if sum65[64] != sum65[63] then
- exit (SignalException(Ov))
+ (SignalException(Ov))
else
wGPR(rd) := sum65[63..0]
}
@@ -126,7 +126,7 @@ function clause execute (ADD(rs, rt, rd)) =
else
let (bit[33]) sum33 = (EXTS(opA[31 .. 0]) + EXTS(opB[31 .. 0])) in
if sum33[32] != sum33[31] then
- exit (SignalException(Ov))
+ (SignalException(Ov))
else
wGPR(rd) := EXTS(sum33[31..0])
}
@@ -146,7 +146,7 @@ function clause execute (ADDI(rs, rt, imm)) =
else
let (bit[33]) sum33 = (EXTS(opA[31 .. 0]) + EXTS(imm)) in
if sum33[32] != sum33[31] then
- exit (SignalException(Ov))
+ (SignalException(Ov))
else
wGPR(rt) := EXTS(sum33[31..0])
}
@@ -213,7 +213,7 @@ function clause execute (DSUB (rs, rt, rd)) =
let (bit[65]) temp65 = (EXTS(rGPR(rs)) - EXTS(rGPR(rt))) in
{
if temp65[64] != temp65[63] then
- exit (SignalException(Ov))
+ (SignalException(Ov))
else
wGPR(rd) := temp65[63..0]
}
@@ -231,11 +231,11 @@ function clause execute (SUB(rs, rt, rd)) =
(bit[64]) opA := rGPR(rs);
(bit[64]) opB := rGPR(rt);
if NotWordVal(opA) | NotWordVal(opB) then
- wGPR(rd) := undefined (* XXX could exit instead *)
+ wGPR(rd) := undefined (* XXX could instead *)
else
let (bit[33]) temp33 = (EXTS(opA[31..0]) - EXTS(opB[31..0])) in
if temp33[32] != temp33[31] then
- exit (SignalException(Ov))
+ (SignalException(Ov))
else
wGPR(rd) := EXTS(temp33[31..0])
}
@@ -1013,7 +1013,7 @@ function clause decode (0b000000 : (bit[20]) code : 0b001100) =
Some(SYSCALL) (* code is ignored *)
function clause execute (SYSCALL) =
{
- exit (SignalException(Sys))
+ (SignalException(Sys))
}
(* BREAK is identical to SYSCALL exception for the exception raised *)
@@ -1022,7 +1022,7 @@ function clause decode (0b000000 : (bit[20]) code : 0b001101) =
Some(BREAK) (* code is ignored *)
function clause execute (BREAK) =
{
- exit (SignalException(Bp))
+ (SignalException(Bp))
}
(* Accept WAIT as a NOP *)
@@ -1053,7 +1053,7 @@ function clause execute (TRAPREG(rs, rt, cmp)) =
rt_val := rGPR(rt);
condition := compare(cmp, rs_val, rt_val);
if (condition) then
- exit (SignalException(Tr))
+ (SignalException(Tr))
}
@@ -1077,7 +1077,7 @@ function clause execute (TRAPIMM(rs, imm, cmp)) =
imm_val := EXTS(imm);
condition := compare(cmp, rs_val, imm_val);
if (condition) then
- exit (SignalException(Tr))
+ (SignalException(Tr))
}
(**************************************************************************************)
@@ -1107,7 +1107,7 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) =
{
(bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, width);
if ~ (isAddressAligned(vAddr, width)) then
- exit (SignalExceptionBadAddr(AdEL, vAddr)) (* unaligned access *)
+ (SignalExceptionBadAddr(AdEL, vAddr)) (* unaligned access *)
else
let pAddr = (TLBTranslate(vAddr, LoadData)) in
{
@@ -1148,7 +1148,7 @@ function clause execute (Store(width, conditional, base, rt, offset)) =
(bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), StoreData, width);
(bit[64]) rt_val := rGPR(rt);
if ~ (isAddressAligned(vAddr, width)) then
- exit (SignalExceptionBadAddr(AdES, vAddr)) (* unaligned access *)
+ (SignalExceptionBadAddr(AdES, vAddr)) (* unaligned access *)
else
let pAddr = (TLBTranslate(vAddr, StoreData)) in
{
@@ -1457,7 +1457,7 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
case (0b10011,0b000) -> 0 (* 19, WatchHi *)
case (0b10100,0b000) -> TLBXContext (* 20, XContext *)
case (0b11110,0b000) -> CP0ErrorEPC (* 30, ErrorEPC *)
- case _ -> {exit (SignalException(ResI)); 0}
+ case _ -> (SignalException(ResI))
} in
wGPR(rt) := if (double) then result else EXTS(result[31..0])
}
@@ -1526,7 +1526,7 @@ function clause execute (MTC0(rt, rd, sel, double)) = {
case (0b10000,0b000) -> () (* XXX ignore K0 cache config 16: Config0 *)
case (0b10100,0b000) -> (TLBXContext.PTEBase) := (reg_val[63..33])
case (0b11110,0b000) -> CP0ErrorEPC := reg_val (* 30, ErrorEPC *)
- case _ -> exit (SignalException(ResI))
+ case _ -> (SignalException(ResI))
}
}
@@ -1542,7 +1542,7 @@ function unit TLBWriteEntry((TLBIndexT) idx) = {
case 0x0fff -> ()
case 0x3fff -> ()
case 0xffff -> ()
- case _ -> exit (SignalException(MCheck))
+ case _ -> (SignalException(MCheck))
};
((TLBEntries[idx]).pagemask) := pagemask;
((TLBEntries[idx]).r ) := TLBEntryHi.R;
@@ -1627,14 +1627,14 @@ function clause decode (0b011111 : 0b00000 : (regno) rt : (regno) rd : 0b00000 :
function clause execute (RDHWR(rt, rd)) = {
let accessLevel = getAccessLevel() in
if ((accessLevel != Kernel) & (~((CP0Status.CU)[0])) & ~(CP0HWREna[rd])) then
- exit (SignalException(ResI));
+ (SignalException(ResI));
let (bit[64]) temp = switch (rd) {
case 0b00000 -> EXTZ([bitzero]) (* CPUNum *)
case 0b00001 -> EXTZ([bitzero]) (* SYNCI_step *)
case 0b00010 -> EXTZ(CP0Count) (* Count *)
case 0b00011 -> EXTZ([bitone]) (* Count resolution *)
case 0b11101 -> CP0UserLocal (* User local register *)
- case _ -> exit (SignalException(ResI))
+ case _ -> (SignalException(ResI))
} in
wGPR(rt) := temp;
}
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 27efc4b5..957ce041 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -396,7 +396,7 @@ function (bit[5]) ExceptionCode ((Exception) ex) =
-function unit SignalExceptionMIPS ((Exception) ex, (bit[64]) kccBase) =
+function forall Type 'o. 'o SignalExceptionMIPS ((Exception) ex, (bit[64]) kccBase) =
{
(* Only update EPC and BD if not already in EXL mode *)
if (~ (CP0Status.EXL)) then
@@ -433,17 +433,18 @@ function unit SignalExceptionMIPS ((Exception) ex, (bit[64]) kccBase) =
nextPC := ((bit[64])(vectorBase + EXTS(vectorOffset))) - kccBase;
CP0Cause.ExcCode := ExceptionCode(ex);
CP0Status.EXL := 1;
+ exit ();
}
-val Exception -> unit effect {rreg, wreg} SignalException
+val forall Type 'o . Exception -> 'o effect {escape, rreg, wreg} SignalException
-function unit SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) =
+function forall Type 'o. 'o SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) =
{
CP0BadVAddr := badAddr;
SignalException(ex);
}
-function unit SignalExceptionTLB((Exception) ex, (bit[64]) badAddr) = {
+function forall Type 'o. 'o SignalExceptionTLB((Exception) ex, (bit[64]) badAddr) = {
CP0BadVAddr := badAddr;
(TLBContext.BadVPN2) := (badAddr[31..13]);
(TLBXContext.BadVPN2):= (badAddr[39..13]);
@@ -473,7 +474,7 @@ function unit checkCP0Access () =
if ((accessLevel != Kernel) & (~((CP0Status.CU)[28]))) then
{
(CP0Cause.CE) := 0b00;
- exit (SignalException(CpU));
+ SignalException(CpU);
}
}
@@ -492,7 +493,7 @@ function unit incrementCP0Count() = {
let exl = CP0Status.EXL in
let erl = CP0Status.ERL in
if ((~(exl)) & (~(erl)) & ie & ((ips & ims) != 0x00)) then
- exit (SignalException(Int));
+ SignalException(Int);
}
function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) =
@@ -543,13 +544,13 @@ function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessT
else
(entry.caps0, entry.capl0, entry.pfn0, entry.d0, entry.v0) in
if (~(v)) then
- exit (SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr))
+ (SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr))
else if ((accessType == StoreData) & ~(d)) then
- exit (SignalExceptionTLB(TLBMod, vAddr))
+ (SignalExceptionTLB(TLBMod, vAddr))
else
(EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]),
if (accessType == StoreData) then caps else capl)
- case None -> exit (SignalExceptionTLB(
+ case None -> (SignalExceptionTLB(
if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr))
}
}
@@ -571,17 +572,17 @@ function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessT
case 0b00 -> (User, None) (* xuseg - user mapped *)
} in
if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then
- exit (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
+ (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
let (pa, c) = switch(addr) {
case (Some(a)) -> (a, false)
case None -> if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then
- exit (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
+ (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
TLBTranslate2(vAddr, accessType)
}
in if (unsigned(pa) > MAX_PA) then
- exit (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
+ (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
(pa, c)
}
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
index 03d03cec..cda96b2c 100644
--- a/mips/mips_wrappers.sail
+++ b/mips/mips_wrappers.sail
@@ -53,7 +53,7 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy
function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = {
incrementCP0Count();
if (vAddr[1..0] != 0b00) then (* bad PC alignment *)
- exit (SignalExceptionBadAddr(AdEL, vAddr))
+ (SignalExceptionBadAddr(AdEL, vAddr))
else
TLBTranslate(vAddr, accessType)
}
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 034fd991..87eafa56 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -245,6 +245,10 @@ let run
| Error0 s ->
errorf "%s: %s: %s\n" (grey name) (red "error") s;
(false, mode, !track_dependencies, env)
+ | Escape (None, _) ->
+ show "exiting current instruction" "" "" "";
+ interactf "%s: %s\n" (grey name) (blue "done");
+ (true, mode, !track_dependencies, env)
| Fail0 (Some s) ->
errorf "%s: %s: %s\n" (grey name) (red "assertion failed") s;
(false, mode, !track_dependencies, env)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 05:52:10 +0000