[analyzer] Return from reAssume if State is posteriorly overconstrained

[martong]

Summary

Depends on D124758. That patch introduced serious regression in the run-time in
some special cases. This fixes that.

[martong]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2553

I am wondering, that maybe it would be better to check for isPosteriorlyOverconstrained here. Because only State->assume can return such States, and by checking it here, we could spare some instructions.

[steakhal]

Thanks for the quick response!

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h

137

This shouldnt be the way.
Consider fwd declaring and making it friend instead.
I really dont want to expose this api.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2553

Play with it.

clang/test/Analysis/runtime-regression.c

8

Sadly, I had to manually track this down xD.

9

Maybe the test infra has something to specify a timeout.

13

Pin the tartget triple.

[martong]

• Make reAssume friend, pin the target in the test

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h

137

Okay, I've made it a friend.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2553

Yeah, I will, but I don't know how much time that would take to assess. So, in the meantime let's proceed with this version.

clang/test/Analysis/runtime-regression.c

8

Ok, I removed the sentence.

9

I could not find how to set a timeout in the test file. There is a lit cli option that might be used, however, that would affect all other test cases. https://llvm.org/docs/CommandGuide/lit.html#cmdoption-lit-timeout

13

Ok, done.

[steakhal]

Typo; other than that LGTM

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h

118

clang/test/Analysis/runtime-regression.c

9

Why you could do is to call RUN {lit} --max-time XX Then do a FileCheck against the output of that.
Alternatively, we can craft something to make the situation worse, to the point that we will notice, and effectively hang the test suite. Either way, I'm fine with how things look ATM.

[martong]

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h

118

Fixed, thx.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h

 template <typename T> struct ProgramStateTrait {
   typedef typename T::data_type data_type;
   static inline void *MakeVoidPtr(data_type D) { return (void*) D; }
   static inline data_type MakeData(void *const* P) {
     return P ? (data_type) *P : (data_type) 0;
   }
 };
 
+class RangeSet;
+
 /// \class ProgramState
 /// ProgramState - This class encapsulates:
 ///
 ///    1. A mapping from expressions to values (Environment)
 ///    2. A mapping from locations to values (Store)
 ///    3. Constraints on symbolic values (GenericDataMap)
 ///
 ///  Together these represent the "abstract state" of a program.
 ///
 ///  ProgramState is intended to be used as a functional object; that is,
 ///  once it is created and made "persistent" in a FoldingSet, its
 ///  values will never change.
 class ProgramState : public llvm::FoldingSetNode {
 public:
   typedef llvm::ImmutableSet<llvm::APSInt*>                IntSetTy;
   typedef llvm::ImmutableMap<void*, void*>                 GenericDataMap;
 
 private:
   void operator=(const ProgramState& R) = delete;
 
   friend class ProgramStateManager;
   friend class ExplodedGraph;
   friend class ExplodedNode;
   friend class NodeBuilder;
-  friend class ConstraintManager;
 
   ProgramStateManager *stateMgr;
   Environment Env;           // Maps a Stmt to its current SVal.
   Store store;               // Maps a location to its current value.
   GenericDataMap   GDM;      // Custom data stored by a client of this class.
 
   // A state is infeasible if there is a contradiction among the constraints.
   // An infeasible state is represented by a `nullptr`.
private:
   // solver re-evaluates the existing constraints and realizes the
   // contradiction `0 * 0 = 4`.
   // We also evaluate the negated constraint `x != 0`;  the constraint solver
   // deduces `x = 1` and then realizes the contradiction `1 * 1 = 4`.
   // Both children are infeasible, thus the parent state is marked as
   // posteriorly over-constrained. These parents are handled with special care:
   // we do not allow transitions to exploded nodes with such states.
   bool PosteriorlyOverconstrained = false;
+  // Make internal constraint solver entities friends so they can access the
+  // overconstrained-related functions. We want to keep this API inaccessible
+  // for Checkers.
+  friend class ConstraintManager;
+  friend ProgramStateRef reAssume(ProgramStateRef State,
+                                  const RangeSet *Constraint, SVal TheValue);
+  bool isPosteriorlyOverconstrained() const {
+    return PosteriorlyOverconstrained;
+  }
+  ProgramStateRef cloneAsPosteriorlyOverconstrained() const;
 
   unsigned refCount;
 
   /// makeWithStore - Return a ProgramState with the same values as the current
   ///  state with the exception of using the specified Store.
   ProgramStateRef makeWithStore(const StoreRef &store) const;
 
   void setStore(const StoreRef &storeRef);
 
-  ProgramStateRef cloneAsPosteriorlyOverconstrained() const;
-  bool isPosteriorlyOverconstrained() const {
-    return PosteriorlyOverconstrained;
-  }
-
 public:
   /// This ctor is used when creating the first ProgramState object.
   ProgramState(ProgramStateManager *mgr, const Environment& env,
           StoreRef st, GenericDataMap gdm);
 
   /// Copy ctor - We must explicitly define this or else the "Next" ptr
   ///  in FoldingSetNode will also get copied.
   ProgramState(const ProgramState &RHS);
 
   ~ProgramState();

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

EquivalenceClass::removeMember(ProgramStateRef State, const SymbolRef Old) {
   ClassMapTy Classes = State->get<ClassMap>();
   ClassMapTy::Factory &CMF = State->get_context<ClassMap>();
   Classes = CMF.remove(Classes, Old);
   State = State->set<ClassMap>(Classes);
 
   return State;
 }
 
+// We must declare reAssume in clang::ento, otherwise we could not declare that
+// as a friend in ProgramState. More precisely, the call of reAssume would be
+// ambiguous (one in the global namespace and an other which is declared in
+// ProgramState is in clang::ento).
+namespace clang {
+namespace ento {
 // Re-evaluate an SVal with top-level `State->assume` logic.
 LLVM_NODISCARD ProgramStateRef reAssume(ProgramStateRef State,
                                         const RangeSet *Constraint,
                                         SVal TheValue) {
+  assert(State);
+  if (State->isPosteriorlyOverconstrained())
+    return nullptr;
   if (!Constraint)
     return State;
 
   const auto DefinedVal = TheValue.castAs<DefinedSVal>();
 
   // If the SVal is 0, we can simply interpret that as `false`.
   if (Constraint->encodesFalseRange())
     return State->assume(DefinedVal, false);
 
   // If the constraint does not encode 0 then we can interpret that as `true`
   // AND as a Range(Set).
   if (Constraint->encodesTrueRange()) {
     State = State->assume(DefinedVal, true);
     if (!State)
       return nullptr;
     // Fall through, re-assume based on the range values as well.
   }
   // Overestimate the individual Ranges with the RangeSet' lowest and
   // highest values.
   return State->assumeInclusiveRange(DefinedVal, Constraint->getMinValue(),
                                      Constraint->getMaxValue(), true);
 }
+} // namespace ento
+} // namespace clang
 
 // Iterate over all symbols and try to simplify them. Once a symbol is
 // simplified then we check if we can merge the simplified symbol's equivalence
 // class to this class. This way, we simplify not just the symbols but the
 // classes as well: we strive to keep the number of the classes to be the
 // absolute minimum.
 LLVM_NODISCARD ProgramStateRef
 EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F,

clang/test/Analysis/runtime-regression.c

+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core,alpha.security.ArrayBoundV2 \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -triple x86_64-unknown-linux-gnu \
+// RUN:   -verify
+
+// This test is here to check if there is no significant run-time regression
+// related to the assume machinery. The analysis should finish in less than 10
+// seconds.
+
+// expected-no-diagnostics
+
+typedef unsigned char uint8_t;
+typedef unsigned short uint16_t;
+typedef unsigned long uint64_t;
+
+int filter_slice_word(int sat_linesize, int sigma, int radius, uint64_t *sat,
+                      uint64_t *square_sat, int width, int height,
+                      int src_linesize, int dst_linesize, const uint16_t *src,
+                      uint16_t *dst, int jobnr, int nb_jobs) {
+  const int starty = height * jobnr / nb_jobs;
+  const int endy = height * (jobnr + 1) / nb_jobs;
+
+  for (int y = starty; y < endy; y++) {
+
+    int lower_y = y - radius < 0 ? 0 : y - radius;
+    int higher_y = y + radius + 1 > height ? height : y + radius + 1;
+    int dist_y = higher_y - lower_y;
+
+    for (int x = 0; x < width; x++) {
+
+      int lower_x = x - radius < 0 ? 0 : x - radius;
+      int higher_x = x + radius + 1 > width ? width : x + radius + 1;
+      int count = dist_y * (higher_x - lower_x);
+
+      // The below hunk caused significant regression in run-time.
+#if 1
+      uint64_t sum = sat[higher_y * sat_linesize + higher_x] -
+                     sat[higher_y * sat_linesize + lower_x] -
+                     sat[lower_y * sat_linesize + higher_x] +
+                     sat[lower_y * sat_linesize + lower_x];
+      uint64_t square_sum = square_sat[higher_y * sat_linesize + higher_x] -
+                            square_sat[higher_y * sat_linesize + lower_x] -
+                            square_sat[lower_y * sat_linesize + higher_x] +
+                            square_sat[lower_y * sat_linesize + lower_x];
+      uint64_t mean = sum / count;
+      uint64_t var = (square_sum - sum * sum / count) / count;
+      dst[y * dst_linesize + x] =
+          (sigma * mean + var * src[y * src_linesize + x]) / (sigma + var);
+#endif
+
+    }
+  }
+  return 0;
+}