===== Stack Checking Utility: Debugging through Run-Time Stack Checks =====
==== Stack Checking idea ====
The Stack Checking utility is a debugging tool for Forth, used to validate stack comments and the actual stack behaviour of a word. It's a run-time check that ensures the number of items in the stack before and after the execution of a word, matches the comment description.
Often, an incorrect stack effect, i.e., the actual stack effect differing from the one specified, results in programming errors. With the Stack Checking utility, these can be identified and rectified in the programming phase itself, thus ensuring robust programs and applications.
==== Stack Checking Implementation ====
The Stack Checking utility uses the stack comments provided to check the stack. This does not aim to understand the semantics of the stack comment but uses the information about the number of stack items available before and after a word's execution. Stack comments used for checking are started with **(?** and have the form
(? items before execution -- items after execution )
The utility analyses these kinds of comments and checks for two things:
1. The number of stack items a given word expects on the data stack. If this number is violated, it indicates improper use of the word.
2. The number of items a given word will additionally put on the top of the data stack (or remove). If the word leaves less or more items than this number, it indicates improper behavior of the word.
It checks the stack depth on entry of a word and calculates the expected stack depth on exit. Once the execution of the word has finished, the expected stack depth is checked against the actual stack depth.
==== Pseudo code for the Stack Checking implementation ====
Analyze stack comments by counting the number of tokens before and after the - -. This gives the number of items expected by the word and the number of items then left by the word. We can easily calculate the change in the number of items (the stack effect).
Assuming we know the **required number of items** of the current word and **its stack effect**. We can generate code that will check the stack on entry and (and by creating a stack frame) on exit of the word. This code will
* Examine the current stack depth before the execution of the word.
* Check if the stack depth is at least equal to the number of items expected by the word.
* If not, trigger a runtime error message.
* If yes, calculate the expected stack depth after the execution of the word.
* Create a stack frame do that we can execute code after the current words execution.
* Execute the current word.
* In the exit code check the actual stack depth after execution against the expected stack depth.
* If they are different, trigger a runtime error message.
==== Various Stack Checking Implementations ====
Stack Checking is actually performed by the word CHECK that uses the noForth specifica DIVE facility to execute code before and after a word. See the [[https://home.hccnet.nl/anij/nof/noforth%20documentation.pdf|noForth documentation]] to learn how DIVE works.
INS and OUTS counts the number of items in the stack comment before and after - -.
=== Stack Checking for noForth T ===
(* Runtime Stack Checking a Debugging Aid, Ulrich Hoffmann see euroFORML'91 / FORML'91 proceedings
noForth Forth Version 2023-04-23
Use (? as stack comment start to check the stack of the current word at runtime.
*)
inside also definitions
: check ( name #chge #before -- )
depth 3 - >
IF swap count type ." needs more arguments!" abort THEN
depth 2 - + r> -rot 2>r >r ( pass name and #after )
dive 2r> ( name #after -- )
2 + depth = IF drop EXIT THEN
count type ." has incorrect stack effect!" abort ;
: ins ( -- n ) 0 BEGIN bl-word count s" --" s<> WHILE 1+ REPEAT ;
: outs ( -- n ) 0 BEGIN bl-word count s" )" s<> WHILE 1+ REPEAT ;
forth definitions
: (? ( -- )
created LFA>N postpone LITERAL \ word name
ins outs over - postpone LITERAL \ stack depth change
postpone LITERAL \ number of expected items
postpone CHECK
; immediate
=== How to use the Stack Checking Utility ===
\ a word with mismatched stack effect and comment
: unchecked ( a b -- c ) over + ; \ wrong, unchecked
\ 1 2 unchecked will just give an incorrect result
\ a word with mismatched stack effect and comment now with stack checking
: test (? a b c -- 1 2 ) drop drop drop 1 ; \ wrong
\ 1 2 3 test -> error message "test has incorrect stack effect"
\ a word that uses the incorrect TEST
: t (? a -- b ) dup dup test drop ; \ wrong
\ 1 t -> error message "test has incorrect stack effect"
\ a word with non static stack effect - not checked
: -dup ( n -- n n | 0 ) \ unchecked
dup IF dup THEN ;
\ 10 -dup -> will just run without checking nor error
\ a word with matching stack effect and stack comment
: fine (? n1 n2 n3 -- n3 n3 n3 ) nip nip ( n3 ) dup dup ; \ correct
\ 1 2 3 fine -> just runs fine
Alternative implementations of stack checking might exist and can be added at the end of this description.
==== Possible pitfalls with Stack Checking ====
Some Forth words, such as "?DUP" do not have a fixed stack effect. They change the stack according to the data received, and these words cannot be checked by this method. However, checking is only enabled by starting a stack comment with (?. Normal stack comments are not checked. You could place a special visual comment maker (like !!!) after the stack comment to warn the programmer about these potential dangerous words and encourage extensive testing.
==== Contributions ====
Alternative Implementations
=== Albert Nijhof's version ===
Albert proposes to avoid counting traditional stack comments but to add the stack effect at the end of the stack comments. This results in simpler code:
A poor man's stack checker for noForth - (an) 02may2023
: STACK.CHECK ( stack-growth nfa -- )
depth
swap r> 2>r \ save nfa
+ r> 2>r \ save expected depth
dive \ finish the main word now
2r> depth - \ depth not as expected?
dup if cr ." Error in "
over count hx 1F and type space
dup s>d if ." +" then negate .
?abort
then 2drop ;
0 value CHECK?
: (? ( -- )
[char] ) parse + 2 - \ read "n)"
check?
if count swap c@ \ sign and digit
[char] 0 - swap
[char] - = if negate then
postpone literal \ expected stack growth
created lfa>n postpone literal \ nfa of main word
postpone stack.check
exit then
drop ; immediate
Use:\\
Start a definition with (? ... n) which means that at EXIT the stack is
expected to have n elements more, or less, depending on the sign of n.\\
n consists of two characters, the first must be + or -,
the second a digit in [0,9]. See examples below.
Usual stack comment is possible between (? and n), for example:
: ?NEGATE (? x y -- x' -1) 0< if negate then ;
A flag in the value CHECK? determines whether the stack checker
will be compiled or not.
Typical noForth words in the code:
DIVE Exchange IP and top of return stack
?ABORT Same as ABORT" " - in this case the effect is the same as ABORT" STACK.CHECK"
CREATED LFA of the definition which is being build at the moment
LFA>N LFA -> NFA
HX The following number is in HEX
Examples
true to check?
: T1 (? +1) ?dup ; \ stack is expected to grow with 1 element
: T2 (? +2) ; \ stack should grow with 2 elements
: T3 (? -3) ; \ stack should shrink with 3 elements
: T4 (? +0) ; \ stack depth should not change
Test results
@)5 t1 .s 2drop ( 5 5 ) OK.0
@)0 t1 .s drop
Error in T1 -1
Msg from STACK.CHECK \ Error # AB29 -54D7
( this means that there is 1 element less than expected on the stack )
@)t2
Error in T2 -2
Msg from STACK.CHECK \ Error # AB29 -54D7
( 2 elements less than expected )
@)t3
Error in T3 3
Msg from STACK.CHECK \ Error # AB29 -54D7
( 3 elements more than expected )
@)t4 OK.0
=== Do you have another approach to Stack Checking? ===
Please add it at the end of this document.
~~DISCUSSION~~