Skip to content

Commit dae6e7f

Browse files
smowtonsmowton
authored
Merge pull request #5082 from smowton/smowton/feature/ensure-one-backedge-per-target
Add pass to (try to) ensure a single backedge per loop header
2 parents a7c1018 + 82f239c commit dae6e7f

File tree

28 files changed

+383
-5
lines changed

28 files changed

+383
-5
lines changed

‎regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/test.c

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
int main(int argc, char **argv)
2+
{
3+
int i = 0;
4+
do
5+
{
6+
++i;
7+
if(i == 5)
8+
continue;
9+
++i;
10+
} while(i < 10);
11+
}

‎regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/with-transform.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.c
3+
--ensure-one-backedge-per-target --show-natural-loops
4+
^2 is head of \{ 2, 3, 4, 5, 6, 7 \(backedge\) \}$
5+
^EXIT=0$
6+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/without-transform.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.c
3+
--show-natural-loops
4+
^2 is head of \{ 2, 3, 4, 5, 6, 7 \(backedge\) \}$
5+
^EXIT=0$
6+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-for-loop/test.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
int main(int argc, char **argv)
2+
{
3+
for(int i = 0; i < 10; ++i)
4+
{
5+
++i;
6+
if(i == 5)
7+
continue;
8+
--i;
9+
}
10+
}

‎regression/goto-instrument/ensure-one-backedge-per-target-for-loop/with-transform.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.c
3+
--ensure-one-backedge-per-target --show-natural-loops
4+
^2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9 \(backedge\) \}$
5+
^EXIT=0$
6+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-for-loop/without-transform.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.c
3+
--show-natural-loops
4+
^2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9 \(backedge\) \}$
5+
^EXIT=0$
6+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/test.c

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
int main(int argc, char **argv)
2+
{
3+
int i = 0;
4+
top:
5+
{
6+
++i;
7+
if(i == 5)
8+
goto top;
9+
++i;
10+
}
11+
if(i < 10)
12+
goto top;
13+
14+
i = 0;
15+
top2:
16+
{
17+
++i;
18+
if(i == 5)
19+
goto top2;
20+
++i;
21+
}
22+
if(i < 10)
23+
goto top2;
24+
}

‎regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/with-transform.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
test.c
3+
--ensure-one-backedge-per-target --show-natural-loops
4+
^2 is head of \{ 2, 3, 4, 5, 6, 7, 8 \(backedge\) \}
5+
^12 is head of \{ 12, 13, 14, 15, 16, 17, 18 \(backedge\) \}
6+
^EXIT=0$
7+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/without-transform.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
test.c
3+
--show-natural-loops
4+
^2 is head of \{ 2, 3 \(backedge\), 4, 5, 6, 7 \(backedge\) \}
5+
^11 is head of \{ 11, 12 \(backedge\), 13, 14, 15, 16 \(backedge\) \}
6+
^EXIT=0$
7+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/test.c

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
int main(int argc, char **argv)
2+
{
3+
int i = 0;
4+
top:
5+
{
6+
++i;
7+
if(i == 5)
8+
goto top;
9+
if(i == 6)
10+
goto top;
11+
if(i == 7)
12+
goto top;
13+
if(i == 8)
14+
goto top;
15+
++i;
16+
}
17+
if(i < 10)
18+
goto top;
19+
}

‎regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/with-transform.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.c
3+
--ensure-one-backedge-per-target --show-natural-loops
4+
^2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17 \(backedge\) \}$
5+
^EXIT=0$
6+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/without-transform.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.c
3+
--show-natural-loops
4+
^2 is head of \{ 2, 3 \(backedge\), 4, 5, 6 \(backedge\), 7, 8, 9 \(backedge\), 10, 11, 12 \(backedge\), 13, 14, 15, 16 \(backedge\) \}$
5+
^EXIT=0$
6+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/test.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
int main(int argc, char **argv)
2+
{
3+
int i = 0;
4+
top:
5+
{
6+
++i;
7+
if(i == 5)
8+
goto top;
9+
if(i > 10)
10+
return 0;
11+
++i;
12+
}
13+
goto top;
14+
}

‎regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/with-transform.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.c
3+
--ensure-one-backedge-per-target --show-natural-loops
4+
^2 is head of \{ 2, 3, 4, 5, 6, 10, 11, 12 \(backedge\) \}$
5+
^EXIT=0$
6+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/without-transform.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.c
3+
--show-natural-loops
4+
^2 is head of \{ 2, 3 \(backedge\), 4, 5, 6, 10, 11, 12 \(backedge\) \}$
5+
^EXIT=0$
6+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-goto-top/test.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
int main(int argc, char **argv)
2+
{
3+
int i = 0;
4+
top:
5+
{
6+
++i;
7+
if(i == 5)
8+
goto top;
9+
++i;
10+
}
11+
if(i < 10)
12+
goto top;
13+
}

‎regression/goto-instrument/ensure-one-backedge-per-target-goto-top/with-transform.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.c
3+
--ensure-one-backedge-per-target --show-natural-loops
4+
^2 is head of \{ 2, 3, 4, 5, 6, 7, 8 \(backedge\) \}$
5+
^EXIT=0$
6+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-goto-top/without-transform.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.c
3+
--show-natural-loops
4+
^2 is head of \{ 2, 3 \(backedge\), 4, 5, 6, 7 \(backedge\) \}$
5+
^EXIT=0$
6+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-while-loop/test.c

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
int main(int argc, char **argv)
2+
{
3+
int i = 0;
4+
while(i < 10)
5+
{
6+
++i;
7+
if(i == 5)
8+
continue;
9+
++i;
10+
}
11+
}

‎regression/goto-instrument/ensure-one-backedge-per-target-while-loop/with-transform.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.c
3+
--ensure-one-backedge-per-target --show-natural-loops
4+
^2 is head of \{ 2, 3, 4, 5, 6, 7, 8 \(backedge\) \}$
5+
^EXIT=0$
6+
^SIGNAL=0$

‎regression/goto-instrument/ensure-one-backedge-per-target-while-loop/without-transform.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.c
3+
--show-natural-loops
4+
^2 is head of \{ 2, 3, 4, 5, 6, 7, 8 \(backedge\) \}$
5+
^EXIT=0$
6+
^SIGNAL=0$

‎regression/goto-instrument/natural-loops-multiple-backedges/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--show-natural-loops
4-
0 is head of \{ [0124], [0124], [0124], [0124] \}
4+
0 is head of \{ 0, 1, 2 \(backedge\), 4 \(backedge\) \}
55
^EXIT=0$
66
^SIGNAL=0$
77
--

‎src/analyses/natural_loops.h

Lines changed: 15 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -281,13 +281,24 @@ void natural_loops_templatet<P, T>::output(std::ostream &out) const
281281
{
282282
unsigned n=loop.first->location_number;
283283

284+
std::unordered_set<std::size_t> backedge_location_numbers;
285+
for(const auto &backedge : loop.first->incoming_edges)
286+
backedge_location_numbers.insert(backedge->location_number);
287+
284288
out << n << " is head of { ";
285-
for(typename natural_loopt::const_iterator l_it=loop.second.begin();
286-
l_it!=loop.second.end(); ++l_it)
289+
290+
std::vector<std::size_t> loop_location_numbers;
291+
for(const auto &loop_instruction_it : loop.second)
292+
loop_location_numbers.push_back(loop_instruction_it->location_number);
293+
std::sort(loop_location_numbers.begin(), loop_location_numbers.end());
294+
295+
for(const auto location_number : loop_location_numbers)
287296
{
288-
if(l_it!=loop.second.begin())
297+
if(location_number != loop_location_numbers.at(0))
289298
out << ", ";
290-
out << (*l_it)->location_number;
299+
out << location_number;
300+
if(backedge_location_numbers.count(location_number))
301+
out << " (backedge)";
291302
}
292303
out << " }\n";
293304
}

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
2424
#include <util/version.h>
2525

2626
#include <goto-programs/class_hierarchy.h>
27+
#include <goto-programs/ensure_one_backedge_per_target.h>
2728
#include <goto-programs/goto_convert_functions.h>
2829
#include <goto-programs/goto_inline.h>
2930
#include <goto-programs/interpreter.h>
@@ -1579,6 +1580,12 @@ void goto_instrument_parse_optionst::instrument_goto_program()
15791580
reachability_slicer(goto_model);
15801581
}
15811582

1583+
if(cmdline.isset("ensure-one-backedge-per-target"))
1584+
{
1585+
log.status() << "Trying to force one backedge per target" << messaget::eom;
1586+
ensure_one_backedge_per_target(goto_model);
1587+
}
1588+
15821589
// recalculate numbers, etc.
15831590
goto_model.goto_functions.update();
15841591
}

‎src/goto-instrument/goto_instrument_parse_options.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -111,6 +111,7 @@ Author: Daniel Kroening, [email protected]
111111
"(validate-goto-binary)" \
112112
OPT_VALIDATE \
113113
OPT_ANSI_C_LANGUAGE \
114+
"(ensure-one-backedge-per-target)" \
114115
// empty last line
115116

116117
// clang-format on

‎src/goto-programs/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ SRC = adjust_float_expressions.cpp \
66
destructor.cpp \
77
destructor_tree.cpp \
88
elf_reader.cpp \
9+
ensure_one_backedge_per_target.cpp \
910
format_strings.cpp \
1011
goto_asm.cpp \
1112
goto_clean_expr.cpp \

0 commit comments

Comments
 (0)