diff --git a/tests/misc/oracle/dom_graph.f.dot b/tests/misc/oracle/dom_graph.f.dot new file mode 100644 index 0000000000000000000000000000000000000000..ca126d8e69606de83dd763955586838d1244081d --- /dev/null +++ b/tests/misc/oracle/dom_graph.f.dot @@ -0,0 +1,56 @@ +digraph G { + label="Dominators for function f"; + node [shape=box, style="filled", ]; + 1 [label="/* sid:1 */ +c = 12;", ]; + 3 [label="/* sid:3 */ +if (c) { + /* sid:4 */ + test: c = 42; + /* sid:5 */ + goto test; +} +else { + /* sid:6 */ + c = 12; + /* sid:53 */ + { + /* sid:8 */ + __retres = c; + /* sid:54 */ + goto return_label; + } +}", + ]; + 4 [label="/* sid:4 */ +test: c = 42;", ]; + 53 [label="/* sid:53 */ +{ + /* sid:8 */ + __retres = c; + /* sid:54 */ + goto return_label; +}", + ]; + 5 [label="/* sid:5 */ +goto test;", ]; + 54 [label="/* sid:54 */ +goto return_label;", ]; + 6 [label="/* sid:6 */ +c = 12;", ]; + 55 [label="/* sid:55 */ +return_label: return __retres;", ]; + 8 [label="/* sid:8 */ +__retres = c;", ]; + + + 1 -> 3; + 3 -> 4; + 6 -> 53; + 4 -> 5; + 8 -> 54; + 3 -> 6; + 54 -> 55; + 53 -> 8; + + } diff --git a/tests/misc/oracle/dom_graph.g.dot b/tests/misc/oracle/dom_graph.g.dot new file mode 100644 index 0000000000000000000000000000000000000000..8d9ff3a679f7c9177486a7097ff2c4094561cfdd --- /dev/null +++ b/tests/misc/oracle/dom_graph.g.dot @@ -0,0 +1,63 @@ +digraph G { + label="Dominators for function g"; + node [shape=box, style="filled", ]; + 16 [label="/* sid:16 */ +c = 12;", ]; + 18 [label="/* sid:18 */ +__retres = c;", ]; + 20 [label="/* sid:20 */ +__retres = c;", ]; + 57 [label="/* sid:57 */ +{ + /* sid:18 */ + __retres = c; + /* sid:58 */ + goto return_label; +}", + ]; + 58 [label="/* sid:58 */ +goto return_label;", ]; + 10 [label="/* sid:10 */ +c = 12;", ]; + 59 [label="/* sid:59 */ +return_label: return __retres;", ]; + 12 [label="/* sid:12 */ +if (c) { + /* sid:13 */ + goto test; + /* sid:14 */ + c += 1; + /* sid:15 */ + test: c = 42; +} +else { + /* sid:16 */ + c = 12; + /* sid:57 */ + { + /* sid:18 */ + __retres = c; + /* sid:58 */ + goto return_label; + } +}", + ]; + 13 [label="/* sid:13 */ +goto test;", ]; + 14 [label="/* sid:14 */ +c += 1;", ]; + 15 [label="/* sid:15 */ +test: c = 42;", ]; + + + 12 -> 16; + 57 -> 18; + 15 -> 20; + 16 -> 57; + 18 -> 58; + 12 -> 59; + 10 -> 12; + 12 -> 13; + 13 -> 15; + + } diff --git a/tests/misc/oracle/dom_graph.h.dot b/tests/misc/oracle/dom_graph.h.dot new file mode 100644 index 0000000000000000000000000000000000000000..2826acff315de2ec5020301ef387f3faa4f016dd --- /dev/null +++ b/tests/misc/oracle/dom_graph.h.dot @@ -0,0 +1,113 @@ +digraph G { + label="Dominators for function h"; + node [shape=box, style="filled", ]; + 33 [label="/* sid:33 */ +j += 1;", ]; + 34 [label="/* sid:34 */ +stop();", ]; + 36 [label="/* sid:36 */ +return x;", ]; + 22 [label="/* sid:22 */ +{ + /* sid:23 */ + int j = 0; + /* sid:24 */ + while (1) { + /* sid:26 */ + if (j < 10) { + + } + else { + /* sid:27 */ + break; + } + /* sid:28 */ + { + /* sid:30 */ + if (j % 2 == 0) { + /* sid:31 */ + x += 1; + } + else { + + } + } + /* sid:33 */ + j += 1; + } +}", + ]; + 23 [label="/* sid:23 */ +int j = 0;", ]; + 24 [label="/* sid:24 */ +while (1) { + /* sid:26 */ + if (j < 10) { + + } + else { + /* sid:27 */ + break; + } + /* sid:28 */ + { + /* sid:30 */ + if (j % 2 == 0) { + /* sid:31 */ + x += 1; + } + else { + + } + } + /* sid:33 */ + j += 1; +}", + ]; + 26 [label="/* sid:26 */ +if (j < 10) { + +} +else { + /* sid:27 */ + break; +}", + ]; + 27 [label="/* sid:27 */ +break;", ]; + 28 [label="/* sid:28 */ +{ + /* sid:30 */ + if (j % 2 == 0) { + /* sid:31 */ + x += 1; + } + else { + + } +}", + ]; + 30 [label="/* sid:30 */ +if (j % 2 == 0) { + /* sid:31 */ + x += 1; +} +else { + +}", + ]; + 31 [label="/* sid:31 */ +x += 1;", ]; + + + 30 -> 33; + 27 -> 34; + 22 -> 23; + 23 -> 24; + 24 -> 26; + 26 -> 27; + 26 -> 28; + 28 -> 30; + 30 -> 31; + + } diff --git a/tests/misc/oracle/dom_graph.i.dot b/tests/misc/oracle/dom_graph.i.dot new file mode 100644 index 0000000000000000000000000000000000000000..9a4bece54956587ce9dae0bd4f0b35284a442c10 --- /dev/null +++ b/tests/misc/oracle/dom_graph.i.dot @@ -0,0 +1,76 @@ +digraph G { + label="Dominators for function i"; + node [shape=box, style="filled", ]; + 48 [label="/* sid:48 */ +{ + /* sid:49 */ + x += 1; + /* sid:50 */ + loop: ; +}", + ]; + 49 [label="/* sid:49 */ +x += 1;", ]; + 50 [label="/* sid:50 */ +loop: ;", ]; + 38 [label="/* sid:38 */ +int x = 0;", ]; + 40 [label="/* sid:40 */ +if (nondet) { + /* sid:41 */ + goto loop; +} +else { + +}", + ]; + 41 [label="/* sid:41 */ +goto loop;", ]; + 43 [label="/* sid:43 */ +x = 1;", ]; + 44 [label="/* sid:44 */ +while (1) { + /* sid:46 */ + if (x < 10) { + + } + else { + /* sid:47 */ + break; + } + /* sid:48 */ + { + /* sid:49 */ + x += 1; + /* sid:50 */ + loop: ; + } +}", + ]; + 62 [label="/* sid:62 */ +return;", ]; + 46 [label="/* sid:46 */ +if (x < 10) { + +} +else { + /* sid:47 */ + break; +}", + ]; + 47 [label="/* sid:47 */ +break;", ]; + + + 46 -> 48; + 48 -> 49; + 40 -> 50; + 38 -> 40; + 40 -> 41; + 40 -> 43; + 40 -> 44; + 47 -> 62; + 44 -> 46; + 46 -> 47; + + } diff --git a/tests/misc/oracle/postdom_graph.f.dot b/tests/misc/oracle/postdom_graph.f.dot new file mode 100644 index 0000000000000000000000000000000000000000..71ad2d4f34a6fa5eecb47ace6feff3ac300b10d7 --- /dev/null +++ b/tests/misc/oracle/postdom_graph.f.dot @@ -0,0 +1,54 @@ +digraph G { + label="PostDominators for function f"; + node [shape=box, style="filled", ]; + 1 [label="/* sid:1 */ +c = 12;", ]; + 3 [label="/* sid:3 */ +if (c) { + /* sid:4 */ + test: c = 42; + /* sid:5 */ + goto test; +} +else { + /* sid:6 */ + c = 12; + /* sid:53 */ + { + /* sid:8 */ + __retres = c; + /* sid:54 */ + goto return_label; + } +}", + ]; + 4 [label="/* sid:4 */ +test: c = 42;", ]; + 5 [label="/* sid:5 */ +goto test;", ]; + 53 [label="/* sid:53 */ +{ + /* sid:8 */ + __retres = c; + /* sid:54 */ + goto return_label; +}", + ]; + 54 [label="/* sid:54 */ +goto return_label;", ]; + 6 [label="/* sid:6 */ +c = 12;", ]; + 55 [label="/* sid:55 */ +return_label: return __retres;", ]; + 8 [label="/* sid:8 */ +__retres = c;", ]; + + + 3 -> 1; + 6 -> 3; + 8 -> 53; + 55 -> 54; + 53 -> 6; + 54 -> 8; + + } diff --git a/tests/misc/oracle/postdom_graph.g.dot b/tests/misc/oracle/postdom_graph.g.dot new file mode 100644 index 0000000000000000000000000000000000000000..b67c6c4a95ef21b02083a75cc6de251f36b93280 --- /dev/null +++ b/tests/misc/oracle/postdom_graph.g.dot @@ -0,0 +1,64 @@ +digraph G { + label="PostDominators for function g"; + node [shape=box, style="filled", ]; + 16 [label="/* sid:16 */ +c = 12;", ]; + 18 [label="/* sid:18 */ +__retres = c;", ]; + 20 [label="/* sid:20 */ +__retres = c;", ]; + 57 [label="/* sid:57 */ +{ + /* sid:18 */ + __retres = c; + /* sid:58 */ + goto return_label; +}", + ]; + 58 [label="/* sid:58 */ +goto return_label;", ]; + 10 [label="/* sid:10 */ +c = 12;", ]; + 59 [label="/* sid:59 */ +return_label: return __retres;", ]; + 12 [label="/* sid:12 */ +if (c) { + /* sid:13 */ + goto test; + /* sid:14 */ + c += 1; + /* sid:15 */ + test: c = 42; +} +else { + /* sid:16 */ + c = 12; + /* sid:57 */ + { + /* sid:18 */ + __retres = c; + /* sid:58 */ + goto return_label; + } +}", + ]; + 13 [label="/* sid:13 */ +goto test;", ]; + 14 [label="/* sid:14 */ +c += 1;", ]; + 15 [label="/* sid:15 */ +test: c = 42;", ]; + + + 57 -> 16; + 58 -> 18; + 59 -> 20; + 18 -> 57; + 59 -> 58; + 12 -> 10; + 59 -> 12; + 15 -> 13; + 15 -> 14; + 20 -> 15; + + } diff --git a/tests/misc/oracle/postdom_graph.h.dot b/tests/misc/oracle/postdom_graph.h.dot new file mode 100644 index 0000000000000000000000000000000000000000..0335859b42222119a397f5b135f16a7000b958d4 --- /dev/null +++ b/tests/misc/oracle/postdom_graph.h.dot @@ -0,0 +1,104 @@ +digraph G { + label="PostDominators for function h"; + node [shape=box, style="filled", ]; + 33 [label="/* sid:33 */ +j += 1;", ]; + 34 [label="/* sid:34 */ +stop();", ]; + 36 [label="/* sid:36 */ +return x;", ]; + 22 [label="/* sid:22 */ +{ + /* sid:23 */ + int j = 0; + /* sid:24 */ + while (1) { + /* sid:26 */ + if (j < 10) { + + } + else { + /* sid:27 */ + break; + } + /* sid:28 */ + { + /* sid:30 */ + if (j % 2 == 0) { + /* sid:31 */ + x += 1; + } + else { + + } + } + /* sid:33 */ + j += 1; + } +}", + ]; + 23 [label="/* sid:23 */ +int j = 0;", ]; + 24 [label="/* sid:24 */ +while (1) { + /* sid:26 */ + if (j < 10) { + + } + else { + /* sid:27 */ + break; + } + /* sid:28 */ + { + /* sid:30 */ + if (j % 2 == 0) { + /* sid:31 */ + x += 1; + } + else { + + } + } + /* sid:33 */ + j += 1; +}", + ]; + 26 [label="/* sid:26 */ +if (j < 10) { + +} +else { + /* sid:27 */ + break; +}", + ]; + 27 [label="/* sid:27 */ +break;", ]; + 28 [label="/* sid:28 */ +{ + /* sid:30 */ + if (j % 2 == 0) { + /* sid:31 */ + x += 1; + } + else { + + } +}", + ]; + 30 [label="/* sid:30 */ +if (j % 2 == 0) { + /* sid:31 */ + x += 1; +} +else { + +}", + ]; + 31 [label="/* sid:31 */ +x += 1;", ]; + + + + } diff --git a/tests/misc/oracle/postdom_graph.i.dot b/tests/misc/oracle/postdom_graph.i.dot new file mode 100644 index 0000000000000000000000000000000000000000..64c9cb923c32876d2623b6c6f46fb35effa107a6 --- /dev/null +++ b/tests/misc/oracle/postdom_graph.i.dot @@ -0,0 +1,76 @@ +digraph G { + label="PostDominators for function i"; + node [shape=box, style="filled", ]; + 48 [label="/* sid:48 */ +{ + /* sid:49 */ + x += 1; + /* sid:50 */ + loop: ; +}", + ]; + 49 [label="/* sid:49 */ +x += 1;", ]; + 50 [label="/* sid:50 */ +loop: ;", ]; + 38 [label="/* sid:38 */ +int x = 0;", ]; + 40 [label="/* sid:40 */ +if (nondet) { + /* sid:41 */ + goto loop; +} +else { + +}", + ]; + 41 [label="/* sid:41 */ +goto loop;", ]; + 43 [label="/* sid:43 */ +x = 1;", ]; + 44 [label="/* sid:44 */ +while (1) { + /* sid:46 */ + if (x < 10) { + + } + else { + /* sid:47 */ + break; + } + /* sid:48 */ + { + /* sid:49 */ + x += 1; + /* sid:50 */ + loop: ; + } +}", + ]; + 62 [label="/* sid:62 */ +return;", ]; + 46 [label="/* sid:46 */ +if (x < 10) { + +} +else { + /* sid:47 */ + break; +}", + ]; + 47 [label="/* sid:47 */ +break;", ]; + + + 49 -> 48; + 50 -> 49; + 44 -> 50; + 40 -> 38; + 44 -> 40; + 50 -> 41; + 44 -> 43; + 46 -> 44; + 47 -> 46; + 62 -> 47; + + } diff --git a/tests/misc/oracle/test_dominators.res.oracle b/tests/misc/oracle/test_dominators.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..0d6e7207b590df53de2142a8918ffb1c1553dadd --- /dev/null +++ b/tests/misc/oracle/test_dominators.res.oracle @@ -0,0 +1,388 @@ +[kernel] Parsing test_dominators.c (with preprocessing) +Computing for function f: +{ + int __retres; + /* sid:1 */ + c = 12; + /* sid:3 */ + if (c) { + /* sid:4 */ + test: c = 42; + /* sid:5 */ + goto test; + } + else { + /* sid:6 */ + c = 12; + /* sid:53 */ + { + /* sid:8 */ + __retres = c; + /* sid:54 */ + goto return_label; + } + } + /* sid:55 */ + return_label: return __retres; +} +[kernel] dot file generated in dom_graph.f.dot +[kernel] dot file generated in postdom_graph.f.dot +Immediate dominators of f (sid, idom, ipostdom): + (1, none, 3), (3, 1, 6), (4, 3, none), (5, 4, none), (6, 3, 53), + (53, 6, 8), (8, 53, 54), (54, 8, 55), (55, 54, none) +Nearest common ancestors/children of f (sid, sid, ancestor, children): + (1, 1, none, 3), (1, 3, none, 6), (1, 4, none, none), (1, 5, none, none), + (1, 6, none, 53), (1, 53, none, 8), (1, 8, none, 54), (1, 54, none, 55), + (1, 55, none, none), (3, 1, none, 6), (3, 3, 1, 6), (3, 4, 1, none), + (3, 5, 1, none), (3, 6, 1, 53), (3, 53, 1, 8), (3, 8, 1, 54), + (3, 54, 1, 55), (3, 55, 1, none), (4, 1, none, none), (4, 3, 1, none), + (4, 4, 3, none), (4, 5, 3, none), (4, 6, 3, none), (4, 53, 3, none), + (4, 8, 3, none), (4, 54, 3, none), (4, 55, 3, none), (5, 1, none, none), + (5, 3, 1, none), (5, 4, 3, none), (5, 5, 4, none), (5, 6, 3, none), + (5, 53, 3, none), (5, 8, 3, none), (5, 54, 3, none), (5, 55, 3, none), + (6, 1, none, 53), (6, 3, 1, 53), (6, 4, 3, none), (6, 5, 3, none), + (6, 6, 3, 53), (6, 53, 3, 8), (6, 8, 3, 54), (6, 54, 3, 55), + (6, 55, 3, none), (53, 1, none, 8), (53, 3, 1, 8), (53, 4, 3, none), + (53, 5, 3, none), (53, 6, 3, 8), (53, 53, 6, 8), (53, 8, 6, 54), + (53, 54, 6, 55), (53, 55, 6, none), (8, 1, none, 54), (8, 3, 1, 54), + (8, 4, 3, none), (8, 5, 3, none), (8, 6, 3, 54), (8, 53, 6, 54), + (8, 8, 53, 54), (8, 54, 53, 55), (8, 55, 53, none), (54, 1, none, 55), + (54, 3, 1, 55), (54, 4, 3, none), (54, 5, 3, none), (54, 6, 3, 55), + (54, 53, 6, 55), (54, 8, 53, 55), (54, 54, 8, 55), (54, 55, 8, none), + (55, 1, none, none), (55, 3, 1, none), (55, 4, 3, none), (55, 5, 3, none), + (55, 6, 3, none), (55, 53, 6, none), (55, 8, 53, none), (55, 54, 8, none), + (55, 55, 54, none) + +Computing for function g: +{ + int __retres; + /* sid:10 */ + c = 12; + /* sid:12 */ + if (c) { + /* sid:13 */ + goto test; + /* sid:14 */ + c += 1; + /* sid:15 */ + test: c = 42; + } + else { + /* sid:16 */ + c = 12; + /* sid:57 */ + { + /* sid:18 */ + __retres = c; + /* sid:58 */ + goto return_label; + } + } + /* sid:20 */ + __retres = c; + /* sid:59 */ + return_label: return __retres; +} +[kernel] dot file generated in dom_graph.g.dot +[kernel] dot file generated in postdom_graph.g.dot +Immediate dominators of g (sid, idom, ipostdom): + (10, none, 12), (12, 10, 59), (13, 12, 15), (14, none, 15), (15, 13, 20), + (16, 12, 57), (57, 16, 18), (18, 57, 58), (58, 18, 59), (20, 15, 59), + (59, 12, none) +Nearest common ancestors/children of g (sid, sid, ancestor, children): + (10, 10, none, 12), (10, 12, none, 59), (10, 13, none, 59), + (10, 14, none, 59), (10, 15, none, 59), (10, 16, none, 59), + (10, 57, none, 59), (10, 18, none, 59), (10, 58, none, 59), + (10, 20, none, 59), (10, 59, none, none), (12, 10, none, 59), + (12, 12, 10, 59), (12, 13, 10, 59), (12, 14, none, 59), (12, 15, 10, 59), + (12, 16, 10, 59), (12, 57, 10, 59), (12, 18, 10, 59), (12, 58, 10, 59), + (12, 20, 10, 59), (12, 59, 10, none), (13, 10, none, 59), (13, 12, 10, 59), + (13, 13, 12, 15), (13, 14, none, 15), (13, 15, 12, 20), (13, 16, 12, 59), + (13, 57, 12, 59), (13, 18, 12, 59), (13, 58, 12, 59), (13, 20, 12, 59), + (13, 59, 12, none), (14, 10, none, 59), (14, 12, none, 59), + (14, 13, none, 15), (14, 14, none, 15), (14, 15, none, 20), + (14, 16, none, 59), (14, 57, none, 59), (14, 18, none, 59), + (14, 58, none, 59), (14, 20, none, 59), (14, 59, none, none), + (15, 10, none, 59), (15, 12, 10, 59), (15, 13, 12, 20), (15, 14, none, 20), + (15, 15, 13, 20), (15, 16, 12, 59), (15, 57, 12, 59), (15, 18, 12, 59), + (15, 58, 12, 59), (15, 20, 13, 59), (15, 59, 12, none), (16, 10, none, 59), + (16, 12, 10, 59), (16, 13, 12, 59), (16, 14, none, 59), (16, 15, 12, 59), + (16, 16, 12, 57), (16, 57, 12, 18), (16, 18, 12, 58), (16, 58, 12, 59), + (16, 20, 12, 59), (16, 59, 12, none), (57, 10, none, 59), (57, 12, 10, 59), + (57, 13, 12, 59), (57, 14, none, 59), (57, 15, 12, 59), (57, 16, 12, 18), + (57, 57, 16, 18), (57, 18, 16, 58), (57, 58, 16, 59), (57, 20, 12, 59), + (57, 59, 12, none), (18, 10, none, 59), (18, 12, 10, 59), (18, 13, 12, 59), + (18, 14, none, 59), (18, 15, 12, 59), (18, 16, 12, 58), (18, 57, 16, 58), + (18, 18, 57, 58), (18, 58, 57, 59), (18, 20, 12, 59), (18, 59, 12, none), + (58, 10, none, 59), (58, 12, 10, 59), (58, 13, 12, 59), (58, 14, none, 59), + (58, 15, 12, 59), (58, 16, 12, 59), (58, 57, 16, 59), (58, 18, 57, 59), + (58, 58, 18, 59), (58, 20, 12, 59), (58, 59, 12, none), (20, 10, none, 59), + (20, 12, 10, 59), (20, 13, 12, 59), (20, 14, none, 59), (20, 15, 13, 59), + (20, 16, 12, 59), (20, 57, 12, 59), (20, 18, 12, 59), (20, 58, 12, 59), + (20, 20, 15, 59), (20, 59, 12, none), (59, 10, none, none), + (59, 12, 10, none), (59, 13, 12, none), (59, 14, none, none), + (59, 15, 12, none), (59, 16, 12, none), (59, 57, 12, none), + (59, 18, 12, none), (59, 58, 12, none), (59, 20, 12, none), + (59, 59, 12, none) + +Computing for function h: +{ + /* sid:22 */ + { + /* sid:23 */ + int j = 0; + /* sid:24 */ + while (1) { + /* sid:26 */ + if (j < 10) { + + } + else { + /* sid:27 */ + break; + } + /* sid:28 */ + { + /* sid:30 */ + if (j % 2 == 0) { + /* sid:31 */ + x += 1; + } + else { + + } + } + /* sid:33 */ + j += 1; + } + } + /* sid:34 */ + stop(); + /* sid:36 */ + return x; +} +[kernel] dot file generated in dom_graph.h.dot +[kernel] dot file generated in postdom_graph.h.dot +Immediate dominators of h (sid, idom, ipostdom): + (22, none, none), (23, 22, none), (24, 23, none), (26, 24, none), + (27, 26, none), (28, 26, none), (30, 28, none), (31, 30, none), + (33, 30, none), (34, 27, none), (36, none, none) +Nearest common ancestors/children of h (sid, sid, ancestor, children): + (22, 22, none, none), (22, 23, none, none), (22, 24, none, none), + (22, 26, none, none), (22, 27, none, none), (22, 28, none, none), + (22, 30, none, none), (22, 31, none, none), (22, 33, none, none), + (22, 34, none, none), (22, 36, none, none), (23, 22, none, none), + (23, 23, 22, none), (23, 24, 22, none), (23, 26, 22, none), + (23, 27, 22, none), (23, 28, 22, none), (23, 30, 22, none), + (23, 31, 22, none), (23, 33, 22, none), (23, 34, 22, none), + (23, 36, none, none), (24, 22, none, none), (24, 23, 22, none), + (24, 24, 23, none), (24, 26, 23, none), (24, 27, 23, none), + (24, 28, 23, none), (24, 30, 23, none), (24, 31, 23, none), + (24, 33, 23, none), (24, 34, 23, none), (24, 36, none, none), + (26, 22, none, none), (26, 23, 22, none), (26, 24, 23, none), + (26, 26, 24, none), (26, 27, 24, none), (26, 28, 24, none), + (26, 30, 24, none), (26, 31, 24, none), (26, 33, 24, none), + (26, 34, 24, none), (26, 36, none, none), (27, 22, none, none), + (27, 23, 22, none), (27, 24, 23, none), (27, 26, 24, none), + (27, 27, 26, none), (27, 28, 26, none), (27, 30, 26, none), + (27, 31, 26, none), (27, 33, 26, none), (27, 34, 26, none), + (27, 36, none, none), (28, 22, none, none), (28, 23, 22, none), + (28, 24, 23, none), (28, 26, 24, none), (28, 27, 26, none), + (28, 28, 26, none), (28, 30, 26, none), (28, 31, 26, none), + (28, 33, 26, none), (28, 34, 26, none), (28, 36, none, none), + (30, 22, none, none), (30, 23, 22, none), (30, 24, 23, none), + (30, 26, 24, none), (30, 27, 26, none), (30, 28, 26, none), + (30, 30, 28, none), (30, 31, 28, none), (30, 33, 28, none), + (30, 34, 26, none), (30, 36, none, none), (31, 22, none, none), + (31, 23, 22, none), (31, 24, 23, none), (31, 26, 24, none), + (31, 27, 26, none), (31, 28, 26, none), (31, 30, 28, none), + (31, 31, 30, none), (31, 33, 30, none), (31, 34, 26, none), + (31, 36, none, none), (33, 22, none, none), (33, 23, 22, none), + (33, 24, 23, none), (33, 26, 24, none), (33, 27, 26, none), + (33, 28, 26, none), (33, 30, 28, none), (33, 31, 30, none), + (33, 33, 30, none), (33, 34, 26, none), (33, 36, none, none), + (34, 22, none, none), (34, 23, 22, none), (34, 24, 23, none), + (34, 26, 24, none), (34, 27, 26, none), (34, 28, 26, none), + (34, 30, 26, none), (34, 31, 26, none), (34, 33, 26, none), + (34, 34, 27, none), (34, 36, none, none), (36, 22, none, none), + (36, 23, none, none), (36, 24, none, none), (36, 26, none, none), + (36, 27, none, none), (36, 28, none, none), (36, 30, none, none), + (36, 31, none, none), (36, 33, none, none), (36, 34, none, none), + (36, 36, none, none) + +Computing for function i: +{ + /* sid:38 */ + int x = 0; + /* sid:40 */ + if (nondet) { + /* sid:41 */ + goto loop; + } + else { + + } + /* sid:43 */ + x = 1; + /* sid:44 */ + while (1) { + /* sid:46 */ + if (x < 10) { + + } + else { + /* sid:47 */ + break; + } + /* sid:48 */ + { + /* sid:49 */ + x += 1; + /* sid:50 */ + loop: ; + } + } + /* sid:62 */ + return; +} +[kernel] dot file generated in dom_graph.i.dot +[kernel] dot file generated in postdom_graph.i.dot +Immediate dominators of i (sid, idom, ipostdom): + (38, none, 40), (40, 38, 44), (41, 40, 50), (43, 40, 44), (44, 40, 46), + (46, 44, 47), (47, 46, 62), (48, 46, 49), (49, 48, 50), (50, 40, 44), + (62, 47, none) +Nearest common ancestors/children of i (sid, sid, ancestor, children): + (38, 38, none, 40), (38, 40, none, 44), (38, 41, none, 44), + (38, 43, none, 44), (38, 44, none, 46), (38, 46, none, 47), + (38, 47, none, 62), (38, 48, none, 44), (38, 49, none, 44), + (38, 50, none, 44), (38, 62, none, none), (40, 38, none, 44), + (40, 40, 38, 44), (40, 41, 38, 44), (40, 43, 38, 44), (40, 44, 38, 46), + (40, 46, 38, 47), (40, 47, 38, 62), (40, 48, 38, 44), (40, 49, 38, 44), + (40, 50, 38, 44), (40, 62, 38, none), (41, 38, none, 44), (41, 40, 38, 44), + (41, 41, 40, 50), (41, 43, 40, 44), (41, 44, 40, 46), (41, 46, 40, 47), + (41, 47, 40, 62), (41, 48, 40, 50), (41, 49, 40, 50), (41, 50, 40, 44), + (41, 62, 40, none), (43, 38, none, 44), (43, 40, 38, 44), (43, 41, 40, 44), + (43, 43, 40, 44), (43, 44, 40, 46), (43, 46, 40, 47), (43, 47, 40, 62), + (43, 48, 40, 44), (43, 49, 40, 44), (43, 50, 40, 44), (43, 62, 40, none), + (44, 38, none, 46), (44, 40, 38, 46), (44, 41, 40, 46), (44, 43, 40, 46), + (44, 44, 40, 46), (44, 46, 40, 47), (44, 47, 40, 62), (44, 48, 40, 46), + (44, 49, 40, 46), (44, 50, 40, 46), (44, 62, 40, none), (46, 38, none, 47), + (46, 40, 38, 47), (46, 41, 40, 47), (46, 43, 40, 47), (46, 44, 40, 47), + (46, 46, 44, 47), (46, 47, 44, 62), (46, 48, 44, 47), (46, 49, 44, 47), + (46, 50, 40, 47), (46, 62, 44, none), (47, 38, none, 62), (47, 40, 38, 62), + (47, 41, 40, 62), (47, 43, 40, 62), (47, 44, 40, 62), (47, 46, 44, 62), + (47, 47, 46, 62), (47, 48, 46, 62), (47, 49, 46, 62), (47, 50, 40, 62), + (47, 62, 46, none), (48, 38, none, 44), (48, 40, 38, 44), (48, 41, 40, 50), + (48, 43, 40, 44), (48, 44, 40, 46), (48, 46, 44, 47), (48, 47, 46, 62), + (48, 48, 46, 49), (48, 49, 46, 50), (48, 50, 40, 44), (48, 62, 46, none), + (49, 38, none, 44), (49, 40, 38, 44), (49, 41, 40, 50), (49, 43, 40, 44), + (49, 44, 40, 46), (49, 46, 44, 47), (49, 47, 46, 62), (49, 48, 46, 50), + (49, 49, 48, 50), (49, 50, 40, 44), (49, 62, 46, none), (50, 38, none, 44), + (50, 40, 38, 44), (50, 41, 40, 44), (50, 43, 40, 44), (50, 44, 40, 46), + (50, 46, 40, 47), (50, 47, 40, 62), (50, 48, 40, 44), (50, 49, 40, 44), + (50, 50, 40, 44), (50, 62, 40, none), (62, 38, none, none), + (62, 40, 38, none), (62, 41, 40, none), (62, 43, 40, none), + (62, 44, 40, none), (62, 46, 44, none), (62, 47, 46, none), + (62, 48, 46, none), (62, 49, 46, none), (62, 50, 40, none), + (62, 62, 47, none) + +Dominators analysis: + Stmt:1 -> {1} + Stmt:3 -> {1,3} + Stmt:4 -> {1,3,4} + Stmt:5 -> {1,3,4,5} + Stmt:6 -> {1,3,6} + Stmt:8 -> {1,3,6,8,53} + Stmt:10 -> {10} + Stmt:12 -> {10,12} + Stmt:13 -> {10,12,13} + Stmt:14 -> Top + Stmt:15 -> {10,12,13,15} + Stmt:16 -> {10,12,16} + Stmt:18 -> {10,12,16,18,57} + Stmt:20 -> {10,12,13,15,20} + Stmt:22 -> {22} + Stmt:23 -> {22,23} + Stmt:24 -> {22,23,24} + Stmt:26 -> {22,23,24,26} + Stmt:27 -> {22,23,24,26,27} + Stmt:28 -> {22,23,24,26,28} + Stmt:30 -> {22,23,24,26,28,30} + Stmt:31 -> {22,23,24,26,28,30,31} + Stmt:33 -> {22,23,24,26,28,30,33} + Stmt:34 -> {22,23,24,26,27,34} + Stmt:36 -> Top + Stmt:38 -> {38} + Stmt:40 -> {38,40} + Stmt:41 -> {38,40,41} + Stmt:43 -> {38,40,43} + Stmt:44 -> {38,40,44} + Stmt:46 -> {38,40,44,46} + Stmt:47 -> {38,40,44,46,47} + Stmt:48 -> {38,40,44,46,48} + Stmt:49 -> {38,40,44,46,48,49} + Stmt:50 -> {38,40,50} + Stmt:53 -> {1,3,6,53} + Stmt:54 -> {1,3,6,8,53,54} + Stmt:55 -> {1,3,6,8,53,54,55} + Stmt:57 -> {10,12,16,57} + Stmt:58 -> {10,12,16,18,57,58} + Stmt:59 -> {10,12,59} + Stmt:62 -> {38,40,44,46,47,62} + +Postominators analysis: + Stmt:1 -> {1,3,6,8,53,54,55} + Stmt:3 -> {3,6,8,53,54,55} + Stmt:4 -> Top + Stmt:5 -> Top + Stmt:6 -> {6,8,53,54,55} + Stmt:8 -> {8,54,55} + Stmt:10 -> {10,12,59} + Stmt:12 -> {12,59} + Stmt:13 -> {13,15,20,59} + Stmt:14 -> {14,15,20,59} + Stmt:15 -> {15,20,59} + Stmt:16 -> {16,18,57,58,59} + Stmt:18 -> {18,58,59} + Stmt:20 -> {20,59} + Stmt:22 -> Top + Stmt:23 -> Top + Stmt:24 -> Top + Stmt:26 -> Top + Stmt:27 -> Top + Stmt:28 -> Top + Stmt:30 -> Top + Stmt:31 -> Top + Stmt:33 -> Top + Stmt:34 -> Top + Stmt:36 -> {36} + Stmt:38 -> {38,40,44,46,47,62} + Stmt:40 -> {40,44,46,47,62} + Stmt:41 -> {41,44,46,47,50,62} + Stmt:43 -> {43,44,46,47,62} + Stmt:44 -> {44,46,47,62} + Stmt:46 -> {46,47,62} + Stmt:47 -> {47,62} + Stmt:48 -> {44,46,47,48,49,50,62} + Stmt:49 -> {44,46,47,49,50,62} + Stmt:50 -> {44,46,47,50,62} + Stmt:53 -> {8,53,54,55} + Stmt:54 -> {54,55} + Stmt:55 -> {55} + Stmt:57 -> {18,57,58,59} + Stmt:58 -> {58,59} + Stmt:59 -> {59} + Stmt:62 -> {62} + +Invalidate tables, which should now be empty + +Dominators analysis: + Empty + +Postominators analysis: + Empty + +[kernel] Failure: Statement -1 is not part of a function +[kernel] Failure: No first statement in function stop +[kernel] Failure: No return statement in function stop +[kernel] Failure: cannot compute for a function without body stop diff --git a/tests/misc/test_dominators.c b/tests/misc/test_dominators.c new file mode 100644 index 0000000000000000000000000000000000000000..a461d101dce754b2061bc83fdf2bddc1a137e38f --- /dev/null +++ b/tests/misc/test_dominators.c @@ -0,0 +1,54 @@ +/* run.config + MODULE: @PTEST_NAME@ + LOG: postdom_graph.f.dot dom_graph.f.dot + LOG: postdom_graph.g.dot dom_graph.g.dot + LOG: postdom_graph.h.dot dom_graph.h.dot + LOG: postdom_graph.i.dot dom_graph.i.dot + OPT: -kernel-msg-key printer:sid -print-as-is +*/ + +void stop(void) __attribute__ ((noreturn)) ; + +int f (int c){ + c = 12; + if (c) { + test: c = 42; + goto test; + } + else { + c = 12; + return c; + } +} + +int g (int c){ + c = 12; + if (c) { + goto test; + c++; + test: c = 42; + } + else { + c = 12; + return c; + } + return c; +} + +int h(int x){ + for (int j = 0; j < 10; j++){ + if (j % 2 == 0) x++; + } + stop(); + return x; +} + +void i (int nondet) { + int x = 0; + if (nondet) goto loop; + x = 1; + while (x < 10) { + x++; + loop: ; + } +} diff --git a/tests/misc/test_dominators.ml b/tests/misc/test_dominators.ml new file mode 100644 index 0000000000000000000000000000000000000000..8fad610175916d06704c810599a042884387aa2d --- /dev/null +++ b/tests/misc/test_dominators.ml @@ -0,0 +1,126 @@ +open Cil_types + +module StmtSet = Cil_datatype.Stmt.Hptset + +let get = function + | None -> "none" + | Some stmt -> string_of_int stmt.sid + +let pp_res = + Pretty_utils.pp_list ~pre:"(" ~sep:", " ~suf:")" Format.pp_print_string + +let first_stmt_f = ref None +let first_stmt_g = ref None + +(** For each statement of [f], find its immediate dominator and postdominator + and print the triplets. *) +let print_immediate f = + let res = + List.map (fun s -> + let dom = Dominators.get_idom s in + let postdom = Dominators.get_ipostdom s in + [string_of_int s.sid; get dom; get postdom] + ) f.sallstmts + in + Format.printf "@[<v2>Immediate dominators of %s (sid, idom, ipostdom):@;%a@]@;" + f.svar.vname + (Pretty_utils.pp_list ~pre:"@[" ~sep:",@ " ~suf:"@]" pp_res) res + +(** For each couple of statement of [f], find their common ancestor and children + and print the quadruplets. *) +let print_nearest f = + assert (Dominators.nearest_common_ancestor [] = None); + let res = + List.map (fun s -> + List.map (fun s' -> + let dom = Dominators.nearest_common_ancestor [s; s'] in + let postdom = Dominators.nearest_common_children [s; s'] in + [string_of_int s.sid; string_of_int s'.sid; get dom; get postdom] + ) f.sallstmts + ) f.sallstmts + |> List.flatten + in + Format.printf "@[<v2>Nearest common ancestors/children of %s (sid, sid, ancestor, children):@;%a@]@;" + f.svar.vname + (Pretty_utils.pp_list ~pre:"@[" ~sep:",@ " ~suf:"@]" pp_res) res + +(* Make sure that the difference between (post)dominators and strict + (post)dominators of a statement [s] is equal to the singleton [s]. *) +let test_strict f = + let test s dom strict_dom = + match dom, strict_dom with + | Some dom, Some strict_dom -> + assert (StmtSet.diff dom strict_dom == StmtSet.singleton s) + | None, None -> () + | _ -> assert false + in + List.iter (fun s -> + let dom = Dominators.get_dominators s in + let sdom = Dominators.get_strict_dominators s in + let postdom = Dominators.get_postdominators s in + let spostdom = Dominators.get_strict_postdominators s in + test s dom sdom; + test s postdom spostdom; + assert (Dominators.strictly_dominates s s = false); + assert (Dominators.strictly_postdominates s s = false) + ) f.sallstmts + +class visitPostDom = object(self) + inherit Visitor.frama_c_inplace + + method! vfunc f = + let kf = Option.get (self#current_kf) in + Format.printf "@[<v>Computing for function %s:@;%a@?@;@?" + f.svar.vname Cil_printer.pp_block f.sbody; + + Dominators.compute_dominators kf; + Dominators.print_dot_dominators "dom_graph" kf; + + Dominators.compute_postdominators kf; + Dominators.print_dot_postdominators "postdom_graph" kf; + + print_immediate f; + print_nearest f; + test_strict f; + + Format.printf "@]@."; + SkipChildren +end + +let catch f x = + try ignore (f x) + with Log.AbortFatal _ -> () + +let cover_errors () = + let loc = Cil_datatype.Location.unknown in + (* Test statement not in a function. *) + let skip = Cil_builder.Pure.(cil_stmt ~loc skip) in + catch Dominators.get_postdominators skip; + let trigger kf = + match kf.fundec with + | Definition _ -> () + | Declaration _ -> + (* Test Kernel_function.find_first_stmt on decl. *) + catch Dominators.compute_dominators kf; + (* Test Kernel_function.find_return on decl. *) + catch Dominators.compute_postdominators kf; + (* Test print_dot on decl. *) + catch (Dominators.print_dot_dominators "tmp") kf + in + Globals.Functions.iter trigger + +let pretty () = + Format.printf "@[<v2>Dominators analysis:@;%a@]\n@." + Dominators.pretty_dominators (); + Format.printf "@[<v2>Postominators analysis:@;%a@]\n@." + Dominators.pretty_postdominators () + +let startup () = + ignore (Cil.visitCilFileSameGlobals (new visitPostDom:>Cil.cilVisitor) (Ast.get ())); + pretty (); + Ast.mark_as_changed (); + Format.printf "Invalidate tables, which should now be empty\n@."; + pretty (); + cover_errors () + +let () = Boot.Main.extend startup