@@ -11,6 +11,7 @@ use vm_memory::{
1111} ;
1212
1313use super :: iov_deque:: { IovDeque , IovDequeError } ;
14+ use super :: queue:: FIRECRACKER_MAX_QUEUE_SIZE ;
1415use crate :: devices:: virtio:: queue:: DescriptorChain ;
1516use crate :: vstate:: memory:: GuestMemoryMmap ;
1617
@@ -223,10 +224,11 @@ pub struct ParsedDescriptorChain {
223224/// It describes a write-only buffer passed to us by the guest that is scattered across multiple
224225/// memory regions. Additionally, this wrapper provides methods that allow reading arbitrary ranges
225226/// of data from that buffer.
227+ /// `L` const generic value must be a multiple of 256 as required by the `IovDeque` requirements.
226228#[ derive( Debug ) ]
227- pub struct IoVecBufferMut {
229+ pub struct IoVecBufferMut < const L : u16 = FIRECRACKER_MAX_QUEUE_SIZE > {
228230 // container of the memory regions included in this IO vector
229- pub vecs : IovDeque ,
231+ pub vecs : IovDeque < L > ,
230232 // Total length of the IoVecBufferMut
231233 // We use `u32` here because we use this type in devices which
232234 // should not give us huge buffers. In any case this
@@ -236,9 +238,9 @@ pub struct IoVecBufferMut {
236238
237239// SAFETY: `IoVecBufferMut` doesn't allow for interior mutability and no shared ownership is
238240// possible as it doesn't implement clone
239- unsafe impl Send for IoVecBufferMut { }
241+ unsafe impl < const L : u16 > Send for IoVecBufferMut < L > { }
240242
241- impl IoVecBufferMut {
243+ impl < const L : u16 > IoVecBufferMut < L > {
242244 /// Append a `DescriptorChain` in this `IoVecBufferMut`
243245 ///
244246 /// # Safety
@@ -477,7 +479,11 @@ mod tests {
477479 use libc:: { c_void, iovec} ;
478480 use vm_memory:: VolatileMemoryError ;
479481
480- use super :: { IoVecBuffer , IoVecBufferMut } ;
482+ use super :: IoVecBuffer ;
483+ // Redefine `IoVecBufferMut` with specific length. Otherwise
484+ // Rust will not know what to do.
485+ type IoVecBufferMut = super :: IoVecBufferMut < 256 > ;
486+
481487 use crate :: devices:: virtio:: iov_deque:: IovDeque ;
482488 use crate :: devices:: virtio:: queue:: { Queue , VIRTQ_DESC_F_NEXT , VIRTQ_DESC_F_WRITE } ;
483489 use crate :: devices:: virtio:: test_utils:: VirtQueue ;
@@ -514,7 +520,7 @@ mod tests {
514520 }
515521 }
516522
517- impl From < & mut [ u8 ] > for IoVecBufferMut {
523+ impl < const L : u16 > From < & mut [ u8 ] > for super :: IoVecBufferMut < L > {
518524 fn from ( buf : & mut [ u8 ] ) -> Self {
519525 let mut vecs = IovDeque :: new ( ) . unwrap ( ) ;
520526 vecs. push_back ( iovec {
@@ -529,7 +535,7 @@ mod tests {
529535 }
530536 }
531537
532- impl From < Vec < & mut [ u8 ] > > for IoVecBufferMut {
538+ impl < const L : u16 > From < Vec < & mut [ u8 ] > > for super :: IoVecBufferMut < L > {
533539 fn from ( buffer : Vec < & mut [ u8 ] > ) -> Self {
534540 let mut len = 0 ;
535541 let mut vecs = IovDeque :: new ( ) . unwrap ( ) ;
@@ -804,9 +810,14 @@ mod verification {
804810 use vm_memory:: bitmap:: BitmapSlice ;
805811 use vm_memory:: VolatileSlice ;
806812
807- use super :: { IoVecBuffer , IoVecBufferMut } ;
808- use crate :: arch:: PAGE_SIZE ;
813+ use super :: IoVecBuffer ;
809814 use crate :: devices:: virtio:: iov_deque:: IovDeque ;
815+ // Redefine `IoVecBufferMut` and `IovDeque` with specific length. Otherwise
816+ // Rust will not know what to do.
817+ type IoVecBufferMut256 = super :: IoVecBufferMut < 256 > ;
818+ type IovDeque256 = IovDeque < 256 > ;
819+
820+ use crate :: arch:: PAGE_SIZE ;
810821 use crate :: devices:: virtio:: queue:: FIRECRACKER_MAX_QUEUE_SIZE ;
811822
812823 // Maximum memory size to use for our buffers. For the time being 1KB.
@@ -837,7 +848,7 @@ mod verification {
837848 ///
838849 /// This stub helps imitate the effect of mirroring without all the elaborate memory
839850 /// allocation trick.
840- pub fn push_back ( deque : & mut IovDeque , iov : iovec ) {
851+ pub fn push_back < const L : u16 > ( deque : & mut IovDeque < L > , iov : iovec ) {
841852 // This should NEVER happen, since our ring buffer is as big as the maximum queue size.
842853 // We also check for the sanity of the VirtIO queues, in queue.rs, which means that if
843854 // we ever try to add something in a full ring buffer, there is an internal
@@ -893,22 +904,22 @@ mod verification {
893904 }
894905 }
895906
896- fn create_iov_deque ( ) -> IovDeque {
907+ fn create_iov_deque ( ) -> IovDeque256 {
897908 // SAFETY: safe because the layout has non-zero size
898909 let mem = unsafe {
899910 std:: alloc:: alloc ( std:: alloc:: Layout :: from_size_align_unchecked (
900911 2 * PAGE_SIZE ,
901912 PAGE_SIZE ,
902913 ) )
903914 } ;
904- IovDeque {
915+ IovDeque256 {
905916 iov : mem. cast ( ) ,
906917 start : kani:: any_where ( |& start| start < FIRECRACKER_MAX_QUEUE_SIZE ) ,
907918 len : 0 ,
908919 }
909920 }
910921
911- fn create_iovecs_mut ( mem : * mut u8 , size : usize , nr_descs : usize ) -> ( IovDeque , u32 ) {
922+ fn create_iovecs_mut ( mem : * mut u8 , size : usize , nr_descs : usize ) -> ( IovDeque256 , u32 ) {
912923 let mut vecs = create_iov_deque ( ) ;
913924 let mut len = 0u32 ;
914925 for _ in 0 ..nr_descs {
@@ -928,7 +939,7 @@ mod verification {
928939 ( vecs, len)
929940 }
930941
931- impl IoVecBufferMut {
942+ impl IoVecBufferMut256 {
932943 fn any_of_length ( nr_descs : usize ) -> Self {
933944 // We only write into `IoVecBufferMut` objects, so we can simply create a guest memory
934945 // object initialized to zeroes, trying to be nice to Kani.
@@ -1018,10 +1029,12 @@ mod verification {
10181029 #[ kani:: proof]
10191030 #[ kani:: unwind( 5 ) ]
10201031 #[ 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.
10211034 #[ kani:: stub( IovDeque :: push_back, stubs:: push_back) ]
10221035 fn verify_write_to_iovec ( ) {
10231036 for nr_descs in 0 ..MAX_DESC_LENGTH {
1024- let mut iov_mut = IoVecBufferMut :: any_of_length ( nr_descs) ;
1037+ let mut iov_mut = IoVecBufferMut256 :: any_of_length ( nr_descs) ;
10251038
10261039 let mut buf = kani:: vec:: any_vec :: < u8 , GUEST_MEMORY_SIZE > ( ) ;
10271040 let offset: u32 = kani:: any ( ) ;
0 commit comments