SimpleConstraintManager.cpp [plain text]
#include "SimpleConstraintManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
namespace clang {
namespace ento {
SimpleConstraintManager::~SimpleConstraintManager() {}
bool SimpleConstraintManager::canReasonAbout(SVal X) const {
nonloc::SymbolVal *SymVal = dyn_cast<nonloc::SymbolVal>(&X);
if (SymVal && SymVal->isExpression()) {
const SymExpr *SE = SymVal->getSymbol();
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
switch (SIE->getOpcode()) {
case BO_And:
case BO_Or:
case BO_Xor:
return false;
case BO_Mul:
case BO_Div:
case BO_Rem:
case BO_Shl:
case BO_Shr:
return false;
default:
return true;
}
}
return false;
}
return true;
}
ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
DefinedSVal Cond,
bool Assumption) {
if (isa<NonLoc>(Cond))
return assume(state, cast<NonLoc>(Cond), Assumption);
else
return assume(state, cast<Loc>(Cond), Assumption);
}
ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond,
bool assumption) {
state = assumeAux(state, cond, assumption);
if (NotifyAssumeClients && SU)
return SU->processAssume(state, cond, assumption);
return state;
}
ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
Loc Cond, bool Assumption) {
switch (Cond.getSubKind()) {
default:
assert (false && "'Assume' not implemented for this Loc.");
return state;
case loc::MemRegionKind: {
const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion();
const SubRegion *SubR = dyn_cast<SubRegion>(R);
while (SubR) {
if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth();
if (Assumption)
return assumeSymNE(state, SymR->getSymbol(), zero, zero);
else
return assumeSymEQ(state, SymR->getSymbol(), zero, zero);
}
SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
}
}
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;
}
} }
ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
NonLoc cond,
bool assumption) {
state = assumeAux(state, cond, assumption);
if (NotifyAssumeClients && SU)
return SU->processAssume(state, cond, assumption);
return state;
}
static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
switch (op) {
default:
llvm_unreachable("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;
}
}
ProgramStateRef
SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
SymbolRef Sym, bool Assumption) {
BasicValueFactory &BVF = getBasicVals();
QualType T = Sym->getType();
if (!T->isIntegerType())
return State;
const llvm::APSInt &zero = BVF.getValue(0, T);
if (Assumption)
return assumeSymNE(State, Sym, zero, zero);
else
return assumeSymEQ(State, Sym, zero, zero);
}
ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
NonLoc Cond,
bool Assumption) {
if (!canReasonAbout(Cond)) {
SymbolRef sym = Cond.getAsSymExpr();
return assumeAuxForSymbol(state, sym, Assumption);
}
BasicValueFactory &BasicVals = getBasicVals();
switch (Cond.getSubKind()) {
default:
llvm_unreachable("'Assume' not implemented for this NonLoc");
case nonloc::SymbolValKind: {
nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
SymbolRef sym = SV.getSymbol();
assert(sym);
if (!SV.isExpression()) {
return assumeAuxForSymbol(state, sym, Assumption);
} else {
const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
if (!SE)
return assumeAuxForSymbol(state, sym, Assumption);
BinaryOperator::Opcode op = SE->getOpcode();
if (!BinaryOperator::isComparisonOp(op)) {
QualType T = SE->getType();
const llvm::APSInt &zero = BasicVals.getValue(0, T);
op = (Assumption ? BO_NE : BO_EQ);
return assumeSymRel(state, SE, op, zero);
}
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);
} }
static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
BinaryOperator::Opcode Op = SE->getOpcode();
if (Op == BO_Add || Op == BO_Sub) {
Sym = SE->getLHS();
Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
if (Op == BO_Sub)
Adjustment = -Adjustment;
}
}
}
ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef 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.");
BasicValueFactory &BVF = getBasicVals();
APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
SymbolRef Sym = LHS;
llvm::APSInt Adjustment = WraparoundType.getZeroValue();
computeAdjustment(Sym, Adjustment);
APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
switch (op) {
default:
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);
} }
}
}