Author: martinboehme Date: 2023-10-30T13:18:57+01:00 New Revision: 526c9b7e37fa12abc17eebc68f21c1d213477ba8
URL: https://github.com/llvm/llvm-project/commit/526c9b7e37fa12abc17eebc68f21c1d213477ba8 DIFF: https://github.com/llvm/llvm-project/commit/526c9b7e37fa12abc17eebc68f21c1d213477ba8.diff LOG: [clang][nullability] Use `proves()` and `assume()` instead of deprecated synonyms. (#70297) Added: Modified: clang/lib/Analysis/FlowSensitive/HTMLLogger.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/SignAnalysisTest.cpp clang/unittests/Analysis/FlowSensitive/TransferTest.cpp clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp Removed: ################################################################################ diff --git a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp index 8aef1d6f46089d2..8329367098b1dbb 100644 --- a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp +++ b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp @@ -114,11 +114,10 @@ class ModelDumper { // guaranteed true/false here is valuable and hard to determine by hand. if (auto *B = llvm::dyn_cast<BoolValue>(&V)) { JOS.attribute("formula", llvm::to_string(B->formula())); - JOS.attribute( - "truth", Env.flowConditionImplies(B->formula()) ? "true" - : Env.flowConditionImplies(Env.arena().makeNot(B->formula())) - ? "false" - : "unknown"); + JOS.attribute("truth", Env.proves(B->formula()) ? "true" + : Env.proves(Env.arena().makeNot(B->formula())) + ? "false" + : "unknown"); } } void dump(const StorageLocation &L) { diff --git a/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp b/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp index 895f4ff04a172f9..f49087ababc44ce 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.arena().makeLiteral(false)); + Env.assume(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 8bd9a030f50cda0..55d0713639d90da 100644 --- a/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp +++ b/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp @@ -413,7 +413,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.arena().makeNot(HasValueVal->formula())); + Env.proves(Env.arena().makeNot(HasValueVal->formula())); } /// Returns true if and only if `OptionalVal` is initialized and known to be @@ -421,8 +421,7 @@ 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->formula()); + return HasValueVal != nullptr && Env.proves(HasValueVal->formula()); } Value *getValueBehindPossiblePointer(const Expr &E, const Environment &Env) { @@ -490,8 +489,8 @@ void transferValueOrImpl( if (HasValueVal == nullptr) return; - Env.addToFlowCondition(ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr), - HasValueVal->formula())); + Env.assume(ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr), + HasValueVal->formula())); } void transferValueOrStringEmptyCall(const clang::Expr *ComparisonExpr, @@ -717,8 +716,8 @@ void transferOptionalAndOptionalCmp(const clang::CXXOperatorCallExpr *CmpExpr, if (auto *RHasVal = getHasValue(Env, Env.getValue(*CmpExpr->getArg(1)))) { if (CmpExpr->getOperator() == clang::OO_ExclaimEqual) CmpValue = &A.makeNot(*CmpValue); - Env.addToFlowCondition(evaluateEquality(A, *CmpValue, LHasVal->formula(), - RHasVal->formula())); + Env.assume(evaluateEquality(A, *CmpValue, LHasVal->formula(), + RHasVal->formula())); } } @@ -729,7 +728,7 @@ void transferOptionalAndValueCmp(const clang::CXXOperatorCallExpr *CmpExpr, if (auto *HasVal = getHasValue(Env, Env.getValue(*E))) { if (CmpExpr->getOperator() == clang::OO_ExclaimEqual) CmpValue = &A.makeNot(*CmpValue); - Env.addToFlowCondition( + Env.assume( evaluateEquality(A, *CmpValue, HasVal->formula(), A.makeLiteral(true))); } } @@ -917,7 +916,7 @@ llvm::SmallVector<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->formula())) + if (Env.proves(HasValueVal->formula())) return {}; } } @@ -1004,14 +1003,13 @@ bool UncheckedOptionalAccessModel::merge(QualType Type, const Value &Val1, bool MustNonEmpty1 = isNonEmptyOptional(Val1, Env1); bool MustNonEmpty2 = isNonEmptyOptional(Val2, Env2); if (MustNonEmpty1 && MustNonEmpty2) - MergedEnv.addToFlowCondition(HasValueVal.formula()); + MergedEnv.assume(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.arena().makeNot(HasValueVal.formula())); + MergedEnv.assume(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 23b062665a687ca..e54fb2a01ddeead 100644 --- a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp +++ b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp @@ -148,7 +148,7 @@ class TerminatorVisitor ConditionValue = false; } - Env.addToFlowCondition(Val->formula()); + Env.assume(Val->formula()); return {&Cond, ConditionValue}; } diff --git a/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp b/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp index 1cb51a9cf37c5c4..a2762046665a2ce 100644 --- a/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp @@ -159,7 +159,7 @@ TEST(ChromiumCheckModelTest, CheckSuccessImpliesConditionHolds) { auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl)); - EXPECT_TRUE(Env.flowConditionImplies(FooVal->formula())); + EXPECT_TRUE(Env.proves(FooVal->formula())); }; std::string Code = R"( @@ -190,7 +190,7 @@ TEST(ChromiumCheckModelTest, UnrelatedCheckIgnored) { auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl)); - EXPECT_FALSE(Env.flowConditionImplies(FooVal->formula())); + EXPECT_FALSE(Env.proves(FooVal->formula())); }; std::string Code = R"( diff --git a/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp b/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp index f8897929a59cf4d..362b0dea58d6b80 100644 --- a/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp @@ -157,44 +157,44 @@ void transferBinary(const BinaryOperator *BO, const MatchFinder::MatchResult &M, switch (BO->getOpcode()) { case BO_GT: // pos > pos - State.Env.addToFlowCondition( + State.Env.assume( A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(), LHSProps.Pos->formula()))); // pos > zero - State.Env.addToFlowCondition( + State.Env.assume( A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(), LHSProps.Pos->formula()))); break; case BO_LT: // neg < neg - State.Env.addToFlowCondition( + State.Env.assume( A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(), LHSProps.Neg->formula()))); // neg < zero - State.Env.addToFlowCondition( + State.Env.assume( A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(), LHSProps.Neg->formula()))); break; case BO_GE: // pos >= pos - State.Env.addToFlowCondition( + State.Env.assume( A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(), LHSProps.Pos->formula()))); break; case BO_LE: // neg <= neg - State.Env.addToFlowCondition( + State.Env.assume( A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(), LHSProps.Neg->formula()))); break; case BO_EQ: - State.Env.addToFlowCondition( + State.Env.assume( A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(), LHSProps.Neg->formula()))); - State.Env.addToFlowCondition( + State.Env.assume( A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(), LHSProps.Zero->formula()))); - State.Env.addToFlowCondition( + State.Env.assume( A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(), LHSProps.Pos->formula()))); break; @@ -215,14 +215,14 @@ void transferUnaryMinus(const UnaryOperator *UO, return; // a is pos ==> -a is neg - State.Env.addToFlowCondition( + State.Env.assume( A.makeImplies(OperandProps.Pos->formula(), UnaryOpProps.Neg->formula())); // a is neg ==> -a is pos - State.Env.addToFlowCondition( + State.Env.assume( A.makeImplies(OperandProps.Neg->formula(), UnaryOpProps.Pos->formula())); // a is zero ==> -a is zero - State.Env.addToFlowCondition(A.makeImplies(OperandProps.Zero->formula(), - UnaryOpProps.Zero->formula())); + State.Env.assume(A.makeImplies(OperandProps.Zero->formula(), + UnaryOpProps.Zero->formula())); } void transferUnaryNot(const UnaryOperator *UO, @@ -235,7 +235,7 @@ void transferUnaryNot(const UnaryOperator *UO, return; // a is neg or pos ==> !a is zero - State.Env.addToFlowCondition(A.makeImplies( + State.Env.assume(A.makeImplies( A.makeOr(OperandProps.Pos->formula(), OperandProps.Neg->formula()), UnaryOpProps.Zero->formula())); @@ -243,11 +243,11 @@ void transferUnaryNot(const UnaryOperator *UO, // put the generic handler, transferExpr maybe? if (auto *UOBoolVal = dyn_cast<BoolValue>(UnaryOpValue)) { // !a <==> a is zero - State.Env.addToFlowCondition( + State.Env.assume( A.makeEquals(UOBoolVal->formula(), OperandProps.Zero->formula())); // !a <==> !a is not zero - State.Env.addToFlowCondition(A.makeEquals( - UOBoolVal->formula(), A.makeNot(UnaryOpProps.Zero->formula()))); + State.Env.assume(A.makeEquals(UOBoolVal->formula(), + A.makeNot(UnaryOpProps.Zero->formula()))); } } @@ -391,11 +391,10 @@ 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(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())); + if (Env1.proves(B1) && Env2.proves(B2)) { + MergedEnv.assume(MergedBool.formula()); + } else if (Env1.proves(A.makeNot(B1)) && Env2.proves(A.makeNot(B2))) { + MergedEnv.assume(A.makeNot(MergedBool.formula())); } return MergedBool; } @@ -484,7 +483,7 @@ testing::AssertionResult isPropertyImplied(const Environment &Env, if (!Prop) return Result; auto *BVProp = cast<BoolValue>(Prop); - if (Env.flowConditionImplies(BVProp->formula()) != Implies) + if (Env.proves(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 0c2106777560ee6..0f9f13df817075e 100644 --- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp @@ -3795,11 +3795,10 @@ TEST(TransferTest, BooleanEquality) { ASSERT_THAT(BarDecl, NotNull()); auto &BarValThen = getFormula(*BarDecl, EnvThen); - EXPECT_TRUE(EnvThen.flowConditionImplies(BarValThen)); + EXPECT_TRUE(EnvThen.proves(BarValThen)); auto &BarValElse = getFormula(*BarDecl, EnvElse); - EXPECT_TRUE( - EnvElse.flowConditionImplies(EnvElse.arena().makeNot(BarValElse))); + EXPECT_TRUE(EnvElse.proves(EnvElse.arena().makeNot(BarValElse))); }); } @@ -3830,11 +3829,10 @@ TEST(TransferTest, BooleanInequality) { ASSERT_THAT(BarDecl, NotNull()); auto &BarValThen = getFormula(*BarDecl, EnvThen); - EXPECT_TRUE( - EnvThen.flowConditionImplies(EnvThen.arena().makeNot(BarValThen))); + EXPECT_TRUE(EnvThen.proves(EnvThen.arena().makeNot(BarValThen))); auto &BarValElse = getFormula(*BarDecl, EnvElse); - EXPECT_TRUE(EnvElse.flowConditionImplies(BarValElse)); + EXPECT_TRUE(EnvElse.proves(BarValElse)); }); } @@ -3853,7 +3851,7 @@ TEST(TransferTest, IntegerLiteralEquality) { auto &Equal = getValueForDecl<BoolValue>(ASTCtx, Env, "equal").formula(); - EXPECT_TRUE(Env.flowConditionImplies(Equal)); + EXPECT_TRUE(Env.proves(Equal)); }); } @@ -3890,19 +3888,19 @@ TEST(TransferTest, CorrelatedBranches) { ASSERT_THAT(BDecl, NotNull()); auto &BVal = getFormula(*BDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BVal))); + EXPECT_TRUE(Env.proves(Env.arena().makeNot(BVal))); } { const Environment &Env = getEnvironmentAtAnnotation(Results, "p1"); auto &CVal = getFormula(*CDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(CVal)); + EXPECT_TRUE(Env.proves(CVal)); } { const Environment &Env = getEnvironmentAtAnnotation(Results, "p2"); auto &CVal = getFormula(*CDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(CVal)); + EXPECT_TRUE(Env.proves(CVal)); } }); } @@ -3934,7 +3932,7 @@ TEST(TransferTest, LoopWithAssignmentConverges) { ASSERT_THAT(BarDecl, NotNull()); auto &BarVal = getFormula(*BarDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal))); + EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal))); }); } @@ -3967,12 +3965,11 @@ TEST(TransferTest, LoopWithStagedAssignments) { auto &BarVal = getFormula(*BarDecl, Env); auto &ErrVal = getFormula(*ErrDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(BarVal)); + EXPECT_TRUE(Env.proves(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.arena().makeNot(ErrVal))); + EXPECT_FALSE(Env.proves(Env.arena().makeNot(ErrVal))); }); } @@ -4002,7 +3999,7 @@ TEST(TransferTest, LoopWithReferenceAssignmentConverges) { ASSERT_THAT(BarDecl, NotNull()); auto &BarVal = getFormula(*BarDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal))); + EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal))); }); } @@ -4531,11 +4528,10 @@ TEST(TransferTest, IfStmtBranchExtendsFlowCondition) { ASSERT_THAT(FooDecl, NotNull()); auto &ThenFooVal= getFormula(*FooDecl, ThenEnv); - EXPECT_TRUE(ThenEnv.flowConditionImplies(ThenFooVal)); + EXPECT_TRUE(ThenEnv.proves(ThenFooVal)); auto &ElseFooVal = getFormula(*FooDecl, ElseEnv); - EXPECT_TRUE( - ElseEnv.flowConditionImplies(ElseEnv.arena().makeNot(ElseFooVal))); + EXPECT_TRUE(ElseEnv.proves(ElseEnv.arena().makeNot(ElseFooVal))); }); } @@ -4565,11 +4561,11 @@ TEST(TransferTest, WhileStmtBranchExtendsFlowCondition) { ASSERT_THAT(FooDecl, NotNull()); auto &LoopBodyFooVal = getFormula(*FooDecl, LoopBodyEnv); - EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal)); + EXPECT_TRUE(LoopBodyEnv.proves(LoopBodyFooVal)); auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv); - EXPECT_TRUE(AfterLoopEnv.flowConditionImplies( - AfterLoopEnv.arena().makeNot(AfterLoopFooVal))); + EXPECT_TRUE( + AfterLoopEnv.proves(AfterLoopEnv.arena().makeNot(AfterLoopFooVal))); }); } @@ -4606,15 +4602,13 @@ TEST(TransferTest, DoWhileStmtBranchExtendsFlowCondition) { auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv); auto &LoopBodyBarVal = getFormula(*BarDecl, LoopBodyEnv); - EXPECT_TRUE(LoopBodyEnv.flowConditionImplies( - A.makeOr(LoopBodyBarVal, LoopBodyFooVal))); + EXPECT_TRUE( + LoopBodyEnv.proves(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))); + EXPECT_TRUE(AfterLoopEnv.proves(A.makeNot(AfterLoopFooVal))); + EXPECT_TRUE(AfterLoopEnv.proves(A.makeNot(AfterLoopBarVal))); }); } @@ -4644,11 +4638,11 @@ TEST(TransferTest, ForStmtBranchExtendsFlowCondition) { ASSERT_THAT(FooDecl, NotNull()); auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv); - EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal)); + EXPECT_TRUE(LoopBodyEnv.proves(LoopBodyFooVal)); auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv); - EXPECT_TRUE(AfterLoopEnv.flowConditionImplies( - AfterLoopEnv.arena().makeNot(AfterLoopFooVal))); + EXPECT_TRUE( + AfterLoopEnv.proves(AfterLoopEnv.arena().makeNot(AfterLoopFooVal))); }); } @@ -4673,7 +4667,7 @@ TEST(TransferTest, ForStmtBranchWithoutConditionDoesNotExtendFlowCondition) { ASSERT_THAT(FooDecl, NotNull()); auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv); - EXPECT_FALSE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal)); + EXPECT_FALSE(LoopBodyEnv.proves(LoopBodyFooVal)); }); } @@ -4699,8 +4693,8 @@ TEST(TransferTest, ContextSensitiveOptionDisabled) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_FALSE(Env.flowConditionImplies(FooVal)); - EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal))); + EXPECT_FALSE(Env.proves(FooVal)); + EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal))); }, {BuiltinOptions{/*.ContextSensitiveOpts=*/std::nullopt}}); } @@ -4838,8 +4832,8 @@ TEST(TransferTest, ContextSensitiveDepthZero) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_FALSE(Env.flowConditionImplies(FooVal)); - EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal))); + EXPECT_FALSE(Env.proves(FooVal)); + EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal))); }, {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/0}}}); } @@ -4866,7 +4860,7 @@ TEST(TransferTest, ContextSensitiveSetTrue) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -4893,7 +4887,7 @@ TEST(TransferTest, ContextSensitiveSetFalse) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(FooVal))); + EXPECT_TRUE(Env.proves(Env.arena().makeNot(FooVal))); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -4926,12 +4920,12 @@ TEST(TransferTest, ContextSensitiveSetBothTrueAndFalse) { ASSERT_THAT(BarDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); - EXPECT_FALSE(Env.flowConditionImplies(A.makeNot(FooVal))); + EXPECT_TRUE(Env.proves(FooVal)); + EXPECT_FALSE(Env.proves(A.makeNot(FooVal))); auto &BarVal = getFormula(*BarDecl, Env); - EXPECT_FALSE(Env.flowConditionImplies(BarVal)); - EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(BarVal))); + EXPECT_FALSE(Env.proves(BarVal)); + EXPECT_TRUE(Env.proves(A.makeNot(BarVal))); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -4959,8 +4953,8 @@ TEST(TransferTest, ContextSensitiveSetTwoLayersDepthOne) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_FALSE(Env.flowConditionImplies(FooVal)); - EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal))); + EXPECT_FALSE(Env.proves(FooVal)); + EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal))); }, {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/1}}}); } @@ -4988,7 +4982,7 @@ TEST(TransferTest, ContextSensitiveSetTwoLayersDepthTwo) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/2}}}); } @@ -5017,8 +5011,8 @@ TEST(TransferTest, ContextSensitiveSetThreeLayersDepthTwo) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_FALSE(Env.flowConditionImplies(FooVal)); - EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal))); + EXPECT_FALSE(Env.proves(FooVal)); + EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal))); }, {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/2}}}); } @@ -5047,7 +5041,7 @@ TEST(TransferTest, ContextSensitiveSetThreeLayersDepthThree) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/3}}}); } @@ -5090,8 +5084,8 @@ TEST(TransferTest, ContextSensitiveMutualRecursion) { auto &FooVal = getFormula(*FooDecl, Env); // ... but it also can't prove anything here. - EXPECT_FALSE(Env.flowConditionImplies(FooVal)); - EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal))); + EXPECT_FALSE(Env.proves(FooVal)); + EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal))); }, {BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/4}}}); } @@ -5124,12 +5118,12 @@ TEST(TransferTest, ContextSensitiveSetMultipleLines) { ASSERT_THAT(BarDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); - EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal))); + EXPECT_TRUE(Env.proves(FooVal)); + EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal))); auto &BarVal = getFormula(*BarDecl, Env); - EXPECT_FALSE(Env.flowConditionImplies(BarVal)); - EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal))); + EXPECT_FALSE(Env.proves(BarVal)); + EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal))); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5166,12 +5160,12 @@ TEST(TransferTest, ContextSensitiveSetMultipleBlocks) { ASSERT_THAT(BazDecl, NotNull()); auto &BarVal = getFormula(*BarDecl, Env); - EXPECT_FALSE(Env.flowConditionImplies(BarVal)); - EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal))); + EXPECT_FALSE(Env.proves(BarVal)); + EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal))); auto &BazVal = getFormula(*BazDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(BazVal)); - EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(BazVal))); + EXPECT_TRUE(Env.proves(BazVal)); + EXPECT_FALSE(Env.proves(Env.arena().makeNot(BazVal))); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5215,7 +5209,7 @@ TEST(TransferTest, ContextSensitiveReturnTrue) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5240,7 +5234,7 @@ TEST(TransferTest, ContextSensitiveReturnFalse) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(FooVal))); + EXPECT_TRUE(Env.proves(Env.arena().makeNot(FooVal))); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5268,7 +5262,7 @@ TEST(TransferTest, ContextSensitiveReturnArg) { ASSERT_THAT(BazDecl, NotNull()); auto &BazVal = getFormula(*BazDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(BazVal)); + EXPECT_TRUE(Env.proves(BazVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5316,7 +5310,7 @@ TEST(TransferTest, ContextSensitiveMethodLiteral) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5348,7 +5342,7 @@ TEST(TransferTest, ContextSensitiveMethodGetter) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5380,7 +5374,7 @@ TEST(TransferTest, ContextSensitiveMethodSetter) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5414,7 +5408,7 @@ TEST(TransferTest, ContextSensitiveMethodGetterAndSetter) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5449,7 +5443,7 @@ TEST(TransferTest, ContextSensitiveMethodTwoLayersVoid) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5483,7 +5477,7 @@ TEST(TransferTest, ContextSensitiveMethodTwoLayersReturn) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5514,7 +5508,7 @@ TEST(TransferTest, ContextSensitiveConstructorBody) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5545,7 +5539,7 @@ TEST(TransferTest, ContextSensitiveConstructorInitializer) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5576,7 +5570,7 @@ TEST(TransferTest, ContextSensitiveConstructorDefault) { ASSERT_THAT(FooDecl, NotNull()); auto &FooVal = getFormula(*FooDecl, Env); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }, {BuiltinOptions{ContextSensitiveOptions{}}}); } @@ -5656,7 +5650,7 @@ TEST(TransferTest, ChainedLogicalOps) { ASTContext &ASTCtx) { const Environment &Env = getEnvironmentAtAnnotation(Results, "p"); auto &B = getValueForDecl<BoolValue>(ASTCtx, Env, "b").formula(); - EXPECT_TRUE(Env.flowConditionImplies(B)); + EXPECT_TRUE(Env.proves(B)); }); } @@ -5701,30 +5695,30 @@ TEST(TransferTest, NoReturnFunctionInsideShortCircuitedBooleanOp) { auto &A = Env.arena(); // Check that [[p]] is reachable with a non-false flow condition. - EXPECT_FALSE(Env.flowConditionImplies(A.makeLiteral(false))); + EXPECT_FALSE(Env.proves(A.makeLiteral(false))); auto &B1 = getValueForDecl<BoolValue>(ASTCtx, Env, "b1").formula(); - EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(B1))); + EXPECT_TRUE(Env.proves(A.makeNot(B1))); auto &NoreturnOnRhsOfAnd = getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfAnd").formula(); - EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(NoreturnOnRhsOfAnd))); + EXPECT_TRUE(Env.proves(A.makeNot(NoreturnOnRhsOfAnd))); auto &B2 = getValueForDecl<BoolValue>(ASTCtx, Env, "b2").formula(); - EXPECT_TRUE(Env.flowConditionImplies(B2)); + EXPECT_TRUE(Env.proves(B2)); auto &NoreturnOnRhsOfOr = getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfOr") .formula(); - EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnRhsOfOr)); + EXPECT_TRUE(Env.proves(NoreturnOnRhsOfOr)); auto &NoreturnOnLhsMakesAndUnreachable = getValueForDecl<BoolValue>( ASTCtx, Env, "NoreturnOnLhsMakesAndUnreachable").formula(); - EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnLhsMakesAndUnreachable)); + EXPECT_TRUE(Env.proves(NoreturnOnLhsMakesAndUnreachable)); auto &NoreturnOnLhsMakesOrUnreachable = getValueForDecl<BoolValue>( ASTCtx, Env, "NoreturnOnLhsMakesOrUnreachable").formula(); - EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnLhsMakesOrUnreachable)); + EXPECT_TRUE(Env.proves(NoreturnOnLhsMakesOrUnreachable)); }); } @@ -5944,7 +5938,7 @@ TEST(TransferTest, AnonymousStruct) { S->getChild(*cast<ValueDecl>(IndirectField->chain().front()))); auto *B = cast<BoolValue>(getFieldValue(&AnonStruct, *BDecl, Env)); - ASSERT_TRUE(Env.flowConditionImplies(B->formula())); + ASSERT_TRUE(Env.proves(B->formula())); }); } @@ -5975,7 +5969,7 @@ TEST(TransferTest, AnonymousStructWithInitializer) { *cast<ValueDecl>(IndirectField->chain().front()))); auto *B = cast<BoolValue>(getFieldValue(&AnonStruct, *BDecl, Env)); - ASSERT_TRUE(Env.flowConditionImplies(B->formula())); + ASSERT_TRUE(Env.proves(B->formula())); }); } diff --git a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp index 8422f3804db5494..e33bea47137ad73 100644 --- a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp @@ -450,8 +450,7 @@ class SpecialBoolAnalysis final if (IsSet2 == nullptr) return ComparisonResult::Different; - return Env1.flowConditionImplies(IsSet1->formula()) == - Env2.flowConditionImplies(IsSet2->formula()) + return Env1.proves(IsSet1->formula()) == Env2.proves(IsSet2->formula()) ? ComparisonResult::Same : ComparisonResult::Different; } @@ -475,9 +474,8 @@ class SpecialBoolAnalysis final auto &IsSet = MergedEnv.makeAtomicBoolValue(); MergedVal.setProperty("is_set", IsSet); - if (Env1.flowConditionImplies(IsSet1->formula()) && - Env2.flowConditionImplies(IsSet2->formula())) - MergedEnv.addToFlowCondition(IsSet.formula()); + if (Env1.proves(IsSet1->formula()) && Env2.proves(IsSet2->formula())) + MergedEnv.assume(IsSet.formula()); return true; } @@ -544,10 +542,10 @@ TEST_F(JoinFlowConditionsTest, JoinDistinctButProvablyEquivalentValues) { ->formula(); }; - EXPECT_FALSE(Env1.flowConditionImplies(GetFoo(Env1))); - EXPECT_TRUE(Env2.flowConditionImplies(GetFoo(Env2))); - EXPECT_TRUE(Env3.flowConditionImplies(GetFoo(Env3))); - EXPECT_TRUE(Env4.flowConditionImplies(GetFoo(Env4))); + EXPECT_FALSE(Env1.proves(GetFoo(Env1))); + EXPECT_TRUE(Env2.proves(GetFoo(Env2))); + EXPECT_TRUE(Env3.proves(GetFoo(Env3))); + EXPECT_TRUE(Env4.proves(GetFoo(Env4))); }); } @@ -849,11 +847,11 @@ TEST_F(FlowConditionTest, IfStmtSingleVar) { const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula(); - EXPECT_TRUE(Env1.flowConditionImplies(FooVal1)); + EXPECT_TRUE(Env1.proves(FooVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula(); - EXPECT_FALSE(Env2.flowConditionImplies(FooVal2)); + EXPECT_FALSE(Env2.proves(FooVal2)); }); } @@ -880,11 +878,11 @@ TEST_F(FlowConditionTest, IfStmtSingleNegatedVar) { const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula(); - EXPECT_FALSE(Env1.flowConditionImplies(FooVal1)); + EXPECT_FALSE(Env1.proves(FooVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula(); - EXPECT_TRUE(Env2.flowConditionImplies(FooVal2)); + EXPECT_TRUE(Env2.proves(FooVal2)); }); } @@ -908,7 +906,7 @@ TEST_F(FlowConditionTest, WhileStmt) { const Environment &Env = getEnvironmentAtAnnotation(Results, "p"); auto &FooVal = cast<BoolValue>(Env.getValue(*FooDecl))->formula(); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }); } @@ -931,7 +929,7 @@ TEST_F(FlowConditionTest, WhileStmtWithAssignmentInCondition) { ASTContext &ASTCtx) { const Environment &Env = getEnvironmentAtAnnotation(Results, "p"); auto &FooVal = getValueForDecl<BoolValue>(ASTCtx, Env, "Foo").formula(); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }); } @@ -961,14 +959,14 @@ TEST_F(FlowConditionTest, Conjunction) { const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); 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)); + EXPECT_TRUE(Env1.proves(FooVal1)); + EXPECT_TRUE(Env1.proves(BarVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); 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)); + EXPECT_FALSE(Env2.proves(FooVal2)); + EXPECT_FALSE(Env2.proves(BarVal2)); }); } @@ -998,14 +996,14 @@ TEST_F(FlowConditionTest, Disjunction) { const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); 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)); + EXPECT_FALSE(Env1.proves(FooVal1)); + EXPECT_FALSE(Env1.proves(BarVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); 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)); + EXPECT_FALSE(Env2.proves(FooVal2)); + EXPECT_FALSE(Env2.proves(BarVal2)); }); } @@ -1035,14 +1033,14 @@ TEST_F(FlowConditionTest, NegatedConjunction) { const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); 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)); + EXPECT_FALSE(Env1.proves(FooVal1)); + EXPECT_FALSE(Env1.proves(BarVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); 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)); + EXPECT_TRUE(Env2.proves(FooVal2)); + EXPECT_TRUE(Env2.proves(BarVal2)); }); } @@ -1072,14 +1070,14 @@ TEST_F(FlowConditionTest, DeMorgan) { const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); 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)); + EXPECT_TRUE(Env1.proves(FooVal1)); + EXPECT_TRUE(Env1.proves(BarVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); 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)); + EXPECT_FALSE(Env2.proves(FooVal2)); + EXPECT_FALSE(Env2.proves(BarVal2)); }); } @@ -1108,7 +1106,7 @@ TEST_F(FlowConditionTest, Join) { const Environment &Env = getEnvironmentAtAnnotation(Results, "p"); auto &FooVal = cast<BoolValue>(Env.getValue(*FooDecl))->formula(); - EXPECT_TRUE(Env.flowConditionImplies(FooVal)); + EXPECT_TRUE(Env.proves(FooVal)); }); } @@ -1142,7 +1140,7 @@ TEST_F(FlowConditionTest, OpaqueFlowConditionMergesToOpaqueBool) { auto &BarVal = cast<BoolValue>(Env.getValue(*BarDecl))->formula(); - EXPECT_FALSE(Env.flowConditionImplies(BarVal)); + EXPECT_FALSE(Env.proves(BarVal)); }); } @@ -1183,7 +1181,7 @@ TEST_F(FlowConditionTest, OpaqueFieldFlowConditionMergesToOpaqueBool) { auto &BarVal = cast<BoolValue>(Env.getValue(*BarDecl))->formula(); - EXPECT_FALSE(Env.flowConditionImplies(BarVal)); + EXPECT_FALSE(Env.proves(BarVal)); }); } @@ -1217,7 +1215,7 @@ TEST_F(FlowConditionTest, OpaqueFlowConditionInsideBranchMergesToOpaqueBool) { auto &BarVal = cast<BoolValue>(Env.getValue(*BarDecl))->formula(); - EXPECT_FALSE(Env.flowConditionImplies(BarVal)); + EXPECT_FALSE(Env.proves(BarVal)); }); } @@ -1245,11 +1243,11 @@ TEST_F(FlowConditionTest, PointerToBoolImplicitCast) { const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1"); auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula(); - EXPECT_TRUE(Env1.flowConditionImplies(FooVal1)); + EXPECT_TRUE(Env1.proves(FooVal1)); const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2"); auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula(); - EXPECT_FALSE(Env2.flowConditionImplies(FooVal2)); + EXPECT_FALSE(Env2.proves(FooVal2)); }); } @@ -1585,7 +1583,7 @@ TEST_F(TopTest, TopUsedInBothBranchesWithoutPrecisionLoss) { auto *BarVal = dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl)); ASSERT_THAT(BarVal, NotNull()); - EXPECT_TRUE(Env.flowConditionImplies( + EXPECT_TRUE(Env.proves( Env.arena().makeEquals(FooVal->formula(), BarVal->formula()))); }); } _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
