@@ -482,10 +482,12 @@ mod tests {
482
482
use super :: IoVecBuffer ;
483
483
// Redefine `IoVecBufferMut` with specific length. Otherwise
484
484
// Rust will not know what to do.
485
- type IoVecBufferMut = super :: IoVecBufferMut < 256 > ;
485
+ type IoVecBufferMutDefault = super :: IoVecBufferMut < FIRECRACKER_MAX_QUEUE_SIZE > ;
486
486
487
487
use crate :: devices:: virtio:: iov_deque:: IovDeque ;
488
- use crate :: devices:: virtio:: queue:: { Queue , VIRTQ_DESC_F_NEXT , VIRTQ_DESC_F_WRITE } ;
488
+ use crate :: devices:: virtio:: queue:: {
489
+ Queue , FIRECRACKER_MAX_QUEUE_SIZE , VIRTQ_DESC_F_NEXT , VIRTQ_DESC_F_WRITE ,
490
+ } ;
489
491
use crate :: devices:: virtio:: test_utils:: VirtQueue ;
490
492
use crate :: test_utils:: multi_region_mem;
491
493
use crate :: vstate:: memory:: { Bytes , GuestAddress , GuestMemoryMmap } ;
@@ -614,12 +616,12 @@ mod tests {
614
616
let ( mut q, _) = read_only_chain ( & mem) ;
615
617
let head = q. pop ( ) . unwrap ( ) ;
616
618
// SAFETY: This descriptor chain is only loaded into one buffer
617
- unsafe { IoVecBufferMut :: from_descriptor_chain ( & mem, head) . unwrap_err ( ) } ;
619
+ unsafe { IoVecBufferMutDefault :: from_descriptor_chain ( & mem, head) . unwrap_err ( ) } ;
618
620
619
621
let ( mut q, _) = write_only_chain ( & mem) ;
620
622
let head = q. pop ( ) . unwrap ( ) ;
621
623
// SAFETY: This descriptor chain is only loaded into one buffer
622
- unsafe { IoVecBufferMut :: from_descriptor_chain ( & mem, head) . unwrap ( ) } ;
624
+ unsafe { IoVecBufferMutDefault :: from_descriptor_chain ( & mem, head) . unwrap ( ) } ;
623
625
}
624
626
625
627
#[ test]
@@ -640,7 +642,8 @@ mod tests {
640
642
let head = q. pop ( ) . unwrap ( ) ;
641
643
642
644
// SAFETY: This descriptor chain is only loaded once in this test
643
- let mut iovec = unsafe { IoVecBufferMut :: from_descriptor_chain ( & mem, head) . unwrap ( ) } ;
645
+ let mut iovec =
646
+ unsafe { IoVecBufferMutDefault :: from_descriptor_chain ( & mem, head) . unwrap ( ) } ;
644
647
assert_eq ! ( iovec. len( ) , 4 * 64 ) ;
645
648
646
649
// We are creating a new queue where we can get descriptors from. Probably, this is not
@@ -717,7 +720,8 @@ mod tests {
717
720
let head = q. pop ( ) . unwrap ( ) ;
718
721
719
722
// SAFETY: This descriptor chain is only loaded into one buffer
720
- let mut iovec = unsafe { IoVecBufferMut :: from_descriptor_chain ( & mem, head) . unwrap ( ) } ;
723
+ let mut iovec =
724
+ unsafe { IoVecBufferMutDefault :: from_descriptor_chain ( & mem, head) . unwrap ( ) } ;
721
725
let buf = vec ! [ 0u8 , 1 , 2 , 3 , 4 ] ;
722
726
723
727
// One test vector for each part of the chain
@@ -814,8 +818,8 @@ mod verification {
814
818
use crate :: devices:: virtio:: iov_deque:: IovDeque ;
815
819
// Redefine `IoVecBufferMut` and `IovDeque` with specific length. Otherwise
816
820
// Rust will not know what to do.
817
- type IoVecBufferMut256 = super :: IoVecBufferMut < 256 > ;
818
- type IovDeque256 = IovDeque < 256 > ;
821
+ type IoVecBufferMutDefault = super :: IoVecBufferMut < FIRECRACKER_MAX_QUEUE_SIZE > ;
822
+ type IovDequeDefault = IovDeque < FIRECRACKER_MAX_QUEUE_SIZE > ;
819
823
820
824
use crate :: arch:: PAGE_SIZE ;
821
825
use crate :: devices:: virtio:: queue:: FIRECRACKER_MAX_QUEUE_SIZE ;
@@ -860,10 +864,10 @@ mod verification {
860
864
) ;
861
865
862
866
let offset = ( deque. start + deque. len ) as usize ;
863
- let mirror = if offset >= FIRECRACKER_MAX_QUEUE_SIZE as usize {
864
- offset - FIRECRACKER_MAX_QUEUE_SIZE as usize
867
+ let mirror = if offset >= L as usize {
868
+ offset - L as usize
865
869
} else {
866
- offset + FIRECRACKER_MAX_QUEUE_SIZE as usize
870
+ offset + L as usize
867
871
} ;
868
872
869
873
// SAFETY: self.iov is a valid pointer and `self.start + self.len` is within range (we
@@ -904,22 +908,22 @@ mod verification {
904
908
}
905
909
}
906
910
907
- fn create_iov_deque ( ) -> IovDeque256 {
911
+ fn create_iov_deque ( ) -> IovDequeDefault {
908
912
// SAFETY: safe because the layout has non-zero size
909
913
let mem = unsafe {
910
914
std:: alloc:: alloc ( std:: alloc:: Layout :: from_size_align_unchecked (
911
915
2 * PAGE_SIZE ,
912
916
PAGE_SIZE ,
913
917
) )
914
918
} ;
915
- IovDeque256 {
919
+ IovDequeDefault {
916
920
iov : mem. cast ( ) ,
917
921
start : kani:: any_where ( |& start| start < FIRECRACKER_MAX_QUEUE_SIZE ) ,
918
922
len : 0 ,
919
923
}
920
924
}
921
925
922
- fn create_iovecs_mut ( mem : * mut u8 , size : usize , nr_descs : usize ) -> ( IovDeque256 , u32 ) {
926
+ fn create_iovecs_mut ( mem : * mut u8 , size : usize , nr_descs : usize ) -> ( IovDequeDefault , u32 ) {
923
927
let mut vecs = create_iov_deque ( ) ;
924
928
let mut len = 0u32 ;
925
929
for _ in 0 ..nr_descs {
@@ -939,7 +943,7 @@ mod verification {
939
943
( vecs, len)
940
944
}
941
945
942
- impl IoVecBufferMut256 {
946
+ impl IoVecBufferMutDefault {
943
947
fn any_of_length ( nr_descs : usize ) -> Self {
944
948
// We only write into `IoVecBufferMut` objects, so we can simply create a guest memory
945
949
// object initialized to zeroes, trying to be nice to Kani.
@@ -1029,12 +1033,10 @@ mod verification {
1029
1033
#[ kani:: proof]
1030
1034
#[ kani:: unwind( 5 ) ]
1031
1035
#[ kani:: solver( cadical) ]
1032
- // The `IovDeque` is defined as type alias in the kani module. Because of this
1033
- // we need to specify original type here for stub to work.
1034
1036
#[ kani:: stub( IovDeque :: push_back, stubs:: push_back) ]
1035
1037
fn verify_write_to_iovec ( ) {
1036
1038
for nr_descs in 0 ..MAX_DESC_LENGTH {
1037
- let mut iov_mut = IoVecBufferMut256 :: any_of_length ( nr_descs) ;
1039
+ let mut iov_mut = IoVecBufferMutDefault :: any_of_length ( nr_descs) ;
1038
1040
1039
1041
let mut buf = kani:: vec:: any_vec :: < u8 , GUEST_MEMORY_SIZE > ( ) ;
1040
1042
let offset: u32 = kani:: any ( ) ;
0 commit comments