Merge pull request #5 from rems-project/rmn30

Add base address register as extra argument to ext_data_check_addr hook

3 files changed, 27 insertions, 17 deletions

diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail
index c485577..2471075 100644
--- a/model/riscv_addr_checks.sail
+++ b/model/riscv_addr_checks.sail
@@ -39,11 +39,16 @@ function ext_control_check_pc(pc : xlenbits) -> Ext_ControlAddr_Check(ext_contro
 function ext_handle_control_check_error(err : ext_control_addr_error) -> unit =
   ()
 
-/* default data address checks */
+
+/* The default data address function does not perform any checks so
+   just uses unit for error type. */
 type ext_data_addr_error = unit
 
-function ext_data_check_addr(addr : xlenbits, acc : AccessType, rt : ReadType, width : word_width)
+/* Default data addr is just base register + immediate offset (may be zero).
+   Extensions might override and add additional checks. */
+function ext_data_get_addr(base : regbits, offset : xlenbits, acc : AccessType, rt : ReadType, width : word_width)
          -> Ext_DataAddr_Check(ext_data_addr_error) =
+  let addr = X(base) + offset in
   Ext_DataAddr_OK(addr)
 
 function ext_handle_data_check_error(err : ext_data_addr_error) -> unit =
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index f38b28f..86a8b32 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -41,9 +41,10 @@ function process_loadres(rd, addr, value, is_unsigned) =
 
 function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
   if haveAtomics() then {
-    let pre_vaddr : xlenbits = X(rs1);
-    /* Let extensions get the first check on address validity. */
-    match ext_data_check_addr(pre_vaddr, Read, Data, width) {
+    /* Get the address, X(rs1) (no offset).
+     * Extensions might perform additional checks on address validity.
+     */
+    match ext_data_get_addr(rs1, zeros(), Read, Data, width) {
       Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
       Ext_DataAddr_OK(vaddr) => {
         let aligned : bool =
@@ -99,9 +100,10 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
       /* normal non-rmem case
        * rmem: SC is allowed to succeed (but might fail later)
        */
-      pre_vaddr : xlenbits = X(rs1);
-      /* Let extensions get the first check on address validity. */
-      match ext_data_check_addr(pre_vaddr, Read, Data, width) {
+      /* Get the address, X(rs1) (no offset).
+       * Extensions might perform additional checks on address validity.
+       */
+      match ext_data_get_addr(rs1, zeros(), Read, Data, width) {
         Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
         Ext_DataAddr_OK(vaddr) => {
           let aligned : bool =
@@ -183,9 +185,10 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd)
    This may need revisiting. */
 function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
   if haveAtomics() then {
-    pre_vaddr : xlenbits = X(rs1);
-    /* Let extensions get the first check on address validity. */
-    match ext_data_check_addr(pre_vaddr, Read, Data, width) {
+    /* Get the address, X(rs1) (no offset).
+     * Some extensions perform additional checks on address validity.
+     */
+    match ext_data_get_addr(rs1, zeros(), Read, Data, width) {
       Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
       Ext_DataAddr_OK(vaddr) => {
         match translateAddr(vaddr, ReadWrite, Data) {
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 0cfc0ec..5819a81 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -315,9 +315,10 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
        }
 
 function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
-  let pre_vaddr : xlenbits = X(rs1) + EXTS(imm);
-  /* Let extensions get the first check on address validity. */
-  match ext_data_check_addr(pre_vaddr, Read, Data, width) {
+  let offset : xlenbits = EXTS(imm);
+  /* Get the address, X(rs1) + offset.
+     Some extensions perform additional checks on address validity. */
+  match ext_data_get_addr(rs1, offset, Read, Data, width) {
     Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
     Ext_DataAddr_OK(vaddr) =>
       if   check_misaligned(vaddr, width)
@@ -370,9 +371,10 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */
 function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
-  let pre_vaddr : xlenbits = X(rs1) + EXTS(imm);
-  /* Let extensions get the first check on address validity. */
-  match ext_data_check_addr(pre_vaddr, Write, Data, width) {
+  let offset : xlenbits = EXTS(imm);
+  /* Get the address, X(rs1) + offset.
+     Some extensions perform additional checks on address validity. */
+  match ext_data_get_addr(rs1, offset, Write, Data, width) {
     Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
     Ext_DataAddr_OK(vaddr) =>
       if   check_misaligned(vaddr, width)