File tree 1 file changed +13
-21
lines changed
1 file changed +13
-21
lines changed Original file line number Diff line number Diff line change @@ -2188,31 +2188,23 @@ fn first_leading_bit(concrete_int: ConcreteInt<1>) -> ConcreteInt<1> {
2188
2188
// NOTE: Bit indices for this built-in start at 0 at the "right" (or LSB). For example, 1 means
2189
2189
// the least significant bit is set. Therefore, an input of 1 would return a right-to-left bit
2190
2190
// index of 0.
2191
- let highest_rtl_bit_index = 32 /* bit */ - 1 /* count to zero index */ ;
2191
+ let rtl_to_ltr_bit_idx = |e : u32 | -> u32 {
2192
+ match e {
2193
+ idx @ 0 ..=31 => 31 - idx,
2194
+ 32 => u32:: MAX ,
2195
+ _ => unreachable ! ( ) ,
2196
+ }
2197
+ } ;
2192
2198
match concrete_int {
2193
2199
ConcreteInt :: I32 ( [ e] ) => ConcreteInt :: I32 ( [ {
2194
- if matches ! ( e, 0 | -1 ) {
2195
- -1
2196
- } else {
2197
- let rtl_bit_index = if e. is_positive ( ) {
2198
- e. leading_zeros ( )
2199
- } else {
2200
- // must be negative
2201
- e. leading_ones ( )
2202
- } ;
2203
- ( highest_rtl_bit_index - rtl_bit_index)
2204
- . try_into ( )
2205
- . expect ( "bit count outside of 0..32 (!?)" )
2206
- }
2207
- } ] ) ,
2208
- ConcreteInt :: U32 ( [ e] ) => ConcreteInt :: U32 ( [ {
2209
- if e == 0 {
2210
- u32:: MAX
2200
+ let rtl_bit_index = if e. is_negative ( ) {
2201
+ e. leading_ones ( )
2211
2202
} else {
2212
- let rtl_bit_index = e. leading_zeros ( ) ;
2213
- highest_rtl_bit_index - rtl_bit_index
2214
- }
2203
+ e. leading_zeros ( )
2204
+ } ;
2205
+ rtl_to_ltr_bit_idx ( rtl_bit_index ) as i32
2215
2206
} ] ) ,
2207
+ ConcreteInt :: U32 ( [ e] ) => ConcreteInt :: U32 ( [ rtl_to_ltr_bit_idx ( e. leading_zeros ( ) ) ] ) ,
2216
2208
}
2217
2209
}
2218
2210
You can’t perform that action at this time.
0 commit comments