use newtype to reflect address type

Makefile

@@ -97,7 +97,7 @@ SAIL_VM_SRCS += riscv_vmem_tlb.sail
 SAIL_VM_SRCS += riscv_vmem.sail
 
 # Non-instruction sources
-PRELUDE = prelude.sail riscv_errors.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
+PRELUDE = prelude.sail riscv_errors.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_addrtype.sail prelude_mem_metadata.sail prelude_mem.sail
 
 SAIL_REGS_SRCS =  riscv_csr_begin.sail       # Start of CSR scattered definitions.
 SAIL_REGS_SRCS += riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail

model/prelude_mem.sail

@@ -90,9 +90,9 @@ instantiation sail_mem_write with
    */
 type max_mem_access : Int = 4096
 
-val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool
+val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, physaddr, int('n), bits(8 * 'n), mem_meta) -> bool
 
-function write_ram(wk, addr, width, data, meta) = {
+function write_ram(wk, physaddr(addr), width, data, meta) = {
   let request : Mem_write_request('n, 64, xlenbits, unit, RISCV_strong_access) = struct {
     access_kind = match wk {
       Write_plain => AK_explicit(struct { variety = AV_plain, strength = AS_normal }),
@@ -125,14 +125,14 @@ function write_ram(wk, addr, width, data, meta) = {
   }
 }
 
-val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n)) -> unit
-function write_ram_ea(wk, addr, width) = ()
+val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access. (write_kind, physaddr, int('n)) -> unit
+function write_ram_ea(wk, physaddr(addr), width) = ()
 
 instantiation sail_mem_read with
   pa_bits = xlenbits_identity
 
-val read_ram : forall 'n, 0 < 'n <= max_mem_access.  (read_kind, xlenbits, int('n), bool) -> (bits(8 * 'n), mem_meta)
-function read_ram(rk, addr, width, read_meta) = {
+val read_ram : forall 'n, 0 < 'n <= max_mem_access.  (read_kind, physaddr, int('n), bool) -> (bits(8 * 'n), mem_meta)
+function read_ram(rk, physaddr(addr), width, read_meta) = {
   let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta;
   let request : Mem_read_request('n, 64, xlenbits, unit, RISCV_strong_access) = struct {
     access_kind = match rk {

model/prelude_mem_addrtype.sail

@@ -0,0 +1,18 @@
+/*=======================================================================================*/
+/*  This Sail RISC-V architecture model, comprising all files and                        */
+/*  directories except where otherwise noted is subject the BSD                          */
+/*  two-clause license in the LICENSE file.                                              */
+/*                                                                                       */
+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+/* Note: virtaddr includes physical addresses when address translation is disabled.
+ * It is used where the address would be virtual if address translation is active.
+ */
+
+newtype physaddr = physaddr : xlenbits
+newtype virtaddr = virtaddr : xlenbits
+
+function physaddr_bits(physaddr(paddr) : physaddr) -> xlenbits = paddr
+
+function virtaddr_bits(virtaddr(vaddr) : virtaddr) -> xlenbits = vaddr

model/riscv_addr_checks.sail

@@ -18,7 +18,7 @@ type ext_fetch_addr_error = unit
  *           any address translation errors are reported for pc, not the returned value.
  */
 function ext_fetch_check_pc(start_pc : xlenbits, pc : xlenbits) -> Ext_FetchAddr_Check(ext_fetch_addr_error) =
-  Ext_FetchAddr_OK(pc)
+  Ext_FetchAddr_OK(virtaddr(pc))
 
 function ext_handle_fetch_check_error(err : ext_fetch_addr_error) -> unit =
   ()
@@ -38,11 +38,11 @@ type ext_control_addr_error = unit
 
 /* the control address is derived from a non-PC register, e.g. in JALR */
 function ext_control_check_addr(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) =
-  Ext_ControlAddr_OK(pc)
+  Ext_ControlAddr_OK(virtaddr(pc))
 
 /* the control address is derived from the PC register, e.g. in JAL */
 function ext_control_check_pc(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) =
-  Ext_ControlAddr_OK(pc)
+  Ext_ControlAddr_OK(virtaddr(pc))
 
 function ext_handle_control_check_error(err : ext_control_addr_error) -> unit =
   ()
@@ -56,7 +56,7 @@ type ext_data_addr_error = unit
    Extensions might override and add additional checks. */
 function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : range(1, max_mem_access))
          -> Ext_DataAddr_Check(ext_data_addr_error) =
-  let addr = X(base) + offset in
+  let addr = virtaddr(X(base) + offset) in
   Ext_DataAddr_OK(addr)
 
 function ext_handle_data_check_error(err : ext_data_addr_error) -> unit =

model/riscv_addr_checks_common.sail

@@ -15,17 +15,17 @@
  */
 
 union Ext_FetchAddr_Check ('a : Type) = {
-  Ext_FetchAddr_OK  : xlenbits,  /* PC value to use for the actual fetch */
+  Ext_FetchAddr_OK  : virtaddr,  /* PC value to use for the actual fetch */
   Ext_FetchAddr_Error : 'a
 }
 
 union Ext_ControlAddr_Check ('a : Type) = {
-  Ext_ControlAddr_OK : xlenbits, /* PC value to use for the target of the control operation */
+  Ext_ControlAddr_OK : virtaddr, /* PC value to use for the target of the control operation */
   Ext_ControlAddr_Error : 'a
 }
 
 union Ext_DataAddr_Check ('a : Type) = {
-  Ext_DataAddr_OK : xlenbits,    /* Address to use for the data access */
+  Ext_DataAddr_OK : virtaddr,    /* Address to use for the data access */
   Ext_DataAddr_Error : 'a
 }
 
@@ -40,12 +40,12 @@ union Ext_PhysAddr_Check = {
  * return Some(exception) to abort the read or None to allow it to proceed. The
  * check is performed after PMP checks and does not apply to MMIO memory.
  */
-val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType (ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> Ext_PhysAddr_Check
+val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType (ext_access_type), physaddr, int('n), bool, bool, bool, bool) -> Ext_PhysAddr_Check
 
 /*!
  * Validate a write to physical memory.
  * THIS(write_kind, paddr, size, data, metadata) should return Some(exception)
  * to abort the write or None to allow it to proceed. The check is performed
  * after PMP checks and does not apply to MMIO memory.
  */
-val ext_check_phys_mem_write : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> Ext_PhysAddr_Check
+val ext_check_phys_mem_write : forall 'n, 0 < 'n <= max_mem_access . (write_kind, physaddr, int('n), bits(8 * 'n), mem_meta) -> Ext_PhysAddr_Check

model/riscv_fetch.sail

@@ -19,7 +19,8 @@ function fetch() -> FetchResult =
   match ext_fetch_check_pc(PC, PC) {
     Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
     Ext_FetchAddr_OK(use_pc) => {
-      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(extensionEnabled(Ext_Zca))))
+      let use_pc_bits = virtaddr_bits(use_pc);
+      if   (use_pc_bits[0] != bitzero | (use_pc_bits[1] != bitzero & not(extensionEnabled(Ext_Zca))))
       then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e, _)     => F_Error(e, PC),

model/riscv_fetch_rvfi.sail

@@ -17,7 +17,8 @@ function fetch() -> FetchResult = {
     Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
     Ext_FetchAddr_OK(use_pc) => {
       /* then check PC alignment */
-      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(extensionEnabled(Ext_Zca))))
+      let use_pc_bits = virtaddr_bits(use_pc);
+      if   (use_pc_bits[0] != bitzero | (use_pc_bits[1] != bitzero & not(extensionEnabled(Ext_Zca))))
       then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e, _) => F_Error(e, PC),

model/riscv_insts_aext.sail

@@ -86,13 +86,13 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
       /* "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(is_aligned(vaddr, width))
+      if not(is_aligned(virtaddr_bits(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(addr, _) =>
           match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) {
-            MemValue(result) => { load_reservation(addr); X(rd) = sign_extend(result); RETIRE_SUCCESS },
+            MemValue(result) => { load_reservation(physaddr_bits(addr)); X(rd) = sign_extend(result); RETIRE_SUCCESS },
             MemException(e)  => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
           },
       }
@@ -131,15 +131,15 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
     match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
       Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
       Ext_DataAddr_OK(vaddr) => {
-        if not(is_aligned(vaddr, width))
+        if not(is_aligned(virtaddr_bits(vaddr), width))
         then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
         else {
           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_Address(addr, _) => {
               // Check reservation with physical address.
-              if not(match_reservation(addr)) then {
+              if not(match_reservation(physaddr_bits(addr))) then {
                 /* cannot happen in rmem */
                 X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
               } else {
@@ -202,7 +202,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
   match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width_bytes) {
     Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) => {
-      if not(is_aligned(vaddr, width))
+      if not(is_aligned(virtaddr_bits(vaddr), width))
       then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
       else match translateAddr(vaddr, ReadWrite(Data, Data)) {
         TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },

model/riscv_insts_base.sail

@@ -72,13 +72,14 @@ function clause execute (RISCV_JAL(imm, rd)) = {
     },
     Ext_ControlAddr_OK(target) => {
       /* Perform standard alignment check */
-      if bit_to_bool(target[1]) & not(extensionEnabled(Ext_Zca))
+      let target_bits = virtaddr_bits(target);
+      if bit_to_bool(target_bits[1]) & not(extensionEnabled(Ext_Zca))
       then {
         handle_mem_exception(target, E_Fetch_Addr_Align());
         RETIRE_FAIL
       } else {
         X(rd) = get_next_pc();
-        set_next_pc(target);
+        set_next_pc(target_bits);
         RETIRE_SUCCESS
       }
     }
@@ -136,11 +137,12 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
         RETIRE_FAIL
       },
       Ext_ControlAddr_OK(target) => {
-        if bit_to_bool(target[1]) & not(extensionEnabled(Ext_Zca)) then {
+        let target_bits = virtaddr_bits(target);
+        if bit_to_bool(target_bits[1]) & not(extensionEnabled(Ext_Zca)) then {
           handle_mem_exception(target, E_Fetch_Addr_Align());
           RETIRE_FAIL;
         } else {
-          set_next_pc(target);
+          set_next_pc(target_bits);
           RETIRE_SUCCESS
         }
       }
@@ -317,8 +319,8 @@ function is_aligned(vaddr : xlenbits, width : word_width) -> bool =
   }
 
 // Return true if the address is misaligned and we don't support misaligned access.
-function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
-  not(plat_enable_misaligned_access()) & not(is_aligned(vaddr, width))
+function check_misaligned(vaddr : virtaddr, width : word_width) -> bool =
+  not(plat_enable_misaligned_access()) & not(is_aligned(virtaddr_bits(vaddr), width))
 
 function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
   let offset : xlenbits = sign_extend(imm);
@@ -678,7 +680,7 @@ mapping clause encdec = EBREAK()
   <-> 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute EBREAK() = {
-  handle_mem_exception(PC, E_Breakpoint());
+  handle_mem_exception(virtaddr(PC), E_Breakpoint());
   RETIRE_FAIL
 }
 

model/riscv_insts_fext.sail

@@ -290,7 +290,7 @@ mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE)        if extensionEnabled
 
 /* Execution semantics ================================ */
 
-val process_fload64 : (regidx, xlenbits, MemoryOpResult(bits(64)))
+val process_fload64 : (regidx, virtaddr, MemoryOpResult(bits(64)))
                       -> Retired
 function process_fload64(rd, addr, value) =
   if   flen == 64
@@ -303,15 +303,15 @@ function process_fload64(rd, addr, value) =
     RETIRE_FAIL
   }
 
-val process_fload32 : (regidx, xlenbits, MemoryOpResult(bits(32)))
+val process_fload32 : (regidx, virtaddr, MemoryOpResult(bits(32)))
                       -> Retired
 function process_fload32(rd, addr, value) =
   match value {
     MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
     MemException(e)  => { handle_mem_exception(addr, e); RETIRE_FAIL }
   }
 
-val process_fload16 : (regidx, xlenbits, MemoryOpResult(bits(16)))
+val process_fload16 : (regidx, virtaddr, MemoryOpResult(bits(16)))
                       -> Retired
 function process_fload16(rd, addr, value) =
   match value {
@@ -376,7 +376,7 @@ mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE)
 
 /* Execution semantics ================================ */
 
-val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired
+val process_fstore : (virtaddr, MemoryOpResult(bool)) -> Retired
 function process_fstore(vaddr, value) =
   match value {
     MemValue(true)  => { RETIRE_SUCCESS },

model/riscv_jalr_seq.sail

@@ -23,9 +23,9 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
       RETIRE_FAIL
     },
     Ext_ControlAddr_OK(addr) => {
-      let target = [addr with 0 = bitzero];  /* clear addr[0] */
+      let target = [virtaddr_bits(addr) with 0 = bitzero];  /* clear addr[0] */
       if bit_to_bool(target[1]) & not(extensionEnabled(Ext_Zca)) then {
-        handle_mem_exception(target, E_Fetch_Addr_Align());
+        handle_mem_exception(addr, E_Fetch_Addr_Align());
         RETIRE_FAIL
       } else {
         X(rd) = get_next_pc();