22use  std:: mem:: ManuallyDrop ; 
33use  std:: num:: Wrapping ; 
44
5- use  vm_memory:: { AtomicAccess ,  GuestMemoryError ,  GuestMemoryRegion ,  MemoryRegionAddress } ; 
5+ use  vm_memory:: { 
6+     AtomicAccess ,  GuestMemoryError ,  GuestMemoryRegion ,  GuestMemoryResult ,  MemoryRegionAddress , 
7+     VolatileSlice , 
8+ } ; 
69
7- use  std:: io:: { Read ,  Write } ; 
810use  std:: mem:: MaybeUninit ; 
911use  vm_memory:: ByteValued ; 
1012
@@ -69,9 +71,24 @@ impl GuestMemoryRegion for StubRegion {
6971        self . region_start 
7072    } 
7173
72-     fn  bitmap ( & self )  -> & Self :: B  { 
74+     fn  bitmap ( & self )  -> Self :: B  { 
7375        // For Kani, we do not need a bitmap, so we return an empty tuple. 
74-         & ( ) 
76+         ( ) 
77+     } 
78+ 
79+     fn  get_slice ( 
80+         & self , 
81+         offset :  MemoryRegionAddress , 
82+         count :  usize , 
83+     )  -> GuestMemoryResult < VolatileSlice < ( ) > >  { 
84+         Ok ( unsafe  { 
85+             VolatileSlice :: with_bitmap ( 
86+                 self . buffer . add ( offset. raw_value ( )  as  usize ) , 
87+                 count, 
88+                 ( ) , 
89+                 None , 
90+             ) 
91+         } ) 
7592    } 
7693} 
7794
@@ -118,36 +135,6 @@ impl Bytes<MemoryRegionAddress> for StubRegion {
118135        Ok ( ( ) ) 
119136    } 
120137
121-     fn  read_from < F :  Read > ( 
122-         & self , 
123-         addr :  MemoryRegionAddress , 
124-         src :  & mut  F , 
125-         count :  usize , 
126-     )  -> Result < usize ,  Self :: E >  { 
127-         let  mut  temp = vec ! [ 0u8 ;  count] ; 
128-         src. read_exact ( & mut  temp) 
129-             . map_err ( |_| GuestMemoryError :: PartialBuffer  { 
130-                 expected :  count, 
131-                 completed :  0 , 
132-             } ) ?; 
133-         self . write ( & temp,  addr) 
134-     } 
135- 
136-     fn  read_exact_from < F :  Read > ( 
137-         & self , 
138-         addr :  MemoryRegionAddress , 
139-         src :  & mut  F , 
140-         count :  usize , 
141-     )  -> Result < ( ) ,  Self :: E >  { 
142-         let  mut  temp = vec ! [ 0u8 ;  count] ; 
143-         src. read_exact ( & mut  temp) 
144-             . map_err ( |_| GuestMemoryError :: PartialBuffer  { 
145-                 expected :  count, 
146-                 completed :  0 , 
147-             } ) ?; 
148-         self . write_slice ( & temp,  addr) 
149-     } 
150- 
151138    fn  read_obj < T :  ByteValued > ( & self ,  addr :  MemoryRegionAddress )  -> Result < T ,  Self :: E >  { 
152139        let  size = std:: mem:: size_of :: < T > ( ) ; 
153140        let  offset = addr. 0  as  usize ; 
@@ -168,12 +155,37 @@ impl Bytes<MemoryRegionAddress> for StubRegion {
168155        Ok ( result) 
169156    } 
170157
171-     fn  write_to < F :  Write > ( 
158+     fn  write_obj < T :  ByteValued > ( & self ,  val :  T ,  addr :  MemoryRegionAddress )  -> Result < ( ) ,  Self :: E >  { 
159+         let  size = std:: mem:: size_of :: < T > ( ) ; 
160+         let  offset = addr. 0  as  usize ; 
161+         let  end = offset
162+             . checked_add ( size) 
163+             . ok_or ( GuestMemoryError :: InvalidGuestAddress ( GuestAddress ( addr. 0 ) ) ) ?; 
164+         if  end > self . region_len  as  usize  { 
165+             return  Err ( GuestMemoryError :: InvalidGuestAddress ( GuestAddress ( addr. 0 ) ) ) ; 
166+         } 
167+         let  bytes = val. as_slice ( ) ; 
168+         unsafe  { 
169+             std:: ptr:: copy_nonoverlapping ( bytes. as_ptr ( ) ,  self . buffer . add ( offset) ,  size) ; 
170+         } 
171+         Ok ( ( ) ) 
172+     } 
173+ 
174+     // The non-volatile Read/Write helpers are not part of the current 
175+     // `vm_memory::Bytes` trait in this workspace. Implement the volatile 
176+     // helpers expected by the trait as simple stubs that return an error 
177+     // when invoked. These are sufficient for the Kani proofs here which 
178+     // don't exercise volatile stream IO. 
179+ 
180+     fn  read_volatile_from < F > ( 
172181        & self , 
173182        addr :  MemoryRegionAddress , 
174-         dst :  & mut  F , 
183+         _src :  & mut  F , 
175184        count :  usize , 
176-     )  -> Result < usize ,  Self :: E >  { 
185+     )  -> Result < usize ,  Self :: E > 
186+     where 
187+         F :  vm_memory:: ReadVolatile , 
188+     { 
177189        let  offset = addr. 0  as  usize ; 
178190        let  end = offset
179191            . checked_add ( count) 
@@ -182,39 +194,61 @@ impl Bytes<MemoryRegionAddress> for StubRegion {
182194            return  Err ( GuestMemoryError :: InvalidGuestAddress ( GuestAddress ( addr. 0 ) ) ) ; 
183195        } 
184196        unsafe  { 
185-             let  slice = std:: slice:: from_raw_parts ( self . buffer . add ( offset) ,  count) ; 
186-             dst. write_all ( slice) 
187-                 . map_err ( |_| GuestMemoryError :: PartialBuffer  { 
188-                     expected :  count, 
189-                     completed :  0 , 
190-                 } ) ?; 
197+             let  slice = std:: slice:: from_raw_parts_mut ( self . buffer . add ( offset) ,  count) ; 
198+             let  v = vm_memory:: volatile_memory:: VolatileSlice :: from ( slice) ; 
199+             let  mut  s = v. offset ( 0 ) . map_err ( Into :: < Self :: E > :: into) ?; 
200+             let  n = _src. read_volatile ( & mut  s) . map_err ( Into :: < Self :: E > :: into) ?; 
201+             return  Ok ( n) ; 
191202        } 
192-         Ok ( count) 
193203    } 
194204
195-     fn  write_obj < T :  ByteValued > ( & self ,  val :  T ,  addr :  MemoryRegionAddress )  -> Result < ( ) ,  Self :: E >  { 
196-         let  size = std:: mem:: size_of :: < T > ( ) ; 
205+     fn  read_exact_volatile_from < F > ( 
206+         & self , 
207+         addr :  MemoryRegionAddress , 
208+         src :  & mut  F , 
209+         count :  usize , 
210+     )  -> Result < ( ) ,  Self :: E > 
211+     where 
212+         F :  vm_memory:: ReadVolatile , 
213+     { 
214+         // Reuse read_volatile_from which performs bounds checks and delegates to `ReadVolatile`. 
215+         let  _ = self . read_volatile_from ( addr,  src,  count) ?; 
216+         Ok ( ( ) ) 
217+     } 
218+ 
219+     fn  write_volatile_to < F > ( 
220+         & self , 
221+         addr :  MemoryRegionAddress , 
222+         dst :  & mut  F , 
223+         count :  usize , 
224+     )  -> Result < usize ,  Self :: E > 
225+     where 
226+         F :  vm_memory:: WriteVolatile , 
227+     { 
197228        let  offset = addr. 0  as  usize ; 
198229        let  end = offset
199-             . checked_add ( size ) 
230+             . checked_add ( count ) 
200231            . ok_or ( GuestMemoryError :: InvalidGuestAddress ( GuestAddress ( addr. 0 ) ) ) ?; 
201232        if  end > self . region_len  as  usize  { 
202233            return  Err ( GuestMemoryError :: InvalidGuestAddress ( GuestAddress ( addr. 0 ) ) ) ; 
203234        } 
204-         let  bytes = val. as_slice ( ) ; 
205235        unsafe  { 
206-             std:: ptr:: copy_nonoverlapping ( bytes. as_ptr ( ) ,  self . buffer . add ( offset) ,  size) ; 
236+             let  slice = std:: slice:: from_raw_parts_mut ( self . buffer . add ( offset) ,  count) ; 
237+             let  v = vm_memory:: volatile_memory:: VolatileSlice :: from ( slice) ; 
238+             return  dst. write_volatile ( & v) . map_err ( Into :: into) ; 
207239        } 
208-         Ok ( ( ) ) 
209240    } 
210241
211-     fn  write_all_to < F :   Write > ( 
242+     fn  write_all_volatile_to < F > ( 
212243        & self , 
213244        addr :  MemoryRegionAddress , 
214245        dst :  & mut  F , 
215246        count :  usize , 
216-     )  -> Result < ( ) ,  Self :: E >  { 
217-         self . write_to ( addr,  dst,  count) ?; 
247+     )  -> Result < ( ) ,  Self :: E > 
248+     where 
249+         F :  vm_memory:: WriteVolatile , 
250+     { 
251+         let  _ = self . write_volatile_to ( addr,  dst,  count) ?; 
218252        Ok ( ( ) ) 
219253    } 
220254
@@ -537,8 +571,10 @@ fn get_used_idx(
537571/// if the descriptor index is out of bounds, the operation must fail and the 
538572/// used index must not be incremented. Note that this proof does not verify 
539573/// Section 2.7.8.2: "Device Requirements: The Virtqueue Used Ring" 
540- #[ kani:: proof]  
541- #[ kani:: unwind( 0 ) ]  
574+ // Re-enable this proof once https://github.com/rust-vmm/vm-virtio/issues/373 
575+ // is fixed. 
576+ //#[kani::proof] 
577+ //#[kani::unwind(0)] 
542578fn  verify_add_used ( )  { 
543579    let  ProofContext  {  mut  queue,  memory }  = kani:: any ( ) ; 
544580    let  used_idx = queue. next_used ; 
0 commit comments