From 3353f7dd3d91c9b2b6a15ba9229bee53e0cb8196 Mon Sep 17 00:00:00 2001 From: Douglas Yung Date: Fri, 22 Sep 2023 11:43:27 -0700 Subject: [PATCH] Revert "[dataflow] use true/false literals in formulas, rather than variables" This reverts commit 36bd5bd888f193b70abf43a09bb4fc04cd2a2ff1. This change is causing a test failure on several build bots: - https://lab.llvm.org/buildbot/#/builders/139/builds/50255 - https://lab.llvm.org/buildbot/#/builders/216/builds/27735 - https://lab.llvm.org/buildbot/#/builders/247/builds/9334 --- .../clang/Analysis/FlowSensitive/Arena.h | 10 +- .../FlowSensitive/DataflowEnvironment.h | 5 +- .../clang/Analysis/FlowSensitive/Formula.h | 15 +-- clang/lib/Analysis/FlowSensitive/Arena.cpp | 100 +++++++----------- .../FlowSensitive/DataflowAnalysisContext.cpp | 9 +- clang/lib/Analysis/FlowSensitive/Formula.cpp | 17 +-- .../FlowSensitive/WatchedLiteralsSolver.cpp | 3 - .../Analysis/FlowSensitive/ArenaTest.cpp | 55 +++++----- .../FlowSensitive/DebugSupportTest.cpp | 20 ++-- .../Analysis/FlowSensitive/TestingSupport.h | 5 - .../Analysis/FlowSensitive/TransferTest.cpp | 6 +- 11 files changed, 98 insertions(+), 147 deletions(-) diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h index 4be308c43fb7..4e07053aae1a 100644 --- a/clang/include/clang/Analysis/FlowSensitive/Arena.h +++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h @@ -20,9 +20,7 @@ namespace clang::dataflow { /// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`. class Arena { public: - Arena() - : True(Formula::create(Alloc, Formula::Literal, {}, 1)), - False(Formula::create(Alloc, Formula::Literal, {}, 0)) {} + Arena() : True(makeAtom()), False(makeAtom()) {} Arena(const Arena &) = delete; Arena &operator=(const Arena &) = delete; @@ -108,7 +106,9 @@ class Arena { const Formula &makeAtomRef(Atom A); /// Returns a formula for a literal true/false. - const Formula &makeLiteral(bool Value) { return Value ? True : False; } + const Formula &makeLiteral(bool Value) { + return makeAtomRef(Value ? True : False); + } // Parses a formula from its textual representation. // This may refer to atoms that were not produced by makeAtom() yet! @@ -144,7 +144,7 @@ class Arena { llvm::DenseMap FormulaValues; unsigned NextAtom = 0; - const Formula &True, &False; + Atom True, False; }; } // namespace clang::dataflow diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h index 57e9d2fc87c2..c128ee4ea85c 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h @@ -466,8 +466,9 @@ class Environment { /// Returns a symbolic boolean value that models a boolean literal equal to /// `Value` - BoolValue &getBoolLiteralValue(bool Value) const { - return arena().makeBoolValue(arena().makeLiteral(Value)); + AtomicBoolValue &getBoolLiteralValue(bool Value) const { + return cast( + arena().makeBoolValue(arena().makeLiteral(Value))); } /// Returns an atomic boolean value. diff --git a/clang/include/clang/Analysis/FlowSensitive/Formula.h b/clang/include/clang/Analysis/FlowSensitive/Formula.h index 7cd9f29961ba..51264444fda8 100644 --- a/clang/include/clang/Analysis/FlowSensitive/Formula.h +++ b/clang/include/clang/Analysis/FlowSensitive/Formula.h @@ -53,8 +53,7 @@ class alignas(const Formula *) Formula { /// A reference to an atomic boolean variable. /// We name these e.g. "V3", where 3 == atom identity == Value. AtomRef, - /// Constant true or false. - Literal, + // FIXME: add const true/false rather than modeling them as variables Not, /// True if its only operand is false @@ -71,11 +70,6 @@ class alignas(const Formula *) Formula { return static_cast(Value); } - bool literal() const { - assert(kind() == Literal); - return static_cast(Value); - } - ArrayRef operands() const { return ArrayRef(reinterpret_cast(this + 1), numOperands(kind())); @@ -88,9 +82,9 @@ class alignas(const Formula *) Formula { void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const; // Allocate Formulas using Arena rather than calling this function directly. - static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K, - ArrayRef Operands, - unsigned Value = 0); + static Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K, + ArrayRef Operands, + unsigned Value = 0); private: Formula() = default; @@ -100,7 +94,6 @@ class alignas(const Formula *) Formula { static unsigned numOperands(Kind K) { switch (K) { case AtomRef: - case Literal: return 0; case Not: return 1; diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp index 81137e8088e3..b043a52b609d 100644 --- a/clang/lib/Analysis/FlowSensitive/Arena.cpp +++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp @@ -22,83 +22,63 @@ canonicalFormulaPair(const Formula &LHS, const Formula &RHS) { return Res; } -template -const Formula &cached(llvm::DenseMap &Cache, Key K, - ComputeFunc &&Compute) { - auto [It, Inserted] = Cache.try_emplace(std::forward(K)); +const Formula &Arena::makeAtomRef(Atom A) { + auto [It, Inserted] = AtomRefs.try_emplace(A); if (Inserted) - It->second = Compute(); + It->second = + &Formula::create(Alloc, Formula::AtomRef, {}, static_cast(A)); return *It->second; } -const Formula &Arena::makeAtomRef(Atom A) { - return cached(AtomRefs, A, [&] { - return &Formula::create(Alloc, Formula::AtomRef, {}, - static_cast(A)); - }); -} - const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) { - return cached(Ands, canonicalFormulaPair(LHS, RHS), [&] { - if (&LHS == &RHS) - return &LHS; - if (LHS.kind() == Formula::Literal) - return LHS.literal() ? &RHS : &LHS; - if (RHS.kind() == Formula::Literal) - return RHS.literal() ? &LHS : &RHS; - - return &Formula::create(Alloc, Formula::And, {&LHS, &RHS}); - }); + if (&LHS == &RHS) + return LHS; + + auto [It, Inserted] = + Ands.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr); + if (Inserted) + It->second = &Formula::create(Alloc, Formula::And, {&LHS, &RHS}); + return *It->second; } const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) { - return cached(Ors, canonicalFormulaPair(LHS, RHS), [&] { - if (&LHS == &RHS) - return &LHS; - if (LHS.kind() == Formula::Literal) - return LHS.literal() ? &LHS : &RHS; - if (RHS.kind() == Formula::Literal) - return RHS.literal() ? &RHS : &LHS; - - return &Formula::create(Alloc, Formula::Or, {&LHS, &RHS}); - }); + if (&LHS == &RHS) + return LHS; + + auto [It, Inserted] = + Ors.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr); + if (Inserted) + It->second = &Formula::create(Alloc, Formula::Or, {&LHS, &RHS}); + return *It->second; } const Formula &Arena::makeNot(const Formula &Val) { - return cached(Nots, &Val, [&] { - if (Val.kind() == Formula::Not) - return Val.operands()[0]; - if (Val.kind() == Formula::Literal) - return &makeLiteral(!Val.literal()); - - return &Formula::create(Alloc, Formula::Not, {&Val}); - }); + auto [It, Inserted] = Nots.try_emplace(&Val, nullptr); + if (Inserted) + It->second = &Formula::create(Alloc, Formula::Not, {&Val}); + return *It->second; } const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) { - return cached(Implies, std::make_pair(&LHS, &RHS), [&] { - if (&LHS == &RHS) - return &makeLiteral(true); - if (LHS.kind() == Formula::Literal) - return LHS.literal() ? &RHS : &makeLiteral(true); - if (RHS.kind() == Formula::Literal) - return RHS.literal() ? &RHS : &makeNot(LHS); - - return &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS}); - }); + if (&LHS == &RHS) + return makeLiteral(true); + + auto [It, Inserted] = + Implies.try_emplace(std::make_pair(&LHS, &RHS), nullptr); + if (Inserted) + It->second = &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS}); + return *It->second; } const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) { - return cached(Equals, canonicalFormulaPair(LHS, RHS), [&] { - if (&LHS == &RHS) - return &makeLiteral(true); - if (LHS.kind() == Formula::Literal) - return LHS.literal() ? &RHS : &makeNot(RHS); - if (RHS.kind() == Formula::Literal) - return RHS.literal() ? &LHS : &makeNot(LHS); - - return &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS}); - }); + if (&LHS == &RHS) + return makeLiteral(true); + + auto [It, Inserted] = + Equals.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr); + if (Inserted) + It->second = &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS}); + return *It->second; } IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) { diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp index 28a859555461..e81048ce9233 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -141,6 +141,8 @@ DataflowAnalysisContext::joinFlowConditions(Atom FirstToken, Solver::Result DataflowAnalysisContext::querySolver( llvm::SetVector Constraints) { + Constraints.insert(&arena().makeLiteral(true)); + Constraints.insert(&arena().makeNot(arena().makeLiteral(false))); return S->solve(Constraints.getArrayRef()); } @@ -211,8 +213,13 @@ void DataflowAnalysisContext::dumpFlowCondition(Atom Token, Constraints.insert(&arena().makeAtomRef(Token)); addTransitiveFlowConditionConstraints(Token, Constraints); + // TODO: have formulas know about true/false directly instead + Atom True = arena().makeLiteral(true).getAtom(); + Atom False = arena().makeLiteral(false).getAtom(); + Formula::AtomNames Names = {{False, "false"}, {True, "true"}}; + for (const auto *Constraint : Constraints) { - Constraint->print(OS); + Constraint->print(OS, &Names); OS << "\n"; } } diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp index ef7d23ff6c56..6d22efc5db07 100644 --- a/clang/lib/Analysis/FlowSensitive/Formula.cpp +++ b/clang/lib/Analysis/FlowSensitive/Formula.cpp @@ -17,9 +17,8 @@ namespace clang::dataflow { -const Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K, - ArrayRef Operands, - unsigned Value) { +Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K, + ArrayRef Operands, unsigned Value) { assert(Operands.size() == numOperands(K)); if (Value != 0) // Currently, formulas have values or operands, not both. assert(numOperands(K) == 0); @@ -39,7 +38,6 @@ const Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K, static llvm::StringLiteral sigil(Formula::Kind K) { switch (K) { case Formula::AtomRef: - case Formula::Literal: return ""; case Formula::Not: return "!"; @@ -64,16 +62,7 @@ void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const { switch (numOperands(kind())) { case 0: - switch (kind()) { - case AtomRef: - OS << getAtom(); - break; - case Literal: - OS << (literal() ? "true" : "false"); - break; - default: - llvm_unreachable("unhandled formula kind"); - } + OS << getAtom(); break; case 1: OS << sigil(kind()); diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp index 3ef363753532..ab3a8104e317 100644 --- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp +++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp @@ -322,9 +322,6 @@ CNFFormula buildCNF(const llvm::ArrayRef &Vals) { switch (Val->kind()) { case Formula::AtomRef: break; - case Formula::Literal: - CNF.addClause(Val->literal() ? posLit(Var) : negLit(Var)); - break; case Formula::And: { const Variable LHS = GetVar(Val->operands()[0]); const Variable RHS = GetVar(Val->operands()[1]); diff --git a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp index 5f85bfeb9e79..1208b78a308d 100644 --- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp @@ -34,6 +34,12 @@ TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) { EXPECT_NE(&X, &Y); } +TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) { + auto &X = A.makeAtomRef(A.makeAtom()); + auto &XAndX = A.makeAnd(X, X); + EXPECT_EQ(&XAndX, &X); +} + TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) { auto &X = A.makeAtomRef(A.makeAtom()); auto &Y = A.makeAtomRef(A.makeAtom()); @@ -49,6 +55,12 @@ TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) { EXPECT_NE(&XAndY1, &XAndZ); } +TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) { + auto &X = A.makeAtomRef(A.makeAtom()); + auto &XOrX = A.makeOr(X, X); + EXPECT_EQ(&XOrX, &X); +} + TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) { auto &X = A.makeAtomRef(A.makeAtom()); auto &Y = A.makeAtomRef(A.makeAtom()); @@ -74,6 +86,12 @@ TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) { EXPECT_NE(&NotX1, &NotY); } +TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) { + auto &X = A.makeAtomRef(A.makeAtom()); + auto &XImpliesX = A.makeImplies(X, X); + EXPECT_EQ(&XImpliesX, &A.makeLiteral(true)); +} + TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) { auto &X = A.makeAtomRef(A.makeAtom()); auto &Y = A.makeAtomRef(A.makeAtom()); @@ -89,6 +107,12 @@ TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) { EXPECT_NE(&XImpliesY1, &XImpliesZ); } +TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) { + auto &X = A.makeAtomRef(A.makeAtom()); + auto &XIffX = A.makeEquals(X, X); + EXPECT_EQ(&XIffX, &A.makeLiteral(true)); +} + TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) { auto &X = A.makeAtomRef(A.makeAtom()); auto &Y = A.makeAtomRef(A.makeAtom()); @@ -157,36 +181,5 @@ V1 V2 ^)")); } -TEST_F(ArenaTest, IdentitySimplification) { - auto &X = A.makeAtomRef(A.makeAtom()); - - EXPECT_EQ(&X, &A.makeAnd(X, X)); - EXPECT_EQ(&X, &A.makeOr(X, X)); - EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, X)); - EXPECT_EQ(&A.makeLiteral(true), &A.makeEquals(X, X)); - EXPECT_EQ(&X, &A.makeNot(A.makeNot(X))); -} - -TEST_F(ArenaTest, LiteralSimplification) { - auto &X = A.makeAtomRef(A.makeAtom()); - - EXPECT_EQ(&X, &A.makeAnd(X, A.makeLiteral(true))); - EXPECT_EQ(&A.makeLiteral(false), &A.makeAnd(X, A.makeLiteral(false))); - - EXPECT_EQ(&A.makeLiteral(true), &A.makeOr(X, A.makeLiteral(true))); - EXPECT_EQ(&X, &A.makeOr(X, A.makeLiteral(false))); - - EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, A.makeLiteral(true))); - EXPECT_EQ(&A.makeNot(X), &A.makeImplies(X, A.makeLiteral(false))); - EXPECT_EQ(&X, &A.makeImplies(A.makeLiteral(true), X)); - EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(A.makeLiteral(false), X)); - - EXPECT_EQ(&X, &A.makeEquals(X, A.makeLiteral(true))); - EXPECT_EQ(&A.makeNot(X), &A.makeEquals(X, A.makeLiteral(false))); - - EXPECT_EQ(&A.makeLiteral(false), &A.makeNot(A.makeLiteral(true))); - EXPECT_EQ(&A.makeLiteral(true), &A.makeNot(A.makeLiteral(false))); -} - } // namespace } // namespace clang::dataflow diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp index cf266f4c3a83..22bf8cadd111 100644 --- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp @@ -30,12 +30,6 @@ TEST(BoolValueDebugStringTest, AtomicBoolean) { EXPECT_THAT(llvm::to_string(*B), StrEq(Expected)); } -TEST(BoolValueDebugStringTest, Literal) { - ConstraintContext Ctx; - EXPECT_EQ("true", llvm::to_string(*Ctx.literal(true))); - EXPECT_EQ("false", llvm::to_string(*Ctx.literal(false))); -} - TEST(BoolValueDebugStringTest, Negation) { ConstraintContext Ctx; auto B = Ctx.neg(Ctx.atom()); @@ -97,14 +91,16 @@ TEST(BoolValueDebugStringTest, NestedBoolean) { TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) { ConstraintContext Ctx; - auto X = Ctx.atom(); - auto Y = Ctx.atom(); + auto True = Ctx.atom(); + auto False = Ctx.atom(); + auto V2 = Ctx.atom(); + auto V3 = Ctx.atom(); Formula::AtomNames Names; - Names[X->getAtom()] = "X"; - Names[Y->getAtom()] = "Y"; - auto B = Ctx.disj(Ctx.conj(Y, Ctx.atom()), Ctx.disj(X, Ctx.atom())); + Names[True->getAtom()] = "true"; + Names[False->getAtom()] = "false"; + auto B = Ctx.disj(Ctx.conj(False, V2), Ctx.disj(True, V3)); - auto Expected = R"(((Y & V2) | (X | V3)))"; + auto Expected = R"(((false & V2) | (true | V3)))"; std::string Actual; llvm::raw_string_ostream OS(Actual); B->print(OS, &Names); diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h index 434727c68b31..44d962d5da9a 100644 --- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h +++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h @@ -482,11 +482,6 @@ class ConstraintContext { return &Formula::create(A, Formula::AtomRef, {}, NextAtom++); } - // Returns a reference to a literal boolean value. - const Formula *literal(bool B) { - return &Formula::create(A, Formula::Literal, {}, B); - } - // Creates a boolean conjunction. const Formula *conj(const Formula *LHS, const Formula *RHS) { return make(Formula::And, {LHS, RHS}); diff --git a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp index 0e7f72ade427..e8cbca756460 100644 --- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp @@ -3202,14 +3202,14 @@ TEST(TransferTest, AssignFromBoolLiteral) { ASSERT_THAT(FooDecl, NotNull()); const auto *FooVal = - dyn_cast_or_null(Env.getValue(*FooDecl)); + dyn_cast_or_null(Env.getValue(*FooDecl)); ASSERT_THAT(FooVal, NotNull()); const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); const auto *BarVal = - dyn_cast_or_null(Env.getValue(*BarDecl)); + dyn_cast_or_null(Env.getValue(*BarDecl)); ASSERT_THAT(BarVal, NotNull()); EXPECT_EQ(FooVal, &Env.getBoolLiteralValue(true)); @@ -3387,7 +3387,7 @@ TEST(TransferTest, AssignFromBoolNegation) { ASSERT_THAT(FooDecl, NotNull()); const auto *FooVal = - dyn_cast_or_null(Env.getValue(*FooDecl)); + dyn_cast_or_null(Env.getValue(*FooDecl)); ASSERT_THAT(FooVal, NotNull()); const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");