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

我正在尝试确定是否有一种编程方式来检查可能的情况DivideByZeroException在我的代码库中。我的代码库包含一系列相对简单到相对复杂的公式，大约有 1500 个（并且还在不断增加）。编写新公式时，必须注意确保安全地进行除法，以避免在处理这些公式期间出现异常。

E.g.

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（最新）。

第一：以 100% 的准确度静态检测除数为零，这样既不报告可能的缺陷，也不报告不可能的缺陷，这是不可能的。它相当于已知无法解决的停机问题。

因此，我们必须决定是过度近似（有时会出现误报）还是低于近似（有时会出现误报）。这对工具的设计及其可用性特征和性能产生重大影响。

正如另一个答案所指出的，一个简单的启发式是将不在等式测试的结果子节点上的所有除法标记为零。这会有一个enormous误报率。例如考虑：

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

or

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;

它不能被零除，因为如果是的话我们已经返回了。您必须进行流分析来跟踪不同分支上各种表达式的零值。请记住，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 并且有一个可达标签的可达 goto 然后除以 i2。因此，您不应该在这里报告被零除的错误！

这些都是简单的。现在考虑更复杂的场景：

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

此代码不存在被零除错误。您的缺陷检查员会将其标记为有缺陷吗？

为了防止这种误报，您需要的是错误路径检测器理解序列的代数属性：Any() 是一个谓词，可确保 Count() 大于零，等等。

这将是一项繁重的工作，但您将学到很多关于静态分析的知识！