blob: a4d59bec887381ecc6b880ef0b56b798fd1d7f54 [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::SymIntConstraintVal *Y = dyn_cast<nonloc::SymIntConstraintVal>(&X)) {
const SymIntConstraint& C = Y->getConstraint();
switch (C.getOpcode()) {
// We don't reason yet about bitwise-constraints on symbolic values.
case BinaryOperator::And:
case BinaryOperator::Or:
case BinaryOperator::Xor:
return false;
default:
return true;
}
}
return true;
}
const GRState*
SimpleConstraintManager::Assume(const GRState* St, SVal Cond, bool Assumption,
bool& isFeasible) {
if (Cond.isUnknown()) {
isFeasible = true;
return St;
}
if (isa<NonLoc>(Cond))
return Assume(St, cast<NonLoc>(Cond), Assumption, isFeasible);
else
return Assume(St, cast<Loc>(Cond), Assumption, isFeasible);
}
const GRState*
SimpleConstraintManager::Assume(const GRState* St, Loc Cond, bool Assumption,
bool& isFeasible) {
St = AssumeAux(St, Cond, Assumption, isFeasible);
if (!isFeasible)
return St;
// 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 StateMgr.getTransferFuncs().EvalAssume(StateMgr, St, Cond, Assumption,
isFeasible);
}
const GRState*
SimpleConstraintManager::AssumeAux(const GRState* St, Loc Cond, bool Assumption,
bool& isFeasible) {
BasicValueFactory& BasicVals = StateMgr.getBasicVals();
switch (Cond.getSubKind()) {
default:
assert (false && "'Assume' not implemented for this Loc.");
return St;
case loc::SymbolValKind:
if (Assumption)
return AssumeSymNE(St, cast<loc::SymbolVal>(Cond).getSymbol(),
BasicVals.getZeroWithPtrWidth(), isFeasible);
else
return AssumeSymEQ(St, cast<loc::SymbolVal>(Cond).getSymbol(),
BasicVals.getZeroWithPtrWidth(), isFeasible);
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))
return AssumeAux(St, loc::SymbolVal(SymR->getSymbol()), Assumption,
isFeasible);
SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
}
// FALL-THROUGH.
}
case loc::FuncValKind:
case loc::GotoLabelKind:
isFeasible = Assumption;
return St;
case loc::ConcreteIntKind: {
bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
isFeasible = b ? Assumption : !Assumption;
return St;
}
} // end switch
}
const GRState*
SimpleConstraintManager::Assume(const GRState* St, NonLoc Cond, bool Assumption,
bool& isFeasible) {
St = AssumeAux(St, Cond, Assumption, isFeasible);
if (!isFeasible)
return St;
// 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 StateMgr.getTransferFuncs().EvalAssume(StateMgr, St, Cond, Assumption,
isFeasible);
}
const GRState*
SimpleConstraintManager::AssumeAux(const GRState* St,NonLoc Cond,
bool Assumption, bool& isFeasible) {
BasicValueFactory& BasicVals = StateMgr.getBasicVals();
SymbolManager& SymMgr = StateMgr.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);
if (Assumption)
return AssumeSymNE(St, sym, BasicVals.getValue(0, T), isFeasible);
else
return AssumeSymEQ(St, sym, BasicVals.getValue(0, T), isFeasible);
}
case nonloc::SymIntConstraintValKind:
return
AssumeSymInt(St, Assumption,
cast<nonloc::SymIntConstraintVal>(Cond).getConstraint(),
isFeasible);
case nonloc::ConcreteIntKind: {
bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
isFeasible = b ? Assumption : !Assumption;
return St;
}
case nonloc::LocAsIntegerKind:
return AssumeAux(St, cast<nonloc::LocAsInteger>(Cond).getLoc(),
Assumption, isFeasible);
} // end switch
}
const GRState*
SimpleConstraintManager::AssumeSymInt(const GRState* St, bool Assumption,
const SymIntConstraint& C,
bool& isFeasible) {
switch (C.getOpcode()) {
default:
// No logic yet for other operators.
isFeasible = true;
return St;
case BinaryOperator::EQ:
if (Assumption)
return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
else
return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
case BinaryOperator::NE:
if (Assumption)
return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
else
return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
case BinaryOperator::GT:
if (Assumption)
return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
else
return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
case BinaryOperator::GE:
if (Assumption)
return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
else
return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
case BinaryOperator::LT:
if (Assumption)
return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
else
return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
case BinaryOperator::LE:
if (Assumption)
return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
else
return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
} // end switch
}
const GRState*
SimpleConstraintManager::AssumeInBound(const GRState* St, SVal Idx,
SVal UpperBound, bool Assumption,
bool& isFeasible) {
// Only support ConcreteInt for now.
if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound))){
isFeasible = true;
return St;
}
const llvm::APSInt& Zero = 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);
isFeasible = Assumption ? InBound : !InBound;
return St;
}
} // end of namespace clang