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

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

In D106102#3019921 <https://reviews.llvm.org/D106102#3019921>, @manas wrote:

> I haven't tried specializing that `VisitBinaryOperator` method which converts Ranges from RangeSets (as @vsavchenko mentioned). Should this case for NE stay here in the switch or move?

Please try what @vsavchenko mentioned, seems like with RangeSet::getMinValue and getMaxValue we can achieve the same before coersing to simple Ranges.



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1223-1225
+template <>
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_NE>(Range LHS, Range RHS,
+                                                           QualType T) {
----------------
manas wrote:
> vsavchenko wrote:
> > I think it should be a specialization for another `VisitBinaryOperator`.
> > In the switch, you can see that we give range sets for `LHS` and `RHS`, so how does it work?
> > There is a function in between (also `VisitBinaryOperator`) that creates simple ranges out of range sets and ask to visit binary operator for those.  You can specialize it instead since we can simply check for empty intersection of range sets.
> I went through the code and understood that part. I agree that this should be a specialized case for VisitBinaryOperator. So I understand it in this way:
> 
> 1. Creating a new `VisitBinaryOperator(Range,Range,QualType)` which can check for empty intersections.
> 2. It will then call to appropriate functions (like `VisittBinaryOperator<BO_NE>` and others.)
No. You need the following specialization for `RangeSet`:
```
  template <>
  RangeSet VisitBinaryOperator<BO_NE>(RangeSet LHS, RangeSet RHS, QualType T) {
    // your original code here...
    return infer(T);
  }
```
Besides, I think you should use getMaxValue() and getMinValue() instead of To() and From().


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1241
+  // In all other cases, the resulting range cannot be deduced.
+  return RangeFactory.getEmptySet();
+}
----------------
manas wrote:
> vsavchenko wrote:
> > Empty range set means "This situation is IMPOSSIBLE".  Is that what you want here?
> True! That's incorrect. We cannot find a good rangeset. Should I rather return the entire RangeSet inferred from `T`?
> True! That's incorrect. We cannot find a good rangeset. Should I rather return the entire RangeSet inferred from T?
Yes, that would work! Because the entire RangeSet implies both the logical True (non-zero values) and the logica False values.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106102