Skip to content

Only consider switch exits within the same loop as the switch entry #977

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Nadrieril merged 4 commits into from
Jan 17, 2026
Merged

Only consider switch exits within the same loop as the switch entry #977

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d8ae508
Don't ignore switch exits that are also loop exits
Nadrieril Jan 14, 2026
1587add
Cleanup
Nadrieril Jan 14, 2026
a3f3ddb
Cleanup a bit more
Nadrieril Jan 16, 2026
57ce772
Only consider switch exits within the same loop as the switch entry
Nadrieril Jan 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
364 changes: 111 additions & 253 deletions charon/src/transform/control_flow/ullbc_to_llbc.rs
View file
Open in desktop

Large diffs are not rendered by default.

282 changes: 141 additions & 141 deletions charon/tests/ui/control-flow/issue-297-cfg.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -625,149 +625,149 @@ fn f2<'_0, '_1>(@1: &'_0 [u8], @2: &'_1 mut [i16]) -> usize
break 0
},
Option::Some => {
storage_live(bytes_11)
bytes_11 = copy (_8 as variant Option::Some).0
storage_live(b1_12)
storage_live(_13)
storage_live(_14)
_14 = const 0 : usize
storage_live(_49)
_49 = &(*bytes_11) with_metadata(copy bytes_11.metadata)
storage_live(_50)
_50 = @SliceIndexShared<'_, u8>(move _49, copy _14)
_13 = copy (*_50)
b1_12 = cast<u8, i16>(move _13)
storage_dead(_13)
storage_dead(_14)
storage_live(b2_15)
storage_live(_16)
storage_live(_17)
_17 = const 1 : usize
storage_live(_51)
_51 = &(*bytes_11) with_metadata(copy bytes_11.metadata)
storage_live(_52)
_52 = @SliceIndexShared<'_, u8>(move _51, copy _17)
_16 = copy (*_52)
b2_15 = cast<u8, i16>(move _16)
storage_dead(_16)
storage_dead(_17)
storage_live(b3_18)
storage_live(_19)
storage_live(_20)
_20 = const 2 : usize
storage_live(_53)
_53 = &(*bytes_11) with_metadata(copy bytes_11.metadata)
storage_live(_54)
_54 = @SliceIndexShared<'_, u8>(move _53, copy _20)
_19 = copy (*_54)
b3_18 = cast<u8, i16>(move _19)
storage_dead(_19)
storage_dead(_20)
storage_live(d1_21)
storage_live(_22)
storage_live(_23)
storage_live(_24)
_24 = copy b2_15
_23 = move _24 & const 15 : i16
storage_dead(_24)
_22 = move _23 panic.<< const 8 : i32
storage_dead(_23)
storage_live(_25)
_25 = copy b1_12
d1_21 = move _22 | move _25
storage_dead(_25)
storage_dead(_22)
storage_live(d2_26)
storage_live(_27)
storage_live(_28)
_28 = copy b3_18
_27 = move _28 panic.<< const 4 : i32
storage_dead(_28)
storage_live(_29)
storage_live(_30)
_30 = copy b2_15
_29 = move _30 panic.>> const 4 : i32
storage_dead(_30)
d2_26 = move _27 | move _29
storage_dead(_29)
storage_dead(_27)
storage_live(_31)
storage_live(_32)
_32 = copy d1_21
_31 = move _32 < copy FIELD_MODULUS
if move _31 {
storage_dead(_32)
storage_live(_33)
storage_live(_34)
_34 = copy sampled_3
_33 = move _34 < const 16 : usize
if move _33 {
storage_dead(_34)
storage_live(_35)
_35 = copy d1_21
storage_live(_36)
_36 = copy sampled_3
storage_live(_45)
_45 = &mut (*result_2) with_metadata(copy result_2.metadata)
storage_live(_46)
_46 = @SliceIndexMut<'_, i16>(move _45, copy _36)
(*_46) = move _35
storage_dead(_35)
storage_dead(_36)
_37 = copy sampled_3 panic.+ const 1 : usize
sampled_3 = move _37
} else {
storage_dead(_34)
}
} else {
storage_dead(_32)
}
storage_dead(_33)
storage_dead(_31)
storage_live(_38)
storage_live(_39)
_39 = copy d2_26
_38 = move _39 < copy FIELD_MODULUS
if move _38 {
storage_dead(_39)
storage_live(_40)
storage_live(_41)
_41 = copy sampled_3
_40 = move _41 < const 16 : usize
if move _40 {
storage_dead(_41)
storage_live(_42)
_42 = copy d2_26
storage_live(_43)
_43 = copy sampled_3
storage_live(_47)
_47 = &mut (*result_2) with_metadata(copy result_2.metadata)
storage_live(_48)
_48 = @SliceIndexMut<'_, i16>(move _47, copy _43)
(*_48) = move _42
storage_dead(_42)
storage_dead(_43)
_44 = copy sampled_3 panic.+ const 1 : usize
sampled_3 = move _44
} else {
storage_dead(_41)
}
} else {
storage_dead(_39)
}
storage_dead(_40)
storage_dead(_38)
storage_dead(d2_26)
storage_dead(d1_21)
storage_dead(b3_18)
storage_dead(b2_15)
storage_dead(b1_12)
storage_dead(bytes_11)
storage_dead(_10)
storage_dead(_8)
continue 0
},
}
storage_live(bytes_11)
bytes_11 = copy (_8 as variant Option::Some).0
storage_live(b1_12)
storage_live(_13)
storage_live(_14)
_14 = const 0 : usize
storage_live(_49)
_49 = &(*bytes_11) with_metadata(copy bytes_11.metadata)
storage_live(_50)
_50 = @SliceIndexShared<'_, u8>(move _49, copy _14)
_13 = copy (*_50)
b1_12 = cast<u8, i16>(move _13)
storage_dead(_13)
storage_dead(_14)
storage_live(b2_15)
storage_live(_16)
storage_live(_17)
_17 = const 1 : usize
storage_live(_51)
_51 = &(*bytes_11) with_metadata(copy bytes_11.metadata)
storage_live(_52)
_52 = @SliceIndexShared<'_, u8>(move _51, copy _17)
_16 = copy (*_52)
b2_15 = cast<u8, i16>(move _16)
storage_dead(_16)
storage_dead(_17)
storage_live(b3_18)
storage_live(_19)
storage_live(_20)
_20 = const 2 : usize
storage_live(_53)
_53 = &(*bytes_11) with_metadata(copy bytes_11.metadata)
storage_live(_54)
_54 = @SliceIndexShared<'_, u8>(move _53, copy _20)
_19 = copy (*_54)
b3_18 = cast<u8, i16>(move _19)
storage_dead(_19)
storage_dead(_20)
storage_live(d1_21)
storage_live(_22)
storage_live(_23)
storage_live(_24)
_24 = copy b2_15
_23 = move _24 & const 15 : i16
storage_dead(_24)
_22 = move _23 panic.<< const 8 : i32
storage_dead(_23)
storage_live(_25)
_25 = copy b1_12
d1_21 = move _22 | move _25
storage_dead(_25)
storage_dead(_22)
storage_live(d2_26)
storage_live(_27)
storage_live(_28)
_28 = copy b3_18
_27 = move _28 panic.<< const 4 : i32
storage_dead(_28)
storage_live(_29)
storage_live(_30)
_30 = copy b2_15
_29 = move _30 panic.>> const 4 : i32
storage_dead(_30)
d2_26 = move _27 | move _29
storage_dead(_29)
storage_dead(_27)
storage_live(_31)
storage_live(_32)
_32 = copy d1_21
_31 = move _32 < copy FIELD_MODULUS
if move _31 {
storage_dead(_32)
storage_live(_33)
storage_live(_34)
_34 = copy sampled_3
_33 = move _34 < const 16 : usize
if move _33 {
storage_dead(_34)
storage_live(_35)
_35 = copy d1_21
storage_live(_36)
_36 = copy sampled_3
storage_live(_45)
_45 = &mut (*result_2) with_metadata(copy result_2.metadata)
storage_live(_46)
_46 = @SliceIndexMut<'_, i16>(move _45, copy _36)
(*_46) = move _35
storage_dead(_35)
storage_dead(_36)
_37 = copy sampled_3 panic.+ const 1 : usize
sampled_3 = move _37
} else {
storage_dead(_34)
}
} else {
storage_dead(_32)
}
storage_dead(_33)
storage_dead(_31)
storage_live(_38)
storage_live(_39)
_39 = copy d2_26
_38 = move _39 < copy FIELD_MODULUS
if move _38 {
storage_dead(_39)
storage_live(_40)
storage_live(_41)
_41 = copy sampled_3
_40 = move _41 < const 16 : usize
if move _40 {
storage_dead(_41)
storage_live(_42)
_42 = copy d2_26
storage_live(_43)
_43 = copy sampled_3
storage_live(_47)
_47 = &mut (*result_2) with_metadata(copy result_2.metadata)
storage_live(_48)
_48 = @SliceIndexMut<'_, i16>(move _47, copy _43)
(*_48) = move _42
storage_dead(_42)
storage_dead(_43)
_44 = copy sampled_3 panic.+ const 1 : usize
sampled_3 = move _44
} else {
storage_dead(_41)
}
} else {
storage_dead(_39)
}
storage_dead(_40)
storage_dead(_38)
storage_dead(d2_26)
storage_dead(d1_21)
storage_dead(b3_18)
storage_dead(b2_15)
storage_dead(b1_12)
storage_dead(bytes_11)
storage_dead(_10)
storage_dead(_8)
continue 0
}
storage_dead(_10)
storage_dead(_8)
Expand Down
Loading