Skip to content

Commit eaf8cb3

Browse files
authored
Merge pull request #5083 from smowton/smowton/feature/sese-regions-pass
Add single-entry, single-exit regions pass
2 parents dae6e7f + a808a4f commit eaf8cb3

File tree

41 files changed

+884
-0
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

41 files changed

+884
-0
lines changed

jbmc/src/java_bytecode/java_local_variable_table.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ struct procedure_local_cfg_baset<
4040
typedef std::map<java_bytecode_convert_methodt::method_offsett,
4141
java_bytecode_convert_methodt::method_offsett>
4242
entry_mapt;
43+
typedef std::size_t entryt;
4344
entry_mapt entry_map;
4445

4546
procedure_local_cfg_baset() {}
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
int main(int argc, char **argv)
2+
{
3+
// Function containing two SESE regions,
4+
// one per if-block.
5+
if(argc % 5)
6+
{
7+
if(argc % 2)
8+
{
9+
++argc;
10+
}
11+
else
12+
{
13+
--argc;
14+
}
15+
}
16+
else
17+
{
18+
++argc;
19+
}
20+
21+
return argc;
22+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.c
3+
--show-sese-regions
4+
^Region starting at \(1, [0-9]+\) IF !\(argc % 2 != 0\) THEN GOTO 1 ends at \(5, [0-9]+\) 2: SKIP$
5+
^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(8, [0-9]+\) 4: SKIP$
6+
^Function contains 2 single-entry, single-exit regions:$
7+
^EXIT=0$
8+
^SIGNAL=0$
Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
int main(int argc, char **argv)
2+
{
3+
// A function containing 2 SESE regions: one delimiting the outer
4+
// if-block, and one delimiting the while-loop.
5+
6+
if(argc % 5)
7+
{
8+
int x = 0;
9+
while(x < 10)
10+
{
11+
++x;
12+
}
13+
}
14+
else
15+
{
16+
--argc;
17+
}
18+
19+
return argc;
20+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.c
3+
--show-sese-regions
4+
^Function contains 2 single-entry, single-exit regions:$
5+
^Region starting at \(2, [0-9]+\) x = 0; ends at \(6, [0-9]+\) 2: SKIP$
6+
^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(10, [0-9]+\) 4: SKIP$
7+
^EXIT=0$
8+
^SIGNAL=0$
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
int main(int argc, char **argv)
2+
{
3+
// A function containing 2 SESE regions, one for the outer if-block
4+
// and one for the while-loop, despite a break edge
5+
6+
if(argc % 5)
7+
{
8+
int x = 0;
9+
while(x < 10)
10+
{
11+
if(x % 7)
12+
break;
13+
++x;
14+
}
15+
}
16+
else
17+
{
18+
--argc;
19+
}
20+
21+
return argc;
22+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.c
3+
--show-sese-regions
4+
^Function contains 2 single-entry, single-exit regions:$
5+
^Region starting at \(2, [0-9]+\) x = 0; ends at \(9, [0-9]+\) 2: SKIP$
6+
^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(13, [0-9]+\) 4: SKIP$
7+
^EXIT=0$
8+
^SIGNAL=0$
Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
int main(int argc, char **argv)
2+
{
3+
// A function containing 3 SESE regions, one for the outer if-block
4+
// and one for the while-loop, despite a continue edge, and one for
5+
// the conditional inside the loop.
6+
7+
if(argc % 5)
8+
{
9+
int x = 0;
10+
while(x < 10)
11+
{
12+
if(x % 7)
13+
{
14+
++x;
15+
continue;
16+
}
17+
++x;
18+
}
19+
}
20+
else
21+
{
22+
--argc;
23+
}
24+
25+
return argc;
26+
}
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
test.c
3+
--show-sese-regions
4+
^Function contains 3 single-entry, single-exit regions:$
5+
^Region starting at \(4, [0-9]+\) IF !\(x % 7 != 0\) THEN GOTO 2 ends at \(9, [0-9]+\) 3: GOTO 1$
6+
^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 5 ends at \(14, [0-9]+\) 6: SKIP$
7+
^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 4: SKIP$
8+
^EXIT=0$
9+
^SIGNAL=0$
Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
int main(int argc, char **argv)
2+
{
3+
// A function containing 2 SESE regions, one for the outer if-block
4+
// and one for the while-loop, despite a continue edge that branches
5+
// directly to the top of the loop.
6+
7+
if(argc % 5)
8+
{
9+
int x = 0;
10+
top_continue:
11+
while(x < 10)
12+
{
13+
if(x % 7)
14+
{
15+
++x;
16+
goto top_continue;
17+
}
18+
++x;
19+
}
20+
}
21+
else
22+
{
23+
--argc;
24+
}
25+
26+
return argc;
27+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
FUTURE
2+
test.c
3+
--show-sese-regions
4+
^Function contains 2 single-entry, single-exit regions:$
5+
^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 3: SKIP$
6+
^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$
7+
^EXIT=0$
8+
^SIGNAL=0$
9+
--
10+
--
11+
These regions cannot currently be identified because the function contains a loop with two backedges.
Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
int main(int argc, char **argv)
2+
{
3+
// A function containing 2 SESE regions: one delimiting the outer
4+
// if-block, and one delimiting the do-while loop.
5+
6+
if(argc % 5)
7+
{
8+
int x = 0;
9+
do
10+
{
11+
++x;
12+
} while(x < 10);
13+
}
14+
else
15+
{
16+
--argc;
17+
}
18+
19+
return argc;
20+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.c
3+
--show-sese-regions
4+
^Function contains 2 single-entry, single-exit regions:$
5+
^Region starting at \(2, [0-9]+\) x = 0; ends at \(5, [0-9]+\) SKIP$
6+
^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 2 ends at \(9, [0-9]+\) 3: SKIP$
7+
^EXIT=0$
8+
^SIGNAL=0$
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
int main(int argc, char **argv)
2+
{
3+
// A function containing 2 SESE regions, one for the outer if-block
4+
// and one for the while-loop, despite a break edge
5+
6+
if(argc % 5)
7+
{
8+
int x = 0;
9+
do
10+
{
11+
if(x % 7)
12+
break;
13+
++x;
14+
} while(x < 10);
15+
}
16+
else
17+
{
18+
--argc;
19+
}
20+
21+
return argc;
22+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.c
3+
--show-sese-regions
4+
^Function contains 2 single-entry, single-exit regions:$
5+
^Region starting at \(2, [0-9]+\) x = 0; ends at \(8, [0-9]+\) 2: SKIP$
6+
^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(12, [0-9]+\) 4: SKIP$
7+
^EXIT=0$
8+
^SIGNAL=0$
Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
int main(int argc, char **argv)
2+
{
3+
// A function containing 3 SESE regions, one for the outer if-block
4+
// and one for the while-loop, despite a continue edge, and one for
5+
// the conditional inside the loop.
6+
7+
if(argc % 5)
8+
{
9+
int x = 0;
10+
do
11+
{
12+
if(x % 7)
13+
{
14+
++x;
15+
continue;
16+
}
17+
++x;
18+
} while(x < 10);
19+
}
20+
else
21+
{
22+
--argc;
23+
}
24+
25+
return argc;
26+
}
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
test.c
3+
--show-sese-regions
4+
^Function contains 3 single-entry, single-exit regions:$
5+
^Region starting at \(3, [0-9]+\) 1: IF !\(x % 7 != 0\) THEN GOTO 2 ends at \(8, [0-9]+\) 3: IF x < 10 THEN GOTO 1$
6+
^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(13, [0-9]+\) 5: SKIP$
7+
^Region starting at \(2, [0-9]+\) x = 0; ends at \(9, [0-9]+\) SKIP$
8+
^EXIT=0$
9+
^SIGNAL=0$
Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
int main(int argc, char **argv)
2+
{
3+
// A function containing 2 SESE regions, one for the outer if-block
4+
// and one for the while-loop, despite a continue edge that branches
5+
// directly to the top of the loop.
6+
7+
if(argc % 5)
8+
{
9+
int x = 0;
10+
top_continue:
11+
do
12+
{
13+
if(x % 7)
14+
{
15+
++x;
16+
goto top_continue;
17+
}
18+
++x;
19+
} while(x < 10);
20+
}
21+
else
22+
{
23+
--argc;
24+
}
25+
26+
return argc;
27+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
FUTURE
2+
test.c
3+
--show-sese-regions
4+
^Function contains 2 single-entry, single-exit regions:$
5+
^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 3: SKIP$
6+
^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$
7+
^EXIT=0$
8+
^SIGNAL=0$
9+
--
10+
--
11+
The program test.c produces what is effectively two nested loops, but natural-loop
12+
analysis conflates the two. This would risk identifying a region that straddles the
13+
boundary between those two loops, and so SESE analysis currently conservatively refrains
14+
from identifying the regions.
Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
int main(int argc, char **argv)
2+
{
3+
// Function containing two SESE regions: the inner if-block and the whole
4+
// function. The outer if-block is specifically *not* a region due to
5+
// a spoiling incoming edge.
6+
if(argc % 7)
7+
goto target;
8+
9+
if(argc % 5)
10+
{
11+
if(argc % 2)
12+
{
13+
++argc;
14+
}
15+
else
16+
{
17+
--argc;
18+
}
19+
}
20+
else
21+
{
22+
target:
23+
++argc;
24+
}
25+
26+
return argc;
27+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.c
3+
--show-sese-regions
4+
^Function contains 2 single-entry, single-exit regions:$
5+
^Region starting at \(4, [0-9]+\) IF !\(argc % 2 != 0\) THEN GOTO 1 ends at \(8, [0-9]+\) 2: SKIP$
6+
^Region starting at \(0, [0-9]+\) IF argc % 7 != 0 THEN GOTO 3 ends at \(11, [0-9]+\) 4: SKIP$
7+
^EXIT=0$
8+
^SIGNAL=0$
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
int main(int argc, char **argv)
2+
{
3+
// Function containing two SESE regions: the inner if-block and the whole
4+
// function. The outer if-block is specifically *not* a region due to
5+
// a spoiling outgoing edge,
6+
if(argc % 5)
7+
{
8+
if(argc % 2)
9+
{
10+
++argc;
11+
}
12+
else
13+
{
14+
--argc;
15+
}
16+
}
17+
else
18+
{
19+
return argc - 1;
20+
}
21+
22+
return argc;
23+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.c
3+
--show-sese-regions
4+
^Function contains 2 single-entry, single-exit regions:$
5+
^Region starting at \(1, [0-9]+\) IF !\(argc % 2 != 0\) THEN GOTO 1 ends at \(5, [0-9]+\) 2: SKIP$
6+
^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(12, [0-9]+\) 5: END_FUNCTION$
7+
^EXIT=0$
8+
^SIGNAL=0$

0 commit comments

Comments
 (0)