Fix incorrect behaviour with INT_MAX pmpaddr

This fixes a bug if you set `pmpaddr` to `ones()`. For NAPOT it would return `(zeros(), zeros())`. For NA4 it would return `(ones(), zeros())`. In both cases it will match no addresses, whereas it should match all memory, or the top 4 bytes respectively.

A test is included for NAPOT that fails before and passes afterwards.

Fixes riscv#739

model/riscv_pmp_control.sail

@@ -6,35 +6,6 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
-/* address ranges */
-
-// [min, max) of the matching range, in units of 4 bytes.
-type pmp_addr_range_in_words = option((xlenbits, xlenbits))
-
-function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmp_addr_range_in_words = {
-  match pmpAddrMatchType_of_bits(cfg[A]) {
-    OFF   => None(),
-    TOR   => { Some ((prev_pmpaddr, pmpaddr)) },
-    NA4   => {
-               // NA4 is not selectable when the PMP grain G >= 1. See pmpWriteCfg().
-               assert(sys_pmp_grain() < 1, "NA4 cannot be selected when PMP grain G >= 1.");
-               let lo = pmpaddr;
-               Some((lo, lo + 1))
-             },
-    NAPOT => {
-               // Example pmpaddr: 0b00010101111
-               //                          ^--- last 0 dictates region size & alignment
-               let mask = pmpaddr ^ (pmpaddr + 1);
-               // pmpaddr + 1:     0b00010110000
-               // mask:            0b00000011111
-               // ~mask:           0b11111100000
-               let lo   = pmpaddr & (~ (mask));
-               // mask + 1:        0b00000100000
-               let len  = mask + 1;
-               Some((lo, (lo + len)))
-             }
-  }
-}
 
 /* permission checks */
 
@@ -52,26 +23,58 @@ function pmpCheckRWX(ent, acc) =
 
 enum pmpAddrMatch = {PMP_NoMatch, PMP_PartialMatch, PMP_Match}
 
-function pmpMatchAddr(physaddr(addr): physaddr, width: xlenbits, rng: pmp_addr_range_in_words) -> pmpAddrMatch = {
-  match rng {
-    None()         => PMP_NoMatch,
-    Some((lo, hi)) => {
-      // Convert to integers.
-      let addr  = unsigned(addr);
-      let width = unsigned(width);
-      // These are in units of 4 bytes.
-      let lo = unsigned(lo) * 4;
-      let hi = unsigned(hi) * 4;
-
-      if   hi <= lo   /* to handle mis-configuration */
+// Given a right-open interval [begin, end_), return whether [addr, addr+width)
+// is contained fully within it (PMP_Match), doesn't overlap at all (PMP_NoMatch)
+// or partially intersects it (PMP_PartialMatch).
+function pmpRangeMatch(
+  begin : nat,
+  end_ : nat,
+  addr : nat,
+  width : nat,
+) -> pmpAddrMatch =
+  if      (addr + width <= begin) | (end_ <= addr)
+  then    PMP_NoMatch
+  else if (begin <= addr) & (addr + width <= end_)
+  then    PMP_Match
+  else    PMP_PartialMatch
+
+function pmpMatchAddr(
+  physaddr(addr) : physaddr,
+  width : xlenbits,
+  ent : Pmpcfg_ent,
+  pmpaddr : xlenbits,
+  prev_pmpaddr: xlenbits,
+) -> pmpAddrMatch = {
+  let addr = unsigned(addr);
+  let width = unsigned(width);
+  match pmpAddrMatchType_of_bits(ent[A]) {
+    OFF => PMP_NoMatch,
+    TOR => {
+      // "If PMP entry [i]'s A field is set to TOR, the entry matches
+      //  any address y such that pmpaddr[i-1] <= y < pmpaddr[i]"
+      // "If pmpaddr[i-1] >= pmpaddr[i] and pmpcfg[i].A=TOR, then PMP entry i matches no addresses."
+      if prev_pmpaddr >=_u pmpaddr
       then PMP_NoMatch
-      else {
-        if      (addr + width <= lo) | (hi <= addr)
-        then    PMP_NoMatch
-        else if (lo <= addr) & (addr + width <= hi)
-        then    PMP_Match
-        else    PMP_PartialMatch
-      }
+      else pmpRangeMatch(unsigned(prev_pmpaddr), unsigned(pmpaddr), addr, width)
+    },
+    NA4 => {
+      // NA4 is not selectable when the PMP grain G >= 1. See pmpWriteCfg().
+      assert(sys_pmp_grain() < 1, "NA4 cannot be selected when PMP grain G >= 1.");
+      // Match a 4-byte region.
+      let begin = unsigned(pmpaddr @ 0b00);
+      pmpRangeMatch(begin, begin + 4, addr, width)
+    },
+    NAPOT => {
+      // Example pmpaddr: 0b00010101111
+      //                          ^--- last 0 dictates region size & alignment
+      let mask = pmpaddr ^ (pmpaddr + 1);
+      // pmpaddr + 1:     0b00010110000
+      // mask:            0b00000011111
+      // ~mask:           0b11111100000
+      let begin = unsigned(pmpaddr & (~(mask)));
+      // mask + 1:        0b00000100000
+      let end_ = begin + unsigned(mask) + 1;
+      pmpRangeMatch(begin, end_, addr, width)
     },
   }
 }
@@ -80,8 +83,7 @@ enum pmpMatch = {PMP_Success, PMP_Continue, PMP_Fail}
 
 function pmpMatchEntry(addr: physaddr, width: xlenbits, acc: AccessType(ext_access_type), priv: Privilege,
                        ent: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmpMatch = {
-  let rng = pmpAddrRange(ent, pmpaddr, prev_pmpaddr);
-  match pmpMatchAddr(addr, width, rng) {
+  match pmpMatchAddr(addr, width, ent, pmpaddr, prev_pmpaddr) {
     PMP_NoMatch      => PMP_Continue,
     PMP_PartialMatch => PMP_Fail,
     PMP_Match        => if pmpCheckRWX(ent, acc) | (priv == Machine & not(pmpLocked(ent)))

test/first_party/CMakeLists.txt

@@ -78,6 +78,7 @@ set(common_deps
 
 set(tests
     "test_hello_world.c"
+    "test_max_pmp.c"
     "test_minstret.S"
 )
 

test/first_party/src/test_max_pmp.c

@@ -0,0 +1,41 @@
+#include "common/runtime.h"
+
+#include <stdint.h>
+#include <stddef.h>
+
+#define PMPCFG_L (0b1 << 7)
+#define PMPCFG_NA4 (0b10 << 3)
+#define PMPCFG_NAPOT (0b11 << 3)
+#define PMPCFG_X (0b1 << 2)
+#define PMPCFG_W (0b1 << 1)
+#define PMPCFG_R (0b1 << 0)
+
+#define MSTATUS_MPP_MASK (0b11 << 11)
+#define MSTATUS_MPRV_MASK (0b1 << 17)
+
+int main()
+{
+  printf("Testing 0xFF..FF PMP addresses\n");
+
+  uint_xlen_t ones = UINT_XLEN_MAX;
+
+  asm volatile("csrw pmpaddr0, %[ones]" : : [ones] "r"(ones));
+
+  // Set mstatus.MPP and mstatus.MPRV so that loads/stores are
+  // done in user mode. If they don't match the pmp then
+  // they'll fail.
+  uint_xlen_t mpp = MSTATUS_MPP_MASK;
+  uint_xlen_t mprv = MSTATUS_MPRV_MASK;
+  asm volatile("csrc mstatus, %[mpp];"
+               "csrs mstatus, %[mprv];"
+               :
+               : [mpp] "r"(mpp), [mprv] "r"(mprv));
+
+  uint_xlen_t pmpcfg_napot = PMPCFG_NAPOT | PMPCFG_X | PMPCFG_W | PMPCFG_R;
+
+  asm volatile("csrw pmpcfg0, %[cfg]" : : [cfg] "r"(pmpcfg_napot));
+
+  // Access memory to test loads/stores.
+  printf("Passed\n");
+  return 0;
+}