blob: 82801eb05d38369c69ddc26a10f834a50609517a [file] [log] [blame]
//== SimpleConstraintManager.cpp --------------------------------*- C++ -*--==//
//
// The LLVM Compiler Infrastructure
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
//
// This file defines SimpleConstraintManager, a class that holds code shared
// between BasicConstraintManager and RangeConstraintManager.
//
//===----------------------------------------------------------------------===//
#include "SimpleConstraintManager.h"
#include "clang/Analysis/PathSensitive/GRExprEngine.h"
#include "clang/Analysis/PathSensitive/GRState.h"
namespace clang {
SimpleConstraintManager::~SimpleConstraintManager() {}
bool SimpleConstraintManager::canReasonAbout(SVal X) const {
if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) {
const SymExpr *SE = SymVal->getSymbolicExpression();
if (isa<SymbolData>(SE))
return true;
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
switch (SIE->getOpcode()) {
// We don't reason yet about bitwise-constraints on symbolic values.
case BinaryOperator::And:
case BinaryOperator::Or:
case BinaryOperator::Xor:
return false;
// We don't reason yet about arithmetic constraints on symbolic values.
case BinaryOperator::Mul:
case BinaryOperator::Div:
case BinaryOperator::Rem:
case BinaryOperator::Add:
case BinaryOperator::Sub:
case BinaryOperator::Shl:
case BinaryOperator::Shr:
return false;
// All other cases.
default:
return true;
}
}
return false;
}
return true;
}
const GRState *SimpleConstraintManager::Assume(const GRState *state,
SVal Cond, bool Assumption) {
if (Cond.isUnknown()) {
return state;
}
if (isa<NonLoc>(Cond))
return Assume(state, cast<NonLoc>(Cond), Assumption);
else
return Assume(state, cast<Loc>(Cond), Assumption);
}
const GRState *SimpleConstraintManager::Assume(const GRState *state, Loc Cond,
bool Assumption) {
state = AssumeAux(state, Cond, Assumption);
// EvalAssume is used to call into the GRTransferFunction object to perform
// any checker-specific update of the state based on this assumption being
// true or false.
return state ? state->getTransferFuncs().EvalAssume(state, Cond, Assumption)
: NULL;
}
const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
Loc Cond, bool Assumption) {
BasicValueFactory &BasicVals = state->getBasicVals();
switch (Cond.getSubKind()) {
default:
assert (false && "'Assume' not implemented for this Loc.");
return state;
case loc::MemRegionKind: {
// FIXME: Should this go into the storemanager?
const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion();
const SubRegion *SubR = dyn_cast<SubRegion>(R);
while (SubR) {
// FIXME: now we only find the first symbolic region.
if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
if (Assumption)
return AssumeSymNE(state, SymR->getSymbol(),
BasicVals.getZeroWithPtrWidth());
else
return AssumeSymEQ(state, SymR->getSymbol(),
BasicVals.getZeroWithPtrWidth());
}
SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
}
// FALL-THROUGH.
}
case loc::GotoLabelKind:
return Assumption ? state : NULL;
case loc::ConcreteIntKind: {
bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
bool isFeasible = b ? Assumption : !Assumption;
return isFeasible ? state : NULL;
}
} // end switch
}
const GRState *SimpleConstraintManager::Assume(const GRState *state,
NonLoc Cond,
bool Assumption) {
state = AssumeAux(state, Cond, Assumption);
// EvalAssume is used to call into the GRTransferFunction object to perform
// any checker-specific update of the state based on this assumption being
// true or false.
return state ? state->getTransferFuncs().EvalAssume(state, Cond, Assumption)
: NULL;
}
const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
NonLoc Cond,
bool Assumption) {
// We cannot reason about SymIntExpr and SymSymExpr.
if (!canReasonAbout(Cond)) {
// Just return the current state indicating that the path is feasible.
// This may be an over-approximation of what is possible.
return state;
}
BasicValueFactory &BasicVals = state->getBasicVals();
SymbolManager &SymMgr = state->getSymbolManager();
switch (Cond.getSubKind()) {
default:
assert(false && "'Assume' not implemented for this NonLoc");
case nonloc::SymbolValKind: {
nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
SymbolRef sym = SV.getSymbol();
QualType T = SymMgr.getType(sym);
const llvm::APSInt &zero = BasicVals.getValue(0, T);
return Assumption ? AssumeSymNE(state, sym, zero)
: AssumeSymEQ(state, sym, zero);
}
case nonloc::SymExprValKind: {
nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression()))
return AssumeSymInt(state, Assumption, SE);
// For all other symbolic expressions, over-approximate and consider
// the constraint feasible.
return state;
}
case nonloc::ConcreteIntKind: {
bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
bool isFeasible = b ? Assumption : !Assumption;
return isFeasible ? state : NULL;
}
case nonloc::LocAsIntegerKind:
return AssumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
Assumption);
} // end switch
}
const GRState *SimpleConstraintManager::AssumeSymInt(const GRState *state,
bool Assumption,
const SymIntExpr *SE) {
// Here we assume that LHS is a symbol. This is consistent with the
// rest of the constraint manager logic.
SymbolRef Sym = cast<SymbolData>(SE->getLHS());
const llvm::APSInt &Int = SE->getRHS();
switch (SE->getOpcode()) {
default:
// No logic yet for other operators. Assume the constraint is feasible.
return state;
case BinaryOperator::EQ:
return Assumption ? AssumeSymEQ(state, Sym, Int)
: AssumeSymNE(state, Sym, Int);
case BinaryOperator::NE:
return Assumption ? AssumeSymNE(state, Sym, Int)
: AssumeSymEQ(state, Sym, Int);
case BinaryOperator::GT:
return Assumption ? AssumeSymGT(state, Sym, Int)
: AssumeSymLE(state, Sym, Int);
case BinaryOperator::GE:
return Assumption ? AssumeSymGE(state, Sym, Int)
: AssumeSymLT(state, Sym, Int);
case BinaryOperator::LT:
return Assumption ? AssumeSymLT(state, Sym, Int)
: AssumeSymGE(state, Sym, Int);
case BinaryOperator::LE:
return Assumption ? AssumeSymLE(state, Sym, Int)
: AssumeSymGT(state, Sym, Int);
} // end switch
}
const GRState *SimpleConstraintManager::AssumeInBound(const GRState *state,
SVal Idx,
SVal UpperBound,
bool Assumption) {
// Only support ConcreteInt for now.
if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound)))
return state;
const llvm::APSInt& Zero = state->getBasicVals().getZeroWithPtrWidth(false);
llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue();
// IdxV might be too narrow.
if (IdxV.getBitWidth() < Zero.getBitWidth())
IdxV.extend(Zero.getBitWidth());
// UBV might be too narrow, too.
llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue();
if (UBV.getBitWidth() < Zero.getBitWidth())
UBV.extend(Zero.getBitWidth());
bool InBound = (Zero <= IdxV) && (IdxV < UBV);
bool isFeasible = Assumption ? InBound : !InBound;
return isFeasible ? state : NULL;
}
} // end of namespace clang