fix cheri and mips sail following change to type of TranslateAddress -- can now write registers hence call SignalException instead of returning option<err> .

3 files changed, 14 insertions, 17 deletions

diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail
index 6aaa9a0c..7c5e34a9 100644
--- a/cheri/cheri_prelude.sail
+++ b/cheri/cheri_prelude.sail
@@ -407,12 +407,12 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy
     vAddr64;
   }
 
-function (option<Exception>, option<bit[64]>) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) =
+function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) =
   let (bit[257]) x = PCC in
   let (bit[64])  base = x[127..64] in
   let (bit[64])  length = x[63..0] in
   let (bit[64])  absPC = (base + vAddr) in
   if ((unsigned(vAddr) + 4) > unsigned(length)) then
-    (Some(C2E), None) (* XXX take exception properly *)
+    exit (raise_c2_exception_noreg(CapEx_LengthViolation)) (* XXX take exception properly *)
   else
     TLBTranslate(absPC, accessType)
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index b3fb9a32..5e741104 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -194,28 +194,25 @@ function unit SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) =
 
 typedef MemAccessType = enumerate {Instruction; LoadData; StoreData}
 typedef AccessLevel   = enumerate {Kernel; Supervisor; User}
-function (option<Exception>, option<bit[64]>) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = 
+function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = 
   {
-    err := (if (accessType == StoreData) then Some(AdES) else Some(AdEL));
+    err := (if (accessType == StoreData) then AdES else AdEL);
     switch(vAddr[63..62]) {
       case 0b11 -> switch(vAddr[61..31], vAddr[30..29]) { (* xkseg *)
-        case (0b1111111111111111111111111111111, 0b11) -> (err, None)  (* kseg3 mapped 32-bit compat TODO *)
-        case (0b1111111111111111111111111111111, 0b10) -> (err, None)  (* sseg  mapped 32-bit compat TODO *)
-        case (0b1111111111111111111111111111111, 0b01) -> (None, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *)
-        case (0b1111111111111111111111111111111, 0b00) -> (None, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *)
-        case (_, _) -> (err, None)  (* xkseg mapped TODO *)
+        case (0b1111111111111111111111111111111, 0b11) -> exit (SignalException(err))  (* kseg3 mapped 32-bit compat TODO *)
+        case (0b1111111111111111111111111111111, 0b10) -> exit (SignalException(err))  (* sseg  mapped 32-bit compat TODO *)
+        case (0b1111111111111111111111111111111, 0b01) -> EXTZ(vAddr[28..0])         (* kseg1 unmapped uncached 32-bit compat *)
+        case (0b1111111111111111111111111111111, 0b00) -> EXTZ(vAddr[28..0])         (* kseg0 unmapped cached 32-bit compat *)
+        case (_, _) -> exit (SignalException(err))  (* xkseg mapped TODO *)
       }
-      case 0b10 -> (None, Some(EXTZ(vAddr[58..0]))) (* xkphys bits 61-59 are cache mode which we ignore *)
-      case 0b01 -> (err, None) (* xsseg - supervisor mapped TODO *)
-      case 0b00 -> (err, None) (* xuseg - user mapped TODO *)
+      case 0b10 -> EXTZ(vAddr[58..0]) (* xkphys bits 61-59 are cache mode which we ignore *)
+      case 0b01 -> exit (SignalException(err)) (* xsseg - supervisor mapped TODO *)
+      case 0b00 -> exit (SignalException(err)) (* xuseg - user mapped TODO *)
     }
   }
 
 function bit[64] TranslateOrExit((bit[64]) vAddr, (MemAccessType) accessType) =
-  switch (TLBTranslate(vAddr, accessType)) {
-    case ((Some(ex)), _)    -> (exit (SignalExceptionBadAddr (ex, vAddr)))
-    case (_, (Some(pAddr))) -> pAddr
-  }
+  TLBTranslate(vAddr, accessType)
 
 typedef regno = bit[5]                      (* a register number *)
 typedef imm16 = bit[16]                     (* 16-bit immediate *)
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
index 110b551d..8fe1b4d4 100644
--- a/mips/mips_wrappers.sail
+++ b/mips/mips_wrappers.sail
@@ -5,7 +5,7 @@ function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
 function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
     addr
 
-function (option<Exception>, option<bit[64]>) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = 
+function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = 
     TLBTranslate(vAddr, accessType)
 
 function unit SignalException ((Exception) ex) = SignalExceptionMIPS(ex)