wyt updated this revision to Diff 439762.
wyt added a comment.
Rename createIff to getOrCreateIff based on change in parent patch.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D128521/new/
https://reviews.llvm.org/D128521
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -213,4 +213,67 @@
EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
}
+TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &Y = Context.createAtomicBoolValue();
+ auto &Z = Context.createAtomicBoolValue();
+ auto &True = Context.getBoolLiteralValue(true);
+ auto &False = Context.getBoolLiteralValue(false);
+
+ // X == X
+ EXPECT_TRUE(Context.equivalentBoolValues(X, X));
+ // X != Y
+ EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
+
+ // !X != X
+ EXPECT_FALSE(Context.equivalentBoolValues(Context.getOrCreateNegation(X), X));
+ // !(!X) = X
+ EXPECT_TRUE(Context.equivalentBoolValues(
+ Context.getOrCreateNegation(Context.getOrCreateNegation(X)), X));
+
+ // (X || X) == X
+ EXPECT_TRUE(
+ Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, X), X));
+ // (X || Y) != X
+ EXPECT_FALSE(
+ Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y), X));
+ // (X || True) == True
+ EXPECT_TRUE(Context.equivalentBoolValues(
+ Context.getOrCreateDisjunction(X, True), True));
+ // (X || False) == X
+ EXPECT_TRUE(Context.equivalentBoolValues(
+ Context.getOrCreateDisjunction(X, False), X));
+
+ // (X && X) == X
+ EXPECT_TRUE(
+ Context.equivalentBoolValues(Context.getOrCreateConjunction(X, X), X));
+ // (X && Y) != X
+ EXPECT_FALSE(
+ Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y), X));
+ // (X && True) == X
+ EXPECT_TRUE(
+ Context.equivalentBoolValues(Context.getOrCreateConjunction(X, True), X));
+ // (X && False) == False
+ EXPECT_TRUE(Context.equivalentBoolValues(
+ Context.getOrCreateConjunction(X, False), False));
+
+ // (X || Y) == (Y || X)
+ EXPECT_TRUE(
+ Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y),
+ Context.getOrCreateDisjunction(Y, X)));
+ // (X && Y) == (Y && X)
+ EXPECT_TRUE(
+ Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y),
+ Context.getOrCreateConjunction(Y, X)));
+
+ // ((X || Y) || Z) == (X || (Y || Z))
+ EXPECT_TRUE(Context.equivalentBoolValues(
+ Context.getOrCreateDisjunction(Context.getOrCreateDisjunction(X, Y), Z),
+ Context.getOrCreateDisjunction(X, Context.getOrCreateDisjunction(Y, Z))));
+ // ((X && Y) && Z) == (X && (Y && Z))
+ EXPECT_TRUE(Context.equivalentBoolValues(
+ Context.getOrCreateConjunction(Context.getOrCreateConjunction(X, Y), Z),
+ Context.getOrCreateConjunction(X, Context.getOrCreateConjunction(Y, Z))));
+}
+
} // namespace
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -137,6 +137,13 @@
return checkUnsatisfiable(std::move(Constraints));
}
+bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
+ BoolValue &Val2) {
+ llvm::DenseSet<BoolValue *> Constraints = {
+ &getOrCreateNegation(getOrCreateIff(Val1, Val2))};
+ return checkUnsatisfiable(Constraints);
+}
+
void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -203,6 +203,11 @@
/// identified by `Token` are always true.
bool flowConditionIsTautology(AtomicBoolValue &Token);
+ /// Returns true if `Val1` is equivalent to `Val2`.
+ /// Note: This function doesn't take into account constraints on `Val1` and
+ /// `Val2` imposed by the flow condition.
+ bool equivalentBoolValues(BoolValue &Val1, BoolValue &Val2);
+
private:
/// Adds all constraints of the flow condition identified by `Token` and all
/// of its transitive dependencies to `Constraints`. `VisitedTokens` is used
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
