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

Question

由于编程错误导致堆栈溢出，我正在失去生产力。

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

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

像一个自动工具，检查代码总是匹配(nnn nnn——f)文档?

Answer 1

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

在一般情况下，问题没有解(参见Rice定理和停止问题)。然而，一个实际有用的工具显然是可以实现的。它可以是一个独立的工具，也可以是您的特定Forth系统的扩展，在编译过程中动态检查代码。

关于一些例子，请参阅Peter苏维埃托夫(2003)的Forth Wizard。此工具在内部评估自动生成代码的堆栈效果。另一个例子: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。

Answer 2

分析程序需要知道所使用的所有单词的堆栈效果，而不仅仅是标准单词。在实践中，这意味着必须以某种方式记录所有存在的单词的堆栈效应。我已经代表一个优化器做了这个，所以它是可以做到的。我没有自动将其与规范进行比较。这将需要形式化的规范，就像你提出的(nnn nnn - f)，以及一种指定不确定堆栈效应的方法。

一个折衷的解决方案是使用堆栈效果颜色编码，使堆栈错误突出。它使用ciforth实现中存储在标志字段中的堆栈效果规范。https://home.hccnet.nl/a.w.m.van.der.horst/forthlectureE.html

经验丰富的Forthers对此不以为然。单词必须在创建后立即进行测试，这使得堆栈错误的寿命很短。