[analyzer][solver] Fix infeasible constraints (PR49642)

[vsavchenko]

Summary

Additionally, this patch puts an assertion checking for feasible
constraints in every place where constraints are assigned to states.

[vsavchenko]

Fix typos in comments

[steakhal]

Aa, get it. Looks good.

[NoQ]

Aha ok, seems reasonable, thx!

clang/test/Analysis/PR49642.c

2

Why not the usual %clang_analyze_cc1? Your approach only adds driver testing which doesn't seem to test anything new. Also if you do clang --analyze you don't need to enable core explicitly, you already have all on-by-default checks running.

[vsavchenko]

clang/test/Analysis/PR49642.c

2

I didn't figure out how to reproduce the crash with %clang_analyze_cc1 :-(

[NoQ]

clang/test/Analysis/PR49642.c

2

Mmm ok weird. Let's start by using -### to convert the driver invocation into a -cc1 invocation and then bisecting flags until we obtain a minimal -cc1 invocation.

[vsavchenko]

Re-write the test using %clang_analyze_cc1

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

merge(BasicValueFactory &BV, RangeSet::Factory &F, ProgramStateRef State,
         SymbolRef First, SymbolRef Second);
   // Merge this class with the given class and return a new state.
   LLVM_NODISCARD inline ProgramStateRef merge(BasicValueFactory &BV,
                                               RangeSet::Factory &F,
                                               ProgramStateRef State,
                                               EquivalenceClass Other);
 
   /// Return a set of class members for the given state.
-  LLVM_NODISCARD inline SymbolSet getClassMembers(ProgramStateRef State);
+  LLVM_NODISCARD inline SymbolSet getClassMembers(ProgramStateRef State) const;
   /// Return true if the current class is trivial in the given state.
-  LLVM_NODISCARD inline bool isTrivial(ProgramStateRef State);
+  LLVM_NODISCARD inline bool isTrivial(ProgramStateRef State) const;
   /// Return true if the current class is trivial and its only member is dead.
   LLVM_NODISCARD inline bool isTriviallyDead(ProgramStateRef State,
-                                             SymbolReaper &Reaper);
+                                             SymbolReaper &Reaper) const;
 
   LLVM_NODISCARD static inline ProgramStateRef
   markDisequal(BasicValueFactory &BV, RangeSet::Factory &F,
                ProgramStateRef State, SymbolRef First, SymbolRef Second);
   LLVM_NODISCARD static inline ProgramStateRef
   markDisequal(BasicValueFactory &BV, RangeSet::Factory &F,
                ProgramStateRef State, EquivalenceClass First,
                EquivalenceClass Second);
SymbolRef getRepresentativeSymbol() const {
     return reinterpret_cast<SymbolRef>(ID);
   }
   static inline SymbolSet::Factory &getMembersFactory(ProgramStateRef State);
 
   inline ProgramStateRef mergeImpl(BasicValueFactory &BV, RangeSet::Factory &F,
                                    ProgramStateRef State, SymbolSet Members,
                                    EquivalenceClass Other,
                                    SymbolSet OtherMembers);
-  static inline void
+  static inline bool
   addToDisequalityInfo(DisequalityMapTy &Info, ConstraintRangeTy &Constraints,
                        BasicValueFactory &BV, RangeSet::Factory &F,
                        ProgramStateRef State, EquivalenceClass First,
                        EquivalenceClass Second);
 
   /// This is a unique identifier of the class.
   uintptr_t ID;
 };
 
 //===----------------------------------------------------------------------===//
 //                             Constraint functions
 //===----------------------------------------------------------------------===//
 
+LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED bool
+areFeasible(ConstraintRangeTy Constraints) {
+  return llvm::none_of(
+      Constraints,
+      [](const std::pair<EquivalenceClass, RangeSet> &ClassConstraint) {
+        return ClassConstraint.second.isEmpty();
+      });
+}
+
 LLVM_NODISCARD inline const RangeSet *getConstraint(ProgramStateRef State,
                                                     EquivalenceClass Class) {
   return State->get<ConstraintRange>(Class);
 }
 
 LLVM_NODISCARD inline const RangeSet *getConstraint(ProgramStateRef State,
                                                     SymbolRef Sym) {
   return getConstraint(State, EquivalenceClass::find(State, Sym));
ProgramStateRef trackDisequality(ProgramStateRef State, SymbolRef LHS,
     return EquivalenceClass::markDisequal(getBasicVals(), F, State, LHS, RHS);
   }
 
   ProgramStateRef trackEquality(ProgramStateRef State, SymbolRef LHS,
                                 SymbolRef RHS) {
     return EquivalenceClass::merge(getBasicVals(), F, State, LHS, RHS);
   }
 
-  LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED static bool
-  areFeasible(ConstraintRangeTy Constraints) {
-    return llvm::none_of(
-        Constraints,
-        [](const std::pair<EquivalenceClass, RangeSet> &ClassConstraint) {
-          return ClassConstraint.second.isEmpty();
-        });
-  }
-
   LLVM_NODISCARD ProgramStateRef setConstraint(ProgramStateRef State,
                                                EquivalenceClass Class,
                                                RangeSet Constraint) {
     ConstraintRangeTy Constraints = State->get<ConstraintRange>();
     ConstraintRangeTy::Factory &CF = State->get_context<ConstraintRange>();
 
     assert(!Constraint.isEmpty() && "New constraint should not be empty");
 
     // Add new constraint.
     Constraints = CF.add(Constraints, Class, Constraint);
 
     // There is a chance that we might need to update constraints for the
     // classes that are known to be disequal to Class.
     //
     // In order for this to be even possible, the new constraint should
     // be simply a constant because we can't reason about range disequalities.
     if (const llvm::APSInt *Point = Constraint.getConcreteValue())
       for (EquivalenceClass DisequalClass : Class.getDisequalClasses(State)) {
         RangeSet UpdatedConstraint =
             getRange(State, DisequalClass).Delete(getBasicVals(), F, *Point);
 
         // If we end up with at least one of the disequal classes to be
-        // constrainted with an empty range-set, the state is infeasible.
+        // constrained with an empty range-set, the state is infeasible.
         if (UpdatedConstraint.isEmpty())
           return nullptr;
 
         Constraints = CF.add(Constraints, DisequalClass, UpdatedConstraint);
       }
 
     assert(areFeasible(Constraints) && "Constraint manager shouldn't produce "
                                        "a state with infeasible constraints");
if (NewClassConstraint->isEmpty())
       // Infeasible state
       return nullptr;
 
     // No need in tracking constraints of a now-dissolved class.
     Constraints = CRF.remove(Constraints, Other);
     // Assign new constraints for this class.
     Constraints = CRF.add(Constraints, *this, *NewClassConstraint);
 
+    assert(areFeasible(Constraints) && "Constraint manager shouldn't produce "
+                                       "a state with infeasible constraints");
+
     State = State->set<ConstraintRange>(Constraints);
   }
 
   // 2. Get ALL equivalence-related maps
   ClassMapTy Classes = State->get<ClassMap>();
   ClassMapTy::Factory &CMF = State->get_context<ClassMap>();
 
   ClassMembersTy Members = State->get<ClassMembers>();
EquivalenceClass::mergeImpl(BasicValueFactory &ValueFactory,
   return State;
 }
 
 inline SymbolSet::Factory &
 EquivalenceClass::getMembersFactory(ProgramStateRef State) {
   return State->get_context<SymbolSet>();
 }
 
-SymbolSet EquivalenceClass::getClassMembers(ProgramStateRef State) {
+SymbolSet EquivalenceClass::getClassMembers(ProgramStateRef State) const {
   if (const SymbolSet *Members = State->get<ClassMembers>(*this))
     return *Members;
 
   // This class is trivial, so we need to construct a set
   // with just that one symbol from the class.
   SymbolSet::Factory &F = getMembersFactory(State);
   return F.add(F.getEmptySet(), getRepresentativeSymbol());
 }
 
-bool EquivalenceClass::isTrivial(ProgramStateRef State) {
+bool EquivalenceClass::isTrivial(ProgramStateRef State) const {
   return State->get<ClassMembers>(*this) == nullptr;
 }
 
 bool EquivalenceClass::isTriviallyDead(ProgramStateRef State,
-                                       SymbolReaper &Reaper) {
+                                       SymbolReaper &Reaper) const {
   return isTrivial(State) && Reaper.isDead(getRepresentativeSymbol());
 }
 
 inline ProgramStateRef EquivalenceClass::markDisequal(BasicValueFactory &VF,
                                                       RangeSet::Factory &RF,
                                                       ProgramStateRef State,
                                                       SymbolRef First,
                                                       SymbolRef Second) {
if (*this == Other) {
     return nullptr;
   }
 
   DisequalityMapTy DisequalityInfo = State->get<DisequalityMap>();
   ConstraintRangeTy Constraints = State->get<ConstraintRange>();
 
   // Disequality is a symmetric relation, so if we mark A as disequal to B,
   // we should also mark B as disequalt to A.
-  addToDisequalityInfo(DisequalityInfo, Constraints, VF, RF, State, *this,
-                       Other);
-  addToDisequalityInfo(DisequalityInfo, Constraints, VF, RF, State, Other,
-                       *this);
+  if (!addToDisequalityInfo(DisequalityInfo, Constraints, VF, RF, State, *this,
+                            Other) ||
+      !addToDisequalityInfo(DisequalityInfo, Constraints, VF, RF, State, Other,
+                            *this))
+    return nullptr;
+
+  assert(areFeasible(Constraints) && "Constraint manager shouldn't produce "
+                                     "a state with infeasible constraints");
 
   State = State->set<DisequalityMap>(DisequalityInfo);
   State = State->set<ConstraintRange>(Constraints);
 
   return State;
 }
 
-inline void EquivalenceClass::addToDisequalityInfo(
+inline bool EquivalenceClass::addToDisequalityInfo(
     DisequalityMapTy &Info, ConstraintRangeTy &Constraints,
     BasicValueFactory &VF, RangeSet::Factory &RF, ProgramStateRef State,
     EquivalenceClass First, EquivalenceClass Second) {
 
   // 1. Get all of the required factories.
   DisequalityMapTy::Factory &F = State->get_context<DisequalityMap>();
   ClassSet::Factory &CF = State->get_context<ClassSet>();
   ConstraintRangeTy::Factory &CRF = State->get_context<ConstraintRange>();
inline bool EquivalenceClass::addToDisequalityInfo(
   //    At the same time, the same logic does not apply to ranges.
   if (const RangeSet *SecondConstraint = Constraints.lookup(Second))
     if (const llvm::APSInt *Point = SecondConstraint->getConcreteValue()) {
 
       RangeSet FirstConstraint = SymbolicRangeInferrer::inferRange(
           VF, RF, State, First.getRepresentativeSymbol());
 
       FirstConstraint = FirstConstraint.Delete(VF, RF, *Point);
+
+      // If the First class is about to be constrained with an empty
+      // range-set, the state is infeasible.
+      if (FirstConstraint.isEmpty())
+        return false;
+
       Constraints = CRF.add(Constraints, First, FirstConstraint);
     }
+
+  return true;
 }
 
 inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State,
                                                  SymbolRef FirstSym,
                                                  SymbolRef SecondSym) {
   EquivalenceClass First = find(State, FirstSym);
   EquivalenceClass Second = find(State, SecondSym);
 

clang/test/Analysis/PR49642.c

+// RUN: %clang_analyze_cc1 -w -verify %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=apiModeling.StdCLibraryFunctions
+
+// expected-no-diagnostics
+
+typedef ssize_t;
+b;
+
+unsigned c;
+int write(int, const void *, unsigned long);
+
+a() {
+  d();
+  while (c > 0) {
+    b = write(0, d, c);
+    if (b)
+      c -= b;
+    b < 1;
+  }
+  if (c && c) {
+    //     ^ no-crash
+  }
+}