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
/// 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;
#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;
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) {
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)
const llvm::APSInt *SimpleSValBuilder::getKnownValue(ProgramStateRef state,
SVal V) {
- V = simplifySVal(state, V);
if (V.isUnknownOrUndef())
return nullptr;
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;
}