Banish exit from the mips/cheri sail except at end of SignalException function. There is a plan to replace this syntax with something more understandable. Should make no functional difference using sequential interpretor but will need to do some work on exception functions when integrating with ppcmem so that it know register writes are exceptional etc.

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)