[clang] b5e3dac - [clang][dataflow] Add explicit "AST" nodes for implications and iff
Dmitri Gribenko via cfe-commits
cfe-commits at lists.llvm.org
Tue Jul 26 05:19:28 PDT 2022
Author: Dmitri Gribenko
Date: 2022-07-26T14:19:22+02:00
New Revision: b5e3dac33d42cdf8a3b19b1f64b726e700363ded
URL: https://github.com/llvm/llvm-project/commit/b5e3dac33d42cdf8a3b19b1f64b726e700363ded
DIFF: https://github.com/llvm/llvm-project/commit/b5e3dac33d42cdf8a3b19b1f64b726e700363ded.diff
LOG: [clang][dataflow] Add explicit "AST" nodes for implications and iff
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.
Reviewed By: sgatev, xazax.hun, wyt
Differential Revision: https://reviews.llvm.org/D130519
Added:
Modified:
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
Removed:
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index abc3183e1b0b5..b3e725ad3f6a5 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -340,6 +340,10 @@ class DataflowAnalysisContext {
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
diff --git a/clang/include/clang/Analysis/FlowSensitive/Value.h b/clang/include/clang/Analysis/FlowSensitive/Value.h
index 70348f8745431..c63799fe6a464 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Value.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Value.h
@@ -37,12 +37,13 @@ class Value {
Pointer,
Struct,
- // Synthetic boolean values are either atomic values or composites that
- // represent conjunctions, disjunctions, and negations.
+ // Synthetic boolean values are either atomic values or logical connectives.
AtomicBool,
Conjunction,
Disjunction,
- Negation
+ Negation,
+ Implication,
+ Biconditional,
};
explicit Value(Kind ValKind) : ValKind(ValKind) {}
@@ -84,7 +85,9 @@ class BoolValue : public Value {
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 +165,54 @@ class NegationValue : public BoolValue {
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
index 8f2296dc7e2cc..216f41bdee1cf 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -113,16 +113,27 @@ BoolValue &DataflowAnalysisContext::getOrCreateNegation(BoolValue &Val) {
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 @@ BoolValue &DataflowAnalysisContext::substituteBoolValue(
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");
}
diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
index 309ff0682f50d..714ad08643edb 100644
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -96,6 +96,20 @@ class DebugStringGenerator {
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");
}
diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
index b081543ac1333..cd1fd708a43aa 100644
--- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -221,6 +221,18 @@ BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) {
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;
@@ -320,6 +332,46 @@ BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) {
// 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());
+ }
}
}
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
index 758b1a8b21a2b..926e871a8ee2a 100644
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -304,7 +304,7 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsFalseUnchanged) {
}
#endif
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsAtomicFC) {
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingAtomic) {
auto &X = Context.createAtomicBoolValue();
auto &True = Context.getBoolLiteralValue(true);
auto &False = Context.getBoolLiteralValue(false);
@@ -313,18 +313,18 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsAtomicFC) {
auto &FC = Context.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC, X);
- // If X is true in FC, FC = X must be true
+ // If X is true, FC is true
auto &FCWithXTrue =
Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
- // If X is false in FC, FC = X must be false
+ // If X is false, FC is false
auto &FC1WithXFalse =
Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
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 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsNegatedFC) {
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 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsDisjunctiveFC) {
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 is 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 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsConjunctiveFC) {
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();
@@ -410,7 +475,7 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsForkedFC) {
ForkedFC, {{&Y, &True}, {&Z, &True}});
EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYAndZTrue, X));
- // If any of X,Y,Z is false in ForkedFC, ForkedFC = X && Y && Z must be false
+ // If any of X,Y,Z is false, ForkedFC is false
auto &ForkedFCWithXFalse =
Context.buildAndSubstituteFlowCondition(ForkedFC, {{&X, &False}});
auto &ForkedFCWithYFalse =
@@ -439,8 +504,7 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
auto &JoinedFC = Context.joinFlowConditions(FC1, FC2);
Context.addFlowConditionConstraint(JoinedFC, Z);
- // If any of X, Y is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
- // to evaluating the remaining Z
+ // If any of X, Y is true, JoinedFC is equivalent to Z
auto &JoinedFCWithXTrue =
Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &True}});
auto &JoinedFCWithYTrue =
@@ -448,15 +512,14 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithXTrue, Z));
EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithYTrue, Z));
- // If Z is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent to
- // evaluating the remaining disjunction (X || Y)
+ // If Z is true, JoinedFC is equivalent to (X || Y)
auto &JoinedFCWithZTrue =
Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &True}});
EXPECT_TRUE(Context.equivalentBoolValues(
JoinedFCWithZTrue, Context.getOrCreateDisjunction(X, Y)));
- // If any of X, Y is false in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
- // to evaluating the conjunction of the other value and Z
+ // If any of X, Y is false, JoinedFC is equivalent to the conjunction of the
+ // other value and Z
auto &JoinedFCWithXFalse =
Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &False}});
auto &JoinedFCWithYFalse =
@@ -466,7 +529,7 @@ TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
EXPECT_TRUE(Context.equivalentBoolValues(
JoinedFCWithYFalse, Context.getOrCreateConjunction(X, Z)));
- // If Z is false in JoinedFC, JoinedFC = (X || Y) && Z must be false
+ // If Z is false, JoinedFC is false
auto &JoinedFCWithZFalse =
Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &False}});
EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithZFalse, False));
diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
index 6b9321babfa64..6dded4b267026 100644
--- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -64,33 +64,24 @@ TEST(BoolValueDebugStringTest, Disjunction) {
}
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
index 0c50c19a1559a..1de1c3a22e488 100644
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -206,6 +206,20 @@ TEST(SolverTest, DeepConflict) {
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));
+
+ // !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
+ expectUnsatisfiable(solve({NotEquivalent}));
+}
+
TEST(SolverTest, IffSameVars) {
ConstraintContext Ctx;
auto X = Ctx.atom();
@@ -297,6 +311,18 @@ TEST(SolverTest, RespectsAdditionalConstraints) {
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));
+
+ // !((X => Y) <=> (!X v Y))
+ 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
index debff04a3c068..8cb500853608b 100644
--- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -251,12 +251,16 @@ class ConstraintContext {
// 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:
More information about the cfe-commits
mailing list