C#静态分析,变量/参数的可能值

Question

在类似于以下每个示例的代码中,我希望能够静态分析代码以确定传递给SpecialFunction()的可能值列表.

SpecialFunction(5); // A

int x = 5;
SpecialFunction(x); // B

int x = 5;
x = condition ? 3 : 19;
SpecialFunction(x); // C

我已经可以将C#解析成一个抽象语法树了,我已经可以处理像A这样的情况了,我想我可以跟踪值的初始赋值来猜测案例B,但像C一样简单的情况似乎很快就会变得复杂.

我几乎可以肯定,我们无法在所有情况下静态地解决x问题,这没关系.我想知道尝试它的策略,以及识别何时无法完成的方法.如果我们需要包含类级别字段和多线程,该怎么办？闭包？它是否有助于如果我们知道,集合X了所有可能的值x,|X| < 50？

从@Vladimir Perevalov的建议来看,Pex中的概念如何应用于寻找目标代码点的可能值(而不是Pex似乎做的是发现代码路径和值导致未检查(？)异常情况)？

Answer 1

您想要的是全局数据流分析（“什么值分配/副作用达到什么使用点”）[这需要控制流分析作为前身]和某种范围分析（“总结可以达到的值集”）一个点”）。

计算数据流需要拥有完整的 C# 前端、本地控制和数据流分析，然后将这些答案拼接到全局数据流分析中。

范围分析要求您首先定义打算如何对可能值集进行编码；允许什么规格系统？最简单的，只是一组值，往往会爆炸。中间规范方案类似于 OP 的单关系到常量，例如 "x < 50" 。任何此类有限方案的问题在于，值集的丰富性可能会导致您得到无用的答案，特别是如果还有其他感兴趣的谓词（如果 x 始终为奇数，则单关系到常数只能对此建模因为“x <无穷大”这显然没有帮助。因此，您想要选择一个足够复杂的规范方案来对您感兴趣的各种值进行建模。但是，随着您的规范方案变得更加复杂，推断这些事实的机制正确地变得更加复杂，所以你不能让它变得太复杂。

大多数可用的分析工具都没有这样的分析，更不用说向你展示了。PEX可能确实有这样的机器；如果你幸运的话，它也会暴露出来。

我们的DMS 软件重组工具包具有通用解析、符号表构建、控制/数据流分析，甚至范围分析机制（规范：x < k1*a+k2*b，其中 k1 和 k2 是常量，a 和 b 是其他程序变量x 被消耗的地方可见）。DMS 具有 C#、Java、GNU C 和 COBOL 前端，实际上，我们通过收集（静态分析！）特定于这些语言的事实并提供这些语言，为 GNU C 和 IBM Enterprise COBOL（部分为 Java 7）实例化了该机器。通用机械的事实。我们还没有为 C# 实例化这个机制。但如果您无法从其他来源获得好的答案，那么这可能已经非常接近了。