From 3ba6686fc991998a0a420709dfb0012bbddf77ab Mon Sep 17 00:00:00 2001 From: Cliff Click Date: Tue, 29 Sep 2026 12:21:46 -0700 Subject: Backport lazy memory splits to ch10, split into ch10a and b --- chapter10a/README.md | 183 +++++----- chapter10a/docs/example1.gv | 2 +- chapter10a/docs/example1.svg | 40 +-- chapter10a/docs/example2a.gv | 2 +- chapter10a/docs/example2a.svg | 48 +-- chapter10a/docs/example2b.gv | 7 +- chapter10a/docs/example2b.svg | 49 +-- chapter10a/docs/example2c.gv | 2 +- chapter10a/docs/example2c.svg | 26 +- chapter10a/docs/lattice.gv | 255 ++++++-------- chapter10a/docs/lattice.svg | 726 ++++++++++++++++++++++----------------- chapter10a/docs/type-control.svg | 5 + chapter10a/docs/type-integer.svg | 5 + chapter10a/docs/type-memory.svg | 5 + chapter10a/docs/type-pointer.svg | 5 + chapter10a/docs/type-struct.svg | 5 + chapter10a/docs/type-tuple.svg | 5 + 17 files changed, 741 insertions(+), 629 deletions(-) create mode 100644 chapter10a/docs/type-control.svg create mode 100644 chapter10a/docs/type-integer.svg create mode 100644 chapter10a/docs/type-memory.svg create mode 100644 chapter10a/docs/type-pointer.svg create mode 100644 chapter10a/docs/type-struct.svg create mode 100644 chapter10a/docs/type-tuple.svg (limited to 'chapter10a') diff --git a/chapter10a/README.md b/chapter10a/README.md index 64600fa0..2f25f681 100644 --- a/chapter10a/README.md +++ b/chapter10a/README.md @@ -10,10 +10,11 @@ same in 10a and 10b; the next chapter improves the memory representation. ## One memory value -Arithmetic nodes depend on the values they use. A load also depends on when it -observes memory. In this chapter every store consumes the preceding memory -state and produces the next one. A load consumes memory without changing it. -This makes the source program's effect ordering explicit in the graph. +Arithmetic nodes depend on the values they use, similarly a load also depends +on when it observes memory. In this chapter every store consumes the preceding +memory state and produces the next one, and a load consumes memory without +changing it. This makes the source program's memory ordering explicit in the +graph. ```java struct Point { int x; int y; } @@ -30,27 +31,23 @@ different fields are independent. Chapter 10b will remove it. ![One chain orders stores and loads](docs/example1.svg) -These diagrams are schematic dependency graphs: arrows run from uses to their -definitions. Pointer and value inputs are omitted where they do not explain ordering. - -| Node | Inputs | Result | -|---|---|---| -| `New` | Control and a struct type | A fresh, non-null object pointer | -| `Store` | Memory, pointer, field name, value | The updated whole-memory state | -| `Load` | Memory, pointer, field name | The value of the field | -| `Start` | External entry | Control, initial memory, and `arg` | +| Node | Inputs | Result | +|----------|---|---| +| `New` | Control and a struct type | A fresh, non-null object pointer | +| `Store` | Memory, pointer, field name, value | The updated whole-memory state | +| `Load` | Memory, pointer, field name | The value of the field | +| `Start` | External entry | Control, initial memory, and `arg` | | `Return` | Control, result, memory | Completion with all preceding effects retained | -The memory edge is a dependency token, not a copy of the heap. In the evaluator, -objects contain mutable field arrays; executing a Store changes an array entry. -The graph determines the legal execution order. +The memory edge is a dependency, not a copy of the heap. The graph determines +the legal execution order. In hardware, a Store updates physical memory +directly. In the evaluator, a Store updates an objects' attached memory array. ## Memory is an SSA variable The parser keeps one hidden binding named `$mem`. Source identifiers cannot contain `$`, so user code cannot name it. Reading and updating memory uses the -same `ScopeNode` lookup and update operations as a local variable. Start has a -fixed tuple: control at index 0, memory at index 1, and `arg` at index 2. +same `ScopeNode` lookup and update operations as a local variable. For an `if`, the two branches can finish with different memory values. An ordinary Phi selects the memory from the branch that executed: @@ -88,69 +85,88 @@ optimization, not a correctness problem; it motivates the next chapter. The Type Lattice for Simple has a major revision in this chapter. -![Graph1](./docs/lattice.svg) - -Within the Type Lattice, we now have the following type domains: - -* 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`. - * 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 the whole-memory token - * `⊤:mem` is `TypeMem.TOP`, the high end of the memory domain. - * `⊥:mem` is `TypeMem.BOT`, our conservative type for the whole-memory state. - * Neither token describes the values stored in individual fields. -* Tuple type - when a Node results in a collection of values - -We make use of following operations on the lattice. - -* The `meet` operation takes two types and computes the greatest lower bound - type. While not true for all lattices, in the our lattice this can be - 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 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`. -* 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?`, 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 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`. - * Join of `*void` and `Null` results in `*$TOP`. +![Type lattice with six domains and parallel named struct alternatives](./docs/lattice.svg) + +The diagram uses `⊤` for **top** and `⊥` for **bottom**. A suffix names the +domain: `⊤:struct` is *struct top*, while the bare `⊤` is global top. In the +prose we use those words; in code examples we use the actual Java constants. +The implementation's `$TOP` and `$BOT` names need not appear in the diagram: + +| Diagram | Prose | Java constant | Internal struct name | +|---|---|---|---| +| `⊤:struct` | struct top | `TypeStruct.TOP` | `$TOP` | +| `⊥:struct` | struct bottom | `TypeStruct.BOT` | `$BOT` | + +Edges in this diagram show lattice order, with top above bottom. They are not +the use-to-definition edges of the program graphs elsewhere in the chapter. +Boxes containing an ellipsis abbreviate further parallel alternatives; they +are not extra union types. Field and tuple-element type lattices are elided. + +Within the type lattice, we now have the following domains: + +* ![Control](docs/type-control.svg) represents control flow: unreachable control + at control top, and reachable control at control bottom. +* ![Integer](docs/type-integer.svg) has integer top, integer bottom, and parallel + constants between them. The ellipses stand for the other integer constants. +* ![Pointer](docs/type-pointer.svg) (new) combines a struct type with nullability. + * The prefix `*` means pointer-to: `*Person` is a non-null pointer to a Person. + The suffix `?` includes null, so `*Person?` permits a Person pointer or null. + * The pointer domain contains the whole struct lattice twice, once without + null and once with it. The diagram expands named alternatives in both + copies. It is not just two individual pointer types. + * `null` combines struct top with the nullable flag: it has no non-null + object alternative. The diagram labels it `*⊤:struct?` as well as `null`. + * A pointer to struct bottom can point to any struct. The diagram shows the + non-null form as `*⊥:struct` and the nullable form as `*⊥:struct?`. + The latter is pointer bottom; pointer top is `*⊤:struct`. + * Null evaluates to false; non-null pointers evaluate to true. + + > C analogy: the non-null pointer to struct bottom is akin to `void *`, except + > that C's `void *` may also be null. Simple names this constant + > `TypeMemPtr.VOIDPTR` and prints it as `*void`. Struct bottom itself is the + > common lower bound of struct types, not C's `void` type. + +* ![Struct](docs/type-struct.svg) (new) represents user-defined named structs. + Fields have integer types in this chapter. + * Struct top lies above every named struct; struct bottom lies below every + named struct. Top is the high/empty struct alternative, while bottom + conservatively includes any struct name. + * `Person`, `s1`, `s2`, and further names are parallel alternatives. There is + no inheritance, so different named structs do not nest beneath one another, + even if they have identical fields. + * There is no fixed bound on the names a program can declare. The diagram's + ellipsis stands for more named alternatives, not a distinguished unnamed + struct. Each named box abbreviates its own field-type lattice. +* ![Memory](docs/type-memory.svg) (new) represents the whole-memory token. + Memory top and memory bottom are `TypeMem.TOP` and `TypeMem.BOT`. Neither + records the values stored in individual fields. +* ![Tuple](docs/type-tuple.svg) represents a collection of results from one node, + such as Start's control, memory, and argument. The displayed shapes abbreviate + tuples of different lengths and their element-type lattices. + +We use the following operations on the lattice: + +* **Meet** computes the greatest lower bound. For these examples, think of + combining the alternatives represented by its inputs. + * The meet of `Person` and `s1` is struct bottom. There is no separate type + representing exactly those two names. + * The meet of `*Person` and `*s1` is the non-null pointer to struct bottom. + * The meet of `*Person` and `null` is `*Person?`. + * The meet of the non-null pointer to struct bottom and `null` is pointer bottom. + * The meet of `1` and `2` is integer bottom. +* **Dual** reflects the lattice about its centerline: top and bottom exchange + places, and applying dual twice returns the original type. + * Struct top and struct bottom are duals. + * `null` and the non-null pointer to struct bottom are duals. + * A pointer's dual also duals its struct's fields and flips nullability. Thus + the dual of `*Person` is not generally the original `*Person?`: the field + types must be dualed too. Those field details are omitted in the diagram. +* **Join** computes the least upper bound. It is defined through meet and dual: + `JOIN(x,y) = MEET(x.dual(),y.dual()).dual()`. + * The join of `Person` and `s1` is struct top. + * The join of `*Person` and `*s1` is pointer top. + * The join of the non-null pointer to struct bottom and `null` is pointer top. + * The join of `1` and `2` is integer top. As we construct the Sea of Nodes graph, we ensure that values stay inside the domain they are created in - that is ptr fields will never contain ints @@ -221,8 +237,9 @@ To enable this behaviour, we make following enhancements. predicate is a ptr value. The up-cast removes the null possibility on the true branch making it legal to use the pointer. -* The up-cast is done using a `Cast` op with the type `*void`. This does a - lattice JOIN of the original type and `*void`. This JOIN operation preserves +* The up-cast uses a `Cast` with the non-null pointer to struct bottom + (`TypeMemPtr.VOIDPTR`). It joins the original pointer type with that type, + corresponding to `*⊥:struct` in the diagram. This JOIN operation preserves everything we already know about ptr, and also adds the new knowledge that the ptr is not-null. diff --git a/chapter10a/docs/example1.gv b/chapter10a/docs/example1.gv index e34c73ed..d399b562 100644 --- a/chapter10a/docs/example1.gv +++ b/chapter10a/docs/example1.gv @@ -1,5 +1,5 @@ digraph Memory { - rankdir=LR; + rankdir=RL; node [shape=box]; M0 [label="Initial memory"]; X [label="Store p.x = 3"]; diff --git a/chapter10a/docs/example1.svg b/chapter10a/docs/example1.svg index c0668ce3..d1c5e3bd 100644 --- a/chapter10a/docs/example1.svg +++ b/chapter10a/docs/example1.svg @@ -12,62 +12,62 @@ M0 - -Initial memory + +Initial memory X - -Store p.x = 3 + +Store p.x = 3 X->M0 - - + + Y - -Store p.y = arg + +Store p.y = arg Y->X - - + + L - -Load p.x + +Load p.x L->Y - - + + Return - -Return + +Return Return->Y - - + + Return->L - - + + diff --git a/chapter10a/docs/example2a.gv b/chapter10a/docs/example2a.gv index 64e774fc..ec5afbdc 100644 --- a/chapter10a/docs/example2a.gv +++ b/chapter10a/docs/example2a.gv @@ -1,5 +1,5 @@ digraph Memory { - rankdir=LR; + rankdir=RL; node [shape=box]; M [label="Incoming memory"]; A [label="True: Store x"]; diff --git a/chapter10a/docs/example2a.svg b/chapter10a/docs/example2a.svg index c6801f59..f9a9b4fd 100644 --- a/chapter10a/docs/example2a.svg +++ b/chapter10a/docs/example2a.svg @@ -12,74 +12,74 @@ M - -Incoming memory + +Incoming memory A - -True: Store x + +True: Store x A->M - - + + B - -False: Store y + +False: Store y B->M - - + + P - -Phi(memory) + +Phi(memory) P->A - - + + P->B - - + + Region - -Region + +Region P->Region - - + + Return - -Return + +Return Return->P - - + + diff --git a/chapter10a/docs/example2b.gv b/chapter10a/docs/example2b.gv index 7ccbcc99..3f3309e5 100644 --- a/chapter10a/docs/example2b.gv +++ b/chapter10a/docs/example2b.gv @@ -1,8 +1,11 @@ digraph Memory { - rankdir=LR; + rankdir=RL; node [shape=box]; P [label="Phi(memory)"]; S [label="Loop-body Store"]; - P -> Entry [color=blue]; P -> S -> P [color=blue]; + P -> Entry [color=blue]; + P -> S [color=blue,constraint=false]; // Backedge must not place Store before Phi. + S -> P [color=blue]; P -> Loop [style=dashed]; Return -> P [color=blue]; + Return -> S [style=invis]; // Layout only: Phi, Store, Return from left to right. } diff --git a/chapter10a/docs/example2b.svg b/chapter10a/docs/example2b.svg index 063a6f21..8fff33d4 100644 --- a/chapter10a/docs/example2b.svg +++ b/chapter10a/docs/example2b.svg @@ -4,70 +4,71 @@ - - + + Memory - + P - -Phi(memory) + +Phi(memory) S - -Loop-body Store + +Loop-body Store P->S - - + + Entry - -Entry + +Entry P->Entry - - + + Loop - -Loop + +Loop P->Loop - - + + S->P - - + + Return - -Return + +Return Return->P - - + + + diff --git a/chapter10a/docs/example2c.gv b/chapter10a/docs/example2c.gv index 0c7cf67d..ef8a5fc8 100644 --- a/chapter10a/docs/example2c.gv +++ b/chapter10a/docs/example2c.gv @@ -1,5 +1,5 @@ digraph Memory { - rankdir=LR; + rankdir=RL; node [shape=box]; M [label="Prior memory"]; L [label="Load p.x"]; diff --git a/chapter10a/docs/example2c.svg b/chapter10a/docs/example2c.svg index a4d2f53e..c7b37912 100644 --- a/chapter10a/docs/example2c.svg +++ b/chapter10a/docs/example2c.svg @@ -12,39 +12,39 @@ M - -Prior memory + +Prior memory L - -Load p.x + +Load p.x L->M - - + + S - -Store p.x + +Store p.x S->M - - + + S->L - - -execute load first + + +execute load first diff --git a/chapter10a/docs/lattice.gv b/chapter10a/docs/lattice.gv index b2d8255e..733a5287 100644 --- a/chapter10a/docs/lattice.gv +++ b/chapter10a/docs/lattice.gv @@ -1,151 +1,108 @@ 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]; - - // ---------------------- - // 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]; - - TOP -> MEM_TOP; - MEM_TOP -> MEM_BOT; - MEM_BOT -> BOT; - - - // ---------------------- - // 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; XCTRL; STRUCT_TOP; MEM_TOP; TUPLE_TOP} - {rank=same; INT_MINDOTS; INT_ZERO; INT_MAXDOTS; - STRUCT_S1; STRUCT_S2; STRUCT_SN;} - {rank=same; INT_BOT; CTRL; STRUCT_BOT; MEM_BOT; TUPLE_BOT} - {rank=same; BOT;} + rankdir=TB; + newrank=true; + // Preserve the same-rank ordering edges through cluster layout. + remincross=false; + nodesep=0.22; + ranksep=0.65; + node [shape=ellipse, style=filled, fontname="DejaVu Sans", fontsize=13]; + edge [color="#555555", arrowsize=0.6]; + + // These arrows are lattice-order edges, not use/definition edges. + TOP [label="⊤", fillcolor=black, fontcolor=white]; + BOT [label="⊥", fillcolor=black, fontcolor=white]; + + subgraph cluster_control { + label="Control"; fontname="Arial"; color="#cccccc"; + node [fillcolor="#ffff00"]; + XCTRL [label="⊤:ctrl"]; + CTRL [label="⊥:ctrl"]; + XCTRL -> CTRL; + } + + subgraph cluster_integer { + label="Integer"; fontname="Arial"; color="#cccccc"; + node [fillcolor="#add8e6"]; + INT_TOP [label="⊤:int"]; + INT_BOT [label="⊥:int"]; + INT_NEG [label="… −2, −1"]; + INT_ZERO [label="0"]; + INT_POS [label="1, 2, …"]; + {rank=same; INT_NEG; INT_ZERO; INT_POS;} + INT_NEG -> INT_ZERO -> INT_POS [style=invis]; + INT_TOP -> {INT_NEG INT_ZERO INT_POS}; + {INT_NEG INT_ZERO INT_POS} -> INT_BOT; + } + + subgraph cluster_pointer { + label="Pointer = nullability × struct type"; + fontname="Arial"; color="#cccccc"; + node [fillcolor="#008000", fontcolor=white]; + PTR_TOP [label="⊤:ptr\n[*⊤:struct]"]; + PTR_BOT [label="⊥:ptr\n[*⊥:struct?]"]; + PTR_NULL [label="null"]; + PTR_ANY [label="*⊥:struct\n[ptr any struct]"]; + PTR_PERSON [label="*Person"]; + PTR_S1 [label="*s1"]; + PTR_MORE [label="*s2, …"]; + PTR_PERSON_NIL [label="*Person?"]; + PTR_S1_NIL [label="*s1?"]; + PTR_MORE_NIL [label="*s2?, …"]; + {rank=same; PTR_PERSON; PTR_S1; PTR_MORE; PTR_NULL;} + {rank=same; PTR_ANY; PTR_PERSON_NIL; PTR_S1_NIL; PTR_MORE_NIL;} + PTR_PERSON -> PTR_S1 -> PTR_MORE -> PTR_NULL [style=invis]; + PTR_ANY -> PTR_PERSON_NIL -> PTR_S1_NIL -> PTR_MORE_NIL [style=invis]; + PTR_TOP -> {PTR_PERSON PTR_S1 PTR_MORE PTR_NULL}; + {PTR_PERSON PTR_S1 PTR_MORE} -> PTR_ANY; + PTR_PERSON -> PTR_PERSON_NIL; + PTR_S1 -> PTR_S1_NIL; + PTR_MORE -> PTR_MORE_NIL; + PTR_NULL -> {PTR_PERSON_NIL PTR_S1_NIL PTR_MORE_NIL}; + {PTR_ANY PTR_PERSON_NIL PTR_S1_NIL PTR_MORE_NIL} -> PTR_BOT; + } + + subgraph cluster_struct { + label="Struct\nnamed collection of named scalar types"; + fontname="Arial"; color="#cccccc"; + node [fillcolor="#90ee90"]; + STRUCT_TOP [label="⊤:struct\n[struct top]"]; + STRUCT_BOT [label="⊥:struct\n[struct bottom]"]; + STRUCT_PERSON [label="Person\nage: int", shape=box]; + STRUCT_S1 [label="s1\nx: int", shape=box]; + STRUCT_S2 [label="s2\nx: int, y: *s1", shape=box]; + STRUCT_MORE [label="…", shape=box]; + {rank=same; STRUCT_PERSON; STRUCT_S1; STRUCT_S2; STRUCT_MORE;} + STRUCT_PERSON -> STRUCT_S1 -> STRUCT_S2 -> STRUCT_MORE [style=invis]; + STRUCT_TOP -> {STRUCT_PERSON STRUCT_S1 STRUCT_S2 STRUCT_MORE}; + {STRUCT_PERSON STRUCT_S1 STRUCT_S2 STRUCT_MORE} -> STRUCT_BOT; + } + + subgraph cluster_memory { + label="Memory"; fontname="Arial"; color="#cccccc"; + node [fillcolor="#00008b", fontcolor=white]; + MEM_TOP [label="⊤:mem"]; + MEM_BOT [label="⊥:mem"]; + MEM_TOP -> MEM_BOT; + } + + subgraph cluster_tuple { + label="Tuple\ncollection of types"; + fontname="Arial"; color="#cccccc"; + node [fillcolor="#ffc0cb"]; + TUPLE_TOP [label="⊤:tuple"]; + TUPLE_BOT [label="⊥:tuple"]; + TUPLE1 [label="(type)", shape=box]; + TUPLE2 [label="(type, type)", shape=box]; + TUPLEN [label="(type, …)", shape=box]; + {rank=same; TUPLE1; TUPLE2; TUPLEN;} + TUPLE1 -> TUPLE2 -> TUPLEN [style=invis]; + TUPLE_TOP -> {TUPLE1 TUPLE2 TUPLEN}; + {TUPLE1 TUPLE2 TUPLEN} -> TUPLE_BOT; + } + + TOP -> {XCTRL INT_TOP PTR_TOP STRUCT_TOP MEM_TOP TUPLE_TOP}; + {CTRL INT_BOT PTR_BOT STRUCT_BOT MEM_BOT TUPLE_BOT} -> BOT; + {rank=same; XCTRL; INT_TOP; PTR_TOP; STRUCT_TOP; MEM_TOP; TUPLE_TOP;} + {rank=same; CTRL; INT_BOT; PTR_BOT; STRUCT_BOT; MEM_BOT; TUPLE_BOT;} + XCTRL -> INT_TOP -> PTR_TOP -> STRUCT_TOP -> MEM_TOP -> TUPLE_TOP [style=invis]; } diff --git a/chapter10a/docs/lattice.svg b/chapter10a/docs/lattice.svg index aa296366..24c0de8c 100644 --- a/chapter10a/docs/lattice.svg +++ b/chapter10a/docs/lattice.svg @@ -4,463 +4,567 @@ - - + + Lattice - + + +cluster_control + +Control + + +cluster_integer + +Integer + + +cluster_pointer + +Pointer = nullability × struct type + + +cluster_struct + +Struct +named collection of named scalar types + + +cluster_memory + +Memory + + +cluster_tuple + +Tuple +collection of types + TOP - -⊤ + +⊤ XCTRL - -⊤ -:ctrl + +⊤:ctrl - + TOP->XCTRL - - + + INT_TOP - -⊤ -:int + +⊤:int - + TOP->INT_TOP - - + + - + -PTR - - - -*ptr - - -struct - - - -TOP->PTR - - +PTR_TOP + +⊤:ptr +[*⊤:struct] + + + +TOP->PTR_TOP + + - + STRUCT_TOP - -⊤ -:struct + +⊤:struct +[struct top] - + 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_MINDOTS - -... +INT_NEG + +… −2, −1 - - -INT_TOP->INT_MINDOTS - - + + +INT_TOP->INT_NEG + + INT_ZERO - -0 + +0 - + INT_TOP->INT_ZERO - - + + - + -INT_MAXDOTS - -... +INT_POS + +1, 2, … - - -INT_TOP->INT_MAXDOTS - - + + +INT_TOP->INT_POS + + + INT_BOT - -⊥ -:int + +⊥:int - + INT_BOT->BOT - - + + - - -INT_MINDOTS->INT_BOT - - + + +INT_NEG->INT_BOT + + - + - + INT_ZERO->INT_BOT - - + + + + + + +INT_POS->INT_BOT + + - - - -INT_MAXDOTS->INT_BOT - - + + +PTR_NULL + +null +[*⊤:struct?] - - -PTR0 - - - -*ptr? - - -struct - - - -PTR->PTR0 - - - - + -PTR0->BOT - - +PTR_TOP->PTR_NULL + + - + +PTR_PERSON + +*Person + + + +PTR_TOP->PTR_PERSON + + + + + +PTR_S1 + +*s1 + + + +PTR_TOP->PTR_S1 + + + + + +PTR_MORE + +*s2, … + + + +PTR_TOP->PTR_MORE + + + + + + +PTR_BOT + +⊥:ptr +[*⊥:struct?] + + + +PTR_BOT->BOT + + + + + +PTR_PERSON_NIL + +*Person? + + + +PTR_NULL->PTR_PERSON_NIL + + + + + +PTR_S1_NIL + +*s1? + + + +PTR_NULL->PTR_S1_NIL + + + + + +PTR_MORE_NIL + +*s2?, … + + + +PTR_NULL->PTR_MORE_NIL + + + + + +PTR_ANY + +*⊥:struct +[ptr any struct] + + + +PTR_ANY->PTR_BOT + + + + + + +PTR_PERSON->PTR_ANY + + + + + + +PTR_PERSON->PTR_PERSON_NIL + + + + + +PTR_S1->PTR_ANY + + + + + + +PTR_S1->PTR_S1_NIL + + + + + + +PTR_MORE->PTR_ANY + + + + + +PTR_MORE->PTR_MORE_NIL + + + + + +PTR_PERSON_NIL->PTR_BOT + + + + + + +PTR_S1_NIL->PTR_BOT + + + + + + +PTR_MORE_NIL->PTR_BOT + + + + + +STRUCT_PERSON + +Person +age: int + + + +STRUCT_TOP->STRUCT_PERSON + + + + + STRUCT_S1 - - - -field - - - - - - - - -int/ptr + +s1 +x: int - + STRUCT_TOP->STRUCT_S1 - - + + - + STRUCT_S2 - - - -field - - - - - - - - -int/ptr - - -field - - - - - - - - -int/ptr + +s2 +x: int, y: int - + STRUCT_TOP->STRUCT_S2 - - - - - -STRUCT_SN - - - -field - - - - - - - - -int/ptr - - -...   - - - - - - - - -int/ptr - - -field - - - - - - - - -int/ptr - - - -STRUCT_TOP->STRUCT_SN - - - + + + + + +STRUCT_MORE + +… + + + +STRUCT_TOP->STRUCT_MORE + + + + - + STRUCT_BOT - -⊥ -:struct + +⊥:struct +[struct bottom] - + STRUCT_BOT->BOT - - + + + + +STRUCT_PERSON->STRUCT_BOT + + + + - + STRUCT_S1->STRUCT_BOT - - + + - + STRUCT_S2->STRUCT_BOT - - + + - - - -STRUCT_SN->STRUCT_BOT - - + + + +STRUCT_MORE->STRUCT_BOT + + - + MEM_BOT - -⊥ -:mem + +⊥:mem - + MEM_TOP->MEM_BOT - - + + + - + MEM_BOT->BOT - - + + - + TUPLE1 - - - -Tuple - - -type + +(type) - + TUPLE_TOP->TUPLE1 - - + + - + TUPLE2 - - - -Tuple - - -type - - -type + +(type, type) - + TUPLE_TOP->TUPLE2 - - + + - + TUPLEN - - - -Tuple - - -type - - -... - - -type + +(type, …) - + TUPLE_TOP->TUPLEN - - + + - + TUPLE_BOT - -⊥ -:tuple + +⊥:tuple - + TUPLE_BOT->BOT - - + + - + TUPLE1->TUPLE_BOT - - + + + - + TUPLE2->TUPLE_BOT - - + + + - + TUPLEN->TUPLE_BOT - - + + diff --git a/chapter10a/docs/type-control.svg b/chapter10a/docs/type-control.svg new file mode 100644 index 00000000..d4b79c53 --- /dev/null +++ b/chapter10a/docs/type-control.svg @@ -0,0 +1,5 @@ + + Control + + Control + diff --git a/chapter10a/docs/type-integer.svg b/chapter10a/docs/type-integer.svg new file mode 100644 index 00000000..97d03372 --- /dev/null +++ b/chapter10a/docs/type-integer.svg @@ -0,0 +1,5 @@ + + Integer + + Integer + diff --git a/chapter10a/docs/type-memory.svg b/chapter10a/docs/type-memory.svg new file mode 100644 index 00000000..16b5121f --- /dev/null +++ b/chapter10a/docs/type-memory.svg @@ -0,0 +1,5 @@ + + Memory + + Memory + diff --git a/chapter10a/docs/type-pointer.svg b/chapter10a/docs/type-pointer.svg new file mode 100644 index 00000000..7604492e --- /dev/null +++ b/chapter10a/docs/type-pointer.svg @@ -0,0 +1,5 @@ + + Pointer + + Pointer + diff --git a/chapter10a/docs/type-struct.svg b/chapter10a/docs/type-struct.svg new file mode 100644 index 00000000..97a16562 --- /dev/null +++ b/chapter10a/docs/type-struct.svg @@ -0,0 +1,5 @@ + + Struct + + Struct + diff --git a/chapter10a/docs/type-tuple.svg b/chapter10a/docs/type-tuple.svg new file mode 100644 index 00000000..691478ac --- /dev/null +++ b/chapter10a/docs/type-tuple.svg @@ -0,0 +1,5 @@ + + Tuple + + Tuple + -- cgit v1.2.3