use newtype to reflect address type #615

KotorinMinami · 2024-11-12T04:26:04Z

As mentioned in the #434 , using newtype to refactor the types of virtual memory and physical memory, the xlenbits type in the sail code part of the model which I think that should be virtaddrs or physaddr is refactored to correspond to the virtaddrs/physaddr type.

Additionally, there seems to be excessive structurally similar redundant code in the memory read and write of the V extension, and I may create a simplified PR later.

github-actions · 2024-11-12T04:58:20Z

Test Results

396 tests ±0 396 ✅ ±0 0s ⏱️ ±0s
4 suites ±0 0 💤 ±0
1 files ±0 0 ❌ ±0

Results for commit 4815231. ± Comparison against base commit 07fa23e.

♻️ This comment has been updated with latest results.

Timmmm · 2024-11-12T12:47:46Z

This looks great! I'll try and review it when I get a chance.

arichardson · 2024-11-14T01:01:40Z

model/prelude_mem_addrtype.sail

+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+newtype physaddr = physaddr : xlenbits


Does not necessarily need fixing for this PR, but the privileged spec defines physical addresses as 34 bits for RV32.

Yeah I think there's a long-standing TODO for that. Hopefully this PR will make fixing it a little easier!

Timmmm

Had a skim. Looks pretty good. I think there are some places where I would move the types slightly. In particular I think handle_mem_exception should take virtaddr and that would greatly reduce the size of the PR too. I haven't checked in detail though so I might be wrong. Can you double check, and if so, make that change and then I'll take another look?

Timmmm · 2024-11-16T14:18:59Z

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) =


Should the parameters here be changed to virtaddr instead? And in the other three functions below.

Hmm, my thought is that although we know the parameters of these four functions are supposed to be virtual addresses, the naming of this function implies that it should be responsible for validating the incoming register values, which is xlenbits, through type checks and then converting them into virtual addresses, or redirecting to other error types. Although the current implementation does not achieve this, we should keep this as an unimplemented interface for future expansion

I don't think PC is an architecturally visible register in the same way that x1 is though - it's kind of an invisible thing that only stores addresses (which aren't necessarily xlenbits).

I haven't made a PR for it yet but in our fork we explicitly handle that via an invalid address conversion function that is called in set_next_pc().

But... it's pretty minor. I don't mind if you leave it.

Timmmm · 2024-11-16T14:21:57Z

model/riscv_insts_aext.sail

-      if not(is_aligned(vaddr, width))
-      then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
+      if not(is_aligned(virtaddr_bits(vaddr), width))
+      then { handle_mem_exception(virtaddr_bits(vaddr), E_Load_Addr_Align()); RETIRE_FAIL }


I think handle_mem_exception always takes a virtual address, so maybe you can change its parameter to virtaddr?

Thank you for pointing that out, so I won't be tormented by multiple calls in vext_mem, I will fix it.

Timmmm · 2024-11-16T14:23:31Z

model/riscv_insts_aext.sail

@@ -131,27 +131,27 @@ 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))
-        then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
+        if not(is_aligned(virtaddr_bits(vaddr), width))


I would probably turn is_aligned into an overload that can take bits(), physaddr or virtaddr. Maybe not in this PR...

Timmmm · 2024-11-16T14:28:07Z

model/prelude_mem_addrtype.sail

+/*=======================================================================================*/
+
+newtype physaddr = physaddr : xlenbits
+newtype virtaddr = virtaddr : xlenbits


Can you add a note:

Note virtaddr includes physical addresses when address translation is disabled. It is used where the address would be virtual if address translation is active.

It's slightly confusing otherwise and I don't think we're going to come up with a clearer name (untranslatedaddr?...)

I find this comment confusing and I believe this is not needed?

We already have a "no-op" translation from virtaddr to physaddr for the bare case (Sbare => return TR_Address(physaddr(virtaddr_bits(vAddr)), init_ext_ptw),) so we can just always start out with a virtual address, but in the SBare case it just happens to be 1:1 mapped to a physical one?

However, in chip implementations that do not support virtual addresses, there is no concept of a virtual address, so virtaddr should be interpreted as physaddr, rather than through translation. The Sbare implementation just happens to be compatible with this situation while also being compatible with direct read and write of physical memory in M-mode

Yeah exactly. Also in Sbare mode I think it's natural to think of the address as physical addresses rather than virtual addresses that go through an identity translation.

Maybe my comment didn't explain that very well, but I think we need to have some kind of explanation of this subtlety.

If you would like to define it that way, I would prefer to add something like a "cpuaddr" that is explicitly converted to virtaddr/physaddr depending on whether a MMU is present/enabled. That is IMO cleaner than saying virtaddr can be physaddr depending on where it is being used. For a m-mode only CPU I'd be fine with cpuaddr being physaddr, but I still view sbare as a 1:1 mapping rather than addresses being physical when switching off the MMU (since the MMU could be turned on again).

Once hypervisor is implemented we should add intermediate physical addresses that are stage2 translated before being turned into physaddrs, this also means directly using physaddr when the stage1 MMU is disabled is not correct.

Timmmm

The changes look good to me. What do people think about the ergonomics of this?

Timmmm · 2024-11-22T10:03:02Z

model/riscv_insts_base.sail

      /* Perform standard alignment check */
      if bit_to_bool(target[1]) & not(extensionEnabled(Ext_Zca))
      then {
-        handle_mem_exception(target, E_Fetch_Addr_Align());
+        handle_mem_exception(virtaddr(target), E_Fetch_Addr_Align());


Hmm it's unfortunate that we have to destructure to xlenbits to access the bits and then reconstruct the type. @Alasdair since a newtype is always a known type is there any way we can access the inner type without destructuring it? E.g. in Rust you have this idiom:

struct virtaddr(xlenbits);

And then you can access the xlenbits via my_virt_addr.0.

Oh actually @KotorinMinami I guess we could use your virtaddr_bits function like:

Ext_ControlAddr_OK(target) => { /* Perform standard alignment check */ if bit_to_bool(virtaddr_bits(target)[1]) & not(extensionEnabled(Ext_Zca)) then { handle_mem_exception(target, E_Fetch_Addr_Align());

It's a bit verbose though. Hmm.

arichardson · 2024-11-22T20:42:54Z

model/prelude_mem_addrtype.sail

+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+/* Note: virtaddr includes physical addresses when address translation is disabled.


As noted below, I don't see how this can work once physaddr is actually bits(34) on RV32. But I guess that can be fixed once this is actually changed.

Well with satp.MODE = Bare you can't address more than XLEN bits of PA space, you have to have translation for that

arichardson

LGTM, my comments can be addressed once physaddr is actually changed.

KotorinMinami force-pushed the newtype_addr branch from 085fe0a to 1f3e64f Compare November 12, 2024 04:45

Timmmm self-requested a review November 12, 2024 12:47

arichardson reviewed Nov 14, 2024

View reviewed changes

Timmmm requested changes Nov 16, 2024

View reviewed changes

KotorinMinami force-pushed the newtype_addr branch from 1f3e64f to bc8b8d8 Compare November 18, 2024 21:13

KotorinMinami requested a review from Timmmm November 21, 2024 18:57

Timmmm reviewed Nov 22, 2024

View reviewed changes

arichardson reviewed Nov 22, 2024

View reviewed changes

arichardson approved these changes Nov 22, 2024

View reviewed changes

use newtype to reflect address type

4815231

KotorinMinami force-pushed the newtype_addr branch from bc8b8d8 to 4815231 Compare November 24, 2024 20:12

KotorinMinami requested a review from Timmmm November 27, 2024 19:58

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

use newtype to reflect address type #615

use newtype to reflect address type #615

KotorinMinami commented Nov 12, 2024

github-actions bot commented Nov 12, 2024 •

edited

Loading

Timmmm commented Nov 12, 2024

arichardson Nov 14, 2024

Timmmm Nov 16, 2024

Timmmm left a comment

Timmmm Nov 16, 2024

KotorinMinami Nov 18, 2024

Timmmm Nov 18, 2024

Timmmm Nov 16, 2024

KotorinMinami Nov 18, 2024

Timmmm Nov 16, 2024

Timmmm Nov 16, 2024

arichardson Nov 18, 2024

KotorinMinami Nov 18, 2024

Timmmm Nov 18, 2024

arichardson Nov 18, 2024

Timmmm left a comment

Timmmm Nov 22, 2024

arichardson Nov 22, 2024

jrtc27 Nov 22, 2024

arichardson left a comment

use newtype to reflect address type #615

Are you sure you want to change the base?

use newtype to reflect address type #615

Conversation

KotorinMinami commented Nov 12, 2024

github-actions bot commented Nov 12, 2024 • edited Loading

Test Results

Timmmm commented Nov 12, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Timmmm left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Timmmm left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

arichardson left a comment

Choose a reason for hiding this comment

github-actions bot commented Nov 12, 2024 •

edited

Loading