[dataflow] document & test determinism of formula structure

[sammccall]

Summary

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

[xazax.hun]

clang/lib/Analysis/FlowSensitive/Arena.cpp

13

[gribozavr2]

clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp

165–169

169

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

169

Sorry, I meant, shouldn't these lines use "B.make...()"?

[sammccall]

fix busted test

[sammccall]

clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp

169

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...)

[sammccall]

typo fix

clang/lib/Analysis/FlowSensitive/Arena.cpp

 //===-- Arena.cpp ---------------------------------------------------------===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 
 #include "clang/Analysis/FlowSensitive/Arena.h"
 
 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);
   if (&RHS < &LHS)
     std::swap(Res.first, Res.second);
   return Res;
 }
 

clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp

TEST_F(ArenaTest, ValueToFormulaCached) {
   auto &Y = A.create<AtomicBoolValue>();
   auto &XIffY = A.makeEquals(X, Y);
 
   auto &Formula1 = A.getFormula(XIffY);
   auto &Formula2 = A.getFormula(XIffY);
   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