diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -340,6 +340,10 @@ llvm::DenseMap, DisjunctionValue *> DisjunctionVals; llvm::DenseMap NegationVals; + llvm::DenseMap, ImplicationValue *> + ImplicationVals; + llvm::DenseMap, BiconditionalValue *> + BiconditionalVals; // Flow conditions are tracked symbolically: each unique flow condition is // associated with a fresh symbolic variable (token), bound to the clause that diff --git a/clang/include/clang/Analysis/FlowSensitive/Value.h b/clang/include/clang/Analysis/FlowSensitive/Value.h --- a/clang/include/clang/Analysis/FlowSensitive/Value.h +++ b/clang/include/clang/Analysis/FlowSensitive/Value.h @@ -42,7 +42,9 @@ AtomicBool, Conjunction, Disjunction, - Negation + Negation, + Implication, + Biconditional, }; explicit Value(Kind ValKind) : ValKind(ValKind) {} @@ -84,7 +86,9 @@ return Val->getKind() == Kind::AtomicBool || Val->getKind() == Kind::Conjunction || Val->getKind() == Kind::Disjunction || - Val->getKind() == Kind::Negation; + Val->getKind() == Kind::Negation || + Val->getKind() == Kind::Implication || + Val->getKind() == Kind::Biconditional; } }; @@ -162,6 +166,54 @@ BoolValue &SubVal; }; +/// Models a boolean implication. +/// +/// Equivalent to `!LHS v RHS`. +class ImplicationValue : public BoolValue { +public: + explicit ImplicationValue(BoolValue &LeftSubVal, BoolValue &RightSubVal) + : BoolValue(Kind::Implication), LeftSubVal(LeftSubVal), + RightSubVal(RightSubVal) {} + + static bool classof(const Value *Val) { + return Val->getKind() == Kind::Implication; + } + + /// Returns the left sub-value of the implication. + BoolValue &getLeftSubValue() const { return LeftSubVal; } + + /// Returns the right sub-value of the implication. + BoolValue &getRightSubValue() const { return RightSubVal; } + +private: + BoolValue &LeftSubVal; + BoolValue &RightSubVal; +}; + +/// Models a boolean biconditional. +/// +/// Equivalent to `(LHS ^ RHS) v (!LHS ^ !RHS)`. +class BiconditionalValue : public BoolValue { +public: + explicit BiconditionalValue(BoolValue &LeftSubVal, BoolValue &RightSubVal) + : BoolValue(Kind::Biconditional), LeftSubVal(LeftSubVal), + RightSubVal(RightSubVal) {} + + static bool classof(const Value *Val) { + return Val->getKind() == Kind::Biconditional; + } + + /// Returns the left sub-value of the biconditional. + BoolValue &getLeftSubValue() const { return LeftSubVal; } + + /// Returns the right sub-value of the biconditional. + BoolValue &getRightSubValue() const { return RightSubVal; } + +private: + BoolValue &LeftSubVal; + BoolValue &RightSubVal; +}; + /// Models an integer. class IntegerValue : public Value { public: 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 @@ -113,16 +113,27 @@ BoolValue &DataflowAnalysisContext::getOrCreateImplication(BoolValue &LHS, BoolValue &RHS) { - return &LHS == &RHS ? getBoolLiteralValue(true) - : getOrCreateDisjunction(getOrCreateNegation(LHS), RHS); + if (&LHS == &RHS) + return getBoolLiteralValue(true); + + auto Res = ImplicationVals.try_emplace(std::make_pair(&LHS, &RHS), nullptr); + if (Res.second) + Res.first->second = + &takeOwnership(std::make_unique(LHS, RHS)); + return *Res.first->second; } BoolValue &DataflowAnalysisContext::getOrCreateIff(BoolValue &LHS, BoolValue &RHS) { - return &LHS == &RHS - ? getBoolLiteralValue(true) - : getOrCreateConjunction(getOrCreateImplication(LHS, RHS), - getOrCreateImplication(RHS, LHS)); + if (&LHS == &RHS) + return getBoolLiteralValue(true); + + auto Res = BiconditionalVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS), + nullptr); + if (Res.second) + Res.first->second = + &takeOwnership(std::make_unique(LHS, RHS)); + return *Res.first->second; } AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() { @@ -258,6 +269,24 @@ Result = &getOrCreateConjunction(LeftSub, RightSub); break; } + case Value::Kind::Implication: { + auto &IV = *cast(&Val); + auto &LeftSub = + substituteBoolValue(IV.getLeftSubValue(), SubstitutionsCache); + auto &RightSub = + substituteBoolValue(IV.getRightSubValue(), SubstitutionsCache); + Result = &getOrCreateImplication(LeftSub, RightSub); + break; + } + case Value::Kind::Biconditional: { + auto &BV = *cast(&Val); + auto &LeftSub = + substituteBoolValue(BV.getLeftSubValue(), SubstitutionsCache); + auto &RightSub = + substituteBoolValue(BV.getRightSubValue(), SubstitutionsCache); + Result = &getOrCreateIff(LeftSub, RightSub); + break; + } default: llvm_unreachable("Unhandled Value Kind"); } diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp --- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp +++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp @@ -96,6 +96,20 @@ S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1)); break; } + case Value::Kind::Implication: { + auto &IV = cast(B); + auto L = debugString(IV.getLeftSubValue(), Depth + 1); + auto R = debugString(IV.getRightSubValue(), Depth + 1); + S = formatv("(=>\n{0}\n{1})", L, R); + break; + } + case Value::Kind::Biconditional: { + auto &BV = cast(B); + auto L = debugString(BV.getLeftSubValue(), Depth + 1); + auto R = debugString(BV.getRightSubValue(), Depth + 1); + S = formatv("(=\n{0}\n{1})", L, R); + break; + } default: llvm_unreachable("Unhandled value 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 @@ -221,6 +221,18 @@ UnprocessedSubVals.push(&N->getSubVal()); break; } + case Value::Kind::Implication: { + auto *I = cast(Val); + UnprocessedSubVals.push(&I->getLeftSubValue()); + UnprocessedSubVals.push(&I->getRightSubValue()); + break; + } + case Value::Kind::Biconditional: { + auto *B = cast(Val); + UnprocessedSubVals.push(&B->getLeftSubValue()); + UnprocessedSubVals.push(&B->getRightSubValue()); + break; + } case Value::Kind::AtomicBool: { Atomics[Var] = cast(Val); break; @@ -298,6 +310,46 @@ // Visit the sub-values of `Val`. UnprocessedSubVals.push(&N->getSubVal()); + } else if (auto *I = dyn_cast(Val)) { + const Variable LeftSubVar = GetVar(&I->getLeftSubValue()); + const Variable RightSubVar = GetVar(&I->getRightSubValue()); + + // `X <=> (A => B)` is equivalent to + // `(X v A) ^ (X v !B) ^ (!X v !A v B)` which is already in + // conjunctive normal form. Below we add each of the conjuncts of the + // latter expression to the result. + Formula.addClause(posLit(Var), posLit(LeftSubVar)); + Formula.addClause(posLit(Var), negLit(RightSubVar)); + Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar)); + + // Visit the sub-values of `Val`. + UnprocessedSubVals.push(&I->getLeftSubValue()); + UnprocessedSubVals.push(&I->getRightSubValue()); + } else if (auto *B = dyn_cast(Val)) { + const Variable LeftSubVar = GetVar(&B->getLeftSubValue()); + const Variable RightSubVar = GetVar(&B->getRightSubValue()); + + if (LeftSubVar == RightSubVar) { + // `X <=> (A <=> A)` is equvalent to `X` which is already in + // conjunctive normal form. Below we add each of the conjuncts of the + // latter expression to the result. + Formula.addClause(posLit(Var)); + + // No need to visit the sub-values of `Val`. + } else { + // `X <=> (A <=> B)` is equivalent to + // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which is + // already in conjunctive normal form. Below we add each of the conjuncts + // of the latter expression to the result. + Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar)); + Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar)); + Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar)); + Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar)); + + // Visit the sub-values of `Val`. + UnprocessedSubVals.push(&B->getLeftSubValue()); + UnprocessedSubVals.push(&B->getRightSubValue()); + } } } diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp --- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp @@ -304,7 +304,7 @@ } #endif -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsAtomicFC) { +TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingAtomic) { auto &X = Context.createAtomicBoolValue(); auto &True = Context.getBoolLiteralValue(true); auto &False = Context.getBoolLiteralValue(false); @@ -324,7 +324,7 @@ EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, False)); } -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsNegatedFC) { +TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingNegation) { auto &X = Context.createAtomicBoolValue(); auto &True = Context.getBoolLiteralValue(true); auto &False = Context.getBoolLiteralValue(false); @@ -333,18 +333,18 @@ auto &FC = Context.makeFlowConditionToken(); Context.addFlowConditionConstraint(FC, Context.getOrCreateNegation(X)); - // If X is true in FC, FC = !X must be false + // If X is true, FC is false auto &FCWithXTrue = Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}}); EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, False)); - // If X is false in FC, FC = !X must be true + // If X is false, FC is true auto &FC1WithXFalse = Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}}); EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True)); } -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsDisjunctiveFC) { +TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingDisjunction) { auto &X = Context.createAtomicBoolValue(); auto &Y = Context.createAtomicBoolValue(); auto &True = Context.getBoolLiteralValue(true); @@ -354,18 +354,18 @@ auto &FC = Context.makeFlowConditionToken(); Context.addFlowConditionConstraint(FC, Context.getOrCreateDisjunction(X, Y)); - // If X is true in FC, FC = X || Y must be true + // If X is true, FC must be true auto &FCWithXTrue = Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}}); EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True)); - // If X is false in FC, FC = X || Y is equivalent to evaluating Y + // If X is false, FC is equivalent to Y auto &FC1WithXFalse = Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}}); EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, Y)); } -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsConjunctiveFC) { +TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingConjunction) { auto &X = Context.createAtomicBoolValue(); auto &Y = Context.createAtomicBoolValue(); auto &True = Context.getBoolLiteralValue(true); @@ -375,17 +375,82 @@ auto &FC = Context.makeFlowConditionToken(); Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y)); - // If X is true in FC, FC = X && Y is equivalent to evaluating Y + // If X is true, FC is equivalent to Y auto &FCWithXTrue = Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}}); EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y)); - // If X is false in FC, FC = X && Y must be false + // If X is false, FC is false auto &FCWithXFalse = Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}}); EXPECT_TRUE(Context.equivalentBoolValues(FCWithXFalse, False)); } +TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingImplication) { + auto &X = Context.createAtomicBoolValue(); + auto &Y = Context.createAtomicBoolValue(); + auto &True = Context.getBoolLiteralValue(true); + auto &False = Context.getBoolLiteralValue(false); + + // FC = (X => Y) + auto &FC = Context.makeFlowConditionToken(); + Context.addFlowConditionConstraint(FC, Context.getOrCreateImplication(X, Y)); + + // If X is true, FC is equivalent to Y + auto &FCWithXTrue = + Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}}); + EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y)); + + // If X is false, FC is true + auto &FC1WithXFalse = + Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}}); + EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True)); + + // If Y is true, FC is true + auto &FCWithYTrue = + Context.buildAndSubstituteFlowCondition(FC, {{&Y, &True}}); + EXPECT_TRUE(Context.equivalentBoolValues(FCWithYTrue, True)); + + // If Y is false, FC is equivalent to !X + auto &FCWithYFalse = + Context.buildAndSubstituteFlowCondition(FC, {{&Y, &False}}); + EXPECT_TRUE(Context.equivalentBoolValues(FCWithYFalse, + Context.getOrCreateNegation(X))); +} + +TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingBiconditional) { + auto &X = Context.createAtomicBoolValue(); + auto &Y = Context.createAtomicBoolValue(); + auto &True = Context.getBoolLiteralValue(true); + auto &False = Context.getBoolLiteralValue(false); + + // FC = (X <=> Y) + auto &FC = Context.makeFlowConditionToken(); + Context.addFlowConditionConstraint(FC, Context.getOrCreateIff(X, Y)); + + // If X is true, FC is equivalent to Y + auto &FCWithXTrue = + Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}}); + EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y)); + + // If X is false, FC is equivalent to !Y + auto &FC1WithXFalse = + Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}}); + EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, + Context.getOrCreateNegation(Y))); + + // If Y is true, FC is equivalent to X + auto &FCWithYTrue = + Context.buildAndSubstituteFlowCondition(FC, {{&Y, &True}}); + EXPECT_TRUE(Context.equivalentBoolValues(FCWithYTrue, X)); + + // If Y is false, FC is equivalent to !X + auto &FCWithYFalse = + Context.buildAndSubstituteFlowCondition(FC, {{&Y, &False}}); + EXPECT_TRUE(Context.equivalentBoolValues(FCWithYFalse, + Context.getOrCreateNegation(X))); +} + TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsForkedFC) { auto &X = Context.createAtomicBoolValue(); auto &Y = Context.createAtomicBoolValue(); 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 @@ -64,33 +64,24 @@ } TEST(BoolValueDebugStringTest, Implication) { - // B0 => B1, implemented as !B0 v B1 + // B0 => B1 ConstraintContext Ctx; - auto B = Ctx.disj(Ctx.neg(Ctx.atom()), Ctx.atom()); + auto B = Ctx.impl(Ctx.atom(), Ctx.atom()); - auto Expected = R"((or - (not - B0) + auto Expected = R"((=> + B0 B1))"; EXPECT_THAT(debugString(*B), StrEq(Expected)); } TEST(BoolValueDebugStringTest, Iff) { - // B0 <=> B1, implemented as (!B0 v B1) ^ (B0 v !B1) + // B0 <=> B1 ConstraintContext Ctx; - auto B0 = Ctx.atom(); - auto B1 = Ctx.atom(); - auto B = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1))); + auto B = Ctx.iff(Ctx.atom(), Ctx.atom()); - auto Expected = R"((and - (or - (not - B0) - B1) - (or - B0 - (not - B1))))"; + auto Expected = R"((= + B0 + B1))"; EXPECT_THAT(debugString(*B), StrEq(Expected)); } diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp --- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp @@ -188,6 +188,19 @@ expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY})); } +TEST(SolverTest, IffIsEquivalentToDNF) { + ConstraintContext Ctx; + auto X = Ctx.atom(); + auto Y = Ctx.atom(); + auto NotX = Ctx.neg(X); + auto NotY = Ctx.neg(Y); + auto XIffY = Ctx.iff(X, Y); + auto XIffYDNF = Ctx.disj(Ctx.conj(X, Y), Ctx.conj(NotX, NotY)); + auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF)); + + expectUnsatisfiable(solve({NotEquivalent})); +} + TEST(SolverTest, IffSameVars) { ConstraintContext Ctx; auto X = Ctx.atom(); @@ -279,6 +292,17 @@ expectUnsatisfiable(solve({XEqY, X, NotY})); } +TEST(SolverTest, ImplicationIsEquivalentToDNF) { + ConstraintContext Ctx; + auto X = Ctx.atom(); + auto Y = Ctx.atom(); + auto XImpliesY = Ctx.impl(X, Y); + auto XImpliesYDNF = Ctx.disj(Ctx.neg(X), Y); + auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF)); + + expectUnsatisfiable(solve({NotEquivalent})); +} + TEST(SolverTest, ImplicationConflict) { ConstraintContext Ctx; auto X = Ctx.atom(); 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 @@ -251,12 +251,16 @@ // Creates a boolean implication value. BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) { - return disj(neg(LeftSubVal), RightSubVal); + Vals.push_back( + std::make_unique(*LeftSubVal, *RightSubVal)); + return Vals.back().get(); } // Creates a boolean biconditional value. BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) { - return conj(impl(LeftSubVal, RightSubVal), impl(RightSubVal, LeftSubVal)); + Vals.push_back( + std::make_unique(*LeftSubVal, *RightSubVal)); + return Vals.back().get(); } private: