[analyzer] Track assume call stack to detect fixpoint
authorGabor Marton <gabor.marton@ericsson.com>
Fri, 27 May 2022 18:44:43 +0000 (20:44 +0200)
committerGabor Marton <gabor.marton@ericsson.com>
Tue, 7 Jun 2022 06:36:11 +0000 (08:36 +0200)
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.

Fixes https://github.com/llvm/llvm-project/issues/55851

Differential Revision: https://reviews.llvm.org/D126560

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

index d1e0629..de08ac5 100644 (file)
@@ -144,6 +144,20 @@ protected:
   /// 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;
 
index 8b04d3d..bfda967 100644 (file)
@@ -16,6 +16,7 @@
 #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;
@@ -49,6 +50,18 @@ ConstraintManager::assumeDualImpl(ProgramStateRef &State,
   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) {
index 1232dcc..3922511 100644 (file)
@@ -320,7 +320,6 @@ static NonLoc doRearrangeUnchecked(ProgramStateRef State,
   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)
@@ -1190,7 +1189,6 @@ SVal SimpleSValBuilder::evalBinOpLN(ProgramStateRef state,
 
 const llvm::APSInt *SimpleSValBuilder::getKnownValue(ProgramStateRef state,
                                                    SVal V) {
-  V = simplifySVal(state, V);
   if (V.isUnknownOrUndef())
     return nullptr;
 
@@ -1384,14 +1382,6 @@ SVal SimpleSValBuilder::simplifySValOnce(ProgramStateRef State, SVal V) {
     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;
 }