@@ -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,42 +51,34 @@ 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.
61- ///
62- /// The `offset` parameter specified the offset from [`layout::DRAM_MEM_START`].
63- pub fn arch_memory_regions ( offset : usize , size : usize ) -> Vec < ( GuestAddress , usize ) > {
56+ pub fn arch_memory_regions ( size : usize ) -> Vec < ( GuestAddress , usize ) > {
6457 assert ! ( size > 0 , "Attempt to allocate guest memory of length 0" ) ;
65- assert ! (
66- offset. checked_add( size) . is_some( ) ,
67- "Attempt to allocate guest memory such that the address space would wrap around"
68- ) ;
69- assert ! (
70- offset < layout:: DRAM_MEM_MAX_SIZE ,
71- "offset outside allowed DRAM range"
72- ) ;
7358
74- let dram_size = min ( size, layout:: DRAM_MEM_MAX_SIZE - offset ) ;
59+ let dram_size = min ( size, layout:: DRAM_MEM_MAX_SIZE ) ;
7560
7661 if dram_size != size {
7762 logger:: warn!(
78- "Requested offset/memory size {}/{} exceeds architectural maximum (1022GiB). Size has \
79- been truncated to {}",
80- offset,
63+ "Requested memory size {} exceeds architectural maximum (1022GiB). Size has been \
64+ truncated to {}",
8165 size,
8266 dram_size
8367 ) ;
8468 }
8569
86- vec ! [ (
87- GuestAddress ( layout:: DRAM_MEM_START + offset as u64 ) ,
70+ let mut regions = vec ! [ ] ;
71+ if let Some ( ( offset, remaining) ) = arch_memory_regions_with_gap (
72+ & mut regions,
73+ u64_to_usize ( layout:: DRAM_MEM_START ) ,
8874 dram_size,
89- ) ]
75+ u64_to_usize ( layout:: MMIO64_MEM_START ) ,
76+ u64_to_usize ( layout:: MMIO64_MEM_SIZE ) ,
77+ ) {
78+ regions. push ( ( GuestAddress ( offset as u64 ) , remaining) ) ;
79+ }
80+
81+ regions
9082}
9183
9284/// Configures the system for booting Linux.
@@ -211,73 +203,109 @@ pub fn load_kernel(
211203
212204#[ cfg( kani) ]
213205mod verification {
214- use vm_memory :: GuestAddress ;
215-
216- use crate :: arch :: aarch64 :: layout ;
206+ use crate :: arch :: aarch64 :: layout :: {
207+ DRAM_MEM_MAX_SIZE , DRAM_MEM_START , FIRST_ADDR_PAST_64BITS_MMIO , MMIO64_MEM_START ,
208+ } ;
217209 use crate :: arch:: arch_memory_regions;
218210
219211 #[ kani:: proof]
220212 #[ kani:: unwind( 3 ) ]
221213 fn verify_arch_memory_regions ( ) {
222- let offset: u64 = kani:: any :: < u64 > ( ) ;
223- let len: u64 = kani:: any :: < u64 > ( ) ;
224-
214+ let len: usize = kani:: any :: < usize > ( ) ;
225215 kani:: assume ( len > 0 ) ;
226- kani:: assume ( offset. checked_add ( len) . is_some ( ) ) ;
227- kani:: assume ( offset < layout:: DRAM_MEM_MAX_SIZE as u64 ) ;
228216
229- let regions = arch_memory_regions ( offset as usize , len as usize ) ;
217+ let regions = arch_memory_regions ( len) ;
230218
231- // No MMIO gap on ARM
232- assert_eq ! ( regions. len( ) , 1 ) ;
219+ for region in & regions {
220+ println ! (
221+ "region: [{:x}:{:x})" ,
222+ region. 0.0 ,
223+ region. 0.0 + region. 1 as u64
224+ ) ;
225+ }
233226
234- let ( GuestAddress ( start) , actual_len) = regions[ 0 ] ;
235- let actual_len = actual_len as u64 ;
227+ // On Arm we have one MMIO gap that might fall within addressable ranges,
228+ // so we can get either 1 or 2 regions.
229+ assert ! ( regions. len( ) >= 1 ) ;
230+ assert ! ( regions. len( ) <= 2 ) ;
236231
237- assert_eq ! ( start, layout:: DRAM_MEM_START + offset) ;
238- assert ! ( actual_len <= layout:: DRAM_MEM_MAX_SIZE as u64 ) ;
232+ // The total length of all regions cannot exceed DRAM_MEM_MAX_SIZE
233+ let actual_len = regions. iter ( ) . map ( |& ( _, len) | len) . sum :: < usize > ( ) ;
234+ assert ! ( actual_len <= DRAM_MEM_MAX_SIZE ) ;
235+ // The total length is smaller or equal to the length we asked
239236 assert ! ( actual_len <= len) ;
237+ // If it's smaller, it's because we asked more than the the maximum possible.
238+ if ( actual_len) < len {
239+ assert ! ( len > DRAM_MEM_MAX_SIZE ) ;
240+ }
240241
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 ) ;
242+ // No region overlaps the 64-bit MMIO gap
243+ assert ! (
244+ regions
245+ . iter( )
246+ . all( |& ( start, len) | start. 0 >= FIRST_ADDR_PAST_64BITS_MMIO
247+ || start. 0 + len as u64 <= MMIO64_MEM_START )
248+ ) ;
249+
250+ // All regions start after our DRAM_MEM_START
251+ assert ! ( regions. iter( ) . all( |& ( start, _) | start. 0 >= DRAM_MEM_START ) ) ;
252+
253+ // All regions have non-zero length
254+ assert ! ( regions. iter( ) . all( |& ( _, len) | len > 0 ) ) ;
255+
256+ // If there's two regions, they perfectly snuggle up the 64bit MMIO gap
257+ if regions. len ( ) == 2 {
258+ kani:: cover!( ) ;
259+
260+ // The very first address should be DRAM_MEM_START
261+ assert_eq ! ( regions[ 0 ] . 0.0 , DRAM_MEM_START ) ;
262+ // The first region ends at the beginning of the 64 bits gap.
263+ assert_eq ! ( regions[ 0 ] . 0.0 + regions[ 0 ] . 1 as u64 , MMIO64_MEM_START ) ;
264+ // The second region starts exactly after the 64 bits gap.
265+ assert_eq ! ( regions[ 1 ] . 0.0 , FIRST_ADDR_PAST_64BITS_MMIO ) ;
247266 }
248267 }
249268}
250269
251270#[ cfg( test) ]
252271mod tests {
253272 use super :: * ;
273+ use crate :: arch:: aarch64:: layout:: {
274+ DRAM_MEM_MAX_SIZE , DRAM_MEM_START , FDT_MAX_SIZE , FIRST_ADDR_PAST_64BITS_MMIO ,
275+ MMIO64_MEM_START ,
276+ } ;
254277 use crate :: test_utils:: arch_mem;
255278
256279 #[ test]
257280 fn test_regions_lt_1024gb ( ) {
258- let regions = arch_memory_regions ( 0 , 1usize << 29 ) ;
281+ let regions = arch_memory_regions ( 1usize << 29 ) ;
259282 assert_eq ! ( 1 , regions. len( ) ) ;
260- assert_eq ! ( GuestAddress ( super :: layout :: DRAM_MEM_START ) , regions[ 0 ] . 0 ) ;
283+ assert_eq ! ( GuestAddress ( DRAM_MEM_START ) , regions[ 0 ] . 0 ) ;
261284 assert_eq ! ( 1usize << 29 , regions[ 0 ] . 1 ) ;
262285 }
263286
264287 #[ test]
265288 fn test_regions_gt_1024gb ( ) {
266- 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 ) ;
289+ let regions = arch_memory_regions ( 1usize << 41 ) ;
290+ assert_eq ! ( 2 , regions. len( ) ) ;
291+ assert_eq ! ( GuestAddress ( DRAM_MEM_START ) , regions[ 0 ] . 0 ) ;
292+ assert_eq ! ( MMIO64_MEM_START - DRAM_MEM_START , regions[ 0 ] . 1 as u64 ) ;
293+ assert_eq ! ( GuestAddress ( FIRST_ADDR_PAST_64BITS_MMIO ) , regions[ 1 ] . 0 ) ;
294+ assert_eq ! (
295+ DRAM_MEM_MAX_SIZE as u64 - MMIO64_MEM_START + DRAM_MEM_START ,
296+ regions[ 1 ] . 1 as u64
297+ ) ;
270298 }
271299
272300 #[ test]
273301 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 ) ;
302+ let mem = arch_mem ( FDT_MAX_SIZE - 0x1000 ) ;
303+ assert_eq ! ( get_fdt_addr( & mem) , DRAM_MEM_START ) ;
276304
277- let mem = arch_mem ( layout :: FDT_MAX_SIZE ) ;
278- assert_eq ! ( get_fdt_addr( & mem) , layout :: DRAM_MEM_START ) ;
305+ let mem = arch_mem ( FDT_MAX_SIZE ) ;
306+ assert_eq ! ( get_fdt_addr( & mem) , DRAM_MEM_START ) ;
279307
280- let mem = arch_mem ( layout :: FDT_MAX_SIZE + 0x1000 ) ;
281- assert_eq ! ( get_fdt_addr( & mem) , 0x1000 + layout :: DRAM_MEM_START ) ;
308+ let mem = arch_mem ( FDT_MAX_SIZE + 0x1000 ) ;
309+ assert_eq ! ( get_fdt_addr( & mem) , 0x1000 + DRAM_MEM_START ) ;
282310 }
283311}
0 commit comments