[clang][dataflow] Move logic for creating implication and iff expressions into `DataflowAnalysisContext` from `DataflowEnvironment`.

[wyt]

Summary

To keep functionality of creating boolean expressions in a consistent location.

Depends On D128357

[sgatev]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

170

Let's call it getOrCreateImplication similar to the members above. Same for iff below.

170

Let's add tests for the new members, possibly moving existing tests from DataflowEnvironmentTest.cpp to DataflowAnalysisContextTest.cpp.

[wyt]

Address comments - rename createIff/Implication to getOrCreateIff/Implication and add tests for these functions

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

public:
   AtomicBoolValue &createAtomicBoolValue() {
     return takeOwnership(std::make_unique<AtomicBoolValue>());
   }
 
   /// Returns a boolean value that represents the conjunction of `LHS` and
   /// `RHS`. Subsequent calls with the same arguments, regardless of their
   /// order, will return the same result. If the given boolean values represent
   /// the same value, the result will be the value itself.
-  BoolValue &getOrCreateConjunctionValue(BoolValue &LHS, BoolValue &RHS);
+  BoolValue &getOrCreateConjunction(BoolValue &LHS, BoolValue &RHS);
 
   /// Returns a boolean value that represents the disjunction of `LHS` and
   /// `RHS`. Subsequent calls with the same arguments, regardless of their
   /// order, will return the same result. If the given boolean values represent
   /// the same value, the result will be the value itself.
-  BoolValue &getOrCreateDisjunctionValue(BoolValue &LHS, BoolValue &RHS);
+  BoolValue &getOrCreateDisjunction(BoolValue &LHS, BoolValue &RHS);
 
   /// Returns a boolean value that represents the negation of `Val`. Subsequent
   /// calls with the same argument will return the same result.
-  BoolValue &getOrCreateNegationValue(BoolValue &Val);
+  BoolValue &getOrCreateNegation(BoolValue &Val);
+
+  /// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with
+  /// the same arguments, regardless of their order, will return the same
+  /// result. If the given boolean values represent the same value, the result
+  /// will be a value that represents the true boolean literal.
+  BoolValue &createImplication(BoolValue &LHS, BoolValue &RHS);
+
+  /// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with
+  /// the same arguments, regardless of their order, will return the same
+  /// result. If the given boolean values represent the same value, the result
+  /// will be a value that represents the true boolean literal.
+  BoolValue &createIff(BoolValue &LHS, BoolValue &RHS);
 
   /// Creates a fresh flow condition and returns a token that identifies it. The
   /// token can be used to perform various operations on the flow condition such
   /// as adding constraints to it, forking it, joining it with another flow
   /// condition, or checking implications.
   AtomicBoolValue &makeFlowConditionToken();
 
   /// Adds `Constraint` to the flow condition identified by `Token`.

clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h

BoolValue &makeAtomicBoolValue() const {
     return DACtx->createAtomicBoolValue();
   }
 
   /// Returns a boolean value that represents the conjunction of `LHS` and
   /// `RHS`. Subsequent calls with the same arguments, regardless of their
   /// order, will return the same result. If the given boolean values represent
   /// the same value, the result will be the value itself.
   BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) const {
-    return DACtx->getOrCreateConjunctionValue(LHS, RHS);
+    return DACtx->getOrCreateConjunction(LHS, RHS);
   }
 
   /// Returns a boolean value that represents the disjunction of `LHS` and
   /// `RHS`. Subsequent calls with the same arguments, regardless of their
   /// order, will return the same result. If the given boolean values represent
   /// the same value, the result will be the value itself.
   BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS) const {
-    return DACtx->getOrCreateDisjunctionValue(LHS, RHS);
+    return DACtx->getOrCreateDisjunction(LHS, RHS);
   }
 
   /// Returns a boolean value that represents the negation of `Val`. Subsequent
   /// calls with the same argument will return the same result.
   BoolValue &makeNot(BoolValue &Val) const {
-    return DACtx->getOrCreateNegationValue(Val);
+    return DACtx->getOrCreateNegation(Val);
   }
 
   /// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with
   /// the same arguments, regardless of their order, will return the same
   /// result. If the given boolean values represent the same value, the result
   /// will be a value that represents the true boolean literal.
   BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) const {
-    return &LHS == &RHS ? getBoolLiteralValue(true) : makeOr(makeNot(LHS), RHS);
+    return DACtx->createImplication(LHS, RHS);
   }
 
   /// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with
   /// the same arguments, regardless of their order, will return the same
   /// result. If the given boolean values represent the same value, the result
   /// will be a value that represents the true boolean literal.
   BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) const {
-    return &LHS == &RHS
-               ? getBoolLiteralValue(true)
-               : makeAnd(makeImplication(LHS, RHS), makeImplication(RHS, LHS));
+    return DACtx->createIff(LHS, RHS);
   }
 
   /// Returns the token that identifies the flow condition of the environment.
   AtomicBoolValue &getFlowConditionToken() const { return *FlowConditionToken; }
 
   /// Adds `Val` to the set of clauses that constitute the flow condition.
   void addToFlowCondition(BoolValue &Val);
 

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

 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;
 }
 
-BoolValue &
-DataflowAnalysisContext::getOrCreateConjunctionValue(BoolValue &LHS,
+BoolValue &DataflowAnalysisContext::getOrCreateConjunction(BoolValue &LHS,
                                                            BoolValue &RHS) {
   if (&LHS == &RHS)
     return LHS;
 
   auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
                                          nullptr);
   if (Res.second)
     Res.first->second =
         &takeOwnership(std::make_unique<ConjunctionValue>(LHS, RHS));
   return *Res.first->second;
 }
 
-BoolValue &
-DataflowAnalysisContext::getOrCreateDisjunctionValue(BoolValue &LHS,
+BoolValue &DataflowAnalysisContext::getOrCreateDisjunction(BoolValue &LHS,
                                                            BoolValue &RHS) {
   if (&LHS == &RHS)
     return LHS;
 
   auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
                                          nullptr);
   if (Res.second)
     Res.first->second =
         &takeOwnership(std::make_unique<DisjunctionValue>(LHS, RHS));
   return *Res.first->second;
 }
 
-BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) {
+BoolValue &DataflowAnalysisContext::getOrCreateNegation(BoolValue &Val) {
   auto Res = NegationVals.try_emplace(&Val, nullptr);
   if (Res.second)
     Res.first->second = &takeOwnership(std::make_unique<NegationValue>(Val));
   return *Res.first->second;
 }
 
+BoolValue &DataflowAnalysisContext::createImplication(BoolValue &LHS,
+                                                      BoolValue &RHS) {
+  return &LHS == &RHS ? getBoolLiteralValue(true)
+                      : getOrCreateDisjunction(getOrCreateNegation(LHS), RHS);
+}
+
+BoolValue &DataflowAnalysisContext::createIff(BoolValue &LHS, BoolValue &RHS) {
+  return &LHS == &RHS ? getBoolLiteralValue(true)
+                      : getOrCreateConjunction(createImplication(LHS, RHS),
+                                               createImplication(RHS, LHS));
+}
+
 AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() {
   return createAtomicBoolValue();
 }
 
 void DataflowAnalysisContext::addFlowConditionConstraint(
     AtomicBoolValue &Token, BoolValue &Constraint) {
   auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint);
   if (!Res.second) {
-    Res.first->second =
-        &getOrCreateConjunctionValue(*Res.first->second, Constraint);
+    Res.first->second = &getOrCreateConjunction(*Res.first->second, Constraint);
   }
 }
 
 AtomicBoolValue &
 DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
   auto &ForkToken = makeFlowConditionToken();
   FlowConditionDeps[&ForkToken].insert(&Token);
   addFlowConditionConstraint(ForkToken, Token);
   return ForkToken;
 }
 
 AtomicBoolValue &
 DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
                                             AtomicBoolValue &SecondToken) {
   auto &Token = makeFlowConditionToken();
   FlowConditionDeps[&Token].insert(&FirstToken);
   FlowConditionDeps[&Token].insert(&SecondToken);
-  addFlowConditionConstraint(
-      Token, getOrCreateDisjunctionValue(FirstToken, SecondToken));
+  addFlowConditionConstraint(Token,
+                             getOrCreateDisjunction(FirstToken, SecondToken));
   return Token;
 }
 
 bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
                                                    BoolValue &Val) {
   // Returns true if and only if truth assignment of the flow condition implies
   // that `Val` is also true. We prove whether or not this property holds by
   // reducing the problem to satisfiability checking. In other words, we attempt
   // to show that assuming `Val` is false makes the constraints induced by the
   // flow condition unsatisfiable.
   llvm::DenseSet<BoolValue *> Constraints = {
       &Token,
       &getBoolLiteralValue(true),
-      &getOrCreateNegationValue(getBoolLiteralValue(false)),
-      &getOrCreateNegationValue(Val),
+      &getOrCreateNegation(getBoolLiteralValue(false)),
+      &getOrCreateNegation(Val),
   };
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
 }
 
 bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
   // Returns true if and only if we cannot prove that the flow condition can
   // ever be false.
   llvm::DenseSet<BoolValue *> Constraints = {
       &getBoolLiteralValue(true),
-      &getOrCreateNegationValue(getBoolLiteralValue(false)),
-      &getOrCreateNegationValue(Token),
+      &getOrCreateNegation(getBoolLiteralValue(false)),
+      &getOrCreateNegation(Token),
   };
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
 }
 
 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
     AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
   auto Res = VisitedTokens.insert(&Token);
   if (!Res.second)
     return;
 
   auto ConstraintsIT = FlowConditionConstraints.find(&Token);
   if (ConstraintsIT == FlowConditionConstraints.end()) {
     Constraints.insert(&Token);
   } else {
     // Bind flow condition token via `iff` to its set of constraints:
     // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
-    Constraints.insert(&getOrCreateConjunctionValue(
-        getOrCreateDisjunctionValue(
-            Token, getOrCreateNegationValue(*ConstraintsIT->second)),
-        getOrCreateDisjunctionValue(getOrCreateNegationValue(Token),
-                                    *ConstraintsIT->second)));
+    Constraints.insert(&createIff(Token, *ConstraintsIT->second));
   }
 
   auto DepsIT = FlowConditionDeps.find(&Token);
   if (DepsIT != FlowConditionDeps.end()) {
     for (AtomicBoolValue *DepToken : DepsIT->second) {
       addTransitiveFlowConditionConstraints(*DepToken, Constraints,
                                             VisitedTokens);
     }

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

TEST_F(DataflowAnalysisContextTest,
   auto &X = Context.createAtomicBoolValue();
   auto &Y = Context.createAtomicBoolValue();
   EXPECT_NE(&X, &Y);
 }
 
 TEST_F(DataflowAnalysisContextTest,
        GetOrCreateConjunctionValueReturnsSameExprGivenSameArgs) {
   auto &X = Context.createAtomicBoolValue();
-  auto &XAndX = Context.getOrCreateConjunctionValue(X, X);
+  auto &XAndX = Context.getOrCreateConjunction(X, X);
   EXPECT_EQ(&XAndX, &X);
 }
 
 TEST_F(DataflowAnalysisContextTest,
        GetOrCreateConjunctionValueReturnsSameExprOnSubsequentCalls) {
   auto &X = Context.createAtomicBoolValue();
   auto &Y = Context.createAtomicBoolValue();
-  auto &XAndY1 = Context.getOrCreateConjunctionValue(X, Y);
-  auto &XAndY2 = Context.getOrCreateConjunctionValue(X, Y);
+  auto &XAndY1 = Context.getOrCreateConjunction(X, Y);
+  auto &XAndY2 = Context.getOrCreateConjunction(X, Y);
   EXPECT_EQ(&XAndY1, &XAndY2);
 
-  auto &YAndX = Context.getOrCreateConjunctionValue(Y, X);
+  auto &YAndX = Context.getOrCreateConjunction(Y, X);
   EXPECT_EQ(&XAndY1, &YAndX);
 
   auto &Z = Context.createAtomicBoolValue();
-  auto &XAndZ = Context.getOrCreateConjunctionValue(X, Z);
+  auto &XAndZ = Context.getOrCreateConjunction(X, Z);
   EXPECT_NE(&XAndY1, &XAndZ);
 }
 
 TEST_F(DataflowAnalysisContextTest,
        GetOrCreateDisjunctionValueReturnsSameExprGivenSameArgs) {
   auto &X = Context.createAtomicBoolValue();
-  auto &XOrX = Context.getOrCreateDisjunctionValue(X, X);
+  auto &XOrX = Context.getOrCreateDisjunction(X, X);
   EXPECT_EQ(&XOrX, &X);
 }
 
 TEST_F(DataflowAnalysisContextTest,
        GetOrCreateDisjunctionValueReturnsSameExprOnSubsequentCalls) {
   auto &X = Context.createAtomicBoolValue();
   auto &Y = Context.createAtomicBoolValue();
-  auto &XOrY1 = Context.getOrCreateDisjunctionValue(X, Y);
-  auto &XOrY2 = Context.getOrCreateDisjunctionValue(X, Y);
+  auto &XOrY1 = Context.getOrCreateDisjunction(X, Y);
+  auto &XOrY2 = Context.getOrCreateDisjunction(X, Y);
   EXPECT_EQ(&XOrY1, &XOrY2);
 
-  auto &YOrX = Context.getOrCreateDisjunctionValue(Y, X);
+  auto &YOrX = Context.getOrCreateDisjunction(Y, X);
   EXPECT_EQ(&XOrY1, &YOrX);
 
   auto &Z = Context.createAtomicBoolValue();
-  auto &XOrZ = Context.getOrCreateDisjunctionValue(X, Z);
+  auto &XOrZ = Context.getOrCreateDisjunction(X, Z);
   EXPECT_NE(&XOrY1, &XOrZ);
 }
 
 TEST_F(DataflowAnalysisContextTest,
        GetOrCreateNegationValueReturnsSameExprOnSubsequentCalls) {
   auto &X = Context.createAtomicBoolValue();
-  auto &NotX1 = Context.getOrCreateNegationValue(X);
-  auto &NotX2 = Context.getOrCreateNegationValue(X);
+  auto &NotX1 = Context.getOrCreateNegation(X);
+  auto &NotX2 = Context.getOrCreateNegation(X);
   EXPECT_EQ(&NotX1, &NotX2);
 
   auto &Y = Context.createAtomicBoolValue();
-  auto &NotY = Context.getOrCreateNegationValue(Y);
+  auto &NotY = Context.getOrCreateNegation(Y);
   EXPECT_NE(&NotX1, &NotY);
 }
 
 TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) {
   auto &FC = Context.makeFlowConditionToken();
   auto &C = Context.createAtomicBoolValue();
   EXPECT_FALSE(Context.flowConditionImplies(FC, C));
 }
TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
   auto &C1 = Context.createAtomicBoolValue();
   auto &FC4 = Context.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC4, C1);
   EXPECT_FALSE(Context.flowConditionIsTautology(FC4));
 
   // ... but we can prove A || !A is true.
   auto &FC5 = Context.makeFlowConditionToken();
   Context.addFlowConditionConstraint(
-      FC5, Context.getOrCreateDisjunctionValue(
-               C1, Context.getOrCreateNegationValue(C1)));
+      FC5, Context.getOrCreateDisjunction(C1, Context.getOrCreateNegation(C1)));
   EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
 }
 
 } // namespace