Added pmm Support

c_emulator/riscv_platform.c

@@ -47,6 +47,11 @@ bool sys_enable_writable_fiom(unit u)
   return rv_enable_writable_fiom;
 }
 
+bool sys_enable_pmm(unit u)
+{
+  return rv_enable_pmm;
+}
+
 bool sys_enable_vext(unit u)
 {
   return rv_enable_vext;

c_emulator/riscv_platform.h

@@ -8,6 +8,7 @@ bool sys_enable_zcb(unit);
 bool sys_enable_zfinx(unit);
 bool sys_enable_writable_misa(unit);
 bool sys_enable_writable_fiom(unit);
+bool sys_enable_pmm(unit);
 bool sys_enable_vext(unit);
 
 uint64_t sys_pmp_count(unit);

c_emulator/riscv_platform_impl.c

@@ -18,6 +18,7 @@ bool rv_enable_dirty_update = false;
 bool rv_enable_misaligned = false;
 bool rv_mtval_has_illegal_inst_bits = false;
 bool rv_enable_writable_fiom = true;
+bool rv_enable_pmm = false;
 
 uint64_t rv_ram_base = UINT64_C(0x80000000);
 uint64_t rv_ram_size = UINT64_C(0x4000000);

c_emulator/riscv_platform_impl.h

@@ -22,6 +22,7 @@ extern bool rv_enable_dirty_update;
 extern bool rv_enable_misaligned;
 extern bool rv_mtval_has_illegal_inst_bits;
 extern bool rv_enable_writable_fiom;
+extern bool rv_enable_pmm;
 
 extern uint64_t rv_ram_base;
 extern uint64_t rv_ram_size;

c_emulator/riscv_sim.c

@@ -136,6 +136,7 @@ static struct option options[] = {
     {"report-arch",                 no_argument,       0, 'a'                     },
     {"test-signature",              required_argument, 0, 'T'                     },
     {"signature-granularity",       required_argument, 0, 'g'                     },
+    {"enable-pmm",                  no_argument,       0, 'Y'                     },
 #ifdef RVFI_DII
     {"rvfi-dii",                    required_argument, 0, 'r'                     },
 #endif
@@ -145,7 +146,7 @@ static struct option options[] = {
     {"trace-output",                required_argument, 0, OPT_TRACE_OUTPUT        },
     {"inst-limit",                  required_argument, 0, 'l'                     },
     {"enable-zfinx",                no_argument,       0, 'x'                     },
-    {"enable-writable-fiom",        no_argument,       0, OPT_ENABLE_WRITABLE_FIOM},
+    {"enable-writable-fiom",        no_argument,       0, OPT_ENABLE_WRITABLE_FIOM},    
     {"enable-zcb",                  no_argument,       0, OPT_ENABLE_ZCB          },
 #ifdef SAILCOV
     {"sailcov-file",                required_argument, 0, 'c'                     },
@@ -263,6 +264,7 @@ static int process_args(int argc, char **argv)
                     "T:"
                     "g:"
                     "h"
+                    "Y"                    
 #ifdef RVFI_DII
                     "r:"
 #endif
@@ -314,6 +316,10 @@ static int process_args(int argc, char **argv)
       fprintf(stderr, "enabling N extension.\n");
       rv_enable_next = true;
       break;
+    case 'Y':
+      fprintf(stderr, "enabling pointer masking support.\n");
+      rv_enable_pmm = true;
+      break;      
     case 'I':
       fprintf(stderr, "disabling writable misa CSR.\n");
       rv_enable_writable_misa = false;

handwritten_support/riscv_extras.lem

@@ -169,6 +169,10 @@ val sys_enable_writable_fiom : unit -> bool
 let sys_enable_writable_fiom () = true
 declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom`
 
+val sys_enable_pmm : unit -> bool
+let sys_enable_pmm () = false
+declare ocaml target_rep function sys_enable_pmm = `Platform.enable_pmm`
+
 val plat_ram_base : unit -> bitvector
 let plat_ram_base () = []
 declare ocaml target_rep function plat_ram_base = `Platform.dram_base`

handwritten_support/riscv_extras.v

@@ -201,6 +201,7 @@ Axiom sys_enable_fdext : unit -> bool.
 Axiom sys_enable_next : unit -> bool.
 Axiom sys_enable_zfinx : unit -> bool.
 Axiom sys_enable_writable_fiom : unit -> bool.
+Axiom sys_enable_pmm : unit -> bool.
 
 (* The constraint solver can do this itself, but a Coq bug puts
    anonymous_subproof into the term instead of an actual subproof. *)

handwritten_support/riscv_extras_sequential.lem

@@ -157,6 +157,10 @@ val sys_enable_writable_fiom : unit -> bool
 let sys_enable_writable_fiom () = true
 declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom`
 
+val sys_enable_pmm : unit -> bool
+let sys_enable_pmm () = false
+declare ocaml target_rep function sys_enable_pmm = `Platform.enable_pmm`
+
 val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_ram_base () = wordFromInteger 0
 declare ocaml target_rep function plat_ram_base = `Platform.dram_base`

model/riscv_csr_map.sail

@@ -161,6 +161,8 @@ mapping clause csr_name_map = 0xB00  <-> "mcycle"
 mapping clause csr_name_map = 0xB02  <-> "minstret"
 mapping clause csr_name_map = 0xB80  <-> "mcycleh"
 mapping clause csr_name_map = 0xB82  <-> "minstreth"
+/* machine security */
+mapping clause csr_name_map = 0x747  <-> "mseccfg"
 /* TODO: other hpm counters and events */
 /* trigger/debug */
 mapping clause csr_name_map = 0x7a0  <-> "tselect"

model/riscv_insts_aext.sail

@@ -61,36 +61,38 @@ function process_loadres(rd, addr, value, is_unsigned) =
   }
 
 function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
+  let pmm = is_pmm_active();
   if haveAtomics() then {
     /* 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); RETIRE_FAIL },
       Ext_DataAddr_OK(vaddr) => {
+        let  vaddr_ = transform_effective_address(vaddr, pmm);
         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..0] == 0b0,
-             WORD   => vaddr[1..0] == 0b00,
-             DOUBLE => vaddr[2..0] == 0b000
+             HALF   => vaddr_[0..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 not(aligned)
-        then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
-        else match translateAddr(vaddr, Read(Data)) {
-               TR_Failure(e, _)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+        then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); RETIRE_FAIL }
+        else match translateAddr(vaddr_, Read(Data)) {
+               TR_Failure(e, _)    => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
                TR_Address(addr, _) =>
                  match (width, sizeof(xlen)) {
-                   (BYTE, _)    => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 1, aq, aq & rl, true), false),
-                   (HALF, _)    => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false),
-                   (WORD, _)    => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 4, aq, aq & rl, true), false),
-                   (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 8, aq, aq & rl, true), false),
+                   (BYTE, _)    => process_loadres(rd, vaddr_, mem_read(Read(Data), addr, 1, aq, aq & rl, true), false),
+                   (HALF, _)    => process_loadres(rd, vaddr_, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false),
+                   (WORD, _)    => process_loadres(rd, vaddr_, mem_read(Read(Data), addr, 4, aq, aq & rl, true), false),
+                   (DOUBLE, 64) => process_loadres(rd, vaddr_, mem_read(Read(Data), addr, 8, aq, aq & rl, true), false),
                    _            => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
                  }
              }
@@ -113,6 +115,7 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if amo_width_valid(
 
 /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
 function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
+  let pmm = is_pmm_active();
   if speculate_conditional () == false then {
     /* should only happen in rmem
      * rmem: allow SC to fail very early
@@ -129,26 +132,27 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
       match ext_data_get_addr(rs1, zeros(), Write(Data), width) {
         Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
         Ext_DataAddr_OK(vaddr) => {
+          let  vaddr_ = transform_effective_address(vaddr, pmm);
           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..0] == 0b0,
-              WORD   => vaddr[1..0] == 0b00,
-              DOUBLE => vaddr[2..0] == 0b000
+              HALF   => vaddr_[0..0] == 0b0,
+              WORD   => vaddr_[1..0] == 0b00,
+              DOUBLE => vaddr_[2..0] == 0b000
             };
           if not(aligned)
-          then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
+          then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL }
           else {
-            if match_reservation(vaddr) == false then {
+            if match_reservation(vaddr_) == false then {
               /* cannot happen in rmem */
               X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
             } else {
-              match translateAddr(vaddr, Write(Data)) {  /* Write and ReadWrite are equivalent here:
+              match translateAddr(vaddr_, Write(Data)) {  /* Write and ReadWrite are equivalent here:
                                                           * both result in a SAMO exception */
-                TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+                TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
                 TR_Address(addr, _) => {
                   let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
                     (BYTE, _)    => mem_write_ea(addr, 1, aq & rl, rl, true),
@@ -158,7 +162,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
                     _            => internal_error(__FILE__, __LINE__, "STORECON expected word or double")
                   };
                   match (eares) {
-                    MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+                    MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
                     MemValue(_) => {
                       rs2_val = X(rs2);
                       let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
@@ -171,7 +175,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
                       match (res) {
                         MemValue(true)  => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
                         MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
-                        MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
+                        MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }
                       }
                     }
                   }
@@ -212,15 +216,17 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if amo_width_valid(s
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */
 function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
+  let pmm = is_pmm_active();
   if haveAtomics() then {
     /* Get the address, X(rs1) (no offset).
      * Some extensions perform additional checks on address validity.
      */
     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, Data)) {
-          TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+        let  vaddr_ = transform_effective_address(vaddr, pmm) in 
+        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)) {
               (BYTE, _)    => mem_write_ea(addr, 1, aq & rl, rl, true),
@@ -241,7 +247,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
               DOUBLE => X(rs2)
             };
             match (eares) {
-              MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+              MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
               MemValue(_) => {
                 let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
                   (BYTE, _)    => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 1, aq, aq & rl, true)),
@@ -251,7 +257,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                   _            => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
                 };
                 match (mval) {
-                  MemException(e)  => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+                  MemException(e)  => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
                   MemValue(loaded) => {
                     let result : xlenbits =
                       match op {
@@ -285,7 +291,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
                     match (wval) {
                       MemValue(true)  => { X(rd) = rval; RETIRE_SUCCESS },
                       MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") },
-                      MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
+                      MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }
                     }
                   }
                 }

model/riscv_insts_base.sail

@@ -321,28 +321,80 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
          WORD   => vaddr[0] == bitone | vaddr[1] == bitone,
          DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone
        }
+function transform_VA (effective_address : xlenbits,PMLEN :int) -> xlenbits = {
+  assert(PMLEN >= 0, "PMLEN out of range");
+  assert(PMLEN <= 63, "PMLEN out of range");
+  let XLEN = sizeof(xlen);
+  let i = XLEN -(PMLEN +1);
+  let effective_bit = effective_address[i..i];
+  let NVBITS = replicate_bits(effective_bit, PMLEN);
+  let VBITS = effective_address[i..0];
+  NVBITS @ VBITS
+}
+
+function transform_PA (effective_address : xlenbits,PMLEN :int) -> xlenbits = {
+  assert(PMLEN >= 0, "PMLEN out of range");
+  assert(PMLEN <= 63, "PMLEN out of range");
+  let XLEN = sizeof(xlen);
+  let i = XLEN -(PMLEN + 1);
+  let NVBITS = replicate_bits(0b0, PMLEN);
+  let VBITS = effective_address[i..0];
+  NVBITS @ VBITS
+}
+
+function transform_effective_address(vaddr : xlenbits, pmm : bool) -> xlenbits = {
+ if pmm then {
+    let pmm_bits : bits(2) = get_pmm();
+    let mode : SATPMode = translationMode(cur_privilege);
+    match (mode) {
+      (Sbare) => {
+        match (pmm_bits){
+          (0b10) => transform_PA (vaddr,7),
+          (0b11) => transform_PA (vaddr,16),
+        }
+      },
+      (Sv48) => {
+        match (pmm_bits){
+          (0b10) => transform_VA (vaddr,7),
+          (0b11) => transform_VA (vaddr,16),          
+        }
+      },
+      (Sv57) => {
+        match (pmm_bits){
+          (0b10) => transform_VA (vaddr,7),
+          (0b11) => transform_VA (vaddr,16),          
+        }
+      },
+    }
+ }
+ else {
+  vaddr //PMM is not active
+ }
+}
 
 function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
+  let pmm = is_pmm_active();
   let offset : xlenbits = sign_extend(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); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) =>
-      if   check_misaligned(vaddr, width)
-      then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
-      else match translateAddr(vaddr, Read(Data)) {
-        TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+      let  vaddr_ = transform_effective_address(vaddr, pmm) in
+      if   check_misaligned(vaddr_, width)
+      then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); RETIRE_FAIL }
+      else match translateAddr(vaddr_, Read(Data)) {
+        TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
         TR_Address(paddr, _) =>
           match (width) {
             BYTE =>
-              process_load(rd, vaddr, mem_read(Read(Data), paddr, 1, aq, rl, false), is_unsigned),
+              process_load(rd, vaddr_, mem_read(Read(Data), paddr, 1, aq, rl, false), is_unsigned),
             HALF =>
-              process_load(rd, vaddr, mem_read(Read(Data), paddr, 2, aq, rl, false), is_unsigned),
+              process_load(rd, vaddr_, mem_read(Read(Data), paddr, 2, aq, rl, false), is_unsigned),
             WORD =>
-              process_load(rd, vaddr, mem_read(Read(Data), paddr, 4, aq, rl, false), is_unsigned),
+              process_load(rd, vaddr_, mem_read(Read(Data), paddr, 4, aq, rl, false), is_unsigned),
             DOUBLE if sizeof(xlen) >= 64 =>
-              process_load(rd, vaddr, mem_read(Read(Data), paddr, 8, aq, rl, false), is_unsigned),
+              process_load(rd, vaddr_, mem_read(Read(Data), paddr, 8, aq, rl, false), is_unsigned),
             _ => report_invalid_width(__FILE__, __LINE__, width, "load")
           }
       }
@@ -379,16 +431,18 @@ 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 pmm = is_pmm_active();
   let offset : xlenbits = sign_extend(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); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) =>
-      if   check_misaligned(vaddr, width)
-      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
-      else match translateAddr(vaddr, Write(Data)) {
-        TR_Failure(e, _)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+      let  vaddr_ = transform_effective_address(vaddr, pmm) in
+      if   check_misaligned(vaddr_, width)
+      then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL }
+      else match translateAddr(vaddr_, Write(Data)) {
+        TR_Failure(e, _)    => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
         TR_Address(paddr, _) => {
           let eares : MemoryOpResult(unit) = match width {
             BYTE   => mem_write_ea(paddr, 1, aq, rl, false),
@@ -397,7 +451,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
             DOUBLE => mem_write_ea(paddr, 8, aq, rl, false)
           };
           match (eares) {
-            MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+            MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
             MemValue(_) => {
               let rs2_val = X(rs2);
               let res : MemoryOpResult(bool) = match (width) {
@@ -411,7 +465,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
               match (res) {
                 MemValue(true)  => RETIRE_SUCCESS,
                 MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
-                MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
+                MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }
               }
             }
           }