diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h --- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h @@ -544,15 +544,11 @@ /// 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 --- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp @@ -894,16 +894,10 @@ 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 --- a/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp +++ b/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp @@ -59,7 +59,7 @@ if (const auto *M = dyn_cast(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 --- 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 @@ 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(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 @@ auto *HasValueVal = cast_or_null(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 isNonEmptyOptional(const Value &OptionalVal, const Environment &Env) { auto *HasValueVal = cast_or_null(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 @@ /// `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 @@ 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 @@ 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 @@ 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 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 @@ // 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 @@ if (auto *OptionalVal = getValueBehindPossiblePointer(*ObjectExpr, Env)) { auto *Prop = OptionalVal->getProperty("has_value"); if (auto *HasValueVal = cast_or_null(Prop)) { - if (Env.flowConditionImplies(*HasValueVal)) + if (Env.flowConditionImplies(HasValueVal->formula())) return {}; } } @@ -1015,13 +1019,14 @@ 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 --- a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp +++ b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp @@ -145,7 +145,7 @@ 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 --- a/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp @@ -160,7 +160,7 @@ auto *FooVal = cast(Env.getValue(*FooDecl)); - EXPECT_TRUE(Env.flowConditionImplies(*FooVal)); + EXPECT_TRUE(Env.flowConditionImplies(FooVal->formula())); }; std::string Code = R"( @@ -191,7 +191,7 @@ auto *FooVal = cast(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 --- a/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp @@ -25,9 +25,7 @@ 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 @@ 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 --- a/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp @@ -131,10 +131,13 @@ void transferBinary(const BinaryOperator *BO, const MatchFinder::MatchResult &M, LatticeTransferState &State) { - BoolValue *Comp = cast_or_null(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(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 @@ 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 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 @@ // 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(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 @@ 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 @@ // 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 @@ if (!Prop) return Result; auto *BVProp = cast(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 --- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp @@ -66,6 +66,10 @@ Std, TargetFun); } +const Formula &getFormula(const ValueDecl &D, const Environment &Env) { + return cast(Env.getValue(D))->formula(); +} + TEST(TransferTest, IntVarDeclNotTrackedWhenTransferDisabled) { std::string Code = R"( void target() { @@ -3578,10 +3582,10 @@ const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); - auto &BarValThen = *cast(EnvThen.getValue(*BarDecl)); + auto &BarValThen = getFormula(*BarDecl, EnvThen); EXPECT_TRUE(EnvThen.flowConditionImplies(BarValThen)); - auto &BarValElse = *cast(EnvElse.getValue(*BarDecl)); + auto &BarValElse = getFormula(*BarDecl, EnvElse); EXPECT_FALSE(EnvElse.flowConditionImplies(BarValElse)); }); } @@ -3612,10 +3616,10 @@ const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); - auto &BarValThen = *cast(EnvThen.getValue(*BarDecl)); + auto &BarValThen = getFormula(*BarDecl, EnvThen); EXPECT_FALSE(EnvThen.flowConditionImplies(BarValThen)); - auto &BarValElse = *cast(EnvElse.getValue(*BarDecl)); + auto &BarValElse = getFormula(*BarDecl, EnvElse); EXPECT_TRUE(EnvElse.flowConditionImplies(BarValElse)); }); } @@ -3633,7 +3637,8 @@ ASTContext &ASTCtx) { const Environment &Env = getEnvironmentAtAnnotation(Results, "p"); - auto &Equal = getValueForDecl(ASTCtx, Env, "equal"); + auto &Equal = + getValueForDecl(ASTCtx, Env, "equal").formula(); EXPECT_TRUE(Env.flowConditionImplies(Equal)); }); } @@ -3669,20 +3674,20 @@ const Environment &Env = getEnvironmentAtAnnotation(Results, "p0"); const ValueDecl *BDecl = findValueDecl(ASTCtx, "B"); ASSERT_THAT(BDecl, NotNull()); - auto &BVal = *cast(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(Env.getValue(*CDecl)); + auto &CVal = getFormula(*CDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(CVal)); } { const Environment &Env = getEnvironmentAtAnnotation(Results, "p2"); - auto &CVal = *cast(Env.getValue(*CDecl)); + auto &CVal = getFormula(*CDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(CVal)); } }); @@ -3714,8 +3719,8 @@ const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); - auto &BarVal = *cast(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 @@ const ValueDecl *ErrDecl = findValueDecl(ASTCtx, "Err"); ASSERT_THAT(ErrDecl, NotNull()); - auto &BarVal = *cast(Env.getValue(*BarDecl)); - auto &ErrVal = *cast(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 @@ const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); - auto &BarVal = *cast(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 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - BoolValue &ThenFooVal = *cast(ThenEnv.getValue(*FooDecl)); + auto &ThenFooVal= getFormula(*FooDecl, ThenEnv); EXPECT_TRUE(ThenEnv.flowConditionImplies(ThenFooVal)); - BoolValue &ElseFooVal = *cast(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 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - BoolValue &LoopBodyFooVal = - *cast(LoopBodyEnv.getValue(*FooDecl)); + auto &LoopBodyFooVal = getFormula(*FooDecl, LoopBodyEnv); EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal)); - BoolValue &AfterLoopFooVal = - *cast(AfterLoopEnv.getValue(*FooDecl)); + auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv); EXPECT_TRUE(AfterLoopEnv.flowConditionImplies( - AfterLoopEnv.makeNot(AfterLoopFooVal))); + AfterLoopEnv.arena().makeNot(AfterLoopFooVal))); }); } @@ -4323,6 +4328,7 @@ 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 @@ const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); - BoolValue &LoopBodyFooVal = - *cast(LoopBodyEnv.getValue(*FooDecl)); - BoolValue &LoopBodyBarVal = - *cast(LoopBodyEnv.getValue(*BarDecl)); + auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv); + auto &LoopBodyBarVal = getFormula(*BarDecl, LoopBodyEnv); EXPECT_TRUE(LoopBodyEnv.flowConditionImplies( - LoopBodyEnv.makeOr(LoopBodyBarVal, LoopBodyFooVal))); - - BoolValue &AfterLoopFooVal = - *cast(AfterLoopEnv.getValue(*FooDecl)); - BoolValue &AfterLoopBarVal = - *cast(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 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - BoolValue &LoopBodyFooVal = - *cast(LoopBodyEnv.getValue(*FooDecl)); + auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv); EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal)); - BoolValue &AfterLoopFooVal = - *cast(AfterLoopEnv.getValue(*FooDecl)); + auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv); EXPECT_TRUE(AfterLoopEnv.flowConditionImplies( - AfterLoopEnv.makeNot(AfterLoopFooVal))); + AfterLoopEnv.arena().makeNot(AfterLoopFooVal))); }); } @@ -4404,8 +4404,7 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - BoolValue &LoopBodyFooVal = - *cast(LoopBodyEnv.getValue(*FooDecl)); + auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv); EXPECT_FALSE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal)); }); } @@ -4431,9 +4430,9 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(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 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(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 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); @@ -4625,8 +4624,8 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(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 @@ 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 @@ const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); - auto &FooVal = *cast(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(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 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(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 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/2}}}); @@ -4748,9 +4748,9 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(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 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/3}}}); @@ -4820,10 +4820,10 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(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 @@ const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); - auto &FooVal = *cast(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(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 @@ const ValueDecl *BazDecl = findValueDecl(ASTCtx, "Baz"); ASSERT_THAT(BazDecl, NotNull()); - auto &BarVal = *cast(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(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 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); @@ -4971,8 +4971,8 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(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 @@ const ValueDecl *BazDecl = findValueDecl(ASTCtx, "Baz"); ASSERT_THAT(BazDecl, NotNull()); - auto &BazVal = *cast(Env.getValue(*BazDecl)); + auto &BazVal = getFormula(*BazDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(BazVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); @@ -5047,7 +5047,7 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); @@ -5079,7 +5079,7 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); @@ -5111,7 +5111,7 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); @@ -5145,7 +5145,7 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); @@ -5180,7 +5180,7 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); @@ -5214,7 +5214,7 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); @@ -5245,7 +5245,7 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); @@ -5276,7 +5276,7 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); @@ -5307,7 +5307,7 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto &FooVal = *cast(Env.getValue(*FooDecl)); + auto &FooVal = getFormula(*FooDecl, Env); EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); @@ -5352,7 +5352,7 @@ [](const llvm::StringMap> &Results, ASTContext &ASTCtx) { const Environment &Env = getEnvironmentAtAnnotation(Results, "p"); - auto &B = getValueForDecl(ASTCtx, Env, "b"); + auto &B = getValueForDecl(ASTCtx, Env, "b").formula(); EXPECT_TRUE(Env.flowConditionImplies(B)); }); } @@ -5395,30 +5395,32 @@ 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(ASTCtx, Env, "b1"); - EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(B1))); + auto &B1 = getValueForDecl(ASTCtx, Env, "b1").formula(); + EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(B1))); auto &NoreturnOnRhsOfAnd = - getValueForDecl(ASTCtx, Env, "NoreturnOnRhsOfAnd"); - EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(NoreturnOnRhsOfAnd))); + getValueForDecl(ASTCtx, Env, "NoreturnOnRhsOfAnd").formula(); + EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(NoreturnOnRhsOfAnd))); - auto &B2 = getValueForDecl(ASTCtx, Env, "b2"); + auto &B2 = getValueForDecl(ASTCtx, Env, "b2").formula(); EXPECT_TRUE(Env.flowConditionImplies(B2)); auto &NoreturnOnRhsOfOr = - getValueForDecl(ASTCtx, Env, "NoreturnOnRhsOfOr"); + getValueForDecl(ASTCtx, Env, "NoreturnOnRhsOfOr") + .formula(); EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnRhsOfOr)); auto &NoreturnOnLhsMakesAndUnreachable = getValueForDecl( - ASTCtx, Env, "NoreturnOnLhsMakesAndUnreachable"); + ASTCtx, Env, "NoreturnOnLhsMakesAndUnreachable").formula(); EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnLhsMakesAndUnreachable)); auto &NoreturnOnLhsMakesOrUnreachable = getValueForDecl( - ASTCtx, Env, "NoreturnOnLhsMakesOrUnreachable"); + ASTCtx, Env, "NoreturnOnLhsMakesOrUnreachable").formula(); EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnLhsMakesOrUnreachable)); }); } @@ -5587,7 +5589,7 @@ S->getChild(*cast(IndirectField->chain().front()))); auto *B = cast(getFieldValue(&AnonStruct, *BDecl, Env)); - ASSERT_TRUE(Env.flowConditionImplies(*B)); + ASSERT_TRUE(Env.flowConditionImplies(B->formula())); }); } @@ -5618,7 +5620,7 @@ *cast(IndirectField->chain().front()))); auto *B = cast(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 --- a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp @@ -429,8 +429,8 @@ 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 @@ 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 @@ const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo"); ASSERT_THAT(FooDecl, NotNull()); - auto GetFooValue = [FooDecl](const Environment &Env) { - return cast(Env.getValue(*FooDecl)->getProperty("is_set")); + auto GetFoo = [FooDecl](const Environment &Env) -> const Formula & { + return cast(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 @@ ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2")); const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); - auto *FooVal1 = cast(Env1.getValue(*FooDecl)); - EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1)); + auto &FooVal1 = cast(Env1.getValue(*FooDecl))->formula(); + EXPECT_TRUE(Env1.flowConditionImplies(FooVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); - auto *FooVal2 = cast(Env2.getValue(*FooDecl)); - EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2)); + auto &FooVal2 = cast(Env2.getValue(*FooDecl))->formula(); + EXPECT_FALSE(Env2.flowConditionImplies(FooVal2)); }); } @@ -860,12 +861,12 @@ ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2")); const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); - auto *FooVal1 = cast(Env1.getValue(*FooDecl)); - EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1)); + auto &FooVal1 = cast(Env1.getValue(*FooDecl))->formula(); + EXPECT_FALSE(Env1.flowConditionImplies(FooVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); - auto *FooVal2 = cast(Env2.getValue(*FooDecl)); - EXPECT_TRUE(Env2.flowConditionImplies(*FooVal2)); + auto &FooVal2 = cast(Env2.getValue(*FooDecl))->formula(); + EXPECT_TRUE(Env2.flowConditionImplies(FooVal2)); }); } @@ -888,8 +889,8 @@ ASSERT_THAT(Results.keys(), UnorderedElementsAre("p")); const Environment &Env = getEnvironmentAtAnnotation(Results, "p"); - auto *FooVal = cast(Env.getValue(*FooDecl)); - EXPECT_TRUE(Env.flowConditionImplies(*FooVal)); + auto &FooVal = cast(Env.getValue(*FooDecl))->formula(); + EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }); } @@ -917,16 +918,16 @@ ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2")); const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); - auto *FooVal1 = cast(Env1.getValue(*FooDecl)); - auto *BarVal1 = cast(Env1.getValue(*BarDecl)); - EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1)); - EXPECT_TRUE(Env1.flowConditionImplies(*BarVal1)); + auto &FooVal1 = cast(Env1.getValue(*FooDecl))->formula(); + auto &BarVal1 = cast(Env1.getValue(*BarDecl))->formula(); + EXPECT_TRUE(Env1.flowConditionImplies(FooVal1)); + EXPECT_TRUE(Env1.flowConditionImplies(BarVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); - auto *FooVal2 = cast(Env2.getValue(*FooDecl)); - auto *BarVal2 = cast(Env2.getValue(*BarDecl)); - EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2)); - EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2)); + auto &FooVal2 = cast(Env2.getValue(*FooDecl))->formula(); + auto &BarVal2 = cast(Env2.getValue(*BarDecl))->formula(); + EXPECT_FALSE(Env2.flowConditionImplies(FooVal2)); + EXPECT_FALSE(Env2.flowConditionImplies(BarVal2)); }); } @@ -954,16 +955,16 @@ ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2")); const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); - auto *FooVal1 = cast(Env1.getValue(*FooDecl)); - auto *BarVal1 = cast(Env1.getValue(*BarDecl)); - EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1)); - EXPECT_FALSE(Env1.flowConditionImplies(*BarVal1)); + auto &FooVal1 = cast(Env1.getValue(*FooDecl))->formula(); + auto &BarVal1 = cast(Env1.getValue(*BarDecl))->formula(); + EXPECT_FALSE(Env1.flowConditionImplies(FooVal1)); + EXPECT_FALSE(Env1.flowConditionImplies(BarVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); - auto *FooVal2 = cast(Env2.getValue(*FooDecl)); - auto *BarVal2 = cast(Env2.getValue(*BarDecl)); - EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2)); - EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2)); + auto &FooVal2 = cast(Env2.getValue(*FooDecl))->formula(); + auto &BarVal2 = cast(Env2.getValue(*BarDecl))->formula(); + EXPECT_FALSE(Env2.flowConditionImplies(FooVal2)); + EXPECT_FALSE(Env2.flowConditionImplies(BarVal2)); }); } @@ -991,16 +992,16 @@ ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2")); const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); - auto *FooVal1 = cast(Env1.getValue(*FooDecl)); - auto *BarVal1 = cast(Env1.getValue(*BarDecl)); - EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1)); - EXPECT_FALSE(Env1.flowConditionImplies(*BarVal1)); + auto &FooVal1 = cast(Env1.getValue(*FooDecl))->formula(); + auto &BarVal1 = cast(Env1.getValue(*BarDecl))->formula(); + EXPECT_FALSE(Env1.flowConditionImplies(FooVal1)); + EXPECT_FALSE(Env1.flowConditionImplies(BarVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); - auto *FooVal2 = cast(Env2.getValue(*FooDecl)); - auto *BarVal2 = cast(Env2.getValue(*BarDecl)); - EXPECT_TRUE(Env2.flowConditionImplies(*FooVal2)); - EXPECT_TRUE(Env2.flowConditionImplies(*BarVal2)); + auto &FooVal2 = cast(Env2.getValue(*FooDecl))->formula(); + auto &BarVal2 = cast(Env2.getValue(*BarDecl))->formula(); + EXPECT_TRUE(Env2.flowConditionImplies(FooVal2)); + EXPECT_TRUE(Env2.flowConditionImplies(BarVal2)); }); } @@ -1028,16 +1029,16 @@ ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2")); const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); - auto *FooVal1 = cast(Env1.getValue(*FooDecl)); - auto *BarVal1 = cast(Env1.getValue(*BarDecl)); - EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1)); - EXPECT_TRUE(Env1.flowConditionImplies(*BarVal1)); + auto &FooVal1 = cast(Env1.getValue(*FooDecl))->formula(); + auto &BarVal1 = cast(Env1.getValue(*BarDecl))->formula(); + EXPECT_TRUE(Env1.flowConditionImplies(FooVal1)); + EXPECT_TRUE(Env1.flowConditionImplies(BarVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); - auto *FooVal2 = cast(Env2.getValue(*FooDecl)); - auto *BarVal2 = cast(Env2.getValue(*BarDecl)); - EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2)); - EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2)); + auto &FooVal2 = cast(Env2.getValue(*FooDecl))->formula(); + auto &BarVal2 = cast(Env2.getValue(*BarDecl))->formula(); + EXPECT_FALSE(Env2.flowConditionImplies(FooVal2)); + EXPECT_FALSE(Env2.flowConditionImplies(BarVal2)); }); } @@ -1065,8 +1066,8 @@ ASSERT_THAT(FooDecl, NotNull()); const Environment &Env = getEnvironmentAtAnnotation(Results, "p"); - auto *FooVal = cast(Env.getValue(*FooDecl)); - EXPECT_TRUE(Env.flowConditionImplies(*FooVal)); + auto &FooVal = cast(Env.getValue(*FooDecl))->formula(); + EXPECT_TRUE(Env.flowConditionImplies(FooVal)); }); } @@ -1098,7 +1099,7 @@ const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); - auto &BarVal = *cast(Env.getValue(*BarDecl)); + auto &BarVal = cast(Env.getValue(*BarDecl))->formula(); EXPECT_FALSE(Env.flowConditionImplies(BarVal)); }); @@ -1139,7 +1140,7 @@ const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); - auto &BarVal = *cast(Env.getValue(*BarDecl)); + auto &BarVal = cast(Env.getValue(*BarDecl))->formula(); EXPECT_FALSE(Env.flowConditionImplies(BarVal)); }); @@ -1173,7 +1174,7 @@ const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); - auto &BarVal = *cast(Env.getValue(*BarDecl)); + auto &BarVal = cast(Env.getValue(*BarDecl))->formula(); EXPECT_FALSE(Env.flowConditionImplies(BarVal)); }); @@ -1202,11 +1203,11 @@ ASSERT_THAT(FooDecl, NotNull()); const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); - auto &FooVal1 = *cast(Env1.getValue(*FooDecl)); + auto &FooVal1 = cast(Env1.getValue(*FooDecl))->formula(); EXPECT_TRUE(Env1.flowConditionImplies(FooVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); - auto &FooVal2 = *cast(Env2.getValue(*FooDecl)); + auto &FooVal2 = cast(Env2.getValue(*FooDecl))->formula(); EXPECT_FALSE(Env2.flowConditionImplies(FooVal2)); }); } @@ -1543,7 +1544,8 @@ auto *BarVal = dyn_cast_or_null(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()))); }); }