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

Gabor Marton via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Thu Aug 4 11:45:27 PDT 2022

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`.

  rG LLVM Github Monorepo



More information about the cfe-commits mailing list