Is it possible to use Rosyln or Resharper to detect possible DivideByZero cases?

Question

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.

E.g.

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

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

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.

My environment is: VS2017Pro, Resharper (latest).

Answer 1

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;

or

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.

What about something like this?

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?

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;

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;

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?

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!

Answer 2

You can create an analyzer that checks all DivideExpression and if it's NOT a subnode of an EqualsExpression with an NumericLiteralExpression, the analyzer should add a diagnostic for this which applies the codefix.