From 65454d77eba95d7f814336377f78d9f42c7455f9 Mon Sep 17 00:00:00 2001 From: Cliff Click Date: Wed, 27 Nov 2024 11:29:33 -0800 Subject: More lattice docs reworks --- chapter02/README.md | 13 +- chapter02/docs/02-lattice.gv | 35 --- chapter02/docs/02-lattice.svg | 143 --------- chapter02/docs/lattice.gv | 40 +++ chapter02/docs/lattice.svg | 159 ++++++++++ chapter04/README.md | 41 ++- chapter04/docs/lattice.gv | 81 +++-- chapter04/docs/lattice.svg | 260 +++++++++++----- chapter06/docs/lattice.gv | 86 ++++-- chapter06/docs/lattice.svg | 293 ++++++++++++------ chapter10/README.md | 63 ++-- chapter10/docs/lattice.gv | 46 ++- chapter10/docs/lattice.svg | 602 +++++++++++++++++------------------- chapter12/README.md | 3 +- chapter12/docs/lattice.gv | 182 +++++++++++ chapter12/docs/lattice.svg | 598 ++++++++++++++++++++++++++++++++++++ chapter14/README.md | 21 +- chapter14/docs/lattice.gv | 202 ++++++++++++ chapter14/docs/lattice.svg | 691 ++++++++++++++++++++++++++++++++++++++++++ 19 files changed, 2775 insertions(+), 784 deletions(-) delete mode 100644 chapter02/docs/02-lattice.gv delete mode 100644 chapter02/docs/02-lattice.svg create mode 100644 chapter02/docs/lattice.gv create mode 100644 chapter02/docs/lattice.svg create mode 100644 chapter12/docs/lattice.gv create mode 100644 chapter12/docs/lattice.svg create mode 100644 chapter14/docs/lattice.gv create mode 100644 chapter14/docs/lattice.svg diff --git a/chapter02/README.md b/chapter02/README.md index db23796d..04e34eb9 100644 --- a/chapter02/README.md +++ b/chapter02/README.md @@ -93,17 +93,18 @@ Type ``` It turns out that the set of values associated with a Type at a specific Node -can be conveniently represented as a "lattice" -https://en.wikipedia.org/wiki/Lattice_(order) -. Our lattice has the following structure: +can be conveniently represented as a *lattice* +[wiki/Lattice_(order)](https://en.wikipedia.org/wiki/Lattice_(order)). Our lattice has the following structure: -![Lattice](./docs/02-lattice.svg) +![Lattice](./docs/lattice.svg) Our lattice elements can be one of three types: -* The highest element is "top", denoted by T; assigning T means that the Node's value may or may not be a compile time constant. +* The highest element is "top", denoted by ⊤; assigning ⊤ means that the Node's + value may or may not be a compile time constant. * All elements in the middle are constants. -* The lowest is "bottom", denoted by ⊥; assigning ⊥ means that we know that the Node's value is **not** a compile time constant. +* The lowest is "bottom", denoted by ⊥; assigning ⊥ means that we know that the + Node's value is **not** a compile time constant. An invariant of peephole optimizations is that the type of a Node always moves *up* the lattice (towards "top"); peepholes are *pessmistic* assuming the worst diff --git a/chapter02/docs/02-lattice.gv b/chapter02/docs/02-lattice.gv deleted file mode 100644 index 4faa0e11..00000000 --- a/chapter02/docs/02-lattice.gv +++ /dev/null @@ -1,35 +0,0 @@ -digraph Lattice { - // Define nodes - node [shape=circle, style=filled, fillcolor=lightblue]; - Top [label="⊤"]; - Bottom [label="⊥"]; - - A [label="MIN_INT"]; - B [label="..." shape=none style=none]; - C [label="-1"]; - D [label="0"]; - E [label="1"]; - F [label="..." shape=none style=none]; - G [label="MAX_INT"]; - - - // Define edges - Top -> A [arrowhead=none]; - Top -> B [arrowhead=none]; - Top -> C [arrowhead=none]; - Top -> D [arrowhead=none]; - Top -> E [arrowhead=none]; - Top -> F [arrowhead=none]; - Top -> G [arrowhead=none]; - A -> Bottom [arrowhead=none]; - B -> Bottom [arrowhead=none]; - C -> Bottom [arrowhead=none]; - D -> Bottom [arrowhead=none]; - E -> Bottom [arrowhead=none]; - F -> Bottom [arrowhead=none]; - G -> Bottom [arrowhead=none]; - - // Additional customization - {rank=same; A; B; C; D; E; F; G; } - {rank=same; Bottom;} -} diff --git a/chapter02/docs/02-lattice.svg b/chapter02/docs/02-lattice.svg deleted file mode 100644 index 218acc6a..00000000 --- a/chapter02/docs/02-lattice.svg +++ /dev/null @@ -1,143 +0,0 @@ - - - - - - - Lattice - - - - Top - - ⊤ - - - - A - - MIN_INT - - - - Top->A - - - - - B - ... - - - - Top->B - - - - - C - - -1 - - - - Top->C - - - - - D - - 0 - - - - Top->D - - - - - E - - 1 - - - - Top->E - - - - - F - ... - - - - Top->F - - - - - G - - MAX_INT - - - - Top->G - - - - - Bottom - - ⊥ - - - - A->Bottom - - - - - B->Bottom - - - - - C->Bottom - - - - - D->Bottom - - - - - E->Bottom - - - - - F->Bottom - - - - - G->Bottom - - - - diff --git a/chapter02/docs/lattice.gv b/chapter02/docs/lattice.gv new file mode 100644 index 00000000..fe8df136 --- /dev/null +++ b/chapter02/docs/lattice.gv @@ -0,0 +1,40 @@ +digraph Lattice { + compound = true; + // Define nodes + splines=false; + node [shape=circle, style=filled]; + nodesep=0.6; + + // ---------------------- + // 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]; + + 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_MIN -> INT_MINDOTS -> INT_MINUS -> INT_ZERO -> INT_PLUS -> INT_MAXDOTS -> INT_MAX [style=invis]; + + // Additional customization + {rank=same; INT_MIN; INT_MINDOTS; INT_MINUS; INT_ZERO; INT_PLUS; INT_MAXDOTS; INT_MAX; } +} diff --git a/chapter02/docs/lattice.svg b/chapter02/docs/lattice.svg new file mode 100644 index 00000000..b11d57aa --- /dev/null +++ b/chapter02/docs/lattice.svg @@ -0,0 +1,159 @@ + + + + + + +Lattice + + + +INT_TOP + +⊤ +:int + + + +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_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 + + + + + diff --git a/chapter04/README.md b/chapter04/README.md index 299d5da9..1b14bf0a 100644 --- a/chapter04/README.md +++ b/chapter04/README.md @@ -184,11 +184,9 @@ lattice. In this chapter we extend the Type hierarchy as follows: ``` -Type -+-- TypeControl (New - represents control token) -+-- TypeInteger (Enhanced - now has Top and Bottom types) -+-- TypeBot -+-- TypeTuple (New - represents multi-valued result) +Type (Enhanced - now has Control, and a global Top and Bottom) ++-- TypeInteger (Enhanced - now has Top and Bottom types) ++-- TypeTuple (New - represents multi-valued result) ``` Our enhanced Lattice looks like this: @@ -197,14 +195,18 @@ Our enhanced Lattice looks like this: In this chapter we introduce the possibility of a program input variable named -`arg`; all we know about this variable is that it is some integer value, but we do not know whether it is a constant or not. +`arg`; all we know about this variable is that it is some integer value, but we +do not know whether it is a constant or not. -To support the requirements for non-constant integer values, we enhance `TypeInteger` to -allow it to represent `IntTop` and `IntBot` integer types in addition to the earlier constant value. +To support the requirements for non-constant integer values, we enhance +`TypeInteger` to allow it to represent `IntTop` and `IntBot` integer types in +addition to the earlier constant value. -Now that integer values may be constants or non-constants, we need to introduce the "meet" operator -in our lattice. The `meet` operator describes rules that define the resulting type when we combine -integer values. +Now that integer values may be constants or non-constants, we need to introduce +the *meet* operator over our lattice. The `meet` operator describes rules that +define the resulting type when we combine integer values. In the lattice +diagram you can start from the two elements being `meet` and follow the +two arrows down the graph to the first point they meet. | | IntBot | Con1 | Con2 | IntTop | |--------|--------|--------|--------|--------| @@ -223,13 +225,26 @@ Currently, all our integer valued nodes are either a constant or a `IntBot` inte When we start optimizing loops, we will start seeing `IntTop` values. +### Tuple Types + +Tuple types need a little more explaination: they are a fixed-size grouping of +types; literally a `Type[]`. Tuples represent a collection of otherwise +unrelated types, and come from `MultiNode`s. `ProjNode`s will take the +appropriate `Type` array element out of a Tuple. The `StartNode` now produces +a 2-element `TypeTuple` with control and the type of `arg`: `[ctrl, TypeInteger.INTBOT]` + +The lattice `meet` operator on Tuples is done element by element; each array +element recursively calls `meet`. Tuples of mixed sizes are a internal +compiler error, and the `meet` uses Bottom for them. + + ## `$ctrl` name binding In previous chapters, we had a hard coded control input edge from Start to Return. In this chapter we no longer have such a hard-wired edge. Instead, we track the current in-scope control node via the name `$ctrl`. This means that -when we need to create an edge to the predecessor control node, we simply -look up this name in the current scope. +when we need to create an edge to the predecessor control node, we simply look +up this name in the current scope. This introduces the idea that the control flow subgraph is a Petri net model.[^1] The control token moves virtually from node to node as execution proceeds. The diff --git a/chapter04/docs/lattice.gv b/chapter04/docs/lattice.gv index 29a53b0a..6efef107 100644 --- a/chapter04/docs/lattice.gv +++ b/chapter04/docs/lattice.gv @@ -1,29 +1,32 @@ digraph Lattice { + compound = true; // Define nodes splines=false; - node [shape=circle, style=filled, fillcolor=lightblue]; + node [shape=circle, style=filled]; nodesep=0.6; - TOP [label="⊤" , fillcolor=black, fontcolor=white]; - BOT [label="⊥", fillcolor=black, fontcolor=white]; + TOP [label=<⊤>, fillcolor=black, fontcolor=white]; + BOT [label=<⊥>, fillcolor=black, fontcolor=white]; - CTRL [label="Ctrl", fillcolor=yellow]; + // ---------------------- + // Control + CTRL [label="ctrl", fillcolor=yellow, shape=oval]; - INT_TOP [label="⊤ :Int"]; - INT_BOT [label="⊥ :Int"]; - - INT_MIN [label="-n"]; - INT_MINDOTS [label="..." shape=none style=none]; - INT_MINUS [label="-1"]; - INT_ZERO [label="0"]; - INT_PLUS [label="1"]; - INT_MAXDOTS [label="..." shape=none style=none]; - INT_MAX [label="+n"]; + TOP -> CTRL; + CTRL -> BOT; - TUPLE [label="TUPLE", fillcolor=pink]; + // ---------------------- + // Integers + INT_TOP [label=<⊤:int>, fillcolor=lightblue, shape=oval]; + INT_BOT [label=<⊥:int>, fillcolor=lightblue, shape=oval]; - // Define edges - edge [arrowhead=none]; + 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; @@ -43,22 +46,52 @@ digraph Lattice { INT_BOT -> BOT; INT_MIN -> INT_MINDOTS -> INT_MINUS -> INT_ZERO -> INT_PLUS -> INT_MAXDOTS -> INT_MAX [style=invis]; + + // ---------------------- + // Tuples - TOP -> TUPLE; - TUPLE -> BOT; + 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 -> CTRL; - CTRL -> BOT; + 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; INT_TOP} + {rank=same; INT_TOP; TUPLE_TOP} {rank=same; CTRL; INT_MIN; INT_MINDOTS; INT_MINUS; INT_ZERO; INT_PLUS; INT_MAXDOTS; INT_MAX; - TUPLE } - {rank=same; INT_BOT} + {rank=same; INT_BOT, TUPLE_BOT} {rank=same; BOT;} } diff --git a/chapter04/docs/lattice.svg b/chapter04/docs/lattice.svg index 1cab7681..35cb9296 100644 --- a/chapter04/docs/lattice.svg +++ b/chapter04/docs/lattice.svg @@ -4,192 +4,302 @@ - - + + Lattice - + TOP - -⊤ + +⊤ CTRL - -Ctrl + +ctrl - + TOP->CTRL - + + INT_TOP - -⊤ :Int + +⊤ +:int - + TOP->INT_TOP - + + - + -TUPLE - -TUPLE +TUPLE_TOP + +⊤ +:tuple - - -TOP->TUPLE - + + +TOP->TUPLE_TOP + + BOT - -⊥ + +⊥ - + CTRL->BOT - + + INT_MIN - --n + +-n - + INT_TOP->INT_MIN - + + INT_MINDOTS -... + +... - + INT_TOP->INT_MINDOTS - + + INT_MINUS - --1 + +-1 - + INT_TOP->INT_MINUS - + + INT_ZERO - -0 + +0 - + INT_TOP->INT_ZERO - + + INT_PLUS - -1 + +1 - + INT_TOP->INT_PLUS - + + INT_MAXDOTS -... + +... - + INT_TOP->INT_MAXDOTS - + + INT_MAX - -+n + ++n - + INT_TOP->INT_MAX - + + INT_BOT - -⊥ :Int + +⊥ +: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 - - - - -TUPLE->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 + + diff --git a/chapter06/docs/lattice.gv b/chapter06/docs/lattice.gv index 782c2253..e5cc59be 100644 --- a/chapter06/docs/lattice.gv +++ b/chapter06/docs/lattice.gv @@ -4,27 +4,30 @@ digraph Lattice { node [shape=circle, style=filled, fillcolor=lightblue]; nodesep=0.6; - TOP [label="⊤" , fillcolor=black, fontcolor=white]; - BOT [label="⊥", fillcolor=black, fontcolor=white]; + TOP [label=<⊤>, fillcolor=black, fontcolor=white]; + BOT [label=<⊥>, fillcolor=black, fontcolor=white]; - XCTRL [label="⊤ :Ctrl", fillcolor=yellow]; - CTRL [label="⊥ :Ctrl", fillcolor=yellow]; + // ---------------------- + // Control + XCTRL [label=<⊤:ctrl>, fillcolor=yellow, shape=oval]; + CTRL [label=<⊥:ctrl>, fillcolor=yellow, shape=oval]; - INT_TOP [label="⊤ :Int"]; - INT_BOT [label="⊥ :Int"]; - - INT_MIN [label="-n"]; - INT_MINUS [label="-1"]; - INT_MINDOTS [label="..." shape=none style=none]; - INT_ZERO [label="0"]; - INT_PLUS [label="1"]; - INT_MAXDOTS [label="..." shape=none style=none]; - INT_MAX [label="+n"]; + TOP -> XCTRL; + XCTRL -> CTRL; + CTRL -> BOT; - TUPLE [label="TUPLE", fillcolor=pink]; + // ---------------------- + // Integers + INT_TOP [label=<⊤:int>, fillcolor=lightblue, shape=oval]; + INT_BOT [label=<⊥:int>, fillcolor=lightblue, shape=oval]; - // Define edges - edge [arrowhead=none]; + 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; @@ -44,18 +47,51 @@ digraph Lattice { INT_BOT -> BOT; INT_MIN -> INT_MINDOTS -> INT_MINUS -> INT_ZERO -> INT_PLUS -> INT_MAXDOTS -> INT_MAX [style=invis]; + + // ---------------------- + // Tuples - TOP -> TUPLE; - TUPLE -> BOT; + TUPLE_TOP [label=<⊤:tuple>, fillcolor=pink, shape=oval]; + TUPLE_BOT [label=<⊥:tuple>, fillcolor=pink, shape=oval]; - TOP -> XCTRL; - XCTRL -> CTRL; - CTRL -> BOT; + 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; INT_TOP; XCTRL} - {rank=same; INT_MIN; INT_MINDOTS; INT_MINUS; INT_ZERO; INT_PLUS; INT_MAXDOTS; INT_MAX; TUPLE } - {rank=same; INT_BOT; CTRL} + {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/chapter06/docs/lattice.svg b/chapter06/docs/lattice.svg index f4929b41..86371c93 100644 --- a/chapter06/docs/lattice.svg +++ b/chapter06/docs/lattice.svg @@ -4,203 +4,316 @@ - - + + Lattice - + TOP - -⊤ + +⊤ XCTRL - -⊤ :Ctrl + +⊤ +:ctrl - + TOP->XCTRL - + + INT_TOP - -⊤ :Int + +⊤ +:int - + TOP->INT_TOP - + + - + -TUPLE - -TUPLE +TUPLE_TOP + +⊤ +:tuple - - -TOP->TUPLE - + + +TOP->TUPLE_TOP + + BOT -⊥ +⊥ CTRL - -⊥ :Ctrl + +⊥ +:ctrl - + XCTRL->CTRL - + + - + CTRL->BOT - + + INT_MIN - --n + +-n - + INT_TOP->INT_MIN - - - - -INT_MINUS - --1 - - - -INT_TOP->INT_MINUS - + + - + INT_MINDOTS -... + +... - + INT_TOP->INT_MINDOTS - + + + + + +INT_MINUS + +-1 + + + +INT_TOP->INT_MINUS + + INT_ZERO - -0 + +0 - + INT_TOP->INT_ZERO - + + INT_PLUS - -1 + +1 - + INT_TOP->INT_PLUS - + + INT_MAXDOTS -... + +... - + INT_TOP->INT_MAXDOTS - + + INT_MAX - -+n + ++n - + INT_TOP->INT_MAX - + + INT_BOT - -⊥ :Int + +⊥ +:int - + INT_BOT->BOT - + + - + INT_MIN->INT_BOT - + + - - -INT_MINUS->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 - - - - -TUPLE->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 + + diff --git a/chapter10/README.md b/chapter10/README.md index c27c4b74..957be607 100644 --- a/chapter10/README.md +++ b/chapter10/README.md @@ -118,6 +118,7 @@ Additionally, the following Node types will be enhanced: | Start | Control | Start will produce the initial Memory projections, one per slice | | Return | Control | Will merge all memory slices | + ## Enhanced Type Lattice The Type Lattice for Simple has a major revision in this chapter. @@ -126,22 +127,38 @@ The Type Lattice for Simple has a major revision in this chapter. Within the Type Lattice, we now have the following type domains: -* Control type - this represents control flow -* Integer type - Integer values -* Tuple type - when a Node results in more than one value -* Struct type (new) - Represents user defined struct types, a struct type is allowed to have members of Integer type only in this chapter - * `$TOP` represents local Top for struct type; all we know about the type is that it is a struct but, we do not know if it is a specific struct, or all possible structs, etc. - * `$BOT` represents local Bottom for struct type; we definitely know the value can take all possible struct types. -* Pointer type (new) - Represents a pointer to a struct type - * `null` is a pointer to non-existent memory object - * We use the prefix `*` to mean pointer-to. Thus `*S1` means pointer to `S1`, `*$TOP` means pointer to `$TOP`. - * `*void` is a synonym for `*$BOT` - i.e. it represents a Non-Null pointer to all possible struct types, akin to `void *` in C except not null. +* Control type - represents control flow +* Integer type - Integer values, with a Top, Bottom and constants +* Pointer type (new) - Represents a pointer to a struct type + * We use the prefix `*` to mean pointer-to. Thus `*S1` means pointer to + `S1`, `*$TOP` means pointer to `$TOP`. * `?` suffix represents the union of a pointer to some type and `null`. - * `null` pointer evaluates to False and non-null pointers evaluate to True, as in C. -* Memory (new) - Represents memory and memory slices - * `MEM#TOP` - Nothing known about a slice - * `#n` - refers to a memory slice - * `MEM#BOT` - all of memory + * The pointer lattice has only 2 entries: null or not-null. In both cases a struct lattice element is + included, and can be any member of the struct lattice. + * `null` is a pointer to non-existent memory object, i.e. `*$TOP?`, and is a + nullable. Notice that the null part of the type is low in the lattice, + while the struct part is the highest struct. + * `*void` is a synonym for `*$BOT` - i.e. it represents a non-null pointer to + all possible struct types, akin to `void *` in C except not null. It is + the inverse or *dual* of `null`, and the null part is high in the pointer + lattice, while the struct part is the lowest struct. + * `null` pointer evaluates to False and non-null pointers evaluate to True, as in C. + +* Struct type (new) - + Represents user defined struct types, a struct type is allowed to have + members of Integer type only in this chapter, later chapters will expand + this. + * `⊤:struct` represents local Top for struct type; all we know about the type + is that it is a struct but, we do not know if it is a specific struct, or + all possible structs. In the code, we use a struct with no fields named `$TOP`. + * `⊥:struct` represents local Bottom for struct type; we definitely know the + value can take all possible struct types. In the code, we uise a struct + with no fields named `$BOT`. +* Memory type (new) - Represents memory and memory slices + * `⊤:mem` - Nothing known about a slice; in the code we use `MEM#TOP`. + * `#n` - refers to a memory slice, and `n` is the alias class. + * `⊥:mem` - all of memory; in the code we use `MEM#BOT`. +* Tuple type - when a Node results in a collection of values We make use of following operations on the lattice. @@ -150,20 +167,22 @@ We make use of following operations on the lattice. thought of as set union (ORing) of its input types (as sets). * Example, meet of `*S1` and `*S2` results in `*void` - there is no lattice element for exactly both `{*S1,*S2}`, so we drop down to the nearest - element containing both (and maybe more), which is `*void*`. - * Meet of `*S1` and struct `Null` results in `*S1?` - * Meet of `*void` and `Null` results in `*$BOT?`; bear in mind that `*void` is a synonym for `*$BOT`. + element containing both (and maybe more), which is `*void`. + * Meet of `*S1` and pointer `null` results in `*S1?` + * Meet of `*void` and `null` results in `*$BOT?`; bear in mind that `*void` is a synonym for `*$BOT`. * Meet of `1` and `2` results in `Int Bot`. * Meet of `#1` and `#2` results in `MEM#BOT`. * The `dual` operation is symmetric across the lattice centerline. Types directly on the centerline are their own dual. * Find the corresponding node of the lattice after inverting the lattice. * Thus, dual of `Top` is `Bot`. * The dual of `*$TOP` is `*$BOT?`. - * For structs, the dual is obtained by computing the dual of each struct member. Thus, dual of `*S1` is not `*S1?`. + * For structs, the dual is obtained by computing the dual of each struct + member. Thus, dual of `*S1` is not `*S1?`, it is some `*S1?` with dualed + fields. * The `join` operation takes two types and computes the least upper bound type. Similar to `meet` this can thought of as set intersection (ANDing) of its input types. - Because our lattice structure is simple, we compute `join` with a well known identity: + Because our lattice structure is symmetric and complete, we compute `join` with a well known identity: `JOIN(x,y) === MEET(x.dual,y.dual).dual` * Example, join of `*S1` and `*S2` results in `*$TOP`. * Join of `1` and `2` results in `Int Top`. @@ -195,8 +214,8 @@ lattice described in the previous section. ## Null Pointer Analysis The Simple language syntax allows a pointer variable to be specified as -Null-able - and it prevents ever throwing a Null Pointer Exception. The -compiler tries to decide in a null check is needed, and if needed and missing +null-able - and it prevents ever throwing a Null Pointer Exception. The +compiler decides if a null check is needed, and if needed and missing the compiler rejects the program (asking the user to insert a null check). When the Parser encounters conditions that test the truthiness of a pointer variable, it uses this knowledge to refine the type information in the branches that follow. diff --git a/chapter10/docs/lattice.gv b/chapter10/docs/lattice.gv index 5ac1bd5a..7723e2a2 100644 --- a/chapter10/docs/lattice.gv +++ b/chapter10/docs/lattice.gv @@ -5,12 +5,12 @@ digraph Lattice { node [shape=circle, style=filled]; nodesep=0.6; - TOP [label=<⊤ >, fillcolor=black, fontcolor=white]; + TOP [label=<⊤>, fillcolor=black, fontcolor=white]; BOT [label=<⊥>, fillcolor=black, fontcolor=white]; // ---------------------- // Control - XCTRL [label=<⊤ :ctrl>, fillcolor=yellow, shape=oval]; + XCTRL [label=<⊤:ctrl>, fillcolor=yellow, shape=oval]; CTRL [label=<⊥:ctrl>, fillcolor=yellow, shape=oval]; TOP -> XCTRL; @@ -19,29 +19,23 @@ digraph Lattice { // ---------------------- // Integers - INT_TOP [label=<⊤ :int>, fillcolor=lightblue, shape=oval]; + 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_ZERO [label="0" , 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_ZERO; INT_TOP -> INT_MAXDOTS; - INT_TOP -> INT_MAX; - INT_MIN -> INT_BOT; INT_MINDOTS -> INT_BOT; INT_ZERO -> INT_BOT; INT_MAXDOTS -> INT_BOT; - INT_MAX -> INT_BOT; INT_BOT -> BOT; - INT_MIN -> INT_MINDOTS -> INT_ZERO -> INT_MAXDOTS -> INT_MAX [style=invis]; + INT_MINDOTS -> INT_ZERO -> INT_MAXDOTS [style=invis]; // ---------------------- // Pointers, just a boolean nil/not and a struct @@ -64,28 +58,28 @@ digraph Lattice { // ---------------------- // Structs - STRUCT_TOP [label=<⊤:struct>, fillcolor=lightgreen, shape=oval]; + STRUCT_TOP [label=<⊤:struct>, fillcolor=lightgreen, shape=oval]; + STRUCT_BOT [label=<⊥:struct>, fillcolor=lightgreen, shape=oval]; STRUCT_S1 [shape=none, fillcolor=none, label=< - +
fieldint:ptr
fieldint/ptr
>]; STRUCT_S2 [shape=none, fillcolor=none, label=< - - + +
fieldint:ptr
fieldint:ptr
fieldint/ptr
fieldint/ptr
>]; STRUCT_SN [shape=none, fillcolor=none, label=< - - - + + +
fieldint:ptr
... int:ptr
fieldint:ptr
fieldint/ptr
... int/ptr
fieldint/ptr
>]; - STRUCT_BOT [label=<⊥:struct>, fillcolor=lightgreen, shape=oval] TOP -> STRUCT_TOP; STRUCT_TOP -> STRUCT_S1; @@ -100,11 +94,11 @@ digraph Lattice { // ---------------------- // Memory - MEM_TOP [label=<⊤:mem>, fillcolor=blue, fontcolor=white, shape=oval]; + MEM_TOP [label=<⊤:mem>, fillcolor=blue, fontcolor=white, shape=oval]; + MEM_BOT [label=<⊥:mem>, fillcolor=blue, fontcolor=white, shape=oval]; MEM_ALIAS1 [label="#1" , fillcolor=blue, fontcolor=white]; MEM_ALIASDOTS [label="..." , fillcolor=blue, fontcolor=white, shape=oval]; MEM_ALIASN [label="#n" , fillcolor=blue, fontcolor=white]; - MEM_BOT [label=<⊥:mem>, fillcolor=blue, fontcolor=white, shape=oval]; TOP -> MEM_TOP; MEM_TOP -> MEM_ALIAS1; @@ -120,7 +114,8 @@ digraph Lattice { // ---------------------- // Tuples - TUPLE_TOP [label=<⊤:tuple>, fillcolor=pink, shape=oval]; + TUPLE_TOP [label=<⊤:tuple>, fillcolor=pink, shape=oval]; + TUPLE_BOT [label=<⊥:tuple>, fillcolor=pink, shape=oval]; TUPLE1 [shape=none, fillcolor=none, label=< @@ -144,7 +139,6 @@ digraph Lattice {
>]; - TUPLE_BOT [label=<⊥:tuple>, fillcolor=pink, shape=oval]; TOP -> TUPLE_TOP; TUPLE_TOP -> TUPLE1; @@ -159,11 +153,9 @@ digraph Lattice { // Additional customization {rank=same; TOP;} {rank=same; INT_TOP; XCTRL; STRUCT_TOP; MEM_TOP; TUPLE_TOP} - {rank=same; INT_MIN; INT_MINDOTS; - INT_ZERO; INT_MAXDOTS; - INT_MAX; STRUCT_S1; STRUCT_S2; STRUCT_SN; - MEM_ALIAS1; - MEM_ALIASDOTS; MEM_ALIASN;} + {rank=same; INT_MINDOTS; INT_ZERO; INT_MAXDOTS; + STRUCT_S1; STRUCT_S2; STRUCT_SN; + MEM_ALIAS1; MEM_ALIASDOTS; MEM_ALIASN;} {rank=same; INT_BOT; CTRL; STRUCT_BOT; MEM_BOT; TUPLE_BOT} {rank=same; BOT;} } diff --git a/chapter10/docs/lattice.svg b/chapter10/docs/lattice.svg index 02f3ce69..9eb36bbe 100644 --- a/chapter10/docs/lattice.svg +++ b/chapter10/docs/lattice.svg @@ -4,551 +4,513 @@ - - + + Lattice - + TOP - -⊤ + +⊤ XCTRL - -⊤ -:ctrl + +⊤ +:ctrl TOP->XCTRL - - + + INT_TOP - -⊤ -:int + +⊤ +:int TOP->INT_TOP - - + + - + PTR - - - -*ptr - - -struct + + + +*ptr + + +struct - + TOP->PTR - - + + - + STRUCT_TOP - -⊤ -:struct + +⊤ +:struct - + TOP->STRUCT_TOP - - + + - + MEM_TOP - -⊤ -:mem + +⊤ +:mem - + TOP->MEM_TOP - - + + - + TUPLE_TOP - -⊤ -:tuple + +⊤ +:tuple - + TOP->TUPLE_TOP - - + + BOT - -⊥ + +⊥ CTRL - -⊥ -:ctrl + +⊥ +:ctrl XCTRL->CTRL - - + + CTRL->BOT - - - - - -INT_MIN - --n - - - -INT_TOP->INT_MIN - - + + - + INT_MINDOTS - -... + +... - + INT_TOP->INT_MINDOTS - - + + - + INT_ZERO - -0 + +0 - + INT_TOP->INT_ZERO - - + + - + INT_MAXDOTS - -... + +... - + INT_TOP->INT_MAXDOTS - - - - - -INT_MAX - -+n - - - -INT_TOP->INT_MAX - - + + INT_BOT - -⊥ -:int + +⊥ +:int - + INT_BOT->BOT - - - - - -INT_MIN->INT_BOT - - + + - - + INT_MINDOTS->INT_BOT - - + + - + INT_ZERO->INT_BOT - - + + - + INT_MAXDOTS->INT_BOT - - - - - - -INT_MAX->INT_BOT - - + + - + PTR0 - - - -*ptr? - - -struct + + + +*ptr? + + +struct - + PTR->PTR0 - - + + - + PTR0->BOT - - + + - + STRUCT_S1 - - - -field + + + +field - + - - -int:ptr + + +int/ptr - + STRUCT_TOP->STRUCT_S1 - - + + - + STRUCT_S2 - - - -field + + + +field - + - - -int:ptr - - -field + + +int/ptr + + +field - + - - -int:ptr + + +int/ptr - + STRUCT_TOP->STRUCT_S2 - - + + - + STRUCT_SN - - - -field + + + +field - + - - -int:ptr - - -...   + + +int/ptr + + +...   - + - - -int:ptr - - -field + + +int/ptr + + +field - + - - -int:ptr + + +int/ptr - + STRUCT_TOP->STRUCT_SN - - + + - - + STRUCT_BOT - -⊥ -:struct + +⊥ +:struct + + + +STRUCT_BOT->BOT + + - + STRUCT_S1->STRUCT_BOT - - + + - + - + STRUCT_S2->STRUCT_BOT - - + + + - + STRUCT_SN->STRUCT_BOT - - - - - -STRUCT_BOT->BOT - - + + - + MEM_ALIAS1 - -#1 + +#1 - + MEM_TOP->MEM_ALIAS1 - - + + - + MEM_ALIASDOTS - -... + +... - + MEM_TOP->MEM_ALIASDOTS - - + + - + MEM_ALIASN - -#n + +#n - + MEM_TOP->MEM_ALIASN - - + + - - + MEM_BOT - -⊥ -:mem + +⊥ +:mem + + + +MEM_BOT->BOT + + - + MEM_ALIAS1->MEM_BOT - - + + - + - + MEM_ALIASDOTS->MEM_BOT - - + + + - + MEM_ALIASN->MEM_BOT - - - - - -MEM_BOT->BOT - - + + - + TUPLE1 - - - -Tuple - - -type + + + +Tuple + + +type - + TUPLE_TOP->TUPLE1 - - + + - + TUPLE2 - - - -Tuple - - -type - - -type + + + +Tuple + + +type + + +type - + TUPLE_TOP->TUPLE2 - - + + - + TUPLEN - - - -Tuple - - -type - - -... - - -type + + + +Tuple + + +type + + +... + + +type - + TUPLE_TOP->TUPLEN - - + + - + TUPLE_BOT - -⊥ -:tuple + +⊥ +:tuple + + + +TUPLE_BOT->BOT + + - + TUPLE1->TUPLE_BOT - - + + - + TUPLE2->TUPLE_BOT - - + + - + TUPLEN->TUPLE_BOT - - - - - -TUPLE_BOT->BOT - - + + diff --git a/chapter12/README.md b/chapter12/README.md index 0a32298a..53866440 100644 --- a/chapter12/README.md +++ b/chapter12/README.md @@ -47,7 +47,8 @@ And their own section in the Type lattice: Within the Type Lattice, we now add the following domain: -* Float type - Float values. The same shape as the Integer values, but floats +* Float type - Float values. The same shape as the Integer values, but floats with a TOP, BOT and constants +![Graph1](./docs/lattice.svg) diff --git a/chapter12/docs/lattice.gv b/chapter12/docs/lattice.gv new file mode 100644 index 00000000..eec7cc1d --- /dev/null +++ b/chapter12/docs/lattice.gv @@ -0,0 +1,182 @@ +digraph Lattice { + compound = true; + // Define nodes + splines=false; + node [shape=circle, style=filled]; + 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_MINDOTS [label="...", fillcolor=lightblue, shape=oval]; + INT_ZERO [label="0" , fillcolor=lightblue]; + INT_MAXDOTS [label="...", fillcolor=lightblue, shape=oval]; + + TOP -> INT_TOP; + INT_TOP -> INT_MINDOTS; + INT_TOP -> INT_ZERO; + INT_TOP -> INT_MAXDOTS; + INT_MINDOTS -> INT_BOT; + INT_ZERO -> INT_BOT; + INT_MAXDOTS -> INT_BOT; + INT_BOT -> BOT; + + INT_MINDOTS -> INT_ZERO -> INT_MAXDOTS [style=invis]; + + // ---------------------- + // Integers + FLT_TOP [label=<⊤:flt>, fillcolor=aqua, shape=oval]; + FLT_BOT [label=<⊥:flt>, fillcolor=aqua, shape=oval]; + + FLT_MINDOTS [label="...", fillcolor=aqua, shape=oval]; + FLT_ZERO [label="0" , fillcolor=aqua]; + FLT_MAXDOTS [label="...", fillcolor=aqua, shape=oval]; + + TOP -> FLT_TOP; + FLT_TOP -> FLT_MINDOTS; + FLT_TOP -> FLT_ZERO; + FLT_TOP -> FLT_MAXDOTS; + FLT_MINDOTS -> FLT_BOT; + FLT_ZERO -> FLT_BOT; + FLT_MAXDOTS -> FLT_BOT; + FLT_BOT -> BOT; + + FLT_MINDOTS -> FLT_ZERO -> FLT_MAXDOTS [style=invis]; + + // ---------------------- + // Pointers, just a boolean nil/not and a struct + PTR [shape=none, fillcolor=none, label=< + + + +
*ptr
struct
+ >]; + PTR0 [shape=none, fillcolor=none, label=< + + + +
*ptr?
struct
+ >]; + + TOP -> PTR; + PTR -> PTR0; + PTR0 -> BOT; + + // ---------------------- + // Structs + STRUCT_TOP [label=<⊤:struct>, fillcolor=lightgreen, shape=oval]; + STRUCT_BOT [label=<⊥:struct>, fillcolor=lightgreen, shape=oval]; + + STRUCT_S1 [shape=none, fillcolor=none, label=< + + +
fieldint/ptr
+ >]; + STRUCT_S2 [shape=none, fillcolor=none, label=< + + + +
fieldint/ptr
fieldint/ptr
+ >]; + STRUCT_SN [shape=none, fillcolor=none, label=< + + + + +
fieldint/ptr
... int/ptr
fieldint/ptr
+ >]; + + + TOP -> STRUCT_TOP; + STRUCT_TOP -> STRUCT_S1; + STRUCT_TOP -> STRUCT_S2; + STRUCT_TOP -> STRUCT_SN; + STRUCT_S1 -> STRUCT_BOT; + STRUCT_S2 -> STRUCT_BOT; + STRUCT_SN -> STRUCT_BOT; + STRUCT_BOT -> BOT; + + STRUCT_S1 -> STRUCT_S2 -> STRUCT_SN [style=invis]; + + // ---------------------- + // Memory + MEM_TOP [label=<⊤:mem>, fillcolor=blue, fontcolor=white, shape=oval]; + MEM_BOT [label=<⊥:mem>, fillcolor=blue, fontcolor=white, shape=oval]; + MEM_ALIAS1 [label="#1" , fillcolor=blue, fontcolor=white]; + MEM_ALIASDOTS [label="..." , fillcolor=blue, fontcolor=white, shape=oval]; + MEM_ALIASN [label="#n" , fillcolor=blue, fontcolor=white]; + + TOP -> MEM_TOP; + MEM_TOP -> MEM_ALIAS1; + MEM_TOP -> MEM_ALIASDOTS; + MEM_TOP -> MEM_ALIASN; + MEM_ALIAS1 -> MEM_BOT; + MEM_ALIASDOTS -> MEM_BOT; + MEM_ALIASN -> MEM_BOT; + MEM_BOT -> BOT; + + MEM_ALIAS1 -> MEM_ALIASDOTS -> MEM_ALIASN [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; INT_TOP; FLT_TOP; XCTRL; STRUCT_TOP; MEM_TOP; TUPLE_TOP} + {rank=same; INT_MINDOTS; INT_ZERO; INT_MAXDOTS; + FLT_MINDOTS; FLT_ZERO; FLT_MAXDOTS; + STRUCT_S1; STRUCT_S2; STRUCT_SN; + MEM_ALIAS1; MEM_ALIASDOTS; MEM_ALIASN;} + {rank=same; INT_BOT; FLT_BOT; CTRL; STRUCT_BOT; MEM_BOT; TUPLE_BOT} + {rank=same; BOT;} +} diff --git a/chapter12/docs/lattice.svg b/chapter12/docs/lattice.svg new file mode 100644 index 00000000..1bb4f692 --- /dev/null +++ b/chapter12/docs/lattice.svg @@ -0,0 +1,598 @@ + + + + + + +Lattice + + + +TOP + +⊤ + + + +XCTRL + +⊤ +:ctrl + + + +TOP->XCTRL + + + + + +INT_TOP + +⊤ +:int + + + +TOP->INT_TOP + + + + + +FLT_TOP + +⊤ +:flt + + + +TOP->FLT_TOP + + + + + +PTR + + + +*ptr + + +struct + + + +TOP->PTR + + + + + +STRUCT_TOP + +⊤ +:struct + + + +TOP->STRUCT_TOP + + + + + +MEM_TOP + +⊤ +:mem + + + +TOP->MEM_TOP + + + + + +TUPLE_TOP + +⊤ +:tuple + + + +TOP->TUPLE_TOP + + + + + +BOT + +⊥ + + + +CTRL + +⊥ +:ctrl + + + +XCTRL->CTRL + + + + + +CTRL->BOT + + + + + +INT_MINDOTS + +... + + + +INT_TOP->INT_MINDOTS + + + + + +INT_ZERO + +0 + + + +INT_TOP->INT_ZERO + + + + + +INT_MAXDOTS + +... + + + +INT_TOP->INT_MAXDOTS + + + + + +INT_BOT + +⊥ +:int + + + +INT_BOT->BOT + + + + + +INT_MINDOTS->INT_BOT + + + + + + +INT_ZERO->INT_BOT + + + + + + +INT_MAXDOTS->INT_BOT + + + + + +FLT_MINDOTS + +... + + + +FLT_TOP->FLT_MINDOTS + + + + + +FLT_ZERO + +0 + + + +FLT_TOP->FLT_ZERO + + + + + +FLT_MAXDOTS + +... + + + +FLT_TOP->FLT_MAXDOTS + + + + + +FLT_BOT + +⊥ +:flt + + + +FLT_BOT->BOT + + + + + +FLT_MINDOTS->FLT_BOT + + + + + + +FLT_ZERO->FLT_BOT + + + + + + +FLT_MAXDOTS->FLT_BOT + + + + + +PTR0 + + + +*ptr? + + +struct + + + +PTR->PTR0 + + + + + +PTR0->BOT + + + + + +STRUCT_S1 + + + +field + + + + + + + + +int/ptr + + + +STRUCT_TOP->STRUCT_S1 + + + + + +STRUCT_S2 + + + +field + + + + + + + + +int/ptr + + +field + + + + + + + + +int/ptr + + + +STRUCT_TOP->STRUCT_S2 + + + + + +STRUCT_SN + + + +field + + + + + + + + +int/ptr + + +...   + + + + + + + + +int/ptr + + +field + + + + + + + + +int/ptr + + + +STRUCT_TOP->STRUCT_SN + + + + + +STRUCT_BOT + +⊥ +:struct + + + +STRUCT_BOT->BOT + + + + + +STRUCT_S1->STRUCT_BOT + + + + + + +STRUCT_S2->STRUCT_BOT + + + + + + +STRUCT_SN->STRUCT_BOT + + + + + +MEM_ALIAS1 + +#1 + + + +MEM_TOP->MEM_ALIAS1 + + + + + +MEM_ALIASDOTS + +... + + + +MEM_TOP->MEM_ALIASDOTS + + + + + +MEM_ALIASN + +#n + + + +MEM_TOP->MEM_ALIASN + + + + + +MEM_BOT + +⊥ +:mem + + + +MEM_BOT->BOT + + + + + +MEM_ALIAS1->MEM_BOT + + + + + + +MEM_ALIASDOTS->MEM_BOT + + + + + + +MEM_ALIASN->MEM_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 + + + + + diff --git a/chapter14/README.md b/chapter14/README.md index 8451c4f5..fccb2aa5 100644 --- a/chapter14/README.md +++ b/chapter14/README.md @@ -65,12 +65,27 @@ f32 // IEEE 754 32-bit float ## Type Implementation -The TypeInteger class is reworked to support a full range of min/max values. -At this time, only some power-of-2 sized ranges are exposed but the optimizer +The TypeInteger type class is +reworked to support a full range of min/max values. At this time, only some +power-of-2 sized ranges are exposed to the programmer but the optimizer internally supports all ranges. The MEET operation takes the min-of-mins and max-of-maxes. The DUAL operation inverts the min and max. -The TypeFloat class is also reworked to support 32-bit and 64-bit sizes. +Example: the constant `0` has `[0...0]`. + +Example: the `bool` the range `[0...1]`. + +Example: the `u8` the range `[0...255]`. + +Example: the `i8` the range `[-128...127]`. + +Example: the `dual` of `bool` is `[1...0]` (just swap min and max). + +The TypeFloat class is also reworked to support 32-bit and 64-bit sizes. + +![Graph1](./docs/lattice.svg) + + ## Nodes diff --git a/chapter14/docs/lattice.gv b/chapter14/docs/lattice.gv new file mode 100644 index 00000000..4a8b1d4c --- /dev/null +++ b/chapter14/docs/lattice.gv @@ -0,0 +1,202 @@ +digraph Lattice { + compound = true; + // Define nodes + splines=false; + node [shape=circle, style=filled]; + 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_HI [label="max < min" , fillcolor=lightblue, shape=oval]; + INT_XBOOL [label="1...0", fillcolor=lightblue, shape=oval]; + INT_CON [label="constants", fillcolor=lightblue, shape=oval]; + INT_CON0 [label="0", fillcolor=lightblue]; + INT_CON1 [label="1", fillcolor=lightblue]; + INT_BOOL [label="0...1", fillcolor=lightblue,shape=oval]; + INT_LO [label="max > min" , fillcolor=lightblue, shape=oval]; + + TOP -> INT_TOP; + INT_TOP -> INT_HI; + INT_HI -> INT_XBOOL; + INT_XBOOL -> INT_CON0; + INT_XBOOL -> INT_CON1; + INT_HI -> INT_CON; + INT_CON0 -> INT_BOOL; + INT_CON1 -> INT_BOOL; + INT_BOOL -> INT_LO; + INT_CON -> INT_LO; + INT_LO -> INT_BOT; + INT_BOT -> BOT; + + INT_CON0 -> INT_CON1 -> INT_CON [style=invis]; + + // ---------------------- + // Integers + FLT_TOP [label=<⊤:flt>, fillcolor=aqua, shape=oval]; + FLT_BOT [label=<⊥:flt>, fillcolor=aqua, shape=oval]; + + FLT_CON64 [label="64b consts\n[excludes\n32b consts]" , fillcolor=aqua, shape=oval]; + FLT_CON32 [label="32b consts", fillcolor=aqua, shape=oval]; + FLT_CONPI [label="3.14159...", fillcolor=aqua, shape=oval]; + FLT_X32 [label="~f32", fillcolor=aqua]; + FLT_CON0 [label="0." , fillcolor=aqua]; + FLT_32 [label="f32" , fillcolor=aqua]; + + TOP -> FLT_TOP; + FLT_TOP -> FLT_CON64 + FLT_TOP -> FLT_CONPI + FLT_CON64 -> FLT_BOT + FLT_CONPI -> FLT_BOT + + FLT_TOP -> FLT_X32; + FLT_X32 -> FLT_CON0; + FLT_X32 -> FLT_CON32; + FLT_CON0 -> FLT_32; + FLT_CON32 -> FLT_32; + FLT_32 -> FLT_BOT + + FLT_BOT -> BOT; + + FLT_CON0 -> FLT_CON32 -> FLT_CONPI -> FLT_CON64 [style=invis]; + + + // ---------------------- + // Pointers, just a boolean nil/not and a struct + PTR [shape=none, fillcolor=none, label=< + + + +
*ptr
struct
+ >]; + PTR0 [shape=none, fillcolor=none, label=< + + + +
*ptr?
struct
+ >]; + + TOP -> PTR; + PTR -> PTR0; + PTR0 -> BOT; + + // ---------------------- + // Structs + STRUCT_TOP [label=<⊤:struct>, fillcolor=lightgreen, shape=oval]; + STRUCT_BOT [label=<⊥:struct>, fillcolor=lightgreen, shape=oval]; + + STRUCT_S1 [shape=none, fillcolor=none, label=< + + +
fieldint/ptr
+ >]; + STRUCT_S2 [shape=none, fillcolor=none, label=< + + + +
fieldint/ptr
fieldint/ptr
+ >]; + STRUCT_SN [shape=none, fillcolor=none, label=< + + + + +
fieldint/ptr
... int/ptr
fieldint/ptr
+ >]; + + + TOP -> STRUCT_TOP; + STRUCT_TOP -> STRUCT_S1; + STRUCT_TOP -> STRUCT_S2; + STRUCT_TOP -> STRUCT_SN; + STRUCT_S1 -> STRUCT_BOT; + STRUCT_S2 -> STRUCT_BOT; + STRUCT_SN -> STRUCT_BOT; + STRUCT_BOT -> BOT; + + STRUCT_S1 -> STRUCT_S2 -> STRUCT_SN [style=invis]; + + // ---------------------- + // Memory + MEM_TOP [label=<⊤:mem>, fillcolor=blue, fontcolor=white, shape=oval]; + MEM_BOT [label=<⊥:mem>, fillcolor=blue, fontcolor=white, shape=oval]; + MEM_ALIAS1 [label="#1" , fillcolor=blue, fontcolor=white]; + MEM_ALIASDOTS [label="..." , fillcolor=blue, fontcolor=white, shape=oval]; + MEM_ALIASN [label="#n" , fillcolor=blue, fontcolor=white]; + + TOP -> MEM_TOP; + MEM_TOP -> MEM_ALIAS1; + MEM_TOP -> MEM_ALIASDOTS; + MEM_TOP -> MEM_ALIASN; + MEM_ALIAS1 -> MEM_BOT; + MEM_ALIASDOTS -> MEM_BOT; + MEM_ALIASN -> MEM_BOT; + MEM_BOT -> BOT; + + MEM_ALIAS1 -> MEM_ALIASDOTS -> MEM_ALIASN [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; INT_TOP; FLT_TOP; XCTRL; PTR; STRUCT_TOP; MEM_TOP; TUPLE_TOP} + {rank=same; INT_CON; INT_CON0; INT_CON1; + FLT_CON32; FLT_CON64; FLT_CON0; FLT_CONPI; + STRUCT_S1; STRUCT_S2; STRUCT_SN; + MEM_ALIAS1; MEM_ALIASDOTS; MEM_ALIASN; + TUPLE1; TUPLE2; TUPLEN; + } + {rank=same; INT_BOT; FLT_BOT; CTRL; PTR0; STRUCT_BOT; MEM_BOT; TUPLE_BOT} + {rank=same; BOT;} +} diff --git a/chapter14/docs/lattice.svg b/chapter14/docs/lattice.svg new file mode 100644 index 00000000..99f74ed0 --- /dev/null +++ b/chapter14/docs/lattice.svg @@ -0,0 +1,691 @@ + + + + + + +Lattice + + + +TOP + +⊤ + + + +XCTRL + +⊤ +:ctrl + + + +TOP->XCTRL + + + + + +INT_TOP + +⊤ +:int + + + +TOP->INT_TOP + + + + + +FLT_TOP + +⊤ +:flt + + + +TOP->FLT_TOP + + + + + +PTR + + + +*ptr + + +struct + + + +TOP->PTR + + + + + +STRUCT_TOP + +⊤ +:struct + + + +TOP->STRUCT_TOP + + + + + +MEM_TOP + +⊤ +:mem + + + +TOP->MEM_TOP + + + + + +TUPLE_TOP + +⊤ +:tuple + + + +TOP->TUPLE_TOP + + + + + +BOT + +⊥ + + + +CTRL + +⊥ +:ctrl + + + +XCTRL->CTRL + + + + + +CTRL->BOT + + + + + +INT_HI + +max < min + + + +INT_TOP->INT_HI + + + + + +INT_BOT + +⊥ +:int + + + +INT_BOT->BOT + + + + + +INT_XBOOL + +1...0 + + + +INT_HI->INT_XBOOL + + + + + +INT_CON + +constants + + + +INT_HI->INT_CON + + + + + +INT_CON0 + +0 + + + +INT_XBOOL->INT_CON0 + + + + + +INT_CON1 + +1 + + + +INT_XBOOL->INT_CON1 + + + + + +INT_LO + +max > min + + + +INT_CON->INT_LO + + + + + + +INT_BOOL + +0...1 + + + +INT_CON0->INT_BOOL + + + + + + +INT_CON1->INT_BOOL + + + + + +INT_BOOL->INT_LO + + + + + +INT_LO->INT_BOT + + + + + +FLT_CON64 + +64b consts +[excludes +32b consts] + + + +FLT_TOP->FLT_CON64 + + + + + +FLT_CONPI + +3.14159... + + + +FLT_TOP->FLT_CONPI + + + + + +FLT_X32 + +~f32 + + + +FLT_TOP->FLT_X32 + + + + + +FLT_BOT + +⊥ +:flt + + + +FLT_BOT->BOT + + + + + +FLT_CON64->FLT_BOT + + + + + +FLT_CON32 + +32b consts + + + + +FLT_32 + +f32 + + + +FLT_CON32->FLT_32 + + + + + +FLT_CONPI->FLT_BOT + + + + + + +FLT_X32->FLT_CON32 + + + + + +FLT_CON0 + +0. + + + +FLT_X32->FLT_CON0 + + + + + + +FLT_CON0->FLT_32 + + + + + +FLT_32->FLT_BOT + + + + + +PTR0 + + + +*ptr? + + +struct + + + +PTR->PTR0 + + + + + +PTR0->BOT + + + + + +STRUCT_S1 + + + +field + + + + + + + + +int/ptr + + + +STRUCT_TOP->STRUCT_S1 + + + + + +STRUCT_S2 + + + +field + + + + + + + + +int/ptr + + +field + + + + + + + + +int/ptr + + + +STRUCT_TOP->STRUCT_S2 + + + + + +STRUCT_SN + + + +field + + + + + + + + +int/ptr + + +...   + + + + + + + + +int/ptr + + +field + + + + + + + + +int/ptr + + + +STRUCT_TOP->STRUCT_SN + + + + + +STRUCT_BOT + +⊥ +:struct + + + +STRUCT_BOT->BOT + + + + + +STRUCT_S1->STRUCT_BOT + + + + + + +STRUCT_S2->STRUCT_BOT + + + + + + +STRUCT_SN->STRUCT_BOT + + + + + +MEM_ALIAS1 + +#1 + + + +MEM_TOP->MEM_ALIAS1 + + + + + +MEM_ALIASDOTS + +... + + + +MEM_TOP->MEM_ALIASDOTS + + + + + +MEM_ALIASN + +#n + + + +MEM_TOP->MEM_ALIASN + + + + + +MEM_BOT + +⊥ +:mem + + + +MEM_BOT->BOT + + + + + +MEM_ALIAS1->MEM_BOT + + + + + + +MEM_ALIASDOTS->MEM_BOT + + + + + + +MEM_ALIASN->MEM_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