[clang] 6272226 - [dataflow] Remove deprecated BoolValue flow condition accessors
Sam McCall via cfe-commits
cfe-commits at lists.llvm.org
Thu Jul 13 00:39:29 PDT 2023
Author: Sam McCall
Date: 2023-07-13T09:39:23+02:00
New Revision: 6272226b9f94ba252eabfa7d32e44408b8a12883
URL: https://github.com/llvm/llvm-project/commit/6272226b9f94ba252eabfa7d32e44408b8a12883
DIFF: https://github.com/llvm/llvm-project/commit/6272226b9f94ba252eabfa7d32e44408b8a12883.diff
LOG: [dataflow] Remove deprecated BoolValue flow condition accessors
Use the Formula versions instead, now.
Differential Revision: https://reviews.llvm.org/D155152
Added:
Modified:
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp
clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp
clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp
clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
index 6fd4a085fa7a5f..07af485e786c81 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -544,15 +544,11 @@ class Environment {
/// 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.
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
index 3cf3c721763085..a49c529c37a46b 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -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
diff --git a/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp b/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp
index 969883874052b5..895f4ff04a172f 100644
--- a/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp
@@ -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;
}
}
diff --git a/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp b/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
index 91aa9d11e751cd..7f516984094648 100644
--- a/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
@@ -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;
}
diff --git a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
index 183cb32e5e7687..1146a21b05c68c 100644
--- a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
+++ b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
@@ -145,7 +145,7 @@ class TerminatorVisitor
ConditionValue = false;
}
- Env.addToFlowCondition(*Val);
+ Env.addToFlowCondition(Val->formula());
return {&Cond, ConditionValue};
}
diff --git a/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp b/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp
index f88a179f93a45a..0edf3ca6b359b2 100644
--- a/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp
@@ -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"(
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
index 17c0f7b16c1c71..e9531d1e7e8fd4 100644
--- a/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
@@ -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 @@ class EnvironmentTest : public ::testing::Test {
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));
}
diff --git a/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp b/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp
index fe4fdda888bf5e..481bcd15443f8d 100644
--- a/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp
@@ -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";
diff --git a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
index a89ff8e7bc5ab5..5a5540cbaee3dc 100644
--- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
@@ -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)));
-
- 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)));
+ A.makeOr(LoopBodyBarVal, LoopBodyFooVal)));
+
+ 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()));
});
}
diff --git a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
index d811aed8fddd99..11b346fbf64f3b 100644
--- a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -429,8 +429,8 @@ class SpecialBoolAnalysis final
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 @@ class SpecialBoolAnalysis final
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())));
});
}
More information about the cfe-commits
mailing list