A kinder, gentler splitting of ext_access_type's ReadWrite

This redoes https://github.com/rems-project/sail-riscv/pull/57 without
nearly as much excitement.  We sill want it for CHERI, so that we can
signal from the instruction to the PTW whether we are prepared to load a
capability (or will strip any tags that we load) and whether the store
will (or might) set a tag.

Thanks to Prashanth Mundkur for several improvements.

6 files changed, 37 insertions, 31 deletions

diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index e760b90..55727b8 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -189,10 +189,10 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
     /* Get the address, X(rs1) (no offset).
      * Some extensions perform additional checks on address validity.
      */
-    match ext_data_get_addr(rs1, zeros(), ReadWrite(Data), width) {
+    match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) {
       Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
       Ext_DataAddr_OK(vaddr) => {
-        match translateAddr(vaddr, ReadWrite(Data)) {
+        match translateAddr(vaddr, ReadWrite(Data, Data)) {
           TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
           TR_Address(addr, _) => {
             let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
@@ -214,8 +214,8 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
               MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
               MemValue(_) => {
                 let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
-                  (WORD, _)    => extend_value(is_unsigned, mem_read(ReadWrite(Data), addr, 4, aq, aq & rl, true)),
-                  (DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data), addr, 8, aq, aq & rl, true)),
+                  (WORD, _)    => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, aq & rl, true)),
+                  (DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, aq & rl, true)),
                   _            => internal_error("AMO expected WORD or DOUBLE")
                 };
                 match (mval) {
diff --git a/model/riscv_iris.sail b/model/riscv_iris.sail
index 80f3515..2b3bb46 100644
--- a/model/riscv_iris.sail
+++ b/model/riscv_iris.sail
@@ -303,7 +303,7 @@ enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL}
 union AccessType ('a : Type) = {
   Read      : 'a,
   Write     : 'a,
-  ReadWrite : 'a,
+  ReadWrite : ('a, 'a),
   Execute   : unit
 }
 
@@ -365,10 +365,10 @@ let default_write_acc : ext_access_type = Data
 val accessType_to_str : AccessType(ext_access_type) -> string
 function accessType_to_str (a) =
   match (a) {
-    Read(Data)      => "R",
-    Write(Data)     => "W",
-    ReadWrite(Data) => "RW",
-    Execute()       => "X"
+    Read(Data)            => "R",
+    Write(Data)           => "W",
+    ReadWrite(Data, Data) => "RW",
+    Execute()             => "X"
   }
 
 overload to_str = {accessType_to_str}
diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail
index d07018f..08cedc5 100644
--- a/model/riscv_pte.sail
+++ b/model/riscv_pte.sail
@@ -42,14 +42,14 @@ function to_pte_check(b : bool) -> PTE_Check =
  */
 function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte, ext_ptw : ext_ptw) -> PTE_Check = {
   match (ac, priv) {
-    (Read(Data),      User)       => to_pte_check(p.U() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
-    (Write(Data),     User)       => to_pte_check(p.U() == 0b1 & p.W() == 0b1),
-    (ReadWrite(Data), User)       => to_pte_check(p.U() == 0b1 & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
+    (Read(_),         User)       => to_pte_check(p.U() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
+    (Write(_),        User)       => to_pte_check(p.U() == 0b1 & p.W() == 0b1),
+    (ReadWrite(_, _), User)       => to_pte_check(p.U() == 0b1 & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
     (Execute(),       User)       => to_pte_check(p.U() == 0b1 & p.X() == 0b1),
 
-    (Read(Data),      Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
-    (Write(Data),     Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1),
-    (ReadWrite(Data), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
+    (Read(_),         Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
+    (Write(_),        Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1),
+    (ReadWrite(_, _), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
     (Execute(),       Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1),
 
     (_,               Machine)    => internal_error("m-mode mem perm check")
@@ -57,8 +57,14 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
 }
 
 function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : extPte) -> option((PTE_Bits, extPte)) = {
-  let update_d = (a == Write(Data) | a == ReadWrite(Data)) & p.D() == 0b0; // dirty-bit
-  let update_a = p.A() == 0b0;                                             // accessed-bit
+  let update_d = p.D() == 0b0 & (match a {                                       // dirty-bit
+                                  Execute() => false,
+                                  Read() => false,
+                                  Write(_) => true,
+                                  ReadWrite(_,_) => true
+                                });
+
+  let update_a = p.A() == 0b0;                                                   // accessed-bit
   if update_d | update_a then {
     let np = update_A(p, 0b1);
     let np = if update_d then update_D(np, 0b1) else np;
diff --git a/model/riscv_ptw.sail b/model/riscv_ptw.sail
index ed4db30..a46a755 100644
--- a/model/riscv_ptw.sail
+++ b/model/riscv_ptw.sail
@@ -35,15 +35,15 @@ function ext_get_ptw_error(ext_ptw : ext_ptw) -> PTW_Error =
 function translationException(a : AccessType(ext_access_type), f : PTW_Error) -> ExceptionType = {
   let e : ExceptionType =
   match (a, f) {
-    (_, PTW_Ext_Error(e))           => E_Extension(ext_translate_exception(e)),
-    (ReadWrite(Data), PTW_Access()) => E_SAMO_Access_Fault(),
-    (ReadWrite(Data), _)            => E_SAMO_Page_Fault(),
-    (Read(Data), PTW_Access())      => E_Load_Access_Fault(),
-    (Read(Data), _)                 => E_Load_Page_Fault(),
-    (Write(Data), PTW_Access())     => E_SAMO_Access_Fault(),
-    (Write(Data), _)                => E_SAMO_Page_Fault(),
-    (Execute(), PTW_Access())       => E_Fetch_Access_Fault(),
-    (Execute(), _)                  => E_Fetch_Page_Fault()
+    (_, PTW_Ext_Error(e))        => E_Extension(ext_translate_exception(e)),
+    (ReadWrite(_), PTW_Access()) => E_SAMO_Access_Fault(),
+    (ReadWrite(_), _)            => E_SAMO_Page_Fault(),
+    (Read(_), PTW_Access())      => E_Load_Access_Fault(),
+    (Read(_), _)                 => E_Load_Page_Fault(),
+    (Write(_), PTW_Access())     => E_SAMO_Access_Fault(),
+    (Write(_), _)                => E_SAMO_Page_Fault(),
+    (Execute(), PTW_Access())    => E_Fetch_Access_Fault(),
+    (Execute(), _)               => E_Fetch_Page_Fault()
   } in {
 /*  print_mem("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */
     e
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index 987743a..f8c9308 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -100,7 +100,7 @@ enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL}
 union AccessType ('a : Type) = {
   Read      : 'a,
   Write     : 'a,
-  ReadWrite : 'a,
+  ReadWrite : ('a, 'a),
   Execute   : unit
 }
 
diff --git a/model/riscv_vmem_types.sail b/model/riscv_vmem_types.sail
index bf5551d..e01ad0f 100644
--- a/model/riscv_vmem_types.sail
+++ b/model/riscv_vmem_types.sail
@@ -9,10 +9,10 @@ let default_write_acc : ext_access_type = Data
 val accessType_to_str : AccessType(ext_access_type) -> string
 function accessType_to_str (a) =
   match (a) {
-    Read(Data)      => "R",
-    Write(Data)     => "W",
-    ReadWrite(Data) => "RW",
-    Execute()       => "X"
+    Read(_)            => "R",
+    Write(_)           => "W",
+    ReadWrite(_, _)    => "RW",
+    Execute()          => "X"
   }
 
 overload to_str = {accessType_to_str}