[analyzer][solver] Prevent infeasible states (PR49490)

[vsavchenko]

Summary

This patch fixes the situation when our knowledge of disequalities
can help us figuring out that some assumption is infeasible, but
the solver still produces a state with inconsistent constraints.

Additionally, this patch adds a couple of assertions to catch this
type of problems easier.

[NoQ]

You're testing it with the help of an alpha checker. Is this checker doing something special that we don't do normally? In particular, both array bound checkers that we have are very likely to be re-done from scratch if they are ever to be completed. A lot of decisions in them are questionable. So i'm worried that this test will become stale in that process. Maybe a unittest would be more appropriate so that to guarantee the specific functionality without relying on implementation details of the specific checker(?)

Code looks great and I guess assertions are a test on their own.

[steakhal]

Looks good btw.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1400–1406

inline is unnecessary. All member functions are inline by default.
I would take the parameter by const ref in the lambda.
Why did you mark it LLVM_ATTRIBUTE_UNUSED ? LLVM_NODISCARD would be probably a better choice.

[vsavchenko]

Fix review comments

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1400–1406

Fair point about inline.
LLVM_NODISCARD doesn't exclude LLVM_ATTRIBUTE_UNUSED.
It should be marked that way for Release builds when compiler might figure out that this class is local to only this TU, and this function is not used here anywhere. You can see in the comment for this macro that this is actually the main motivation for this macro to be used.

[vsavchenko]

Make areFeasible function static

[steakhal]

clang/test/Analysis/PR49490.cpp

13

I think you can remove this line.
We already have a global variable to be invalidated by the evaluation of oob_access() call.

[vsavchenko]

Remove unused global variable from the test

[steakhal]

The assertion areFeasible(Constraints) triggered on trunk.
More details in the Bugzilla ticket.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 #include "clang/Basic/JsonSupport.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
 #include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/ImmutableSet.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/Support/Compiler.h"
 #include "llvm/Support/raw_ostream.h"
 
 using namespace clang;
 using namespace ento;
 
 // This class can be extended with other tables which will help to reason
 // about ranges more precisely.
 class OperatorRelationsTable {
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 inline ProgramStateRef setConstraint(ProgramStateRef State,
-                                                      EquivalenceClass Class,
-                                                      RangeSet Constraint) {
+  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,
     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.
+        if (UpdatedConstraint.isEmpty())
+          return nullptr;
+
         Constraints = CF.add(Constraints, DisequalClass, UpdatedConstraint);
       }
 
+    assert(areFeasible(Constraints) && "Constraint manager shouldn't produce "
+                                       "a state with infeasible constraints");
+
     return State->set<ConstraintRange>(Constraints);
   }
 
   LLVM_NODISCARD inline ProgramStateRef
   setConstraint(ProgramStateRef State, SymbolRef Sym, RangeSet Constraint) {
     return setConstraint(State, EquivalenceClass::find(State, Sym), Constraint);
   }
 };

clang/test/Analysis/PR49490.cpp

+// RUN: %clang_analyze_cc1 -w -analyzer-checker=core -verify %s
+
+// expected-no-diagnostics
+
+struct toggle {
+  bool value;
+};
+
+toggle global_toggle;
+toggle get_global_toggle() { return global_toggle; }
+
+int oob_access();
+
+bool compare(toggle one, bool other) {
+  if (one.value != other)
+    return true;
+
+  if (one.value)
+    oob_access();
+  return true;
+}
+
+bool coin();
+
+void bar() {
+  bool left = coin();
+  bool right = coin();
+  for (;;)
+    compare(get_global_toggle(), left) && compare(get_global_toggle(), right);
+}