312 lines
10 KiB
C++
312 lines
10 KiB
C++
//== 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/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()) {
|
|
// 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 ProgramState *SimpleConstraintManager::assume(const ProgramState *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 ProgramState *SimpleConstraintManager::assume(const ProgramState *state, Loc cond,
|
|
bool assumption) {
|
|
state = assumeAux(state, cond, assumption);
|
|
return SU.processAssume(state, cond, assumption);
|
|
}
|
|
|
|
const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *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 ProgramState *SimpleConstraintManager::assume(const ProgramState *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 SimpleSValBuilder.cpp.)
|
|
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;
|
|
}
|
|
}
|
|
|
|
|
|
const ProgramState *SimpleConstraintManager::assumeAuxForSymbol(
|
|
const ProgramState *State,
|
|
SymbolRef Sym,
|
|
bool Assumption) {
|
|
QualType T = State->getSymbolManager().getType(Sym);
|
|
const llvm::APSInt &zero = State->getBasicVals().getValue(0, T);
|
|
if (Assumption)
|
|
return assumeSymNE(State, Sym, zero, zero);
|
|
else
|
|
return assumeSymEQ(State, Sym, zero, zero);
|
|
}
|
|
|
|
const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state,
|
|
NonLoc Cond,
|
|
bool Assumption) {
|
|
|
|
// We cannot reason about SymSymExprs, and can only reason about some
|
|
// SymIntExprs.
|
|
if (!canReasonAbout(Cond)) {
|
|
// Just add the constraint to the expression without trying to simplify.
|
|
SymbolRef sym = Cond.getAsSymExpr();
|
|
return assumeAuxForSymbol(state, sym, Assumption);
|
|
}
|
|
|
|
BasicValueFactory &BasicVals = state->getBasicVals();
|
|
SymbolManager &SymMgr = state->getSymbolManager();
|
|
|
|
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);
|
|
|
|
// Handle SymbolData.
|
|
if (!SV.isExpression()) {
|
|
return assumeAuxForSymbol(state, sym, Assumption);
|
|
|
|
// Handle symbolic expression.
|
|
} else {
|
|
// We can only simplify expressions whose RHS is an integer.
|
|
const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
|
|
if (!SE)
|
|
return assumeAuxForSymbol(state, sym, Assumption);
|
|
|
|
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
|
|
}
|
|
|
|
static llvm::APSInt computeAdjustment(const SymExpr *LHS,
|
|
SymbolRef &Sym) {
|
|
llvm::APSInt DefaultAdjustment;
|
|
DefaultAdjustment = 0;
|
|
|
|
// First check if the LHS is a simple symbol reference.
|
|
if (isa<SymbolData>(LHS))
|
|
return DefaultAdjustment;
|
|
|
|
// Next, see if it's a "($sym+constant1)" expression.
|
|
const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
|
|
|
|
// We cannot simplify "($sym1+$sym2)".
|
|
if (!SE)
|
|
return DefaultAdjustment;
|
|
|
|
// Get the constant out of the expression "($sym+constant1)" or
|
|
// "<expr>+constant1".
|
|
Sym = SE->getLHS();
|
|
switch (SE->getOpcode()) {
|
|
case BO_Add:
|
|
return SE->getRHS();
|
|
break;
|
|
case BO_Sub:
|
|
return -SE->getRHS();
|
|
break;
|
|
default:
|
|
// We cannot simplify non-additive operators.
|
|
return DefaultAdjustment;
|
|
}
|
|
|
|
return DefaultAdjustment;
|
|
}
|
|
|
|
const ProgramState *SimpleConstraintManager::assumeSymRel(const ProgramState *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.
|
|
SymbolRef Sym = LHS;
|
|
llvm::APSInt Adjustment = computeAdjustment(LHS, Sym);
|
|
|
|
// 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.
|
|
ProgramStateManager &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->isUnsignedIntegerOrEnumerationType() || Loc::isLocType(T);
|
|
|
|
// Convert the adjustment.
|
|
Adjustment.setIsUnsigned(isSymUnsigned);
|
|
Adjustment = Adjustment.extOrTrunc(bitwidth);
|
|
|
|
// Convert the right-hand side integer.
|
|
llvm::APSInt ConvertedInt(Int, isSymUnsigned);
|
|
ConvertedInt = 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 ento
|
|
|
|
} // end of namespace clang
|