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.

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.

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.

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 noForth documentation to learn how DIVE works.

INS and OUTS counts the number of items in the stack comment before and after - -.

(* 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

\ 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.

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.

Alternative Implementations

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" <name>" - 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

Please add it at the end of this document.