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

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko created this revision.
vsavchenko added reviewers: steakhal, NoQ, xazax.hun, ASDenysPetrov.
Herald added subscribers: martong, Charusso, dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware.
vsavchenko requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

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.


Repository:
  rG LLVM Github Monorepo

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,29 @@
+// RUN: %clang_analyze_cc1 -w -analyzer-checker=core,alpha.security.ArrayBound  -verify %s
+
+struct toggle {
+  bool value;
+};
+
+toggle global_toggle;
+toggle get_global_toggle() { return global_toggle; }
+
+int *ints;
+int oob_access() { return ints[-1]; } // expected-warning{{out-of-bound}}
+
+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,22 @@
     return EquivalenceClass::merge(getBasicVals(), F, State, LHS, RHS);
   }
 
+  LLVM_ATTRIBUTE_UNUSED inline bool areFeasible(ConstraintRangeTy Constraints) {
+    return llvm::none_of(
+        Constraints,
+        [](const std::pair<EquivalenceClass, RangeSet> ClassConstraint) {
+          return ClassConstraint.second.isEmpty();
+        });
+  }
+
   LLVM_NODISCARD inline 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 +1425,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.329636.patch
Type: text/x-patch
Size: 3017 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20210310/38907cfa/attachment-0001.bin>