[PATCH] D126560: [analyzer] Track assume call stack to detect fixpoint

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 433719.
martong marked 3 inline comments as done.
martong edited the summary of this revision.
martong added a comment.

- Add LLVM_UNLIKELY


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D126560/new/

https://reviews.llvm.org/D126560

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


Index: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -320,7 +320,6 @@
   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 @@
 
 const llvm::APSInt *SimpleSValBuilder::getKnownValue(ProgramStateRef state,
                                                    SVal V) {
-  V = simplifySVal(state, V);
   if (V.isUnknownOrUndef())
     return nullptr;
 
@@ -1376,14 +1374,6 @@
     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;
 }
Index: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -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;
@@ -46,6 +47,19 @@
 ConstraintManager::ProgramStatePair
 ConstraintManager::assumeDualImpl(ProgramStateRef &State,
                                   AssumeFunction &Assume) {
+
+  // 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: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -144,6 +144,20 @@
   /// 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;
 


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D126560.433719.patch
Type: text/x-patch
Size: 3457 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20220602/dca6332a/attachment.bin>