@@ -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,9 @@ pub fn load_kernel(
211217
212218#[ cfg( kani) ]
213219mod verification {
214- use vm_memory :: GuestAddress ;
215-
216- use crate :: arch :: aarch64 :: layout ;
220+ use crate :: arch :: aarch64 :: layout :: {
221+ DRAM_MEM_MAX_SIZE , FIRST_ADDR_PAST_64BITS , MMIO32_MEM_START , MMIO64_MEM_START ,
222+ } ;
217223 use crate :: arch:: arch_memory_regions;
218224
219225 #[ kani:: proof]
@@ -228,22 +234,43 @@ mod verification {
228234
229235 let regions = arch_memory_regions ( offset as usize , len as usize ) ;
230236
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 ;
237+ // On Arm we have one MMIO gap that might fall within addressable ranges,
238+ // so we can get either 1 or 2 regions.
239+ assert ! ( regions. len( ) >= 1 ) ;
240+ assert ! ( regions. len( ) <= 2 ) ;
236241
242+ // The very first address should be offset bytes past DRAM_MEM_START
237243 assert_eq ! ( start, layout:: DRAM_MEM_START + offset) ;
238- assert ! ( actual_len <= layout:: DRAM_MEM_MAX_SIZE as u64 ) ;
239- assert ! ( actual_len <= len) ;
240-
241- if actual_len < len {
242- assert_eq ! (
243- start + actual_len,
244- layout:: DRAM_MEM_START + layout:: DRAM_MEM_MAX_SIZE as u64
245- ) ;
246- assert ! ( offset + len >= layout:: DRAM_MEM_MAX_SIZE as u64 ) ;
244+ // The total length of all regions cannot exceed DRAM_MEM_MAX_SIZE
245+ let actual_len = regions. iter ( ) . map ( |& ( _, len) | len) . sum :: < usize > ( ) ;
246+ assert ! ( actual_len <= layout:: DRAM_MEM_MAX_SIZE ) ;
247+ // The total length is smaller or equal to the length we asked
248+ assert ! ( ( actual_len as u64 ) <= len) ;
249+ // If it's smaller, it's because we asked more than the the maximum possible.
250+ if ( actual_len as u64 ) < len {
251+ assert ! ( offset + len >= DRAM_MEM_MAX_SIZE as u64 ) ;
252+ }
253+
254+ // No region overlaps the 64-bit MMIO gap
255+ assert ! (
256+ regions
257+ . iter( )
258+ . all( |& ( start, len) | start. 0 >= FIRST_ADDR_PAST_64BITS_MMIO
259+ || start. 0 + len as u64 <= MMIO64_MEM_START )
260+ ) ;
261+
262+ // All regions start after our specified offset
263+ assert ! ( regions. iter( ) . all( |& ( start, _) | start. 0 >= offset as u64 ) ) ;
264+
265+ // All regions have non-zero length
266+ assert ! ( regions. iter( ) . all( |& ( _, len) | len > 0 ) ) ;
267+
268+ // If there's two regions, they perfectly snuggle up the 64bit MMIO gap
269+ if regions. len ( ) == 2 {
270+ kani:: cover!( ) ;
271+
272+ assert_eq ! ( regions[ 0 ] . 0.0 + regions[ 0 ] . 1 as u64 , MMIO32_MEM_START ) ;
273+ assert_eq ! ( regions[ 1 ] . 0.0 , FIRST_ADDR_PAST_64BITS ) ;
247274 }
248275 }
249276}
0 commit comments