[PATCH] D98341: [analyzer][solver] Prevent infeasible states (PR49490)

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko updated this revision to Diff 329903.
vsavchenko marked an inline comment as done.
vsavchenko added a comment.

Make `areFeasible` function static


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D98341

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/PR49490.cpp


Index: clang/test/Analysis/PR49490.cpp
===================================================================
--- /dev/null
+++ clang/test/Analysis/PR49490.cpp
@@ -0,0 +1,31 @@
+// 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 *ints;
+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);
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ 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 @@
     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 @@
       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);
   }
 


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D98341.329903.patch
Type: text/x-patch
Size: 3197 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20210311/7e730792/attachment.bin>