Refactor the control_check_pc API. (#1234)

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

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

Addresses #1205.

Author: pmundkur

model/riscv_addr_checks.sail

@@ -26,18 +26,16 @@ function ext_handle_fetch_check_error(err : ext_fetch_addr_error) -> unit =
 
 type ext_control_addr_error = unit
 
-/* these functions return the address to use as the target for
- * the control transfer.  any address translation or other errors
- * are reported for the original value, not the returned value.
+/* This function returns an optional exception for the address to use
+ * as the target for the control transfer. The control address is
+ * derived from the PC register, e.g. in JAL.
  *
  * NOTE: the input value does *not* have bit[0] set to 0, to enable
- * more accurate bounds checking.  There is no constraint on the output
- * value, which will have bit[0] cleared by the caller if needed.
+ * more accurate bounds checking.
  */
 
-/* the control address is derived from the PC register, e.g. in JAL */
-function ext_control_check_pc(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) =
-  Ext_ControlAddr_OK(Virtaddr(pc))
+function ext_control_check_pc(pc : xlenbits) -> option(ext_control_addr_error) =
+  None()
 
 function ext_handle_control_check_error(err : ext_control_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_ControlAddr_Check ('a : Type) = {
-  Ext_ControlAddr_OK : virtaddr, /* PC value to use for the target of the control operation */
-  Ext_ControlAddr_Error : 'a
-}
-
 union Ext_DataAddr_Check ('a : Type) = {
   Ext_DataAddr_OK : virtaddr,    /* Address to use for the data access */
   Ext_DataAddr_Error : 'a

model/riscv_insts_base.sail

@@ -48,23 +48,21 @@ mapping clause assembly = UTYPE(imm, rd, op)
 function jump_to(target : xlenbits) -> ExecutionResult = {
   // Extensions get the first checks on the prospective target address.
   match ext_control_check_pc(target) {
-    Ext_ControlAddr_Error(e) => Ext_ControlAddr_Check_Failure(e),
-    Ext_ControlAddr_OK(target) => {
-      // Perform standard alignment check.
-      let target_bits = bits_of(target);
-      // Check target is at least 2-byte aligned (callers must ensure
-      // this so it can be an assertion).
-      assert(target_bits[0] == bitzero);
-      // If it is not 4-byte aligned and compressed instructions are
-      // not enabled then raise an alignment exception.
-      if bit_to_bool(target_bits[1]) & not(currentlyEnabled(Ext_Zca)) then {
-        Memory_Exception(target, E_Fetch_Addr_Align())
-      } else {
-        set_next_pc(target_bits);
-        RETIRE_SUCCESS
-      }
-    }
-  }
+    Some(e) => return Ext_ControlAddr_Check_Failure(e),
+    None()  => (),
+  };
+
+  // Perform standard alignment check.
+  // Check target is at least 2-byte aligned (callers must ensure
+  // this so it can be an assertion).
+  assert(target[0] == bitzero);
+  // If it is not 4-byte aligned and compressed instructions are
+  // not enabled then raise an alignment exception.
+  if bit_to_bool(target[1]) & not(currentlyEnabled(Ext_Zca))
+  then return Memory_Exception(Virtaddr(target), E_Fetch_Addr_Align());
+
+  set_next_pc(target);
+  RETIRE_SUCCESS
 }
 
 /* ****************************************************************** */