From 502e7e752f3efdb069a36b23ab51ac22f9d74e9e Mon Sep 17 00:00:00 2001 From: Cliff Click Date: Tue, 29 Sep 2026 12:34:58 -0700 Subject: Chapter 10a: Structs and Memory --- docs/chapter10a/10-grammar.md | 125 +++++++++ docs/chapter10a/Makefile | 14 + docs/chapter10a/README.md | 290 ++++++++++++++++++++ docs/chapter10a/example1.gv | 10 + docs/chapter10a/example1.svg | 73 +++++ docs/chapter10a/example2a.gv | 10 + docs/chapter10a/example2a.svg | 85 ++++++ docs/chapter10a/example2b.gv | 11 + docs/chapter10a/example2b.svg | 74 +++++ docs/chapter10a/example2c.gv | 9 + docs/chapter10a/example2c.svg | 50 ++++ docs/chapter10a/lattice.gv | 108 ++++++++ docs/chapter10a/lattice.svg | 570 +++++++++++++++++++++++++++++++++++++++ docs/chapter10a/type-control.svg | 5 + docs/chapter10a/type-integer.svg | 5 + docs/chapter10a/type-memory.svg | 5 + docs/chapter10a/type-pointer.svg | 5 + docs/chapter10a/type-struct.svg | 5 + docs/chapter10a/type-tuple.svg | 5 + 19 files changed, 1459 insertions(+) create mode 100644 docs/chapter10a/10-grammar.md create mode 100644 docs/chapter10a/Makefile create mode 100644 docs/chapter10a/README.md create mode 100644 docs/chapter10a/example1.gv create mode 100644 docs/chapter10a/example1.svg create mode 100644 docs/chapter10a/example2a.gv create mode 100644 docs/chapter10a/example2a.svg create mode 100644 docs/chapter10a/example2b.gv create mode 100644 docs/chapter10a/example2b.svg create mode 100644 docs/chapter10a/example2c.gv create mode 100644 docs/chapter10a/example2c.svg create mode 100644 docs/chapter10a/lattice.gv create mode 100644 docs/chapter10a/lattice.svg create mode 100644 docs/chapter10a/type-control.svg create mode 100644 docs/chapter10a/type-integer.svg create mode 100644 docs/chapter10a/type-memory.svg create mode 100644 docs/chapter10a/type-pointer.svg create mode 100644 docs/chapter10a/type-struct.svg create mode 100644 docs/chapter10a/type-tuple.svg (limited to 'docs') diff --git a/docs/chapter10a/10-grammar.md b/docs/chapter10a/10-grammar.md new file mode 100644 index 00000000..5b9b680e --- /dev/null +++ b/docs/chapter10a/10-grammar.md @@ -0,0 +1,125 @@ +# Grammar for Chapter 10a + +```antlrv4 +grammar SimpleLanguage; + +program + : statement+ EOF + ; + +statement + : returnStatement + | structDeclaration + | declStatement + | blockStatment + | expressionStatement + | ifStatement + | whileStatement + | breakStatement + | continueStatment + ; + +field + : 'int' IDENTIFIER ';' + ; + +fields + : field+ + ; + +structDeclaration + : 'struct' IDENTIFIER '{' fields '}' + ; + +whileStatement + : 'while' '(' expression ')' statement + ; + +breakStatement + : 'break' ';' + ; + +continueStatement + : 'continue' ';' + ; + +ifStatement + : 'if' '(' expression ')' statement ('else' statement)? + ; + + +expressionStatement + : IDENTIFIER '=' expression ';' + | fieldExpression '=' expression ';' + ; + +blockStatement + : '{' statement+ '}' + ; + +structName + : IDENTIFIER + ; + +declStatement + : 'int' IDENTIFIER '=' expression ';' + | structName ('?')? IDENTIFIER '=' expression ';' + ; + +returnStatement + : 'return' expression ';' + ; + +expression + : comparisonExpression + ; + +comparisonExpression + : additiveExpression (('==' | '!='| '>'| '<'| '>='| '<=') additiveExpression)* + ; + +additiveExpression + : multiplicativeExpression (('+' | '-') multiplicativeExpression)* + ; + +multiplicativeExpression + : unaryExpression (('*' | '/') unaryExpression)* + ; + +unaryExpression + : ('-') unaryExpression + | '!' unaryExpression + | primaryExpression + ; + +newExpression + : 'new' IDENTIFIER + ; + +fieldExpression + : primaryExpresson '.' IDENTIFIER + ; + +primaryExpression + : IDENTIFIER + | INTEGER_LITERAL + | 'true' + | 'false' + | 'null' + | newExpression + | '(' expression ')' + | fieldExpression + ; + +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/chapter10a/Makefile b/docs/chapter10a/Makefile new file mode 100644 index 00000000..055882b2 --- /dev/null +++ b/docs/chapter10a/Makefile @@ -0,0 +1,14 @@ +GV := $(wildcard *.gv) +SVG := $(patsubst %.gv,%.svg,$(GV)) +.DELETE_ON_ERROR: + +.PHONY: all +all: $(SVG) + +%.svg: %.gv + dot -Tsvg $< > $@ + @sed -i 's/\r$$//' $@ + +.PHONY: clean +clean: + @rm -f $(SVG) diff --git a/docs/chapter10a/README.md b/docs/chapter10a/README.md new file mode 100644 index 00000000..8aaf779c --- /dev/null +++ b/docs/chapter10a/README.md @@ -0,0 +1,290 @@ +# Chapter 10a: Structs and Memory + +[Previous: Chapter 9](../chapter09/README.md) | +[Next: Chapter 10b](../chapter10b/README.md) + +This chapter adds user-defined structs, pointers, allocation, field loads and +stores, and null checking. It also introduces an evaluator that executes the +graph, including its memory effects. The [grammar](10-grammar.md) is the +same in 10a and 10b; the next chapter improves the memory representation. + +## One memory value + +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; } +Point p = new Point; +p.x = 3; +p.y = arg; +return p.x; +``` + +`NewNode` produces the pointer. The parser emits stores of zero for both fields, +then stores 3 into `x` and `arg` into `y`. The final load observes the memory +after the `y` store. We deliberately keep that dependency here, even though +different fields are independent. Chapter 10b will remove it. + +![One chain orders stores and loads](example1.svg) + +| 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, 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. + +For an `if`, the two branches can finish with different memory values. An +ordinary Phi selects the memory from the branch that executed: + +![Whole memory across a branch](example2a.svg) + +Loops reuse Chapter 8's lazy Phi construction. Reading or updating `$mem` in a +loop creates an initially incomplete memory Phi. Closing the loop supplies its +backedge. `break`, `continue`, nested loops, and early returns use the same scope +mechanics as scalar variables. + +![Whole memory around a loop](example2b.svg) + +Every Return consumes the current whole-memory value. This keeps stores alive +even when the returned scalar does not depend on them, or when the program +returns the modified object itself. + +## Local memory optimizations + +A load immediately following a store to the **same pointer and field** can use +the stored value. A store immediately following another store to the same +address can discard the earlier store when no other user needs it. Both the +pointer and field checks matter: two different fields of one object are +different addresses, as are the same fields of two different objects. + +A load can also move through a memory Phi when doing so exposes a useful +load-after-store fold. On a loop, the backedge must fold, preventing this rewrite +from repeatedly moving the load around the cycle. + +The single chain is conservative. A store to `y` can prevent forwarding an +earlier store to `x`, even when the objects are identical. This is a missed +optimization, not a correctness problem; it motivates the next chapter. + +## Enhanced Type Lattice + +The Type Lattice for Simple has a major revision in this chapter. + +![Type lattice with six domains and parallel named struct alternatives](./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](type-control.svg) represents control flow: unreachable control + at control top, and reachable control at control bottom. +* ![Integer](type-integer.svg) has integer top, integer bottom, and parallel + constants between them. The ellipses stand for the other integer constants. +* ![Pointer](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](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](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](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 +(obviously)... nor even the generic `TOP` and `BOT`. There are a couple of +nuances worth highlighting. + +* When Phis are created, the initial type of the Phi is based on the declared + type of its first input. This is a pessimistic type assignment because we do + not yet know what other types will be met. + +* When all the inputs of the Phi are known, we start with the local Top of the + declared type, and then compute a meet of all the input types. This + computation results in a more refined type for the Phi. + +## Parser Enhancements + +In previous chapters the only available type was Integer. Now, variables can +be of Integer type or pointer to Struct types. To support this, the Parser now +tracks the declared type of a variable (used to only be Integer!). The +declared type of a variable defines the set of values that can be legitimately +assigned to the variable. The Sea of Nodes graph also tracks the actual type +of values assigned to variables, these type transitions are defined by the Type +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 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. + +Here are two motivating examples: + +```java +struct Bar { int a; } +Bar? bar = new Bar; +if (arg) bar = null; +if( bar ) bar.a = 1; +``` + +If `bar` is not `null` above, then we would like to allow the assignment to +`bar.a`. If the final line lacked the null check, e.g. a plain `bar.a = 1;`, +then `Java` would compile this program but throw a NPE, and Simple rejects the +program pointing out a null check is required. + + +```java +struct Bar { int a; } +Bar? bar = new Bar; +if (arg) bar = null; +int rez = 3; +if( !bar ) rez=4; +else bar.a = 1; +``` + +If `bar` is `null` then we would like `!bar` to evaluate to `true`. In the else +branch we know `bar` is not null, hence the assignment to `bar.a` should be +allowed. + +To enable this behaviour, we make following enhancements. + +* We track the null-ness of a pointer in the Type system, and hence in every + Node that ptr type flows through. + +* We "wrap" the predicate of an `If` node with an up-cast when we see that the + 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 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. + +* The up-cast is represented by the `CastNode` op, and if applicable, we + replace all occurrences of the original predicate with the up-cast in the + current scope. The change is local to each branch of the `If`; occuring + separately for the true and the false branches of the `If` (and the false + branch inverts the predicate). + +* The up-cast peepholes normally; if its input's type is a super type of the + up-cast, then the `CastNode` can be removed. See `ScopeNode.upcast()` method, + and `CastNode`. + +* When computing a type for Not, we produce an Integer type when its input is a + ptr. When the input is a `null` we convert to `1` and when is a not `null` + ptr value, we convert to `0`. See `NotNode.compute()`. + + +## Executing the graph + +The evaluator includes a small late scheduler. A load must execute before a +later store that consumes the same memory definition, even though there is no +ordinary data edge from the load to that store. These load/store +anti-dependencies supplement the explicit graph edges. + +![A load must precede a clobbering store](example2c.svg) + +The scheduler is sufficient to execute this chapter. Chapter 11 develops +global code motion and scheduling as a separate topic. + +## Build and test + +From this directory, with JDK 21 or newer, Make, and a shell: + +```sh +make lib +make tests +make release +make view +``` + +Make builds this snapshot directly, without Maven. `make release` produces +`build/release/simple.jar`; `make view` launches the shared interactive graph +viewer. Maven and IDEA module descriptions are also supplied. Tests include all +earlier chapters, memory ordering, returned object contents, and nested loops. + +Next, [Chapter 10b](../chapter10b/README.md) keeps this one parser binding while +splitting the graph into independent memory slices. diff --git a/docs/chapter10a/example1.gv b/docs/chapter10a/example1.gv new file mode 100644 index 00000000..d399b562 --- /dev/null +++ b/docs/chapter10a/example1.gv @@ -0,0 +1,10 @@ +digraph Memory { + rankdir=RL; + node [shape=box]; + M0 [label="Initial memory"]; + X [label="Store p.x = 3"]; + Y [label="Store p.y = arg"]; + L [label="Load p.x"]; + L -> Y -> X -> M0 [color=blue]; + Return -> Y [color=blue]; Return -> L; +} diff --git a/docs/chapter10a/example1.svg b/docs/chapter10a/example1.svg new file mode 100644 index 00000000..d1c5e3bd --- /dev/null +++ b/docs/chapter10a/example1.svg @@ -0,0 +1,73 @@ + + + + + + +Memory + + + +M0 + +Initial memory + + + +X + +Store p.x = 3 + + + +X->M0 + + + + + +Y + +Store p.y = arg + + + +Y->X + + + + + +L + +Load p.x + + + +L->Y + + + + + +Return + +Return + + + +Return->Y + + + + + +Return->L + + + + + diff --git a/docs/chapter10a/example2a.gv b/docs/chapter10a/example2a.gv new file mode 100644 index 00000000..ec5afbdc --- /dev/null +++ b/docs/chapter10a/example2a.gv @@ -0,0 +1,10 @@ +digraph Memory { + rankdir=RL; + node [shape=box]; + M [label="Incoming memory"]; + A [label="True: Store x"]; + B [label="False: Store y"]; + P [label="Phi(memory)"]; + P -> A -> M [color=blue]; P -> B -> M [color=blue]; + P -> Region [style=dashed]; Return -> P [color=blue]; +} diff --git a/docs/chapter10a/example2a.svg b/docs/chapter10a/example2a.svg new file mode 100644 index 00000000..f9a9b4fd --- /dev/null +++ b/docs/chapter10a/example2a.svg @@ -0,0 +1,85 @@ + + + + + + +Memory + + + +M + +Incoming memory + + + +A + +True: Store x + + + +A->M + + + + + +B + +False: Store y + + + +B->M + + + + + +P + +Phi(memory) + + + +P->A + + + + + +P->B + + + + + +Region + +Region + + + +P->Region + + + + + +Return + +Return + + + +Return->P + + + + + diff --git a/docs/chapter10a/example2b.gv b/docs/chapter10a/example2b.gv new file mode 100644 index 00000000..3f3309e5 --- /dev/null +++ b/docs/chapter10a/example2b.gv @@ -0,0 +1,11 @@ +digraph Memory { + rankdir=RL; + node [shape=box]; + P [label="Phi(memory)"]; + S [label="Loop-body Store"]; + 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/docs/chapter10a/example2b.svg b/docs/chapter10a/example2b.svg new file mode 100644 index 00000000..8fff33d4 --- /dev/null +++ b/docs/chapter10a/example2b.svg @@ -0,0 +1,74 @@ + + + + + + +Memory + + + +P + +Phi(memory) + + + +S + +Loop-body Store + + + +P->S + + + + + +Entry + +Entry + + + +P->Entry + + + + + +Loop + +Loop + + + +P->Loop + + + + + +S->P + + + + + +Return + +Return + + + +Return->P + + + + + + diff --git a/docs/chapter10a/example2c.gv b/docs/chapter10a/example2c.gv new file mode 100644 index 00000000..ef8a5fc8 --- /dev/null +++ b/docs/chapter10a/example2c.gv @@ -0,0 +1,9 @@ +digraph Memory { + rankdir=RL; + node [shape=box]; + M [label="Prior memory"]; + L [label="Load p.x"]; + S [label="Store p.x"]; + L -> M [color=blue]; S -> M [color=blue]; + S -> L [style=dashed,label="execute load first"]; +} diff --git a/docs/chapter10a/example2c.svg b/docs/chapter10a/example2c.svg new file mode 100644 index 00000000..c7b37912 --- /dev/null +++ b/docs/chapter10a/example2c.svg @@ -0,0 +1,50 @@ + + + + + + +Memory + + + +M + +Prior memory + + + +L + +Load p.x + + + +L->M + + + + + +S + +Store p.x + + + +S->M + + + + + +S->L + + +execute load first + + + diff --git a/docs/chapter10a/lattice.gv b/docs/chapter10a/lattice.gv new file mode 100644 index 00000000..733a5287 --- /dev/null +++ b/docs/chapter10a/lattice.gv @@ -0,0 +1,108 @@ +digraph Lattice { + 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/docs/chapter10a/lattice.svg b/docs/chapter10a/lattice.svg new file mode 100644 index 00000000..24c0de8c --- /dev/null +++ b/docs/chapter10a/lattice.svg @@ -0,0 +1,570 @@ + + + + + + +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 + + + +TOP->XCTRL + + + + + +INT_TOP + +⊤:int + + + +TOP->INT_TOP + + + + + +PTR_TOP + +⊤:ptr +[*⊤:struct] + + + +TOP->PTR_TOP + + + + + +STRUCT_TOP + +⊤:struct +[struct top] + + + +TOP->STRUCT_TOP + + + + + +MEM_TOP + +⊤:mem + + + +TOP->MEM_TOP + + + + + +TUPLE_TOP + +⊤:tuple + + + +TOP->TUPLE_TOP + + + + + +BOT + +⊥ + + + +CTRL + +⊥:ctrl + + + +XCTRL->CTRL + + + + + + +CTRL->BOT + + + + + +INT_NEG + +… −2, −1 + + + +INT_TOP->INT_NEG + + + + + +INT_ZERO + +0 + + + +INT_TOP->INT_ZERO + + + + + +INT_POS + +1, 2, … + + + +INT_TOP->INT_POS + + + + + + +INT_BOT + +⊥:int + + + +INT_BOT->BOT + + + + + +INT_NEG->INT_BOT + + + + + + +INT_ZERO->INT_BOT + + + + + + +INT_POS->INT_BOT + + + + + +PTR_NULL + +null +[*⊤:struct?] + + + +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 + +s1 +x: int + + + +STRUCT_TOP->STRUCT_S1 + + + + + +STRUCT_S2 + +s2 +x: int, y: int + + + +STRUCT_TOP->STRUCT_S2 + + + + + +STRUCT_MORE + +… + + + +STRUCT_TOP->STRUCT_MORE + + + + + + +STRUCT_BOT + +⊥:struct +[struct bottom] + + + +STRUCT_BOT->BOT + + + + + +STRUCT_PERSON->STRUCT_BOT + + + + + + +STRUCT_S1->STRUCT_BOT + + + + + + +STRUCT_S2->STRUCT_BOT + + + + + + +STRUCT_MORE->STRUCT_BOT + + + + + +MEM_BOT + +⊥:mem + + + +MEM_TOP->MEM_BOT + + + + + + +MEM_BOT->BOT + + + + + +TUPLE1 + +(type) + + + +TUPLE_TOP->TUPLE1 + + + + + +TUPLE2 + +(type, type) + + + +TUPLE_TOP->TUPLE2 + + + + + +TUPLEN + +(type, …) + + + +TUPLE_TOP->TUPLEN + + + + + +TUPLE_BOT + +⊥:tuple + + + +TUPLE_BOT->BOT + + + + + +TUPLE1->TUPLE_BOT + + + + + + +TUPLE2->TUPLE_BOT + + + + + + +TUPLEN->TUPLE_BOT + + + + + diff --git a/docs/chapter10a/type-control.svg b/docs/chapter10a/type-control.svg new file mode 100644 index 00000000..d4b79c53 --- /dev/null +++ b/docs/chapter10a/type-control.svg @@ -0,0 +1,5 @@ + + Control + + Control + diff --git a/docs/chapter10a/type-integer.svg b/docs/chapter10a/type-integer.svg new file mode 100644 index 00000000..97d03372 --- /dev/null +++ b/docs/chapter10a/type-integer.svg @@ -0,0 +1,5 @@ + + Integer + + Integer + diff --git a/docs/chapter10a/type-memory.svg b/docs/chapter10a/type-memory.svg new file mode 100644 index 00000000..16b5121f --- /dev/null +++ b/docs/chapter10a/type-memory.svg @@ -0,0 +1,5 @@ + + Memory + + Memory + diff --git a/docs/chapter10a/type-pointer.svg b/docs/chapter10a/type-pointer.svg new file mode 100644 index 00000000..7604492e --- /dev/null +++ b/docs/chapter10a/type-pointer.svg @@ -0,0 +1,5 @@ + + Pointer + + Pointer + diff --git a/docs/chapter10a/type-struct.svg b/docs/chapter10a/type-struct.svg new file mode 100644 index 00000000..97a16562 --- /dev/null +++ b/docs/chapter10a/type-struct.svg @@ -0,0 +1,5 @@ + + Struct + + Struct + diff --git a/docs/chapter10a/type-tuple.svg b/docs/chapter10a/type-tuple.svg new file mode 100644 index 00000000..691478ac --- /dev/null +++ b/docs/chapter10a/type-tuple.svg @@ -0,0 +1,5 @@ + + Tuple + + Tuple + -- cgit v1.2.3