[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

uabelho added a comment. In D112621#4004586 , @steakhal wrote: > Fixed by f61a08b67f5c8b0202dd30821766ee029e880b7c > Yep, thanks! Repository: rG LLVM Github Monorepo CHANGES

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

steakhal added a comment. In D112621#4004409 , @steakhal wrote: > In D112621#4004372 , @uabelho wrote: > >> Hi, >> >> The following starts crashing with this patch: >> >> clang -cc1 -analyze

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

uabelho added a comment. In D112621#4004409 , @steakhal wrote: > In D112621#4004372 , @uabelho wrote: > >> Hi, >> >> The following starts crashing with this patch: >> >> clang -cc1 -analyze

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

steakhal added a comment. In D112621#4004372 , @uabelho wrote: > Hi, > > The following starts crashing with this patch: > > clang -cc1 -analyze -analyzer-checker=core bbi-77010.c > > It crashes with > > bbi-77010.c:6:1: warning: non-void function

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

uabelho added a comment. Hi, The following starts crashing with this patch: clang -cc1 -analyze -analyzer-checker=core bbi-77010.c It crashes with bbi-77010.c:6:1: warning: non-void function does not return a value [-Wreturn-type] } ^ clang:

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

This revision was landed with ongoing or failed builds. This revision was automatically updated to reflect the committed changes. Closed by commit rG77ab7281aa36: [analyzer][solver] Introduce reasoning for not equal to operator (authored by manas, committed by steakhal). Changed prior to commit:

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

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

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas updated this revision to Diff 481545. manas added a comment. Assert over non-empty ranges and add fixme for not handled cases Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 Files:

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas marked 13 inline comments as done. manas added a comment. In D112621#3978285 , @steakhal wrote: > For the test cases where we should be able to prove the case but return > `Unknown` instead, should be marked by a FIXME stating the expected value.

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

steakhal added a comment. For the test cases where we should be able to prove the case but return `Unknown` instead, should be marked by a FIXME stating the expected value. Approximating a concrete value with `Unknown` is (almost) always correct. So, in this case, you don't need to go and fix

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas updated this revision to Diff 480542. manas marked an inline comment as done. manas added a comment. Add more tests for complete coverage Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 Files:

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas marked 2 inline comments as done. manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1624 + if (LHS.isEmpty() || RHS.isEmpty()) +return RangeFactory.getEmptySet(); + steakhal wrote: > This branch is

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

steakhal added a comment. I haven't looked at the implementation. I only checked the tests and something is not quite right there. See my comments inline. BTW the line-coverage is good. I found only two branches which I want to have tests for - see inline. Comment at:

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas updated this revision to Diff 477934. manas added a comment. Fix test cases Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 Files: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas added a comment. In D112621#3949400 , @steakhal wrote: > `Analysis/constant-folding.c` seems to fail. > Please run the `check-clang-analysis` build target to see what fails and > investigate it. @steakhal thank you for reviewing this! I

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

steakhal added a comment. In D112621#3915822 , @manas wrote: > Ping `Analysis/constant-folding.c` seems to fail. Please run the `check-clang-analysis` build target to see what fails and investigate it. Repository: rG LLVM Github Monorepo CHANGES

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas added a comment. Ping Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 ___ cfe-commits mailing list cfe-commits@lists.llvm.org

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas marked 3 inline comments as done. manas added a comment. Thanks @martong and @ASDenysPetrov for the feedback. I utilized `(u != n)` to disallow bifurcation in test cases. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1630-1631 + + RangeSet

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas updated this revision to Diff 463910. manas added a comment. Fix casting to bigger/unsigned type and add tests with multiple ranges in RangeSet Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

ASDenysPetrov added a comment. @manas Ping. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 ___ cfe-commits mailing list cfe-commits@lists.llvm.org

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

ASDenysPetrov added a comment. In D112621#3660256 , @manas wrote: > Is there any other way to formulate the expression so that it constructs `LHS > = [1, 2] U [8, 9]` and doesn't bifurcate? Try this `u1 > 0 && u1 < 10 && u1 != 3 && u1 != 4 && u1 != 5

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

martong added a comment. In D112621#3660256 , @manas wrote: > Considering @ASDenysPetrov 's example of `LHS = [1, 2] U [8, 9]` and `RHS = > [5, 6]`, I constructed a test case as following: > > `(((u1 >= 1 && u1 <= 2) || (u1 >= 8 && u1 <= 9)) && u2 >= 5

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas marked an inline comment as done. manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1272-1273 + // (x != y). + if ((ConvertedLHS.getMaxValue() < ConvertedRHS.getMinValue()) || + (ConvertedLHS.getMinValue() >

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas updated this revision to Diff 445671. manas added a comment. Rebase and fix comments Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 Files:

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas marked 5 inline comments as done. manas added a comment. Considering @ASDenysPetrov 's example of `LHS = [1, 2] U [8, 9]` and `RHS = [5, 6]`, I constructed a test case as following: `(((u1 >= 1 && u1 <= 2) || (u1 >= 8 && u1 <= 9)) && u2 >= 5 && u2 <= 6)` but I can see that the analyzer

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas updated this revision to Diff 445549. manas added a comment. Remove filling gaps and convert, use castTo, and add tests for short-ushort, char-uchar pairs Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

ASDenysPetrov added a comment. @manas I'm sorry but it seems like I brought you a new work :-) I've just loaded these two patches (D129678 and D129498 ) and now you have to rebase your changes. But there is a good news as

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas added a comment. The coverage showing unreachability of `VisitBinaryOperator` for concrete integer cases. F23801808: RangeConstraintManager.cpp.html Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1415-1416 + +

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas updated this revision to Diff 444911. manas added a comment. Add concrete tests for same and different types Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 Files:

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas added a comment. I was busy with other stuff. I will take a look at it now. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 ___ cfe-commits mailing list

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

ASDenysPetrov added a comment. @manas ? Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 ___ cfe-commits mailing list cfe-commits@lists.llvm.org

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

martong added a comment. @manas gentle ping Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 ___ cfe-commits mailing list cfe-commits@lists.llvm.org

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

ASDenysPetrov added a comment. Here are my remarks. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1415-1416 + + Range CoarseLHS = fillGaps(LHS); + Range CoarseRHS = fillGaps(RHS); + Avoid filling the gaps, because it's completely

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas updated this revision to Diff 421134. manas added a comment. Format constant-folding.c Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 Files:

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas updated this revision to Diff 421122. manas added a comment. Fix comments and rebase Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 Files:

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas marked 2 inline comments as done. manas added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1272-1273 + // (x != y). + if ((ConvertedLHS.getMaxValue() < ConvertedRHS.getMinValue()) || + (ConvertedLHS.getMinValue() >

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas added a comment. @steakhal apologies for holding onto this for so long. I managed to fix previously untestable test cases. The issue was that I was building expressions as `(u1 != u2) != 0` and the solver was canonicalizing this to an equivalent `BO_EQ` expression. That's why, it wasn't

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas updated this revision to Diff 420962. manas added a comment. Herald added a project: All. Fix test cases to make them reachable via VisiBinaryOperator and using getConcreteValue() Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

steakhal requested changes to this revision. steakhal added a comment. This revision now requires changes to proceed. In D112621#3160082 , @manas wrote: > I have made few changes: > > 1. The failed assertions due to

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas added a comment. I have made few changes: 1. The failed assertions due to comparison between different types have been fixed by converting all the Ranges to a given type. This will allow comparisons without throwing errors. 2. There was also a build

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas updated this revision to Diff 390526. manas added a comment. Fix comparison between different types and add a test to check it Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D112621/new/ https://reviews.llvm.org/D112621 Files:

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas added a comment. In D112621#3090450 , @steakhal wrote: > It seems like the test does not exercise the modified code segment. > Please investigate, and make sure that the code you submit is actually > exercised by the test you provide. I am really

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

steakhal requested changes to this revision. steakhal added a comment. This revision now requires changes to proceed. It seems like the test does not exercise the modified code segment. Please investigate, and make sure that the code you submit is actually exercised by the test you provide.

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

steakhal added a comment. Please also demonstrate that the patch can deal with sign mismatching ranges. Aside from that, it looks clean and sweet. Although, I still miss the point of how it would bypass anything. Comment at:

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas added a comment. @steakhal @martong This patch solves the comparison between different types by bypassing the RangeSets first to `VisitBinaryOperator` which coarses/converts, and then only it checks for any True/False ranges via comparison. This is similar to what happens with `BO_Rem`,

[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

manas created this revision. Herald added subscribers: steakhal, ASDenysPetrov, martong, dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, szepet, baloghadamsoftware, xazax.hun. Herald added a reviewer: teemperor. manas requested review of this revision. Herald added a project: clang.