SV: [PATCH] Division by zero

[Anders Rönnholm]

Hi,

New iteration with comments addressed.

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)"?

Sorry, thought I still had to loop, I have removed it now.


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?

Yes it looks kinda strange. I have changed it slightly to more resemble how DivZeroChecker does it.

//Anders

On Jun 24, 2014, at 6:29 , Anders Rönnholm <Anders.Ronnholm at evidente.se<mailto: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<mailto:jordan_rose at apple.com>]
Skickat: den 19 juni 2014 18:17
Till: Anders Rönnholm
Cc: cfe-commits at cs.uiuc.edu<mailto: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<mailto: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 --------------
A non-text attachment was scrubbed...
Name: divzero2.diff
Type: text/x-patch
Size: 18490 bytes
Desc: divzero2.diff
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20140702/7a3b77cf/attachment.bin>