Is there a Forth static analyzer for stack effects?

Question

I'm losing productivity to programming errors that cause stack overflow.

For instance, if I omit a drop in an IF ELSE THEN branch, inside a loop, and I get a stack overflow, I usually have to reboot my development environment. I'm using SwapForth on the iCEstick.

Does there exist a static analyzer that predicts the stack outcome of a compiled word?

Like an automated tool that checks that the code always matches the (nnn nnn -- f) documentation?

ruvim ruvim · Accepted Answer · 2016-10-29T17:53:15

No such tool is known to me, but why don't we implement it?

In the general case the problem doesn't have a solution (see Rice's theorem and the halting problem). Nevertheless, a practically useful tool obviously can be implemented. It can be a stand-alone tool or extension to your particular Forth system that checks code on the fly during compilation.

As for some example, see Forth Wizard by Peter Sovietov (2003). This tool internally evaluates stack effect of auto-generated code. Another example: Stack Verification paper by Rob Chapman (1997). Also the following papers can be useful: Type Inference in Stack Based Languages, Bill Stoddart and Peter J. Knaggs, 1992 (PDF); Simple Type Inference for Higher-Order Stack-Oriented Languages, Christopher Diggins, 2008 (PDF).

Perhaps the simplest solution is just to dynamically check the stack effect (changing of the depth) and throw an exception when the stack signature is violated (in development versions only). The idea is to redefine : (and possible ;) to obtain stack effect from stack comment and compile EXECUTE-BALANCED wrapper for colon-definitions.

: EXECUTE-EFFECT ( i*x xt -- j*x n )
  DEPTH 1- >R EXECUTE DEPTH R> -
;
: EXECUTE-BALANCED ( i*x xt n -- j*x ) \ j = i + n
  >R EXECUTE-EFFECT R> = IF EXIT THEN
  -5010 THROW \ stack is unbalanced
;

Evidently, such a solution can catch a mistake between words only, and it won't catch a missed DROP inside a loop.

Is there a Forth static analyzer for stack effects?

2 Answers