[clang][dataflow] Add an early-out to flowConditionImplies() / flowConditionAllows(). (#78172)

This saves having to assemble the set of constraints and run the SAT
solver in
the trivial case of `flowConditionImplies(true)` or
`flowConditionAllows(false)`.

This is an update / reland of my previous reverted
[#77453](#77453). That PR
contained a
logic bug -- the early-out for `flowConditionAllows()` was wrong because
my
intuition about the logic was wrong. (In particular, note that
`flowConditionImplies(F)` does not imply `flowConditionAllows(F)`, even
though
this may run counter to intuition.)

I've now done what I should have done on the first iteration and added
more
tests. These pass both with and without my early-outs.

This patch is a performance win on the benchmarks for the Crubit
nullability
checker, except for one slight regression on a relatively short
benchmark:

```
name                              old cpu/op   new cpu/op   delta
BM_PointerAnalysisCopyPointer     68.5µs ± 7%  67.6µs ± 4%    ~     (p=0.159 n=18+19)
BM_PointerAnalysisIntLoop          173µs ± 3%   162µs ± 4%  -6.40%  (p=0.000 n=19+20)
BM_PointerAnalysisPointerLoop      307µs ± 2%   312µs ± 4%  +1.56%  (p=0.013 n=18+20)
BM_PointerAnalysisBranch           199µs ± 4%   181µs ± 4%  -8.81%  (p=0.000 n=20+20)
BM_PointerAnalysisLoopAndBranch    503µs ± 3%   508µs ± 2%    ~     (p=0.081 n=18+19)
BM_PointerAnalysisTwoLoops         304µs ± 4%   286µs ± 2%  -6.04%  (p=0.000 n=19+20)
BM_PointerAnalysisJoinFilePath    4.78ms ± 3%  4.54ms ± 4%  -4.97%  (p=0.000 n=20+20)
BM_PointerAnalysisCallInLoop      3.05ms ± 3%  2.90ms ± 4%  -5.05%  (p=0.000 n=19+20)
```

When running clang-tidy on real-world code, the results are less clear.
In
three runs, averaged, on an arbitrarily chosen input file, I get 11.60 s
of user
time without this patch and 11.40 s with it, though with considerable
measurement noise (I'm seeing up to 0.2 s of variation between runs).

Still, this is a very simple change, and it is a clear win in
benchmarks, so I
think it is worth making.

Author: martinboehme

clang/include/clang/Analysis/FlowSensitive/Formula.h

@@ -75,6 +75,10 @@ class alignas(const Formula *) Formula {
     return static_cast<bool>(Value);
   }
 
+  bool isLiteral(bool b) const {
+    return kind() == Literal && static_cast<bool>(Value) == b;
+  }
+
   ArrayRef<const Formula *> operands() const {
     return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
                     numOperands(kind()));

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

@@ -174,6 +174,9 @@ Solver::Result DataflowAnalysisContext::querySolver(
 
 bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
                                                    const Formula &F) {
+  if (F.isLiteral(true))
+    return true;
+
   // Returns true if and only if truth assignment of the flow condition implies
   // that `F` is also true. We prove whether or not this property holds by
   // reducing the problem to satisfiability checking. In other words, we attempt
@@ -188,6 +191,9 @@ bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
 
 bool DataflowAnalysisContext::flowConditionAllows(Atom Token,
                                                   const Formula &F) {
+  if (F.isLiteral(false))
+    return false;
+
   llvm::SetVector<const Formula *> Constraints;
   Constraints.insert(&arena().makeAtomRef(Token));
   Constraints.insert(&F);

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

@@ -33,10 +33,34 @@ TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) {
   EXPECT_FALSE(Context.equivalentFormulas(X.formula(), Y.formula()));
 }
 
-TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) {
+TEST_F(DataflowAnalysisContextTest, TautologicalFlowConditionImplies) {
   Atom FC = A.makeFlowConditionToken();
-  auto &C = A.makeAtomRef(A.makeAtom());
-  EXPECT_FALSE(Context.flowConditionImplies(FC, C));
+  EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(true)));
+  EXPECT_FALSE(Context.flowConditionImplies(FC, A.makeLiteral(false)));
+  EXPECT_FALSE(Context.flowConditionImplies(FC, A.makeAtomRef(A.makeAtom())));
+}
+
+TEST_F(DataflowAnalysisContextTest, TautologicalFlowConditionAllows) {
+  Atom FC = A.makeFlowConditionToken();
+  EXPECT_TRUE(Context.flowConditionAllows(FC, A.makeLiteral(true)));
+  EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(false)));
+  EXPECT_TRUE(Context.flowConditionAllows(FC, A.makeAtomRef(A.makeAtom())));
+}
+
+TEST_F(DataflowAnalysisContextTest, ContradictoryFlowConditionImpliesAnything) {
+  Atom FC = A.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC, A.makeLiteral(false));
+  EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(true)));
+  EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(false)));
+  EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeAtomRef(A.makeAtom())));
+}
+
+TEST_F(DataflowAnalysisContextTest, ContradictoryFlowConditionAllowsNothing) {
+  Atom FC = A.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC, A.makeLiteral(false));
+  EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(true)));
+  EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(false)));
+  EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeAtomRef(A.makeAtom())));
 }
 
 TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) {