[PATCH] Division by zero

[Jordan Rose]

On Jun 18, 2014, at 7:30 , Anders Rönnholm <Anders.Ronnholm at evidente.se> wrote:

> Changes according to comments. 
> 
> I'm pretty sure PVS-Studio does not have this checker, this bug has been seen in production code.


Oops, noticing more things:

+  const ExplodedNode *N = C.getPredecessor();
+  while (N) {
+    ProgramStateRef State = N->getState();
+
+    // Find the most recent expression bound to the symbol in the current
+    // context.
+    if (const MemRegion *MR = C.getLocationRegionIfPostStore(N)) {
+      SVal Val = State->getSVal(MR);
+      if (Val == S) {
+        Optional<DefinedSVal> DSV = Val.getAs<DefinedSVal>();
+        if (!C.getConstraintManager().assume(State, *DSV, false))
+          return true;
+      }
+    }
+    N = N->pred_empty() ? nullptr : *(N->pred_begin());
+  }

Why are you looking for the last time a value was stored rather than just asking for the value in the current state?

if (Optional<Loc> L = S.getAs<Loc>()) {
  SVal V = State->getSVal(L) // or getRawSVal if you don't want a symbol constrained to 0 to be simplified to 0.
  // ...


+    if (Optional<KnownSVal> V = Val.getAs<KnownSVal>()) {

Because you needed a symbol already to get this far, you can skip this step. Or assert it.


+void TestAfterDivZeroChecker::checkPreStmt(const BinaryOperator *B,
+                                   CheckerContext &C) const {

Strange alignment here. If the second line doesn't fit, just indent it twice from the start of the function...don't try to right-align it.


+    if (!B->getRHS()->getType()->isScalarType())
+      return;

Dividing by a floating-point 0 is well-defined, so this should be a more specific check.

Jordan