Stack Verification

Rob Chapman

What?

This simple translator application is a framework for verifying the stack gymnastics of text written for a VFM (Virtual Forth Machine).

Why?

The most obvious reason is to ascertain program correctness. The corollary to this, is for ascertaining documentation correctness (in the form of stack comments). This stack verification framework may be viewed from another perspective: the definition of a simple stack comment parser and a Forth code parser.

How?

One of the strong virtues of the VFM is the embodiment of a stack as a workspace. This extra resource for the programmer means they have the ability to play with several strongly coupled things at once. Each word defined in the text for the VFM has a stack comment indicating how it will make use of the stack resource. By writing a few translator rules to parse the stack comment and text, it is possible to verify the stack work done by the definition of the word.

Defined words, stack comments and effects

Each word defined in the VFM text is entered into a wordlist. Each entry in this list contains its name, its net stack effect as dictated by its stack comment and its net stack effect as calculated from parsing the text of the definition.

Notes

These are rules which are used by the Translator to verify stack comments of Forth words. The actual stack comment is parsed to produce a number indicating the net stack effect. If it is positive, the stack is being grown. If it is negative, the stack is being consumed. The body of the word is also parsedto create a number indicating the net stack effect. CONSTANT, VARIABLE and : create words in a special list which only contains the name of the word and the two stack numbers using the following structure:

Different rule lists are created to handle the four different translation states. interpret-rules are used to parse anything outside a : definition. Once a : is encountered, a new translation state is defined by using colon-rules or comment-rules if there is a stack comment following the word name. The fourth translation state is the second half of an IF construct. An assumption is made that both paths of this construct produce the same net stack result so the second path is skipped by using endif-rules.

HEX
0 VARIABLE wordlist ( list of stack records )( NOTE: not reset after SHOWME)

: >comment ( tick -- ) EXECUTE ;
: comment ( -- a ) wordlist @ L>TICK >comment ;
: effect ( -- a ) comment CELL + ;

Invalid Stack

Certain condition will invalidate the ability to properly decipher the stack result. In these cases it is useful to note this by marking the stack as invalid.

  8000 CONSTANT #invalid  ( an unlikely stack depth )

: INVALID? ( a -- f ) @ #invalid = ;
: ?STACK ( n \ a -- ) DUP INVALID? IF 2DROP ELSE ! ENDIF ;

 

Rule sets

We will need 3 sets of rules to parse text: looking for definitions (interpret); translating the stack comment (stack) and calculating the net stack effect (colon).

  RULESET interpret  ( for interpreting )
RULESET colon ( for colon definitions )
RULESET stack ( for parsing stack comments )

Interpret rules

These rules are used to comb the text for word definitions, skipping everything else. If the text doesn't match any of the rules then it is discarded by the default rule { }.

interpret RULES
{ }[ inputq PULL DROP ]

{ ( }[ ` ) SCAN ]
{ ?( }[ 0 CHAR ` ( = IF stack ELSE #invalid comment ! colon ENDIF RULES ]

{ VARIABLE }{ CONSTANT }{ QUEUE }{ CREATE }[ 1 1 ]{ Try this in Forth! }
{ : }[ 0 0 ]{ Try this in Forth! ?( }
{ Try this in Forth! }[ CREATE , , DOES> ]{ New definition. }
{ New definition. }[ latest UNLINK wordlist LINK ]

{ IMMEDIATE }[ #invalid comment ! ]

{ ] }[ colon RULES ]

The phrase "Try this in Forth!" actually refers to three things. Firstly, the definition of this phrase comes after it is referenced (this is like allowing forward referencing in Forth). Secondly, it is a phrase definition not "Try-this-in-Forth!" (kind of like active comments). Lastly, a simple solution to the CREATE DOES> dilemma.

The CREATE DOES> dilemma occurs when you want to manipulate a child word after the DOES> part has been attached. Since everything after the DOES> is considered part of the child definition, there is no place to put more parent code. This leads to complex factoring. As an example, say we wish to create a word, define it and then execute it. This could be required by a module defining word which defines a module and then activates it.

: MODULE  ( -- )  CREATE <module parameters>  DOES> <actions> ;
: MODULE ( -- ) MODULE EXECUTE-LATEST ;

: DOES-MODULE ( a -- ) DOES> <actions> ;
: MODULE ( -- ) CREATE <module parameters> DOES-MODULE EXECUTE-LATEST ;

: MODULE ( -- ) CREATE <module parameters> ' EXECUTE-LATEST >R
DOES> <actions> ;

Example 1. Three possible ways of executing a child word after it is defined. EXECUTE-LATEST executes the most recently defined word.

If instead, we define a rule for MODULE:

{ MODULE }[ CREATE <module parameters>  DOES> <actions> ]{ Execute latest. }

Example 2. A possible translation rule for MODULE.

we find that complexity collapses and the usability and maintainability of the code improves.

Colon rules

Words inside a word definition are searched for in the wordlist. If they are found, the stack comment is extracted from them and added the current definition. If the word isn't found then it is checked to see if it is a number, in which case, its net stack effect is to add 1 thing. Unknown words will cause an #invalid stack effect.

colon RULES
: ADD-STACK ( n \ string -- n' ) wordlist SEARCH-DICTIONARY
IF L>TICK >comment DUP INVALID?
IF DROP #invalid effect ! ELSE @ + ENDIF
ELSE NUMBER? IF 1 + ELSE #invalid effect ! ENDIF ENDIF ;

{ }[ inputq PULL ADD-STACK ]

{ ( }[ ` ) SCAN ]

{ ." }[ ` " SCAN ]
{ " }[ 1 + ]{ ." }

{ ' }{ ` }[ BL WORD 1 + ]

If a change of interpretation state is detected in the text, the translator will be switched back to the interpret rules. At the end of a word definition, the net stack effect is tallied and kept in the definition of the word in the wordlist.

{ [ }[ interpret RULES ]
{ ; }[ effect ?STACK ]{ [ }

{ SP! }{ POSTPONE }[ #invalid effect ! ]

The net stack effect may be traced through parallel execution paths and verified when they rejoin. These are the rules for tracing the stack through control structures which have at most two paths. In the case of loops they are only evaluated once.

{ IF     }{ FOR          }[ 1 - DUP                           ]
{ ELSE }[ SWAP ]
{ ENDIF }{ THEN }{ NEXT }[ OVER ]{ REPEAT }
{ BEGIN }[ DUP ]
{ UNTIL }[ 1 - ]{ ENDIF }
{ WHILE }[ 1 - TUCK ]
{ REPEAT }[ XOR IF #invalid effect ! ENDIF ]

The stack effect of ?DUP can not always be extracted from the text since its net stack effect depends on a runtime stack condition. However, when coupled with words which offer separate paths for the different stack effects, the net stack effect is accountable for.

{ ?DUP       }[ #invalid effect ! ]
{ ?DUP IF }[ DUP 1 - SWAP ]
{ ?DUP WHILE }[ 1 - TUCK 1 + ]
{ ?DUP UNTIL }[ TUCK 1 - ]{ REPEAT }

EXIT records the current stack effect. To verify that all exits from a definition have the same stack effect, ?STACK could check the new value against a previously set value. Since EXECUTE doesn't have a compile time stack context available (although it would be simple enough to have a stack comment and a translation rule to translate it), the stack effect is assumed to be #invalid.

{ EXIT    }[ DUP effect ?STACK ]
{ EXECUTE }[ #invalid effect ! ]

Stack rules

A stack comment is assumed to be right after the naming of the word definition. If it is, it is parsed with these rules. Things on the stack are separated by a backslash. Between backslashes a word or a phrase will cause 1 to be added to the stack calculation. When a -- or --- is encountered, it is assumed that the stack calculation up till then is for the number of expected arguments. This number is negated to indicate this.

stack RULES
{ }[ inputq PULL DROP DUP 0= IF 1 + ENDIF ]

{ ( }[ 0 ]
{ -- }{ --- }[ + NEGATE 0 ]
{ \ }[ + 0 ]
{ ) }[ + comment ?STACK colon RULES 0 ]

{ ? }[ #invalid comment ! ]

Tools

These are a few simple tools which may be used to view results and verify rule sequences. TLD has been redefined to allow a rule set to be selected before translation begins.

: .WORD  ( link \ effect \ comment -- )
base @ >R DECIMAL 6 .R 6 .R R> base ! 2 SPACES .NAME
out @ 28 > IF CR ELSE 28 out @ - SPACES ENDIF ;
: LIST ( -- ) ?CR wordlist
BEGIN @ ?DUP WHILE
DUP DUP L>TICK >comment @+ @ .WORD REPEAT ;

: TEST ( -- ) interpret RULES 0 wordlist ! SHOWME ;

: TLD ( -- ) interpret RULES TLD ;

Results

I used the above rules to verify the stack behaviors defined in the botForth kernel (it's entirely written in high level text). Here is a sampling of the output created by LIST.

    -2    -2  +BITS                         -1    -1  C!-  
1 1 C@- -1 -1 C!+
1 1 C@+ -2 -2 C!
0 0 C@ -2 -2 +!
-1 -1 !- 1 1 @-
-1 -1 !+ 1 1 @+
-2 -2 ! 0 0 @
0 0 CELLS 1 1 CELL
-1 -1 * -1 -1 MOD
-1 -1 / 0 0 /MOD
0 0 NEGATE -1 -1 -
-1 -1 + 0 0 U2/
0 0 2/ 0 0 2*
0 0 NOT -1 -1 XOR
-1 -1 OR -1 -1 AND
1 1 DEPTH -32768-32768 SP!
-32768 1 ?DUP -2 -2 2DROP
2 2 2DUP 1 1 TUCK
1 1 OVER -1 -1 NIP
1 1 NUP -1 -1 DROP
1 1 DUP 0 0 SWAP

Part of the output from LIST. The translation rules are from this paper and the input was the botForth kernel. The first number is the net effect calculated from parsing the definition. The second number is the net stack effect calculated from the stack comment. A value of -32768 indicates an #invalid stack.

All the words matched their stack comments except ?DUP. It was written with square brackets around the second stack result to indicate that it was optional. The definition text was correctly parsed and found to be #invalid. To produce the correct stack comment calculation, either the comment would have to be rewritten or the stack rules will have to be augmented.

: ?DUP  ( n -- [n] \ n )  DUP  IF  DUP  ENDIF ;

Definition of ?DUP from the text for the botForth kernel. The colon RULES deduced that the stack was variant at run time. However, since there are no stack RULES for optional stack items, the net stack effect is listed as a gain of 1.

Future

This framework for stack verification is useful as it is but it can be reused to build other translator applications such as: stack optimizing compilers, code verifiers and possibly even code modifiers which might add comments or even correct definitions.


A PDF version of the original paper is also available.