Remove ProgramState::getSymVal(). It was being misused by Checkers,

with at least one subtle bug in MacOSXKeyChainAPIChecker where the
calling the method was a substitute for assuming a symbolic value
was null (which is not the case).

We still keep ConstraintManager::getSymVal(), but we use that as
an optimization in SValBuilder and ProgramState::getSVal() to
constant-fold SVals.  This is only if the ConstraintManager can
provide us with that information, which is no longer a requirement.
As part of this, introduce a default implementation of
ConstraintManager::getSymVal() which returns null.

For Checkers, introduce ConstraintManager::isNull(), which queries
the state to see if the symbolic value is constrained to be a null
value.  It does this without assuming it has been implicitly constant
folded.

llvm-svn: 163428
This commit is contained in:
Ted Kremenek 2012-09-07 22:31:01 +00:00
parent 334ad6ac13
commit 244e1d7d0f
10 changed files with 128 additions and 40 deletions

View File

@ -26,19 +26,52 @@ namespace ento {
class SubEngine;
class ConditionTruthVal {
llvm::Optional<bool> Val;
public:
/// Construct a ConditionTruthVal indicating the constraint is constrained
/// to either true or false, depending on the boolean value provided.
ConditionTruthVal(bool constraint) : Val(constraint) {}
/// Construct a ConstraintVal indicating the constraint is underconstrained.
ConditionTruthVal() {}
/// Return true if the constraint is perfectly constrained to 'true'.
bool isTrue() const {
return Val.hasValue() && Val.getValue();
}
/// Return true if the constraint is perfectly constrained to 'false'.
bool isFalse() const {
return Val.hasValue() && !Val.getValue();
}
/// Return true if the constrained is perfectly constrained.
bool isConstrained() const {
return Val.hasValue();
}
/// Return true if the constrained is underconstrained and we do not know
/// if the constraint is true of value.
bool isUnderconstrained() const {
return !Val.hasValue();
}
};
class ConstraintManager {
public:
ConstraintManager() : NotifyAssumeClients(true) {}
virtual ~ConstraintManager();
virtual ProgramStateRef assume(ProgramStateRef state,
DefinedSVal Cond,
bool Assumption) = 0;
std::pair<ProgramStateRef, ProgramStateRef >
assumeDual(ProgramStateRef state, DefinedSVal Cond)
{
std::pair<ProgramStateRef, ProgramStateRef > res =
std::make_pair(assume(state, Cond, true), assume(state, Cond, false));
DefinedSVal Cond,
bool Assumption) = 0;
typedef std::pair<ProgramStateRef, ProgramStateRef> ProgramStatePair;
ProgramStatePair assumeDual(ProgramStateRef state, DefinedSVal Cond) {
ProgramStatePair res(assume(state, Cond, true),
assume(state, Cond, false));
assert(!(!res.first && !res.second) && "System is over constrained.");
return res;
}
@ -62,8 +95,20 @@ public:
const char *sep) = 0;
virtual void EndPath(ProgramStateRef state) {}
/// Convenience method to query the state to see if a symbol is null or
/// not null, or neither assumption can be made.
ConditionTruthVal isNull(ProgramStateRef State, SymbolRef 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;
/// canReasonAbout - Not all ConstraintManagers can accurately reason about
/// all SVal values. This method returns true if the ConstraintManager can
/// reasonably handle a given SVal value. This is typically queried by

View File

@ -105,7 +105,12 @@ public:
~ProgramState();
/// Return the ProgramStateManager associated with this state.
ProgramStateManager &getStateManager() const { return *stateMgr; }
ProgramStateManager &getStateManager() const {
return *stateMgr;
}
/// Return the ConstraintManager.
ConstraintManager &getConstraintManager() const;
/// getEnvironment - Return the environment associated with this state.
/// The environment is the mapping from expressions to values.
@ -246,8 +251,6 @@ public:
/// Get the lvalue for an array index.
SVal getLValue(QualType ElementType, SVal Idx, SVal Base) const;
const llvm::APSInt *getSymVal(SymbolRef sym) const;
/// Returns the SVal bound to the statement 'S' in the state's environment.
SVal getSVal(const Stmt *S, const LocationContext *LCtx,
bool useOnlyDirectBindings = false) const;
@ -592,10 +595,6 @@ public:
return ProgramStateTrait<T>::MakeContext(p);
}
const llvm::APSInt* getSymVal(ProgramStateRef St, SymbolRef sym) {
return ConstraintMgr->getSymVal(St, sym);
}
void EndPath(ProgramStateRef St) {
ConstraintMgr->EndPath(St);
}
@ -606,6 +605,10 @@ public:
// Out-of-line method definitions for ProgramState.
//===----------------------------------------------------------------------===//
inline ConstraintManager &ProgramState::getConstraintManager() const {
return stateMgr->getConstraintManager();
}
inline const VarRegion* ProgramState::getRegion(const VarDecl *D,
const LocationContext *LC) const
{
@ -670,10 +673,6 @@ inline SVal ProgramState::getLValue(QualType ElementType, SVal Idx, SVal Base) c
return UnknownVal();
}
inline const llvm::APSInt *ProgramState::getSymVal(SymbolRef sym) const {
return getStateManager().getSymVal(this, sym);
}
inline SVal ProgramState::getSVal(const Stmt *Ex, const LocationContext *LCtx,
bool useOnlyDirectBindings) const{
return Env.getSVal(EnvironmentEntry(Ex, LCtx),

View File

@ -585,7 +585,7 @@ void MacOSKeychainAPIChecker::checkDeadSymbols(SymbolReaper &SR,
State = State->remove<AllocatedData>(I->first);
// If the allocated symbol is null or if the allocation call might have
// returned an error, do not report.
if (State->getSymVal(I->first) ||
if (State->getConstraintManager().isNull(State, I->first).isTrue() ||
definitelyReturnedError(I->second.Region, State, C.getSValBuilder()))
continue;
Errors.push_back(std::make_pair(I->first, &I->second));
@ -630,7 +630,7 @@ void MacOSKeychainAPIChecker::checkEndPath(CheckerContext &C) const {
state = state->remove<AllocatedData>(I->first);
// If the allocated symbol is null or if error code was returned at
// allocation, do not report.
if (state->getSymVal(I.getKey()) ||
if (state->getConstraintManager().isNull(state, I.getKey()).isTrue() ||
definitelyReturnedError(I->second.Region, state,
C.getSValBuilder())) {
continue;

View File

@ -1275,9 +1275,8 @@ ProgramStateRef MallocChecker::evalAssume(ProgramStateRef state,
bool Assumption) const {
RegionStateTy RS = state->get<RegionState>();
for (RegionStateTy::iterator I = RS.begin(), E = RS.end(); I != E; ++I) {
// If the symbol is assumed to NULL or another constant, this will
// return an APSInt*.
if (state->getSymVal(I.getKey()))
// If the symbol is assumed to be NULL, remove it from consideration.
if (state->getConstraintManager().isNull(state, I.getKey()).isTrue())
state = state->remove<RegionState>(I.getKey());
}
@ -1285,12 +1284,10 @@ ProgramStateRef MallocChecker::evalAssume(ProgramStateRef state,
// restore the state of the pointer being reallocated.
ReallocMap RP = state->get<ReallocPairs>();
for (ReallocMap::iterator I = RP.begin(), E = RP.end(); I != E; ++I) {
// If the symbol is assumed to NULL or another constant, this will
// return an APSInt*.
if (state->getSymVal(I.getKey())) {
// If the symbol is assumed to be NULL, remove it from consideration.
if (state->getConstraintManager().isNull(state, I.getKey()).isTrue()) {
SymbolRef ReallocSym = I.getData().ReallocatedSym;
const RefState *RS = state->get<RegionState>(ReallocSym);
if (RS) {
if (const RefState *RS = state->get<RegionState>(ReallocSym)) {
if (RS->isReleased() && ! I.getData().IsFreeOnFailure)
state = state->set<RegionState>(ReallocSym,
RefState::getAllocated(RS->getStmt()));

View File

@ -3445,9 +3445,8 @@ ProgramStateRef RetainCountChecker::evalAssume(ProgramStateRef state,
RefBindings::Factory &RefBFactory = state->get_context<RefBindings>();
for (RefBindings::iterator I = B.begin(), E = B.end(); I != E; ++I) {
// Check if the symbol is null (or equal to any constant).
// If this is the case, stop tracking the symbol.
if (state->getSymVal(I.getKey())) {
// Check if the symbol is null stop tracking the symbol.
if (state->getConstraintManager().isNull(state, I.getKey()).isTrue()) {
changed = true;
B = RefBFactory.remove(B, I.getKey());
}

View File

@ -14,6 +14,7 @@ add_clang_library(clangStaticAnalyzerCore
CheckerHelpers.cpp
CheckerManager.cpp
CheckerRegistry.cpp
ConstraintManager.cpp
CoreEngine.cpp
Environment.cpp
ExplodedGraph.cpp

View File

@ -0,0 +1,46 @@
//== ConstraintManager.cpp - Constraints on symbolic values -----*- C++ -*--==//
//
// The LLVM Compiler Infrastructure
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
//
// This file defined the interface to manage constraints on symbolic values.
//
//===----------------------------------------------------------------------===//
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
#include "llvm/Support/SaveAndRestore.h"
using namespace clang;
using namespace ento;
ConstraintManager::~ConstraintManager() {}
static DefinedSVal getLocFromSymbol(const ProgramStateRef &State,
SymbolRef Sym) {
const MemRegion *R = State->getStateManager().getRegionManager()
.getSymbolicRegion(Sym);
return loc::MemRegionVal(R);
}
/// Convenience method to query the state to see if a symbol is null or
/// not null, or neither assumption can be made.
ConditionTruthVal ConstraintManager::isNull(ProgramStateRef State,
SymbolRef Sym) {
// Disable recursive notification of clients.
llvm::SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
ProgramStateManager &Mgr = State->getStateManager();
QualType Ty = Sym->getType(Mgr.getContext());
DefinedSVal V = Loc::isLocType(Ty) ? getLocFromSymbol(State, Sym)
: nonloc::SymbolVal(Sym);
const ProgramStatePair &P = assumeDual(State, V);
if (P.first && !P.second)
return ConditionTruthVal(false);
if (!P.first && P.second)
return ConditionTruthVal(true);
return ConditionTruthVal();
}

View File

@ -22,10 +22,6 @@
using namespace clang;
using namespace ento;
// Give the vtable for ConstraintManager somewhere to live.
// FIXME: Move this elsewhere.
ConstraintManager::~ConstraintManager() {}
namespace clang { namespace ento {
/// Increments the number of times this state is referenced.
@ -238,7 +234,9 @@ SVal ProgramState::getSVal(Loc location, QualType T) const {
// about).
if (!T.isNull()) {
if (SymbolRef sym = V.getAsSymbol()) {
if (const llvm::APSInt *Int = getSymVal(sym)) {
if (const llvm::APSInt *Int = getStateManager()
.getConstraintManager()
.getSymVal(this, sym)) {
// FIXME: Because we don't correctly model (yet) sign-extension
// and truncation of symbolic values, we need to convert
// the integer value to the correct signedness and bitwidth.

View File

@ -67,7 +67,9 @@ ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond,
bool assumption) {
state = assumeAux(state, cond, assumption);
return SU.processAssume(state, cond, assumption);
if (NotifyAssumeClients)
return SU.processAssume(state, cond, assumption);
return state;
}
ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,

View File

@ -507,7 +507,8 @@ SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state,
} else if (isa<SymbolData>(Sym)) {
// Does the symbol simplify to a constant? If so, "fold" the constant
// by setting 'lhs' to a ConcreteInt and try again.
if (const llvm::APSInt *Constant = state->getSymVal(Sym)) {
if (const llvm::APSInt *Constant = state->getConstraintManager()
.getSymVal(state, Sym)) {
lhs = nonloc::ConcreteInt(*Constant);
continue;
}
@ -942,7 +943,7 @@ const llvm::APSInt *SimpleSValBuilder::getKnownValue(ProgramStateRef state,
return &X->getValue();
if (SymbolRef Sym = V.getAsSymbol())
return state->getSymVal(Sym);
return state->getConstraintManager().getSymVal(state, Sym);
// FIXME: Add support for SymExprs.
return NULL;