blob: 04496e1e3332ab9eb3825becd596fcf3f05f3012 [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/Checker/PathSensitive/GRExprEngine.h"
#include "clang/Checker/PathSensitive/GRState.h"
#include "clang/Checker/PathSensitive/Checker.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 BO_And:
case BO_Or:
case BO_Xor:
return false;
// We don't reason yet about these arithmetic constraints on
// symbolic values.
case BO_Mul:
case BO_Div:
case BO_Rem:
case BO_Shl:
case BO_Shr:
return false;
// All other cases.
default:
return true;
}
}
return false;
}
return true;
}
const GRState *SimpleConstraintManager::Assume(const GRState *state,
DefinedSVal Cond,
bool Assumption) {
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);
return SU.ProcessAssume(state, cond, assumption);
}
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)) {
const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth();
if (Assumption)
return AssumeSymNE(state, SymR->getSymbol(), zero, zero);
else
return AssumeSymEQ(state, SymR->getSymbol(), zero, zero);
}
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);
return SU.ProcessAssume(state, cond, assumption);
}
static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
// FIXME: This should probably be part of BinaryOperator, since this isn't
// the only place it's used. (This code was copied from SimpleSValuator.cpp.)
switch (op) {
default:
assert(false && "Invalid opcode.");
case BO_LT: return BO_GE;
case BO_GT: return BO_LE;
case BO_LE: return BO_GT;
case BO_GE: return BO_LT;
case BO_EQ: return BO_NE;
case BO_NE: return BO_EQ;
}
}
const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
NonLoc Cond,
bool Assumption) {
// We cannot reason about SymSymExprs,
// and can only reason about some SymIntExprs.
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);
if (Assumption)
return AssumeSymNE(state, sym, zero, zero);
else
return AssumeSymEQ(state, sym, zero, zero);
}
case nonloc::SymExprValKind: {
nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
// For now, we only handle expressions whose RHS is an integer.
// All other expressions are assumed to be feasible.
const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression());
if (!SE)
return state;
BinaryOperator::Opcode op = SE->getOpcode();
// Implicitly compare non-comparison expressions to 0.
if (!BinaryOperator::isComparisonOp(op)) {
QualType T = SymMgr.getType(SE);
const llvm::APSInt &zero = BasicVals.getValue(0, T);
op = (Assumption ? BO_NE : BO_EQ);
return AssumeSymRel(state, SE, op, zero);
}
// From here on out, op is the real comparison we'll be testing.
if (!Assumption)
op = NegateComparison(op);
return AssumeSymRel(state, SE->getLHS(), op, SE->getRHS());
}
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::AssumeSymRel(const GRState *state,
const SymExpr *LHS,
BinaryOperator::Opcode op,
const llvm::APSInt& Int) {
assert(BinaryOperator::isComparisonOp(op) &&
"Non-comparison ops should be rewritten as comparisons to zero.");
// We only handle simple comparisons of the form "$sym == constant"
// or "($sym+constant1) == constant2".
// The adjustment is "constant1" in the above expression. It's used to
// "slide" the solution range around for modular arithmetic. For example,
// x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
// in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
// the subclasses of SimpleConstraintManager to handle the adjustment.
llvm::APSInt Adjustment;
// First check if the LHS is a simple symbol reference.
SymbolRef Sym = dyn_cast<SymbolData>(LHS);
if (Sym) {
Adjustment = 0;
} else {
// Next, see if it's a "($sym+constant1)" expression.
const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
// We don't handle "($sym1+$sym2)".
// Give up and assume the constraint is feasible.
if (!SE)
return state;
// We don't handle "(<expr>+constant1)".
// Give up and assume the constraint is feasible.
Sym = dyn_cast<SymbolData>(SE->getLHS());
if (!Sym)
return state;
// Get the constant out of the expression "($sym+constant1)".
switch (SE->getOpcode()) {
case BO_Add:
Adjustment = SE->getRHS();
break;
case BO_Sub:
Adjustment = -SE->getRHS();
break;
default:
// We don't handle non-additive operators.
// Give up and assume the constraint is feasible.
return state;
}
}
// FIXME: This next section is a hack. It silently converts the integers to
// be of the same type as the symbol, which is not always correct. Really the
// comparisons should be performed using the Int's type, then mapped back to
// the symbol's range of values.
GRStateManager &StateMgr = state->getStateManager();
ASTContext &Ctx = StateMgr.getContext();
QualType T = Sym->getType(Ctx);
assert(T->isIntegerType() || Loc::IsLocType(T));
unsigned bitwidth = Ctx.getTypeSize(T);
bool isSymUnsigned = T->isUnsignedIntegerType() || Loc::IsLocType(T);
// Convert the adjustment.
Adjustment.setIsUnsigned(isSymUnsigned);
Adjustment.extOrTrunc(bitwidth);
// Convert the right-hand side integer.
llvm::APSInt ConvertedInt(Int, isSymUnsigned);
ConvertedInt.extOrTrunc(bitwidth);
switch (op) {
default:
// No logic yet for other operators. Assume the constraint is feasible.
return state;
case BO_EQ:
return AssumeSymEQ(state, Sym, ConvertedInt, Adjustment);
case BO_NE:
return AssumeSymNE(state, Sym, ConvertedInt, Adjustment);
case BO_GT:
return AssumeSymGT(state, Sym, ConvertedInt, Adjustment);
case BO_GE:
return AssumeSymGE(state, Sym, ConvertedInt, Adjustment);
case BO_LT:
return AssumeSymLT(state, Sym, ConvertedInt, Adjustment);
case BO_LE:
return AssumeSymLE(state, Sym, ConvertedInt, Adjustment);
} // end switch
}
} // end of namespace clang