Add extended model from cheri-merge.

1 files changed, 123 insertions, 105 deletions

diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 7042583..f38b28f 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -41,31 +41,37 @@ function process_loadres(rd, addr, value, is_unsigned) =
 
 function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
   if haveAtomics() then {
-    let vaddr : xlenbits = X(rs1);
-    let aligned : bool =
-       /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt
-        * to treat them as valid here; otherwise we'd need to throw an internal_error.
-        */
-       match width {
-         BYTE   => true,
-         HALF   => vaddr[0]    == 0b0,
-         WORD   => vaddr[1..0] == 0b00,
-         DOUBLE => vaddr[2..0] == 0b000
-       };
-    /* "LR faults like a normal load, even though it's in the AMO major opcode space."
-     * - Andrew Waterman, isa-dev, 10 Jul 2018.
-     */
-    if (~ (aligned))
-    then { handle_mem_exception(vaddr, E_Load_Addr_Align); false }
-    else match translateAddr(vaddr, Read, Data) {
-           TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
-           TR_Address(addr) =>
-             match (width, sizeof(xlen)) {
-               (WORD, _)    => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false),
-               (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false),
-               _            => internal_error("LOADRES expected WORD or DOUBLE")
+    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) {
+      Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
+      Ext_DataAddr_OK(vaddr) => {
+        let aligned : bool =
+           /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt
+            * to treat them as valid here; otherwise we'd need to throw an internal_error.
+            */
+           match width {
+             BYTE   => true,
+             HALF   => vaddr[0]    == 0b0,
+             WORD   => vaddr[1..0] == 0b00,
+             DOUBLE => vaddr[2..0] == 0b000
+           };
+        /* "LR faults like a normal load, even though it's in the AMO major opcode space."
+         * - Andrew Waterman, isa-dev, 10 Jul 2018.
+         */
+        if (~ (aligned))
+        then { handle_mem_exception(vaddr, E_Load_Addr_Align); false }
+        else match translateAddr(vaddr, Read, Data) {
+               TR_Failure(e)    => { handle_mem_exception(vaddr, e); false },
+               TR_Address(addr) =>
+                 match (width, sizeof(xlen)) {
+                   (WORD, _)    => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false),
+                   (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false),
+                   _            => internal_error("LOADRES expected WORD or DOUBLE")
+                 }
              }
-         }
+      }
+    }
   } else {
     handle_illegal();
     false
@@ -93,45 +99,51 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
       /* normal non-rmem case
        * rmem: SC is allowed to succeed (but might fail later)
        */
-      vaddr : xlenbits = X(rs1);
-      let aligned : bool =
-        /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt
-         * to treat them as valid here; otherwise we'd need to throw an internal_error.
-         */
-        match width {
-          BYTE   => true,
-          HALF   => vaddr[0]    == 0b0,
-          WORD   => vaddr[1..0] == 0b00,
-          DOUBLE => vaddr[2..0] == 0b000
-        };
-      if (~ (aligned))
-      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false }
-      else {
-        if match_reservation(vaddr) == false then {
-          /* cannot happen in rmem */
-          X(rd) = EXTZ(0b1); cancel_reservation(); true
-        } else {
-          match translateAddr(vaddr, Write, Data) {
-            TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
-            TR_Address(addr) => {
-              let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
-                (WORD, _)    => mem_write_ea(addr, 4, aq, rl, true),
-                (DOUBLE, 64) => mem_write_ea(addr, 8, aq, rl, true),
-                _            => internal_error("STORECON expected word or double")
-              };
-              match (eares) {
-                MemException(e) => { handle_mem_exception(addr, e); false },
-                MemValue(_) => {
-                  rs2_val = X(rs2);
-                  let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
-                    (WORD, _)    => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
-                    (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val,        aq, rl, true),
+      pre_vaddr : xlenbits = X(rs1);
+      /* Let extensions get the first check on address validity. */
+      match ext_data_check_addr(pre_vaddr, Read, Data, width) {
+        Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
+        Ext_DataAddr_OK(vaddr) => {
+          let aligned : bool =
+            /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt
+             * to treat them as valid here; otherwise we'd need to throw an internal_error.
+             */
+            match width {
+              BYTE   => true,
+              HALF   => vaddr[0]    == 0b0,
+              WORD   => vaddr[1..0] == 0b00,
+              DOUBLE => vaddr[2..0] == 0b000
+            };
+          if (~ (aligned))
+          then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false }
+          else {
+            if match_reservation(vaddr) == false then {
+              /* cannot happen in rmem */
+              X(rd) = EXTZ(0b1); cancel_reservation(); true
+            } else {
+              match translateAddr(vaddr, Write, Data) {
+                TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
+                TR_Address(addr) => {
+                  let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
+                    (WORD, _)    => mem_write_ea(addr, 4, aq, rl, true),
+                    (DOUBLE, 64) => mem_write_ea(addr, 8, aq, rl, true),
                     _            => internal_error("STORECON expected word or double")
                   };
-                  match (res) {
-                    MemValue(true)  => { X(rd) = EXTZ(0b0); cancel_reservation(); true },
-                    MemValue(false) => { X(rd) = EXTZ(0b1); cancel_reservation(); true },
-                    MemException(e) => { handle_mem_exception(addr, e); false }
+                  match (eares) {
+                    MemException(e) => { handle_mem_exception(addr, e); false },
+                    MemValue(_) => {
+                      rs2_val = X(rs2);
+                      let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
+                        (WORD, _)    => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
+                        (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val,        aq, rl, true),
+                        _            => internal_error("STORECON expected word or double")
+                      };
+                      match (res) {
+                        MemValue(true)  => { X(rd) = EXTZ(0b0); cancel_reservation(); true },
+                        MemValue(false) => { X(rd) = EXTZ(0b1); cancel_reservation(); true },
+                        MemException(e) => { handle_mem_exception(addr, e); false }
+                      }
+                    }
                   }
                 }
               }
@@ -171,53 +183,59 @@ 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 {
-    vaddr : xlenbits = X(rs1);
-    match translateAddr(vaddr, ReadWrite, Data) {
-      TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
-      TR_Address(addr) => {
-        let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
-          (WORD, _)    => mem_write_ea(addr, 4, aq & rl, rl, true),
-          (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true),
-          _            => internal_error ("AMO expected WORD or DOUBLE")
-        };
-        rs2_val : xlenbits = X(rs2);
-        match (eares) {
-          MemException(e) => { handle_mem_exception(addr, e); false },
-          MemValue(_) => {
-            let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
-              (WORD, _)    => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)),
-              (DOUBLE, 64) => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)),
+    pre_vaddr : xlenbits = X(rs1);
+    /* Let extensions get the first check on address validity. */
+    match ext_data_check_addr(pre_vaddr, Read, Data, width) {
+      Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); false },
+      Ext_DataAddr_OK(vaddr) => {
+        match translateAddr(vaddr, ReadWrite, Data) {
+          TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
+          TR_Address(addr) => {
+            let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
+              (WORD, _)    => mem_write_ea(addr, 4, aq & rl, rl, true),
+              (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true),
               _            => internal_error ("AMO expected WORD or DOUBLE")
             };
-            match (rval) {
-              MemException(e)  => { handle_mem_exception(addr, e); false },
-              MemValue(loaded) => {
-                result  : xlenbits =
-                  match op {
-                    AMOSWAP => rs2_val,
-                    AMOADD  => rs2_val + loaded,
-                    AMOXOR  => rs2_val ^ loaded,
-                    AMOAND  => rs2_val & loaded,
-                    AMOOR   => rs2_val | loaded,
-
-                    /* These operations convert bitvectors to integer values using [un]signed,
-                     * and back using to_bits().
-                     */
-                    AMOMIN  => to_bits(sizeof(xlen), min(signed(rs2_val),   signed(loaded))),
-                    AMOMAX  => to_bits(sizeof(xlen), max(signed(rs2_val),   signed(loaded))),
-                    AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))),
-                    AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded)))
-                  };
-
-                let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
-                  (WORD, _)    => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
-                  (DOUBLE, 64) => mem_write_value(addr, 8, result,        aq & rl, rl, true),
-                  _            => internal_error("AMO expected WORD or DOUBLE")
+            rs2_val : xlenbits = X(rs2);
+            match (eares) {
+              MemException(e) => { handle_mem_exception(addr, e); false },
+              MemValue(_) => {
+                let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
+                  (WORD, _)    => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)),
+                  (DOUBLE, 64) => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)),
+                  _            => internal_error ("AMO expected WORD or DOUBLE")
                 };
-                match (wval) {
-                  MemValue(true)  => { X(rd) = loaded; true },
-                  MemValue(false) => { internal_error("AMO got false from mem_write_value") },
-                  MemException(e) => { handle_mem_exception(addr, e); false }
+                match (rval) {
+                  MemException(e)  => { handle_mem_exception(addr, e); false },
+                  MemValue(loaded) => {
+                    result  : xlenbits =
+                      match op {
+                        AMOSWAP => rs2_val,
+                        AMOADD  => rs2_val + loaded,
+                        AMOXOR  => rs2_val ^ loaded,
+                        AMOAND  => rs2_val & loaded,
+                        AMOOR   => rs2_val | loaded,
+
+                        /* These operations convert bitvectors to integer values using [un]signed,
+                         * and back using to_bits().
+                         */
+                        AMOMIN  => to_bits(sizeof(xlen), min(signed(rs2_val),   signed(loaded))),
+                        AMOMAX  => to_bits(sizeof(xlen), max(signed(rs2_val),   signed(loaded))),
+                        AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))),
+                        AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded)))
+                      };
+
+                    let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
+                      (WORD, _)    => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
+                      (DOUBLE, 64) => mem_write_value(addr, 8, result,        aq & rl, rl, true),
+                      _            => internal_error("AMO expected WORD or DOUBLE")
+                    };
+                    match (wval) {
+                      MemValue(true)  => { X(rd) = loaded; true },
+                      MemValue(false) => { internal_error("AMO got false from mem_write_value") },
+                      MemException(e) => { handle_mem_exception(addr, e); false }
+                    }
+                  }
                 }
               }
             }