basis/stack-checker/stack-checker-docs.factor

   1 USING: help.syntax help.markup kernel sequences words io
   2 effects classes math combinators
   3 stack-checker.backend
   4 stack-checker.branches
   5 stack-checker.errors
   6 stack-checker.transforms
   7 stack-checker.state
   8 continuations ;
   9 IN: stack-checker
  10
  11 ARTICLE: "inference-simple" "Straight-line stack effects"
  12 "The simplest case is when a piece of code does not have any branches or recursion, and just pushes literals and calls words."
  13 $nl
  14 "Pushing a literal has stack effect " { $snippet "( -- x )" } ". The stack effect of a most words is always known statically from the declaration. Stack effects of " { $link POSTPONE: inline } " words and " { $link "macros" } ", may depend on literals pushed on the stack prior to the call, and this case is discussed in " { $link "inference-combinators" } "."
  15 $nl
  16 "The stack effect of each element in a code snippet is composed. The result is then the stack effect of the snippet."
  17 $nl
  18 "An example:"
  19 { $example "[ 1 2 3 ] infer." "( -- x x x )" }
  20 "Another example:"
  21 { $example "[ 2 + ] infer." "( x -- x )" } ;
  22
  23 ARTICLE: "inference-combinators" "Combinator stack effects"
  24 "If a word calls a combinator, one of the following two conditions must hold for the stack checker to succeed:"
  25 { $list
  26   { "The combinator must be called with a quotation that is either literal or built from literal quotations, " { $link curry } ", and " { $link compose } ". (Note that quotations that use " { $vocab-link "fry" } " or " { $vocab-link "locals" } " use " { $link curry } " and " { $link compose } " from the perspective of the stack checker.)" }
  27   { "If the word is declared " { $link POSTPONE: inline } ", the combinator may additionally be called on one of the word's input parameters or with quotations built from the word's input parameters, literal quotations, " { $link curry } ", and " { $link compose } ". When inline, a word is itself considered to be a combinator, and its callers must in turn satisfy these conditions." }
  28 }
  29 "If neither condition holds, the stack checker throws a " { $link unknown-macro-input } " or " { $link bad-macro-input } " error. To make the code compile, a runtime checking combinator such as " { $link POSTPONE: call( } " must be used instead. See " { $link "inference-escape" } " for details. An inline combinator can be called with an unknown quotation by " { $link curry } "ing the quotation onto a literal quotation that uses " { $link POSTPONE: call( } "."
  30 { $heading "Input stack effects" }
  31 "Inline combinators will verify the stack effect of their input quotations if they are declared in the combinator's stack effect. See " { $link "effects-variables" } " for details."
  32 { $heading "Examples" }
  33 { $subheading "Calling a combinator" }
  34 "The following usage of " { $link map } " passes the stack checker, because the quotation is the result of " { $link curry } ":"
  35 { $example "USING: math sequences ;" "[ [ + ] curry map ] infer." "( x x -- x )" }
  36 "The equivalent code using " { $vocab-link "fry" } " and " { $vocab-link "locals" } " likewise passes the stack checker:"
  37 { $example "USING: fry math sequences ;" "[ '[ _ + ] map ] infer." "( x x -- x )" }
  38 { $example "USING: locals math sequences ;" "[| a | [ a + ] map ] infer." "( x x -- x )" }
  39 { $subheading "Defining an inline combinator" }
  40 "The following word calls a quotation twice; the word is declared " { $link POSTPONE: inline } ", since it invokes " { $link call } " on the result of " { $link compose } " on an input parameter:"
  41 { $code ": twice ( value quot -- result ) dup compose call ; inline" }
  42 "The following code now passes the stack checker; it would fail were " { $snippet "twice" } " not declared " { $link POSTPONE: inline } ":"
  43 { $unchecked-example "USE: math.functions" "[ [ sqrt ] twice ] infer." "( x -- x )" }
  44 { $subheading "Defining a combinator for unknown quotations" }
  45 "In the next example, " { $link POSTPONE: call( } " must be used because the quotation is the result of calling a runtime accessor, and the compiler cannot make any static assumptions about this quotation at all:"
  46 { $code
  47   "TUPLE: action name quot ;"
  48   ": perform ( value action -- result ) quot>> call( value -- result ) ;"
  49 }
  50 { $subheading "Passing an unknown quotation to an inline combinator" }
  51 "Suppose we want to write:"
  52 { $code ": perform ( values action -- results ) quot>> map ;" }
  53 "However this fails to pass the stack checker since there is no guarantee the quotation has the right stack effect for " { $link map } ". It can be wrapped in a new quotation with a declaration:"
  54 { $code ": perform ( values action -- results )" "    quot>> [ call( value -- result ) ] curry map ;" }
  55 { $heading "Explanation" }
  56 "This restriction exists because without further information, one cannot say what the stack effect of " { $link call } " is; it depends on the given quotation. If the stack checker encounters a " { $link call } " without further information, a " { $link unknown-macro-input } " or " { $link bad-macro-input } " error is raised."
  57 $nl
  58 "On the other hand, the stack effect of applying " { $link call } " to a literal quotation or a " { $link curry } " of a literal quotation is easy to compute; it behaves as if the quotation was substituted at that point."
  59 { $heading "Limitations" }
  60 "The stack checker cannot guarantee that a literal quotation is still literal if it is passed on the data stack to an inlined recursive combinator such as " { $link each } " or " { $link map } ". For example, the following will not infer:"
  61 { $example
  62   "[ [ reverse ] swap [ reverse ] map swap call ] infer." "Cannot apply “call” to a run-time computed value\nmacro call"
  63 }
  64 "To make this work, use " { $link dip } " to pass the quotation instead:"
  65 { $example
  66   "[ [ reverse ] [ [ reverse ] map ] dip call ] infer." "( x -- x )"
  67 } ;
  68
  69 ARTICLE: "inference-branches" "Branch stack effects"
  70 "Conditionals such as " { $link if } " and combinators built on top have the same restrictions as " { $link POSTPONE: inline } " combinators (see " { $link "inference-combinators" } ") with the additional requirement that all branches leave the stack at the same height. If this is not the case, the stack checker throws a " { $link unbalanced-branches-error } "."
  71 $nl
  72 "If all branches leave the stack at the same height, then the stack effect of the conditional is just the maximum of the stack effect of each branch. For example,"
  73 { $example "[ [ + ] [ drop ] if ] infer." "( x x x -- x )" }
  74 "The call to " { $link if } " takes one value from the stack, a generalized boolean. The first branch " { $snippet "[ + ]" } " has stack effect " { $snippet "( x x -- x )" } " and the second has stack effect " { $snippet "( x -- )" } ". Since both branches decrease the height of the stack by one, we say that the stack effect of the two branches is " { $snippet "( x x -- x )" } ", and together with the boolean popped off the stack by " { $link if } ", this gives a total stack effect of " { $snippet "( x x x -- x )" } "." ;
  75
  76 ARTICLE: "inference-recursive-combinators" "Recursive combinator stack effects"
  77 "Most combinators do not call themselves recursively directly; instead, they are implemented in terms of existing combinators, for example " { $link while } ", " { $link map } ", and the " { $link "compositional-combinators" } ". In these cases, the rules outlined in " { $link "inference-combinators" } " apply."
  78 $nl
  79 "Combinators which are recursive require additional care. In addition to being declared " { $link POSTPONE: inline } ", they must be declared " { $link POSTPONE: recursive } ". There are three restrictions that only apply to combinators with this declaration:"
  80 { $heading "Input quotation declaration" }
  81 "Input parameters which are quotations must be annotated as much in the stack effect. For example, the following will not infer:"
  82 { $unchecked-example ": bad ( quot -- ) [ call ] keep bad ; inline recursive" "[ [ ] bad ] infer." "Cannot apply “call” to a run-time computed value\nmacro call" }
  83 "The following is correct:"
  84 { $example ": good ( quot: ( -- ) -- ) [ call ] keep good ; inline recursive" "[ [ ] good ] infer." "( -- )" }
  85 "The effect of the nested quotation itself is only present for documentation purposes; the mere presence of a nested effect is sufficient to mark that value as a quotation parameter."
  86 { $heading "Data flow restrictions" }
  87 "The stack checker does not trace data flow in two instances."
  88 $nl
  89 "An inline recursive word cannot pass a quotation on the data stack through the recursive call. For example, the following will not infer:"
  90 { $unchecked-example ": bad ( ? quot: ( ? -- ) -- ) 2dup [ not ] dip bad call ; inline recursive" "[ [ drop ] bad ] infer." "Cannot apply “call” to a run-time computed value\nmacro call" }
  91 "However a small change can be made:"
  92 { $example ": good ( ? quot: ( ? -- ) -- ) [ good ] 2keep [ not ] dip call ; inline recursive" "[ [ drop ] good ] infer." "( x -- )" }
  93 "An inline recursive word must have a fixed stack effect in its base case. The following will not infer:"
  94 { $example
  95     ": foo ( quot ? -- ) [ f foo ] [ call ] if ; inline"
  96     "[ [ 5 ] t foo ] infer."
  97     "The inline recursive word “foo” must be declared recursive\nword foo"
  98 } ;
  99
 100 ARTICLE: "tools.inference" "Stack effect tools"
 101 { $link "inference" } " can be used interactively to print stack effects of quotations without running them. It can also be used from " { $link "combinators.smart" } "."
 102 { $subsections
 103     infer
 104     infer.
 105 }
 106 "There are also some words for working with " { $link effect } " instances. Getting a word's declared stack effect:"
 107 { $subsections stack-effect }
 108 "Converting a stack effect to a string form:"
 109 { $subsections effect>string }
 110 "Comparing effects:"
 111 { $subsections
 112     effect-height
 113     effect<=
 114     effect=
 115 }
 116 "The class of stack effects:"
 117 { $subsections
 118     effect
 119     effect?
 120 } ;
 121
 122 ARTICLE: "inference-escape" "Stack effect checking escape hatches"
 123 "In a static checking regime, sometimes it is necessary to step outside the boundaries and run some code which cannot be statically checked; perhaps this code is constructed at run-time. There are two ways to get around the static stack checker."
 124 $nl
 125 "If the stack effect of a word or quotation is known, but the word or quotation itself is not, " { $link POSTPONE: execute( } " or " { $link POSTPONE: call( } " can be used. See " { $link "call" } " for details."
 126 $nl
 127 "If the stack effect is not known, the code being called cannot manipulate the datastack directly. Instead, it must reflect the datastack into an array:"
 128 { $subsections with-datastack }
 129 "The surrounding code has a static stack effect since " { $link with-datastack } " has one. However, the array passed in as input may be transformed arbitrarily by calling this combinator." ;
 130
 131 ARTICLE: "inference" "Stack effect checking"
 132 "The " { $link "compiler" } " checks the " { $link "effects" } " of words before they can be run. This ensures that words take exactly the number of inputs and outputs that the programmer declares in source."
 133 $nl
 134 "Words that do not pass the stack checker are rejected and cannot be run, and so essentially this defines a very simple and permissive type system that nevertheless catches some invalid programs and enables compiler optimizations."
 135 $nl
 136 "If a word's stack effect cannot be inferred, a compile error is reported. See " { $link "compiler-errors" } "."
 137 $nl
 138 "The following articles describe how different control structures are handled by the stack checker."
 139 { $subsections
 140     "inference-simple"
 141     "inference-combinators"
 142     "inference-recursive-combinators"
 143     "inference-branches"
 144 }
 145 "Stack checking catches several classes of errors."
 146 { $subsections "inference-errors" }
 147 "Sometimes code with a dynamic stack effect has to be run."
 148 { $subsections "inference-escape" }
 149 { $see-also "effects" "tools.inference" "tools.errors" } ;
 150
 151 ABOUT: "inference"
 152
 153 HELP: inference-error
 154 { $values { "class" class } }
 155 { $description "Creates an instance of " { $snippet "class" } ", wraps it in an " { $link inference-error } " and throws the result." }
 156 { $error-description
 157     "Thrown by " { $link infer } " when the stack effect of a quotation cannot be inferred."
 158     $nl
 159     "The " { $snippet "error" } " slot contains one of several possible " { $link "inference-errors" } "."
 160 } ;
 161
 162 HELP: infer
 163 { $values { "quot" "a quotation" } { "effect" "an instance of " { $link effect } } }
 164 { $description "Attempts to infer the quotation's stack effect. For interactive testing, the " { $link infer. } " word should be called instead since it presents the output in a nicely formatted manner." }
 165 { $errors "Throws an " { $link inference-error } " if stack effect inference fails." } ;
 166
 167 HELP: infer.
 168 { $values { "quot" "a quotation" } }
 169 { $description "Attempts to infer the quotation's stack effect, and prints this data to " { $link output-stream } "." }
 170 { $errors "Throws an " { $link inference-error } " if stack effect inference fails." } ;
 171
 172 { infer infer. } related-words