[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

ASDenysPetrov added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1618-1627 +const SymbolRef LHS = Sym->getLHS(); +const llvm::APSInt = +Builder.getBasicValueFactory().getValue(0, Sym->getType()); +// a % b != 0

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong marked 6 inline comments as done. martong added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1619-1620 +const SymbolRef LHS = Sym->getLHS(); +const llvm::APSInt = +Builder.getBasicValueFactory().getValue(0,

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

ASDenysPetrov added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1618-1627 +const SymbolRef LHS = Sym->getLHS(); +const llvm::APSInt = +Builder.getBasicValueFactory().getValue(0, Sym->getType()); +// a % b != 0

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

This revision was landed with ongoing or failed builds. This revision was automatically updated to reflect the committed changes. martong marked an inline comment as done. Closed by commit rG5f8dca023504: [Analyzer] Extend ConstraintAssignor to handle remainder op (authored by martong).

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong marked an inline comment as done. martong added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1618-1627 +const SymbolRef LHS = Sym->getLHS(); +const llvm::APSInt = +Builder.getBasicValueFactory().getValue(0,

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

ASDenysPetrov added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1618-1627 +const SymbolRef LHS = Sym->getLHS(); +const llvm::APSInt = +Builder.getBasicValueFactory().getValue(0, Sym->getType()); +// a % b != 0

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

steakhal accepted this revision. steakhal added a comment. I see. Now it looks correct. Next time we shall have a z3 proof about the theory. `A => B` <=> `not(A) or B`. which is SAT only if `A and not(B)` UNSAT. a = z3.BitVec('a', 32) b = z3.BitVec('b', 32) zero = z3.BitVecVal(0, 32) s

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong updated this revision to Diff 379988. martong added a comment. - Remove the wrong inferrence of `a % b == 0 implies that a == 0` and related test cases. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D110357/new/

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong added a comment. After taking a look at the new findings we discovered, there is a logic error with this patch, actually `a % b == 0 implies that a == 0` does not hold, one counter example is `10 % 2 == 0`. Argh, probably we should be using Z3 next time to prove or disprove such

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

steakhal added a comment. Additionally to my previous observation, a surprising amount of the new findings are of `deadcode` detections, and most of them there are loops. Other than that, I've seen a true-positive report as well: F19624854: image.png At line

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

steakhal accepted this revision. steakhal added a comment. In D110357#3066207 , @ASDenysPetrov wrote: > Ok. Let's see what the benefits it brings. According to our measurements, it has some effects but is probably difficult to draw clear conclusions.

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

ASDenysPetrov added a comment. Ok. Let's see what the benefits it brings. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1619 + return true; +const SymExpr *LHS = Sym->getLHS(); +const llvm::APSInt = steakhal wrote: >

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong updated this revision to Diff 379830. martong added a comment. - Fix signedness mismatch assertaion and add a test case for that Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D110357/new/ https://reviews.llvm.org/D110357 Files:

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

steakhal accepted this revision. steakhal added a comment. This revision is now accepted and ready to land. Excellent! All lines are covered. Great job. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1619 + return true; +const SymExpr *LHS =

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong updated this revision to Diff 379189. martong marked 3 inline comments as done. martong added a comment. - Fix logic error - Add more test cases - Use SymbolRef Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D110357/new/

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong marked 5 inline comments as done. martong added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1619 + return true; +const SymExpr *LHS = Sym->getLHS(); +const llvm::APSInt = ASDenysPetrov wrote: >

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

ASDenysPetrov added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1619 + return true; +const SymExpr *LHS = Sym->getLHS(); +const llvm::APSInt = steakhal wrote: > Since `SymbolRef` actually is already

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

steakhal added a comment. BWT the following lines are uncovered by tests: L1627, L1651, L1758 Please adjust your tests accordingly. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D110357/new/ https://reviews.llvm.org/D110357

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

steakhal added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1619 + return true; +const SymExpr *LHS = Sym->getLHS(); +const llvm::APSInt = Comment at:

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

ASDenysPetrov added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1609-1612 + const SymExpr *LHS = Sym->getLHS(); + const llvm::APSInt = + Builder.getBasicValueFactory().getValue(0, LHS->getType()); + State =

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1603-1604 + template + bool handleRem(const SymT *Sym, RangeSet Constraint) { +// a % b != 0 implies that a != 0. ASDenysPetrov wrote: > steakhal wrote:

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong updated this revision to Diff 379039. martong marked 11 inline comments as done. martong added a comment. - Handle a % b == 0 implies that a == 0. - Add more test cases Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D110357/new/

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong updated this revision to Diff 379017. martong added a comment. - Rebase on top of new Parent (Use ) Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D110357/new/ https://reviews.llvm.org/D110357 Files:

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

steakhal added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1609-1612 + const SymExpr *LHS = Sym->getLHS(); + const llvm::APSInt = + Builder.getBasicValueFactory().getValue(0, LHS->getType()); + State =

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

ASDenysPetrov added inline comments. Comment at: clang/test/Analysis/constraint-assignor.c:18 + clang_analyzer_warnIfReached(); // no-warning + (void)x; // keep the constraints alive. +} steakhal wrote: > It's still mindboggling that we need to do this. This

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

ASDenysPetrov added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1603-1604 + template + bool handleRem(const SymT *Sym, RangeSet Constraint) { +// a % b != 0 implies that a != 0. steakhal wrote: > Why is this not

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

steakhal added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1591-1595 template LLVM_NODISCARD static ProgramStateRef - assign(ProgramStateRef State, SValBuilder , RangeSet::Factory , - ClassOrSymbol CoS, RangeSet

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

steakhal added a comment. Great work! Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1591-1595 template LLVM_NODISCARD static ProgramStateRef - assign(ProgramStateRef State, SValBuilder , RangeSet::Factory , - ClassOrSymbol CoS, RangeSet

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong updated this revision to Diff 374741. martong added a comment. - Break out the movement of RangeConstraintManager into a parent patch, this way the diff here is clearly visible and makes the review easier. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong added a comment. I had to move the definition of `ConstraintAssignor` after the definition of `RangeConstraintManager` b/c I am using `assumeSymNE` in the new logic. Unfortunately, the diff does not show clearly the changes inside the moved hunk, so I try to indicate the important

[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

martong created this revision. martong added reviewers: NoQ, vsavchenko, steakhal, Szelethus, ASDenysPetrov. Herald added subscribers: manas, gamesh411, dkrupp, donat.nagy, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun, whisperity. martong requested review of this