testing - 在没有模型检查的情况下实现符号执行

Question

我如何在不使用和例如的情况下实现symbolic executionfor ？我需要有关它的详细信息。例如，我可以通过什么语言来实现这个符号执行以及我需要知道的其他事情？particular languagemodel checkingFinite State Machine (FSM)notJava Path Finder

Answer 1

你需要：

• 用于符号执行语言的解析器，可以构建 AST
• 名称解析（和关联的符号表），因此当您的执行引擎遇到标识符时，它可以确定关联的类型和值
• 控制流分析，使符号执行引擎可以通过程序跟踪控制流
• 可以组合和简化符号项的符号代数。这需要一个解析器（这样你就可以输入这样的方程）和漂亮的打印机（这样你就可以看到它计算了什么）
• 一种在符号执行开始时指定假定值的方法

这是相当多的机器，很难在一个地方找到它们。只为一个工具构建它更难，这也是你找不到很多这样的工具的部分原因。

我们的DMS 软件再造工具包具备所有必要条件。您可能会发现使用 DMS 实现的符号语言的示例很有趣。