Skip to content

Commit

Permalink
[analyzer] Track assume call stack to detect fixpoint
Browse files Browse the repository at this point in the history
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 #55851

Differential Revision: https://reviews.llvm.org/D126560
  • Loading branch information
Gabor Marton committed Jun 7, 2022
1 parent a7b154a commit f66f4d3
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 10 deletions.
Expand Up @@ -144,6 +144,20 @@ class ConstraintManager {
/// 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;

Expand Down
13 changes: 13 additions & 0 deletions clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
Expand Up @@ -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;
Expand Down Expand Up @@ -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) {
Expand Down
10 changes: 0 additions & 10 deletions clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
Expand Up @@ -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)
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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;
}

0 comments on commit f66f4d3

Please sign in to comment.