diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h --- a/clang/include/clang/Analysis/FlowSensitive/Arena.h +++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h @@ -19,7 +19,9 @@ /// 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 @@ 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; } /// Returns a new atomic boolean variable, distinct from any other. Atom makeAtom() { return static_cast(NextAtom++); }; @@ -140,7 +140,7 @@ llvm::DenseMap 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 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h @@ -456,9 +456,8 @@ /// Returns a symbolic boolean value that models a boolean literal equal to /// `Value` - AtomicBoolValue &getBoolLiteralValue(bool Value) const { - return cast( - 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 --- a/clang/include/clang/Analysis/FlowSensitive/Formula.h +++ b/clang/include/clang/Analysis/FlowSensitive/Formula.h @@ -50,7 +50,8 @@ /// 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 @@ -67,6 +68,11 @@ 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())); @@ -77,9 +83,9 @@ void print(llvm::raw_ostream &OS, llvm::function_ref = nullptr) const; - static Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K, - ArrayRef Operands, - unsigned Value = 0); + static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K, + ArrayRef Operands, + unsigned Value = 0); private: Formula() = default; @@ -89,6 +95,7 @@ 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 --- a/clang/lib/Analysis/FlowSensitive/Arena.cpp +++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp @@ -19,63 +19,83 @@ return Res; } -const Formula &Arena::makeAtomRef(Atom A) { - auto [It, Inserted] = AtomRefs.try_emplace(A); +template +const Formula &cached(llvm::DenseMap &Cache, Key K, + ComputeFunc &&Compute) { + auto [It, Inserted] = Cache.try_emplace(std::forward(K)); if (Inserted) - It->second = - &Formula::create(Alloc, Formula::AtomRef, {}, static_cast(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(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 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -127,8 +127,6 @@ Solver::Result DataflowAnalysisContext::querySolver( llvm::DenseSet Constraints) { - Constraints.insert(&arena().makeLiteral(true)); - Constraints.insert(&arena().makeNot(arena().makeLiteral(false))); return S->solve(Constraints); } @@ -195,26 +193,11 @@ llvm::DenseSet VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); - // TODO: have formulas know about true/false directly instead - auto &True = arena().makeLiteral(true); - auto &False = arena().makeLiteral(false); - auto Delegate = [&](llvm::raw_ostream &OS, const Formula &F) { - if (&F == &True) { - OS << "True"; - return true; - } - if (&F == &False) { - OS << "False"; - return true; - } - return false; - }; - std::vector Lines; for (const auto *Constraint : Constraints) { Lines.emplace_back(); llvm::raw_string_ostream LineOS(Lines.back()); - Constraint->print(LineOS, Delegate); + Constraint->print(LineOS); } llvm::sort(Lines); for (const auto &Line : Lines) diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp --- a/clang/lib/Analysis/FlowSensitive/Formula.cpp +++ b/clang/lib/Analysis/FlowSensitive/Formula.cpp @@ -16,8 +16,9 @@ namespace clang::dataflow { -Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K, - ArrayRef Operands, unsigned Value) { +const 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); @@ -34,6 +35,7 @@ static llvm::StringLiteral sigil(Formula::Kind K) { switch (K) { case Formula::AtomRef: + case Formula::Literal: return ""; case Formula::Not: return "!"; @@ -56,7 +58,16 @@ switch (numOperands(kind())) { case 0: - OS << atom(); + switch (kind()) { + case AtomRef: + OS << atom(); + 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 --- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp +++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp @@ -240,6 +240,9 @@ switch (Val->kind()) { case Formula::AtomRef: break; + case Formula::Literal: + Form.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 --- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp @@ -31,12 +31,6 @@ 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()); @@ -52,12 +46,6 @@ 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()); @@ -83,12 +71,6 @@ 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()); @@ -104,12 +86,6 @@ 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()); @@ -137,5 +113,36 @@ EXPECT_EQ(&B1.formula(), &F1); } +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 --- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp @@ -32,6 +32,12 @@ 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()); @@ -95,22 +101,22 @@ TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) { ConstraintContext Ctx; - auto True = Ctx.atom(); - auto False = Ctx.atom(); + auto X = Ctx.atom(); + auto Y = Ctx.atom(); auto Delegate = [&](llvm::raw_ostream &OS, const Formula &F) { - if (&F == True) { - OS << "True"; + if (&F == X) { + OS << "X"; return true; } - if (&F == False) { - OS << "False"; + if (&F == Y) { + OS << "Y"; return true; } return false; }; - auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom())); + 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, Delegate); diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h --- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h +++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h @@ -418,6 +418,11 @@ return &Formula::create(A, Formula::AtomRef, {}, NextAtom++); } + // Creates a reference to a literal boolean value. + const Formula *literal(bool B) { + return &Formula::create(A, Formula::Literal, {}, B); + } + // Creates a boolean conjunction value. const Formula *conj(const Formula *LeftSubVal, const Formula *RightSubVal) { return make(Formula::And, {LeftSubVal, RightSubVal}); 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 @@ -2853,14 +2853,14 @@ 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)); @@ -3038,7 +3038,7 @@ 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");