@@ -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///
@@ -83,10 +78,18 @@ pub fn arch_memory_regions(offset: usize, size: usize) -> Vec<(GuestAddress, usi
8378 ) ;
8479 }
8580
86- vec ! [ (
87- GuestAddress ( layout:: DRAM_MEM_START + offset as u64 ) ,
88- dram_size,
89- ) ]
81+ let mut regions = vec ! [ ] ;
82+ if let Some ( ( offset, remaining) ) = arch_memory_regions_with_gap (
83+ & mut regions,
84+ usize:: try_from ( layout:: DRAM_MEM_START ) . unwrap ( ) + offset,
85+ size,
86+ u64_to_usize ( layout:: MMIO64_MEM_START ) ,
87+ u64_to_usize ( layout:: MMIO64_MEM_SIZE ) ,
88+ ) {
89+ regions. push ( ( GuestAddress ( offset as u64 ) , remaining) ) ;
90+ }
91+
92+ regions
9093}
9194
9295/// Configures the system for booting Linux.
@@ -211,9 +214,10 @@ pub fn load_kernel(
211214
212215#[ cfg( kani) ]
213216mod verification {
214- use vm_memory:: GuestAddress ;
215-
216- use crate :: arch:: aarch64:: layout;
217+ use crate :: arch:: aarch64:: layout:: {
218+ DRAM_MEM_MAX_SIZE , DRAM_MEM_START , FIRST_ADDR_PAST_64BITS_MMIO , MMIO32_MEM_START ,
219+ MMIO64_MEM_START ,
220+ } ;
217221 use crate :: arch:: arch_memory_regions;
218222
219223 #[ kani:: proof]
@@ -224,60 +228,90 @@ mod verification {
224228
225229 kani:: assume ( len > 0 ) ;
226230 kani:: assume ( offset. checked_add ( len) . is_some ( ) ) ;
227- kani:: assume ( offset < layout :: DRAM_MEM_MAX_SIZE as u64 ) ;
231+ kani:: assume ( offset < DRAM_MEM_MAX_SIZE as u64 ) ;
228232
229233 let regions = arch_memory_regions ( offset as usize , len as usize ) ;
230234
231- // No MMIO gap on ARM
232- assert_eq ! ( regions. len( ) , 1 ) ;
235+ // On Arm we have one MMIO gap that might fall within addressable ranges,
236+ // so we can get either 1 or 2 regions.
237+ assert ! ( regions. len( ) >= 1 ) ;
238+ assert ! ( regions. len( ) <= 2 ) ;
239+
240+ // The very first address should be offset bytes past DRAM_MEM_START
241+ assert_eq ! ( regions[ 0 ] . 0.0 , DRAM_MEM_START + offset) ;
242+ // The total length of all regions cannot exceed DRAM_MEM_MAX_SIZE
243+ let actual_len = regions. iter ( ) . map ( |& ( _, len) | len) . sum :: < usize > ( ) ;
244+ assert ! ( actual_len <= DRAM_MEM_MAX_SIZE ) ;
245+ // The total length is smaller or equal to the length we asked
246+ assert ! ( ( actual_len as u64 ) <= len) ;
247+ // If it's smaller, it's because we asked more than the the maximum possible.
248+ if ( actual_len as u64 ) < len {
249+ assert ! ( offset + len >= DRAM_MEM_MAX_SIZE as u64 ) ;
250+ }
251+
252+ // No region overlaps the 64-bit MMIO gap
253+ assert ! (
254+ regions
255+ . iter( )
256+ . all( |& ( start, len) | start. 0 >= FIRST_ADDR_PAST_64BITS_MMIO
257+ || start. 0 + len as u64 <= MMIO64_MEM_START )
258+ ) ;
259+
260+ // All regions start after our specified offset
261+ assert ! ( regions. iter( ) . all( |& ( start, _) | start. 0 >= offset as u64 ) ) ;
233262
234- let ( GuestAddress ( start ) , actual_len ) = regions [ 0 ] ;
235- let actual_len = actual_len as u64 ;
263+ // All regions have non-zero length
264+ assert ! ( regions . iter ( ) . all ( | & ( _ , len ) | len > 0 ) ) ;
236265
237- assert_eq ! ( start , layout :: DRAM_MEM_START + offset ) ;
238- assert ! ( actual_len <= layout :: DRAM_MEM_MAX_SIZE as u64 ) ;
239- assert ! ( actual_len <= len ) ;
266+ // If there's two regions, they perfectly snuggle up the 64bit MMIO gap
267+ if regions . len ( ) == 2 {
268+ kani :: cover! ( ) ;
240269
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 ) ;
270+ assert_eq ! ( regions[ 0 ] . 0.0 + regions[ 0 ] . 1 as u64 , MMIO32_MEM_START ) ;
271+ assert_eq ! ( regions[ 1 ] . 0.0 , FIRST_ADDR_PAST_64BITS_MMIO ) ;
247272 }
248273 }
249274}
250275
251276#[ cfg( test) ]
252277mod tests {
253278 use super :: * ;
279+ use crate :: arch:: aarch64:: layout:: {
280+ DRAM_MEM_MAX_SIZE , DRAM_MEM_START , FDT_MAX_SIZE , FIRST_ADDR_PAST_64BITS_MMIO ,
281+ MMIO64_MEM_START ,
282+ } ;
254283 use crate :: test_utils:: arch_mem;
255284
256285 #[ test]
257286 fn test_regions_lt_1024gb ( ) {
258287 let regions = arch_memory_regions ( 0 , 1usize << 29 ) ;
259288 assert_eq ! ( 1 , regions. len( ) ) ;
260- assert_eq ! ( GuestAddress ( super :: layout :: DRAM_MEM_START ) , regions[ 0 ] . 0 ) ;
289+ assert_eq ! ( GuestAddress ( DRAM_MEM_START ) , regions[ 0 ] . 0 ) ;
261290 assert_eq ! ( 1usize << 29 , regions[ 0 ] . 1 ) ;
262291 }
263292
264293 #[ test]
265294 fn test_regions_gt_1024gb ( ) {
266295 let regions = arch_memory_regions ( 0 , 1usize << 41 ) ;
267- assert_eq ! ( 1 , regions. len( ) ) ;
268- assert_eq ! ( GuestAddress ( super :: layout:: DRAM_MEM_START ) , regions[ 0 ] . 0 ) ;
269- assert_eq ! ( super :: layout:: DRAM_MEM_MAX_SIZE , regions[ 0 ] . 1 ) ;
296+ assert_eq ! ( 2 , regions. len( ) ) ;
297+ assert_eq ! ( GuestAddress ( DRAM_MEM_START ) , regions[ 0 ] . 0 ) ;
298+ assert_eq ! ( MMIO64_MEM_START - DRAM_MEM_START , regions[ 0 ] . 1 as u64 ) ;
299+ assert_eq ! ( GuestAddress ( FIRST_ADDR_PAST_64BITS_MMIO ) , regions[ 1 ] . 0 ) ;
300+ assert_eq ! (
301+ DRAM_MEM_MAX_SIZE as u64 - MMIO64_MEM_START + DRAM_MEM_START ,
302+ regions[ 1 ] . 1 as u64
303+ ) ;
270304 }
271305
272306 #[ test]
273307 fn test_get_fdt_addr ( ) {
274- let mem = arch_mem ( layout :: FDT_MAX_SIZE - 0x1000 ) ;
275- assert_eq ! ( get_fdt_addr( & mem) , layout :: DRAM_MEM_START ) ;
308+ let mem = arch_mem ( FDT_MAX_SIZE - 0x1000 ) ;
309+ assert_eq ! ( get_fdt_addr( & mem) , DRAM_MEM_START ) ;
276310
277- let mem = arch_mem ( layout :: FDT_MAX_SIZE ) ;
278- assert_eq ! ( get_fdt_addr( & mem) , layout :: DRAM_MEM_START ) ;
311+ let mem = arch_mem ( FDT_MAX_SIZE ) ;
312+ assert_eq ! ( get_fdt_addr( & mem) , DRAM_MEM_START ) ;
279313
280- let mem = arch_mem ( layout :: FDT_MAX_SIZE + 0x1000 ) ;
281- assert_eq ! ( get_fdt_addr( & mem) , 0x1000 + layout :: DRAM_MEM_START ) ;
314+ let mem = arch_mem ( FDT_MAX_SIZE + 0x1000 ) ;
315+ assert_eq ! ( get_fdt_addr( & mem) , 0x1000 + DRAM_MEM_START ) ;
282316 }
283317}
0 commit comments