[PATCH] Division by zero

[Jordan Rose]

I still don't understand why this is a loop at all:

+bool TestAfterDivZeroChecker::isZero(SVal S, CheckerContext &C) const {
+  Optional<Loc> L;
+  if (!(L = S.getAs<Loc>())) return false;
+
+  const ExplodedNode *N = C.getPredecessor();
+  while (N) {
+    ProgramStateRef State = N->getState();
+
+    // Find the most recent expression bound to the symbol in the current
+    // context.
+    SVal Val = State->getRawSVal(L.getValue());
+    if (Val == S) {
+      Optional<DefinedSVal> DSV = Val.getAs<DefinedSVal>();
+      return !C.getConstraintManager().assume(State, *DSV, false);
+    }
+    N = N->pred_empty() ? nullptr : *(N->pred_begin());
+  }
+  return false;
+}

What's wrong with "Val = C.getState()->getRawSVal(*L)"?

Also, I'm reading your check as saying that the value is zero if there does not exist a state where DSV is not non-zero. I must be reading something wrong (since you have test cases), but what? Can you explain it to me?

Smaller comments:

+  Optional<Loc> L;
+  if (!(L = S.getAs<Loc>())) return false;

I personally think this is clearer if you put the assignment in with the declaration.

+  DivZeroMapTy DivZeroes = State->get<DivZeroMap>();
+  if (DivZeroes.isEmpty())
+    return;
+
+  for (llvm::ImmutableSet<ZeroState>::iterator I = DivZeroes.begin(),
+                                               E = DivZeroes.end();
+       I != E; ++I) {
+    ZeroState ZS = *I;
+    if (ZS.getStackFrameContext() == C.getStackFrame())
+      State = State->remove<DivZeroMap>(ZS);
+  }
+  C.addTransition(State);

I should have mentioned this sooner, but it's more efficient if you use the map factory to remove everything first and then generate one new state with the final map. See MallocChecker::checkDeadSymbols for an example of how to do this (they're using it for RegionState).

Jordan


On Jun 24, 2014, at 6:29 , Anders Rönnholm <Anders.Ronnholm at evidente.se> wrote:

> Thanks for your comments. Here's a new patch.
> 
> //Anders
> 
> ________________________________________
> Från: Jordan Rose [jordan_rose at apple.com]
> Skickat: den 19 juni 2014 18:17
> Till: Anders Rönnholm
> Cc: cfe-commits at cs.uiuc.edu; Daniel Marjamäki
> Ämne: Re: [PATCH] Division by zero
> 
> 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
> <divzero2.diff>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20140701/5e5f4f5c/attachment.html>