[analyzer] Track assume call stack to detect fixpoint

[martong]

Summary

Assume functions might recurse (see reAssume or tryRearrange). During the
recursion, the State might not change anymore, that means we reached a
fixpoint. In this patch, we avoid infinite recursion of assume calls by
checking already visited States on the stack of assume function calls. This
patch renders the previous "workaround" solution (D47155) unnecessary.
Note that this is not an NFC patch. If we were to limit the maximum stack
depth of the assume calls to 1 then would it be equivalent with the previous
solution in D47155.

Additionally, in D113753, we simplify the symbols right at the beginning of evalBinOpNN.
So, a call to simplifySVal in getKnownValue (added in D51252) is no longer needed.

[martong]

• Add AssumeStack to track recursive assume calls

[steakhal]

This isn't an NFC change. It's more than a refactor/cosmetic change.
Please run some benchmarks to validate the assumed performance characteristics.

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

155

Have you considered llvm::SmallPtrSet ?

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

56–59

Why don't you return RawSt on the early return path instead? That seems to contain more information than State, right?

You lookup twice the location of the RawSt entry; once in the hasCycle() and again in the push().
I would recommend doing an unconditional insert() directly and reusing the returned bool part of the pair to observe if it did actually insert.

[martong]

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

155

Actually, a SmallSet of pointers is transparently implemented with a SmallPtrSet.

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

56–59

Why don't you return RawSt on the early return path instead? That seems to contain more information than State, right?

No, RawSt contains the same information as State.

You lookup twice the location of the RawSt entry; once in the hasCycle() and again in the push().
I would recommend doing an unconditional insert() directly and reusing the returned bool part of the pair to observe if it did actually insert.

I am considering to change the container to a SmallVector instead. I'd like to keep the interface of hasCycle and push and pop because those express the intention more clearly. And SmallSet falls back to a simple linear search anyway if size is less than N.

[martong]

In D126560#3549408, @steakhal wrote:

This isn't an NFC change. It's more than a refactor/cosmetic change.

Still, there is no visible change in the behavior, at least that is intended. Should it be an NFCi ?

Please run some benchmarks to validate the assumed performance characteristics.

Yeah I've thought of it, here it is:

[martong]

• Use SmallVector in AssumeStack

[steakhal]

In D126560#3549570, @martong wrote:

In D126560#3549408, @steakhal wrote:

This isn't an NFC change. It's more than a refactor/cosmetic change.

Still, there is no visible change in the behavior, at least that is intended. Should it be an NFCi ?

Please run some benchmarks to validate the assumed performance characteristics.

Yeah I've thought of it, here it is:

Yes, let's go with NFCi.

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

56–59

I'd like to keep the interface of hasCycle and push and pop because those express the intention more clearly.

I disagree. Double lookups are always a code-smell. I insist on this.

[martong]

• Remove FIXME comment

[martong]

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

139–145

This hunk is probably also superfluous. With tracking the assume stack below, it should be safe to call assume even from evalAssume. But, I'd rather remove that in a subsequent patch, because checkNulls behavior is dependent on that.

[steakhal]

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

21

Unused.

139–145

Oh, I haven't thought about that. Thanks. Feel free to do in a followup!

153

Use llvm::is_contained() instead.

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

60

Don't we call these 'Guards'?

[martong]

I've made some measurements with the diff down below. So, it seems like the chance of being a recursive call is very unlikely (roughly 1/10000). Thus I am going to update this condition with LLVM_UNLIKELY. Besides, the depth of the call stack seems to be less than 4 in the majority of cases (99.98%). However, there are edge cases (ffmpeg) when the depth is even bigger than 16. Consequently, a SmallPtrSet with 4 as the small buffer size would be better than the SmallVector.

Attached the csa-testbanch results.

stats.html255 KBDownload

Plus, attached a summarizing excel sheet about the assume stack depth (courtesy of @steakhal).

assume-stack-depths.xlsx25 KBDownload

diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
index f1b75a57115b..097d0ff8d162 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -153,6 +153,7 @@ protected:
     bool contains(const ProgramState *S) const {
       return llvm::find(Aux, S) != Aux.end();
     }
+    size_t size() { return Aux.size(); }

   private:
     llvm::SmallVector<const ProgramState *, 4> Aux;
diff --git a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
index 0866d3d0db74..11bbda9dd899 100644
--- a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -17,10 +17,25 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "llvm/ADT/ScopeExit.h"
+#include "llvm/ADT/Statistic.h"

 using namespace clang;
 using namespace ento;

+#define DEBUG_TYPE "CoreEngine"
+
+STATISTIC(NumAssume, "The # of assume calls");
+STATISTIC(NumAssumeRecurse, "The # of recursive assume calls");
+STATISTIC(AssumeStackSize01, "The # of assume stack size between 0 and 1");
+STATISTIC(AssumeStackSize23, "The # of assume stack size between 2 and 3");
+STATISTIC(AssumeStackSize45, "The # of assume stack size between 4 and 5");
+STATISTIC(AssumeStackSize67, "The # of assume stack size between 6 and 7");
+STATISTIC(AssumeStackSize89, "The # of assume stack size between 8 and 9");
+STATISTIC(AssumeStackSize1011, "The # of assume stack size between 10 and 11");
+STATISTIC(AssumeStackSize1213, "The # of assume stack size between 12 and 13");
+STATISTIC(AssumeStackSize1415, "The # of assume stack size between 14 and 15");
+STATISTIC(AssumeStackSize16XX, "The # of assume stack size greater equal than 16");
+
 ConstraintManager::~ConstraintManager() = default;

 static DefinedSVal getLocFromSymbol(const ProgramStateRef &State,
@@ -53,9 +68,30 @@ ConstraintManager::assumeDualImpl(ProgramStateRef &State,
   // fixpoint.
   // We avoid infinite recursion of assume calls by checking already visited
   // States on the stack of assume function calls.
+  ++NumAssume;
+  if (AssumeStack.size() < 2)
+    ++AssumeStackSize01;
+  else if (AssumeStack.size() < 4)
+    ++AssumeStackSize23;
+  else if (AssumeStack.size() < 6)
+    ++AssumeStackSize45;
+  else if (AssumeStack.size() < 8)
+    ++AssumeStackSize67;
+  else if (AssumeStack.size() < 10)
+    ++AssumeStackSize89;
+  else if (AssumeStack.size() < 12)
+    ++AssumeStackSize1011;
+  else if (AssumeStack.size() < 14)
+    ++AssumeStackSize1213;
+  else if (AssumeStack.size() < 16)
+    ++AssumeStackSize1415;
+  else
+    ++AssumeStackSize16XX;
   const ProgramState *RawSt = State.get();
-  if (AssumeStack.contains(RawSt))
+  if (AssumeStack.contains(RawSt)) {
+    ++NumAssumeRecurse;
     return {State, State};
+  }
   AssumeStack.push(RawSt);
   auto AssumeStackBuilder =
       llvm::make_scope_exit([this]() { AssumeStack.pop(); });

[martong]

Consequently, a SmallPtrSet with 4 as the small buffer size would be better than the SmallVector

Ahh, SmallVector is still better, because with the set we need to do a search in the `erase, which compares badly to a simple decrement in the vector's pop_back.

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

21

Thx.

153

Ok.

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

60

Yeah, we tend to call them guards in the context of exception safety and resource management. But, I think, "builder" is more expressive here.

[martong]

• Add LLVM_UNLIKELY

[steakhal]

Looks good!

[steakhal]

Express why this is not an NFC patch in the summary.

[martong]

Measurement results on the last diff looks good.

[steakhal]

New assertion failure:

llvm-project/clang/lib/StaticAnalyzer/Checkers/UndefResultChecker.cpp:72: bool isLeftShiftResultUnrepresentable(const clang::BinaryOperator *, clang::ento::CheckerContext &): Assertion `LHS && RHS && "Values unknown, inconsistent state"' failed.

Reproduction:

cat > extent.c <<EOF
void crashing(long a, _Bool b) {
  a & 1 && 0;
  b = a & 1;
  b << 1;
}
EOF
build/release/bin/clang --analyze -Xclang -analyzer-checker=core extent.c

The important part of the stack trace:

isLeftShiftResultUnrepresentable(clang::BinaryOperator const*, clang::ento::CheckerContext&) llvm-project/clang/lib/StaticAnalyzer/Checkers/UndefResultChecker.cpp:73:20
UndefResultChecker::checkPostStmt(clang::BinaryOperator const*, clang::ento::CheckerContext&) const llvm-project/clang/lib/StaticAnalyzer/Checkers/UndefResultChecker.cpp:154:18

Please @martong have a look at this.

[martong]

Thanks for the report. I am looking into it.

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

 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
 
 #include "clang/Basic/LLVM.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h"
 #include "llvm/ADT/Optional.h"
 #include "llvm/Support/SaveAndRestore.h"
 #include <memory>
 #include <utility>
 
 namespace llvm {
 
 class APSInt;
 
 } // namespace llvm
public:
   /// not null, or if neither assumption can be made.
   ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
     SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
 
     return checkNull(State, Sym);
   }
 
 protected:
   /// A flag to indicate that clients should be notified of assumptions.
   /// By default this is the case, but sometimes this needs to be restricted
   /// to avoid infinite recursions within the ConstraintManager.
   ///
   /// Note that this flag allows the ConstraintManager to be re-entrant,
   /// but not thread-safe.
   bool NotifyAssumeClients = true;
 
+  /// A helper class to simulate the call stack of nested assume calls.
+  class AssumeStackTy {
+  public:
+    void push(const ProgramState *S) { Aux.push_back(S); }
+    void pop() { Aux.pop_back(); }
+    bool contains(const ProgramState *S) const {
+      return llvm::is_contained(Aux, S);
+    }
+
+  private:
+    llvm::SmallVector<const ProgramState *, 4> Aux;
+  };
+  AssumeStackTy AssumeStack;
+
   virtual ProgramStateRef assumeInternal(ProgramStateRef state,
                                          DefinedSVal Cond, bool Assumption) = 0;
 
   virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State,
                                                        NonLoc Value,
                                                        const llvm::APSInt &From,
                                                        const llvm::APSInt &To,
                                                        bool InBound) = 0;

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

 //===----------------------------------------------------------------------===//
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
 #include "clang/AST/Type.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
+#include "llvm/ADT/ScopeExit.h"
 
 using namespace clang;
 using namespace ento;
 
 ConstraintManager::~ConstraintManager() = default;
 
 static DefinedSVal getLocFromSymbol(const ProgramStateRef &State,
                                     SymbolRef Sym) {

 
 template <typename AssumeFunction>
 ConstraintManager::ProgramStatePair
 ConstraintManager::assumeDualImpl(ProgramStateRef &State,
                                   AssumeFunction &Assume) {
   if (State->isPosteriorlyOverconstrained())
     return {State, State};
 
+  // Assume functions might recurse (see `reAssume` or `tryRearrange`). During
+  // the recursion the State might not change anymore, that means we reached a
+  // fixpoint.
+  // We avoid infinite recursion of assume calls by checking already visited
+  // States on the stack of assume function calls.
+  const ProgramState *RawSt = State.get();
+  if (LLVM_UNLIKELY(AssumeStack.contains(RawSt)))
+    return {State, State};
+  AssumeStack.push(RawSt);
+  auto AssumeStackBuilder =
+      llvm::make_scope_exit([this]() { AssumeStack.pop(); });
+
   ProgramStateRef StTrue = Assume(true);
 
   if (!StTrue) {
     ProgramStateRef StFalse = Assume(false);
     if (LLVM_UNLIKELY(!StFalse)) { // both infeasible
       ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained();
       assert(StInfeasible->isPosteriorlyOverconstrained());
       // Checkers might rely on the API contract that both returned states

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

static NonLoc doRearrangeUnchecked(ProgramStateRef State,
   QualType ResultTy;
   if (BinaryOperator::isComparisonOp(Op))
     ResultTy = SVB.getConditionType();
   else if (BinaryOperator::isAdditiveOp(Op))
     ResultTy = SymTy;
   else
     llvm_unreachable("Operation not suitable for unchecked rearrangement!");
 
-  // FIXME: Can we use assume() without getting into an infinite recursion?
   if (LSym == RSym)
     return SVB.evalBinOpNN(State, Op, nonloc::ConcreteInt(LInt),
                            nonloc::ConcreteInt(RInt), ResultTy)
         .castAs<NonLoc>();
 
   SymbolRef ResultSym = nullptr;
   BinaryOperator::Opcode ResultOp;
   llvm::APSInt ResultInt;
if (Optional<NonLoc> indexV = index.getAs<NonLoc>()) {
                                                        superR, getContext()));
     }
   }
   return UnknownVal();
 }
 
 const llvm::APSInt *SimpleSValBuilder::getKnownValue(ProgramStateRef state,
                                                    SVal V) {
-  V = simplifySVal(state, V);
   if (V.isUnknownOrUndef())
     return nullptr;
 
   if (Optional<loc::ConcreteInt> X = V.getAs<loc::ConcreteInt>())
     return &X->getValue();
 
   if (Optional<nonloc::ConcreteInt> X = V.getAs<nonloc::ConcreteInt>())
     return &X->getValue();
SVal VisitNonLocSymbolVal(nonloc::SymbolVal V) {
       // Simplification is much more costly than computing complexity.
       // For high complexity, it may be not worth it.
       return Visit(V.getSymbol());
     }
 
     SVal VisitSVal(SVal V) { return V; }
   };
 
-  // A crude way of preventing this function from calling itself from evalBinOp.
-  static bool isReentering = false;
-  if (isReentering)
-    return V;
-
-  isReentering = true;
   SVal SimplifiedV = Simplifier(State).Visit(V);
-  isReentering = false;
-
   return SimplifiedV;
 }