mirror of
https://github.com/capstone-engine/llvm-capstone.git
synced 2024-11-30 17:21:10 +00:00
[dataflow] Remove deprecated BoolValue flow condition accessors
Use the Formula versions instead, now. Differential Revision: https://reviews.llvm.org/D155152
This commit is contained in:
Sam McCall
parent
474e37c113
commit
6272226b9f
@ -544,15 +544,11 @@ public:
|
||||
|
||||
/// Record a fact that must be true if this point in the program is reached.
|
||||
void addToFlowCondition(const Formula &);
|
||||
/// Deprecated: Use Formula version instead.
|
||||
void addToFlowCondition(BoolValue &Val);
|
||||
|
||||
/// Returns true if the formula is always true when this point is reached.
|
||||
/// Returns false if the formula may be false, or if the flow condition isn't
|
||||
/// sufficiently precise to prove that it is true.
|
||||
bool flowConditionImplies(const Formula &) const;
|
||||
/// Deprecated: Use Formula version instead.
|
||||
bool flowConditionImplies(BoolValue &Val) const;
|
||||
|
||||
/// Returns the `DeclContext` of the block being analysed, if any. Otherwise,
|
||||
/// returns null.
|
||||
|
||||
@ -894,16 +894,10 @@ const StorageLocation &Environment::skip(const StorageLocation &Loc,
|
||||
void Environment::addToFlowCondition(const Formula &Val) {
|
||||
DACtx->addFlowConditionConstraint(FlowConditionToken, Val);
|
||||
}
|
||||
void Environment::addToFlowCondition(BoolValue &Val) {
|
||||
addToFlowCondition(Val.formula());
|
||||
}
|
||||
|
||||
bool Environment::flowConditionImplies(const Formula &Val) const {
|
||||
return DACtx->flowConditionImplies(FlowConditionToken, Val);
|
||||
}
|
||||
bool Environment::flowConditionImplies(BoolValue &Val) const {
|
||||
return flowConditionImplies(Val.formula());
|
||||
}
|
||||
|
||||
void Environment::dump(raw_ostream &OS) const {
|
||||
// FIXME: add printing for remaining fields and allow caller to decide what
|
||||
|
||||
@ -59,7 +59,7 @@ bool ChromiumCheckModel::transfer(const CFGElement &Element, Environment &Env) {
|
||||
if (const auto *M = dyn_cast<CXXMethodDecl>(Call->getDirectCallee())) {
|
||||
if (isCheckLikeMethod(CheckDecls, *M)) {
|
||||
// Mark this branch as unreachable.
|
||||
Env.addToFlowCondition(Env.getBoolLiteralValue(false));
|
||||
Env.addToFlowCondition(Env.arena().makeLiteral(false));
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
@ -22,6 +22,7 @@
|
||||
#include "clang/Analysis/CFG.h"
|
||||
#include "clang/Analysis/FlowSensitive/CFGMatchSwitch.h"
|
||||
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
|
||||
#include "clang/Analysis/FlowSensitive/Formula.h"
|
||||
#include "clang/Analysis/FlowSensitive/NoopLattice.h"
|
||||
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
|
||||
#include "clang/Analysis/FlowSensitive/Value.h"
|
||||
@ -234,17 +235,17 @@ auto isComparisonOperatorCall(L lhs_arg_matcher, R rhs_arg_matcher) {
|
||||
hasArgument(1, rhs_arg_matcher));
|
||||
}
|
||||
|
||||
/// Ensures that `Expr` is mapped to a `BoolValue` and returns it.
|
||||
BoolValue &forceBoolValue(Environment &Env, const Expr &Expr) {
|
||||
/// Ensures that `Expr` is mapped to a `BoolValue` and returns its formula.
|
||||
const Formula &forceBoolValue(Environment &Env, const Expr &Expr) {
|
||||
auto *Value = cast_or_null<BoolValue>(Env.getValue(Expr, SkipPast::None));
|
||||
if (Value != nullptr)
|
||||
return *Value;
|
||||
return Value->formula();
|
||||
|
||||
auto &Loc = Env.createStorageLocation(Expr);
|
||||
Value = &Env.makeAtomicBoolValue();
|
||||
Env.setValue(Loc, *Value);
|
||||
Env.setStorageLocation(Expr, Loc);
|
||||
return *Value;
|
||||
return Value->formula();
|
||||
}
|
||||
|
||||
/// Sets `HasValueVal` as the symbolic value that represents the "has_value"
|
||||
@ -421,7 +422,7 @@ bool isEmptyOptional(const Value &OptionalVal, const Environment &Env) {
|
||||
auto *HasValueVal =
|
||||
cast_or_null<BoolValue>(OptionalVal.getProperty("has_value"));
|
||||
return HasValueVal != nullptr &&
|
||||
Env.flowConditionImplies(Env.makeNot(*HasValueVal));
|
||||
Env.flowConditionImplies(Env.arena().makeNot(HasValueVal->formula()));
|
||||
}
|
||||
|
||||
/// Returns true if and only if `OptionalVal` is initialized and known to be
|
||||
@ -429,7 +430,8 @@ bool isEmptyOptional(const Value &OptionalVal, const Environment &Env) {
|
||||
bool isNonEmptyOptional(const Value &OptionalVal, const Environment &Env) {
|
||||
auto *HasValueVal =
|
||||
cast_or_null<BoolValue>(OptionalVal.getProperty("has_value"));
|
||||
return HasValueVal != nullptr && Env.flowConditionImplies(*HasValueVal);
|
||||
return HasValueVal != nullptr &&
|
||||
Env.flowConditionImplies(HasValueVal->formula());
|
||||
}
|
||||
|
||||
Value *getValueBehindPossiblePointer(const Expr &E, const Environment &Env) {
|
||||
@ -485,12 +487,11 @@ void transferOptionalHasValueCall(const CXXMemberCallExpr *CallExpr,
|
||||
|
||||
/// `ModelPred` builds a logical formula relating the predicate in
|
||||
/// `ValueOrPredExpr` to the optional's `has_value` property.
|
||||
void transferValueOrImpl(const clang::Expr *ValueOrPredExpr,
|
||||
const MatchFinder::MatchResult &Result,
|
||||
LatticeTransferState &State,
|
||||
BoolValue &(*ModelPred)(Environment &Env,
|
||||
BoolValue &ExprVal,
|
||||
BoolValue &HasValueVal)) {
|
||||
void transferValueOrImpl(
|
||||
const clang::Expr *ValueOrPredExpr, const MatchFinder::MatchResult &Result,
|
||||
LatticeTransferState &State,
|
||||
const Formula &(*ModelPred)(Environment &Env, const Formula &ExprVal,
|
||||
const Formula &HasValueVal)) {
|
||||
auto &Env = State.Env;
|
||||
|
||||
const auto *ObjectArgumentExpr =
|
||||
@ -502,24 +503,25 @@ void transferValueOrImpl(const clang::Expr *ValueOrPredExpr,
|
||||
if (HasValueVal == nullptr)
|
||||
return;
|
||||
|
||||
Env.addToFlowCondition(
|
||||
ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr), *HasValueVal));
|
||||
Env.addToFlowCondition(ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr),
|
||||
HasValueVal->formula()));
|
||||
}
|
||||
|
||||
void transferValueOrStringEmptyCall(const clang::Expr *ComparisonExpr,
|
||||
const MatchFinder::MatchResult &Result,
|
||||
LatticeTransferState &State) {
|
||||
return transferValueOrImpl(ComparisonExpr, Result, State,
|
||||
[](Environment &Env, BoolValue &ExprVal,
|
||||
BoolValue &HasValueVal) -> BoolValue & {
|
||||
[](Environment &Env, const Formula &ExprVal,
|
||||
const Formula &HasValueVal) -> const Formula & {
|
||||
auto &A = Env.arena();
|
||||
// If the result is *not* empty, then we know the
|
||||
// optional must have been holding a value. If
|
||||
// `ExprVal` is true, though, we don't learn
|
||||
// anything definite about `has_value`, so we
|
||||
// don't add any corresponding implications to
|
||||
// the flow condition.
|
||||
return Env.makeImplication(Env.makeNot(ExprVal),
|
||||
HasValueVal);
|
||||
return A.makeImplies(A.makeNot(ExprVal),
|
||||
HasValueVal);
|
||||
});
|
||||
}
|
||||
|
||||
@ -527,12 +529,13 @@ void transferValueOrNotEqX(const Expr *ComparisonExpr,
|
||||
const MatchFinder::MatchResult &Result,
|
||||
LatticeTransferState &State) {
|
||||
transferValueOrImpl(ComparisonExpr, Result, State,
|
||||
[](Environment &Env, BoolValue &ExprVal,
|
||||
BoolValue &HasValueVal) -> BoolValue & {
|
||||
[](Environment &Env, const Formula &ExprVal,
|
||||
const Formula &HasValueVal) -> const Formula & {
|
||||
auto &A = Env.arena();
|
||||
// We know that if `(opt.value_or(X) != X)` then
|
||||
// `opt.hasValue()`, even without knowing further
|
||||
// details about the contents of `opt`.
|
||||
return Env.makeImplication(ExprVal, HasValueVal);
|
||||
return A.makeImplies(ExprVal, HasValueVal);
|
||||
});
|
||||
}
|
||||
|
||||
@ -701,8 +704,8 @@ void transferStdForwardCall(const CallExpr *E, const MatchFinder::MatchResult &,
|
||||
State.Env.setValue(*LocRet, *ValArg);
|
||||
}
|
||||
|
||||
BoolValue &evaluateEquality(Environment &Env, BoolValue &EqVal, BoolValue &LHS,
|
||||
BoolValue &RHS) {
|
||||
const Formula &evaluateEquality(Arena &A, const Formula &EqVal,
|
||||
const Formula &LHS, const Formula &RHS) {
|
||||
// Logically, an optional<T> object is composed of two values - a `has_value`
|
||||
// bit and a value of type T. Equality of optional objects compares both
|
||||
// values. Therefore, merely comparing the `has_value` bits isn't sufficient:
|
||||
@ -717,37 +720,38 @@ BoolValue &evaluateEquality(Environment &Env, BoolValue &EqVal, BoolValue &LHS,
|
||||
// b) (!LHS & !RHS) => EqVal
|
||||
// If neither is set, then they are equal.
|
||||
// We rewrite b) as !EqVal => (LHS v RHS), for a more compact formula.
|
||||
return Env.makeAnd(
|
||||
Env.makeImplication(
|
||||
EqVal, Env.makeOr(Env.makeAnd(LHS, RHS),
|
||||
Env.makeAnd(Env.makeNot(LHS), Env.makeNot(RHS)))),
|
||||
Env.makeImplication(Env.makeNot(EqVal), Env.makeOr(LHS, RHS)));
|
||||
return A.makeAnd(
|
||||
A.makeImplies(EqVal, A.makeOr(A.makeAnd(LHS, RHS),
|
||||
A.makeAnd(A.makeNot(LHS), A.makeNot(RHS)))),
|
||||
A.makeImplies(A.makeNot(EqVal), A.makeOr(LHS, RHS)));
|
||||
}
|
||||
|
||||
void transferOptionalAndOptionalCmp(const clang::CXXOperatorCallExpr *CmpExpr,
|
||||
const MatchFinder::MatchResult &,
|
||||
LatticeTransferState &State) {
|
||||
Environment &Env = State.Env;
|
||||
auto &A = Env.arena();
|
||||
auto *CmpValue = &forceBoolValue(Env, *CmpExpr);
|
||||
if (auto *LHasVal = getHasValue(
|
||||
Env, Env.getValue(*CmpExpr->getArg(0), SkipPast::Reference)))
|
||||
if (auto *RHasVal = getHasValue(
|
||||
Env, Env.getValue(*CmpExpr->getArg(1), SkipPast::Reference))) {
|
||||
if (CmpExpr->getOperator() == clang::OO_ExclaimEqual)
|
||||
CmpValue = &State.Env.makeNot(*CmpValue);
|
||||
Env.addToFlowCondition(
|
||||
evaluateEquality(Env, *CmpValue, *LHasVal, *RHasVal));
|
||||
CmpValue = &A.makeNot(*CmpValue);
|
||||
Env.addToFlowCondition(evaluateEquality(A, *CmpValue, LHasVal->formula(),
|
||||
RHasVal->formula()));
|
||||
}
|
||||
}
|
||||
|
||||
void transferOptionalAndValueCmp(const clang::CXXOperatorCallExpr *CmpExpr,
|
||||
const clang::Expr *E, Environment &Env) {
|
||||
auto &A = Env.arena();
|
||||
auto *CmpValue = &forceBoolValue(Env, *CmpExpr);
|
||||
if (auto *HasVal = getHasValue(Env, Env.getValue(*E, SkipPast::Reference))) {
|
||||
if (CmpExpr->getOperator() == clang::OO_ExclaimEqual)
|
||||
CmpValue = &Env.makeNot(*CmpValue);
|
||||
Env.addToFlowCondition(evaluateEquality(Env, *CmpValue, *HasVal,
|
||||
Env.getBoolLiteralValue(true)));
|
||||
CmpValue = &A.makeNot(*CmpValue);
|
||||
Env.addToFlowCondition(
|
||||
evaluateEquality(A, *CmpValue, HasVal->formula(), A.makeLiteral(true)));
|
||||
}
|
||||
}
|
||||
|
||||
@ -929,7 +933,7 @@ std::vector<SourceLocation> diagnoseUnwrapCall(const Expr *ObjectExpr,
|
||||
if (auto *OptionalVal = getValueBehindPossiblePointer(*ObjectExpr, Env)) {
|
||||
auto *Prop = OptionalVal->getProperty("has_value");
|
||||
if (auto *HasValueVal = cast_or_null<BoolValue>(Prop)) {
|
||||
if (Env.flowConditionImplies(*HasValueVal))
|
||||
if (Env.flowConditionImplies(HasValueVal->formula()))
|
||||
return {};
|
||||
}
|
||||
}
|
||||
@ -1015,13 +1019,14 @@ bool UncheckedOptionalAccessModel::merge(QualType Type, const Value &Val1,
|
||||
bool MustNonEmpty1 = isNonEmptyOptional(Val1, Env1);
|
||||
bool MustNonEmpty2 = isNonEmptyOptional(Val2, Env2);
|
||||
if (MustNonEmpty1 && MustNonEmpty2)
|
||||
MergedEnv.addToFlowCondition(HasValueVal);
|
||||
MergedEnv.addToFlowCondition(HasValueVal.formula());
|
||||
else if (
|
||||
// Only make the costly calls to `isEmptyOptional` if we got "unknown"
|
||||
// (false) for both calls to `isNonEmptyOptional`.
|
||||
!MustNonEmpty1 && !MustNonEmpty2 && isEmptyOptional(Val1, Env1) &&
|
||||
isEmptyOptional(Val2, Env2))
|
||||
MergedEnv.addToFlowCondition(MergedEnv.makeNot(HasValueVal));
|
||||
MergedEnv.addToFlowCondition(
|
||||
MergedEnv.arena().makeNot(HasValueVal.formula()));
|
||||
setHasValue(MergedVal, HasValueVal);
|
||||
return true;
|
||||
}
|
||||
|
||||
@ -145,7 +145,7 @@ private:
|
||||
ConditionValue = false;
|
||||
}
|
||||
|
||||
Env.addToFlowCondition(*Val);
|
||||
Env.addToFlowCondition(Val->formula());
|
||||
return {&Cond, ConditionValue};
|
||||
}
|
||||
|
||||
|
||||
@ -160,7 +160,7 @@ TEST(ChromiumCheckModelTest, CheckSuccessImpliesConditionHolds) {
|
||||
|
||||
auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
|
||||
EXPECT_TRUE(Env.flowConditionImplies(*FooVal));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal->formula()));
|
||||
};
|
||||
|
||||
std::string Code = R"(
|
||||
@ -191,7 +191,7 @@ TEST(ChromiumCheckModelTest, UnrelatedCheckIgnored) {
|
||||
|
||||
auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
|
||||
EXPECT_FALSE(Env.flowConditionImplies(*FooVal));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(FooVal->formula()));
|
||||
};
|
||||
|
||||
std::string Code = R"(
|
||||
|
||||
@ -25,9 +25,7 @@ namespace {
|
||||
using namespace clang;
|
||||
using namespace dataflow;
|
||||
using ::clang::dataflow::test::getFieldValue;
|
||||
using ::testing::ElementsAre;
|
||||
using ::testing::NotNull;
|
||||
using ::testing::Pair;
|
||||
|
||||
class EnvironmentTest : public ::testing::Test {
|
||||
protected:
|
||||
@ -38,17 +36,18 @@ protected:
|
||||
|
||||
TEST_F(EnvironmentTest, FlowCondition) {
|
||||
Environment Env(DAContext);
|
||||
auto &A = Env.arena();
|
||||
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.getBoolLiteralValue(true)));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.getBoolLiteralValue(false)));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(A.makeLiteral(true)));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(A.makeLiteral(false)));
|
||||
|
||||
auto &X = Env.makeAtomicBoolValue();
|
||||
auto &X = A.makeAtomRef(A.makeAtom());
|
||||
EXPECT_FALSE(Env.flowConditionImplies(X));
|
||||
|
||||
Env.addToFlowCondition(X);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(X));
|
||||
|
||||
auto &NotX = Env.makeNot(X);
|
||||
auto &NotX = A.makeNot(X);
|
||||
EXPECT_FALSE(Env.flowConditionImplies(NotX));
|
||||
}
|
||||
|
||||
|
||||
@ -131,10 +131,13 @@ getValueAndSignProperties(const UnaryOperator *UO,
|
||||
|
||||
void transferBinary(const BinaryOperator *BO, const MatchFinder::MatchResult &M,
|
||||
LatticeTransferState &State) {
|
||||
BoolValue *Comp = cast_or_null<BoolValue>(State.Env.getValueStrict(*BO));
|
||||
if (!Comp) {
|
||||
Comp = &State.Env.makeAtomicBoolValue();
|
||||
State.Env.setValueStrict(*BO, *Comp);
|
||||
auto &A = State.Env.arena();
|
||||
const Formula *Comp;
|
||||
if (BoolValue *V = cast_or_null<BoolValue>(State.Env.getValueStrict(*BO))) {
|
||||
Comp = &V->formula();
|
||||
} else {
|
||||
Comp = &A.makeAtomRef(A.makeAtom());
|
||||
State.Env.setValueStrict(*BO, A.makeBoolValue(*Comp));
|
||||
}
|
||||
|
||||
// FIXME Use this as well:
|
||||
@ -154,37 +157,46 @@ void transferBinary(const BinaryOperator *BO, const MatchFinder::MatchResult &M,
|
||||
switch (BO->getOpcode()) {
|
||||
case BO_GT:
|
||||
// pos > pos
|
||||
State.Env.addToFlowCondition(State.Env.makeImplication(
|
||||
*Comp, State.Env.makeImplication(*RHSProps.Pos, *LHSProps.Pos)));
|
||||
State.Env.addToFlowCondition(
|
||||
A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
|
||||
LHSProps.Pos->formula())));
|
||||
// pos > zero
|
||||
State.Env.addToFlowCondition(State.Env.makeImplication(
|
||||
*Comp, State.Env.makeImplication(*RHSProps.Zero, *LHSProps.Pos)));
|
||||
State.Env.addToFlowCondition(
|
||||
A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
|
||||
LHSProps.Pos->formula())));
|
||||
break;
|
||||
case BO_LT:
|
||||
// neg < neg
|
||||
State.Env.addToFlowCondition(State.Env.makeImplication(
|
||||
*Comp, State.Env.makeImplication(*RHSProps.Neg, *LHSProps.Neg)));
|
||||
State.Env.addToFlowCondition(
|
||||
A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
|
||||
LHSProps.Neg->formula())));
|
||||
// neg < zero
|
||||
State.Env.addToFlowCondition(State.Env.makeImplication(
|
||||
*Comp, State.Env.makeImplication(*RHSProps.Zero, *LHSProps.Neg)));
|
||||
State.Env.addToFlowCondition(
|
||||
A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
|
||||
LHSProps.Neg->formula())));
|
||||
break;
|
||||
case BO_GE:
|
||||
// pos >= pos
|
||||
State.Env.addToFlowCondition(State.Env.makeImplication(
|
||||
*Comp, State.Env.makeImplication(*RHSProps.Pos, *LHSProps.Pos)));
|
||||
State.Env.addToFlowCondition(
|
||||
A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
|
||||
LHSProps.Pos->formula())));
|
||||
break;
|
||||
case BO_LE:
|
||||
// neg <= neg
|
||||
State.Env.addToFlowCondition(State.Env.makeImplication(
|
||||
*Comp, State.Env.makeImplication(*RHSProps.Neg, *LHSProps.Neg)));
|
||||
State.Env.addToFlowCondition(
|
||||
A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
|
||||
LHSProps.Neg->formula())));
|
||||
break;
|
||||
case BO_EQ:
|
||||
State.Env.addToFlowCondition(State.Env.makeImplication(
|
||||
*Comp, State.Env.makeImplication(*RHSProps.Neg, *LHSProps.Neg)));
|
||||
State.Env.addToFlowCondition(State.Env.makeImplication(
|
||||
*Comp, State.Env.makeImplication(*RHSProps.Zero, *LHSProps.Zero)));
|
||||
State.Env.addToFlowCondition(State.Env.makeImplication(
|
||||
*Comp, State.Env.makeImplication(*RHSProps.Pos, *LHSProps.Pos)));
|
||||
State.Env.addToFlowCondition(
|
||||
A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
|
||||
LHSProps.Neg->formula())));
|
||||
State.Env.addToFlowCondition(
|
||||
A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
|
||||
LHSProps.Zero->formula())));
|
||||
State.Env.addToFlowCondition(
|
||||
A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
|
||||
LHSProps.Pos->formula())));
|
||||
break;
|
||||
case BO_NE: // Noop.
|
||||
break;
|
||||
@ -196,6 +208,7 @@ void transferBinary(const BinaryOperator *BO, const MatchFinder::MatchResult &M,
|
||||
void transferUnaryMinus(const UnaryOperator *UO,
|
||||
const MatchFinder::MatchResult &M,
|
||||
LatticeTransferState &State) {
|
||||
auto &A = State.Env.arena();
|
||||
auto [UnaryOpValue, UnaryOpProps, OperandProps] =
|
||||
getValueAndSignProperties(UO, M, State);
|
||||
if (!UnaryOpValue)
|
||||
@ -203,37 +216,38 @@ void transferUnaryMinus(const UnaryOperator *UO,
|
||||
|
||||
// a is pos ==> -a is neg
|
||||
State.Env.addToFlowCondition(
|
||||
State.Env.makeImplication(*OperandProps.Pos, *UnaryOpProps.Neg));
|
||||
A.makeImplies(OperandProps.Pos->formula(), UnaryOpProps.Neg->formula()));
|
||||
// a is neg ==> -a is pos
|
||||
State.Env.addToFlowCondition(
|
||||
State.Env.makeImplication(*OperandProps.Neg, *UnaryOpProps.Pos));
|
||||
A.makeImplies(OperandProps.Neg->formula(), UnaryOpProps.Pos->formula()));
|
||||
// a is zero ==> -a is zero
|
||||
State.Env.addToFlowCondition(
|
||||
State.Env.makeImplication(*OperandProps.Zero, *UnaryOpProps.Zero));
|
||||
State.Env.addToFlowCondition(A.makeImplies(OperandProps.Zero->formula(),
|
||||
UnaryOpProps.Zero->formula()));
|
||||
}
|
||||
|
||||
void transferUnaryNot(const UnaryOperator *UO,
|
||||
const MatchFinder::MatchResult &M,
|
||||
LatticeTransferState &State) {
|
||||
auto &A = State.Env.arena();
|
||||
auto [UnaryOpValue, UnaryOpProps, OperandProps] =
|
||||
getValueAndSignProperties(UO, M, State);
|
||||
if (!UnaryOpValue)
|
||||
return;
|
||||
|
||||
// a is neg or pos ==> !a is zero
|
||||
State.Env.addToFlowCondition(State.Env.makeImplication(
|
||||
State.Env.makeOr(*OperandProps.Pos, *OperandProps.Neg),
|
||||
*UnaryOpProps.Zero));
|
||||
State.Env.addToFlowCondition(A.makeImplies(
|
||||
A.makeOr(OperandProps.Pos->formula(), OperandProps.Neg->formula()),
|
||||
UnaryOpProps.Zero->formula()));
|
||||
|
||||
// FIXME Handle this logic universally, not just for unary not. But Where to
|
||||
// put the generic handler, transferExpr maybe?
|
||||
if (auto *UOBoolVal = dyn_cast<BoolValue>(UnaryOpValue)) {
|
||||
// !a <==> a is zero
|
||||
State.Env.addToFlowCondition(
|
||||
State.Env.makeIff(*UOBoolVal, *OperandProps.Zero));
|
||||
A.makeEquals(UOBoolVal->formula(), OperandProps.Zero->formula()));
|
||||
// !a <==> !a is not zero
|
||||
State.Env.addToFlowCondition(
|
||||
State.Env.makeIff(*UOBoolVal, State.Env.makeNot(*UnaryOpProps.Zero)));
|
||||
State.Env.addToFlowCondition(A.makeEquals(
|
||||
UOBoolVal->formula(), A.makeNot(UnaryOpProps.Zero->formula())));
|
||||
}
|
||||
}
|
||||
|
||||
@ -366,6 +380,10 @@ BoolValue &mergeBoolValues(BoolValue &Bool1, const Environment &Env1,
|
||||
return Bool1;
|
||||
}
|
||||
|
||||
auto &B1 = Bool1.formula();
|
||||
auto &B2 = Bool2.formula();
|
||||
|
||||
auto &A = MergedEnv.arena();
|
||||
auto &MergedBool = MergedEnv.makeAtomicBoolValue();
|
||||
|
||||
// If `Bool1` and `Bool2` is constrained to the same true / false value,
|
||||
@ -373,11 +391,11 @@ BoolValue &mergeBoolValues(BoolValue &Bool1, const Environment &Env1,
|
||||
// path taken - this simplifies the flow condition tracked in `MergedEnv`.
|
||||
// Otherwise, information about which path was taken is used to associate
|
||||
// `MergedBool` with `Bool1` and `Bool2`.
|
||||
if (Env1.flowConditionImplies(Bool1) && Env2.flowConditionImplies(Bool2)) {
|
||||
MergedEnv.addToFlowCondition(MergedBool);
|
||||
} else if (Env1.flowConditionImplies(Env1.makeNot(Bool1)) &&
|
||||
Env2.flowConditionImplies(Env2.makeNot(Bool2))) {
|
||||
MergedEnv.addToFlowCondition(MergedEnv.makeNot(MergedBool));
|
||||
if (Env1.flowConditionImplies(B1) && Env2.flowConditionImplies(B2)) {
|
||||
MergedEnv.addToFlowCondition(MergedBool.formula());
|
||||
} else if (Env1.flowConditionImplies(A.makeNot(B1)) &&
|
||||
Env2.flowConditionImplies(A.makeNot(B2))) {
|
||||
MergedEnv.addToFlowCondition(A.makeNot(MergedBool.formula()));
|
||||
}
|
||||
return MergedBool;
|
||||
}
|
||||
@ -466,7 +484,7 @@ testing::AssertionResult isPropertyImplied(const Environment &Env,
|
||||
if (!Prop)
|
||||
return Result;
|
||||
auto *BVProp = cast<BoolValue>(Prop);
|
||||
if (Env.flowConditionImplies(*BVProp) != Implies)
|
||||
if (Env.flowConditionImplies(BVProp->formula()) != Implies)
|
||||
return testing::AssertionFailure()
|
||||
<< Property << " is " << (Implies ? "not" : "") << " implied"
|
||||
<< ", but should " << (Implies ? "" : "not ") << "be";
|
||||
|
||||
@ -66,6 +66,10 @@ void runDataflow(
|
||||
Std, TargetFun);
|
||||
}
|
||||
|
||||
const Formula &getFormula(const ValueDecl &D, const Environment &Env) {
|
||||
return cast<BoolValue>(Env.getValue(D))->formula();
|
||||
}
|
||||
|
||||
TEST(TransferTest, IntVarDeclNotTrackedWhenTransferDisabled) {
|
||||
std::string Code = R"(
|
||||
void target() {
|
||||
@ -3578,10 +3582,10 @@ TEST(TransferTest, BooleanEquality) {
|
||||
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
|
||||
ASSERT_THAT(BarDecl, NotNull());
|
||||
|
||||
auto &BarValThen = *cast<BoolValue>(EnvThen.getValue(*BarDecl));
|
||||
auto &BarValThen = getFormula(*BarDecl, EnvThen);
|
||||
EXPECT_TRUE(EnvThen.flowConditionImplies(BarValThen));
|
||||
|
||||
auto &BarValElse = *cast<BoolValue>(EnvElse.getValue(*BarDecl));
|
||||
auto &BarValElse = getFormula(*BarDecl, EnvElse);
|
||||
EXPECT_FALSE(EnvElse.flowConditionImplies(BarValElse));
|
||||
});
|
||||
}
|
||||
@ -3612,10 +3616,10 @@ TEST(TransferTest, BooleanInequality) {
|
||||
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
|
||||
ASSERT_THAT(BarDecl, NotNull());
|
||||
|
||||
auto &BarValThen = *cast<BoolValue>(EnvThen.getValue(*BarDecl));
|
||||
auto &BarValThen = getFormula(*BarDecl, EnvThen);
|
||||
EXPECT_FALSE(EnvThen.flowConditionImplies(BarValThen));
|
||||
|
||||
auto &BarValElse = *cast<BoolValue>(EnvElse.getValue(*BarDecl));
|
||||
auto &BarValElse = getFormula(*BarDecl, EnvElse);
|
||||
EXPECT_TRUE(EnvElse.flowConditionImplies(BarValElse));
|
||||
});
|
||||
}
|
||||
@ -3633,7 +3637,8 @@ TEST(TransferTest, IntegerLiteralEquality) {
|
||||
ASTContext &ASTCtx) {
|
||||
const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
|
||||
|
||||
auto &Equal = getValueForDecl<BoolValue>(ASTCtx, Env, "equal");
|
||||
auto &Equal =
|
||||
getValueForDecl<BoolValue>(ASTCtx, Env, "equal").formula();
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Equal));
|
||||
});
|
||||
}
|
||||
@ -3669,20 +3674,20 @@ TEST(TransferTest, CorrelatedBranches) {
|
||||
const Environment &Env = getEnvironmentAtAnnotation(Results, "p0");
|
||||
const ValueDecl *BDecl = findValueDecl(ASTCtx, "B");
|
||||
ASSERT_THAT(BDecl, NotNull());
|
||||
auto &BVal = *cast<BoolValue>(Env.getValue(*BDecl));
|
||||
auto &BVal = getFormula(*BDecl, Env);
|
||||
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BVal)));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BVal)));
|
||||
}
|
||||
|
||||
{
|
||||
const Environment &Env = getEnvironmentAtAnnotation(Results, "p1");
|
||||
auto &CVal = *cast<BoolValue>(Env.getValue(*CDecl));
|
||||
auto &CVal = getFormula(*CDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(CVal));
|
||||
}
|
||||
|
||||
{
|
||||
const Environment &Env = getEnvironmentAtAnnotation(Results, "p2");
|
||||
auto &CVal = *cast<BoolValue>(Env.getValue(*CDecl));
|
||||
auto &CVal = getFormula(*CDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(CVal));
|
||||
}
|
||||
});
|
||||
@ -3714,8 +3719,8 @@ TEST(TransferTest, LoopWithAssignmentConverges) {
|
||||
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
|
||||
ASSERT_THAT(BarDecl, NotNull());
|
||||
|
||||
auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BarVal)));
|
||||
auto &BarVal = getFormula(*BarDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal)));
|
||||
});
|
||||
}
|
||||
|
||||
@ -3746,13 +3751,14 @@ TEST(TransferTest, LoopWithStagedAssignments) {
|
||||
const ValueDecl *ErrDecl = findValueDecl(ASTCtx, "Err");
|
||||
ASSERT_THAT(ErrDecl, NotNull());
|
||||
|
||||
auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
|
||||
auto &ErrVal = *cast<BoolValue>(Env.getValue(*ErrDecl));
|
||||
auto &BarVal = getFormula(*BarDecl, Env);
|
||||
auto &ErrVal = getFormula(*ErrDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(BarVal));
|
||||
// An unsound analysis, for example only evaluating the loop once, can
|
||||
// conclude that `Err` is false. So, we test that this conclusion is not
|
||||
// reached.
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(ErrVal)));
|
||||
EXPECT_FALSE(
|
||||
Env.flowConditionImplies(Env.arena().makeNot(ErrVal)));
|
||||
});
|
||||
}
|
||||
|
||||
@ -3781,8 +3787,8 @@ TEST(TransferTest, LoopWithReferenceAssignmentConverges) {
|
||||
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
|
||||
ASSERT_THAT(BarDecl, NotNull());
|
||||
|
||||
auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BarVal)));
|
||||
auto &BarVal = getFormula(*BarDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal)));
|
||||
});
|
||||
}
|
||||
|
||||
@ -4256,11 +4262,12 @@ TEST(TransferTest, IfStmtBranchExtendsFlowCondition) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
BoolValue &ThenFooVal = *cast<BoolValue>(ThenEnv.getValue(*FooDecl));
|
||||
auto &ThenFooVal= getFormula(*FooDecl, ThenEnv);
|
||||
EXPECT_TRUE(ThenEnv.flowConditionImplies(ThenFooVal));
|
||||
|
||||
BoolValue &ElseFooVal = *cast<BoolValue>(ElseEnv.getValue(*FooDecl));
|
||||
EXPECT_TRUE(ElseEnv.flowConditionImplies(ElseEnv.makeNot(ElseFooVal)));
|
||||
auto &ElseFooVal = getFormula(*FooDecl, ElseEnv);
|
||||
EXPECT_TRUE(
|
||||
ElseEnv.flowConditionImplies(ElseEnv.arena().makeNot(ElseFooVal)));
|
||||
});
|
||||
}
|
||||
|
||||
@ -4289,14 +4296,12 @@ TEST(TransferTest, WhileStmtBranchExtendsFlowCondition) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
BoolValue &LoopBodyFooVal =
|
||||
*cast<BoolValue>(LoopBodyEnv.getValue(*FooDecl));
|
||||
auto &LoopBodyFooVal = getFormula(*FooDecl, LoopBodyEnv);
|
||||
EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal));
|
||||
|
||||
BoolValue &AfterLoopFooVal =
|
||||
*cast<BoolValue>(AfterLoopEnv.getValue(*FooDecl));
|
||||
auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv);
|
||||
EXPECT_TRUE(AfterLoopEnv.flowConditionImplies(
|
||||
AfterLoopEnv.makeNot(AfterLoopFooVal)));
|
||||
AfterLoopEnv.arena().makeNot(AfterLoopFooVal)));
|
||||
});
|
||||
}
|
||||
|
||||
@ -4323,6 +4328,7 @@ TEST(TransferTest, DoWhileStmtBranchExtendsFlowCondition) {
|
||||
getEnvironmentAtAnnotation(Results, "loop_body");
|
||||
const Environment &AfterLoopEnv =
|
||||
getEnvironmentAtAnnotation(Results, "after_loop");
|
||||
auto &A = AfterLoopEnv.arena();
|
||||
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
@ -4330,21 +4336,17 @@ TEST(TransferTest, DoWhileStmtBranchExtendsFlowCondition) {
|
||||
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
|
||||
ASSERT_THAT(BarDecl, NotNull());
|
||||
|
||||
BoolValue &LoopBodyFooVal =
|
||||
*cast<BoolValue>(LoopBodyEnv.getValue(*FooDecl));
|
||||
BoolValue &LoopBodyBarVal =
|
||||
*cast<BoolValue>(LoopBodyEnv.getValue(*BarDecl));
|
||||
auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv);
|
||||
auto &LoopBodyBarVal = getFormula(*BarDecl, LoopBodyEnv);
|
||||
EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(
|
||||
LoopBodyEnv.makeOr(LoopBodyBarVal, LoopBodyFooVal)));
|
||||
A.makeOr(LoopBodyBarVal, LoopBodyFooVal)));
|
||||
|
||||
BoolValue &AfterLoopFooVal =
|
||||
*cast<BoolValue>(AfterLoopEnv.getValue(*FooDecl));
|
||||
BoolValue &AfterLoopBarVal =
|
||||
*cast<BoolValue>(AfterLoopEnv.getValue(*BarDecl));
|
||||
EXPECT_TRUE(AfterLoopEnv.flowConditionImplies(
|
||||
AfterLoopEnv.makeNot(AfterLoopFooVal)));
|
||||
EXPECT_TRUE(AfterLoopEnv.flowConditionImplies(
|
||||
AfterLoopEnv.makeNot(AfterLoopBarVal)));
|
||||
auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv);
|
||||
auto &AfterLoopBarVal = getFormula(*BarDecl, AfterLoopEnv);
|
||||
EXPECT_TRUE(
|
||||
AfterLoopEnv.flowConditionImplies(A.makeNot(AfterLoopFooVal)));
|
||||
EXPECT_TRUE(
|
||||
AfterLoopEnv.flowConditionImplies(A.makeNot(AfterLoopBarVal)));
|
||||
});
|
||||
}
|
||||
|
||||
@ -4373,14 +4375,12 @@ TEST(TransferTest, ForStmtBranchExtendsFlowCondition) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
BoolValue &LoopBodyFooVal =
|
||||
*cast<BoolValue>(LoopBodyEnv.getValue(*FooDecl));
|
||||
auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv);
|
||||
EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal));
|
||||
|
||||
BoolValue &AfterLoopFooVal =
|
||||
*cast<BoolValue>(AfterLoopEnv.getValue(*FooDecl));
|
||||
auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv);
|
||||
EXPECT_TRUE(AfterLoopEnv.flowConditionImplies(
|
||||
AfterLoopEnv.makeNot(AfterLoopFooVal)));
|
||||
AfterLoopEnv.arena().makeNot(AfterLoopFooVal)));
|
||||
});
|
||||
}
|
||||
|
||||
@ -4404,8 +4404,7 @@ TEST(TransferTest, ForStmtBranchWithoutConditionDoesNotExtendFlowCondition) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
BoolValue &LoopBodyFooVal =
|
||||
*cast<BoolValue>(LoopBodyEnv.getValue(*FooDecl));
|
||||
auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv);
|
||||
EXPECT_FALSE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal));
|
||||
});
|
||||
}
|
||||
@ -4431,9 +4430,9 @@ TEST(TransferTest, ContextSensitiveOptionDisabled) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_FALSE(Env.flowConditionImplies(FooVal));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
|
||||
},
|
||||
{BuiltinOptions{/*.ContextSensitiveOpts=*/std::nullopt}});
|
||||
}
|
||||
@ -4570,9 +4569,9 @@ TEST(TransferTest, ContextSensitiveDepthZero) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_FALSE(Env.flowConditionImplies(FooVal));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/0}}});
|
||||
}
|
||||
@ -4598,7 +4597,7 @@ TEST(TransferTest, ContextSensitiveSetTrue) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
@ -4625,8 +4624,8 @@ TEST(TransferTest, ContextSensitiveSetFalse) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(FooVal)));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
}
|
||||
@ -4650,6 +4649,7 @@ TEST(TransferTest, ContextSensitiveSetBothTrueAndFalse) {
|
||||
ASTContext &ASTCtx) {
|
||||
ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
|
||||
const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
|
||||
auto &A = Env.arena();
|
||||
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
@ -4657,13 +4657,13 @@ TEST(TransferTest, ContextSensitiveSetBothTrueAndFalse) {
|
||||
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
|
||||
ASSERT_THAT(BarDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(A.makeNot(FooVal)));
|
||||
|
||||
auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
|
||||
auto &BarVal = getFormula(*BarDecl, Env);
|
||||
EXPECT_FALSE(Env.flowConditionImplies(BarVal));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BarVal)));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(BarVal)));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
}
|
||||
@ -4690,9 +4690,9 @@ TEST(TransferTest, ContextSensitiveSetTwoLayersDepthOne) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_FALSE(Env.flowConditionImplies(FooVal));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/1}}});
|
||||
}
|
||||
@ -4719,7 +4719,7 @@ TEST(TransferTest, ContextSensitiveSetTwoLayersDepthTwo) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/2}}});
|
||||
@ -4748,9 +4748,9 @@ TEST(TransferTest, ContextSensitiveSetThreeLayersDepthTwo) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_FALSE(Env.flowConditionImplies(FooVal));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/2}}});
|
||||
}
|
||||
@ -4778,7 +4778,7 @@ TEST(TransferTest, ContextSensitiveSetThreeLayersDepthThree) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/3}}});
|
||||
@ -4820,10 +4820,10 @@ TEST(TransferTest, ContextSensitiveMutualRecursion) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
// ... but it also can't prove anything here.
|
||||
EXPECT_FALSE(Env.flowConditionImplies(FooVal));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/4}}});
|
||||
}
|
||||
@ -4855,13 +4855,13 @@ TEST(TransferTest, ContextSensitiveSetMultipleLines) {
|
||||
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
|
||||
ASSERT_THAT(BarDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(FooVal)));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
|
||||
|
||||
auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
|
||||
auto &BarVal = getFormula(*BarDecl, Env);
|
||||
EXPECT_FALSE(Env.flowConditionImplies(BarVal));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BarVal)));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal)));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
}
|
||||
@ -4897,13 +4897,13 @@ TEST(TransferTest, ContextSensitiveSetMultipleBlocks) {
|
||||
const ValueDecl *BazDecl = findValueDecl(ASTCtx, "Baz");
|
||||
ASSERT_THAT(BazDecl, NotNull());
|
||||
|
||||
auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
|
||||
auto &BarVal = getFormula(*BarDecl, Env);
|
||||
EXPECT_FALSE(Env.flowConditionImplies(BarVal));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BarVal)));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal)));
|
||||
|
||||
auto &BazVal = *cast<BoolValue>(Env.getValue(*BazDecl));
|
||||
auto &BazVal = getFormula(*BazDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(BazVal));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.makeNot(BazVal)));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(BazVal)));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
}
|
||||
@ -4946,7 +4946,7 @@ TEST(TransferTest, ContextSensitiveReturnTrue) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
@ -4971,8 +4971,8 @@ TEST(TransferTest, ContextSensitiveReturnFalse) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(FooVal)));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
}
|
||||
@ -4999,7 +4999,7 @@ TEST(TransferTest, ContextSensitiveReturnArg) {
|
||||
const ValueDecl *BazDecl = findValueDecl(ASTCtx, "Baz");
|
||||
ASSERT_THAT(BazDecl, NotNull());
|
||||
|
||||
auto &BazVal = *cast<BoolValue>(Env.getValue(*BazDecl));
|
||||
auto &BazVal = getFormula(*BazDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(BazVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
@ -5047,7 +5047,7 @@ TEST(TransferTest, ContextSensitiveMethodLiteral) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
@ -5079,7 +5079,7 @@ TEST(TransferTest, ContextSensitiveMethodGetter) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
@ -5111,7 +5111,7 @@ TEST(TransferTest, ContextSensitiveMethodSetter) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
@ -5145,7 +5145,7 @@ TEST(TransferTest, ContextSensitiveMethodGetterAndSetter) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
@ -5180,7 +5180,7 @@ TEST(TransferTest, ContextSensitiveMethodTwoLayersVoid) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
@ -5214,7 +5214,7 @@ TEST(TransferTest, ContextSensitiveMethodTwoLayersReturn) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
@ -5245,7 +5245,7 @@ TEST(TransferTest, ContextSensitiveConstructorBody) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
@ -5276,7 +5276,7 @@ TEST(TransferTest, ContextSensitiveConstructorInitializer) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
@ -5307,7 +5307,7 @@ TEST(TransferTest, ContextSensitiveConstructorDefault) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto &FooVal = *cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
auto &FooVal = getFormula(*FooDecl, Env);
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
},
|
||||
{BuiltinOptions{ContextSensitiveOptions{}}});
|
||||
@ -5352,7 +5352,7 @@ TEST(TransferTest, ChainedLogicalOps) {
|
||||
[](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
|
||||
ASTContext &ASTCtx) {
|
||||
const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
|
||||
auto &B = getValueForDecl<BoolValue>(ASTCtx, Env, "b");
|
||||
auto &B = getValueForDecl<BoolValue>(ASTCtx, Env, "b").formula();
|
||||
EXPECT_TRUE(Env.flowConditionImplies(B));
|
||||
});
|
||||
}
|
||||
@ -5395,30 +5395,32 @@ TEST(TransferTest, NoReturnFunctionInsideShortCircuitedBooleanOp) {
|
||||
ASTContext &ASTCtx) {
|
||||
ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
|
||||
const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
|
||||
auto &A = Env.arena();
|
||||
|
||||
// Check that [[p]] is reachable with a non-false flow condition.
|
||||
EXPECT_FALSE(Env.flowConditionImplies(Env.getBoolLiteralValue(false)));
|
||||
EXPECT_FALSE(Env.flowConditionImplies(A.makeLiteral(false)));
|
||||
|
||||
auto &B1 = getValueForDecl<BoolValue>(ASTCtx, Env, "b1");
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(B1)));
|
||||
auto &B1 = getValueForDecl<BoolValue>(ASTCtx, Env, "b1").formula();
|
||||
EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(B1)));
|
||||
|
||||
auto &NoreturnOnRhsOfAnd =
|
||||
getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfAnd");
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(NoreturnOnRhsOfAnd)));
|
||||
getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfAnd").formula();
|
||||
EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(NoreturnOnRhsOfAnd)));
|
||||
|
||||
auto &B2 = getValueForDecl<BoolValue>(ASTCtx, Env, "b2");
|
||||
auto &B2 = getValueForDecl<BoolValue>(ASTCtx, Env, "b2").formula();
|
||||
EXPECT_TRUE(Env.flowConditionImplies(B2));
|
||||
|
||||
auto &NoreturnOnRhsOfOr =
|
||||
getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfOr");
|
||||
getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfOr")
|
||||
.formula();
|
||||
EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnRhsOfOr));
|
||||
|
||||
auto &NoreturnOnLhsMakesAndUnreachable = getValueForDecl<BoolValue>(
|
||||
ASTCtx, Env, "NoreturnOnLhsMakesAndUnreachable");
|
||||
ASTCtx, Env, "NoreturnOnLhsMakesAndUnreachable").formula();
|
||||
EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnLhsMakesAndUnreachable));
|
||||
|
||||
auto &NoreturnOnLhsMakesOrUnreachable = getValueForDecl<BoolValue>(
|
||||
ASTCtx, Env, "NoreturnOnLhsMakesOrUnreachable");
|
||||
ASTCtx, Env, "NoreturnOnLhsMakesOrUnreachable").formula();
|
||||
EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnLhsMakesOrUnreachable));
|
||||
});
|
||||
}
|
||||
@ -5587,7 +5589,7 @@ TEST(TransferTest, AnonymousStruct) {
|
||||
S->getChild(*cast<ValueDecl>(IndirectField->chain().front())));
|
||||
|
||||
auto *B = cast<BoolValue>(getFieldValue(&AnonStruct, *BDecl, Env));
|
||||
ASSERT_TRUE(Env.flowConditionImplies(*B));
|
||||
ASSERT_TRUE(Env.flowConditionImplies(B->formula()));
|
||||
});
|
||||
}
|
||||
|
||||
@ -5618,7 +5620,7 @@ TEST(TransferTest, AnonymousStructWithInitializer) {
|
||||
*cast<ValueDecl>(IndirectField->chain().front())));
|
||||
|
||||
auto *B = cast<BoolValue>(getFieldValue(&AnonStruct, *BDecl, Env));
|
||||
ASSERT_TRUE(Env.flowConditionImplies(*B));
|
||||
ASSERT_TRUE(Env.flowConditionImplies(B->formula()));
|
||||
});
|
||||
}
|
||||
|
||||
|
||||
@ -429,8 +429,8 @@ public:
|
||||
if (IsSet2 == nullptr)
|
||||
return ComparisonResult::Different;
|
||||
|
||||
return Env1.flowConditionImplies(*IsSet1) ==
|
||||
Env2.flowConditionImplies(*IsSet2)
|
||||
return Env1.flowConditionImplies(IsSet1->formula()) ==
|
||||
Env2.flowConditionImplies(IsSet2->formula())
|
||||
? ComparisonResult::Same
|
||||
: ComparisonResult::Different;
|
||||
}
|
||||
@ -454,9 +454,9 @@ public:
|
||||
|
||||
auto &IsSet = MergedEnv.makeAtomicBoolValue();
|
||||
MergedVal.setProperty("is_set", IsSet);
|
||||
if (Env1.flowConditionImplies(*IsSet1) &&
|
||||
Env2.flowConditionImplies(*IsSet2))
|
||||
MergedEnv.addToFlowCondition(IsSet);
|
||||
if (Env1.flowConditionImplies(IsSet1->formula()) &&
|
||||
Env2.flowConditionImplies(IsSet2->formula()))
|
||||
MergedEnv.addToFlowCondition(IsSet.formula());
|
||||
|
||||
return true;
|
||||
}
|
||||
@ -518,14 +518,15 @@ TEST_F(JoinFlowConditionsTest, JoinDistinctButProvablyEquivalentValues) {
|
||||
const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
auto GetFooValue = [FooDecl](const Environment &Env) {
|
||||
return cast<BoolValue>(Env.getValue(*FooDecl)->getProperty("is_set"));
|
||||
auto GetFoo = [FooDecl](const Environment &Env) -> const Formula & {
|
||||
return cast<BoolValue>(Env.getValue(*FooDecl)->getProperty("is_set"))
|
||||
->formula();
|
||||
};
|
||||
|
||||
EXPECT_FALSE(Env1.flowConditionImplies(*GetFooValue(Env1)));
|
||||
EXPECT_TRUE(Env2.flowConditionImplies(*GetFooValue(Env2)));
|
||||
EXPECT_TRUE(Env3.flowConditionImplies(*GetFooValue(Env3)));
|
||||
EXPECT_TRUE(Env4.flowConditionImplies(*GetFooValue(Env4)));
|
||||
EXPECT_FALSE(Env1.flowConditionImplies(GetFoo(Env1)));
|
||||
EXPECT_TRUE(Env2.flowConditionImplies(GetFoo(Env2)));
|
||||
EXPECT_TRUE(Env3.flowConditionImplies(GetFoo(Env3)));
|
||||
EXPECT_TRUE(Env4.flowConditionImplies(GetFoo(Env4)));
|
||||
});
|
||||
}
|
||||
|
||||
@ -829,12 +830,12 @@ TEST_F(FlowConditionTest, IfStmtSingleVar) {
|
||||
ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
|
||||
|
||||
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
|
||||
auto *FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl));
|
||||
EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1));
|
||||
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
|
||||
EXPECT_TRUE(Env1.flowConditionImplies(FooVal1));
|
||||
|
||||
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
|
||||
auto *FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl));
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
|
||||
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
|
||||
});
|
||||
}
|
||||
|
||||
@ -860,12 +861,12 @@ TEST_F(FlowConditionTest, IfStmtSingleNegatedVar) {
|
||||
ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
|
||||
|
||||
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
|
||||
auto *FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl));
|
||||
EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1));
|
||||
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
|
||||
EXPECT_FALSE(Env1.flowConditionImplies(FooVal1));
|
||||
|
||||
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
|
||||
auto *FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl));
|
||||
EXPECT_TRUE(Env2.flowConditionImplies(*FooVal2));
|
||||
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
|
||||
EXPECT_TRUE(Env2.flowConditionImplies(FooVal2));
|
||||
});
|
||||
}
|
||||
|
||||
@ -888,8 +889,8 @@ TEST_F(FlowConditionTest, WhileStmt) {
|
||||
ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
|
||||
const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
|
||||
|
||||
auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(*FooVal));
|
||||
auto &FooVal = cast<BoolValue>(Env.getValue(*FooDecl))->formula();
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
});
|
||||
}
|
||||
|
||||
@ -917,16 +918,16 @@ TEST_F(FlowConditionTest, Conjunction) {
|
||||
ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
|
||||
|
||||
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
|
||||
auto *FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl));
|
||||
auto *BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl));
|
||||
EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1));
|
||||
EXPECT_TRUE(Env1.flowConditionImplies(*BarVal1));
|
||||
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
|
||||
auto &BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl))->formula();
|
||||
EXPECT_TRUE(Env1.flowConditionImplies(FooVal1));
|
||||
EXPECT_TRUE(Env1.flowConditionImplies(BarVal1));
|
||||
|
||||
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
|
||||
auto *FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl));
|
||||
auto *BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl));
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2));
|
||||
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
|
||||
auto &BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl))->formula();
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(BarVal2));
|
||||
});
|
||||
}
|
||||
|
||||
@ -954,16 +955,16 @@ TEST_F(FlowConditionTest, Disjunction) {
|
||||
ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
|
||||
|
||||
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
|
||||
auto *FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl));
|
||||
auto *BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl));
|
||||
EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1));
|
||||
EXPECT_FALSE(Env1.flowConditionImplies(*BarVal1));
|
||||
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
|
||||
auto &BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl))->formula();
|
||||
EXPECT_FALSE(Env1.flowConditionImplies(FooVal1));
|
||||
EXPECT_FALSE(Env1.flowConditionImplies(BarVal1));
|
||||
|
||||
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
|
||||
auto *FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl));
|
||||
auto *BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl));
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2));
|
||||
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
|
||||
auto &BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl))->formula();
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(BarVal2));
|
||||
});
|
||||
}
|
||||
|
||||
@ -991,16 +992,16 @@ TEST_F(FlowConditionTest, NegatedConjunction) {
|
||||
ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
|
||||
|
||||
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
|
||||
auto *FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl));
|
||||
auto *BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl));
|
||||
EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1));
|
||||
EXPECT_FALSE(Env1.flowConditionImplies(*BarVal1));
|
||||
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
|
||||
auto &BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl))->formula();
|
||||
EXPECT_FALSE(Env1.flowConditionImplies(FooVal1));
|
||||
EXPECT_FALSE(Env1.flowConditionImplies(BarVal1));
|
||||
|
||||
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
|
||||
auto *FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl));
|
||||
auto *BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl));
|
||||
EXPECT_TRUE(Env2.flowConditionImplies(*FooVal2));
|
||||
EXPECT_TRUE(Env2.flowConditionImplies(*BarVal2));
|
||||
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
|
||||
auto &BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl))->formula();
|
||||
EXPECT_TRUE(Env2.flowConditionImplies(FooVal2));
|
||||
EXPECT_TRUE(Env2.flowConditionImplies(BarVal2));
|
||||
});
|
||||
}
|
||||
|
||||
@ -1028,16 +1029,16 @@ TEST_F(FlowConditionTest, DeMorgan) {
|
||||
ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
|
||||
|
||||
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
|
||||
auto *FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl));
|
||||
auto *BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl));
|
||||
EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1));
|
||||
EXPECT_TRUE(Env1.flowConditionImplies(*BarVal1));
|
||||
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
|
||||
auto &BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl))->formula();
|
||||
EXPECT_TRUE(Env1.flowConditionImplies(FooVal1));
|
||||
EXPECT_TRUE(Env1.flowConditionImplies(BarVal1));
|
||||
|
||||
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
|
||||
auto *FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl));
|
||||
auto *BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl));
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2));
|
||||
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
|
||||
auto &BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl))->formula();
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(BarVal2));
|
||||
});
|
||||
}
|
||||
|
||||
@ -1065,8 +1066,8 @@ TEST_F(FlowConditionTest, Join) {
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
|
||||
auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(*FooVal));
|
||||
auto &FooVal = cast<BoolValue>(Env.getValue(*FooDecl))->formula();
|
||||
EXPECT_TRUE(Env.flowConditionImplies(FooVal));
|
||||
});
|
||||
}
|
||||
|
||||
@ -1098,7 +1099,7 @@ TEST_F(FlowConditionTest, OpaqueFlowConditionMergesToOpaqueBool) {
|
||||
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
|
||||
ASSERT_THAT(BarDecl, NotNull());
|
||||
|
||||
auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
|
||||
auto &BarVal = cast<BoolValue>(Env.getValue(*BarDecl))->formula();
|
||||
|
||||
EXPECT_FALSE(Env.flowConditionImplies(BarVal));
|
||||
});
|
||||
@ -1139,7 +1140,7 @@ TEST_F(FlowConditionTest, OpaqueFieldFlowConditionMergesToOpaqueBool) {
|
||||
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
|
||||
ASSERT_THAT(BarDecl, NotNull());
|
||||
|
||||
auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
|
||||
auto &BarVal = cast<BoolValue>(Env.getValue(*BarDecl))->formula();
|
||||
|
||||
EXPECT_FALSE(Env.flowConditionImplies(BarVal));
|
||||
});
|
||||
@ -1173,7 +1174,7 @@ TEST_F(FlowConditionTest, OpaqueFlowConditionInsideBranchMergesToOpaqueBool) {
|
||||
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
|
||||
ASSERT_THAT(BarDecl, NotNull());
|
||||
|
||||
auto &BarVal = *cast<BoolValue>(Env.getValue(*BarDecl));
|
||||
auto &BarVal = cast<BoolValue>(Env.getValue(*BarDecl))->formula();
|
||||
|
||||
EXPECT_FALSE(Env.flowConditionImplies(BarVal));
|
||||
});
|
||||
@ -1202,11 +1203,11 @@ TEST_F(FlowConditionTest, PointerToBoolImplicitCast) {
|
||||
ASSERT_THAT(FooDecl, NotNull());
|
||||
|
||||
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
|
||||
auto &FooVal1 = *cast<BoolValue>(Env1.getValue(*FooDecl));
|
||||
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
|
||||
EXPECT_TRUE(Env1.flowConditionImplies(FooVal1));
|
||||
|
||||
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
|
||||
auto &FooVal2 = *cast<BoolValue>(Env2.getValue(*FooDecl));
|
||||
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
|
||||
EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
|
||||
});
|
||||
}
|
||||
@ -1543,7 +1544,8 @@ TEST_F(TopTest, TopUsedInBothBranchesWithoutPrecisionLoss) {
|
||||
auto *BarVal = dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
|
||||
ASSERT_THAT(BarVal, NotNull());
|
||||
|
||||
EXPECT_TRUE(Env.flowConditionImplies(Env.makeIff(*FooVal, *BarVal)));
|
||||
EXPECT_TRUE(Env.flowConditionImplies(
|
||||
Env.arena().makeEquals(FooVal->formula(), BarVal->formula())));
|
||||
});
|
||||
}
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user