是否可以使用Rosyln或Resharper来检测可能的DivideByZero案例？

Question

我正在尝试确定是否有一种编程方式来检查DivideByZeroException我的代码库中是否存在可能性.我的代码库包括一系列相对简单到相对复杂的公式,大约1500个(并且正在增长).在编写新公式时,必须注意确保安全地进行除法,以避免在处理这些公式期间出现异常.

例如

decimal val1 = 1.1m;
decimal val2 = 0m;
var res = val1/val2; //bad

var res = val2 == 0 ? 0 : val1/val2; //good

有没有办法使用Roslyn或Resharper或其他工具来检查我的代码库并找出DivideByZeroException未经适当防范的情况？公式基于动态且复杂的数据,足以使用简单的单元测试难以检测.这些公式可以访问数百个输入,并且可以动态地相互构建.

我的环境是:VS2017Pro,Resharper(最新).

Answer 1

第一:静态检测零除以100%的准确度 - 这样既不会报告可能的缺陷也不会报告不可能的缺陷 - 是不可能的.它等同于Halting Problem,它已知不可解决.

因此,我们必须决定是否在过度逼近方面犯错,有时会出现误报或低估,有时还会有错误的否定报告.这对工具的设计及其可用性特征和性能有重大影响.

正如另一个答案所指出的,一个简单的启发式方法是将不在相等测试的结果子节点上的所有分区标记为零.这将产生巨大的误报率.考虑例如:

var res = val2 == 0 ? 0 : val1 / val2;

要么

var res = val2 != 0 ? val1 / val2 : 0;

这些可能被正确标记为否定.但是关于

int? res = val2 > 10 ? (int?) (val1 / val2) : null;

那里没有可能被零除.但是提议的测试不会捕获它,并且会错误地将它们归类为正面.

这样的事情怎么样？

int i1 = whatever;
int i2 = whatever;
int i3 = whatever;
int i4 = i1 > 0 && i2 > 0 ? i3 / (i1 + i2) : 0;

首先:我们可以假设总和不会溢出到零吗？ 在设计检查器时,这是一个非常重要的问题.通常我们会做出保守的假设,即这些值足够小,不会溢出.但是现在我们还有另一个问题:你的程序是否足够聪明才能理解两个正整数之和永远不为零？

为了静态地表示这些类型的计算,您可能必须使用算术模型构建SMT求解器.

您还需要一个流检查器:

int i1 = whatever;
int i2 = whatever;
if (i2 == 0) return;
int i3 = i1 / i2;

这不能除以零,因为如果是的话我们已经回来了.您将不得不进行流分析,以跟踪不同分支上各种表达式的zeroness.请记住,C#中的流分析可能非常奇怪:

int i1 = whatever;
int i2 = whatever;
if (i2 != 0)
  goto X;
try {
  Debug.Assert(i2 == 0);
  goto X;
}
finally {
  throw something;
}
X:
int i3 = i1 / i2;

这段代码非常奇怪和愚蠢,但它不包含除零错误,即使我们在可到达的代码路径上为i2分配零,并且可达到的可转换标签然后除以i2.因此,您不应该在此报告零除错误!

这些都很简单.现在考虑更复杂的场景:

static int Mean(IEnumerable<int> items) => 
  items.Any() ? items.Sum() / items.Count() : 0;

此代码没有除零错误.您的缺陷检查器会将其标记为有缺陷吗？

为了防止这种误报,你需要的是一个理解序列代数属性的错误路径检测器:Any()是一个谓词,它确保Count()大于零,依此类推.

这将是很多工作,但你会学到很多关于静态分析的知识!

Answer 2

您可以创建一个检查所有内容的分析器DivideExpression，如果它不是EqualsExpression带有 an的子节点NumericLiteralExpression，则分析器应为此添加一个应用代码修复的诊断。