55// Use of this source code is governed by a BSD-style license that can be
66// found in the THIRD-PARTY file.
77
8- use std:: cmp:: min;
98use std:: num:: Wrapping ;
109use std:: sync:: atomic:: { Ordering , fence} ;
1110
@@ -462,12 +461,6 @@ impl Queue {
462461 }
463462 }
464463
465- /// Return the actual size of the queue, as the driver may not set up a
466- /// queue as big as the device allows.
467- pub fn actual_size ( & self ) -> u16 {
468- min ( self . size , self . max_size )
469- }
470-
471464 /// Validates the queue's in-memory layout is correct.
472465 pub fn is_valid < M : GuestMemory > ( & self , mem : & M ) -> bool {
473466 let desc_table = self . desc_table_address ;
@@ -548,9 +541,9 @@ impl Queue {
548541 // once. Checking and reporting such incorrect driver behavior
549542 // can prevent potential hanging and Denial-of-Service from
550543 // happening on the VMM side.
551- if len > self . actual_size ( ) {
544+ if self . size < len {
552545 return Err ( InvalidAvailIdx {
553- queue_size : self . actual_size ( ) ,
546+ queue_size : self . size ,
554547 reported_len : len,
555548 } ) ;
556549 }
@@ -602,17 +595,15 @@ impl Queue {
602595 //
603596 // We use `self.next_avail` to store the position, in `ring`, of the next available
604597 // descriptor index, with a twist: we always only increment `self.next_avail`, so the
605- // actual position will be `self.next_avail % self.actual_size() `.
606- let idx = self . next_avail . 0 % self . actual_size ( ) ;
598+ // actual position will be `self.next_avail % self.size `.
599+ let idx = self . next_avail . 0 % self . size ;
607600 // SAFETY:
608601 // index is bound by the queue size
609602 let desc_index = unsafe { self . avail_ring_ring_get ( usize:: from ( idx) ) } ;
610603
611- DescriptorChain :: checked_new ( self . desc_table_ptr , self . actual_size ( ) , desc_index) . inspect (
612- |_| {
613- self . next_avail += Wrapping ( 1 ) ;
614- } ,
615- )
604+ DescriptorChain :: checked_new ( self . desc_table_ptr , self . size , desc_index) . inspect ( |_| {
605+ self . next_avail += Wrapping ( 1 ) ;
606+ } )
616607 }
617608
618609 /// Undo the effects of the last `self.pop()` call.
@@ -630,15 +621,15 @@ impl Queue {
630621 desc_index : u16 ,
631622 len : u32 ,
632623 ) -> Result < ( ) , QueueError > {
633- if self . actual_size ( ) <= desc_index {
624+ if self . size <= desc_index {
634625 error ! (
635626 "attempted to add out of bounds descriptor to used ring: {}" ,
636627 desc_index
637628 ) ;
638629 return Err ( QueueError :: DescIndexOutOfBounds ( desc_index) ) ;
639630 }
640631
641- let next_used = ( self . next_used + Wrapping ( ring_index_offset) ) . 0 % self . actual_size ( ) ;
632+ let next_used = ( self . next_used + Wrapping ( ring_index_offset) ) . 0 % self . size ;
642633 let used_element = UsedElement {
643634 id : u32:: from ( desc_index) ,
644635 len,
@@ -684,9 +675,9 @@ impl Queue {
684675 if len != 0 {
685676 // The number of descriptor chain heads to process should always
686677 // be smaller or equal to the queue size.
687- if len > self . actual_size ( ) {
678+ if len > self . size {
688679 return Err ( InvalidAvailIdx {
689- queue_size : self . actual_size ( ) ,
680+ queue_size : self . size ,
690681 reported_len : len,
691682 } ) ;
692683 }
@@ -1086,7 +1077,7 @@ mod verification {
10861077 // done. This is relying on implementation details of add_used, namely that
10871078 // the check for out-of-bounds descriptor index happens at the very beginning of the
10881079 // function.
1089- assert ! ( used_desc_table_index >= queue. actual_size ( ) ) ;
1080+ assert ! ( used_desc_table_index >= queue. size ) ;
10901081 }
10911082 }
10921083
@@ -1123,11 +1114,11 @@ mod verification {
11231114
11241115 #[ kani:: proof]
11251116 #[ kani:: unwind( 0 ) ]
1126- fn verify_actual_size ( ) {
1117+ fn verify_size ( ) {
11271118 let ProofContext ( queue, _) = kani:: any ( ) ;
11281119
1129- assert ! ( queue. actual_size ( ) <= queue. max_size) ;
1130- assert ! ( queue. actual_size ( ) <= queue. size) ;
1120+ assert ! ( queue. size <= queue. max_size) ;
1121+ assert ! ( queue. size <= queue. size) ;
11311122 }
11321123
11331124 #[ kani:: proof]
@@ -1192,7 +1183,7 @@ mod verification {
11921183 // is called when the queue is being initialized, e.g. empty. We compute it using
11931184 // local variables here to make things easier on kani: One less roundtrip through vm-memory.
11941185 let queue_len = queue. len ( ) ;
1195- kani:: assume ( queue_len <= queue. actual_size ( ) ) ;
1186+ kani:: assume ( queue_len <= queue. size ) ;
11961187
11971188 let next_avail = queue. next_avail ;
11981189
@@ -1210,7 +1201,7 @@ mod verification {
12101201 let ProofContext ( mut queue, _) = kani:: any ( ) ;
12111202
12121203 // See verify_pop for explanation
1213- kani:: assume ( queue. len ( ) <= queue. actual_size ( ) ) ;
1204+ kani:: assume ( queue. len ( ) <= queue. size ) ;
12141205
12151206 let queue_clone = queue. clone ( ) ;
12161207 if let Some ( _) = queue. pop ( ) . unwrap ( ) {
@@ -1226,7 +1217,7 @@ mod verification {
12261217 fn verify_try_enable_notification ( ) {
12271218 let ProofContext ( mut queue, _) = ProofContext :: bounded_queue ( ) ;
12281219
1229- kani:: assume ( queue. len ( ) <= queue. actual_size ( ) ) ;
1220+ kani:: assume ( queue. len ( ) <= queue. size ) ;
12301221
12311222 if queue. try_enable_notification ( ) . unwrap ( ) && queue. uses_notif_suppression {
12321223 // We only require new notifications if the queue is empty (e.g. we've processed
@@ -1244,10 +1235,9 @@ mod verification {
12441235 let ProofContext ( queue, mem) = kani:: any ( ) ;
12451236
12461237 let index = kani:: any ( ) ;
1247- let maybe_chain =
1248- DescriptorChain :: checked_new ( queue. desc_table_ptr , queue. actual_size ( ) , index) ;
1238+ let maybe_chain = DescriptorChain :: checked_new ( queue. desc_table_ptr , queue. size , index) ;
12491239
1250- if index >= queue. actual_size ( ) {
1240+ if index >= queue. size {
12511241 assert ! ( maybe_chain. is_none( ) )
12521242 } else {
12531243 // If the index was in-bounds for the descriptor table, we at least should be
@@ -1262,7 +1252,7 @@ mod verification {
12621252 match maybe_chain {
12631253 None => {
12641254 // This assert is the negation of the "is_valid" check in checked_new
1265- assert ! ( desc. flags & VIRTQ_DESC_F_NEXT == 1 && desc. next >= queue. actual_size ( ) )
1255+ assert ! ( desc. flags & VIRTQ_DESC_F_NEXT == 1 && desc. next >= queue. size )
12661256 }
12671257 Some ( head) => {
12681258 assert ! ( head. is_valid( ) )
0 commit comments