Refactor the ext_fetch_check_pc API. (#1226)

This makes it return just an option instead of also a possibly modified
target address.

The more general API was designed for an earlier CHERI model, but now
the generality is not used.

Addresses #1205.

Author: pmundkur

model/riscv_addr_checks.sail

@@ -14,11 +14,10 @@ type ext_fetch_addr_error = unit
  * start_pc: the PC at the start of the current fetch sequence
  * pc:       the PC for the current granule
  *
- * returns:  the *virtual* memory address to use for the fetch.
- *           any address translation errors are reported for pc, not the returned value.
+ * returns:  an optional fetch error.
  */
-function ext_fetch_check_pc(start_pc : xlenbits, pc : xlenbits) -> Ext_FetchAddr_Check(ext_fetch_addr_error) =
-  Ext_FetchAddr_OK(Virtaddr(pc))
+function ext_fetch_check_pc(start_pc : xlenbits, pc : xlenbits) -> option(ext_fetch_addr_error) =
+  None()
 
 function ext_handle_fetch_check_error(err : ext_fetch_addr_error) -> unit =
   ()

model/riscv_addr_checks_common.sail

@@ -14,11 +14,6 @@
  * extensions would need to define their own functions to override them.
  */
 
-union Ext_FetchAddr_Check ('a : Type) = {
-  Ext_FetchAddr_OK  : virtaddr,  /* PC value to use for the actual fetch */
-  Ext_FetchAddr_Error : 'a
-}
-
 union Ext_ControlAddr_Check ('a : Type) = {
   Ext_ControlAddr_OK : virtaddr, /* PC value to use for the target of the control operation */
   Ext_ControlAddr_Error : 'a

model/riscv_fetch.sail

@@ -17,47 +17,47 @@ function fetch() -> FetchResult = {
    * but any exceptions use the untransformed PC.
    */
   // TODO: Add a parameter to try_step() to allow forcing the fetch result and use that instead.
+
   if get_config_rvfi()
   then return rvfi_fetch();
+
   match ext_fetch_check_pc(PC, PC) {
-    Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
-    Ext_FetchAddr_OK(use_pc) => {
-      let use_pc_bits = bits_of(use_pc);
-      if   (use_pc_bits[0] != bitzero | (use_pc_bits[1] != bitzero & not(currentlyEnabled(Ext_Zca))))
-      then F_Error(E_Fetch_Addr_Align(), PC)
-      else match translateAddr(use_pc, InstructionFetch()) {
-        Err(e, _)    => F_Error(e, PC),
-        Ok(ppclo, _) => {
-          /* split instruction fetch into 16-bit granules to handle RVC, as
-           * well as to generate precise fault addresses in any fetch
-           * exceptions.
-           */
-          match mem_read(InstructionFetch(), ppclo, 2, false, false, false) {
-            Err(e)  => F_Error(e, PC),
-            Ok(ilo) => {
-              if   isRVC(ilo)
-              then F_RVC(ilo)
-              else {
-                /* fetch PC check for the next instruction granule */
-                let PC_hi = PC + 2;
-                match ext_fetch_check_pc(PC, PC_hi) {
-                  Ext_FetchAddr_Error(e)      => F_Ext_Error(e),
-                  Ext_FetchAddr_OK(use_pc_hi) => {
-                    match translateAddr(use_pc_hi, InstructionFetch()) {
-                      Err(e, _)    => F_Error(e, PC_hi),
-                      Ok(ppchi, _) => {
-                        match mem_read(InstructionFetch(), ppchi, 2, false, false, false) {
-                          Err(e)  => F_Error(e, PC_hi),
-                          Ok(ihi) => F_Base(append(ihi, ilo))
-                        }
-                      }
-                    }
-                  }
+    Some(e) => return F_Ext_Error(e),
+    None()  => (),
+  };
+
+  if   (PC[0] != bitzero | (PC[1] != bitzero & not(currentlyEnabled(Ext_Zca))))
+  then return F_Error(E_Fetch_Addr_Align(), PC);
+
+  match translateAddr(Virtaddr(PC), InstructionFetch()) {
+    Err(e, _)    => F_Error(e, PC),
+    Ok(ppclo, _) => {
+      /* split instruction fetch into 16-bit granules to handle RVC, as
+       * well as to generate precise fault addresses in any fetch
+       * exceptions.
+       */
+      match mem_read(InstructionFetch(), ppclo, 2, false, false, false) {
+        Err(e)  => F_Error(e, PC),
+        Ok(ilo) =>
+          if   isRVC(ilo)
+          then F_RVC(ilo)
+          else {
+            /* fetch PC check for the next instruction granule */
+            let PC_hi = PC + 2;
+            match ext_fetch_check_pc(PC, PC_hi) {
+              Some(e) => return F_Ext_Error(e),
+              None()  => (),
+            };
+
+            match translateAddr(Virtaddr(PC_hi), InstructionFetch()) {
+              Err(e, _)    => F_Error(e, PC_hi),
+              Ok(ppchi, _) =>
+                match mem_read(InstructionFetch(), ppchi, 2, false, false, false) {
+                  Err(e)  => F_Error(e, PC_hi),
+                  Ok(ihi) => F_Base(append(ihi, ilo))
                 }
-              }
             }
           }
-        }
       }
     }
   }

model/riscv_fetch_rvfi.sail

@@ -14,33 +14,33 @@ function rvfi_fetch() -> FetchResult = {
 
   /* First allow extensions to check pc */
   match ext_fetch_check_pc(PC, PC) {
-    Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
-    Ext_FetchAddr_OK(use_pc) => {
-      /* then check PC alignment */
-      let use_pc_bits = bits_of(use_pc);
-      if   (use_pc_bits[0] != bitzero | (use_pc_bits[1] != bitzero & not(currentlyEnabled(Ext_Zca))))
-      then F_Error(E_Fetch_Addr_Align(), PC)
-      else match translateAddr(use_pc, InstructionFetch()) {
-        Err(e, _) => F_Error(e, PC),
-        Ok(_, _)  => {
-          let i = rvfi_instruction[rvfi_insn];
-          rvfi_inst_data[rvfi_insn]   = zero_extend(i);
-          if   (i[1 .. 0] != 0b11)
-          then F_RVC(i[15 .. 0])
-          else {
-            /* fetch PC check for the next instruction granule */
-            let PC_hi = PC + 2;
-            match ext_fetch_check_pc(PC, PC_hi) {
-              Ext_FetchAddr_Error(e)      => F_Ext_Error(e),
-              Ext_FetchAddr_OK(use_pc_hi) =>
-                match translateAddr(use_pc_hi, InstructionFetch()) {
-                  Err(e, _) => F_Error(e, PC),
-                  Ok(_, _)  => F_Base(i)
-              }
-            }
-          }
-        }
-      }
-    }
+    Some(e) => return F_Ext_Error(e),
+    None()  => (),
+  };
+
+  /* Then check PC alignment */
+  if   (PC[0] != bitzero | (PC[1] != bitzero & not(currentlyEnabled(Ext_Zca))))
+  then return F_Error(E_Fetch_Addr_Align(), PC);
+
+  match translateAddr(Virtaddr(PC), InstructionFetch()) {
+    Err(e, _) => return F_Error(e, PC),
+    Ok(_, _)  => (),
+  };
+
+  let i = rvfi_instruction[rvfi_insn];
+  rvfi_inst_data[rvfi_insn]   = zero_extend(i);
+  if   (i[1 .. 0] != 0b11)
+  then return F_RVC(i[15 .. 0]);
+
+  /* fetch PC check for the next instruction granule */
+  let PC_hi = PC + 2;
+  match ext_fetch_check_pc(PC, PC_hi) {
+    Some(e) => return F_Ext_Error(e),
+    None()  => (),
+  };
+
+  match translateAddr(Virtaddr(PC_hi), InstructionFetch()) {
+    Err(e, _) => F_Error(e, PC),
+    Ok(_, _)  => F_Base(i)
   }
 }