[PATCH] D131006: [analyzer] Use DisequalityMap while inferring constraints

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.


================
Comment at: clang/test/Analysis/range-inferring-from-disequality-map.cpp:50-51
+    if(x != tmp1 && x != tmp2)
+      // TODO: This condition should be infeasible.
+      //       Thus, the branch should be unreachable.
+      clang_analyzer_value(x); // expected-warning {{{ empty }}}
----------------
ASDenysPetrov wrote:
> martong wrote:
> > Why can't we return an empty set from `getInvertedRangeFromDisequalityMap` in this case? `intersect` should handle the rest then.
> Currently, we can't.  At least, in this patch.
> We produce infeasible branches (aka `nullptr` `ProgramStateRef`) when use `ConstraintAssignor::assign`.
> But here we use `SymbolicRangeInferrer` which only produces a RangeSet. In other words, we don't store this range anywhere but infer it every time.
> 
> Basically, this is a work for the next patches. They should remove the TODOs.
You mean this hunk?
```
       for (EquivalenceClass DisequalClass : Class.getDisequalClasses(State)) {
        RangeSet UpdatedConstraint = SymbolicRangeInferrer::inferRange(
            RangeFactory, State, DisequalClass);

        UpdatedConstraint = RangeFactory.deletePoint(UpdatedConstraint, *Point);

        // If we end up with at least one of the disequal classes to be
        // constrained with an empty range-set, the state is infeasible.
        if (UpdatedConstraint.isEmpty())
          return nullptr;

```

Yeah, I am not sure why do we infer a range here instead of simply getting the associated range from the constraint set. Inferring here might result with an inconsistent result. I think we should infer only in the `SymbolicRangeInferrer`.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D131006