[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

2547

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

127

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

2547

Play with it.

clang/test/Analysis/runtime-regression.c

7

Sadly, I had to manually track this down xD.

8

Maybe the test infra has something to specify a timeout.

12

Pin the tartget triple.

[martong]

• Make reAssume friend, pin the target in the test

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

127

Okay, I've made it a friend.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2547

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

7

Ok, I removed the sentence.

8

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

12

Ok, done.

[steakhal]

Typo; other than that LGTM

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

117

clang/test/Analysis/runtime-regression.c

8

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

117

Fixed, thx.

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

private:
   // 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;
 
   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;
+
+public:
   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);
 

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

EquivalenceClass::removeMember(ProgramStateRef State, const SymbolRef Old) {
 
   return State;
 }
 
 // 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.

clang/test/Analysis/runtime-regression.c

+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core,alpha.security.ArrayBoundV2 \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+// This test is here to check if there is no significant run-time regression
+// related to the assume machinery. This is an automatically reduced code. 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;
+}