@@ -24,11 +24,11 @@ use linux_loader::loader::pe::PE as Loader;
2424use linux_loader:: loader:: { Cmdline , KernelLoader } ;
2525use vm_memory:: GuestMemoryError ;
2626
27- use crate :: arch:: { BootProtocol , EntryPoint } ;
27+ use crate :: arch:: { BootProtocol , EntryPoint , arch_memory_regions_with_gap } ;
2828use crate :: cpu_config:: aarch64:: { CpuConfiguration , CpuConfigurationError } ;
2929use crate :: cpu_config:: templates:: CustomCpuTemplate ;
3030use crate :: initrd:: InitrdConfig ;
31- use crate :: utils:: { align_up, usize_to_u64} ;
31+ use crate :: utils:: { align_up, u64_to_usize , usize_to_u64} ;
3232use crate :: vmm_config:: machine_config:: MachineConfig ;
3333use crate :: vstate:: memory:: { Address , Bytes , GuestAddress , GuestMemory , GuestMemoryMmap } ;
3434use crate :: vstate:: vcpu:: KvmVcpuError ;
@@ -51,11 +51,6 @@ pub enum ConfigurationError {
5151 VcpuConfigure ( #[ from] KvmVcpuError ) ,
5252}
5353
54- /// The start of the memory area reserved for MMIO devices.
55- pub const MMIO_MEM_START : u64 = layout:: MAPPED_IO_START ;
56- /// The size of the memory area reserved for MMIO devices.
57- pub const MMIO_MEM_SIZE : u64 = layout:: DRAM_MEM_START - layout:: MAPPED_IO_START ; //>> 1GB
58-
5954/// Returns a Vec of the valid memory addresses for aarch64.
6055/// See [`layout`](layout) module for a drawing of the specific memory model for this platform.
6156///
@@ -71,7 +66,10 @@ pub fn arch_memory_regions(offset: usize, size: usize) -> Vec<(GuestAddress, usi
7166 "offset outside allowed DRAM range"
7267 ) ;
7368
74- let dram_size = min ( size, layout:: DRAM_MEM_MAX_SIZE - offset) ;
69+ let dram_size = min (
70+ size,
71+ layout:: DRAM_MEM_MAX_SIZE - offset - u64_to_usize ( layout:: MMIO64_MEM_SIZE ) ,
72+ ) ;
7573
7674 if dram_size != size {
7775 logger:: warn!(
@@ -83,10 +81,18 @@ pub fn arch_memory_regions(offset: usize, size: usize) -> Vec<(GuestAddress, usi
8381 ) ;
8482 }
8583
86- vec ! [ (
87- GuestAddress ( layout:: DRAM_MEM_START + offset as u64 ) ,
88- dram_size,
89- ) ]
84+ let mut regions = vec ! [ ] ;
85+ if let Some ( ( offset, remaining) ) = arch_memory_regions_with_gap (
86+ & mut regions,
87+ usize:: try_from ( layout:: DRAM_MEM_START ) . unwrap ( ) + offset,
88+ size,
89+ u64_to_usize ( layout:: MMIO64_MEM_START ) ,
90+ u64_to_usize ( layout:: MMIO64_MEM_SIZE ) ,
91+ ) {
92+ regions. push ( ( GuestAddress ( offset as u64 ) , remaining) ) ;
93+ }
94+
95+ regions
9096}
9197
9298/// Configures the system for booting Linux.
@@ -211,9 +217,10 @@ pub fn load_kernel(
211217
212218#[ cfg( kani) ]
213219mod verification {
214- use vm_memory:: GuestAddress ;
215-
216220 use crate :: arch:: aarch64:: layout;
221+ use crate :: arch:: aarch64:: layout:: {
222+ FIRST_ADDR_PAST_32BITS , FIRST_ADDR_PAST_64BITS_MMIO , MMIO32_MEM_START , MMIO64_MEM_START ,
223+ } ;
217224 use crate :: arch:: arch_memory_regions;
218225
219226 #[ kani:: proof]
@@ -228,23 +235,44 @@ mod verification {
228235
229236 let regions = arch_memory_regions ( offset as usize , len as usize ) ;
230237
231- // No MMIO gap on ARM
232- assert_eq ! ( regions. len( ) , 1 ) ;
233-
234- let ( GuestAddress ( start) , actual_len) = regions[ 0 ] ;
235- let actual_len = actual_len as u64 ;
238+ // On Arm we have one MMIO gap that might fall within addressable ranges,
239+ // so we can get either 1 or 2 regions.
240+ assert ! ( regions. len( ) >= 1 ) ;
241+ assert ! ( regions. len( ) <= 2 ) ;
236242
243+ // The very first address should be offset bytes past DRAM_MEM_START
237244 assert_eq ! ( start, layout:: DRAM_MEM_START + offset) ;
238- assert ! ( actual_len <= layout:: DRAM_MEM_MAX_SIZE as u64 ) ;
245+ // The total length of all regions cannot exceed DRAM_MEM_MAX_SIZE
246+ let actual_len = regions. iter ( ) . map ( |& ( _, len) | len) . sum :: < usize > ( ) ;
247+ assert ! ( actual_len <= layout:: DRAM_MEM_MAX_SIZE ) ;
248+ // The total length is smaller or equal to the length we asked
239249 assert ! ( actual_len <= len) ;
240-
250+ // If it's smaller, it's because we asked more than the the maximum possible.
241251 if actual_len < len {
242- assert_eq ! (
243- start + actual_len,
244- layout:: DRAM_MEM_START + layout:: DRAM_MEM_MAX_SIZE as u64
245- ) ;
246252 assert ! ( offset + len >= layout:: DRAM_MEM_MAX_SIZE as u64 ) ;
247253 }
254+
255+ // No region overlaps the 64-bit MMIO gap
256+ assert ! (
257+ regions
258+ . iter( )
259+ . all( |& ( start, len) | start. 0 >= FIRST_ADDR_PAST_64BITS_MMIO
260+ || start. 0 + len as u64 <= MMIO64_MEM_START )
261+ ) ;
262+
263+ // All regions start after our specified offset
264+ assert ! ( regions. iter( ) . all( |& ( start, _) | start. 0 >= offset as u64 ) ) ;
265+
266+ // All regions have non-zero length
267+ assert ! ( regions. iter( ) . all( |& ( _, len) | len > 0 ) ) ;
268+
269+ // If there's two regions, they perfectly snuggle up the 64bit MMIO gap
270+ if regions. len ( ) == 2 {
271+ kani:: cover!( ) ;
272+
273+ assert_eq ! ( regions[ 0 ] . 0.0 + regions[ 0 ] . 1 as u64 , MMIO32_MEM_START ) ;
274+ assert_eq ! ( regions[ 1 ] . 0.0 , FIRST_ADDR_PAST_32BITS ) ;
275+ }
248276 }
249277}
250278
0 commit comments