Add DDC translation to riscv memory instructions. Not an ideal factorisation because the DDC translation has to take place before alignment check and therefore can't happen in translateAddr. To be considered. Also fix a bug where registers where reversed in CapRegs vector and so DDC was getting cleared during initialisation!

5 files changed, 246 insertions, 173 deletions

diff --git a/model/cheri_insts.sail b/model/cheri_insts.sail
index 17a5284..daf4e75 100644
--- a/model/cheri_insts.sail
+++ b/model/cheri_insts.sail
@@ -32,9 +32,9 @@
 /*  SUCH DAMAGE.                                                          */
 /*========================================================================*/
 
-val raise_c2_exception6 : (CapEx, bits(6)) -> bool effect {escape, rreg, wreg}
 function raise_c2_exception6(capEx, regnum) =
   {
+    print("CHERI " ^ string_of_capex(capEx) ^ " Reg=" ^ BitStr(regnum));
     let cause : cheri_cause = struct {
         cap_idx = regnum,
         capEx   = capEx
diff --git a/model/cheri_prelude_128.sail b/model/cheri_prelude_128.sail
index 1030245..563bb15 100644
--- a/model/cheri_prelude_128.sail
+++ b/model/cheri_prelude_128.sail
@@ -473,3 +473,4 @@ function capToString (cap) = {
 
 val checkCP2usable : unit -> unit
 function checkCP2usable () = ()
+
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 3b74ac6..b2aca21 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -42,30 +42,36 @@ 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 {
-               WORD   => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false),
-               DOUBLE => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false),
-               _      => internal_error("LOADRES expected WORD or DOUBLE")
+    let ddc_result = translateDDC(vaddr, Write, width);
+    match ddc_result {
+      DDC_Failure(ex) => raise_c2_exception6(ex, 0b100001),
+      DDC_Address(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 {
+                   WORD   => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false),
+                   DOUBLE => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false),
+                   _      => internal_error("LOADRES expected WORD or DOUBLE")
+                 }
              }
-         }
+      }
+    }
   } else {
     handle_illegal();
     false
@@ -94,44 +100,50 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
        * 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); 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 {
-                WORD   => mem_write_ea(addr, 4, aq, rl, true),
-                DOUBLE => 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 {
-                    WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
-                    DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, true),
+      let ddc_result = translateDDC(vaddr, Write, width);
+      match ddc_result {
+        DDC_Failure(ex) => raise_c2_exception6(ex, 0b100001),
+        DDC_Address(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); 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 {
+                    WORD   => mem_write_ea(addr, 4, aq, rl, true),
+                    DOUBLE => 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 {
+                        WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
+                        DOUBLE => 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 }
+                      }
+                    }
                   }
                 }
               }
@@ -172,50 +184,56 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd)
 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 {
-          WORD   => mem_write_ea(addr, 4, aq & rl, rl, true),
-          DOUBLE => mem_write_ea(addr, 8, aq & rl, rl, true),
-          _      => internal_error ("AMO expected WORD or DOUBLE")
-        };
-        match (eares) {
-          MemException(e) => { handle_mem_exception(addr, e); false },
-          MemValue(_) => {
-            let rval : MemoryOpResult(xlenbits) = match width {
-              WORD   => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)),
-              DOUBLE => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)),
+    let ddc_result = translateDDC(vaddr, Write, width);
+    match ddc_result {
+      DDC_Failure(ex) => raise_c2_exception6(ex, 0b100001),
+      DDC_Address(vaddr) => {
+        match translateAddr(vaddr, ReadWrite, Data) {
+          TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
+          TR_Address(addr) => {
+            let eares : MemoryOpResult(unit) = match width {
+              WORD   => mem_write_ea(addr, 4, aq & rl, rl, true),
+              DOUBLE => 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) => {
-                rs2_val : xlenbits = X(rs2);
-                result  : xlenbits =
-                  match op {
-                    AMOSWAP => rs2_val,
-                    AMOADD  => rs2_val + loaded,
-                    AMOXOR  => rs2_val ^ loaded,
-                    AMOAND  => rs2_val & loaded,
-                    AMOOR   => rs2_val | loaded,
-
-                    /* Have to convert number to vector here. Check this */
-                    AMOMIN  => vector64(min(signed(rs2_val),   signed(loaded))),
-                    AMOMAX  => vector64(max(signed(rs2_val),   signed(loaded))),
-                    AMOMINU => vector64(min(unsigned(rs2_val), unsigned(loaded))),
-                    AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded)))
-                  };
-
-                let wval : MemoryOpResult(bool) = match width {
-                  WORD   => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
-                  DOUBLE => mem_write_value(addr, 8, result,        aq & rl, rl, true),
-                  _      => internal_error("AMO expected WORD or DOUBLE")
+            match (eares) {
+              MemException(e) => { handle_mem_exception(addr, e); false },
+              MemValue(_) => {
+                let rval : MemoryOpResult(xlenbits) = match width {
+                  WORD   => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)),
+                  DOUBLE => 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) => {
+                    rs2_val : xlenbits = X(rs2);
+                    result  : xlenbits =
+                      match op {
+                        AMOSWAP => rs2_val,
+                        AMOADD  => rs2_val + loaded,
+                        AMOXOR  => rs2_val ^ loaded,
+                        AMOAND  => rs2_val & loaded,
+                        AMOOR   => rs2_val | loaded,
+       
+                        /* Have to convert number to vector here. Check this */
+                        AMOMIN  => vector64(min(signed(rs2_val),   signed(loaded))),
+                        AMOMAX  => vector64(max(signed(rs2_val),   signed(loaded))),
+                        AMOMINU => vector64(min(unsigned(rs2_val), unsigned(loaded))),
+                        AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded)))
+                      };
+       
+                    let wval : MemoryOpResult(bool) = match width {
+                      WORD   => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
+                      DOUBLE => 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 }
+                    }
+                  }
                 }
               }
             }
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 0ebd9a2..7750268 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -283,23 +283,29 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
        }
 
 function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
-  let vaddr : xlenbits = X(rs1) + EXTS(imm);
-  if   check_misaligned(vaddr, width)
-  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 {
-        BYTE   =>
-	  process_load(rd, vaddr, mem_read(addr, 1, aq, rl, false), is_unsigned),
-        HALF   =>
-	  process_load(rd, vaddr, mem_read(addr, 2, aq, rl, false), is_unsigned),
-        WORD   =>
-	  process_load(rd, vaddr, mem_read(addr, 4, aq, rl, false), is_unsigned),
-        DOUBLE =>
-	  process_load(rd, vaddr, mem_read(addr, 8, aq, rl, false), is_unsigned)
+  vaddr1 : xlenbits = X(rs1) + EXTS(imm);
+  let ddc_result = translateDDC(vaddr1, Read, width);
+  match ddc_result {
+    DDC_Failure(ex) => raise_c2_exception6(ex, 0b100001),
+    DDC_Address(vaddr) =>
+      if check_misaligned(vaddr, width)
+      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 {
+            BYTE   =>
+              process_load(rd, vaddr, mem_read(addr, 1, aq, rl, false), is_unsigned),
+            HALF   =>
+              process_load(rd, vaddr, mem_read(addr, 2, aq, rl, false), is_unsigned),
+            WORD   =>
+              process_load(rd, vaddr, mem_read(addr, 4, aq, rl, false), is_unsigned),
+            DOUBLE =>
+              process_load(rd, vaddr, mem_read(addr, 8, aq, rl, false), is_unsigned)
       }
   }
+  }
+  
 }
 
 val maybe_aq : bool <-> string
@@ -333,36 +339,41 @@ 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 vaddr : xlenbits = X(rs1) + EXTS(imm);
-  if   check_misaligned(vaddr, width)
-  then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false }
-  else match translateAddr(vaddr, Write, Data) {
-    TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
-    TR_Address(addr) => {
-      let eares : MemoryOpResult(unit) = match width {
-        BYTE   => mem_write_ea(addr, 1, aq, rl, false),
-        HALF   => mem_write_ea(addr, 2, aq, rl, false),
-        WORD   => mem_write_ea(addr, 4, aq, rl, false),
-        DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
-      };
-      match (eares) {
-        MemException(e) => { handle_mem_exception(addr, e); false },
-        MemValue(_) => {
-          let rs2_val = X(rs2);
-          let res : MemoryOpResult(bool) = match width {
-            BYTE   => mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false),
-            HALF   => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false),
-            WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false),
-            DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, false)
+  let vaddr1 : xlenbits = X(rs1) + EXTS(imm);
+  let ddc_result = translateDDC(vaddr1, Write, width);
+  match ddc_result {
+    DDC_Failure(ex) => raise_c2_exception6(ex, 0b100001),
+    DDC_Address(vaddr) =>
+      if   check_misaligned(vaddr, width)
+      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false }
+      else match translateAddr(vaddr, Write, Data) {
+        TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
+        TR_Address(addr) => {
+          let eares : MemoryOpResult(unit) = match width {
+            BYTE   => mem_write_ea(addr, 1, aq, rl, false),
+            HALF   => mem_write_ea(addr, 2, aq, rl, false),
+            WORD   => mem_write_ea(addr, 4, aq, rl, false),
+            DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
           };
-          match (res) {
-            MemValue(true)     => true,
-            MemValue(false)    => internal_error("store got false from mem_write_value"),
-            MemException(e) => { handle_mem_exception(addr, e); false }
+          match (eares) {
+            MemException(e) => { handle_mem_exception(addr, e); false },
+            MemValue(_) => {
+              let rs2_val = X(rs2);
+              let res : MemoryOpResult(bool) = match width {
+                BYTE   => mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false),
+                HALF   => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false),
+                WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false),
+                DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, false)
+              };
+              match (res) {
+                MemValue(true)     => true,
+                MemValue(false)    => internal_error("store got false from mem_write_value"),
+                MemException(e) => { handle_mem_exception(addr, e); false }
+              }
+            }
           }
         }
       }
-    }
   }
 }
 
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index 907b07c..3fb467f 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -91,38 +91,38 @@ register x30 : Capability
 register x31 : Capability
 
 let CapRegs : vector(32, dec, register(Capability)) = [
-  ref DDC,
-  ref x1 ,
-  ref x2 ,
-  ref x3 ,
-  ref x4 ,
-  ref x5 ,
-  ref x6 ,
-  ref x7 ,
-  ref x8 ,
-  ref x9 ,
-  ref x10,
-  ref x11,
-  ref x12,
-  ref x13,
-  ref x14,
-  ref x15,
-  ref x16,
-  ref x17,
-  ref x18,
-  ref x19,
-  ref x20,
-  ref x21,
-  ref x22,
-  ref x23,
-  ref x24,
-  ref x25,
-  ref x26,
-  ref x27,
-  ref x28,
-  ref x29,
+  ref x31,
   ref x30,
-  ref x31
+  ref x29,
+  ref x28,
+  ref x27,
+  ref x26,
+  ref x25,
+  ref x24,
+  ref x23,
+  ref x22,
+  ref x21,
+  ref x20,
+  ref x19,
+  ref x18,
+  ref x17,
+  ref x16,
+  ref x15,
+  ref x14,
+  ref x13,
+  ref x12,
+  ref x11,
+  ref x10,
+  ref x9 ,
+  ref x8 ,
+  ref x7 ,
+  ref x6 ,
+  ref x5 ,
+  ref x4 ,
+  ref x3 ,
+  ref x2 ,
+  ref x1 ,
+  ref DDC
 ]
 
 /*!
@@ -596,3 +596,46 @@ mapping size_mnemonic : word_width <-> string = {
   WORD   <-> "w",
   DOUBLE <-> "d"
 }
+
+union DDC_Result = {
+  DDC_Address : xlenbits,
+  DDC_Failure : CapEx
+}
+
+val translateDDC : (xlenbits, AccessType, word_width) -> DDC_Result effect {rreg, escape}
+function translateDDC (addr, at, width) = {
+  let ddc = DDC;
+  let have_rqd_load_perm : bool = match at {
+    Read       => ddc.permit_load,
+    Write      => true,
+    ReadWrite  => ddc.permit_load,
+    Execute    => false /* DDC should only be for load/store */
+  };
+  let have_rqd_store_perm : bool = match at {
+    Read       => true,
+    Write      => ddc.permit_store,
+    ReadWrite  => ddc.permit_store,
+    Execute    => false /* DDC should only be for load/store */
+  };
+  let newAddr = (getCapCursor(ddc) + unsigned(addr)) % pow2(xlen);
+  let size  = word_width_bytes(width);
+  let (base, top) = getCapBounds(ddc);
+
+  if not(ddc.tag) then
+    DDC_Failure(CapEx_TagViolation)
+  else if ddc.sealed then
+    DDC_Failure(CapEx_SealViolation)
+  else if not(have_rqd_load_perm) then
+    DDC_Failure(CapEx_PermitLoadViolation)
+  else if not(have_rqd_store_perm) then
+    DDC_Failure(CapEx_PermitStoreViolation)
+  else if (newAddr + size) > top then
+    DDC_Failure(CapEx_LengthViolation)
+  else if newAddr < base then
+    DDC_Failure(CapEx_LengthViolation)
+  else
+    DDC_Address(to_bits(64, newAddr))
+}
+
+val raise_c2_exception6 : (CapEx, bits(6)) -> bool effect {escape, rreg, wreg}
+