Author: Sam McCall Date: 2023-09-22T17:12:20+02:00 New Revision: 36bd5bd888f193b70abf43a09bb4fc04cd2a2ff1
URL: https://github.com/llvm/llvm-project/commit/36bd5bd888f193b70abf43a09bb4fc04cd2a2ff1 DIFF: https://github.com/llvm/llvm-project/commit/36bd5bd888f193b70abf43a09bb4fc04cd2a2ff1.diff LOG: [dataflow] use true/false literals in formulas, rather than variables And simplify formulas containing true/false It's unclear to me how useful this is, it does make formulas more conveniently self-contained now (we can usefully print them without carrying around the "true/false" labels) (while here, simplify !!X to X, too) Differential Revision: https://reviews.llvm.org/D153485 Added: Modified: clang/include/clang/Analysis/FlowSensitive/Arena.h clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h clang/include/clang/Analysis/FlowSensitive/Formula.h clang/lib/Analysis/FlowSensitive/Arena.cpp clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp clang/lib/Analysis/FlowSensitive/Formula.cpp clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp clang/unittests/Analysis/FlowSensitive/TestingSupport.h clang/unittests/Analysis/FlowSensitive/TransferTest.cpp Removed: ################################################################################ diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h index 4e07053aae1af53..4be308c43fb7675 100644 --- a/clang/include/clang/Analysis/FlowSensitive/Arena.h +++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h @@ -20,7 +20,9 @@ namespace clang::dataflow { /// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`. class Arena { public: - Arena() : True(makeAtom()), False(makeAtom()) {} + Arena() + : True(Formula::create(Alloc, Formula::Literal, {}, 1)), + False(Formula::create(Alloc, Formula::Literal, {}, 0)) {} Arena(const Arena &) = delete; Arena &operator=(const Arena &) = delete; @@ -106,9 +108,7 @@ class Arena { const Formula &makeAtomRef(Atom A); /// Returns a formula for a literal true/false. - const Formula &makeLiteral(bool Value) { - return makeAtomRef(Value ? True : False); - } + const Formula &makeLiteral(bool Value) { return 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<const Formula *, BoolValue *> FormulaValues; unsigned NextAtom = 0; - Atom True, False; + const Formula &True, &False; }; } // namespace clang::dataflow diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h index c128ee4ea85c928..57e9d2fc87c2f41 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h @@ -466,9 +466,8 @@ class Environment { /// Returns a symbolic boolean value that models a boolean literal equal to /// `Value` - AtomicBoolValue &getBoolLiteralValue(bool Value) const { - return cast<AtomicBoolValue>( - arena().makeBoolValue(arena().makeLiteral(Value))); + BoolValue &getBoolLiteralValue(bool Value) const { + return 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 51264444fda8440..7cd9f29961ba9ca 100644 --- a/clang/include/clang/Analysis/FlowSensitive/Formula.h +++ b/clang/include/clang/Analysis/FlowSensitive/Formula.h @@ -53,7 +53,8 @@ class alignas(const Formula *) Formula { /// A reference to an atomic boolean variable. /// We name these e.g. "V3", where 3 == atom identity == Value. AtomRef, - // FIXME: add const true/false rather than modeling them as variables + /// Constant true or false. + Literal, Not, /// True if its only operand is false @@ -70,6 +71,11 @@ class alignas(const Formula *) Formula { return static_cast<Atom>(Value); } + bool literal() const { + assert(kind() == Literal); + return static_cast<bool>(Value); + } + ArrayRef<const Formula *> operands() const { return ArrayRef(reinterpret_cast<Formula *const *>(this + 1), numOperands(kind())); @@ -82,9 +88,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 Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K, - ArrayRef<const Formula *> Operands, - unsigned Value = 0); + static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K, + ArrayRef<const Formula *> Operands, + unsigned Value = 0); private: Formula() = default; @@ -94,6 +100,7 @@ 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 b043a52b609df36..81137e8088e330b 100644 --- a/clang/lib/Analysis/FlowSensitive/Arena.cpp +++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp @@ -22,63 +22,83 @@ canonicalFormulaPair(const Formula &LHS, const Formula &RHS) { return Res; } -const Formula &Arena::makeAtomRef(Atom A) { - auto [It, Inserted] = AtomRefs.try_emplace(A); +template <class Key, class ComputeFunc> +const Formula &cached(llvm::DenseMap<Key, const Formula *> &Cache, Key K, + ComputeFunc &&Compute) { + auto [It, Inserted] = Cache.try_emplace(std::forward<Key>(K)); if (Inserted) - It->second = - &Formula::create(Alloc, Formula::AtomRef, {}, static_cast<unsigned>(A)); + It->second = Compute(); return *It->second; } -const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) { - if (&LHS == &RHS) - return LHS; +const Formula &Arena::makeAtomRef(Atom A) { + return cached(AtomRefs, A, [&] { + return &Formula::create(Alloc, Formula::AtomRef, {}, + static_cast<unsigned>(A)); + }); +} - 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::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}); + }); } const Formula &Arena::makeOr(const Formula &LHS, const Formula &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; + 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}); + }); } const Formula &Arena::makeNot(const Formula &Val) { - auto [It, Inserted] = Nots.try_emplace(&Val, nullptr); - if (Inserted) - It->second = &Formula::create(Alloc, Formula::Not, {&Val}); - return *It->second; + 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}); + }); } const Formula &Arena::makeImplies(const Formula &LHS, const Formula &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; + 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}); + }); } const Formula &Arena::makeEquals(const Formula &LHS, const Formula &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; + 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}); + }); } IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) { diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp index e81048ce9233808..28a859555461c3d 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -141,8 +141,6 @@ DataflowAnalysisContext::joinFlowConditions(Atom FirstToken, Solver::Result DataflowAnalysisContext::querySolver( llvm::SetVector<const Formula *> Constraints) { - Constraints.insert(&arena().makeLiteral(true)); - Constraints.insert(&arena().makeNot(arena().makeLiteral(false))); return S->solve(Constraints.getArrayRef()); } @@ -213,13 +211,8 @@ 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, &Names); + Constraint->print(OS); OS << "\n"; } } diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp index 6d22efc5db07be4..ef7d23ff6c56519 100644 --- a/clang/lib/Analysis/FlowSensitive/Formula.cpp +++ b/clang/lib/Analysis/FlowSensitive/Formula.cpp @@ -17,8 +17,9 @@ namespace clang::dataflow { -Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K, - ArrayRef<const Formula *> Operands, unsigned Value) { +const Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K, + ArrayRef<const Formula *> Operands, + unsigned Value) { assert(Operands.size() == numOperands(K)); if (Value != 0) // Currently, formulas have values or operands, not both. assert(numOperands(K) == 0); @@ -38,6 +39,7 @@ 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 "!"; @@ -62,7 +64,16 @@ void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const { switch (numOperands(kind())) { case 0: - OS << getAtom(); + switch (kind()) { + case AtomRef: + OS << getAtom(); + break; + case Literal: + OS << (literal() ? "true" : "false"); + break; + default: + llvm_unreachable("unhandled formula kind"); + } break; case 1: OS << sigil(kind()); diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp index ab3a8104e317174..3ef363753532460 100644 --- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp +++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp @@ -322,6 +322,9 @@ CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &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 1208b78a308d1df..5f85bfeb9e7988b 100644 --- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp @@ -34,12 +34,6 @@ 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()); @@ -55,12 +49,6 @@ 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()); @@ -86,12 +74,6 @@ 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()); @@ -107,12 +89,6 @@ 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()); @@ -181,5 +157,36 @@ 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 22bf8cadd1116ff..cf266f4c3a832dc 100644 --- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp @@ -30,6 +30,12 @@ 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()); @@ -91,16 +97,14 @@ TEST(BoolValueDebugStringTest, NestedBoolean) { TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) { ConstraintContext Ctx; - auto True = Ctx.atom(); - auto False = Ctx.atom(); - auto V2 = Ctx.atom(); - auto V3 = Ctx.atom(); + auto X = Ctx.atom(); + auto Y = Ctx.atom(); Formula::AtomNames Names; - Names[True->getAtom()] = "true"; - Names[False->getAtom()] = "false"; - auto B = Ctx.disj(Ctx.conj(False, V2), Ctx.disj(True, V3)); + Names[X->getAtom()] = "X"; + Names[Y->getAtom()] = "Y"; + auto B = Ctx.disj(Ctx.conj(Y, Ctx.atom()), Ctx.disj(X, Ctx.atom())); - auto Expected = R"(((false & V2) | (true | V3)))"; + auto Expected = R"(((Y & V2) | (X | 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 44d962d5da9a97b..434727c68b31535 100644 --- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h +++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h @@ -482,6 +482,11 @@ 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 e8cbca756460369..0e7f72ade427cd3 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<AtomicBoolValue>(Env.getValue(*FooDecl)); + dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl)); ASSERT_THAT(FooVal, NotNull()); const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); const auto *BarVal = - dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*BarDecl)); + dyn_cast_or_null<BoolValue>(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<AtomicBoolValue>(Env.getValue(*FooDecl)); + dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl)); ASSERT_THAT(FooVal, NotNull()); const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
