@@ -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