Skip to content

Commit

Permalink
Merge pull request #537 from Nadrieril/debug-goto-chains
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril authored Jan 24, 2025
2 parents 1103c51 + d3d272d commit e6ff54c
Show file tree
Hide file tree
Showing 8 changed files with 108 additions and 99 deletions.
25 changes: 17 additions & 8 deletions charon/src/transform/merge_goto_chains.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,15 +9,19 @@ use super::ctx::UllbcPass;
/// antecedent.
enum Antecedents {
Zero,
One(BlockId),
One {
id: BlockId,
/// Whether the antecedent is a goto.
is_goto: bool,
},
Many,
}

impl Antecedents {
fn add(&mut self, id: BlockId) {
fn add(&mut self, id: BlockId, is_goto: bool) {
match self {
Antecedents::Zero => *self = Antecedents::One(id),
Antecedents::One(_) => *self = Antecedents::Many,
Antecedents::Zero => *self = Antecedents::One { id, is_goto },
Antecedents::One { .. } => *self = Antecedents::Many,
Antecedents::Many => {}
}
}
Expand All @@ -35,23 +39,28 @@ impl UllbcPass for Transform {
let mut antecedents: Vector<BlockId, Antecedents> =
body.body.map_ref(|_| Antecedents::Zero);
for (block_id, block) in body.body.iter_indexed() {
let is_goto = block.terminator.content.is_goto();
for target in block.targets() {
antecedents.get_mut(target).unwrap().add(block_id);
antecedents.get_mut(target).unwrap().add(block_id, is_goto);
}
}
// Merge blocks with a single antecedent into their antecedent.
for mut id in body.body.all_indices() {
// Go up the chain to find the first parent with zero (the start block) or multiple
// antecedents. This avoids quadratic behavior where we repeatedly copy a growing list
// of statements, since blocks may not be sorted..
while let Antecedents::One(antecedent) = antecedents[id] {
id = antecedent;
while let Antecedents::One {
id: antecedent_id,
is_goto: true,
} = antecedents[id]
{
id = antecedent_id;
}
// While the current block is a straight goto, merge the target block back into this
// one.
while let Some(source) = body.body.get(id)
&& let RawTerminator::Goto { target } = source.terminator.content
&& let Antecedents::One(_) = antecedents[target]
&& let Antecedents::One { .. } = antecedents[target]
{
let mut target = body.body.remove(target).unwrap();
let source = &mut body.body[id];
Expand Down
40 changes: 20 additions & 20 deletions charon/tests/ui/arrays.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1231,8 +1231,8 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
drop @10
drop @11
i@3 := copy (i@3) + const (1 : usize)
@14 := ()
@5 := move (@14)
@13 := ()
@5 := move (@13)
drop @6
continue 0
}
Expand All @@ -1242,8 +1242,8 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
}
drop @8
drop @7
@13 := ()
@4 := move (@13)
@14 := ()
@4 := move (@14)
drop @12
drop @6
drop @4
Expand Down Expand Up @@ -1335,8 +1335,8 @@ fn test_crate::sum2<'_0, '_1>(@1: &'_0 (Slice<u32>), @2: &'_1 (Slice<u32>)) -> u
drop @21
drop @19
i@10 := copy (i@10) + const (1 : usize)
@25 := ()
@12 := move (@25)
@24 := ()
@12 := move (@24)
drop @13
continue 0
}
Expand All @@ -1346,8 +1346,8 @@ fn test_crate::sum2<'_0, '_1>(@1: &'_0 (Slice<u32>), @2: &'_1 (Slice<u32>)) -> u
}
drop @15
drop @14
@24 := ()
@11 := move (@24)
@25 := ()
@11 := move (@25)
drop @22
drop @13
drop @11
Expand Down Expand Up @@ -1568,13 +1568,13 @@ fn test_crate::ite()
drop @9
drop @11
drop @8
@13 := ()
@0 := move (@13)
@12 := ()
@0 := move (@12)
drop y@3
}
else {
@12 := ()
@0 := move (@12)
@13 := ()
@0 := move (@13)
}
drop @2
drop x@1
Expand Down Expand Up @@ -1619,8 +1619,8 @@ fn test_crate::zero_slice<'_0>(@1: &'_0 mut (Slice<u8>))
*(@14) := const (0 : u8)
drop @9
i@2 := copy (i@2) + const (1 : usize)
@12 := ()
@5 := move (@12)
@11 := ()
@5 := move (@11)
drop @6
continue 0
}
Expand All @@ -1630,8 +1630,8 @@ fn test_crate::zero_slice<'_0>(@1: &'_0 mut (Slice<u8>))
}
drop @8
drop @7
@11 := ()
@0 := move (@11)
@12 := ()
@0 := move (@12)
drop @10
drop @6
drop len@3
Expand Down Expand Up @@ -1731,8 +1731,8 @@ fn test_crate::sum_mut_slice<'_0>(@1: &'_0 mut (Slice<u32>)) -> u32
drop @10
drop @11
i@2 := copy (i@2) + const (1 : usize)
@14 := ()
@5 := move (@14)
@13 := ()
@5 := move (@13)
drop @6
continue 0
}
Expand All @@ -1742,8 +1742,8 @@ fn test_crate::sum_mut_slice<'_0>(@1: &'_0 mut (Slice<u32>)) -> u32
}
drop @8
drop @7
@13 := ()
@4 := move (@13)
@14 := ()
@4 := move (@14)
drop @12
drop @6
drop @4
Expand Down
8 changes: 4 additions & 4 deletions charon/tests/ui/comments.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,8 +83,8 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
drop @14
// Increment `i`
i@3 := copy (i@3) + const (1 : usize)
@24 := ()
@8 := move (@24)
@23 := ()
@8 := move (@23)
// Before end of loop
drop @9
continue 0
Expand All @@ -95,8 +95,8 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
}
drop @11
drop @10
@23 := ()
@7 := move (@23)
@24 := ()
@7 := move (@24)
drop @15
drop @9
drop @7
Expand Down
24 changes: 12 additions & 12 deletions charon/tests/ui/issue-297-cfg.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -746,19 +746,19 @@ fn test_crate::f2<'_0, '_1>(@1: &'_0 (Slice<u8>), @2: &'_1 mut (Slice<i16>)) ->
drop @39
drop @40
sampled@3 := copy (sampled@3) + const (1 : usize)
@50 := ()
@34 := move (@50)
@49 := ()
@34 := move (@49)
}
else {
drop @38
@49 := ()
@34 := move (@49)
@50 := ()
@34 := move (@50)
}
}
else {
drop @36
@49 := ()
@34 := move (@49)
@50 := ()
@34 := move (@50)
}
drop @37
drop @35
Expand All @@ -780,19 +780,19 @@ fn test_crate::f2<'_0, '_1>(@1: &'_0 (Slice<u8>), @2: &'_1 mut (Slice<i16>)) ->
drop @45
drop @46
sampled@3 := copy (sampled@3) + const (1 : usize)
@53 := ()
@10 := move (@53)
@52 := ()
@10 := move (@52)
}
else {
drop @44
@52 := ()
@10 := move (@52)
@53 := ()
@10 := move (@53)
}
}
else {
drop @42
@52 := ()
@10 := move (@52)
@53 := ()
@10 := move (@53)
}
drop @43
drop @41
Expand Down
10 changes: 5 additions & 5 deletions charon/tests/ui/issue-92-nonpositive-variant-indices.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,17 +18,17 @@ fn test_crate::main()
@fake_read(@1)
match @1 {
0 => {
@2 := ()
@0 := move (@2)
},
1 => {
@3 := ()
@0 := move (@3)
},
1 => {
2 => {
@4 := ()
@0 := move (@4)
},
2 => {
@2 := ()
@0 := move (@2)
},
}
drop @1
@0 := ()
Expand Down
56 changes: 28 additions & 28 deletions charon/tests/ui/loops.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1522,19 +1522,19 @@ fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize
},
1 => {
s@3 := copy (s@3) + const (1 : usize)
@30 := ()
@9 := move (@30)
@31 := ()
@9 := move (@31)
drop @12
drop @10
drop @9
@31 := ()
@8 := move (@31)
@32 := ()
@8 := move (@32)
continue 0
},
}
}
@32 := ()
@4 := move (@32)
@30 := ()
@4 := move (@30)
drop @12
drop @10
drop @9
Expand Down Expand Up @@ -1578,19 +1578,19 @@ fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize
},
1 => {
s@3 := copy (s@3) + const (1 : usize)
@34 := ()
@26 := move (@34)
@36 := ()
@26 := move (@36)
drop @29
drop @27
drop @26
@35 := ()
@8 := move (@35)
@37 := ()
@8 := move (@37)
continue 0
},
}
}
@36 := ()
@18 := move (@36)
@34 := ()
@18 := move (@34)
drop @29
drop @27
drop @26
Expand All @@ -1599,8 +1599,8 @@ fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize
drop @21
drop @19
drop @18
@37 := ()
@8 := move (@37)
@35 := ()
@8 := move (@35)
continue 0
},
}
Expand Down Expand Up @@ -1733,20 +1733,20 @@ fn test_crate::loop_inside_if(@1: bool, @2: u32) -> u32
@16 := copy (i@15)
s@4 := copy (s@4) + move (@16)
drop @16
@17 := ()
@11 := move (@17)
@18 := ()
@11 := move (@18)
drop i@15
drop @14
drop @12
drop @11
@18 := ()
@10 := move (@18)
@19 := ()
@10 := move (@19)
continue 0
},
}
}
@19 := ()
@5 := move (@19)
@17 := ()
@5 := move (@17)
drop @14
drop @12
drop @11
Expand Down Expand Up @@ -1852,8 +1852,8 @@ fn test_crate::sum_array<const N : usize>(@1: Array<u32, const N : usize>) -> u3
drop @8
drop @9
i@2 := copy (i@2) + const (1 : usize)
@12 := ()
@5 := move (@12)
@11 := ()
@5 := move (@11)
drop @6
continue 0
}
Expand All @@ -1862,8 +1862,8 @@ fn test_crate::sum_array<const N : usize>(@1: Array<u32, const N : usize>) -> u3
}
}
drop @7
@11 := ()
@4 := move (@11)
@12 := ()
@4 := move (@12)
drop @10
drop @6
drop @4
Expand Down Expand Up @@ -1982,8 +1982,8 @@ fn test_crate::clear<'_0>(@1: &'_0 mut (alloc::vec::Vec<u32, alloc::alloc::Globa
*(@8) := const (0 : u32)
drop @8
i@2 := copy (i@2) + const (1 : usize)
@13 := ()
@3 := move (@13)
@12 := ()
@3 := move (@12)
drop @4
continue 0
}
Expand All @@ -1993,8 +1993,8 @@ fn test_crate::clear<'_0>(@1: &'_0 mut (alloc::vec::Vec<u32, alloc::alloc::Globa
}
drop @6
drop @5
@12 := ()
@0 := move (@12)
@13 := ()
@0 := move (@13)
drop @11
drop @4
drop i@2
Expand Down
Loading

0 comments on commit e6ff54c

Please sign in to comment.