是否可以使用 Rosyln 或 Resharper 来检测可能的 DivideByZero 案例? [英] Is it possible to use Rosyln or Resharper to detect possible DivideByZero cases?

问题描述

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

I'm trying to determine if there's a programmatic way to check for possible DivideByZeroException in my codebase. My codebase includes a series of relatively simple to relatively complex formulas, approximately 1500 of them (and growing). When new formulas are written, care must be taken to ensure that division is done safely to avoid exceptions during processing of these formulas.

例如

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

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

有什么方法可以使用 Roslyn 或 Resharper 或其他工具来检查我的代码库并识别 DivideByZeroException 没有得到适当防范的情况?这些公式基于动态且足够复杂的数据，因此使用简单的单元测试很难检测到这一点.这些公式可以访问数百个输入，并且可以动态地相互构建.

Is there any way to use Roslyn or Resharper, or other tools to inspect my codebase and identify cases where DivideByZeroException has not been properly guarded against? The formulas are based off of data that is dynamic and complex enough to make this difficult to detect using simple unit tests. The formulas have access to hundreds of inputs, and can build upon each other dynamically.

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

My environment is: VS2017Pro, Resharper (latest).

推荐答案

第一:以 100% 的准确度静态检测除以零 - 这样您既不会不报告可能的缺陷，也不会报告不可能的缺陷 - 是不可能的.它等价于停机问题，已知它是不可解的.

First: statically detecting divisions by zero with 100% accuracy -- so that you neither fail to report possible defects nor report impossible defects -- is impossible. It's equivalent to the Halting Problem, which is known to be not solvable.

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

Therefore we must decide whether to err on the side of over-approximating, and sometimes having false positive reports, or under-approximating, and sometimes having false negative reports. This has a major impact upon the design of the tool and its usability characteristics and performance.

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

As another answer noted, a simple heuristic is to flag all divisions that are not on the consequence subnode of an equality test for zero. This would have an enormous false positive rate. Consider for example:

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

或

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

这些可能会被正确标记为否定.但是呢

These would presumably be correctly flagged as a negative. But what about

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

那里不可能被零除.但是提议的测试不会发现它，并且会将这些错误地归类为阳性.

There's no possibility of division by zero there. But the proposed test wouldn't catch it, and would falsely categorize these as positives.

这样的事情怎么样?

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

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

First: can we assume that the sum does not ever overflow to zero? This is a really important question when designing your checker. Typically we would make the conservative assumption that the values are small enough to not overflow. But now we have another problem: is your program smart enough to understand that the sum of two positive integers is never zero?

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

In order to represent these sorts of computations statically you will probably have to build an SMT solver with a model for arithmetic.

您还需要一个流量检查器:

You'll also need a flow checker:

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

不能除以零，因为我们已经返回了.您必须进行流分析来跟踪不同分支上各种表达式的零度.请记住，C# 中的流分析可能非常奇怪:

That cannot divide by zero because we've already returned if it was. You'll have to do a flow analysis that tracks zeroness of various expressions on different branches. Keep in mind that flow analysis in C# can be super weird:

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.因此，您不应在此处报告除以零错误！

This code is really weird and dumb, but it does not contain a divide by zero error, even though we assign zero to i2 on a reachable code path and have a reachable goto to a reachable label that then divides by i2. Thus you should not be reporting a divide by zero error here!

那些是容易的.现在考虑更复杂的场景:

Those are the easy ones. Now consider more complex scenarios:

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

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

This code does not have a division by zero error. Would your defect checker flag it as having one?

为了防止这种误报，您需要一个假路径检测器，它可以理解序列的代数特性:Any() 是一个谓词，它确保 Count() 大于零，并且以此类推.

To prevent this false positive, what you need is a false path detector that understands algebraic properties of sequences: that Any() is a predicate which ensures that Count() is greater than zero, and so on.

这将是大量的工作，但是您将学到很多关于静态分析的知识！

This will be a lot of work, but you will learn a lot about static analysis doing it!

这篇关于是否可以使用 Rosyln 或 Resharper 来检测可能的 DivideByZero 案例?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！