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 IN: stack-checker
   9
  10 ARTICLE: "inference-simple" "Straight-line stack effects"
  11 "The simplest case to look at is that of a quotation which does not have any branches or recursion, and just pushes literals and calls words, each of which has a known stack effect."
  12 $nl
  13 "Stack effect inference works by stepping through the quotation, while maintaining a \"shadow stack\" which tracks stack height at the current position in the quotation. Initially, the shadow stack is empty. If a word is encountered which expects more values than there are on the shadow stack, a global counter is incremented. This counter keeps track of the number of inputs the quotation expects on the stack. When inference is done, this counter, together with the final height of the shadow stack, gives the inferred stack effect."
  14 { $subsection d-in }
  15 { $subsection meta-d }
  16 "When a literal is encountered, it is simply pushed on the shadow stack. For example, the stack effect of the following quotation is inferred by pushing all three literals on the shadow stack, then taking the value of " { $link d-in } " and the length of " { $link meta-d } ":"
  17 { $example "[ 1 2 3 ] infer." "( -- object object object )" }
  18 "In the following example, the call to " { $link + } " expects two values on the shadow stack, but only one value is present, the literal which was pushed previously. This increments the " { $link d-in } " counter by one:"
  19 { $example "[ 2 + ] infer." "( object -- object )" }
  20 "After the call to " { $link + } ", the shadow stack contains a \"computed value placeholder\", since the inferencer has no way to know what the resulting value actually is (in fact it is arbitrary)." ;
  21
  22 ARTICLE: "inference-combinators" "Combinator stack effects"
  23 "Without further information, one cannot say what the stack effect of " { $link call } " is; it depends on the given quotation. If the inferencer encounters a " { $link call } " without further information, a " { $link literal-expected } " error is raised."
  24 { $example "[ dup call ] infer." "... an error ..." }
  25 "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:"
  26 { $example "[ [ 2 + ] call ] infer." "( object -- object )" }
  27 "Consider a combinator such as " { $link keep } ". The combinator itself does not have a stack effect, because it applies " { $link call } " to a potentially arbitrary quotation. However, since the combinator is declared " { $link POSTPONE: inline } ", a given usage of it can have a stack effect:"
  28 { $example "[ [ 2 + ] keep ] infer." "( object -- object object )" }
  29 "Another example is the " { $link compose } " combinator. Because it is decared " { $link POSTPONE: inline } ", we can infer the stack effect of applying " { $link call } " to the result of " { $link compose } ":"
  30 { $example "[ 2 [ + ] curry [ sq ] compose ] infer." "( -- object object )" }
  31 "Incidentally, this example demonstrates that the stack effect of nested currying and composition can also be inferred."
  32 $nl
  33 "A general rule of thumb is that any word which applies " { $link call } " or " { $link curry } " to one of its inputs must be declared " { $link POSTPONE: inline } "."
  34 $nl
  35 "Here is an example where the stack effect cannot be inferred:"
  36 { $code ": foo 0 [ + ] ;" "[ foo reduce ] infer." }
  37 "However if " { $snippet "foo" } " was declared " { $link POSTPONE: inline } ", everything would work, since the " { $link reduce } " combinator is also " { $link POSTPONE: inline } ", and the inferencer can see the literal quotation value at the point it is passed to " { $link call } ":"
  38 { $example ": foo 0 [ + ] ; inline" "[ foo reduce ] infer." "( object -- object )" } ;
  39
  40 ARTICLE: "inference-branches" "Branch stack effects"
  41 "Conditionals such as " { $link if } " and combinators built on " { $link if } " present a problem, in that if the two branches leave the stack at a different height, it is not clear what the stack effect should be. In this case, inference throws a " { $link unbalanced-branches-error } "."
  42 $nl
  43 "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,"
  44 { $example "[ [ + ] [ drop ] if ] infer." "( object object object -- object )" }
  45 "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 )" } "." ;
  46
  47 ARTICLE: "inference-recursive" "Stack effects of recursive words"
  48 "When a recursive call is encountered, the declared stack effect is substituted in. When inference is complete, the inferred stack effect is compared with the declared stack effect."
  49 $nl
  50 "Attempting to infer the stack effect of a recursive word which outputs a variable number of objects on the stack will fail. For example, the following will throw an " { $link unbalanced-branches-error } ":"
  51 { $code ": foo ( seq -- ) dup empty? [ drop ] [ dup pop foo ] if" "[ foo ] infer." }
  52 "If you declare an incorrect stack effect, inference will fail also. Badly defined recursive words cannot confuse the inferencer." ;
  53
  54 ARTICLE: "inference-recursive-combinators" "Recursive combinator inference"
  55 "Most combinators are not explicitly recursive; instead, they are implemented in terms of existing combinators, for example " { $link while } ", " { $link map } ", and the " { $link "compositional-combinators" } "."
  56 $nl
  57 "Combinators which are recursive require additional care."
  58 $nl
  59 "If a recursive word takes quotation parameters from the stack and calls them, it must be declared " { $link POSTPONE: inline } " (as documented in " { $link "inference-combinators" } ") as well as " { $link POSTPONE: recursive } "."
  60 $nl
  61 "Furthermore, the input parameters which are quotations must be annotated in the stack effect. For example,"
  62 { $see loop }
  63 "An inline recursive word cannot pass a quotation through the recursive call. For example, the following will not infer:"
  64 { $code ": foo ( a b c -- d e f ) [ f foo drop ] when 2dup call ; inline" "[ 1 [ 1+ ] foo ] infer." }
  65 "However a small change can be made:"
  66 { $example ": foo ( a b c -- d ) [ 2dup f foo drop ] when call ; inline" "[ 1 [ 1+ ] t foo ] infer." "( -- object )" }
  67 "An inline recursive word must have a fixed stack effect in its base case. The following will not infer:"
  68 { $code
  69     ": foo ( quot ? -- ) [ f foo ] [ call ] if ; inline"
  70     "[ [ 5 ] t foo ] infer."
  71 } ;
  72
  73 ARTICLE: "compiler-transforms" "Compiler transforms"
  74 "Compiler transforms can be used to allow words to compile which would otherwise not have a stack effect, and to expand combinators into more efficient code at compile time."
  75 { $subsection define-transform }
  76 "An example is the " { $link cond } " word. If the association list of quotations it is given is literal, the entire form is expanded into a series of nested calls to " { $link if } "."
  77 $nl
  78 "The " { $vocab-link "macros" } " vocabulary defines some nice syntax sugar which makes compiler transforms easier to work with." ;
  79
  80 ARTICLE: "inference" "Stack effect inference"
  81 "The stack effect inference tool is used to check correctness of code before it is run. It is also used by the optimizing compiler to build the high-level SSA representation on which optimizations can be performed. Only words for which a stack effect can be inferred will compile with the optimizing compiler; all other words will be compiled with the non-optimizing compiler (see " { $link "compiler" } ")."
  82 $nl
  83 "The main entry point is a single word which takes a quotation and prints its stack effect and variable usage:"
  84 { $subsection infer. }
  85 "Instead of printing the inferred information, it can be returned as objects on the stack:"
  86 { $subsection infer }
  87 "Static stack effect inference can be combined with unit tests; see " { $link "tools.test.write" } "."
  88 $nl
  89 "The following articles describe the implementation of the stack effect inference algorithm:"
  90 { $subsection "inference-simple" }
  91 { $subsection "inference-recursive" }
  92 { $subsection "inference-combinators" }
  93 { $subsection "inference-recursive-combinators" }
  94 { $subsection "inference-branches" }
  95 { $subsection "inference-errors" }
  96 { $subsection "compiler-transforms" }
  97 { $see-also "effects" } ;
  98
  99 ABOUT: "inference"
 100
 101 HELP: inference-error
 102 { $values { "class" class } }
 103 { $description "Creates an instance of " { $snippet "class" } ", wraps it in an " { $link inference-error } " and throws the result." }
 104 { $error-description
 105     "Thrown by " { $link infer } " when the stack effect of a quotation cannot be inferred."
 106     $nl
 107     "The " { $snippet "error" } " slot contains one of several possible " { $link "inference-errors" } "."
 108 } ;
 109
 110
 111 HELP: infer
 112 { $values { "quot" "a quotation" } { "effect" "an instance of " { $link effect } } }
 113 { $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." }
 114 { $errors "Throws an " { $link inference-error } " if stack effect inference fails." } ;
 115
 116 HELP: infer.
 117 { $values { "quot" "a quotation" } }
 118 { $description "Attempts to infer the quotation's stack effect, and prints this data to " { $link output-stream } "." }
 119 { $errors "Throws an " { $link inference-error } " if stack effect inference fails." } ;
 120
 121 { infer infer. } related-words
 122
 123 HELP: forget-errors
 124 { $description "Removes markers indicating which words do not have stack effects."
 125 $nl
 126 "The stack effect inference code remembers which words failed to infer as an optimization, so that it does not try to infer the stack effect of words which do not have one over and over again." }
 127 { $notes "Usually this word does not need to be called directly; if a word failed to compile because of a stack effect error, fixing the word definition clears the flag automatically. However, if words failed to compile due to external factors which were subsequently rectified, such as an unavailable C library or a missing or broken compiler transform, this flag can be cleared for all words:"
 128 { $code "forget-errors" }
 129 "Subsequent invocations of the compiler will consider all words for compilation." } ;