gribozavr created this revision.
Herald added subscribers: martong, tschuett, xazax.hun.
Herald added a reviewer: NoQ.
Herald added a project: All.
gribozavr requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
Previously we used to desugar implications and biconditionals into
equivalent CNF/DNF as soon as possible. However, this desugaring makes
debug output (Environment::dump()) less readable than it could be.
Therefore, it makes sense to keep the sugared representation of a
boolean formula, and desugar it in the solver.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D130519
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
Index: clang/unittests/Analysis/FlowSensitive/TestingSupport.h
===================================================================
--- clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ 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<ImplicationValue>(*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<BiconditionalValue>(*LeftSubVal, *RightSubVal));
+ return Vals.back().get();
}
private:
Index: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ 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();
Index: clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ 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));
}
Index: clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ 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();
Index: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -221,6 +221,18 @@
UnprocessedSubVals.push(&N->getSubVal());
break;
}
+ case Value::Kind::Implication: {
+ auto *I = cast<ImplicationValue>(Val);
+ UnprocessedSubVals.push(&I->getLeftSubValue());
+ UnprocessedSubVals.push(&I->getRightSubValue());
+ break;
+ }
+ case Value::Kind::Biconditional: {
+ auto *B = cast<BiconditionalValue>(Val);
+ UnprocessedSubVals.push(&B->getLeftSubValue());
+ UnprocessedSubVals.push(&B->getRightSubValue());
+ break;
+ }
case Value::Kind::AtomicBool: {
Atomics[Var] = cast<AtomicBoolValue>(Val);
break;
@@ -298,6 +310,46 @@
// Visit the sub-values of `Val`.
UnprocessedSubVals.push(&N->getSubVal());
+ } else if (auto *I = dyn_cast<ImplicationValue>(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<BiconditionalValue>(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());
+ }
}
}
Index: clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ 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<ImplicationValue>(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<BiconditionalValue>(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");
}
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ 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<ImplicationValue>(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<BiconditionalValue>(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<ImplicationValue>(&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<BiconditionalValue>(&Val);
+ auto &LeftSub =
+ substituteBoolValue(BV.getLeftSubValue(), SubstitutionsCache);
+ auto &RightSub =
+ substituteBoolValue(BV.getRightSubValue(), SubstitutionsCache);
+ Result = &getOrCreateIff(LeftSub, RightSub);
+ break;
+ }
default:
llvm_unreachable("Unhandled Value Kind");
}
Index: clang/include/clang/Analysis/FlowSensitive/Value.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/Value.h
+++ 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:
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -340,6 +340,10 @@
llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
DisjunctionVals;
llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
+ llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ImplicationValue *>
+ ImplicationVals;
+ llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
+ BiconditionalVals;
// Flow conditions are tracked symbolically: each unique flow condition is
// associated with a fresh symbolic variable (token), bound to the clause that
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
