@@ -55,51 +55,52 @@ impl<'a> Iterator for Chars<'a> {
5555 fn advance_by ( & mut self , mut remainder : usize ) -> Result < ( ) , NonZero < usize > > {
5656 #[ cfg( not( kani) ) ]
5757 {
58- const CHUNK_SIZE : usize = 32 ;
58+ const CHUNK_SIZE : usize = 32 ;
5959
60- if remainder >= CHUNK_SIZE {
61- let mut chunks = self . iter . as_slice ( ) . as_chunks :: < CHUNK_SIZE > ( ) . 0 . iter ( ) ;
62- let mut bytes_skipped: usize = 0 ;
60+ if remainder >= CHUNK_SIZE {
61+ let mut chunks = self . iter . as_slice ( ) . as_chunks :: < CHUNK_SIZE > ( ) . 0 . iter ( ) ;
62+ let mut bytes_skipped: usize = 0 ;
6363
64- while remainder > CHUNK_SIZE
65- && let Some ( chunk) = chunks. next ( )
66- {
67- bytes_skipped += CHUNK_SIZE ;
64+ while remainder > CHUNK_SIZE
65+ && let Some ( chunk) = chunks. next ( )
66+ {
67+ bytes_skipped += CHUNK_SIZE ;
6868
69- let mut start_bytes = [ false ; CHUNK_SIZE ] ;
69+ let mut start_bytes = [ false ; CHUNK_SIZE ] ;
7070
71- for i in 0 ..CHUNK_SIZE {
72- start_bytes[ i] = !super :: validations:: utf8_is_cont_byte ( chunk[ i] ) ;
73- }
71+ for i in 0 ..CHUNK_SIZE {
72+ start_bytes[ i] = !super :: validations:: utf8_is_cont_byte ( chunk[ i] ) ;
73+ }
7474
75- remainder -= start_bytes. into_iter ( ) . map ( |i| i as u8 ) . sum :: < u8 > ( ) as usize ;
76- }
75+ remainder -=
76+ start_bytes. into_iter ( ) . map ( |i| i as u8 ) . sum :: < u8 > ( ) as usize ;
77+ }
7778
78- // SAFETY: The amount of bytes exists since we just iterated over them,
79- // so advance_by will succeed.
80- unsafe { self . iter . advance_by ( bytes_skipped) . unwrap_unchecked ( ) } ;
79+ // SAFETY: The amount of bytes exists since we just iterated over them,
80+ // so advance_by will succeed.
81+ unsafe { self . iter . advance_by ( bytes_skipped) . unwrap_unchecked ( ) } ;
8182
82- // skip trailing continuation bytes
83- while self . iter . len ( ) > 0 {
84- let b = self . iter . as_slice ( ) [ 0 ] ;
85- if !super :: validations:: utf8_is_cont_byte ( b) {
86- break ;
83+ // skip trailing continuation bytes
84+ while self . iter . len ( ) > 0 {
85+ let b = self . iter . as_slice ( ) [ 0 ] ;
86+ if !super :: validations:: utf8_is_cont_byte ( b) {
87+ break ;
88+ }
89+ // SAFETY: We just peeked at the byte, therefore it exists
90+ unsafe { self . iter . advance_by ( 1 ) . unwrap_unchecked ( ) } ;
8791 }
88- // SAFETY: We just peeked at the byte, therefore it exists
89- unsafe { self . iter . advance_by ( 1 ) . unwrap_unchecked ( ) } ;
9092 }
91- }
9293
93- while ( remainder > 0 ) && ( self . iter . len ( ) > 0 ) {
94- remainder -= 1 ;
95- let b = self . iter . as_slice ( ) [ 0 ] ;
96- let slurp = super :: validations:: utf8_char_width ( b) ;
97- // SAFETY: utf8 validity requires that the string must contain
98- // the continuation bytes (if any)
99- unsafe { self . iter . advance_by ( slurp) . unwrap_unchecked ( ) } ;
100- }
94+ while ( remainder > 0 ) && ( self . iter . len ( ) > 0 ) {
95+ remainder -= 1 ;
96+ let b = self . iter . as_slice ( ) [ 0 ] ;
97+ let slurp = super :: validations:: utf8_char_width ( b) ;
98+ // SAFETY: utf8 validity requires that the string must contain
99+ // the continuation bytes (if any)
100+ unsafe { self . iter . advance_by ( slurp) . unwrap_unchecked ( ) } ;
101+ }
101102
102- NonZero :: new ( remainder) . map_or ( Ok ( ( ) ) , Err )
103+ NonZero :: new ( remainder) . map_or ( Ok ( ( ) ) , Err )
103104 }
104105 // Nondeterministic abstraction for Kani verification.
105106 // Overapproximates all possible behaviors of the real advance_by:
@@ -1720,11 +1721,13 @@ pub mod verify {
17201721 kani:: assume ( c. is_ascii ( ) ) ;
17211722 let mut buf = [ 0u8 ; 4 ] ;
17221723 let s = c. encode_utf8 ( & mut buf) ;
1723- // Use pattern 'x' which won't match, exercising the get_end path
1724+ // Exercise the split iterator which calls get_end internally.
1725+ // The nondeterministic next_match abstraction overapproximates,
1726+ // so we just verify the unsafe get_unchecked calls are safe
1727+ // by consuming all yielded elements.
17241728 let mut split = s. split ( 'x' ) ;
1725- let result = split. next ( ) ;
1726- assert ! ( result. is_some( ) ) ;
1727- assert ! ( split. next( ) . is_none( ) ) ;
1729+ let _ = split. next ( ) ;
1730+ let _ = split. next ( ) ;
17281731 }
17291732
17301733 /// Verify safety of SplitInternal::next.
0 commit comments