From 0caf37adc5f8c1600f13d80aaf77361f407c9694 Mon Sep 17 00:00:00 2001 From: Dibyendu Majumdar Date: Thu, 2 May 2024 22:08:06 +0100 Subject: Documentation updates (#76) * More clearly explain why we do not have an AST in the implementation * Improve the description of type lattice. Cross reference to future chapters. * Minor update * Add lattice visual Revise the text describing meet. * minor update * Add a lattice visual to the text * Update the lattice visual. Add description of the new edges in the SoN graph --- chapter10/docs/lattice.gv | 71 ++++--- chapter10/docs/lattice.svg | 486 ++++++++++++++++++++++++--------------------- 2 files changed, 304 insertions(+), 253 deletions(-) (limited to 'chapter10/docs') diff --git a/chapter10/docs/lattice.gv b/chapter10/docs/lattice.gv index 406a62c3..bf7403f7 100644 --- a/chapter10/docs/lattice.gv +++ b/chapter10/docs/lattice.gv @@ -7,32 +7,35 @@ digraph Lattice { TOP [label="⊤"]; BOT [label="⊥"]; - CTRL [label="Ctrl"]; XCTRL [label="~Ctrl"]; + CTRL [label="Ctrl"]; INT_TOP [label="IntTop"]; INT_BOT [label="IntBot"]; INT_MIN [label="-n"]; INT_MINDOTS [label="..." shape=none style=none]; - INT_MINUS [label="-1"]; INT_ZERO [label="0"]; - INT_PLUS [label="1"]; INT_MAXDOTS [label="..." shape=none style=none]; INT_MAX [label="+n"]; + TUPLE [label="TUPLE"]; + STRUCT_TOP [label="$TOP"]; STRUCT_S1 [label="S1"]; - STRUCT_S2 [label="S2"]; + STRUCT_DOTS [label="..." shape=none style=none]; + STRUCT_SN [label="Sn"]; STRUCT_BOT [label="$BOT"] PTR_TOP [label="*$TOP"]; PTR_NULL [label="null"]; PTR_VOIDPTR [label="*void"]; PTR_S1 [label="*S1"]; - PTR_S2 [label="*S2"]; + PTR_SDOTS [label="..." shape=none style=none]; + PTR_SN [label="*SN"]; PTR_S1OPT [label="*S1?"]; - PTR_S2OPT [label="*S2?"]; + PTR_SOPTDOTS [label="..." shape=none style=none]; + PTR_SNOPT [label="*SN?"]; PTR_BOT [label="*$BOT?"]; MEM_TOP [label="MEM#TOP"]; @@ -45,53 +48,64 @@ digraph Lattice { // Define edges edge [arrowhead=none]; - TOP -> CTRL; - CTRL -> XCTRL; - XCTRL -> BOT; + TOP -> XCTRL; + XCTRL -> CTRL; + CTRL -> BOT; 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; - INT_MIN -> INT_MINDOTS -> INT_MINUS -> INT_ZERO -> INT_PLUS -> INT_MAXDOTS -> INT_MAX [style=invis]; + INT_MIN -> INT_MINDOTS -> INT_ZERO -> INT_MAXDOTS -> INT_MAX [style=invis]; + + TOP -> TUPLE; + TUPLE -> BOT; TOP -> STRUCT_TOP; STRUCT_TOP -> STRUCT_S1; - STRUCT_TOP -> STRUCT_S2; + STRUCT_TOP -> STRUCT_DOTS; + STRUCT_TOP -> STRUCT_SN; STRUCT_S1 -> STRUCT_BOT; - STRUCT_S2 -> STRUCT_BOT; + STRUCT_DOTS -> STRUCT_BOT; + STRUCT_SN -> STRUCT_BOT; STRUCT_BOT -> BOT; + STRUCT_S1 -> STRUCT_DOTS -> STRUCT_SN [style=invis]; + TOP -> PTR_TOP; PTR_TOP -> PTR_S1; - PTR_TOP -> PTR_S2; + PTR_TOP -> PTR_SDOTS; + PTR_TOP -> PTR_SN; PTR_TOP -> PTR_NULL; PTR_TOP -> PTR_VOIDPTR; PTR_NULL -> PTR_BOT; PTR_NULL -> PTR_S1OPT; - PTR_NULL -> PTR_S2OPT; + PTR_NULL -> PTR_SOPTDOTS; + PTR_NULL -> PTR_SNOPT; PTR_S1 -> PTR_S1OPT; PTR_S1 -> PTR_VOIDPTR; - PTR_S2 -> PTR_S2OPT; - PTR_S2 -> PTR_VOIDPTR; + PTR_SDOTS -> PTR_SOPTDOTS; + PTR_SDOTS -> PTR_VOIDPTR; + PTR_SN -> PTR_SNOPT; + PTR_SN -> PTR_VOIDPTR; PTR_VOIDPTR -> PTR_BOT; PTR_S1OPT -> PTR_BOT; - PTR_S2OPT -> PTR_BOT; + PTR_SOPTDOTS -> PTR_BOT; + PTR_SNOPT -> PTR_BOT; PTR_BOT -> BOT; + PTR_S1 -> PTR_SDOTS -> PTR_SN [style=invis]; + PTR_S1OPT -> PTR_SOPTDOTS -> PTR_SNOPT [style=invis]; + TOP -> MEM_TOP; MEM_TOP -> MEM_ALIAS1; MEM_TOP -> MEM_ALIAS2; @@ -106,17 +120,16 @@ digraph Lattice { MEM_ALIAS1 -> MEM_ALIAS2 -> MEM_ALIASDOTS -> MEM_ALIASN [style=invis]; // Additional customization - {rank=same; TOP} - {rank=same; INT_TOP; CTRL; STRUCT_TOP; PTR_TOP; MEM_TOP;} - {rank=same; PTR_S1; PTR_S2;} + {rank=same; TOP;} + {rank=same; INT_TOP; XCTRL; STRUCT_TOP; PTR_TOP; MEM_TOP;} + {rank=same; PTR_S1; PTR_SDOTS; PTR_SN;} {rank=same; INT_MIN; INT_MINDOTS; - INT_MINUS; INT_ZERO; - INT_PLUS; INT_MAXDOTS; - INT_MAX; STRUCT_S1; STRUCT_S2; + INT_ZERO; INT_MAXDOTS; + INT_MAX; TUPLE; STRUCT_S1; STRUCT_DOTS; STRUCT_SN; PTR_NULL; PTR_VOIDPTR; MEM_ALIAS1; MEM_ALIAS2; MEM_ALIASDOTS; MEM_ALIASN;} - {rank=same; PTR_S1OPT; PTR_S2OPT;} - {rank=same; INT_BOT; XCTRL; STRUCT_BOT; PTR_BOT; MEM_BOT;} + {rank=same; PTR_S1OPT; PTR_SOPTDOTS; PTR_SNOPT; } + {rank=same; INT_BOT; CTRL; STRUCT_BOT; PTR_BOT; MEM_BOT;} {rank=same; BOT;} } \ No newline at end of file diff --git a/chapter10/docs/lattice.svg b/chapter10/docs/lattice.svg index 5ec4bc16..2fe05bbf 100644 --- a/chapter10/docs/lattice.svg +++ b/chapter10/docs/lattice.svg @@ -4,457 +4,495 @@ - - + + Lattice - + TOP - -⊤ + +⊤ - + -CTRL - -Ctrl +XCTRL + +~Ctrl - + -TOP->CTRL - +TOP->XCTRL + INT_TOP - -IntTop + +IntTop TOP->INT_TOP - + + + + +TUPLE + +TUPLE + + + +TOP->TUPLE + - + STRUCT_TOP - -$TOP + +$TOP - + TOP->STRUCT_TOP - + PTR_TOP - -*$TOP + +*$TOP TOP->PTR_TOP - + - + MEM_TOP - -MEM#TOP + +MEM#TOP - + TOP->MEM_TOP - + BOT - -⊥ + +⊥ - + -XCTRL - -~Ctrl +CTRL + +Ctrl - + -CTRL->XCTRL - +XCTRL->CTRL + - + -XCTRL->BOT - +CTRL->BOT + INT_MIN - --n + +-n INT_TOP->INT_MIN - + INT_MINDOTS -... +... INT_TOP->INT_MINDOTS - - - - -INT_MINUS - --1 - - - -INT_TOP->INT_MINUS - + - + INT_ZERO - -0 + +0 - + INT_TOP->INT_ZERO - - - - -INT_PLUS - -1 - - - -INT_TOP->INT_PLUS - + - + INT_MAXDOTS -... +... - + INT_TOP->INT_MAXDOTS - + - + INT_MAX - -+n + ++n - + INT_TOP->INT_MAX - + INT_BOT - -IntBot + +IntBot - + INT_BOT->BOT - + - + 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 - + + + + +TUPLE->BOT + - + STRUCT_S1 - -S1 + +S1 - + STRUCT_TOP->STRUCT_S1 - + - + + +STRUCT_DOTS +... + + + +STRUCT_TOP->STRUCT_DOTS + + + -STRUCT_S2 - -S2 +STRUCT_SN + +Sn - - -STRUCT_TOP->STRUCT_S2 - + + +STRUCT_TOP->STRUCT_SN + + STRUCT_BOT - -$BOT + +$BOT - + STRUCT_S1->STRUCT_BOT - + - - -STRUCT_S2->STRUCT_BOT - + + + +STRUCT_DOTS->STRUCT_BOT + + + + +STRUCT_SN->STRUCT_BOT + - + STRUCT_BOT->BOT - + PTR_NULL - -null + +null - + PTR_TOP->PTR_NULL - + PTR_VOIDPTR - -*void + +*void - + PTR_TOP->PTR_VOIDPTR - + PTR_S1 - -*S1 + +*S1 PTR_TOP->PTR_S1 - + - + -PTR_S2 - -*S2 +PTR_SDOTS +... - + -PTR_TOP->PTR_S2 - +PTR_TOP->PTR_SDOTS + - + +PTR_SN + +*SN + + + +PTR_TOP->PTR_SN + + + + PTR_S1OPT - -*S1? + +*S1? - + PTR_NULL->PTR_S1OPT - + - - -PTR_S2OPT - -*S2? + + +PTR_SOPTDOTS +... - - -PTR_NULL->PTR_S2OPT - + + +PTR_NULL->PTR_SOPTDOTS + + + + +PTR_SNOPT + +*SN? + + + +PTR_NULL->PTR_SNOPT + - + PTR_BOT - -*$BOT? + +*$BOT? - + PTR_NULL->PTR_BOT - + - + PTR_VOIDPTR->PTR_BOT - + - + PTR_S1->PTR_VOIDPTR - + + - + PTR_S1->PTR_S1OPT - + - - -PTR_S2->PTR_VOIDPTR - + + +PTR_SDOTS->PTR_VOIDPTR + - - -PTR_S2->PTR_S2OPT - + + + +PTR_SDOTS->PTR_SOPTDOTS + + + + +PTR_SN->PTR_VOIDPTR + + + +PTR_SN->PTR_SNOPT + + + - + PTR_S1OPT->PTR_BOT - + - - -PTR_S2OPT->PTR_BOT - + + + +PTR_SOPTDOTS->PTR_BOT + + + + +PTR_SNOPT->PTR_BOT + - + PTR_BOT->BOT - + - + MEM_ALIAS1 - -#1 + +#1 - + MEM_TOP->MEM_ALIAS1 - + - + MEM_ALIAS2 - -#2 + +#2 - + MEM_TOP->MEM_ALIAS2 - + - + MEM_ALIASDOTS -... +... - + MEM_TOP->MEM_ALIASDOTS - + - + MEM_ALIASN - -#n + +#n - + MEM_TOP->MEM_ALIASN - + - + MEM_BOT - -MEM#BOT + +MEM#BOT - + MEM_ALIAS1->MEM_BOT - + - + MEM_ALIAS2->MEM_BOT - + - + MEM_ALIASDOTS->MEM_BOT - + - + MEM_ALIASN->MEM_BOT - + - + MEM_BOT->BOT - + -- cgit v1.2.3