@@ -24,11 +24,11 @@ use linux_loader::loader::pe::PE as Loader;
24
24
use linux_loader:: loader:: { Cmdline , KernelLoader } ;
25
25
use vm_memory:: GuestMemoryError ;
26
26
27
- use crate :: arch:: { BootProtocol , EntryPoint } ;
27
+ use crate :: arch:: { BootProtocol , EntryPoint , arch_memory_regions_with_gap } ;
28
28
use crate :: cpu_config:: aarch64:: { CpuConfiguration , CpuConfigurationError } ;
29
29
use crate :: cpu_config:: templates:: CustomCpuTemplate ;
30
30
use crate :: initrd:: InitrdConfig ;
31
- use crate :: utils:: { align_up, usize_to_u64} ;
31
+ use crate :: utils:: { align_up, u64_to_usize , usize_to_u64} ;
32
32
use crate :: vmm_config:: machine_config:: MachineConfig ;
33
33
use crate :: vstate:: memory:: { Address , Bytes , GuestAddress , GuestMemory , GuestMemoryMmap } ;
34
34
use crate :: vstate:: vcpu:: KvmVcpuError ;
@@ -51,42 +51,34 @@ pub enum ConfigurationError {
51
51
VcpuConfigure ( #[ from] KvmVcpuError ) ,
52
52
}
53
53
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
-
59
54
/// Returns a Vec of the valid memory addresses for aarch64.
60
55
/// 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 ) > {
64
57
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
- ) ;
73
58
74
- let dram_size = min ( size, layout:: DRAM_MEM_MAX_SIZE - offset ) ;
59
+ let dram_size = min ( size, layout:: DRAM_MEM_MAX_SIZE ) ;
75
60
76
61
if dram_size != size {
77
62
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 {}",
81
65
size,
82
66
dram_size
83
67
) ;
84
68
}
85
69
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 ) ,
88
74
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
90
82
}
91
83
92
84
/// Configures the system for booting Linux.
@@ -211,73 +203,109 @@ pub fn load_kernel(
211
203
212
204
#[ cfg( kani) ]
213
205
mod 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
+ } ;
217
209
use crate :: arch:: arch_memory_regions;
218
210
219
211
#[ kani:: proof]
220
212
#[ kani:: unwind( 3 ) ]
221
213
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 > ( ) ;
225
215
kani:: assume ( len > 0 ) ;
226
- kani:: assume ( offset. checked_add ( len) . is_some ( ) ) ;
227
- kani:: assume ( offset < layout:: DRAM_MEM_MAX_SIZE as u64 ) ;
228
216
229
- let regions = arch_memory_regions ( offset as usize , len as usize ) ;
217
+ let regions = arch_memory_regions ( len) ;
230
218
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
+ }
233
226
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 ) ;
236
231
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
239
236
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
+ }
240
241
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 ) ;
247
266
}
248
267
}
249
268
}
250
269
251
270
#[ cfg( test) ]
252
271
mod tests {
253
272
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
+ } ;
254
277
use crate :: test_utils:: arch_mem;
255
278
256
279
#[ test]
257
280
fn test_regions_lt_1024gb ( ) {
258
- let regions = arch_memory_regions ( 0 , 1usize << 29 ) ;
281
+ let regions = arch_memory_regions ( 1usize << 29 ) ;
259
282
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 ) ;
261
284
assert_eq ! ( 1usize << 29 , regions[ 0 ] . 1 ) ;
262
285
}
263
286
264
287
#[ test]
265
288
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
+ ) ;
270
298
}
271
299
272
300
#[ test]
273
301
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 ) ;
276
304
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 ) ;
279
307
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 ) ;
282
310
}
283
311
}
0 commit comments