[analyzer] a few helper methods for getting and comparing symbolic values

API calls should express intent, and that's a motivation behind this patch.

Differential Revision: https://reviews.llvm.org/D42218

llvm-svn: 322809
This commit is contained in:
George Karpenkov 2018-01-18 03:18:36 +00:00
parent e0345b6e1f
commit d5680e5979
5 changed files with 42 additions and 2 deletions

View File

@ -37,6 +37,12 @@ public:
/// Construct a ConstraintVal indicating the constraint is underconstrained.
ConditionTruthVal() {}
/// \return Stored value, assuming that the value is known.
/// Crashes otherwise.
bool getValue() const {
return *Val;
}
/// Return true if the constraint is perfectly constrained to 'true'.
bool isConstrainedTrue() const {
return Val.hasValue() && Val.getValue();

View File

@ -212,10 +212,17 @@ public:
assumeInclusiveRange(DefinedOrUnknownSVal Val, const llvm::APSInt &From,
const llvm::APSInt &To) const;
/// \brief Check if the given SVal is not constrained to zero and is not
/// a zero constant.
ConditionTruthVal isNonNull(SVal V) const;
/// \brief Check if the given SVal is constrained to zero or is a zero
/// constant.
ConditionTruthVal isNull(SVal V) const;
/// \return Whether values \p Lhs and \p Rhs are equal.
ConditionTruthVal areEqual(SVal Lhs, SVal Rhs) const;
/// Utility method for getting regions.
const VarRegion* getRegion(const VarDecl *D, const LocationContext *LC) const;

View File

@ -29,6 +29,8 @@ class CXXBoolLiteralExpr;
namespace ento {
class ConditionTruthVal;
class SValBuilder {
virtual void anchor();
protected:
@ -124,7 +126,12 @@ public:
SVal evalBinOp(ProgramStateRef state, BinaryOperator::Opcode op,
SVal lhs, SVal rhs, QualType type);
/// \return Whether values in \p lhs and \p rhs are equal at \p state.
ConditionTruthVal areEqual(ProgramStateRef state, SVal lhs, SVal rhs);
SVal evalEQ(ProgramStateRef state, SVal lhs, SVal rhs);
DefinedOrUnknownSVal evalEQ(ProgramStateRef state, DefinedOrUnknownSVal lhs,
DefinedOrUnknownSVal rhs);

View File

@ -354,6 +354,17 @@ ProgramStateRef ProgramState::assumeInBound(DefinedOrUnknownSVal Idx,
return CM.assume(this, inBound.castAs<DefinedSVal>(), Assumption);
}
ConditionTruthVal ProgramState::isNonNull(SVal V) const {
ConditionTruthVal IsNull = isNull(V);
if (IsNull.isUnderconstrained())
return IsNull;
return ConditionTruthVal(!IsNull.getValue());
}
ConditionTruthVal ProgramState::areEqual(SVal Lhs, SVal Rhs) const {
return stateMgr->getSValBuilder().areEqual(this, Lhs, Rhs);
}
ConditionTruthVal ProgramState::isNull(SVal V) const {
if (V.isZeroConstant())
return true;

View File

@ -413,10 +413,19 @@ SVal SValBuilder::evalBinOp(ProgramStateRef state, BinaryOperator::Opcode op,
type);
}
ConditionTruthVal SValBuilder::areEqual(ProgramStateRef state, SVal lhs,
SVal rhs) {
return state->isNonNull(evalEQ(state, lhs, rhs));
}
SVal SValBuilder::evalEQ(ProgramStateRef state, SVal lhs, SVal rhs) {
return evalBinOp(state, BO_EQ, lhs, rhs, getConditionType());
}
DefinedOrUnknownSVal SValBuilder::evalEQ(ProgramStateRef state,
DefinedOrUnknownSVal lhs,
DefinedOrUnknownSVal rhs) {
return evalBinOp(state, BO_EQ, lhs, rhs, getConditionType())
return evalEQ(state, static_cast<SVal>(lhs), static_cast<SVal>(rhs))
.castAs<DefinedOrUnknownSVal>();
}