[PATCH] D153476: [dataflow] document & test determinism of formula structure

[Sam McCall via Phabricator via cfe-commits]

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();
+  auto &AY = A.create();
+  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();
+  auto &BY = B.create();
+  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
 makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
   auto Res = std::make_pair(&LHS, &RHS);


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();
+  auto &AY = A.create();
+  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();
+  auto &BY = B.create();
+  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
 makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
   auto Res = std::make_pair(&LHS, &RHS);
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153476: [dataflow] document & test determinism of formula structure

[Sam McCall via Phabricator via cfe-commits]

sammccall added inline comments.



Comment at: clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp:169
+  auto &BOr = A.makeOr(BY, BX);
+  auto &BEqual = A.makeEquals(BOr, BAnd);
+  EXPECT_EQ(Expected, llvm::to_string(B.getFormula(BEqual)));

gribozavr2 wrote:
> gribozavr2 wrote:
> > Shouldn't these lines use "A.make...()"?
> Sorry, I meant, shouldn't these lines use "B.make...()"?
oops, good catch!

(this was the test I expected to fail, which convinced me the code being tested 
was correct. so a bit ironic that the test was wrong and would have passed 
either way...)


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D153476/new/

https://reviews.llvm.org/D153476

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153476: [dataflow] document & test determinism of formula structure

[Sam McCall via Phabricator via cfe-commits]

sammccall updated this revision to Diff 534107.
sammccall marked 3 inline comments as done.
sammccall added a comment.

fix busted test


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();
+  auto &AY = A.create();
+  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();
+  auto &BY = B.create();
+  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 poir 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
 makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
   auto Res = std::make_pair(&LHS, &RHS);


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();
+  auto &AY = A.create();
+  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();
+  auto &BY = B.create();
+  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 poir 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
 makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
   auto Res = std::make_pair(&LHS, &RHS);
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153476: [dataflow] document & test determinism of formula structure

[Dmitri Gribenko via Phabricator via cfe-commits]

gribozavr2 added inline comments.



Comment at: clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp:165-169
+  auto &BX = A.create();
+  auto &BY = A.create();
+  auto &BAnd = A.makeAnd(BX, BY);
+  auto &BOr = A.makeOr(BY, BX);
+  auto &BEqual = A.makeEquals(BOr, BAnd);





Comment at: clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp:169
+  auto &BOr = A.makeOr(BY, BX);
+  auto &BEqual = A.makeEquals(BOr, BAnd);
+  EXPECT_EQ(Expected, llvm::to_string(B.getFormula(BEqual)));

gribozavr2 wrote:
> Shouldn't these lines use "A.make...()"?
Sorry, I meant, shouldn't these lines use "B.make...()"?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D153476/new/

https://reviews.llvm.org/D153476

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153476: [dataflow] document & test determinism of formula structure

[Dmitri Gribenko via Phabricator via cfe-commits]

gribozavr2 added inline comments.



Comment at: clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp:169
+  auto &BOr = A.makeOr(BY, BX);
+  auto &BEqual = A.makeEquals(BOr, BAnd);
+  EXPECT_EQ(Expected, llvm::to_string(B.getFormula(BEqual)));

Shouldn't these lines use "A.make...()"?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D153476/new/

https://reviews.llvm.org/D153476

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153476: [dataflow] document & test determinism of formula structure

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun accepted this revision.
xazax.hun added inline comments.
This revision is now accepted and ready to land.



Comment at: clang/lib/Analysis/FlowSensitive/Arena.cpp:13
 
+// Compute a canonical key for an unordered poir of operands, so that we
+// can intern (A & B) and (B & A) to the same formula.




Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D153476/new/

https://reviews.llvm.org/D153476

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153476: [dataflow] document & test determinism of formula structure

[Sam McCall via Phabricator via cfe-commits]

sammccall created this revision.
Herald added subscribers: martong, mgrang, xazax.hun.
Herald added a reviewer: NoQ.
Herald added a project: All.
sammccall requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

This doesn't depend on object addresses, even though they are used
in canonicalization. This is important & subtle, so add a comment+test.


Repository:
  rG LLVM Github Monorepo

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();
+  auto &AY = A.create();
+  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 = A.create();
+  auto &BY = A.create();
+  auto &BAnd = A.makeAnd(BX, BY);
+  auto &BOr = A.makeOr(BY, BX);
+  auto &BEqual = A.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 poir 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
 makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
   auto Res = std::make_pair(&LHS, &RHS);


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();
+  auto &AY = A.create();
+  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 = A.create();
+  auto &BY = A.create();
+  auto &BAnd = A.makeAnd(BX, BY);
+  auto &BOr = A.makeOr(BY, BX);
+  auto &BEqual = A.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 poir 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
 makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
   auto Res = std::make_pair(&LHS, &RHS);
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits