From 65454d77eba95d7f814336377f78d9f42c7455f9 Mon Sep 17 00:00:00 2001 From: Cliff Click Date: Wed, 27 Nov 2024 11:29:33 -0800 Subject: More lattice docs reworks --- chapter10/README.md | 63 +++-- chapter10/docs/lattice.gv | 46 ++-- chapter10/docs/lattice.svg | 602 +++++++++++++++++++++------------------------ 3 files changed, 342 insertions(+), 369 deletions(-) (limited to 'chapter10') diff --git a/chapter10/README.md b/chapter10/README.md index c27c4b74..957be607 100644 --- a/chapter10/README.md +++ b/chapter10/README.md @@ -118,6 +118,7 @@ Additionally, the following Node types will be enhanced: | Start | Control | Start will produce the initial Memory projections, one per slice | | Return | Control | Will merge all memory slices | + ## Enhanced Type Lattice The Type Lattice for Simple has a major revision in this chapter. @@ -126,22 +127,38 @@ The Type Lattice for Simple has a major revision in this chapter. Within the Type Lattice, we now have the following type domains: -* Control type - this represents control flow -* Integer type - Integer values -* Tuple type - when a Node results in more than one value -* Struct type (new) - Represents user defined struct types, a struct type is allowed to have members of Integer type only in this chapter - * `$TOP` represents local Top for struct type; all we know about the type is that it is a struct but, we do not know if it is a specific struct, or all possible structs, etc. - * `$BOT` represents local Bottom for struct type; we definitely know the value can take all possible struct types. -* Pointer type (new) - Represents a pointer to a struct type - * `null` is a pointer to non-existent memory object - * We use the prefix `*` to mean pointer-to. Thus `*S1` means pointer to `S1`, `*$TOP` means pointer to `$TOP`. - * `*void` is a synonym for `*$BOT` - i.e. it represents a Non-Null pointer to all possible struct types, akin to `void *` in C except not null. +* Control type - represents control flow +* Integer type - Integer values, with a Top, Bottom and constants +* Pointer type (new) - Represents a pointer to a struct type + * We use the prefix `*` to mean pointer-to. Thus `*S1` means pointer to + `S1`, `*$TOP` means pointer to `$TOP`. * `?` suffix represents the union of a pointer to some type and `null`. - * `null` pointer evaluates to False and non-null pointers evaluate to True, as in C. -* Memory (new) - Represents memory and memory slices - * `MEM#TOP` - Nothing known about a slice - * `#n` - refers to a memory slice - * `MEM#BOT` - all of memory + * The pointer lattice has only 2 entries: null or not-null. In both cases a struct lattice element is + included, and can be any member of the struct lattice. + * `null` is a pointer to non-existent memory object, i.e. `*$TOP?`, and is a + nullable. Notice that the null part of the type is low in the lattice, + while the struct part is the highest struct. + * `*void` is a synonym for `*$BOT` - i.e. it represents a non-null pointer to + all possible struct types, akin to `void *` in C except not null. It is + the inverse or *dual* of `null`, and the null part is high in the pointer + lattice, while the struct part is the lowest struct. + * `null` pointer evaluates to False and non-null pointers evaluate to True, as in C. + +* Struct type (new) - + Represents user defined struct types, a struct type is allowed to have + members of Integer type only in this chapter, later chapters will expand + this. + * `⊤:struct` represents local Top for struct type; all we know about the type + is that it is a struct but, we do not know if it is a specific struct, or + all possible structs. In the code, we use a struct with no fields named `$TOP`. + * `⊥:struct` represents local Bottom for struct type; we definitely know the + value can take all possible struct types. In the code, we uise a struct + with no fields named `$BOT`. +* Memory type (new) - Represents memory and memory slices + * `⊤:mem` - Nothing known about a slice; in the code we use `MEM#TOP`. + * `#n` - refers to a memory slice, and `n` is the alias class. + * `⊥:mem` - all of memory; in the code we use `MEM#BOT`. +* Tuple type - when a Node results in a collection of values We make use of following operations on the lattice. @@ -150,20 +167,22 @@ We make use of following operations on the lattice. thought of as set union (ORing) of its input types (as sets). * Example, meet of `*S1` and `*S2` results in `*void` - there is no lattice element for exactly both `{*S1,*S2}`, so we drop down to the nearest - element containing both (and maybe more), which is `*void*`. - * Meet of `*S1` and struct `Null` results in `*S1?` - * Meet of `*void` and `Null` results in `*$BOT?`; bear in mind that `*void` is a synonym for `*$BOT`. + element containing both (and maybe more), which is `*void`. + * Meet of `*S1` and pointer `null` results in `*S1?` + * Meet of `*void` and `null` results in `*$BOT?`; bear in mind that `*void` is a synonym for `*$BOT`. * Meet of `1` and `2` results in `Int Bot`. * Meet of `#1` and `#2` results in `MEM#BOT`. * The `dual` operation is symmetric across the lattice centerline. Types directly on the centerline are their own dual. * Find the corresponding node of the lattice after inverting the lattice. * Thus, dual of `Top` is `Bot`. * The dual of `*$TOP` is `*$BOT?`. - * For structs, the dual is obtained by computing the dual of each struct member. Thus, dual of `*S1` is not `*S1?`. + * For structs, the dual is obtained by computing the dual of each struct + member. Thus, dual of `*S1` is not `*S1?`, it is some `*S1?` with dualed + fields. * The `join` operation takes two types and computes the least upper bound type. Similar to `meet` this can thought of as set intersection (ANDing) of its input types. - Because our lattice structure is simple, we compute `join` with a well known identity: + Because our lattice structure is symmetric and complete, we compute `join` with a well known identity: `JOIN(x,y) === MEET(x.dual,y.dual).dual` * Example, join of `*S1` and `*S2` results in `*$TOP`. * Join of `1` and `2` results in `Int Top`. @@ -195,8 +214,8 @@ lattice described in the previous section. ## Null Pointer Analysis The Simple language syntax allows a pointer variable to be specified as -Null-able - and it prevents ever throwing a Null Pointer Exception. The -compiler tries to decide in a null check is needed, and if needed and missing +null-able - and it prevents ever throwing a Null Pointer Exception. The +compiler decides if a null check is needed, and if needed and missing the compiler rejects the program (asking the user to insert a null check). When the Parser encounters conditions that test the truthiness of a pointer variable, it uses this knowledge to refine the type information in the branches that follow. diff --git a/chapter10/docs/lattice.gv b/chapter10/docs/lattice.gv index 5ac1bd5a..7723e2a2 100644 --- a/chapter10/docs/lattice.gv +++ b/chapter10/docs/lattice.gv @@ -5,12 +5,12 @@ digraph Lattice { node [shape=circle, style=filled]; nodesep=0.6; - TOP [label=<⊤ >, fillcolor=black, fontcolor=white]; + TOP [label=<⊤>, fillcolor=black, fontcolor=white]; BOT [label=<⊥>, fillcolor=black, fontcolor=white]; // ---------------------- // Control - XCTRL [label=<⊤ :ctrl>, fillcolor=yellow, shape=oval]; + XCTRL [label=<⊤:ctrl>, fillcolor=yellow, shape=oval]; CTRL [label=<⊥:ctrl>, fillcolor=yellow, shape=oval]; TOP -> XCTRL; @@ -19,29 +19,23 @@ digraph Lattice { // ---------------------- // Integers - INT_TOP [label=<⊤ :int>, fillcolor=lightblue, shape=oval]; + INT_TOP [label=<⊤:int>, fillcolor=lightblue, shape=oval]; INT_BOT [label=<⊥:int>, fillcolor=lightblue, shape=oval]; - INT_MIN [label="-n" , fillcolor=lightblue]; INT_MINDOTS [label="...", fillcolor=lightblue, shape=oval]; INT_ZERO [label="0" , fillcolor=lightblue]; INT_MAXDOTS [label="...", fillcolor=lightblue, shape=oval]; - INT_MAX [label="+n" , fillcolor=lightblue]; TOP -> INT_TOP; - INT_TOP -> INT_MIN; INT_TOP -> INT_MINDOTS; INT_TOP -> INT_ZERO; INT_TOP -> INT_MAXDOTS; - INT_TOP -> INT_MAX; - INT_MIN -> INT_BOT; INT_MINDOTS -> INT_BOT; INT_ZERO -> INT_BOT; INT_MAXDOTS -> INT_BOT; - INT_MAX -> INT_BOT; INT_BOT -> BOT; - INT_MIN -> INT_MINDOTS -> INT_ZERO -> INT_MAXDOTS -> INT_MAX [style=invis]; + INT_MINDOTS -> INT_ZERO -> INT_MAXDOTS [style=invis]; // ---------------------- // Pointers, just a boolean nil/not and a struct @@ -64,28 +58,28 @@ digraph Lattice { // ---------------------- // Structs - STRUCT_TOP [label=<⊤:struct>, fillcolor=lightgreen, shape=oval]; + STRUCT_TOP [label=<⊤:struct>, fillcolor=lightgreen, shape=oval]; + STRUCT_BOT [label=<⊥:struct>, fillcolor=lightgreen, shape=oval]; STRUCT_S1 [shape=none, fillcolor=none, label=< - +
fieldint:ptr
fieldint/ptr
>]; STRUCT_S2 [shape=none, fillcolor=none, label=< - - + +
fieldint:ptr
fieldint:ptr
fieldint/ptr
fieldint/ptr
>]; STRUCT_SN [shape=none, fillcolor=none, label=< - - - + + +
fieldint:ptr
... int:ptr
fieldint:ptr
fieldint/ptr
... int/ptr
fieldint/ptr
>]; - STRUCT_BOT [label=<⊥:struct>, fillcolor=lightgreen, shape=oval] TOP -> STRUCT_TOP; STRUCT_TOP -> STRUCT_S1; @@ -100,11 +94,11 @@ digraph Lattice { // ---------------------- // Memory - MEM_TOP [label=<⊤:mem>, fillcolor=blue, fontcolor=white, shape=oval]; + MEM_TOP [label=<⊤:mem>, fillcolor=blue, fontcolor=white, shape=oval]; + MEM_BOT [label=<⊥:mem>, fillcolor=blue, fontcolor=white, shape=oval]; MEM_ALIAS1 [label="#1" , fillcolor=blue, fontcolor=white]; MEM_ALIASDOTS [label="..." , fillcolor=blue, fontcolor=white, shape=oval]; MEM_ALIASN [label="#n" , fillcolor=blue, fontcolor=white]; - MEM_BOT [label=<⊥:mem>, fillcolor=blue, fontcolor=white, shape=oval]; TOP -> MEM_TOP; MEM_TOP -> MEM_ALIAS1; @@ -120,7 +114,8 @@ digraph Lattice { // ---------------------- // Tuples - TUPLE_TOP [label=<⊤:tuple>, fillcolor=pink, shape=oval]; + TUPLE_TOP [label=<⊤:tuple>, fillcolor=pink, shape=oval]; + TUPLE_BOT [label=<⊥:tuple>, fillcolor=pink, shape=oval]; TUPLE1 [shape=none, fillcolor=none, label=< @@ -144,7 +139,6 @@ digraph Lattice {
>]; - TUPLE_BOT [label=<⊥:tuple>, fillcolor=pink, shape=oval]; TOP -> TUPLE_TOP; TUPLE_TOP -> TUPLE1; @@ -159,11 +153,9 @@ digraph Lattice { // Additional customization {rank=same; TOP;} {rank=same; INT_TOP; XCTRL; STRUCT_TOP; MEM_TOP; TUPLE_TOP} - {rank=same; INT_MIN; INT_MINDOTS; - INT_ZERO; INT_MAXDOTS; - INT_MAX; STRUCT_S1; STRUCT_S2; STRUCT_SN; - MEM_ALIAS1; - MEM_ALIASDOTS; MEM_ALIASN;} + {rank=same; INT_MINDOTS; INT_ZERO; INT_MAXDOTS; + STRUCT_S1; STRUCT_S2; STRUCT_SN; + MEM_ALIAS1; MEM_ALIASDOTS; MEM_ALIASN;} {rank=same; INT_BOT; CTRL; STRUCT_BOT; MEM_BOT; TUPLE_BOT} {rank=same; BOT;} } diff --git a/chapter10/docs/lattice.svg b/chapter10/docs/lattice.svg index 02f3ce69..9eb36bbe 100644 --- a/chapter10/docs/lattice.svg +++ b/chapter10/docs/lattice.svg @@ -4,551 +4,513 @@ - - + + Lattice - + TOP - -⊤ + +⊤ XCTRL - -⊤ -:ctrl + +⊤ +:ctrl TOP->XCTRL - - + + INT_TOP - -⊤ -:int + +⊤ +:int TOP->INT_TOP - - + + - + PTR - - - -*ptr - - -struct + + + +*ptr + + +struct - + TOP->PTR - - + + - + STRUCT_TOP - -⊤ -:struct + +⊤ +:struct - + TOP->STRUCT_TOP - - + + - + MEM_TOP - -⊤ -:mem + +⊤ +:mem - + TOP->MEM_TOP - - + + - + TUPLE_TOP - -⊤ -:tuple + +⊤ +:tuple - + TOP->TUPLE_TOP - - + + BOT - -⊥ + +⊥ CTRL - -⊥ -:ctrl + +⊥ +:ctrl XCTRL->CTRL - - + + CTRL->BOT - - - - - -INT_MIN - --n - - - -INT_TOP->INT_MIN - - + + - + INT_MINDOTS - -... + +... - + INT_TOP->INT_MINDOTS - - + + - + INT_ZERO - -0 + +0 - + INT_TOP->INT_ZERO - - + + - + INT_MAXDOTS - -... + +... - + INT_TOP->INT_MAXDOTS - - - - - -INT_MAX - -+n - - - -INT_TOP->INT_MAX - - + + INT_BOT - -⊥ -:int + +⊥ +:int - + INT_BOT->BOT - - - - - -INT_MIN->INT_BOT - - + + - - + INT_MINDOTS->INT_BOT - - + + - + INT_ZERO->INT_BOT - - + + - + INT_MAXDOTS->INT_BOT - - - - - - -INT_MAX->INT_BOT - - + + - + PTR0 - - - -*ptr? - - -struct + + + +*ptr? + + +struct - + PTR->PTR0 - - + + - + PTR0->BOT - - + + - + STRUCT_S1 - - - -field + + + +field - + - - -int:ptr + + +int/ptr - + STRUCT_TOP->STRUCT_S1 - - + + - + STRUCT_S2 - - - -field + + + +field - + - - -int:ptr - - -field + + +int/ptr + + +field - + - - -int:ptr + + +int/ptr - + STRUCT_TOP->STRUCT_S2 - - + + - + STRUCT_SN - - - -field + + + +field - + - - -int:ptr - - -...   + + +int/ptr + + +...   - + - - -int:ptr - - -field + + +int/ptr + + +field - + - - -int:ptr + + +int/ptr - + STRUCT_TOP->STRUCT_SN - - + + - - + STRUCT_BOT - -⊥ -:struct + +⊥ +:struct + + + +STRUCT_BOT->BOT + + - + STRUCT_S1->STRUCT_BOT - - + + - + - + STRUCT_S2->STRUCT_BOT - - + + + - + STRUCT_SN->STRUCT_BOT - - - - - -STRUCT_BOT->BOT - - + + - + MEM_ALIAS1 - -#1 + +#1 - + MEM_TOP->MEM_ALIAS1 - - + + - + MEM_ALIASDOTS - -... + +... - + MEM_TOP->MEM_ALIASDOTS - - + + - + MEM_ALIASN - -#n + +#n - + MEM_TOP->MEM_ALIASN - - + + - - + MEM_BOT - -⊥ -:mem + +⊥ +:mem + + + +MEM_BOT->BOT + + - + MEM_ALIAS1->MEM_BOT - - + + - + - + MEM_ALIASDOTS->MEM_BOT - - + + + - + MEM_ALIASN->MEM_BOT - - - - - -MEM_BOT->BOT - - + + - + TUPLE1 - - - -Tuple - - -type + + + +Tuple + + +type - + TUPLE_TOP->TUPLE1 - - + + - + TUPLE2 - - - -Tuple - - -type - - -type + + + +Tuple + + +type + + +type - + TUPLE_TOP->TUPLE2 - - + + - + TUPLEN - - - -Tuple - - -type - - -... - - -type + + + +Tuple + + +type + + +... + + +type - + TUPLE_TOP->TUPLEN - - + + - + TUPLE_BOT - -⊥ -:tuple + +⊥ +:tuple + + + +TUPLE_BOT->BOT + + - + TUPLE1->TUPLE_BOT - - + + - + TUPLE2->TUPLE_BOT - - + + - + TUPLEN->TUPLE_BOT - - - - - -TUPLE_BOT->BOT - - + + -- cgit v1.2.3