[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

This revision was automatically updated to reflect the committed changes. Closed by commit rG73c120a9895a: [analyzer] Introduce reasoning about symbolic remainder operator (authored by vsavchenko). Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko updated this revision to Diff 266890. vsavchenko added a comment. Fix code review remarks Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D80117/new/ https://reviews.llvm.org/D80117 Files:

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

NoQ added a comment. In D80117#2059567 , @NoQ wrote: > > I believe that as of now we can submit these modifications as is and > > explore performance optimizations later if needed. > > I still encourage you to explore the tests we have from our previous

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko marked an inline comment as done. vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:506-507 + /// + /// where abs(Origin) is the maximal absolute value of any possible values + /// from Origin, and min(T)

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

NoQ accepted this revision. NoQ added a comment. This revision is now accepted and ready to land. Aha, so performance regressions on real code weren't real, that's a relief :) > I believe that as of now we can submit these modifications as is and explore > performance optimizations later if

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko added a comment. Performance-wise, I've investigated huge slowdowns on `tmux` and `pytorch`. - `pytorch` build produces a lot of warnings and simply trashed my terminal. I guess one time it had more troubles with displaying all that than the other. Here is a table with new times:

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko marked an inline comment as done. vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:459-469 +if (Origin.From().isMinSignedValue()) { + // If mini is a minimal signed value, absolute value of it is greater +

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko updated this revision to Diff 266586. vsavchenko added a comment. Fix code review remarks Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D80117/new/ https://reviews.llvm.org/D80117 Files:

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko marked 5 inline comments as done. vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:459-469 +if (Origin.From().isMinSignedValue()) { + // If mini is a minimal signed value, absolute value of it is greater +

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko updated this revision to Diff 266551. vsavchenko added a comment. Move 0 % x case to SValBuilder Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D80117/new/ https://reviews.llvm.org/D80117 Files:

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

ASDenysPetrov added a comment. @vsavchenko I've made some assumptions. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:459-469 +if (Origin.From().isMinSignedValue()) { + // If mini is a minimal signed value, absolute value of it is greater +

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

xazax.hun added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:633 + + // Check if LHS is 0. It's a special case when the result is guaranteed + // to be 0 no matter what RHS is (we put to the side the case when RHS is I

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko updated this revision to Diff 264863. vsavchenko added a comment. Fix code review remarks. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D80117/new/ https://reviews.llvm.org/D80117 Files:

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko marked an inline comment as done. vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:462 +if (CoversTheWholeType) { + return {ValueFactory.getMinValue(RangeType), +

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

NoQ added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:459 +bool CoversTheWholeType = +(Origin.From().isMinSignedValue() || Origin.To().isMaxValue()); + vsavchenko wrote: > NoQ wrote: > > `(Origin.From() +

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

NoQ added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:462 +if (CoversTheWholeType) { + return {ValueFactory.getMinValue(RangeType), + ValueFactory.getMaxValue(RangeType)}; vsavchenko wrote: > NoQ

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko marked 2 inline comments as done. vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:459 +bool CoversTheWholeType = +(Origin.From().isMinSignedValue() || Origin.To().isMaxValue()); + NoQ

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

NoQ added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:459 +bool CoversTheWholeType = +(Origin.From().isMinSignedValue() || Origin.To().isMaxValue()); + `(Origin.From() + 1).isMinSignedValue()` is another

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko added a comment. Here is a short summary of the performance testing I conducted across a bunch of open-source projects: | | vim | git | tmux| redis

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko updated this revision to Diff 264605. vsavchenko added a comment. Rebase Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D80117/new/ https://reviews.llvm.org/D80117 Files: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko added a comment. Here is a proof in Z3: https://gist.github.com/SavchenkoValeriy/559ca923b050f2c01e340c1be543b7e0 Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D80117/new/ https://reviews.llvm.org/D80117

[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

vsavchenko created this revision. vsavchenko added reviewers: NoQ, dcoughlin, xazax.hun, ASDenysPetrov. Herald added subscribers: cfe-commits, martong, Charusso, dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware. Herald added a project: clang. New