From c22fbdce1936baf7c73eb2e390199163111d4e3a Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 27 Jun 2024 11:17:48 +0200
Subject: [PATCH] Add a test for Dominators, 100% coverage
---
tests/misc/oracle/dom_graph.f.dot | 56 +++
tests/misc/oracle/dom_graph.g.dot | 63 +++
tests/misc/oracle/dom_graph.h.dot | 113 ++++++
tests/misc/oracle/dom_graph.i.dot | 76 ++++
tests/misc/oracle/postdom_graph.f.dot | 54 +++
tests/misc/oracle/postdom_graph.g.dot | 64 +++
tests/misc/oracle/postdom_graph.h.dot | 104 +++++
tests/misc/oracle/postdom_graph.i.dot | 76 ++++
tests/misc/oracle/test_dominators.res.oracle | 388 +++++++++++++++++++
tests/misc/test_dominators.c | 54 +++
tests/misc/test_dominators.ml | 126 ++++++
11 files changed, 1174 insertions(+)
create mode 100644 tests/misc/oracle/dom_graph.f.dot
create mode 100644 tests/misc/oracle/dom_graph.g.dot
create mode 100644 tests/misc/oracle/dom_graph.h.dot
create mode 100644 tests/misc/oracle/dom_graph.i.dot
create mode 100644 tests/misc/oracle/postdom_graph.f.dot
create mode 100644 tests/misc/oracle/postdom_graph.g.dot
create mode 100644 tests/misc/oracle/postdom_graph.h.dot
create mode 100644 tests/misc/oracle/postdom_graph.i.dot
create mode 100644 tests/misc/oracle/test_dominators.res.oracle
create mode 100644 tests/misc/test_dominators.c
create mode 100644 tests/misc/test_dominators.ml
diff --git a/tests/misc/oracle/dom_graph.f.dot b/tests/misc/oracle/dom_graph.f.dot
new file mode 100644
index 0000000000..ca126d8e69
--- /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 0000000000..8d9ff3a679
--- /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 0000000000..2826acff31
--- /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 0000000000..9a4bece549
--- /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 0000000000..71ad2d4f34
--- /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 0000000000..b67c6c4a95
--- /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 0000000000..0335859b42
--- /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 0000000000..64c9cb923c
--- /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 0000000000..0d6e7207b5
--- /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 0000000000..a461d101dc
--- /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 0000000000..8fad610175
--- /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
--
GitLab