From 7176713a6841bb5e293c1df0913310e602878ceb Mon Sep 17 00:00:00 2001 From: Cliff Click Date: Sat, 11 Nov 2023 23:17:22 +0000 Subject: Chapter 6: Peepholes for If MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Dibyendu Majumdar Co-authored-by: Thalia Archibald Co-authored-by: Yichen Yan Co-authored-by: tannal Co-authored-by: hadha Co-authored-by: Tamás Hadházy <85063808+Hels15@users.noreply.github.com> Co-authored-by: Tamas Hadhazy Co-authored-by: Robert Obkircher --- docs/chapter06/06-grammar.md | 83 +++++ docs/chapter06/06-graph1-post.gv | 29 ++ docs/chapter06/06-graph1-post.svg | 67 ++++ docs/chapter06/06-graph1-pre.gv | 52 +++ docs/chapter06/06-graph1-pre.svg | 160 +++++++++ docs/chapter06/06-graph2-post.gv | 33 ++ docs/chapter06/06-graph2-post.svg | 67 ++++ docs/chapter06/06-graph2-pre.gv | 55 +++ docs/chapter06/06-graph2-pre.svg | 154 +++++++++ docs/chapter06/06-graph3-false.gv | 35 ++ docs/chapter06/06-graph3-false.svg | 67 ++++ docs/chapter06/06-graph3-nonconst-peephole.gv | 56 +++ docs/chapter06/06-graph3-nonconst-peephole.svg | 150 ++++++++ docs/chapter06/06-graph3-nonconst.gv | 86 +++++ docs/chapter06/06-graph3-nonconst.svg | 290 ++++++++++++++++ docs/chapter06/06-graph3-true.gv | 35 ++ docs/chapter06/06-graph3-true.svg | 67 ++++ docs/chapter06/06-graph4-arg2.gv | 37 ++ docs/chapter06/06-graph4-arg2.svg | 67 ++++ docs/chapter06/06-graph4-nonconst.gv | 122 +++++++ docs/chapter06/06-graph4-nonconst.svg | 456 +++++++++++++++++++++++++ docs/chapter06/06-graph4-true.gv | 37 ++ docs/chapter06/06-graph4-true.svg | 67 ++++ docs/chapter06/Makefile | 12 + docs/chapter06/README.md | 200 +++++++++++ docs/chapter06/lattice.gv | 97 ++++++ docs/chapter06/lattice.svg | 319 +++++++++++++++++ 27 files changed, 2900 insertions(+) create mode 100644 docs/chapter06/06-grammar.md create mode 100644 docs/chapter06/06-graph1-post.gv create mode 100644 docs/chapter06/06-graph1-post.svg create mode 100644 docs/chapter06/06-graph1-pre.gv create mode 100644 docs/chapter06/06-graph1-pre.svg create mode 100644 docs/chapter06/06-graph2-post.gv create mode 100644 docs/chapter06/06-graph2-post.svg create mode 100644 docs/chapter06/06-graph2-pre.gv create mode 100644 docs/chapter06/06-graph2-pre.svg create mode 100644 docs/chapter06/06-graph3-false.gv create mode 100644 docs/chapter06/06-graph3-false.svg create mode 100644 docs/chapter06/06-graph3-nonconst-peephole.gv create mode 100644 docs/chapter06/06-graph3-nonconst-peephole.svg create mode 100644 docs/chapter06/06-graph3-nonconst.gv create mode 100644 docs/chapter06/06-graph3-nonconst.svg create mode 100644 docs/chapter06/06-graph3-true.gv create mode 100644 docs/chapter06/06-graph3-true.svg create mode 100644 docs/chapter06/06-graph4-arg2.gv create mode 100644 docs/chapter06/06-graph4-arg2.svg create mode 100644 docs/chapter06/06-graph4-nonconst.gv create mode 100644 docs/chapter06/06-graph4-nonconst.svg create mode 100644 docs/chapter06/06-graph4-true.gv create mode 100644 docs/chapter06/06-graph4-true.svg create mode 100644 docs/chapter06/Makefile create mode 100644 docs/chapter06/README.md create mode 100644 docs/chapter06/lattice.gv create mode 100644 docs/chapter06/lattice.svg (limited to 'docs/chapter06') diff --git a/docs/chapter06/06-grammar.md b/docs/chapter06/06-grammar.md new file mode 100644 index 00000000..4cf1cac6 --- /dev/null +++ b/docs/chapter06/06-grammar.md @@ -0,0 +1,83 @@ +# Grammar for Chapter 6 + +```antlrv4 +grammar SimpleLanguage; + +program + : statement+ EOF + ; + +statement + : returnStatement + | declStatement + | blockStatment + | expressionStatement + | ifStatement + | metaStatement + ; + +ifStatement + : 'if' '(' expression ')' statement ('else' statement)? + ; + +metaStatement + : '#showGraph' ';' + ; + +expressionStatement + : IDENTIFIER '=' expression ';' + ; + +blockStatement + : '{' statement+ '}' + ; + +declStatement + : 'int' IDENTIFIER '=' expression ';' + ; + +returnStatement + : 'return' expression ';' + ; + +expression + : comparisonExpression + ; + +comparisonExpression + : additiveExpression (('==' | '!='| '>'| '<'| '>='| '<=') additiveExpression)* + ; + +additiveExpression + : multiplicativeExpression (('+' | '-') multiplicativeExpression)* + ; + +multiplicativeExpression + : unaryExpression (('*' | '/') unaryExpression)* + ; + +unaryExpression + : ('-') unaryExpression + | primaryExpression + ; + +primaryExpression + : IDENTIFIER + | INTEGER_LITERAL + | 'true' + | 'false' + | '(' expression ')' + ; + +INTEGER_LITERAL + : [1-9][0-9]* + | [0] + ; + +IDENTIFIER + : NON_DIGIT (NON_DIGIT | DIGIT)* + ; + +NON_DIGIT: [a-zA-Z_]; +DEC_DIGIT: [0-9]; +``` diff --git a/docs/chapter06/06-graph1-post.gv b/docs/chapter06/06-graph1-post.gv new file mode 100644 index 00000000..31480991 --- /dev/null +++ b/docs/chapter06/06-graph1-post.gv @@ -0,0 +1,29 @@ +digraph chapter06 { +/* +if( true ) return 2; +return 1; + +*/ + rankdir=BT; + ordering="in"; + concentrate="true"; + subgraph cluster_Nodes { + Start2 [ shape=plaintext label=< + + + +
Start
+ + +
$ctrl
+
> + ]; + Stop3 [ shape=box style=filled fillcolor=yellow label="Stop" ]; + Con_12 [ label="#2" ]; + Return13 [ shape=box style=filled fillcolor=yellow label="Return" ]; + } + edge [ fontname=Helvetica, fontsize=8 ]; + Stop3 -> Return13[taillabel=0 color=red]; + Return13 -> Start2:p0[taillabel=0 color=red]; + Return13 -> Con_12[taillabel=1]; +} diff --git a/docs/chapter06/06-graph1-post.svg b/docs/chapter06/06-graph1-post.svg new file mode 100644 index 00000000..faabcd8c --- /dev/null +++ b/docs/chapter06/06-graph1-post.svg @@ -0,0 +1,67 @@ + + + + + + +chapter06 + + +cluster_Nodes + + + + +Start2 + + +Start + + + +$ctrl + + + +Stop3 + +Stop + + + +Return13 + +Return + + + +Stop3->Return13 + + +0 + + + +Con_12 + +#2 + + + +Return13->Start2:p0 + + +0 + + + +Return13->Con_12 + + +1 + + + diff --git a/docs/chapter06/06-graph1-pre.gv b/docs/chapter06/06-graph1-pre.gv new file mode 100644 index 00000000..2bfdd23d --- /dev/null +++ b/docs/chapter06/06-graph1-pre.gv @@ -0,0 +1,52 @@ +digraph chapter06 { +/* +if( true ) return 2; +return 1; + +*/ + rankdir=BT; + ordering="in"; + concentrate="true"; + subgraph cluster_Nodes { + Start2 [ shape=plaintext label=< + + + +
Start
+ + +
$ctrl
+
> + ]; + Stop3 [ shape=box style=filled fillcolor=yellow label="Stop" ]; + Con_6 [ label="#1" ]; + If7 [ shape=plaintext label=< + + + +
If
+ + +
TrueFalse
+
> + ]; + Con_11 [ label="#2" ]; + Return12 [ shape=box style=filled fillcolor=yellow label="Return" ]; + Con_13 [ label="#~CONTROL" ]; + Region14 [ shape=box style=filled fillcolor=yellow label="Region" ]; + Con_15 [ label="#1" ]; + Return16 [ shape=box style=filled fillcolor=yellow label="Return" ]; + { rank=same; Region14;} + } + edge [ fontname=Helvetica, fontsize=8 ]; + Stop3 -> Return12[taillabel=0 color=red]; + Stop3 -> Return16[taillabel=1 color=red]; + If7 -> Start2:p0[taillabel=0 color=red]; + If7 -> Con_6[taillabel=1]; + Return12 -> If7:p0[taillabel=0 color=red]; + Return12 -> Con_11[taillabel=1]; + Region14 -> Con_13[taillabel=1]; + Region14 -> If7:p1[taillabel=2 color=red]; + Return16 -> Region14[taillabel=0 color=red]; + Return16 -> Con_15[taillabel=1]; +} diff --git a/docs/chapter06/06-graph1-pre.svg b/docs/chapter06/06-graph1-pre.svg new file mode 100644 index 00000000..f80edcfc --- /dev/null +++ b/docs/chapter06/06-graph1-pre.svg @@ -0,0 +1,160 @@ + + + + + + +chapter06 + + +cluster_Nodes + + + + +Start2 + + +Start + + + +$ctrl + + + +Stop3 + +Stop + + + +Return12 + +Return + + + +Stop3->Return12 + + +0 + + + +Return16 + +Return + + + +Stop3->Return16 + + +1 + + + +Con_6 + +#1 + + + +If7 + + +If + + + +True + + +False + + + +If7->Start2:p0 + + +0 + + + +If7->Con_6 + + +1 + + + +Con_11 + +#2 + + + +Return12->If7:p0 + + +0 + + + +Return12->Con_11 + + +1 + + + +Con_13 + +#~CONTROL + + + +Region14 + +Region + + + +Region14->If7:p1 + + +2 + + + +Region14->Con_13 + + +1 + + + +Con_15 + +#1 + + + +Return16->Region14 + + +0 + + + +Return16->Con_15 + + +1 + + + diff --git a/docs/chapter06/06-graph2-post.gv b/docs/chapter06/06-graph2-post.gv new file mode 100644 index 00000000..61ae2ca1 --- /dev/null +++ b/docs/chapter06/06-graph2-post.gv @@ -0,0 +1,33 @@ +digraph chapter06 { +/* +int a=1; +if( true ) + a=2; +else + a=3; +return a; + +*/ + rankdir=BT; + ordering="in"; + concentrate="true"; + subgraph cluster_Nodes { + Return17 [ shape=box style=filled fillcolor=yellow label="Return" ]; + Start2 [ shape=plaintext label=< + + + +
Start
+ + +
$ctrl
+
> + ]; + Stop3 [ shape=box style=filled fillcolor=yellow label="Stop" ]; + Con_13 [ label="#2" ]; + } + edge [ fontname=Helvetica, fontsize=8 ]; + Return17 -> Start2:p0[taillabel=0 color=red]; + Return17 -> Con_13[taillabel=1]; + Stop3 -> Return17[taillabel=0 color=red]; +} diff --git a/docs/chapter06/06-graph2-post.svg b/docs/chapter06/06-graph2-post.svg new file mode 100644 index 00000000..269eb15c --- /dev/null +++ b/docs/chapter06/06-graph2-post.svg @@ -0,0 +1,67 @@ + + + + + + +chapter06 + + +cluster_Nodes + + + + +Return17 + +Return + + + +Start2 + + +Start + + + +$ctrl + + + +Return17->Start2:p0 + + +0 + + + +Con_13 + +#2 + + + +Return17->Con_13 + + +1 + + + +Stop3 + +Stop + + + +Stop3->Return17 + + +0 + + + diff --git a/docs/chapter06/06-graph2-pre.gv b/docs/chapter06/06-graph2-pre.gv new file mode 100644 index 00000000..d183b4c4 --- /dev/null +++ b/docs/chapter06/06-graph2-pre.gv @@ -0,0 +1,55 @@ +digraph chapter06 { +/* +int a=1; +if( true ) + a=2; +else + a=3; +return a; + +*/ + rankdir=BT; + ordering="in"; + concentrate="true"; + subgraph cluster_Nodes { + Return16 [ shape=box style=filled fillcolor=yellow label="Return" ]; + Start2 [ shape=plaintext label=< + + + +
Start
+ + +
$ctrl
+
> + ]; + Stop3 [ shape=box style=filled fillcolor=yellow label="Stop" ]; + Con_7 [ label="#1" ]; + If8 [ shape=plaintext label=< + + + +
If
+ + +
TrueFalse
+
> + ]; + Con_12 [ label="#2" ]; + Con_13 [ label="#3" ]; + Region14 [ shape=box style=filled fillcolor=yellow label="Region" ]; + Phi_a15 [ style=filled fillcolor=lightyellow label="φ_a" ]; + { rank=same; Region14;Phi_a15;} + } + edge [ fontname=Helvetica, fontsize=8 ]; + Return16 -> Region14[taillabel=0 color=red]; + Return16 -> Phi_a15[taillabel=1]; + Stop3 -> Return16[taillabel=0 color=red]; + If8 -> Start2:p0[taillabel=0 color=red]; + If8 -> Con_7[taillabel=1]; + Region14 -> If8:p0[taillabel=1 color=red]; + Region14 -> If8:p1[taillabel=2 color=red]; + Phi_a15 -> Region14 [style=dotted taillabel=0]; + Phi_a15 -> Con_12[taillabel=1]; + Phi_a15 -> Con_13[taillabel=2]; +} diff --git a/docs/chapter06/06-graph2-pre.svg b/docs/chapter06/06-graph2-pre.svg new file mode 100644 index 00000000..e9a4dd55 --- /dev/null +++ b/docs/chapter06/06-graph2-pre.svg @@ -0,0 +1,154 @@ + + + + + + +chapter06 + + +cluster_Nodes + + + + +Return16 + +Return + + + +Region14 + +Region + + + +Return16->Region14 + + +0 + + + +Phi_a15 + +φ_a + + + +Return16->Phi_a15 + + +1 + + + +Start2 + + +Start + + + +$ctrl + + + +Stop3 + +Stop + + + +Stop3->Return16 + + +0 + + + +Con_7 + +#1 + + + +If8 + + +If + + + +True + + +False + + + +If8->Start2:p0 + + +0 + + + +If8->Con_7 + + +1 + + + +Con_12 + +#2 + + + +Con_13 + +#3 + + + +Region14->If8:p0 + + +1 + + + +Region14->If8:p1 + + +2 + + + +Phi_a15->Con_12 + + +1 + + + +Phi_a15->Con_13 + + +2 + + + +Phi_a15->Region14 + + +0 + + + diff --git a/docs/chapter06/06-graph3-false.gv b/docs/chapter06/06-graph3-false.gv new file mode 100644 index 00000000..28f741fa --- /dev/null +++ b/docs/chapter06/06-graph3-false.gv @@ -0,0 +1,35 @@ +digraph chapter06 { +/* +int a = 0; +int b = 1; +if( arg ) { + a = 2; + if( arg ) { b = 2; } + else b = 3; +} +return a+b; + +*/ + rankdir=BT; + ordering="in"; + concentrate="true"; + subgraph cluster_Nodes { + Start2 [ shape=plaintext label=< + + + +
Start
+ + +
$ctrl
+
> + ]; + Stop3 [ shape=box style=filled fillcolor=yellow label="Stop" ]; + Con_30 [ label="#1" ]; + Return31 [ shape=box style=filled fillcolor=yellow label="Return" ]; + } + edge [ fontname=Helvetica, fontsize=8 ]; + Stop3 -> Return31[taillabel=0 color=red]; + Return31 -> Start2:p0[taillabel=0 color=red]; + Return31 -> Con_30[taillabel=1]; +} diff --git a/docs/chapter06/06-graph3-false.svg b/docs/chapter06/06-graph3-false.svg new file mode 100644 index 00000000..49b04f09 --- /dev/null +++ b/docs/chapter06/06-graph3-false.svg @@ -0,0 +1,67 @@ + + + + + + +chapter06 + + +cluster_Nodes + + + + +Start2 + + +Start + + + +$ctrl + + + +Stop3 + +Stop + + + +Return31 + +Return + + + +Stop3->Return31 + + +0 + + + +Con_30 + +#1 + + + +Return31->Start2:p0 + + +0 + + + +Return31->Con_30 + + +1 + + + diff --git a/docs/chapter06/06-graph3-nonconst-peephole.gv b/docs/chapter06/06-graph3-nonconst-peephole.gv new file mode 100644 index 00000000..f8e3e5fa --- /dev/null +++ b/docs/chapter06/06-graph3-nonconst-peephole.gv @@ -0,0 +1,56 @@ +digraph chapter06 { +/* +int a = 0; +int b = 1; +if( arg ) { + a = 2; + if( arg ) { b = 2; } + else b = 3; +} +return a+b; + +*/ + rankdir=BT; + ordering="in"; + concentrate="true"; + subgraph cluster_Nodes { + Start2 [ shape=plaintext label=< + + + +
Start
+ + +
$ctrlarg
+
> + ]; + Stop3 [ shape=box style=filled fillcolor=yellow label="Stop" ]; + Region22 [ shape=box style=filled fillcolor=yellow label="Region" ]; + If8 [ shape=plaintext label=< + + + +
If
+ + +
TrueFalse
+
> + ]; + Con_27 [ label="#4" ]; + Con_29 [ label="#1" ]; + Phi_ab30 [ style=filled fillcolor=lightyellow label="φ_ab" ]; + Return31 [ shape=box style=filled fillcolor=yellow label="Return" ]; + { rank=same; Region22;Phi_ab30;} + } + edge [ fontname=Helvetica, fontsize=8 ]; + Stop3 -> Return31[taillabel=0 color=red]; + Region22 -> If8:p0[taillabel=1 color=red]; + Region22 -> If8:p1[taillabel=2 color=red]; + If8 -> Start2:p0[taillabel=0 color=red]; + If8 -> Start2:p1[taillabel=1]; + Phi_ab30 -> Region22 [style=dotted taillabel=0]; + Phi_ab30 -> Con_27[taillabel=1]; + Phi_ab30 -> Con_29[taillabel=2]; + Return31 -> Region22[taillabel=0 color=red]; + Return31 -> Phi_ab30[taillabel=1]; +} diff --git a/docs/chapter06/06-graph3-nonconst-peephole.svg b/docs/chapter06/06-graph3-nonconst-peephole.svg new file mode 100644 index 00000000..c312ffc5 --- /dev/null +++ b/docs/chapter06/06-graph3-nonconst-peephole.svg @@ -0,0 +1,150 @@ + + + + + + +chapter06 + + +cluster_Nodes + + + + +Start2 + + +Start + + + +$ctrl + +arg + + + +Stop3 + +Stop + + + +Return31 + +Return + + + +Stop3->Return31 + + +0 + + + +Region22 + +Region + + + +If8 + + +If + + + +True + + +False + + + +Region22->If8:p0 + + +1 + + + +Region22->If8:p1 + + +2 + + + +If8->Start2:p0 + + +0 + + + +If8->Start2:p1 + + +1 + + + +Con_27 + +#4 + + + +Con_29 + +#1 + + + +Phi_ab30 + +φ_ab + + + +Phi_ab30->Region22 + + +0 + + + +Phi_ab30->Con_27 + + +1 + + + +Phi_ab30->Con_29 + + +2 + + + +Return31->Region22 + + +0 + + + +Return31->Phi_ab30 + + +1 + + + diff --git a/docs/chapter06/06-graph3-nonconst.gv b/docs/chapter06/06-graph3-nonconst.gv new file mode 100644 index 00000000..7cd4e8e2 --- /dev/null +++ b/docs/chapter06/06-graph3-nonconst.gv @@ -0,0 +1,86 @@ +digraph chapter06 { +/* +int a = 0; +int b = 1; +if( arg ) { + a = 2; + if( arg ) { b = 2; } + else b = 3; +} +return a+b; + +*/ + rankdir=BT; + ordering="in"; + concentrate="true"; + subgraph cluster_Nodes { + Start2 [ shape=plaintext label=< + + + +
Start
+ + +
$ctrlarg
+
> + ]; + Stop3 [ shape=box style=filled fillcolor=yellow label="Stop" ]; + Con_6 [ label="#0" ]; + Con_7 [ label="#1" ]; + If8 [ shape=plaintext label=< + + + +
If
+ + +
TrueFalse
+
> + ]; + Con_12 [ label="#2" ]; + If13 [ shape=plaintext label=< + + + +
If
+ + +
TrueFalse
+
> + ]; + Con_17 [ label="#2" ]; + Con_18 [ label="#3" ]; + Region19 [ shape=box style=filled fillcolor=yellow label="Region" ]; + Phi_b20 [ style=filled fillcolor=lightyellow label="φ_b" ]; + Region21 [ shape=box style=filled fillcolor=yellow label="Region" ]; + Phi_a22 [ style=filled fillcolor=lightyellow label="φ_a" ]; + Phi_b23 [ style=filled fillcolor=lightyellow label="φ_b" ]; + Add24 [ label="+" ]; + Return25 [ shape=box style=filled fillcolor=yellow label="Return" ]; + { rank=same; Region19;Phi_b20;} + { rank=same; Region21;Phi_b23;Phi_a22;} + } + edge [ fontname=Helvetica, fontsize=8 ]; + Stop3 -> Return25[taillabel=0 color=red]; + If8 -> Start2:p0[taillabel=0 color=red]; + If8 -> Start2:p1[taillabel=1]; + If13 -> If8:p0[taillabel=0 color=red]; + If13 -> Start2:p1[taillabel=1]; + Region19 -> If13:p0[taillabel=1 color=red]; + Region19 -> If13:p1[taillabel=2 color=red]; + Phi_b20 -> Region19 [style=dotted taillabel=0]; + Phi_b20 -> Con_17[taillabel=1]; + Phi_b20 -> Con_18[taillabel=2]; + Region21 -> Region19[taillabel=1 color=red]; + Region21 -> If8:p1[taillabel=2 color=red]; + Phi_a22 -> Region21 [style=dotted taillabel=0]; + Phi_a22 -> Con_12[taillabel=1]; + Phi_a22 -> Con_6[taillabel=2]; + Phi_b23 -> Region21 [style=dotted taillabel=0]; + Phi_b23 -> Phi_b20[taillabel=1]; + Phi_b23 -> Con_7[taillabel=2]; + Add24 -> Phi_b23[taillabel=1]; + Add24 -> Phi_a22[taillabel=2]; + Return25 -> Region21[taillabel=0 color=red]; + Return25 -> Add24[taillabel=1]; +} diff --git a/docs/chapter06/06-graph3-nonconst.svg b/docs/chapter06/06-graph3-nonconst.svg new file mode 100644 index 00000000..dee852e4 --- /dev/null +++ b/docs/chapter06/06-graph3-nonconst.svg @@ -0,0 +1,290 @@ + + + + + + +chapter06 + + +cluster_Nodes + + + + +Start2 + + +Start + + + +$ctrl + +arg + + + +Stop3 + +Stop + + + +Return25 + +Return + + + +Stop3->Return25 + + +0 + + + +Con_6 + +#0 + + + +Con_7 + +#1 + + + +If8 + + +If + + + +True + + +False + + + +If8->Start2:p0 + + +0 + + + +If8->Start2:p1 + + +1 + + + +Con_12 + +#2 + + + +If13 + + +If + + + +True + + +False + + + +If13->Start2:p1 + + +1 + + + +If13->If8:p0 + + +0 + + + +Con_17 + +#2 + + + +Con_18 + +#3 + + + +Region19 + +Region + + + +Region19->If13:p0 + + +1 + + + +Region19->If13:p1 + + +2 + + + +Phi_b20 + +φ_b + + + +Phi_b20->Con_17 + + +1 + + + +Phi_b20->Con_18 + + +2 + + + +Phi_b20->Region19 + + +0 + + + +Region21 + +Region + + + +Region21->If8:p1 + + +2 + + + +Region21->Region19 + + +1 + + + +Phi_a22 + +φ_a + + + +Phi_a22->Con_6 + + +2 + + + +Phi_a22->Con_12 + + +1 + + + +Phi_a22->Region21 + + +0 + + + +Phi_b23 + +φ_b + + + +Phi_b23->Con_7 + + +2 + + + +Phi_b23->Phi_b20 + + +1 + + + +Phi_b23->Region21 + + +0 + + + +Add24 + ++ + + + +Add24->Phi_a22 + + +2 + + + +Add24->Phi_b23 + + +1 + + + +Return25->Region21 + + +0 + + + +Return25->Add24 + + +1 + + + diff --git a/docs/chapter06/06-graph3-true.gv b/docs/chapter06/06-graph3-true.gv new file mode 100644 index 00000000..9739169c --- /dev/null +++ b/docs/chapter06/06-graph3-true.gv @@ -0,0 +1,35 @@ +digraph chapter06 { +/* +int a = 0; +int b = 1; +if( arg ) { + a = 2; + if( arg ) { b = 2; } + else b = 3; +} +return a+b; + +*/ + rankdir=BT; + ordering="in"; + concentrate="true"; + subgraph cluster_Nodes { + Start2 [ shape=plaintext label=< + + + +
Start
+ + +
$ctrl
+
> + ]; + Stop3 [ shape=box style=filled fillcolor=yellow label="Stop" ]; + Con_28 [ label="#4" ]; + Return29 [ shape=box style=filled fillcolor=yellow label="Return" ]; + } + edge [ fontname=Helvetica, fontsize=8 ]; + Stop3 -> Return29[taillabel=0 color=red]; + Return29 -> Start2:p0[taillabel=0 color=red]; + Return29 -> Con_28[taillabel=1]; +} diff --git a/docs/chapter06/06-graph3-true.svg b/docs/chapter06/06-graph3-true.svg new file mode 100644 index 00000000..7e573cc6 --- /dev/null +++ b/docs/chapter06/06-graph3-true.svg @@ -0,0 +1,67 @@ + + + + + + +chapter06 + + +cluster_Nodes + + + + +Start2 + + +Start + + + +$ctrl + + + +Stop3 + +Stop + + + +Return29 + +Return + + + +Stop3->Return29 + + +0 + + + +Con_28 + +#4 + + + +Return29->Start2:p0 + + +0 + + + +Return29->Con_28 + + +1 + + + diff --git a/docs/chapter06/06-graph4-arg2.gv b/docs/chapter06/06-graph4-arg2.gv new file mode 100644 index 00000000..7d6913e2 --- /dev/null +++ b/docs/chapter06/06-graph4-arg2.gv @@ -0,0 +1,37 @@ +digraph chapter06 { +/* +int a = 0; +int b = 1; +int c = 0; +if( arg ) { + a = 1; + if( arg==2 ) { c=2; } else { c=3; } + if( arg ) { b = 2; } + else b = 3; +} +return a+b+c; + +*/ + rankdir=BT; + ordering="in"; + concentrate="true"; + subgraph cluster_Nodes { + Start2 [ shape=plaintext label=< + + + +
Start
+ + +
$ctrl
+
> + ]; + Stop3 [ shape=box style=filled fillcolor=yellow label="Stop" ]; + Con_44 [ label="#5" ]; + Return45 [ shape=box style=filled fillcolor=yellow label="Return" ]; + } + edge [ fontname=Helvetica, fontsize=8 ]; + Stop3 -> Return45[taillabel=0 color=red]; + Return45 -> Start2:p0[taillabel=0 color=red]; + Return45 -> Con_44[taillabel=1]; +} diff --git a/docs/chapter06/06-graph4-arg2.svg b/docs/chapter06/06-graph4-arg2.svg new file mode 100644 index 00000000..8ec80be4 --- /dev/null +++ b/docs/chapter06/06-graph4-arg2.svg @@ -0,0 +1,67 @@ + + + + + + +chapter06 + + +cluster_Nodes + + + + +Start2 + + +Start + + + +$ctrl + + + +Stop3 + +Stop + + + +Return45 + +Return + + + +Stop3->Return45 + + +0 + + + +Con_44 + +#5 + + + +Return45->Start2:p0 + + +0 + + + +Return45->Con_44 + + +1 + + + diff --git a/docs/chapter06/06-graph4-nonconst.gv b/docs/chapter06/06-graph4-nonconst.gv new file mode 100644 index 00000000..b8899b48 --- /dev/null +++ b/docs/chapter06/06-graph4-nonconst.gv @@ -0,0 +1,122 @@ +digraph chapter06 { +/* +int a = 0; +int b = 1; +int c = 0; +if( arg ) { + a = 1; + if( arg==2 ) { c=2; } else { c=3; } + if( arg ) { b = 2; } + else b = 3; +} +return a+b+c; + +*/ + rankdir=BT; + ordering="in"; + concentrate="true"; + subgraph cluster_Nodes { + Start2 [ shape=plaintext label=< + + + +
Start
+ + +
$ctrlarg
+
> + ]; + Stop3 [ shape=box style=filled fillcolor=yellow label="Stop" ]; + Con_6 [ label="#0" ]; + Con_7 [ label="#1" ]; + Con_8 [ label="#0" ]; + If9 [ shape=plaintext label=< + + + +
If
+ + +
TrueFalse
+
> + ]; + Con_13 [ label="#1" ]; + Con_14 [ label="#2" ]; + EQNode15 [ label="==" ]; + If16 [ shape=plaintext label=< + + + +
If
+ + +
TrueFalse
+
> + ]; + Con_20 [ label="#2" ]; + Con_21 [ label="#3" ]; + Region22 [ shape=box style=filled fillcolor=yellow label="Region" ]; + Phi_c23 [ style=filled fillcolor=lightyellow label="φ_c" ]; + If24 [ shape=plaintext label=< + + + +
If
+ + +
TrueFalse
+
> + ]; + Con_28 [ label="#2" ]; + Con_29 [ label="#3" ]; + Region30 [ shape=box style=filled fillcolor=yellow label="Region" ]; + Phi_b31 [ style=filled fillcolor=lightyellow label="φ_b" ]; + Region32 [ shape=box style=filled fillcolor=yellow label="Region" ]; + Phi_a33 [ style=filled fillcolor=lightyellow label="φ_a" ]; + Phi_b34 [ style=filled fillcolor=lightyellow label="φ_b" ]; + Phi_c35 [ style=filled fillcolor=lightyellow label="φ_c" ]; + Add36 [ label="+" ]; + Add37 [ label="+" ]; + Return38 [ shape=box style=filled fillcolor=yellow label="Return" ]; + { rank=same; Region22;Phi_c23;} + { rank=same; Region30;Phi_b31;} + { rank=same; Region32;Phi_c35;Phi_a33;Phi_b34;} + } + edge [ fontname=Helvetica, fontsize=8 ]; + Stop3 -> Return38[taillabel=0 color=red]; + If9 -> Start2:p0[taillabel=0 color=red]; + If9 -> Start2:p1[taillabel=1]; + EQNode15 -> Start2:p1[taillabel=1]; + EQNode15 -> Con_14[taillabel=2]; + If16 -> If9:p0[taillabel=0 color=red]; + If16 -> EQNode15[taillabel=1]; + Region22 -> If16:p0[taillabel=1 color=red]; + Region22 -> If16:p1[taillabel=2 color=red]; + Phi_c23 -> Region22 [style=dotted taillabel=0]; + Phi_c23 -> Con_20[taillabel=1]; + Phi_c23 -> Con_21[taillabel=2]; + If24 -> Region22[taillabel=0 color=red]; + If24 -> Start2:p1[taillabel=1]; + Region30 -> If24:p0[taillabel=1 color=red]; + Region30 -> If24:p1[taillabel=2 color=red]; + Phi_b31 -> Region30 [style=dotted taillabel=0]; + Phi_b31 -> Con_28[taillabel=1]; + Phi_b31 -> Con_29[taillabel=2]; + Region32 -> Region30[taillabel=1 color=red]; + Region32 -> If9:p1[taillabel=2 color=red]; + Phi_a33 -> Region32 [style=dotted taillabel=0]; + Phi_a33 -> Con_13[taillabel=1]; + Phi_a33 -> Con_6[taillabel=2]; + Phi_b34 -> Region32 [style=dotted taillabel=0]; + Phi_b34 -> Phi_b31[taillabel=1]; + Phi_b34 -> Con_7[taillabel=2]; + Phi_c35 -> Region32 [style=dotted taillabel=0]; + Phi_c35 -> Phi_c23[taillabel=1]; + Phi_c35 -> Con_8[taillabel=2]; + Add36 -> Phi_c35[taillabel=1]; + Add36 -> Phi_b34[taillabel=2]; + Add37 -> Add36[taillabel=1]; + Add37 -> Phi_a33[taillabel=2]; + Return38 -> Region32[taillabel=0 color=red]; + Return38 -> Add37[taillabel=1]; +} diff --git a/docs/chapter06/06-graph4-nonconst.svg b/docs/chapter06/06-graph4-nonconst.svg new file mode 100644 index 00000000..d38c3636 --- /dev/null +++ b/docs/chapter06/06-graph4-nonconst.svg @@ -0,0 +1,456 @@ + + + + + + +chapter06 + + +cluster_Nodes + + + + +Start2 + + +Start + + + +$ctrl + +arg + + + +Stop3 + +Stop + + + +Return38 + +Return + + + +Stop3->Return38 + + +0 + + + +Con_6 + +#0 + + + +Con_7 + +#1 + + + +Con_8 + +#0 + + + +If9 + + +If + + + +True + + +False + + + +If9->Start2:p0 + + +0 + + + +If9->Start2:p1 + + +1 + + + +Con_13 + +#1 + + + +Con_14 + +#2 + + + +EQNode15 + +== + + + +EQNode15->Start2:p1 + + +1 + + + +EQNode15->Con_14 + + +2 + + + +If16 + + +If + + + +True + + +False + + + +If16->If9:p0 + + +0 + + + +If16->EQNode15 + + +1 + + + +Con_20 + +#2 + + + +Con_21 + +#3 + + + +Region22 + +Region + + + +Region22->If16:p0 + + +1 + + + +Region22->If16:p1 + + +2 + + + +Phi_c23 + +φ_c + + + +Phi_c23->Con_20 + + +1 + + + +Phi_c23->Con_21 + + +2 + + + +Phi_c23->Region22 + + +0 + + + +If24 + + +If + + + +True + + +False + + + +If24->Start2:p1 + + +1 + + + +If24->Region22 + + +0 + + + +Con_28 + +#2 + + + +Con_29 + +#3 + + + +Region30 + +Region + + + +Region30->If24:p0 + + +1 + + + +Region30->If24:p1 + + +2 + + + +Phi_b31 + +φ_b + + + +Phi_b31->Con_28 + + +1 + + + +Phi_b31->Con_29 + + +2 + + + +Phi_b31->Region30 + + +0 + + + +Region32 + +Region + + + +Region32->If9:p1 + + +2 + + + +Region32->Region30 + + +1 + + + +Phi_a33 + +φ_a + + + +Phi_a33->Con_6 + + +2 + + + +Phi_a33->Con_13 + + +1 + + + +Phi_a33->Region32 + + +0 + + + +Phi_b34 + +φ_b + + + +Phi_b34->Con_7 + + +2 + + + +Phi_b34->Phi_b31 + + +1 + + + +Phi_b34->Region32 + + +0 + + + +Phi_c35 + +φ_c + + + +Phi_c35->Con_8 + + +2 + + + +Phi_c35->Phi_c23 + + +1 + + + +Phi_c35->Region32 + + +0 + + + +Add36 + ++ + + + +Add36->Phi_b34 + + +2 + + + +Add36->Phi_c35 + + +1 + + + +Add37 + ++ + + + +Add37->Phi_a33 + + +2 + + + +Add37->Add36 + + +1 + + + +Return38->Region32 + + +0 + + + +Return38->Add37 + + +1 + + + diff --git a/docs/chapter06/06-graph4-true.gv b/docs/chapter06/06-graph4-true.gv new file mode 100644 index 00000000..6e48ee7d --- /dev/null +++ b/docs/chapter06/06-graph4-true.gv @@ -0,0 +1,37 @@ +digraph chapter06 { +/* +int a = 0; +int b = 1; +int c = 0; +if( arg ) { + a = 1; + if( arg==2 ) { c=2; } else { c=3; } + if( arg ) { b = 2; } + else b = 3; +} +return a+b+c; + +*/ + rankdir=BT; + ordering="in"; + concentrate="true"; + subgraph cluster_Nodes { + Start2 [ shape=plaintext label=< + + + +
Start
+ + +
$ctrl
+
> + ]; + Stop3 [ shape=box style=filled fillcolor=yellow label="Stop" ]; + Con_44 [ label="#6" ]; + Return45 [ shape=box style=filled fillcolor=yellow label="Return" ]; + } + edge [ fontname=Helvetica, fontsize=8 ]; + Stop3 -> Return45[taillabel=0 color=red]; + Return45 -> Start2:p0[taillabel=0 color=red]; + Return45 -> Con_44[taillabel=1]; +} diff --git a/docs/chapter06/06-graph4-true.svg b/docs/chapter06/06-graph4-true.svg new file mode 100644 index 00000000..a533ea21 --- /dev/null +++ b/docs/chapter06/06-graph4-true.svg @@ -0,0 +1,67 @@ + + + + + + +chapter06 + + +cluster_Nodes + + + + +Start2 + + +Start + + + +$ctrl + + + +Stop3 + +Stop + + + +Return45 + +Return + + + +Stop3->Return45 + + +0 + + + +Con_44 + +#6 + + + +Return45->Start2:p0 + + +0 + + + +Return45->Con_44 + + +1 + + + diff --git a/docs/chapter06/Makefile b/docs/chapter06/Makefile new file mode 100644 index 00000000..12659b8f --- /dev/null +++ b/docs/chapter06/Makefile @@ -0,0 +1,12 @@ +GV := $(wildcard *.gv) +SVG := $(patsubst %.gv,%.svg,$(GV)) + +.PHONY: all +all: $(SVG) + +%.svg: %.gv + dot -Tsvg $< > $@ + +.PHONY: clean +clean: + @rm -f $(SVG) diff --git a/docs/chapter06/README.md b/docs/chapter06/README.md new file mode 100644 index 00000000..a5151586 --- /dev/null +++ b/docs/chapter06/README.md @@ -0,0 +1,200 @@ +# Chapter 6: Peepholes for If + +# Table of Contents + +1. [Type System Revision](#type-system-revision) +2. [Peephole of `if`](#peephole-of-if) +3. [`Region` and `Phi`](#Region-and-Phi) +4. [Discussion](#discussion) +5. [Expanding Peephole Beyond Constant Expressions](#expanding-peephole-beyond-constant-expressions) +6. [Dominators](#dominators) + +You can also read [this chapter](https://github.com/SeaOfNodes/Simple/tree/linear-chapter06) in a linear Git revision history on the [linear](https://github.com/SeaOfNodes/Simple/tree/linear) branch and [compare](https://github.com/SeaOfNodes/Simple/compare/linear-chapter05...linear-chapter06) it to the previous chapter. + +In this chapter we do not add new language features. Our goal is to add peephole optimization to `if` statements. + + +## Type System Revision + +We now need to extend the type system to introduce another lattice structure, in addition to the Integer sub-lattice. +As before we denote "Top" by T and "Bottom" by ⊥. + +* "Ctrl" represents a live control, whereas "~Ctrl" represents a dead control. +* "INT" refers to an integer value, note that integer values have their own sub-lattice. + +| | ⊥ | Ctrl | ~Ctrl | T | INT | +|-------|---|------|-------|-------|-----| +| T | ⊥ | Ctrl | ~Ctrl | T | INT | +| Ctrl | ⊥ | Ctrl | Ctrl | Ctrl | ⊥ | +| ~Ctrl | ⊥ | Ctrl | ~Ctrl | ~Ctrl | ⊥ | +| ⊥ | ⊥ | ⊥ | ⊥ | ⊥ | ⊥ | + +* "Top" meets any type is that type, +* "Bottom" meets any type is "Bottom", +* "Top", "Bottom", "Ctrl", "~Ctrl" are classed as simple types, +* "Ctrl" meets "~Ctrl" is "Ctrl" +* Unless covered above, a simple type meets non-simple results in "Bottom" + +The entire revised Lattice is shown below: + +![Lattice](./lattice.svg) + + +## Peephole of `if` + +* Our general strategy is to continue parsing the entire `if` statement even if we know that one branch is dead. +* This approach creates dead nodes which get cleaned up by dead code + elimination. The benefits are that we do not introduce special logic during + parsing, the normal graph building machinery takes care of cleaning up dead + nodes. +* When we peephole an `If` node we test if the predicate is a constant. If so, + then one branch or the other dead, depending on if the constant is `0` or not. +* When we add the `Proj` nodes, in this scenario, we already know one of the projections is dead. The peephole of the + relevant `Proj` node replaces the `Proj` with a `Constant` of type "~Ctrl" indicating dead control. +* At this point our dead code elimination would kill the `If` node since it has no uses + - but we cannot do that because we need to continue the parse. The + important observation is that *we __can__ kill the `If` node after __both__ + the `Proj` nodes have been created*, because any subsequent control flow can + only see the `Proj` nodes. +* To ensure this, we add a dummy user to `If` before creating the first `Proj` and remove it immediately after, allowing the + second `Proj` to trigger a dead code elimination of the `If`. +* The live `Proj` gets replaced by the parent of `If`, whereas the dead `Proj` gets replaced by "~Ctrl". +* The parsing then continues as normal. +* The other changes are when we reach the merge point with a dead control. +* Again keeping with our strategy we merge as normal, including creating `Phi` nodes. +* The `Region` may have have one of its inputs as "~Ctrl". This will be seen + by the `Phi` which then optimizes itself. If the `Phi` has just one live + input, the `Phi` peephole replaces itself with the remaining input. +* Finally, at the end, when the `Region` node is peepholed, we see that it has only one live input and no Phi uses + and can be replaced with its one live input. + +## `Region` and `Phi` + +One of the invariants we maintain is that the for each control input to a +`Region` every `Phi` has a 1-to-1 relationship with a data input. Thus, if a +`Region` loses a control input, every `Phi`'s corresponding data input must be +deleted. Conversely, we cannot collapse a Region until it has no dependent +`Phi`s. + +When processing `If` we do not remove control inputs to a `Region`, instead the +dead control input is simply set to `Constant(~Ctrl)`. The peephole logic in +a `Phi` notices this and replaces itself with the live input. + +## Discussion + +With the changes above, our peephole optimization is able to fold dead code when +an `if` statement has a condition that evaluates to `true` or `false` at compile time. + +Let's look at a simple example below: + +```java +if( true ) return 2; +return 1; +``` + +Before peephole: + +![Graph1-Pre](./06-graph1-pre.svg) + +After peephole: + +![Graph1-Post](./06-graph1-post.svg) + +Another example: + +```java +int a=1; +if( true ) + a=2; +else + a=3; +return a; +``` + +Before peephole: + +![Graph2-Pre](./06-graph2-pre.svg) + +After peephole: + +![Graph2-Post](./06-graph2-post.svg) + +## Expanding Peephole Beyond Constant Expressions + +While our peephole of the `CFG` collapses dead code when the expression is +a compile time constant. it does not do as well as it could with following example: + +```java +int a = 0; +int b = 1; +if( arg ) { + a = 2; + if( arg ) { b = 2; } + else b = 3; +} +return a+b; +``` + +In this example, `arg` is defined externally, and we have to assume it is not a constant. +However, the code repeats the `if( arg )` condition in the inner `if` statement. +We know that if the outer `if( arg )` is true, then the *inner `if` must also evaluate to true*. + +Our peephole at present cannot see this: + +![Graph3-NonConst](./06-graph3-nonconst.svg) + +What we would like is for our peephole to see that the inner `if` is fully determined by the +outer `if` and thus, the code can be simplified as follows: + +```java +int a = 0; +int b = 1; +if ( arg ) { + a = 2; + b = 2; +} +return a+b; +``` + +That is, the final outcome is either `4` if `arg` happens to be true, or `1` if `arg` happens to be false. + +## Dominators + +The key to implementing this peephole is the observation that the inner `if` is completely determined by the +outer `if`. In compiler parlance, we say that the outer `if` dominates the inner `if`. + +There is a generic way to determine this type of domination; it involves constructing a dominator +tree. For details of how to do this, please refer to the paper `A Simple, Fast Dominance Algorithm`.[^1] + +However, constructing a dominator tree is an expensive operation; one that we would not like to +do in the middle of parsing. Fortunately, since we do not have loops yet, we do not +have back edges in our control flow graph. Our control flow graph is essentially hierarchical, tree like. +Thus, a simple form of dominator identification is possible. + +The main idea is that we can assign a `depth` to each control node, this represents the node's depth +in the hierarchy. We can compute this depth incrementally as we need to. The nodes that are deeper in the hierarchy +have a greater depth than the ones above. + +Secondly we know that for our control nodes, except for `Region`s, there is only one incoming control edge, +which means that most control nodes have a single immediate dominating control node. `Region` nodes are different +as they can have one or more control edges; but, we know that for `if` statements, a `Region` node has exactly two +control inputs, one from each branch of the `if`. To find the immediate dominator of a `Region` node in the +limited scenario of an `if`, we can follow the immediate dominator of each branch until we find the common ancestor +node that dominates both the branches. + +If this ancestor node is also an `if` and its predicate is the same as the current `if`, then we know that +the outcome of the present `if` is fully determined. + +The code that does this check is in the [`compute` method of the `if`](https://github.com/SeaOfNodes/Simple/blob/main/chapter06/src/main/java/com/seaofnodes/simple/node/IfNode.java#L38-L45). + +The `idom` method in `Node` provides a default implementation of the depth based immediate dominator calculation. +`Region`'s [override this](https://github.com/SeaOfNodes/Simple/blob/main/chapter06/src/main/java/com/seaofnodes/simple/node/RegionNode.java#L57-L74) to implement the more complex search described above. + +It turns out that to simplify the example above, we need a [further peephole in our `Add` node](https://github.com/SeaOfNodes/Simple/blob/main/chapter06/src/main/java/com/seaofnodes/simple/node/AddNode.java#L64-L67). + +With all these changes, the outcome of the peephole is just what we would like to see! + +![Graph3-NonConst-Peephole](./06-graph3-nonconst-peephole.svg) + +[^1]: Cooper, K. D. Cooper, Harvey, T. J., and Kennedy, K. (2001). + A Simple, Fast Dominance Algorithm. diff --git a/docs/chapter06/lattice.gv b/docs/chapter06/lattice.gv new file mode 100644 index 00000000..e5cc59be --- /dev/null +++ b/docs/chapter06/lattice.gv @@ -0,0 +1,97 @@ +digraph Lattice { + // Define nodes + splines=false; + node [shape=circle, style=filled, fillcolor=lightblue]; + nodesep=0.6; + + TOP [label=<⊤>, fillcolor=black, fontcolor=white]; + BOT [label=<⊥>, fillcolor=black, fontcolor=white]; + + // ---------------------- + // Control + XCTRL [label=<⊤:ctrl>, fillcolor=yellow, shape=oval]; + CTRL [label=<⊥:ctrl>, fillcolor=yellow, shape=oval]; + + TOP -> XCTRL; + XCTRL -> CTRL; + CTRL -> BOT; + + // ---------------------- + // Integers + INT_TOP [label=<⊤:int>, fillcolor=lightblue, shape=oval]; + INT_BOT [label=<⊥:int>, fillcolor=lightblue, shape=oval]; + + INT_MIN [label="-n" , fillcolor=lightblue]; + INT_MINDOTS [label="...", fillcolor=lightblue shape=oval]; + INT_MINUS [label="-1" , fillcolor=lightblue]; + INT_ZERO [label="0" , fillcolor=lightblue]; + INT_PLUS [label="1" , fillcolor=lightblue]; + INT_MAXDOTS [label="...", fillcolor=lightblue, shape=oval]; + INT_MAX [label="+n" , fillcolor=lightblue]; + + TOP -> INT_TOP; + INT_TOP -> INT_MIN; + INT_TOP -> INT_MINDOTS; + INT_TOP -> INT_MINUS; + INT_TOP -> INT_ZERO; + INT_TOP -> INT_PLUS; + INT_TOP -> INT_MAXDOTS; + INT_TOP -> INT_MAX; + INT_MIN -> INT_BOT; + INT_MINDOTS -> INT_BOT; + INT_MINUS -> INT_BOT; + INT_ZERO -> INT_BOT; + INT_PLUS -> INT_BOT; + INT_MAXDOTS -> INT_BOT; + INT_MAX -> INT_BOT; + INT_BOT -> BOT; + + INT_MIN -> INT_MINDOTS -> INT_MINUS -> INT_ZERO -> INT_PLUS -> INT_MAXDOTS -> INT_MAX [style=invis]; + + // ---------------------- + // Tuples + + TUPLE_TOP [label=<⊤:tuple>, fillcolor=pink, shape=oval]; + TUPLE_BOT [label=<⊥:tuple>, fillcolor=pink, shape=oval]; + + TUPLE1 [shape=none, fillcolor=none, label=< + + + +
tuple
type
+ >]; + TUPLE2 [shape=none, fillcolor=none, label=< + + + + +
tuple
type
type
+ >]; + TUPLEN [shape=none, fillcolor=none, label=< + + + + + +
tuple
type
...
type
+ >]; + + + TOP -> TUPLE_TOP; + TUPLE_TOP -> TUPLE1; + TUPLE_TOP -> TUPLE2; + TUPLE_TOP -> TUPLEN; + TUPLE1 -> TUPLE_BOT; + TUPLE2 -> TUPLE_BOT; + TUPLEN -> TUPLE_BOT; + TUPLE_BOT -> BOT; + + // Additional customization + {rank=same; TOP} + {rank=same; XCTRL; INT_TOP; TUPLE_TOP} + {rank=same; + INT_MIN; INT_MINDOTS; INT_MINUS; INT_ZERO; INT_PLUS; INT_MAXDOTS; INT_MAX; + } + {rank=same; CTRL; INT_BOT, TUPLE_BOT} + {rank=same; BOT;} +} diff --git a/docs/chapter06/lattice.svg b/docs/chapter06/lattice.svg new file mode 100644 index 00000000..86371c93 --- /dev/null +++ b/docs/chapter06/lattice.svg @@ -0,0 +1,319 @@ + + + + + + +Lattice + + + +TOP + +⊤ + + + +XCTRL + +⊤ +:ctrl + + + +TOP->XCTRL + + + + + +INT_TOP + +⊤ +:int + + + +TOP->INT_TOP + + + + + +TUPLE_TOP + +⊤ +:tuple + + + +TOP->TUPLE_TOP + + + + + +BOT + +⊥ + + + +CTRL + +⊥ +:ctrl + + + +XCTRL->CTRL + + + + + +CTRL->BOT + + + + + +INT_MIN + +-n + + + +INT_TOP->INT_MIN + + + + + +INT_MINDOTS + +... + + + +INT_TOP->INT_MINDOTS + + + + + +INT_MINUS + +-1 + + + +INT_TOP->INT_MINUS + + + + + +INT_ZERO + +0 + + + +INT_TOP->INT_ZERO + + + + + +INT_PLUS + +1 + + + +INT_TOP->INT_PLUS + + + + + +INT_MAXDOTS + +... + + + +INT_TOP->INT_MAXDOTS + + + + + +INT_MAX + ++n + + + +INT_TOP->INT_MAX + + + + + +INT_BOT + +⊥ +:int + + + +INT_BOT->BOT + + + + + +INT_MIN->INT_BOT + + + + + + +INT_MINDOTS->INT_BOT + + + + + + +INT_MINUS->INT_BOT + + + + + + +INT_ZERO->INT_BOT + + + + + + +INT_PLUS->INT_BOT + + + + + + +INT_MAXDOTS->INT_BOT + + + + + + +INT_MAX->INT_BOT + + + + + +TUPLE1 + + + +tuple + + +type + + + +TUPLE_TOP->TUPLE1 + + + + + +TUPLE2 + + + +tuple + + +type + + +type + + + +TUPLE_TOP->TUPLE2 + + + + + +TUPLEN + + + +tuple + + +type + + +... + + +type + + + +TUPLE_TOP->TUPLEN + + + + + +TUPLE_BOT + +⊥ +:tuple + + + +TUPLE_BOT->BOT + + + + + +TUPLE1->TUPLE_BOT + + + + + +TUPLE2->TUPLE_BOT + + + + + +TUPLEN->TUPLE_BOT + + + + + -- cgit v1.2.3