if (!SE)
return state;
- GRStateManager &StateMgr = state->getStateManager();
- ASTContext &Ctx = StateMgr.getContext();
- BasicValueFactory &BasicVals = StateMgr.getBasicVals();
-
- // FIXME: This is a hack. It silently converts the RHS integer to be
- // of the same type as on the left side. This should be removed once
- // we support truncation/extension of symbolic values.
- const SymExpr *LHS = SE->getLHS();
- QualType LHSType = LHS->getType(Ctx);
- const llvm::APSInt &RHS = BasicVals.Convert(LHSType, SE->getRHS());
-
BinaryOperator::Opcode op = SE->getOpcode();
// FIXME: We should implicitly compare non-comparison expressions to 0.
if (!BinaryOperator::isComparisonOp(op))
if (!Assumption)
op = NegateComparison(op);
- return AssumeSymRel(state, LHS, op, RHS);
+ return AssumeSymRel(state, SE->getLHS(), op, SE->getRHS());
}
case nonloc::ConcreteIntKind: {
// 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(Int.getBitWidth(), Int.isUnsigned());
+ llvm::APSInt Adjustment;
// First check if the LHS is a simple symbol reference.
SymbolRef Sym = dyn_cast<SymbolData>(LHS);
- if (!Sym) {
+ if (Sym) {
+ Adjustment = 0;
+ } else {
// Next, see if it's a "($sym+constant1)" expression.
const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
}
}
+ // 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 BinaryOperator::EQ:
- return AssumeSymEQ(state, Sym, Int, Adjustment);
+ return AssumeSymEQ(state, Sym, ConvertedInt, Adjustment);
case BinaryOperator::NE:
- return AssumeSymNE(state, Sym, Int, Adjustment);
+ return AssumeSymNE(state, Sym, ConvertedInt, Adjustment);
case BinaryOperator::GT:
- return AssumeSymGT(state, Sym, Int, Adjustment);
+ return AssumeSymGT(state, Sym, ConvertedInt, Adjustment);
case BinaryOperator::GE:
- return AssumeSymGE(state, Sym, Int, Adjustment);
+ return AssumeSymGE(state, Sym, ConvertedInt, Adjustment);
case BinaryOperator::LT:
- return AssumeSymLT(state, Sym, Int, Adjustment);
+ return AssumeSymLT(state, Sym, ConvertedInt, Adjustment);
case BinaryOperator::LE:
- return AssumeSymLE(state, Sym, Int, Adjustment);
+ return AssumeSymLE(state, Sym, ConvertedInt, Adjustment);
} // end switch
}
BinaryOperator::Opcode lop = symIntExpr->getOpcode();
if (BinaryOperator::isAdditiveOp(lop)) {
BasicValueFactory &BVF = ValMgr.getBasicValueFactory();
+
+ // resultTy may not be the best type to convert to, but it's
+ // probably the best choice in expressions with mixed type
+ // (such as x+1U+2LL). The rules for implicit conversions should
+ // choose a reasonable type to preserve the expression, and will
+ // at least match how the value is going to be used.
+ const llvm::APSInt &first =
+ BVF.Convert(resultTy, symIntExpr->getRHS());
+ const llvm::APSInt &second =
+ BVF.Convert(resultTy, rhsInt->getValue());
+
const llvm::APSInt *newRHS;
if (lop == op)
- newRHS = BVF.EvaluateAPSInt(BinaryOperator::Add,
- symIntExpr->getRHS(),
- rhsInt->getValue());
+ newRHS = BVF.EvaluateAPSInt(BinaryOperator::Add, first, second);
else
- newRHS = BVF.EvaluateAPSInt(BinaryOperator::Sub,
- symIntExpr->getRHS(),
- rhsInt->getValue());
+ newRHS = BVF.EvaluateAPSInt(BinaryOperator::Sub, first, second);
return MakeSymIntVal(symIntExpr->getLHS(), lop, *newRHS, resultTy);
}
}