From cf5be6998b26723ae29ab1edab84d32b0702182d Mon Sep 17 00:00:00 2001 From: Cliff Click Date: Wed, 13 Aug 2025 13:25:24 -0700 Subject: TypeAnalysis continued --- docs/lattice_i2.gv | 47 +++++ docs/lattice_i2.svg | 155 ++++++++++++++ docs/lattice_if.gv | 81 ++++---- docs/lattice_if.svg | 405 ++++++++++++++++++------------------ docs/lattice_iff.gv | 97 +++++++++ docs/lattice_iff.svg | 364 ++++++++++++++++++++++++++++++++ docs/lattice_iffc.gv | 106 ++++++++++ docs/lattice_iffc.svg | 396 +++++++++++++++++++++++++++++++++++ docs/lattice_iffcs.gv | 143 +++++++++++++ docs/lattice_iffcs.svg | 547 +++++++++++++++++++++++++++++++++++++++++++++++++ docs/lattice_iffct.gv | 145 +++++++++++++ docs/lattice_iffct.svg | 500 ++++++++++++++++++++++++++++++++++++++++++++ 12 files changed, 2754 insertions(+), 232 deletions(-) create mode 100644 docs/lattice_i2.gv create mode 100644 docs/lattice_i2.svg create mode 100644 docs/lattice_iff.gv create mode 100644 docs/lattice_iff.svg create mode 100644 docs/lattice_iffc.gv create mode 100644 docs/lattice_iffc.svg create mode 100644 docs/lattice_iffcs.gv create mode 100644 docs/lattice_iffcs.svg create mode 100644 docs/lattice_iffct.gv create mode 100644 docs/lattice_iffct.svg (limited to 'docs') diff --git a/docs/lattice_i2.gv b/docs/lattice_i2.gv new file mode 100644 index 00000000..f7eed48c --- /dev/null +++ b/docs/lattice_i2.gv @@ -0,0 +1,47 @@ +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]; + + // ---------------------- + // 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]; + + + // Additional customization + {rank=same; TOP} + {rank=same; INT_TOP; } + {rank=same; INT_CON; INT_CON0; INT_CON1; + } + {rank=same; INT_BOT; } + {rank=same; BOT;} +} diff --git a/docs/lattice_i2.svg b/docs/lattice_i2.svg new file mode 100644 index 00000000..ab10c485 --- /dev/null +++ b/docs/lattice_i2.svg @@ -0,0 +1,155 @@ + + + + + + +Lattice + + + +TOP + +⊤ + + + +INT_TOP + +⊤ +:int + + + +TOP->INT_TOP + + + + + +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 + + + + + diff --git a/docs/lattice_if.gv b/docs/lattice_if.gv index feb53dfe..445afd62 100644 --- a/docs/lattice_if.gv +++ b/docs/lattice_if.gv @@ -13,58 +13,63 @@ digraph Lattice { 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_MINUS [label="-1" , fillcolor=lightblue]; - INT_ZERO [label="0" , fillcolor=lightblue]; - INT_PLUS [label="1" , fillcolor=lightblue]; - INT_MAXDOTS [label="...", fillcolor=lightblue, shape=oval]; - INT_MAX [label="+n" , fillcolor=lightblue]; + 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_MIN; - INT_TOP -> INT_MINDOTS; - INT_TOP -> INT_MINUS; - INT_TOP -> INT_ZERO; - INT_TOP -> INT_PLUS; - INT_TOP -> INT_MAXDOTS; - INT_TOP -> INT_MAX; - INT_MIN -> INT_BOT; - INT_MINDOTS -> INT_BOT; - INT_MINUS -> INT_BOT; - INT_ZERO -> INT_BOT; - INT_PLUS -> INT_BOT; - INT_MAXDOTS -> INT_BOT; - INT_MAX -> INT_BOT; - INT_BOT -> BOT; + 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_MIN -> INT_MINDOTS -> INT_MINUS -> INT_ZERO -> INT_PLUS -> INT_MAXDOTS -> INT_MAX [style=invis]; + 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_MINDOTS [label="...", fillcolor=aqua, shape=oval]; - FLT_ZERO [label="0" , fillcolor=aqua]; - FLT_MAXDOTS [label="...", 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_MINDOTS; - FLT_TOP -> FLT_ZERO; - FLT_TOP -> FLT_MAXDOTS; - FLT_MINDOTS -> FLT_BOT; - FLT_ZERO -> FLT_BOT; - FLT_MAXDOTS -> FLT_BOT; - FLT_BOT -> BOT; + 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_MINDOTS -> FLT_ZERO -> FLT_MAXDOTS [style=invis]; + FLT_CON0 -> FLT_CON32 -> FLT_CONPI -> FLT_CON64 [style=invis]; // Additional customization {rank=same; TOP} {rank=same; INT_TOP; FLT_TOP; } - {rank=same; INT_MIN; INT_MINDOTS; INT_MINUS; INT_ZERO; INT_PLUS; INT_MAXDOTS; INT_MAX; - FLT_MINDOTS; FLT_ZERO; FLT_MAXDOTS; + {rank=same; INT_CON; INT_CON0; INT_CON1; + FLT_CON32; FLT_CON64; FLT_CON0; FLT_CONPI; } {rank=same; INT_BOT; FLT_BOT; } {rank=same; BOT;} diff --git a/docs/lattice_if.svg b/docs/lattice_if.svg index 1f6af94a..7e2e8fc1 100644 --- a/docs/lattice_if.svg +++ b/docs/lattice_if.svg @@ -4,262 +4,279 @@ - - + + Lattice - + TOP - -⊤ + +⊤ INT_TOP - -⊤ -:int + +⊤ +:int TOP->INT_TOP - - + + FLT_TOP - -⊤ -:flt + +⊤ +:flt - + TOP->FLT_TOP - - + + BOT - -⊥ + +⊥ - + -INT_MIN - --n +INT_HI + +max < min - + -INT_TOP->INT_MIN - - +INT_TOP->INT_HI + + - + + +INT_BOT + +⊥ +:int + + + +INT_BOT->BOT + + + + -INT_MINDOTS - -... +INT_XBOOL + +1...0 - + -INT_TOP->INT_MINDOTS - - +INT_HI->INT_XBOOL + + - + -INT_MINUS - --1 +INT_CON + +constants... - - -INT_TOP->INT_MINUS - - + + +INT_HI->INT_CON + + - + -INT_ZERO - -0 +INT_CON0 + +0 - - -INT_TOP->INT_ZERO - - + + +INT_XBOOL->INT_CON0 + + - + -INT_PLUS - -1 +INT_CON1 + +1 - - -INT_TOP->INT_PLUS - - + + +INT_XBOOL->INT_CON1 + + + + + +INT_LO + +max > min + + + +INT_CON->INT_LO + + - + + -INT_MAXDOTS - -... +INT_BOOL + +0...1 - + -INT_TOP->INT_MAXDOTS - - +INT_CON0->INT_BOOL + + - - -INT_MAX - -+n - - + + -INT_TOP->INT_MAX - - - - - -INT_BOT - -⊥ -:int +INT_CON1->INT_BOOL + + - - -INT_BOT->BOT - - - - + -INT_MIN->INT_BOT - - +INT_BOOL->INT_LO + + - - - -INT_MINDOTS->INT_BOT - - - - - + -INT_MINUS->INT_BOT - - +INT_LO->INT_BOT + + - - - -INT_ZERO->INT_BOT - - - - - - -INT_PLUS->INT_BOT - - - - - - -INT_MAXDOTS->INT_BOT - - - - - - -INT_MAX->INT_BOT - - - - + -FLT_MINDOTS - -... - - - -FLT_TOP->FLT_MINDOTS - - - - - -FLT_ZERO - -0 +FLT_CON64 + +64b consts +[excludes +32b consts] - - -FLT_TOP->FLT_ZERO - - + + +FLT_TOP->FLT_CON64 + + - + -FLT_MAXDOTS - -... - - - -FLT_TOP->FLT_MAXDOTS - - +FLT_CONPI + +3.14159... + + + +FLT_TOP->FLT_CONPI + + + + + +FLT_X32 + +~f32 + + + +FLT_TOP->FLT_X32 + + FLT_BOT - -⊥ -:flt + +⊥ +:flt - + FLT_BOT->BOT - - - - - -FLT_MINDOTS->FLT_BOT - - - - - - -FLT_ZERO->FLT_BOT - - - - - - -FLT_MAXDOTS->FLT_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 + + diff --git a/docs/lattice_iff.gv b/docs/lattice_iff.gv new file mode 100644 index 00000000..61e857b1 --- /dev/null +++ b/docs/lattice_iff.gv @@ -0,0 +1,97 @@ +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]; + + // ---------------------- + // 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]; + + // ---------------------- + // sub-Floats + FL8_TOP [label=<⊤:FP8>, fillcolor=aqua, shape=oval]; + FL8_BOT [label=<⊥:FP8>, fillcolor=aqua, shape=oval]; + + FL8_MINDOTS [label="...", fillcolor=aqua, shape=oval]; + FL8_ZERO [label="0" , fillcolor=aqua]; + FL8_MAXDOTS [label="...", fillcolor=aqua, shape=oval]; + + TOP -> FL8_TOP; + FL8_TOP -> FL8_MINDOTS; + FL8_TOP -> FL8_ZERO; + FL8_TOP -> FL8_MAXDOTS; + FL8_MINDOTS -> FL8_BOT; + FL8_ZERO -> FL8_BOT; + FL8_MAXDOTS -> FL8_BOT; + FL8_BOT -> BOT; + + FL8_MINDOTS -> FL8_ZERO -> FL8_MAXDOTS [style=invis]; + + // Additional customization + {rank=same; TOP} + {rank=same; INT_TOP; FLT_TOP; FL8_TOP; } + {rank=same; INT_CON; INT_CON0; INT_CON1; + FLT_CON32; FLT_CON64; FLT_CON0; FLT_CONPI; + FL8_MINDOTS; FL8_ZERO; FL8_MAXDOTS; + } + {rank=same; INT_BOT; FLT_BOT; FL8_BOT; } + {rank=same; BOT;} +} diff --git a/docs/lattice_iff.svg b/docs/lattice_iff.svg new file mode 100644 index 00000000..dbe60f0d --- /dev/null +++ b/docs/lattice_iff.svg @@ -0,0 +1,364 @@ + + + + + + +Lattice + + + +TOP + +⊤ + + + +INT_TOP + +⊤ +:int + + + +TOP->INT_TOP + + + + + +FLT_TOP + +⊤ +:flt + + + +TOP->FLT_TOP + + + + + +FL8_TOP + +⊤ +:FP8 + + + +TOP->FL8_TOP + + + + + +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 + + + + + +FL8_MINDOTS + +... + + + +FL8_TOP->FL8_MINDOTS + + + + + +FL8_ZERO + +0 + + + +FL8_TOP->FL8_ZERO + + + + + +FL8_MAXDOTS + +... + + + +FL8_TOP->FL8_MAXDOTS + + + + + +FL8_BOT + +⊥ +:FP8 + + + +FL8_BOT->BOT + + + + + +FL8_MINDOTS->FL8_BOT + + + + + + +FL8_ZERO->FL8_BOT + + + + + + +FL8_MAXDOTS->FL8_BOT + + + + + diff --git a/docs/lattice_iffc.gv b/docs/lattice_iffc.gv new file mode 100644 index 00000000..483d2026 --- /dev/null +++ b/docs/lattice_iffc.gv @@ -0,0 +1,106 @@ +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]; + + // ---------------------- + // sub-Floats + FL8_TOP [label=<⊤:FP8>, fillcolor=aqua, shape=oval]; + FL8_BOT [label=<⊥:FP8>, fillcolor=aqua, shape=oval]; + + FL8_MINDOTS [label="...", fillcolor=aqua, shape=oval]; + FL8_ZERO [label="0" , fillcolor=aqua]; + FL8_MAXDOTS [label="...", fillcolor=aqua, shape=oval]; + + TOP -> FL8_TOP; + FL8_TOP -> FL8_MINDOTS; + FL8_TOP -> FL8_ZERO; + FL8_TOP -> FL8_MAXDOTS; + FL8_MINDOTS -> FL8_BOT; + FL8_ZERO -> FL8_BOT; + FL8_MAXDOTS -> FL8_BOT; + FL8_BOT -> BOT; + + FL8_MINDOTS -> FL8_ZERO -> FL8_MAXDOTS [style=invis]; + + // Additional customization + {rank=same; TOP} + {rank=same; INT_TOP; FLT_TOP; FL8_TOP; XCTRL } + {rank=same; INT_CON; INT_CON0; INT_CON1; + FLT_CON32; FLT_CON64; FLT_CON0; FLT_CONPI; + FL8_MINDOTS; FL8_ZERO; FL8_MAXDOTS; + } + {rank=same; INT_BOT; FLT_BOT; FL8_BOT; CTRL; } + {rank=same; BOT;} +} diff --git a/docs/lattice_iffc.svg b/docs/lattice_iffc.svg new file mode 100644 index 00000000..8ca5afd0 --- /dev/null +++ b/docs/lattice_iffc.svg @@ -0,0 +1,396 @@ + + + + + + +Lattice + + + +TOP + +⊤ + + + +XCTRL + +⊤ +:ctrl + + + +TOP->XCTRL + + + + + +INT_TOP + +⊤ +:int + + + +TOP->INT_TOP + + + + + +FLT_TOP + +⊤ +:flt + + + +TOP->FLT_TOP + + + + + +FL8_TOP + +⊤ +:FP8 + + + +TOP->FL8_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 + + + + + +FL8_MINDOTS + +... + + + +FL8_TOP->FL8_MINDOTS + + + + + +FL8_ZERO + +0 + + + +FL8_TOP->FL8_ZERO + + + + + +FL8_MAXDOTS + +... + + + +FL8_TOP->FL8_MAXDOTS + + + + + +FL8_BOT + +⊥ +:FP8 + + + +FL8_BOT->BOT + + + + + +FL8_MINDOTS->FL8_BOT + + + + + + +FL8_ZERO->FL8_BOT + + + + + + +FL8_MAXDOTS->FL8_BOT + + + + + diff --git a/docs/lattice_iffcs.gv b/docs/lattice_iffcs.gv new file mode 100644 index 00000000..5b849ccf --- /dev/null +++ b/docs/lattice_iffcs.gv @@ -0,0 +1,143 @@ +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]; + + // ---------------------- + // sub-Floats + FL8_TOP [label=<⊤:FP8>, fillcolor=aqua, shape=oval]; + FL8_BOT [label=<⊥:FP8>, fillcolor=aqua, shape=oval]; + + FL8_MINDOTS [label="...", fillcolor=aqua, shape=oval]; + FL8_ZERO [label="0" , fillcolor=aqua]; + FL8_MAXDOTS [label="...", fillcolor=aqua, shape=oval]; + + TOP -> FL8_TOP; + FL8_TOP -> FL8_MINDOTS; + FL8_TOP -> FL8_ZERO; + FL8_TOP -> FL8_MAXDOTS; + FL8_MINDOTS -> FL8_BOT; + FL8_ZERO -> FL8_BOT; + FL8_MAXDOTS -> FL8_BOT; + FL8_BOT -> BOT; + + FL8_MINDOTS -> FL8_ZERO -> FL8_MAXDOTS [style=invis]; + + // ---------------------- + // 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]; + + // Additional customization + {rank=same; TOP} + {rank=same; INT_TOP; FLT_TOP; FL8_TOP; XCTRL } + {rank=same; INT_CON; INT_CON0; INT_CON1; + FLT_CON32; FLT_CON64; FLT_CON0; FLT_CONPI; + FL8_MINDOTS; FL8_ZERO; FL8_MAXDOTS; + STRUCT_S1; STRUCT_S2; STRUCT_SN; + } + {rank=same; INT_BOT; FLT_BOT; FL8_BOT; CTRL; } + {rank=same; BOT;} +} diff --git a/docs/lattice_iffcs.svg b/docs/lattice_iffcs.svg new file mode 100644 index 00000000..fc976d90 --- /dev/null +++ b/docs/lattice_iffcs.svg @@ -0,0 +1,547 @@ + + + + + + +Lattice + + + +TOP + +⊤ + + + +XCTRL + +⊤ +:ctrl + + + +TOP->XCTRL + + + + + +INT_TOP + +⊤ +:int + + + +TOP->INT_TOP + + + + + +FLT_TOP + +⊤ +:flt + + + +TOP->FLT_TOP + + + + + +FL8_TOP + +⊤ +:FP8 + + + +TOP->FL8_TOP + + + + + +STRUCT_TOP + +⊤ +:struct + + + +TOP->STRUCT_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 + + + + + +FL8_MINDOTS + +... + + + +FL8_TOP->FL8_MINDOTS + + + + + +FL8_ZERO + +0 + + + +FL8_TOP->FL8_ZERO + + + + + +FL8_MAXDOTS + +... + + + +FL8_TOP->FL8_MAXDOTS + + + + + +FL8_BOT + +⊥ +:FP8 + + + +FL8_BOT->BOT + + + + + +FL8_MINDOTS->FL8_BOT + + + + + + +FL8_ZERO->FL8_BOT + + + + + + +FL8_MAXDOTS->FL8_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 + + + + + diff --git a/docs/lattice_iffct.gv b/docs/lattice_iffct.gv new file mode 100644 index 00000000..becb2612 --- /dev/null +++ b/docs/lattice_iffct.gv @@ -0,0 +1,145 @@ +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]; + + // ---------------------- + // sub-Floats + FL8_TOP [label=<⊤:FP8>, fillcolor=aqua, shape=oval]; + FL8_BOT [label=<⊥:FP8>, fillcolor=aqua, shape=oval]; + + FL8_MINDOTS [label="...", fillcolor=aqua, shape=oval]; + FL8_ZERO [label="0" , fillcolor=aqua]; + FL8_MAXDOTS [label="...", fillcolor=aqua, shape=oval]; + + TOP -> FL8_TOP; + FL8_TOP -> FL8_MINDOTS; + FL8_TOP -> FL8_ZERO; + FL8_TOP -> FL8_MAXDOTS; + FL8_MINDOTS -> FL8_BOT; + FL8_ZERO -> FL8_BOT; + FL8_MAXDOTS -> FL8_BOT; + FL8_BOT -> BOT; + + FL8_MINDOTS -> FL8_ZERO -> FL8_MAXDOTS [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; FL8_TOP; XCTRL } + {rank=same; INT_CON; INT_CON0; INT_CON1; + FLT_CON32; FLT_CON64; FLT_CON0; FLT_CONPI; + FL8_MINDOTS; FL8_ZERO; FL8_MAXDOTS; + TUPLE1; TUPLE2; TUPLEN; + } + {rank=same; INT_BOT; FLT_BOT; FL8_BOT; CTRL; } + {rank=same; BOT;} +} diff --git a/docs/lattice_iffct.svg b/docs/lattice_iffct.svg new file mode 100644 index 00000000..3c38552b --- /dev/null +++ b/docs/lattice_iffct.svg @@ -0,0 +1,500 @@ + + + + + + +Lattice + + + +TOP + +⊤ + + + +XCTRL + +⊤ +:ctrl + + + +TOP->XCTRL + + + + + +INT_TOP + +⊤ +:int + + + +TOP->INT_TOP + + + + + +FLT_TOP + +⊤ +:flt + + + +TOP->FLT_TOP + + + + + +FL8_TOP + +⊤ +:FP8 + + + +TOP->FL8_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 + + + + + +FL8_MINDOTS + +... + + + +FL8_TOP->FL8_MINDOTS + + + + + +FL8_ZERO + +0 + + + +FL8_TOP->FL8_ZERO + + + + + +FL8_MAXDOTS + +... + + + +FL8_TOP->FL8_MAXDOTS + + + + + +FL8_BOT + +⊥ +:FP8 + + + +FL8_BOT->BOT + + + + + +FL8_MINDOTS->FL8_BOT + + + + + + +FL8_ZERO->FL8_BOT + + + + + + +FL8_MAXDOTS->FL8_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 + + + + + -- cgit v1.2.3