RPi4: What is the correct peripheral address handling in CAmkES and DTS file?

So, I am running into a very specific problem. On Raspberry Pi platforms, we have the VideoCore GPU and the ARM cores. For the RPi4, the VideoCore uses base address 0x7e000000 and the ARM cores reference peripherals starting from 0xfe000000. In TRMs, documentation and also the DTS files (e.g. in Linux) the VideoCore view with base address 0x7e000000 is used. The DTS files that are used in the seL4 repository are generated based on the Linux kernel. As a result, the DTS files in the seL4 kernel also use the VideoCore view with base address 0x7e000000 (seL4/rpi4.dts at master · seL4/seL4 · GitHub).

Since user code is running on the ARM cores, peripherals in code should be addressed via the ARM base address 0xfe000000. The problem starts when referencing peripherals via the DTS file in CAmkES and the VideoCore address 0x7exxxxxx is mapped. If the drivers in libplatsupport then use hardcoded the peripherals with the ARM view (0xfe000000), then this obviously causes a conflict.

So my question is how to best cope with this situation. It seems to be highly specific to Raspberry Pi platforms. I guess I could simply hardcode the base addresses in CAmkES, but considering the DTS-way to be more elegant, I am wondering what would be the best way to cope with this issue. The following approaches would come to my mind:

Thank you very much in advance.

The same issue might exist on all other RasPis also. Handling this via a DTS overlay seems a nice generic solution.