@@ -10,11 +10,10 @@ use std::num::Wrapping;
10
10
use std:: sync:: atomic:: { fence, Ordering } ;
11
11
12
12
use utils:: usize_to_u64;
13
- use vm_memory:: bitmap:: Bitmap ;
14
13
15
14
use crate :: logger:: error;
16
15
use crate :: vstate:: memory:: {
17
- Address , ByteValued , Bytes , GuestAddress , GuestMemory , GuestMemoryMmap ,
16
+ Address , Bitmap , ByteValued , Bytes , GuestAddress , GuestMemory , GuestMemoryMmap ,
18
17
} ;
19
18
20
19
pub const VIRTQ_DESC_F_NEXT : u16 = 0x1 ;
@@ -659,29 +658,6 @@ impl Queue {
659
658
Ok ( ( ) )
660
659
}
661
660
662
- /// Helper method that writes to the `avail_event` field of the used ring.
663
- #[ inline( always) ]
664
- fn set_used_ring_avail_event < M : GuestMemory > ( & mut self , avail_event : u16 , mem : & M ) {
665
- debug_assert ! ( self . is_valid( mem) ) ;
666
-
667
- // Used ring has layout:
668
- // struct UsedRing {
669
- // flags: u16,
670
- // idx: u16,
671
- // ring: [UsedElement; <queue size>],
672
- // avail_event: u16,
673
- // }
674
- // We calculate offset into `avail_event` field.
675
- let avail_event_offset = std:: mem:: size_of :: < u16 > ( )
676
- + std:: mem:: size_of :: < u16 > ( )
677
- + std:: mem:: size_of :: < UsedElement > ( ) * usize:: from ( self . actual_size ( ) ) ;
678
- let avail_event_addr = self
679
- . used_ring_address
680
- . unchecked_add ( usize_to_u64 ( avail_event_offset) ) ;
681
-
682
- mem. write_obj ( avail_event, avail_event_addr) . unwrap ( ) ;
683
- }
684
-
685
661
/// Try to enable notification events from the guest driver. Returns true if notifications were
686
662
/// successfully enabled. Otherwise it means that one or more descriptors can still be consumed
687
663
/// from the available ring and we can't guarantee that there will be a notification. In this
@@ -714,9 +690,9 @@ impl Queue {
714
690
}
715
691
716
692
// Set the next expected avail_idx as avail_event.
717
- self . set_used_ring_avail_event ( self . next_avail . 0 , mem ) ;
693
+ self . used_ring_avail_event_set ( self . next_avail . 0 ) ;
718
694
719
- // Make sure all subsequent reads are performed after `set_used_ring_avail_event` .
695
+ // Make sure all subsequent reads are performed after we set avail_event .
720
696
fence ( Ordering :: SeqCst ) ;
721
697
722
698
// If the actual avail_idx is different than next_avail one or more descriptors can still
@@ -1021,22 +997,6 @@ mod verification {
1021
997
}
1022
998
}
1023
999
1024
- mod stubs {
1025
- use super :: * ;
1026
-
1027
- // Calls to set_used_ring_address_avail_event tend to cause memory to grow unboundedly
1028
- // during verification. The function writes to the `avail_event` of the virtio
1029
- // queue, which is not read from by the device. It is only intended to be used by
1030
- // guest. Therefore, it does not affect any device functionality (e.g. its only call
1031
- // site, try_enable_notification, will behave independently of what value was
1032
- // written here). Thus we can stub it out with a no-op. Note that we have a separate
1033
- // harness for set_used_ring_address_avail_event, to ensure the function itself is
1034
- // sound.
1035
- fn set_used_ring_avail_event < M : GuestMemory > ( _self : & mut Queue , _val : u16 , _mem : & M ) {
1036
- // do nothing
1037
- }
1038
- }
1039
-
1040
1000
#[ kani:: proof]
1041
1001
#[ kani:: unwind( 0 ) ] // There are no loops anywhere, but kani really enjoys getting stuck in std::ptr::drop_in_place.
1042
1002
// This is a compiler intrinsic that has a "dummy" implementation in stdlib that just
@@ -1168,9 +1128,9 @@ mod verification {
1168
1128
#[ kani:: proof]
1169
1129
#[ kani:: unwind( 0 ) ]
1170
1130
fn verify_set_used_ring_avail_event ( ) {
1171
- let ProofContext ( mut queue, mem ) = ProofContext :: bounded_queue ( ) ;
1131
+ let ProofContext ( mut queue, _ ) = ProofContext :: bounded_queue ( ) ;
1172
1132
1173
- queue. set_used_ring_avail_event ( kani:: any ( ) , & mem ) ;
1133
+ queue. used_ring_avail_event_set ( kani:: any ( ) ) ;
1174
1134
}
1175
1135
1176
1136
#[ kani:: proof]
@@ -1216,7 +1176,6 @@ mod verification {
1216
1176
1217
1177
#[ kani:: proof]
1218
1178
#[ kani:: unwind( 0 ) ]
1219
- #[ kani:: stub( Queue :: set_used_ring_avail_event, stubs:: set_used_ring_avail_event) ]
1220
1179
fn verify_try_enable_notification ( ) {
1221
1180
let ProofContext ( mut queue, mem) = ProofContext :: bounded_queue ( ) ;
1222
1181
@@ -1606,10 +1565,10 @@ mod tests {
1606
1565
let mut q = vq. create_queue ( ) ;
1607
1566
assert_eq ! ( vq. used. event. get( ) , 0 ) ;
1608
1567
1609
- q. set_used_ring_avail_event ( 10 , m ) ;
1568
+ q. used_ring_avail_event_set ( 10 ) ;
1610
1569
assert_eq ! ( vq. used. event. get( ) , 10 ) ;
1611
1570
1612
- q. set_used_ring_avail_event ( u16:: MAX , m ) ;
1571
+ q. used_ring_avail_event_set ( u16:: MAX ) ;
1613
1572
assert_eq ! ( vq. used. event. get( ) , u16 :: MAX ) ;
1614
1573
}
1615
1574
0 commit comments