[clang] 6dc1523 - [analyzer][solver] Prevent infeasible states (PR49490)

[Valeriy Savchenko via cfe-commits]

Author: Valeriy Savchenko
Date: 2021-03-12T15:56:48+03:00
New Revision: 6dc152350824d0abcf4e1836c2846f8f9256779c

URL: https://github.com/llvm/llvm-project/commit/6dc152350824d0abcf4e1836c2846f8f9256779c
DIFF: https://github.com/llvm/llvm-project/commit/6dc152350824d0abcf4e1836c2846f8f9256779c.diff

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

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.

Differential Revision: https://reviews.llvm.org/D98341

Added: 
    clang/test/Analysis/PR49490.cpp

Modified: 
    clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

Removed: 
    


################################################################################
diff  --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index a481bde1651b..95e61f9c8c61 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -19,6 +19,8 @@
 #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;
@@ -1395,12 +1397,23 @@ class RangeConstraintManager : public RangedConstraintManager {
     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,
+                                               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);
 
@@ -1413,9 +1426,18 @@ class RangeConstraintManager : public RangedConstraintManager {
       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);
   }
 

diff  --git a/clang/test/Analysis/PR49490.cpp b/clang/test/Analysis/PR49490.cpp
new file mode 100644
index 000000000000..3254355013a6
--- /dev/null
+++ b/clang/test/Analysis/PR49490.cpp
@@ -0,0 +1,30 @@
+// 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);
+}