是否有用于堆栈效果的 Forth 静态分析器？

Question

我正在因导致堆栈溢出的编程错误而失去生产力。

例如，如果我drop在一个IF ELSE THEN分支中、一个循环中省略 a并且出现堆栈溢出，我通常必须重新启动我的开发环境。我在iCEstick上使用SwapForth。

是否存在预测编译字堆栈结果的静态分析器？

像检查代码是否始终与 ( nnn nnn -- f ) 文档匹配的自动化工具？

Answer 1

我不知道这样的工具，但我们为什么不实施它呢？

在一般情况下，问题没有解决方案（参见莱斯定理和停机问题）。尽管如此，显然可以实现一个实用的工具。它可以是一个独立的工具，也可以是您特定 Forth 系统的扩展，可以在编译期间即时检查代码。

举个例子，请参阅彼得苏维埃托夫的Forth Wizard (2003)。该工具在内部评估自动生成代码的堆栈效果。另一个例子：Rob Chapman 的Stack Verification论文 (1997)。以下论文也很有用：基于堆栈的语言中的类型推断，Bill Stoddart 和 Peter J. Knaggs，1992 ( PDF )；高阶面向堆栈语言的简单类型推断，Christopher Diggins，2008 ( PDF )。

也许最简单的解决方案是动态检查堆栈效果（改变深度）并在违反堆栈签名时抛出异常（仅在开发版本中）。这个想法是重新定义:（和可能的;）以从堆栈注释中获得堆栈效果并编译EXECUTE-BALANCED冒号定义的包装器。

: 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
;

显然，这样的解决方案只能捕捉单词之间的错误，而不会捕捉DROP循环中的遗漏。