From e4dc3273f201ae741637b626998637cce973546b Mon Sep 17 00:00:00 2001 From: Cliff Click Date: Fri, 2 Oct 2026 13:04:34 -0700 Subject: First pass README updates --- chapter14/README.md | 75 ++- chapter14/docs/lattice.gv | 355 +++++------ chapter14/docs/lattice.svg | 1494 ++++++++++++++++++++++++-------------------- 3 files changed, 1000 insertions(+), 924 deletions(-) (limited to 'chapter14') diff --git a/chapter14/README.md b/chapter14/README.md index acd8a492..a68baa5c 100644 --- a/chapter14/README.md +++ b/chapter14/README.md @@ -1,5 +1,8 @@ # Chapter 14: Narrow types +[Previous: Chapter 13](../chapter13/README.md) | +[Next: Chapter 15](../chapter15/README.md) + Memory retains the single `$mem` binding and lazy partitions from Chapter 10b. Narrow-field stores perform this chapter's truncation before updating their alias in MemMerge. Start and Return keep control in slot 0 and memory in slot 1. @@ -7,9 +10,9 @@ alias in MemMerge. Start and Return keep control in slot 0 and memory in slot 1. # Table of Contents 1. [Narrow Word Types](#narrow-or-sub-word-types) -2. [OverFlow handling](#overflow-handling) +2. [Overflow handling](#overflow-handling) 3. [Integer ranges](#integer-ranges) -4. [Bitwise operations](#examples) +4. [Bitwise operations](#bitwise-operations) 5. [Precedence](#precedence) 6. [Type lattice](#type-implementation) 7. [Nodes](#nodes) @@ -21,7 +24,7 @@ You can also read [this chapter](https://github.com/SeaOfNodes/Simple/tree/linea ## Narrow or sub-word types -Narrow or sub-worded integer types refer to integer data types that occupy less memory (fewer bits) than the standard or "full-width"(Typically 32, or 64 bits) integer types provided by a system or programming language. +Narrow or sub-word integer types refer to integer data types that occupy less memory (fewer bits) than the standard or "full-width" (typically 32 or 64 bits) integer types provided by a system or programming language. As a prelude to arrays, especially arrays of bytes common in all networking @@ -32,34 +35,34 @@ extended on a load. ```java i8 x = 123456789; -if( x != 21 ) +if( x != 21 ) return false; return true; ``` -The variable `x` is limited to 8 bits signed. Assigning the vary large value +The variable `x` is limited to 8 bits signed. Assigning the very large value `123456789` (hex `0x75BCD15`) simply truncates to 8 bits yielding `21 (0x15)`. The value is sign-extended on a load. ```java i16 x = 123456789; -if( x != -13035 ) +if( x != -13035 ) return false; return true; ``` -The variable `x` is limited to 16 bits signed. Assigning the vary large value +The variable `x` is limited to 16 bits signed. Assigning the very large value `0x75BCD15` simply truncates to 16 bits yielding `0xCD15`. The value is sign-extended on a load yielding `-13035 (0xFFFF FFFF FFFF CD15)`. ```java u16 x = 123456789; -if( x != 52501 ) +if( x != 52501 ) return false; return true; ``` -The variable `x` is limited to 16 bits unsigned. Assigning the vary large value +The variable `x` is limited to 16 bits unsigned. Assigning the very large value `0x75BCD15` simply truncates to 16 bits yielding `0xCD15`. The value is zero-extended on a load yielding `52501 (0x0000 0000 0000 CD15)`. @@ -91,10 +94,10 @@ There are several cases of overflow: #### Unsigned(fixed-width) integer overflow: -```java -u8 a = 255; +```java +u8 a = 255; u8 b = a + 1; // match u8 type against expr.type -// a = 256 +// a = 256 // u8 = [0...255] return b; ``` @@ -113,7 +116,7 @@ The operands to the "bitwise AND" are the values(256) and the mask(255, max boun This is called truncating. `ZsMask:` -```java +```java // zero/sign extend. "i" is limited to either classic unsigned (min==0) or // classic signed (min=minus-power-of-2); max=power-of-2-minus-1. private Node zsMask(Node val, Type t ) { @@ -140,29 +143,29 @@ The truncation is done by the `AndNode`: if( t0._min==0 ) // Unsigned return new AndNode(val,con(t0._max)).peephole(); ``` -Since they are constants, after calling peephole it truns into`256 & 255` = 0; +Since they are constants, after calling peephole it turns into `256 & 255` = 0; Output: ``` -return 0; +return 0; ``` #### Maximum integer overflow -```java -i64 a = 9223372036854775807; +```java +i64 a = 9223372036854775807; i64 b = a + 1; return b; ``` When we are computing the addition, we make sure they don't overflow: `AddNode.overflow:` -```java +```java private static boolean overflow( long x, long y ) { if( (x ^ y ) < 0 ) return false; // unequal signs, never overflow return (x ^ (x + y)) < 0; // sum has unequal signs, so overflow } ``` `AddNode.compute` -```java +```java ... // Fold ranges like {0-1} + {2-3} into {2-4}. if( !overflow(i1._min,i2._min) && @@ -183,8 +186,8 @@ return TypeInteger.constant(i1.value()+i2.value()); // -9223372036854775808; ``` #### Adding constant ranges -```java -u8 a = 12; +```java +u8 a = 12; u8 b = 13; u8 c = 124; u8 d = a + b + c; @@ -197,30 +200,30 @@ public static TypeInteger make(boolean is_con, long con) { return make(is_con ? con : (con==0 ? Long.MAX_VALUE : Long.MIN_VALUE), is_con ? con : (con==0 ? Long.MIN_VALUE : Long.MAX_VALUE)); ``` -- This results in: +- This results in: ```java return make(con, con); ``` -`value()` is only called in constants, e.g `_min == _max;` invariants holds, then since +`value()` is only called in constants, e.g `_min == _max;` invariant holds, then since both `min_` and `max_` are equal, we can return either one. This is the same as regular additions: -```java -public long value() { assert isConstant(); return _min; } +```java +public long value() { assert isConstant(); return _min; } ``` #### Truncate(2) -```java +```java u8 a = arg; // arg & 255 u8 b = arg; // arg & 255(same as a) u8 c = a + b; // (arg&255)*2, type = TypeInteger.BOT -return c; // (((arg&255)*2)&255), type = TypeInteger.U8 +return c; // (((arg&255)*2)&255), type = TypeInteger.U8 ``` Same as before, **arg** turns into **(arg&255)**, this node is then inserted into the **GVN** table and **b** retrieves this value. -The AddNode peephole will change them into `((arg&255)*2`, and put on extra mask +The AddNode peephole will change them into `((arg&255)*2)`, and put on extra mask on the expression to keep it in the valid boundaries. @@ -238,15 +241,15 @@ And `&`, Or `|`, Xor `^`, Shift left `<<`, Shift right `>>`, Shift right zero `> | **Or** | `\|` | Performs a bitwise OR (inclusive OR) operation. | | **Xor** | `^` | Performs a bitwise XOR (exclusive OR) operation. | | **Shift Left** | `<<` | Shifts bits to the left, filling with zeros. | -| **Shift Right** | `>>` | Shifts bits to the right, any vacated bit postions are filled by replicating the value of the sign bit. | -| **Unsigned Right Shift** | `>>>` | Shifts bits to the right, any vacated bit postions are always filled with zero | +| **Shift Right** | `>>` | Shifts bits to the right, any vacated bit positions are filled by replicating the value of the sign bit. | +| **Unsigned Right Shift** | `>>>` | Shifts bits to the right, any vacated bit positions are always filled with zero | Note `>>>` is a logical shift and not an arithmetic shift. #### AndNode: ##### lhs & -1 = lhs; -```java +```java // And of -1. We do not check for (-1&x) because this will already // canonicalize to (x&-1) if( t2.isConstant() && t2 instanceof TypeInteger i && i.value()==-1 ) @@ -306,7 +309,7 @@ arg + 123 & 3 = (arg + 123) & 3 ## Type Implementation -The TypeInteger type class is +The ![Integer](../chapter10a/docs/type-integer.svg) `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 to the programmer but the optimizer internally supports all ranges. The MEET operation takes the min-of-mins and @@ -322,7 +325,11 @@ Example: the `i8` type has 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. +The ![Float](../docs/type-float.svg) `TypeFloat` class is also reworked to support 32-bit and 64-bit sizes. + +The integer range diagram is schematic: it shows the boolean range and its +dual as examples among the possible ranges. The other domains retain the +named structs, nullable pointers, and precise memory aliases from earlier chapters. ![Graph1](./docs/lattice.svg) @@ -350,4 +357,4 @@ slightly different `idealize()` calls. [^1]: Hacker's delight. - 4-2 Propagating Bounds through Add's and Subtract's + 4-2 Propagating Bounds through Adds and Subtracts diff --git a/chapter14/docs/lattice.gv b/chapter14/docs/lattice.gv index f16a9768..ac2f1f2e 100644 --- a/chapter14/docs/lattice.gv +++ b/chapter14/docs/lattice.gv @@ -1,202 +1,159 @@ 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]; - - // ---------------------- - // Floats - 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; + 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; } - {rank=same; INT_BOT; FLT_BOT; CTRL; PTR0; STRUCT_BOT; MEM_BOT; TUPLE_BOT} - {rank=same; BOT;} + + subgraph cluster_integer { + label="Integer ranges (schematic)"; fontname="Arial"; color="#cccccc"; + 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]; + + 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_CON0 -> INT_CON1 -> INT_CON [style=invis]; + + {rank=same; INT_CON0; INT_CON1; INT_CON;} + } + + subgraph cluster_float { + label="Float"; fontname="Arial"; color="#cccccc"; + 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]; + + 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_CON0 -> FLT_CON32 -> FLT_CONPI -> FLT_CON64 [style=invis]; + + + {rank=same; FLT_CON0; FLT_CON32; FLT_CONPI; FLT_CON64;} + } + + 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 FLT_TOP PTR_TOP STRUCT_TOP MEM_TOP TUPLE_TOP}; + {CTRL INT_BOT FLT_BOT PTR_BOT STRUCT_BOT MEM_BOT TUPLE_BOT} -> BOT; + {rank=same; XCTRL; INT_TOP; FLT_TOP; PTR_TOP; STRUCT_TOP; MEM_TOP; TUPLE_TOP;} + {rank=same; CTRL; INT_BOT; FLT_BOT; PTR_BOT; STRUCT_BOT; MEM_BOT; TUPLE_BOT;} + XCTRL -> INT_TOP -> FLT_TOP -> PTR_TOP -> STRUCT_TOP -> MEM_TOP -> TUPLE_TOP [style=invis]; } diff --git a/chapter14/docs/lattice.svg b/chapter14/docs/lattice.svg index 99f74ed0..131b5601 100644 --- a/chapter14/docs/lattice.svg +++ b/chapter14/docs/lattice.svg @@ -1,691 +1,803 @@ - - - - - - -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 - - - - - + + + + + + +Lattice + + +cluster_control + +Control + + +cluster_integer + +Integer ranges (schematic) + + +cluster_float + +Float + + +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 + + + + + +FLT_TOP + +⊤ +:flt + + + +TOP->FLT_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_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 + + + + + +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