george.karpenkov added inline comments.
================ Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:597 + // than or equal to the quarter of the maximum value of that type. + bool shouldAggressivelySimplifyRelationalComparison(); + ---------------- High level comment: can you list all [[ https://en.wikipedia.org/wiki/Rewriting | rewriting ]] rules you are applying in a formula explicitly in a comment? From the phabricator discussion I see that you are applying ``` A + n >= B + m -> A - B >= n + m // A, B symbolic, n and m are integers ``` but from the code it seems that you are applying more canonicalization rules? ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:317 +// with simpler symbols on every recursive call. +static bool isOverflowClampedBy4(SymbolRef Sym, ProgramStateRef State) { + SValBuilder &SVB = State->getStateManager().getSValBuilder(); ---------------- Can we have a better function name here? I can't think of one straight away, but "clamped" is not very self-descriptive. `isWithinConstantOverflowBounds`? ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:326 + + llvm::APSInt Max = AT.getMaxValue() >> 2; // Divide by 4. + SVal IsCappedFromAbove = ---------------- Would just division produce the same result? Also probably it's better to make "4" a constant, at least with `#define` ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:330 + nonloc::ConcreteInt(Max), SVB.getConditionType()); + if (auto DV = IsCappedFromAbove.getAs<DefinedSVal>()) { + if (State->assume(*DV, false)) ---------------- 6 lines of branching is probably better expressed as ``` if (!isa<DefinedSVal>(IsCappedFromAbove) || State->assume(*dyn_cast<DefinedSVal>(IsCappedFromAbove), false)) return false ``` ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:337 + + llvm::APSInt Min = -Max; + SVal IsCappedFromBelow = ---------------- 326-335 duplicates 338-346. Perhaps we could have ``` static bool isCappedFrom(bool Above, llvm::APSInt bound, ...) ``` ? ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:352 +// Same for the concrete integers: see if I is within [min/4, max/4]. +static bool isOverflowClampedBy4(llvm::APSInt I) { + APSIntType AT(I); ---------------- Again, could we do better with a function name? ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:357 + + llvm::APSInt Max = AT.getMaxValue() >> 2; + if (I > Max) ---------------- I think you want ``` return (I <= Max) && (I >= -Max) ``` instead of 358-365 ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:376 + // Fail to decompose: "reduce" the problem to the "$x + 0" case. + return std::make_tuple(Sym, BO_Add, BV.getValue(0, Sym->getType())); +} ---------------- Is it beneficial to do this though? At the point where `decomposeSymbol` is called we are still checking whether the rearrangement could be performed, so maybe just returning a false flag would be better? ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:403 + if (LOp == BO_Sub) + LInt = -LInt; + else ---------------- I think this is a separate rewrite, which is better performed in a separate function. If you move it to `decomposeSymbol` or to a separate function, you would get a lot of simplifications: 1. This function would be performing only a single rewrite. 2. You would no longer need to take `Lop` and `Rop` as parameters 3. At that point, two separate cases would be clearly seen: `Op` is a comparison operator, or `Op` is an additive operator. I would separate those two rewrites in separate functions, distinguishing between them at the callsite. ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:429 + if (BinaryOperator::isComparisonOp(Op)) { + // Prefer comparing to a non-negative number. + // FIXME: Maybe it'd be better to have consistency in ---------------- It seems that having a concrete positive RHS is a part of your rewrite rule. In that case, that should be documented in a high-level overview of the rewrite rules. ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:432 + // "$x - $y" vs. "$y - $x" because those are solver's keys. + if (LInt > RInt) { + ResultSym = SymMgr.getSymSymExpr(RSym, BO_Sub, LSym, SymTy); ---------------- I think this could be shortened and made more explicit by constructing the LHS and RHS first, and then reversing both and the comparison operator if RHS is negative. ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:472 + if (BinaryOperator::isComparisonOp(Op) && + Opts.shouldAggressivelySimplifyRelationalComparison()) { + if (ResultTy != SVB.getConditionType()) ---------------- I am confused why the option `shouldAggressivelySimplifyRelationalComparison` is checked here. Do we rewrite cases where `Op` is additive even if the option is not checked? It's generally better to check the flag outside of the rearranging function, so that the high-level logic can be seen. ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:489 + if (SingleTy != ResultTy) + return None; + } else { ---------------- This check is weird: you have just set `SingleTy` to `ResultTy` at line 477. Instead of this whole if-block (from line 487), why not just set `SingleTy` above line 473. where you have already checked that the operator is performing comparison? ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:494 + + assert(!SingleTy.isNull() && "We should have figured out the type by now!"); + ---------------- I would also move this assert up, below line 481. ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:497 + // Substracting unsigned integers is a nightmare. + if (!SingleTy->isSignedIntegerOrEnumerationType()) + return None; ---------------- this check should be inside the block at line 477, since it does not make sense for relational comparisons. ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:508 + std::tie(LSym, LOp, LInt) = decomposeSymbol(LSym, BV); + if (LSym->getType() != SingleTy || + !isOverflowClampedBy4(LSym, State) || !isOverflowClampedBy4(LInt)) ---------------- Why `isComparisonOp()` check is done in 512-516, but not here? Additionally, can this check be factored out into a function? ================ Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:774 + if (Optional<NonLoc> V = tryRearrange(state, op, lhs, rhs, resultTy)) + return *V; ---------------- I would expect that checking the analyzer option would be performed here? ================ Comment at: test/Analysis/svalbuilder-rearrange-comparisons.c:19 + if (x < -(((int)INT_MAX) / 4)) + exit(1); + return x; ---------------- assert would express intent better ================ Comment at: test/Analysis/svalbuilder-rearrange-comparisons.c:28 + clang_analyzer_dump(x == y); + // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 0}} +} ---------------- Can we also have integration-like tests where rearrangement would affect observable behavior? Also, `clang_analyzer_dump` is a debugging function, and I am not sure whether we should rely on its output in tests. https://reviews.llvm.org/D41938 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
