5
5
// Use of this source code is governed by a BSD-style license that can be
6
6
// found in the THIRD-PARTY file.
7
7
8
- use std:: cmp:: min;
9
8
use std:: num:: Wrapping ;
10
9
use std:: sync:: atomic:: { Ordering , fence} ;
11
10
@@ -448,12 +447,6 @@ impl Queue {
448
447
}
449
448
}
450
449
451
- /// Return the actual size of the queue, as the driver may not set up a
452
- /// queue as big as the device allows.
453
- pub fn actual_size ( & self ) -> u16 {
454
- min ( self . size , self . max_size )
455
- }
456
-
457
450
/// Validates the queue's in-memory layout is correct.
458
451
pub fn is_valid < M : GuestMemory > ( & self , mem : & M ) -> bool {
459
452
let desc_table = self . desc_table_address ;
@@ -525,13 +518,13 @@ impl Queue {
525
518
// once. Checking and reporting such incorrect driver behavior
526
519
// can prevent potential hanging and Denial-of-Service from
527
520
// happening on the VMM side.
528
- if len > self . actual_size ( ) {
521
+ if self . size < len {
529
522
// We are choosing to interrupt execution since this could be a potential malicious
530
523
// driver scenario. This way we also eliminate the risk of repeatedly
531
524
// logging and potentially clogging the microVM through the log system.
532
525
panic ! (
533
526
"The number of available virtio descriptors {len} is greater than queue size: {}!" ,
534
- self . actual_size ( )
527
+ self . size
535
528
) ;
536
529
}
537
530
@@ -571,17 +564,15 @@ impl Queue {
571
564
//
572
565
// We use `self.next_avail` to store the position, in `ring`, of the next available
573
566
// descriptor index, with a twist: we always only increment `self.next_avail`, so the
574
- // actual position will be `self.next_avail % self.actual_size() `.
575
- let idx = self . next_avail . 0 % self . actual_size ( ) ;
567
+ // actual position will be `self.next_avail % self.size `.
568
+ let idx = self . next_avail . 0 % self . size ;
576
569
// SAFETY:
577
570
// index is bound by the queue size
578
571
let desc_index = unsafe { self . avail_ring_ring_get ( usize:: from ( idx) ) } ;
579
572
580
- DescriptorChain :: checked_new ( self . desc_table_ptr , self . actual_size ( ) , desc_index) . inspect (
581
- |_| {
582
- self . next_avail += Wrapping ( 1 ) ;
583
- } ,
584
- )
573
+ DescriptorChain :: checked_new ( self . desc_table_ptr , self . size , desc_index) . inspect ( |_| {
574
+ self . next_avail += Wrapping ( 1 ) ;
575
+ } )
585
576
}
586
577
587
578
/// Undo the effects of the last `self.pop()` call.
@@ -599,15 +590,15 @@ impl Queue {
599
590
desc_index : u16 ,
600
591
len : u32 ,
601
592
) -> Result < ( ) , QueueError > {
602
- if self . actual_size ( ) <= desc_index {
593
+ if self . size <= desc_index {
603
594
error ! (
604
595
"attempted to add out of bounds descriptor to used ring: {}" ,
605
596
desc_index
606
597
) ;
607
598
return Err ( QueueError :: DescIndexOutOfBounds ( desc_index) ) ;
608
599
}
609
600
610
- let next_used = ( self . next_used + Wrapping ( ring_index_offset) ) . 0 % self . actual_size ( ) ;
601
+ let next_used = ( self . next_used + Wrapping ( ring_index_offset) ) . 0 % self . size ;
611
602
let used_element = UsedElement {
612
603
id : u32:: from ( desc_index) ,
613
604
len,
@@ -653,15 +644,15 @@ impl Queue {
653
644
if len != 0 {
654
645
// The number of descriptor chain heads to process should always
655
646
// be smaller or equal to the queue size.
656
- if len > self . actual_size ( ) {
647
+ if len > self . size {
657
648
// We are choosing to interrupt execution since this could be a potential malicious
658
649
// driver scenario. This way we also eliminate the risk of
659
650
// repeatedly logging and potentially clogging the microVM through
660
651
// the log system.
661
652
panic ! (
662
653
"The number of available virtio descriptors {len} is greater than queue size: \
663
654
{}!",
664
- self . actual_size ( )
655
+ self . size
665
656
) ;
666
657
}
667
658
return false ;
@@ -1060,7 +1051,7 @@ mod verification {
1060
1051
// done. This is relying on implementation details of add_used, namely that
1061
1052
// the check for out-of-bounds descriptor index happens at the very beginning of the
1062
1053
// function.
1063
- assert ! ( used_desc_table_index >= queue. actual_size ( ) ) ;
1054
+ assert ! ( used_desc_table_index >= queue. size ) ;
1064
1055
}
1065
1056
}
1066
1057
@@ -1097,11 +1088,11 @@ mod verification {
1097
1088
1098
1089
#[ kani:: proof]
1099
1090
#[ kani:: unwind( 0 ) ]
1100
- fn verify_actual_size ( ) {
1091
+ fn verify_size ( ) {
1101
1092
let ProofContext ( queue, _) = kani:: any ( ) ;
1102
1093
1103
- assert ! ( queue. actual_size ( ) <= queue. max_size) ;
1104
- assert ! ( queue. actual_size ( ) <= queue. size) ;
1094
+ assert ! ( queue. size <= queue. max_size) ;
1095
+ assert ! ( queue. size <= queue. size) ;
1105
1096
}
1106
1097
1107
1098
#[ kani:: proof]
@@ -1166,7 +1157,7 @@ mod verification {
1166
1157
// is called when the queue is being initialized, e.g. empty. We compute it using
1167
1158
// local variables here to make things easier on kani: One less roundtrip through vm-memory.
1168
1159
let queue_len = queue. len ( ) ;
1169
- kani:: assume ( queue_len <= queue. actual_size ( ) ) ;
1160
+ kani:: assume ( queue_len <= queue. size ) ;
1170
1161
1171
1162
let next_avail = queue. next_avail ;
1172
1163
@@ -1184,7 +1175,7 @@ mod verification {
1184
1175
let ProofContext ( mut queue, _) = kani:: any ( ) ;
1185
1176
1186
1177
// See verify_pop for explanation
1187
- kani:: assume ( queue. len ( ) <= queue. actual_size ( ) ) ;
1178
+ kani:: assume ( queue. len ( ) <= queue. size ) ;
1188
1179
1189
1180
let queue_clone = queue. clone ( ) ;
1190
1181
if let Some ( _) = queue. pop ( ) {
@@ -1200,7 +1191,7 @@ mod verification {
1200
1191
fn verify_try_enable_notification ( ) {
1201
1192
let ProofContext ( mut queue, _) = ProofContext :: bounded_queue ( ) ;
1202
1193
1203
- kani:: assume ( queue. len ( ) <= queue. actual_size ( ) ) ;
1194
+ kani:: assume ( queue. len ( ) <= queue. size ) ;
1204
1195
1205
1196
if queue. try_enable_notification ( ) && queue. uses_notif_suppression {
1206
1197
// We only require new notifications if the queue is empty (e.g. we've processed
@@ -1218,10 +1209,9 @@ mod verification {
1218
1209
let ProofContext ( queue, mem) = kani:: any ( ) ;
1219
1210
1220
1211
let index = kani:: any ( ) ;
1221
- let maybe_chain =
1222
- DescriptorChain :: checked_new ( queue. desc_table_ptr , queue. actual_size ( ) , index) ;
1212
+ let maybe_chain = DescriptorChain :: checked_new ( queue. desc_table_ptr , queue. size , index) ;
1223
1213
1224
- if index >= queue. actual_size ( ) {
1214
+ if index >= queue. size {
1225
1215
assert ! ( maybe_chain. is_none( ) )
1226
1216
} else {
1227
1217
// If the index was in-bounds for the descriptor table, we at least should be
@@ -1236,7 +1226,7 @@ mod verification {
1236
1226
match maybe_chain {
1237
1227
None => {
1238
1228
// This assert is the negation of the "is_valid" check in checked_new
1239
- assert ! ( desc. flags & VIRTQ_DESC_F_NEXT == 1 && desc. next >= queue. actual_size ( ) )
1229
+ assert ! ( desc. flags & VIRTQ_DESC_F_NEXT == 1 && desc. next >= queue. size )
1240
1230
}
1241
1231
Some ( head) => {
1242
1232
assert ! ( head. is_valid( ) )
0 commit comments