Skip to content

Rewrite control-flow reconstruction #896

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

Draft
Nadrieril wants to merge 7 commits into
base: main
Choose a base branch
from
Draft

Rewrite control-flow reconstruction #896

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
733a750
Add tests
Nadrieril Nov 17, 2025
7a475ce
Rewrite cfg reconstruction using `Beyond Relooper`
Nadrieril Nov 17, 2025
14c33da
Rework context stack handling a bit
Nadrieril Nov 17, 2025
adf72d2
Use indexing instead of `HashSet`s everywhere
Nadrieril Nov 17, 2025
18d71fb
Cache some more computation
Nadrieril Nov 17, 2025
9d94311
Remove unneeded `break`/`continue`s
Nadrieril Nov 18, 2025
f6f64d5
Remove some unneeded `loop { ...; break }` constructs
Nadrieril Nov 18, 2025
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
1 change: 1 addition & 0 deletions charon/Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions charon/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@ serde_json = { version = "1.0.91", features = ["unbounded_depth"] }
serde-map-to-array = { version = "1.1.1", features = ["std"] }
serde_stacker = "0.1.11"
serde = { version = "1.0.152", features = ["derive", "rc"] }
smallvec = "1.15.1"
stacker = "0.1"
strip-ansi-escapes = "0.2.1"
take_mut = "0.2.2"
Expand Down
2,014 changes: 350 additions & 1,664 deletions charon/src/transform/control_flow/ullbc_to_llbc.rs
View file
Open in desktop

Large diffs are not rendered by default.

268 changes: 129 additions & 139 deletions charon/tests/ui/arrays.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1606,36 +1606,34 @@ pub fn sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
storage_dead(@7)
@4 := move (@5) < move (@6)
if move (@4) {
storage_dead(@6)
storage_dead(@5)
storage_live(@8)
storage_live(@9)
@9 := copy (i@3)
storage_live(@12)
@12 := &*(s@1) with_metadata(copy ([email protected]))
storage_live(@13)
@13 := @SliceIndexShared<'_, u32>(move (@12), copy (@9))
@8 := copy (*(@13))
@10 := copy (sum@2) panic.+ copy (@8)
sum@2 := move (@10)
storage_dead(@8)
storage_dead(@9)
@11 := copy (i@3) panic.+ const (1 : usize)
i@3 := move (@11)
storage_dead(@4)
}
else {
break 0
storage_dead(@6)
storage_dead(@5)
storage_dead(@4)
@0 := copy (sum@2)
storage_dead(i@3)
storage_dead(sum@2)
return
}
storage_dead(@6)
storage_dead(@5)
storage_live(@8)
storage_live(@9)
@9 := copy (i@3)
storage_live(@12)
@12 := &*(s@1) with_metadata(copy ([email protected]))
storage_live(@13)
@13 := @SliceIndexShared<'_, u32>(move (@12), copy (@9))
@8 := copy (*(@13))
@10 := copy (sum@2) panic.+ copy (@8)
sum@2 := move (@10)
storage_dead(@8)
storage_dead(@9)
@11 := copy (i@3) panic.+ const (1 : usize)
i@3 := move (@11)
storage_dead(@4)
continue 0
}
storage_dead(@6)
storage_dead(@5)
storage_dead(@4)
@0 := copy (sum@2)
storage_dead(i@3)
storage_dead(sum@2)
return
}

// Full name: test_crate::sum2
Expand Down Expand Up @@ -1686,72 +1684,70 @@ pub fn sum2<'_0, '_1>(@1: &'_0 (Slice<u32>), @2: &'_1 (Slice<u32>)) -> u32
storage_dead(@8)
@4 := move (@5) == move (@7)
if move (@4) {
storage_dead(@7)
storage_dead(@5)
storage_dead(@4)
storage_live(i@9)
i@9 := const (0 : usize)
loop {
storage_live(@10)
storage_live(@11)
@11 := copy (i@9)
storage_live(@12)
storage_live(@13)
@13 := &*(s@1) with_metadata(copy ([email protected]))
@12 := len<'_, u32>[{built_in impl Sized for u32}](move (@13))
storage_dead(@13)
@10 := move (@11) < move (@12)
if move (@10) {
storage_dead(@12)
storage_dead(@11)
storage_live(@14)
storage_live(@15)
storage_live(@16)
@16 := copy (i@9)
storage_live(@24)
@24 := &*(s@1) with_metadata(copy ([email protected]))
storage_live(@25)
@25 := @SliceIndexShared<'_, u32>(move (@24), copy (@16))
@15 := copy (*(@25))
storage_live(@17)
storage_live(@18)
@18 := copy (i@9)
storage_live(@22)
@22 := &*(s2@2) with_metadata(copy ([email protected]))
storage_live(@23)
@23 := @SliceIndexShared<'_, u32>(move (@22), copy (@18))
@17 := copy (*(@23))
@19 := copy (@15) panic.+ copy (@17)
@14 := move (@19)
storage_dead(@17)
storage_dead(@15)
@20 := copy (sum@3) panic.+ copy (@14)
sum@3 := move (@20)
storage_dead(@14)
storage_dead(@18)
storage_dead(@16)
@21 := copy (i@9) panic.+ const (1 : usize)
i@9 := move (@21)
storage_dead(@10)
}
else {
storage_dead(@12)
storage_dead(@11)
storage_dead(@10)
@0 := copy (sum@3)
storage_dead(i@9)
storage_dead(sum@3)
return
}
}
}
else {
storage_dead(@7)
storage_dead(@5)
panic(core::panicking::panic)
}
storage_dead(@7)
storage_dead(@5)
storage_dead(@4)
storage_live(i@9)
i@9 := const (0 : usize)
loop {
storage_live(@10)
storage_live(@11)
@11 := copy (i@9)
storage_live(@12)
storage_live(@13)
@13 := &*(s@1) with_metadata(copy ([email protected]))
@12 := len<'_, u32>[{built_in impl Sized for u32}](move (@13))
storage_dead(@13)
@10 := move (@11) < move (@12)
if move (@10) {
}
else {
break 0
}
storage_dead(@12)
storage_dead(@11)
storage_live(@14)
storage_live(@15)
storage_live(@16)
@16 := copy (i@9)
storage_live(@24)
@24 := &*(s@1) with_metadata(copy ([email protected]))
storage_live(@25)
@25 := @SliceIndexShared<'_, u32>(move (@24), copy (@16))
@15 := copy (*(@25))
storage_live(@17)
storage_live(@18)
@18 := copy (i@9)
storage_live(@22)
@22 := &*(s2@2) with_metadata(copy ([email protected]))
storage_live(@23)
@23 := @SliceIndexShared<'_, u32>(move (@22), copy (@18))
@17 := copy (*(@23))
@19 := copy (@15) panic.+ copy (@17)
@14 := move (@19)
storage_dead(@17)
storage_dead(@15)
@20 := copy (sum@3) panic.+ copy (@14)
sum@3 := move (@20)
storage_dead(@14)
storage_dead(@18)
storage_dead(@16)
@21 := copy (i@9) panic.+ const (1 : usize)
i@9 := move (@21)
storage_dead(@10)
continue 0
}
storage_dead(@12)
storage_dead(@11)
storage_dead(@10)
@0 := copy (sum@3)
storage_dead(i@9)
storage_dead(sum@3)
return
}

// Full name: test_crate::f0
Expand Down Expand Up @@ -2063,19 +2059,17 @@ pub fn zero_slice<'_0>(@1: &'_0 mut (Slice<u8>))
@9 := copy (i@2) panic.+ const (1 : usize)
i@2 := move (@9)
storage_dead(@5)
continue 0
}
else {
break 0
storage_dead(@7)
storage_dead(@6)
@0 := ()
storage_dead(@5)
storage_dead(len@3)
storage_dead(i@2)
return
}
}
storage_dead(@7)
storage_dead(@6)
@0 := ()
storage_dead(@5)
storage_dead(len@3)
storage_dead(i@2)
return
}

// Full name: test_crate::iter_mut_slice
Expand Down Expand Up @@ -2113,19 +2107,17 @@ pub fn iter_mut_slice<'_0>(@1: &'_0 mut (Slice<u8>))
@8 := copy (i@4) panic.+ const (1 : usize)
i@4 := move (@8)
storage_dead(@5)
continue 0
}
else {
break 0
storage_dead(@7)
storage_dead(@6)
@0 := ()
storage_dead(@5)
storage_dead(i@4)
storage_dead(len@2)
return
}
}
storage_dead(@7)
storage_dead(@6)
@0 := ()
storage_dead(@5)
storage_dead(i@4)
storage_dead(len@2)
return
}

// Full name: test_crate::sum_mut_slice
Expand Down Expand Up @@ -2163,36 +2155,34 @@ pub fn sum_mut_slice<'_0>(@1: &'_0 mut (Slice<u32>)) -> u32
storage_dead(@7)
@4 := move (@5) < move (@6)
if move (@4) {
storage_dead(@6)
storage_dead(@5)
storage_live(@8)
storage_live(@9)
@9 := copy (i@2)
storage_live(@12)
@12 := &*(a@1) with_metadata(copy ([email protected]))
storage_live(@13)
@13 := @SliceIndexShared<'_, u32>(move (@12), copy (@9))
@8 := copy (*(@13))
@10 := copy (s@3) panic.+ copy (@8)
s@3 := move (@10)
storage_dead(@8)
storage_dead(@9)
@11 := copy (i@2) panic.+ const (1 : usize)
i@2 := move (@11)
storage_dead(@4)
}
else {
break 0
storage_dead(@6)
storage_dead(@5)
storage_dead(@4)
@0 := copy (s@3)
storage_dead(s@3)
storage_dead(i@2)
return
}
storage_dead(@6)
storage_dead(@5)
storage_live(@8)
storage_live(@9)
@9 := copy (i@2)
storage_live(@12)
@12 := &*(a@1) with_metadata(copy ([email protected]))
storage_live(@13)
@13 := @SliceIndexShared<'_, u32>(move (@12), copy (@9))
@8 := copy (*(@13))
@10 := copy (s@3) panic.+ copy (@8)
s@3 := move (@10)
storage_dead(@8)
storage_dead(@9)
@11 := copy (i@2) panic.+ const (1 : usize)
i@2 := move (@11)
storage_dead(@4)
continue 0
}
storage_dead(@6)
storage_dead(@5)
storage_dead(@4)
@0 := copy (s@3)
storage_dead(s@3)
storage_dead(i@2)
return
}

// Full name: test_crate::slice_pattern_1
Expand Down Expand Up @@ -2303,20 +2293,20 @@ fn slice_pattern_4<'_0>(@1: &'_0 (Slice<()>))
@4 := const (1 : usize)
@5 := move (@2) == move (@4)
if move (@5) {
storage_live(_named@6)
storage_live(@7)
@7 := &*(x@1) with_metadata(copy ([email protected]))
storage_live(@8)
@8 := @SliceIndexShared<'_, ()>(move (@7), const (0 : usize))
_named@6 := &*(@8)
@0 := ()
storage_dead(_named@6)
return
}
else {
@0 := ()
return
}
storage_live(_named@6)
storage_live(@7)
@7 := &*(x@1) with_metadata(copy ([email protected]))
storage_live(@8)
@8 := @SliceIndexShared<'_, ()>(move (@7), const (0 : usize))
_named@6 := &*(@8)
@0 := ()
storage_dead(_named@6)
return
}


Expand Down
4 changes: 2 additions & 2 deletions charon/tests/ui/closures.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -242,6 +242,8 @@ where

match *(x@1) {
Option::None => {
@0 := Option::None { }
return
},
Option::Some => {
storage_live(x@3)
Expand All @@ -261,8 +263,6 @@ where
return
},
}
@0 := Option::None { }
return
}

// Full name: test_crate::test_map_option1
Expand Down
Loading
Loading