[PATCH] D153476: [dataflow] document & test determinism of formula structure
Sam McCall via Phabricator via cfe-commits
cfe-commits at lists.llvm.org
Fri Jun 23 16:32:14 PDT 2023
sammccall updated this revision to Diff 534120.
sammccall marked an inline comment as done.
sammccall added a comment.
typo fix
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D153476/new/
https://reviews.llvm.org/D153476
Files:
clang/lib/Analysis/FlowSensitive/Arena.cpp
clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
@@ -147,5 +147,28 @@
EXPECT_EQ(&Formula1, &Formula2);
}
+// Tests that the structure of the formula we end up with does not depend on
+// details like the pointer address of internal values.
+TEST_F(ArenaTest, Canonicalization) {
+ StringRef Expected = "((V0 | V1) = (V1 & V0))";
+
+ auto &AX = A.create<AtomicBoolValue>();
+ auto &AY = A.create<AtomicBoolValue>();
+ auto &AOr = A.makeOr(AX, AY);
+ auto &AAnd = A.makeAnd(AY, AX);
+ auto &AEqual = A.makeEquals(AOr, AAnd);
+ EXPECT_EQ(Expected, llvm::to_string(A.getFormula(AEqual)));
+
+ // Same, but create the & clause first.
+ // The relative order of (&AOr, &AAnd) and (&BOr, &BAnd) likely differs.
+ Arena B;
+ auto &BX = B.create<AtomicBoolValue>();
+ auto &BY = B.create<AtomicBoolValue>();
+ auto &BAnd = B.makeAnd(BX, BY);
+ auto &BOr = B.makeOr(BY, BX);
+ auto &BEqual = B.makeEquals(BOr, BAnd);
+ EXPECT_EQ(Expected, llvm::to_string(B.getFormula(BEqual)));
+}
+
} // namespace
} // namespace clang::dataflow
Index: clang/lib/Analysis/FlowSensitive/Arena.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -10,6 +10,10 @@
namespace clang::dataflow {
+// Compute a canonical key for an unordered pair of operands, so that we
+// can intern (A & B) and (B & A) to the same formula.
+// This does not affect the actual order used in the formula, which is always
+// that of the first call to makeAnd().
static std::pair<BoolValue *, BoolValue *>
makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
auto Res = std::make_pair(&LHS, &RHS);
-------------- next part --------------
A non-text attachment was scrubbed...
Name: D153476.534120.patch
Type: text/x-patch
Size: 1899 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20230623/31d33986/attachment.bin>
More information about the cfe-commits
mailing list