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

Question

由于导致堆栈溢出的编程错误，我正在失去工作效率。

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

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

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

Answer 1

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

在一般情况下，问题没有解决方案(参见 Rice's theorem 和 halting problem)。然而，显然可以实现一个实际有用的工具。它可以是一个独立的工具，也可以是您特定 Forth 系统的扩展，用于在编译期间即时检查代码。

关于一些例子，参见Forth Wizard彼得·苏维埃托夫 (2003)。该工具在内部评估自动生成代码的堆栈效果。另一个例子:Stack Verification Rob Chapman (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。