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
@@ -469,12 +468,6 @@ impl Queue {
469468 }
470469 }
471470
472- /// Return the actual size of the queue, as the driver may not set up a
473- /// queue as big as the device allows.
474- pub fn actual_size ( & self ) -> u16 {
475- min ( self . size , self . max_size )
476- }
477-
478471 /// Validates the queue's in-memory layout is correct.
479472 pub fn is_valid < M : GuestMemory > ( & self , mem : & M ) -> bool {
480473 let desc_table = self . desc_table_address ;
@@ -555,9 +548,9 @@ impl Queue {
555548 // once. Checking and reporting such incorrect driver behavior
556549 // can prevent potential hanging and Denial-of-Service from
557550 // happening on the VMM side.
558- if len > self . actual_size ( ) {
551+ if self . size < len {
559552 return Err ( InvalidAvailIdx {
560- queue_size : self . actual_size ( ) ,
553+ queue_size : self . size ,
561554 reported_len : len,
562555 } ) ;
563556 }
@@ -609,17 +602,15 @@ impl Queue {
609602 //
610603 // We use `self.next_avail` to store the position, in `ring`, of the next available
611604 // descriptor index, with a twist: we always only increment `self.next_avail`, so the
612- // actual position will be `self.next_avail % self.actual_size() `.
613- let idx = self . next_avail . 0 % self . actual_size ( ) ;
605+ // actual position will be `self.next_avail % self.size `.
606+ let idx = self . next_avail . 0 % self . size ;
614607 // SAFETY:
615608 // index is bound by the queue size
616609 let desc_index = unsafe { self . avail_ring_ring_get ( usize:: from ( idx) ) } ;
617610
618- DescriptorChain :: checked_new ( self . desc_table_ptr , self . actual_size ( ) , desc_index) . inspect (
619- |_| {
620- self . next_avail += Wrapping ( 1 ) ;
621- } ,
622- )
611+ DescriptorChain :: checked_new ( self . desc_table_ptr , self . size , desc_index) . inspect ( |_| {
612+ self . next_avail += Wrapping ( 1 ) ;
613+ } )
623614 }
624615
625616 /// Undo the effects of the last `self.pop()` call.
@@ -637,15 +628,15 @@ impl Queue {
637628 desc_index : u16 ,
638629 len : u32 ,
639630 ) -> Result < ( ) , QueueError > {
640- if self . actual_size ( ) <= desc_index {
631+ if self . size <= desc_index {
641632 error ! (
642633 "attempted to add out of bounds descriptor to used ring: {}" ,
643634 desc_index
644635 ) ;
645636 return Err ( QueueError :: DescIndexOutOfBounds ( desc_index) ) ;
646637 }
647638
648- let next_used = ( self . next_used + Wrapping ( ring_index_offset) ) . 0 % self . actual_size ( ) ;
639+ let next_used = ( self . next_used + Wrapping ( ring_index_offset) ) . 0 % self . size ;
649640 let used_element = UsedElement {
650641 id : u32:: from ( desc_index) ,
651642 len,
@@ -691,9 +682,9 @@ impl Queue {
691682 if len != 0 {
692683 // The number of descriptor chain heads to process should always
693684 // be smaller or equal to the queue size.
694- if len > self . actual_size ( ) {
685+ if len > self . size {
695686 return Err ( InvalidAvailIdx {
696- queue_size : self . actual_size ( ) ,
687+ queue_size : self . size ,
697688 reported_len : len,
698689 } ) ;
699690 }
@@ -1093,7 +1084,7 @@ mod verification {
10931084 // done. This is relying on implementation details of add_used, namely that
10941085 // the check for out-of-bounds descriptor index happens at the very beginning of the
10951086 // function.
1096- assert ! ( used_desc_table_index >= queue. actual_size ( ) ) ;
1087+ assert ! ( used_desc_table_index >= queue. size ) ;
10971088 }
10981089 }
10991090
@@ -1130,11 +1121,11 @@ mod verification {
11301121
11311122 #[ kani:: proof]
11321123 #[ kani:: unwind( 0 ) ]
1133- fn verify_actual_size ( ) {
1124+ fn verify_size ( ) {
11341125 let ProofContext ( queue, _) = kani:: any ( ) ;
11351126
1136- assert ! ( queue. actual_size ( ) <= queue. max_size) ;
1137- assert ! ( queue. actual_size ( ) <= queue. size) ;
1127+ assert ! ( queue. size <= queue. max_size) ;
1128+ assert ! ( queue. size <= queue. size) ;
11381129 }
11391130
11401131 #[ kani:: proof]
@@ -1199,7 +1190,7 @@ mod verification {
11991190 // is called when the queue is being initialized, e.g. empty. We compute it using
12001191 // local variables here to make things easier on kani: One less roundtrip through vm-memory.
12011192 let queue_len = queue. len ( ) ;
1202- kani:: assume ( queue_len <= queue. actual_size ( ) ) ;
1193+ kani:: assume ( queue_len <= queue. size ) ;
12031194
12041195 let next_avail = queue. next_avail ;
12051196
@@ -1217,7 +1208,7 @@ mod verification {
12171208 let ProofContext ( mut queue, _) = kani:: any ( ) ;
12181209
12191210 // See verify_pop for explanation
1220- kani:: assume ( queue. len ( ) <= queue. actual_size ( ) ) ;
1211+ kani:: assume ( queue. len ( ) <= queue. size ) ;
12211212
12221213 let queue_clone = queue. clone ( ) ;
12231214 if let Some ( _) = queue. pop ( ) . unwrap ( ) {
@@ -1233,7 +1224,7 @@ mod verification {
12331224 fn verify_try_enable_notification ( ) {
12341225 let ProofContext ( mut queue, _) = ProofContext :: bounded_queue ( ) ;
12351226
1236- kani:: assume ( queue. len ( ) <= queue. actual_size ( ) ) ;
1227+ kani:: assume ( queue. len ( ) <= queue. size ) ;
12371228
12381229 if queue. try_enable_notification ( ) . unwrap ( ) && queue. uses_notif_suppression {
12391230 // We only require new notifications if the queue is empty (e.g. we've processed
@@ -1251,10 +1242,9 @@ mod verification {
12511242 let ProofContext ( queue, mem) = kani:: any ( ) ;
12521243
12531244 let index = kani:: any ( ) ;
1254- let maybe_chain =
1255- DescriptorChain :: checked_new ( queue. desc_table_ptr , queue. actual_size ( ) , index) ;
1245+ let maybe_chain = DescriptorChain :: checked_new ( queue. desc_table_ptr , queue. size , index) ;
12561246
1257- if index >= queue. actual_size ( ) {
1247+ if index >= queue. size {
12581248 assert ! ( maybe_chain. is_none( ) )
12591249 } else {
12601250 // If the index was in-bounds for the descriptor table, we at least should be
@@ -1269,7 +1259,7 @@ mod verification {
12691259 match maybe_chain {
12701260 None => {
12711261 // This assert is the negation of the "is_valid" check in checked_new
1272- assert ! ( desc. flags & VIRTQ_DESC_F_NEXT == 1 && desc. next >= queue. actual_size ( ) )
1262+ assert ! ( desc. flags & VIRTQ_DESC_F_NEXT == 1 && desc. next >= queue. size )
12731263 }
12741264 Some ( head) => {
12751265 assert ! ( head. is_valid( ) )
0 commit comments