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

[Manas Gupta via Phabricator via cfe-commits]

manas added a comment.

The coverage showing unreachability of `VisitBinaryOperator<BO_NE>` for concrete integer cases. F23801808: RangeConstraintManager.cpp.html <https://reviews.llvm.org/F23801808>



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1415-1416
+
+  Range CoarseLHS = fillGaps(LHS);
+  Range CoarseRHS = fillGaps(RHS);
+
----------------
ASDenysPetrov wrote:
> Avoid filling the gaps, because it's completely possible to compare all the ranges.
> E.g. //LHS //`[1,2]U[8,9]`  and  //RHS //`[5,6]` are not equal.
> And you don't need to fiil the gap in LHS, because it will lead you to a wrong answer, like `[1,9] != [5,6]` => **UNKNOWN** instead of **TRUE**.
If we don't fill gaps, then we will be making this method O(n) instead of O(1) as of now. As I see it, filling RHS (and not filling LHS), it can iterate over all ranges in LHS, and check each range's intersection with CoarseRHS.

Before, I do this, I just wanted to point out the unreachability of concrete cases to this method. I have tried to explain this below.


================
Comment at: clang/test/Analysis/constant-folding.c:339
+  }
+}
----------------
ASDenysPetrov wrote:
> I'd like to see the cases with concrete integers as well.
I have checked the coverage reports which show that concrete values are not reaching `VisitBinaryOperator<BO_NE>`. This is due to them being trivially inferred in `RangedConstraintManager.cpp`. I attached the coverage for `RangeConstraintManager.cpp`.

I think that I should remove the handling of concrete APSInt all together from SymbolicRangeInferrer for above reason. What do you guys think?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D112621/new/

https://reviews.llvm.org/D112621