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 <[email protected]> wrote:
> Thanks for your comments. Here's a new patch.
>
> //Anders
>
> ________________________________________
> Från: Jordan Rose [[email protected]]
> Skickat: den 19 juni 2014 18:17
> Till: Anders Rönnholm
> Cc: [email protected]; Daniel Marjamäki
> Ämne: Re: [PATCH] Division by zero
>
> On Jun 18, 2014, at 7:30 , Anders Rönnholm <[email protected]>
> 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>
_______________________________________________
cfe-commits mailing list
[email protected]
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
