From f05ad3837117b3b8cb830981aae619c583d7e694 Mon Sep 17 00:00:00 2001 From: Cliff Click Date: Tue, 29 Sep 2026 12:34:58 -0700 Subject: Chapter 10b: Splitting Memory --- docs/chapter10b/10-grammar.md | 125 +++++++++ docs/chapter10b/Makefile | 14 + docs/chapter10b/README.md | 190 +++++++++++++ docs/chapter10b/example1.gv | 13 + docs/chapter10b/example1.svg | 93 +++++++ docs/chapter10b/example2a.gv | 10 + docs/chapter10b/example2a.svg | 82 ++++++ docs/chapter10b/example2b.gv | 10 + docs/chapter10b/example2b.svg | 101 +++++++ docs/chapter10b/example2c.gv | 10 + docs/chapter10b/example2c.svg | 56 ++++ docs/chapter10b/lattice.gv | 114 ++++++++ docs/chapter10b/lattice.svg | 620 ++++++++++++++++++++++++++++++++++++++++++ 13 files changed, 1438 insertions(+) create mode 100644 docs/chapter10b/10-grammar.md create mode 100644 docs/chapter10b/Makefile create mode 100644 docs/chapter10b/README.md create mode 100644 docs/chapter10b/example1.gv create mode 100644 docs/chapter10b/example1.svg create mode 100644 docs/chapter10b/example2a.gv create mode 100644 docs/chapter10b/example2a.svg create mode 100644 docs/chapter10b/example2b.gv create mode 100644 docs/chapter10b/example2b.svg create mode 100644 docs/chapter10b/example2c.gv create mode 100644 docs/chapter10b/example2c.svg create mode 100644 docs/chapter10b/lattice.gv create mode 100644 docs/chapter10b/lattice.svg (limited to 'docs') diff --git a/docs/chapter10b/10-grammar.md b/docs/chapter10b/10-grammar.md new file mode 100644 index 00000000..9a80d6ea --- /dev/null +++ b/docs/chapter10b/10-grammar.md @@ -0,0 +1,125 @@ +# Grammar for Chapter 10b + +```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/chapter10b/Makefile b/docs/chapter10b/Makefile new file mode 100644 index 00000000..055882b2 --- /dev/null +++ b/docs/chapter10b/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/chapter10b/README.md b/docs/chapter10b/README.md new file mode 100644 index 00000000..69f13335 --- /dev/null +++ b/docs/chapter10b/README.md @@ -0,0 +1,190 @@ +# Chapter 10b: Splitting Memory + +[Previous: Chapter 10a](../chapter10a/README.md) | +[Next: Chapter 11](../chapter11/README.md) + +Chapter 10a made memory effects explicit with one SSA memory value. This +chapter keeps exactly that parser model and recovers independent memory chains +through graph rewrites. There is no new language syntax; the +[grammar](10-grammar.md), pointer types, and null checks are unchanged. + +## Why split memory? + +```java +struct Point { int x; int y; } +Point p = new Point; +p.x = 42; +while (arg > 0) { + p.y = p.y + arg; + arg = arg - 1; +} +return p.x; +``` + +The loop changes `y`, so it cannot affect `x`. With one memory chain the load +of `x` follows the loop's stores. Splitting the fields lets ordinary +load-after-store forwarding turn the return value into 42. + +![Independent field dependencies](example1.svg) + +These are schematic dependency graphs, with arrows from uses to their definitions. +In horizontal diagrams, definitions appear on the left and uses on the right; +in vertical diagrams, definitions appear above uses. +Control, pointer, and value edges are omitted when they do not explain memory. + +## Equivalence-class aliasing + +Each struct field has an integer alias identity. Two different fields receive +different identities, even if they have the same spelling in different structs. +Two instances of the same struct share their field aliases. Thus different +classes never alias; accesses in the same class **may alias**. Same-class does +not mean same-address: forwarding still checks pointer identity. + +The parser assigns field identities at struct declarations, beginning at 2. +These identities are independent of Start's output indices. The default slot +of a memory aggregate is 1; precise slots are greater than 1. + +We do not allocate a Start projection, scope binding, or loop Phi for every +declared field. Start supplies one memory value, Scope holds one `$mem` binding, +and Return consumes one complete memory value. The optimizer introduces slices +only where graph operations require them. + +## Three memory nodes + +| Node | Meaning | +|---|---| +| `MemMerge` | A complete memory state: a default plus precise alias overrides | +| `MemPhi` | One alias selected according to the incoming control path | +| `BulkMemPhi` | All aliases except an explicit exclusion set, selected by control | + +`MemMerge` combines independent pieces of memory at one program point. It is +not a control-flow merge. For example, after storing to alias `x`: + +```text +prior = current memory +store = Store_x(prior, pointer, value) +current memory = MemMerge(default=prior, x=store) +``` + +The Store selects its precise input from any incoming MemMerge. Loads and +precise memory Phis do the same. A missing precise entry falls back to the +default, provided that default still covers the requested alias. + +The explicit entries override the default: the semantic slices are disjoint, +and their union covers all memory. Flattening stacked aggregates preserves +entries that the outer aggregate has not replaced. This allows an `x` store +and a later `y` store to remain visible together at Return. + +![An aggregate preserves both updates](example2a.svg) + +## Splitting a memory Phi + +Scope initially creates a BulkMemPhi wherever the ordinary SSA algorithm needs +to merge memory. Its empty exclusion set means that it covers every alias. +After the Region is complete, the Phi inspects its memory inputs and users. +When they require a precise alias, it splits out that alias: + +```text +BulkPhi(R, left, right) + becomes +MemMerge( + default = BulkPhi_except{x}(R, left, right), + x = MemPhi_x(R, slice(left,x), slice(right,x))) +``` + +The new precise Phi and the remaining bulk Phi share a Region and matching +control-path indices. A loop uses the same transformation, with the backedge +among those inputs. Each further split preserves all previously extracted +slices; replacing a bulk Phi must never drop their parallel precise Phis. + +![Precise and bulk Phis share a control merge](example2b.svg) + +A bulk Phi can bypass an incoming aggregate only when all of that aggregate's +explicit slices are already excluded from the Phi. A precise consumer can +select one entry. A whole-memory consumer cannot just select the default: +that would lose the explicit updates. + +## Types and the worklist + +The type lattice retains Chapter 10a's six domains, colors, and notation: +`⊤` means top, `⊥` means bottom, and a suffix names the domain. The other five +domains are unchanged; memory now adds a flat element `MEM#N` for each precise +alias between memory top (`TypeMem.TOP`) and memory bottom (`TypeMem.BOT`). + +![The type domains, including precise memory aliases](lattice.svg) + +The parallel `MEM#2`, `MEM#3`, and further alias elements describe independent +field slices. For the first `Point` declaration above, these two aliases identify +`Point.x` and `Point.y`. Meeting different aliases gives memory bottom; joining +them gives memory top. Each precise alias is its own dual. The ellipsis stands +for more parallel aliases, not a type representing a set of aliases. + +Memory bottom covers all memory. The default aggregate slot numbered 1 is a +graph input position, not a precise field alias in this diagram. Types do not +track field values, private objects, or escape information. Bulk exclusion sets +and the default-plus-overrides structure of MemMerge belong to graph nodes, +not to an expanded type lattice. As in Chapter 10a, diagram edges show lattice +order, with top above bottom; field and tuple-element type lattices are elided. + +Scalar Phis remain ordinary PhiNodes. The scope's Phi factory chooses a +BulkMemPhi for whole memory; splitting constructs MemPhis explicitly. Generic +arithmetic factoring through Phis must not factor a memory aggregate. + +Memory splitting can increase node count. Progress comes from extracting an +alias from a bulk Phi and simplifying its precise chain, rather than from +requiring every rewrite to shrink the graph. Nodes must have conservative +initial types before introducing cyclic inputs. New bulk and precise Phis are +queued, so a recursive peephole cannot start another split halfway through the +first one. + +This also extends the worklist lesson from Chapter 9. A bulk Phi inspects its +users, so changes to a user's partition must wake the producer. Selecting a +slice from an aggregate can expose a new bulk-Phi user; that selected definition +must be queued too. The optimizer's worklist completeness assertion remains +enabled and checks these dependencies. + +## Evaluation and ordering + +MemMerge is a dependency node; it emits no heap operation. Its evaluator result +is a memory token, while Store mutates the object's fields. The scheduler must +distinguish aggregation from overwriting memory. A MemMerge is not a clobber, +and stores in different alias classes do not impose load/store anti-dependencies. + +![Ordering applies within the affected alias](example2c.svg) + +Tests cover independent-field folding, parallel memory Phis, multiple field +updates surviving at Return, early returns, nested loops with break/continue, +and reads before subsequent stores through potentially aliased pointers. + +## What remains for later chapters? + +Chapter 10b knows every access's alias while parsing. What is lazy here is the +construction of memory partitions. Chapter 25 also allows an existing access's +alias to become known later, using the same representation. Its private +constructor memory, escape tracking, incomplete types, and module alias +remapping are separate extensions and are not needed here. + +Chapters 11-24 currently retain their older parser-managed memory chains. +Forwarding this representation through those snapshots is tracked in the +[backport queue](../chapter-backports.md). Chapter 11's scheduling lesson +therefore still shows the older graph construction, with the same language. + +## Build and test + +With JDK 21 or newer, from this directory: + +```sh +make lib +make tests +make release +make view +``` + +Make builds this complete snapshot without Maven. `make release` writes +`build/release/simple.jar`; `make view` launches the shared graph viewer. +Both the root Maven reactor and the supplied IDEA module descriptor include +the chapter. From the repository root, test both halves with: + +```sh +make tests CHAPTERS="chapter10a chapter10b" +``` diff --git a/docs/chapter10b/example1.gv b/docs/chapter10b/example1.gv new file mode 100644 index 00000000..0b0a5feb --- /dev/null +++ b/docs/chapter10b/example1.gv @@ -0,0 +1,13 @@ +digraph Memory { + rankdir=BT; + node [shape=box]; + M [label="Initial memory"]; + X [label="Store x = 42"]; + Y [label="Loop: Store y"]; + L [label="Load x (42)"]; + L -> X -> M [color=blue]; Y -> M [color=green]; + MemMerge -> X [color=blue]; MemMerge -> Y [color=green]; + Return -> MemMerge; Return -> L; + { rank=same; MemMerge -> L [style=invis]; } + Y -> X [style=invis]; // Layout only: keep the stores in code order. +} diff --git a/docs/chapter10b/example1.svg b/docs/chapter10b/example1.svg new file mode 100644 index 00000000..384b6e12 --- /dev/null +++ b/docs/chapter10b/example1.svg @@ -0,0 +1,93 @@ + + + + + + +Memory + + + +M + +Initial memory + + + +X + +Store x = 42 + + + +X->M + + + + + +Y + +Loop: Store y + + + +Y->M + + + + + + +L + +Load x (42) + + + +L->X + + + + + +MemMerge + +MemMerge + + + +MemMerge->X + + + + + +MemMerge->Y + + + + + + +Return + +Return + + + +Return->L + + + + + +Return->MemMerge + + + + + diff --git a/docs/chapter10b/example2a.gv b/docs/chapter10b/example2a.gv new file mode 100644 index 00000000..d92eea41 --- /dev/null +++ b/docs/chapter10b/example2a.gv @@ -0,0 +1,10 @@ +digraph Memory { + rankdir=RL; + node [shape=box]; + M [label="Default memory"]; + X [label="Store x"]; + Y [label="Store y"]; + X -> M [color=blue]; Y -> M [color=green]; + MemMerge -> M [label="default"]; MemMerge -> X [label="x",color=blue]; + MemMerge -> Y [label="y",color=green]; Return -> MemMerge; +} diff --git a/docs/chapter10b/example2a.svg b/docs/chapter10b/example2a.svg new file mode 100644 index 00000000..97fb144e --- /dev/null +++ b/docs/chapter10b/example2a.svg @@ -0,0 +1,82 @@ + + + + + + +Memory + + + +M + +Default memory + + + +X + +Store x + + + +X->M + + + + + +Y + +Store y + + + +Y->M + + + + + +MemMerge + +MemMerge + + + +MemMerge->M + + +default + + + +MemMerge->X + + +x + + + +MemMerge->Y + + +y + + + +Return + +Return + + + +Return->MemMerge + + + + + diff --git a/docs/chapter10b/example2b.gv b/docs/chapter10b/example2b.gv new file mode 100644 index 00000000..4ddd36b5 --- /dev/null +++ b/docs/chapter10b/example2b.gv @@ -0,0 +1,10 @@ +digraph Memory { + rankdir=RL; + node [shape=box]; + P [label="MemPhi(x)"]; + B [label="BulkMemPhi(All except x)"]; + P -> Left [label="slice x",color=blue]; P -> Right [label="slice x",color=blue]; + B -> Left; B -> Right; + P -> Region [style=dashed]; B -> Region [style=dashed]; + MemMerge -> P [label="x",color=blue]; MemMerge -> B [label="default"]; +} diff --git a/docs/chapter10b/example2b.svg b/docs/chapter10b/example2b.svg new file mode 100644 index 00000000..4e0616f1 --- /dev/null +++ b/docs/chapter10b/example2b.svg @@ -0,0 +1,101 @@ + + + + + + +Memory + + + +P + +MemPhi(x) + + + +Left + +Left + + + +P->Left + + +slice x + + + +Right + +Right + + + +P->Right + + +slice x + + + +Region + +Region + + + +P->Region + + + + + +B + +BulkMemPhi(All except x) + + + +B->Left + + + + + +B->Right + + + + + +B->Region + + + + + +MemMerge + +MemMerge + + + +MemMerge->P + + +x + + + +MemMerge->B + + +default + + + diff --git a/docs/chapter10b/example2c.gv b/docs/chapter10b/example2c.gv new file mode 100644 index 00000000..4fae3bba --- /dev/null +++ b/docs/chapter10b/example2c.gv @@ -0,0 +1,10 @@ +digraph Memory { + rankdir=RL; + node [shape=box]; + M [label="Prior x 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"]; + Y [label="Store p.y: independent"]; +} diff --git a/docs/chapter10b/example2c.svg b/docs/chapter10b/example2c.svg new file mode 100644 index 00000000..8249d677 --- /dev/null +++ b/docs/chapter10b/example2c.svg @@ -0,0 +1,56 @@ + + + + + + +Memory + + + +M + +Prior x memory + + + +L + +Load p.x + + + +L->M + + + + + +S + +Store p.x + + + +S->M + + + + + +S->L + + +execute load first + + + +Y + +Store p.y: independent + + + diff --git a/docs/chapter10b/lattice.gv b/docs/chapter10b/lattice.gv new file mode 100644 index 00000000..f9fb2b09 --- /dev/null +++ b/docs/chapter10b/lattice.gv @@ -0,0 +1,114 @@ +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\nprecise alias slices"; fontname="Arial"; color="#cccccc"; + node [fillcolor="#00008b", fontcolor=white]; + MEM_TOP [label="⊤:mem"]; + MEM_BOT [label="⊥:mem"]; + MEM_ALIAS2 [label="MEM#2"]; + MEM_ALIAS3 [label="MEM#3"]; + MEM_MORE [label="…"]; + {rank=same; MEM_ALIAS2; MEM_ALIAS3; MEM_MORE;} + MEM_ALIAS2 -> MEM_ALIAS3 -> MEM_MORE [style=invis]; + MEM_TOP -> {MEM_ALIAS2 MEM_ALIAS3 MEM_MORE}; + {MEM_ALIAS2 MEM_ALIAS3 MEM_MORE} -> 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/chapter10b/lattice.svg b/docs/chapter10b/lattice.svg new file mode 100644 index 00000000..a11452b9 --- /dev/null +++ b/docs/chapter10b/lattice.svg @@ -0,0 +1,620 @@ + + + + + + +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 +precise alias slices + + +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 + + + +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: *s1 + + + +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_ALIAS2 + +MEM#2 + + + +MEM_TOP->MEM_ALIAS2 + + + + + +MEM_ALIAS3 + +MEM#3 + + + +MEM_TOP->MEM_ALIAS3 + + + + + +MEM_MORE + +… + + + +MEM_TOP->MEM_MORE + + + + + + +MEM_BOT + +⊥:mem + + + +MEM_BOT->BOT + + + + + +MEM_ALIAS2->MEM_BOT + + + + + + +MEM_ALIAS3->MEM_BOT + + + + + + +MEM_MORE->MEM_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 + + + + + -- cgit v1.2.3