[clang][dataflow] Implement functionality for flow condition variable…

… substitution.

This patch introduces `buildAndSubstituteFlowCondition` - given a flow condition token, this function returns the expression of constraints defining the flow condition, with values substituted where specified.

As an example:
Say we have tokens `FC1`, `FC2`, `FC3`:
```
FlowConditionConstraints: {
 FC1: C1,
 FC2: C2,
 FC3: (FC1 v FC2) ^ C3,
}
```
`buildAndSubstituteFlowCondition(FC3, /*Substitutions:*/{{C1 -> C1'}})`
returns a value corresponding to `(C1' v C2) ^ C3`.

Note:
This function returns the flow condition expressed directly as its constraints, which differs to how we currently represent the flow condition as a token bound to a set of constraints and dependencies. Making the representation consistent may be an option to consider in the future.

Depends On D128357

Reviewed By: gribozavr2, xazax.hun

Differential Revision: https://reviews.llvm.org/D128363

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

@@ -211,6 +211,27 @@ class DataflowAnalysisContext {
   AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
                                       AtomicBoolValue &SecondToken);
 
+  // FIXME: This function returns the flow condition expressed directly as its
+  // constraints: (C1 AND C2 AND ...). This differs from the general approach in
+  // the framework where a flow condition is represented as a token (an atomic
+  // boolean) with dependencies and constraints tracked in `FlowConditionDeps`
+  // and `FlowConditionConstraints`: (FC <=> C1 AND C2 AND ...).
+  // Consider if we should make the representation of flow condition consistent,
+  // returning an atomic boolean token with separate constraints instead.
+  //
+  /// Builds and returns the logical formula defining the flow condition
+  /// identified by `Token`. If a value in the formula is present as a key in
+  /// `Substitutions`, it will be substituted with the value it maps to.
+  /// As an example, say we have flow condition tokens FC1, FC2, FC3 and
+  /// FlowConditionConstraints: { FC1: C1,
+  ///                             FC2: C2,
+  ///                             FC3: (FC1 v FC2) ^ C3 }
+  /// buildAndSubstituteFlowCondition(FC3, {{C1 -> C1'}}) will return a value
+  /// corresponding to (C1' v C2) ^ C3.
+  BoolValue &buildAndSubstituteFlowCondition(
+      AtomicBoolValue &Token,
+      llvm::DenseMap<AtomicBoolValue *, BoolValue *> Substitutions);
+
   /// Returns true if and only if the constraints of the flow condition
   /// identified by `Token` imply that `Val` is true.
   bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val);
@@ -246,6 +267,23 @@ class DataflowAnalysisContext {
     return querySolver(std::move(Constraints)) == Solver::Result::Unsatisfiable;
   }
 
+  /// Returns a boolean value as a result of substituting `Val` and its sub
+  /// values based on entries in `SubstitutionsCache`. Intermediate results are
+  /// stored in `SubstitutionsCache` to avoid reprocessing values that have
+  /// already been visited.
+  BoolValue &substituteBoolValue(
+      BoolValue &Val,
+      llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache);
+
+  /// Builds and returns the logical formula defining the flow condition
+  /// identified by `Token`, sub values may be substituted based on entries in
+  /// `SubstitutionsCache`. Intermediate results are stored in
+  /// `SubstitutionsCache` to avoid reprocessing values that have already been
+  /// visited.
+  BoolValue &buildAndSubstituteFlowConditionWithCache(
+      AtomicBoolValue &Token,
+      llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache);
+
   std::unique_ptr<Solver> S;
 
   // Storage for the state of a program.

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

@@ -202,6 +202,76 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
   }
 }
 
+BoolValue &DataflowAnalysisContext::substituteBoolValue(
+    BoolValue &Val,
+    llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache) {
+  auto IT = SubstitutionsCache.find(&Val);
+  if (IT != SubstitutionsCache.end()) {
+    return *IT->second;
+  }
+  BoolValue *Result;
+  switch (Val.getKind()) {
+  case Value::Kind::AtomicBool: {
+    Result = &Val;
+    break;
+  }
+  case Value::Kind::Negation: {
+    auto &Negation = *cast<NegationValue>(&Val);
+    auto &Sub = substituteBoolValue(Negation.getSubVal(), SubstitutionsCache);
+    Result = &getOrCreateNegation(Sub);
+    break;
+  }
+  case Value::Kind::Disjunction: {
+    auto &Disjunct = *cast<DisjunctionValue>(&Val);
+    auto &LeftSub =
+        substituteBoolValue(Disjunct.getLeftSubValue(), SubstitutionsCache);
+    auto &RightSub =
+        substituteBoolValue(Disjunct.getRightSubValue(), SubstitutionsCache);
+    Result = &getOrCreateDisjunction(LeftSub, RightSub);
+    break;
+  }
+  case Value::Kind::Conjunction: {
+    auto &Conjunct = *cast<ConjunctionValue>(&Val);
+    auto &LeftSub =
+        substituteBoolValue(Conjunct.getLeftSubValue(), SubstitutionsCache);
+    auto &RightSub =
+        substituteBoolValue(Conjunct.getRightSubValue(), SubstitutionsCache);
+    Result = &getOrCreateConjunction(LeftSub, RightSub);
+    break;
+  }
+  default:
+    llvm_unreachable("Unhandled Value Kind");
+  }
+  SubstitutionsCache[&Val] = Result;
+  return *Result;
+}
+
+BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowCondition(
+    AtomicBoolValue &Token,
+    llvm::DenseMap<AtomicBoolValue *, BoolValue *> Substitutions) {
+  llvm::DenseMap<BoolValue *, BoolValue *> SubstitutionsCache(
+      Substitutions.begin(), Substitutions.end());
+  return buildAndSubstituteFlowConditionWithCache(Token, SubstitutionsCache);
+}
+
+BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowConditionWithCache(
+    AtomicBoolValue &Token,
+    llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache) {
+  auto ConstraintsIT = FlowConditionConstraints.find(&Token);
+  if (ConstraintsIT == FlowConditionConstraints.end()) {
+    return getBoolLiteralValue(true);
+  }
+  auto DepsIT = FlowConditionDeps.find(&Token);
+  if (DepsIT != FlowConditionDeps.end()) {
+    for (AtomicBoolValue *DepToken : DepsIT->second) {
+      auto &NewDep = buildAndSubstituteFlowConditionWithCache(
+          *DepToken, SubstitutionsCache);
+      SubstitutionsCache[DepToken] = &NewDep;
+    }
+  }
+  return substituteBoolValue(*ConstraintsIT->second, SubstitutionsCache);
+}
+
 } // namespace dataflow
 } // namespace clang
 

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

@@ -276,4 +276,172 @@ TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
       Context.getOrCreateConjunction(X, Context.getOrCreateConjunction(Y, Z))));
 }
 
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsAtomicFC) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // FC = X
+  auto &FC = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC, X);
+
+  // If X is true in FC, FC = X must be true
+  auto &FCWithXTrue =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
+
+  // If X is false in FC, FC = X must be false
+  auto &FC1WithXFalse =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, False));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsNegatedFC) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // FC = !X
+  auto &FC = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC, Context.getOrCreateNegation(X));
+
+  // If X is true in FC, FC = !X must be false
+  auto &FCWithXTrue =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, False));
+
+  // If X is false in FC, FC = !X must be true
+  auto &FC1WithXFalse =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsDisjunctiveFC) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // FC = X || Y
+  auto &FC = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC, Context.getOrCreateDisjunction(X, Y));
+
+  // If X is true in FC, FC = X || Y must be true
+  auto &FCWithXTrue =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
+
+  // If X is false in FC, FC = X || Y is equivalent to evaluating Y
+  auto &FC1WithXFalse =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, Y));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsConjunctiveFC) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // FC = X && Y
+  auto &FC = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
+
+  // If X is true in FC, FC = X && Y is equivalent to evaluating Y
+  auto &FCWithXTrue =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
+
+  // If X is false in FC, FC = X && Y must be false
+  auto &FCWithXFalse =
+      Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(FCWithXFalse, False));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsForkedFC) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &Z = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // FC = X && Y
+  auto &FC = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
+  // ForkedFC = FC && Z = X && Y && Z
+  auto &ForkedFC = Context.forkFlowCondition(FC);
+  Context.addFlowConditionConstraint(ForkedFC, Z);
+
+  // If any of X,Y,Z is true in ForkedFC, ForkedFC = X && Y && Z is equivalent
+  // to evaluating the conjunction of the remaining values
+  auto &ForkedFCWithZTrue =
+      Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      ForkedFCWithZTrue, Context.getOrCreateConjunction(X, Y)));
+  auto &ForkedFCWithYAndZTrue = Context.buildAndSubstituteFlowCondition(
+      ForkedFC, {{&Y, &True}, {&Z, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYAndZTrue, X));
+
+  // If any of X,Y,Z is false in ForkedFC, ForkedFC = X && Y && Z must be false
+  auto &ForkedFCWithXFalse =
+      Context.buildAndSubstituteFlowCondition(ForkedFC, {{&X, &False}});
+  auto &ForkedFCWithYFalse =
+      Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Y, &False}});
+  auto &ForkedFCWithZFalse =
+      Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithXFalse, False));
+  EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYFalse, False));
+  EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithZFalse, False));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &Z = Context.createAtomicBoolValue();
+  auto &True = Context.getBoolLiteralValue(true);
+  auto &False = Context.getBoolLiteralValue(false);
+
+  // FC1 = X
+  auto &FC1 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC1, X);
+  // FC2 = Y
+  auto &FC2 = Context.makeFlowConditionToken();
+  Context.addFlowConditionConstraint(FC2, Y);
+  // JoinedFC = (FC1 || FC2) && Z = (X || Y) && Z
+  auto &JoinedFC = Context.joinFlowConditions(FC1, FC2);
+  Context.addFlowConditionConstraint(JoinedFC, Z);
+
+  // If any of X, Y is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
+  // to evaluating the remaining Z
+  auto &JoinedFCWithXTrue =
+      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &True}});
+  auto &JoinedFCWithYTrue =
+      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithXTrue, Z));
+  EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithYTrue, Z));
+
+  // If Z is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent to
+  // evaluating the remaining disjunction (X || Y)
+  auto &JoinedFCWithZTrue =
+      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &True}});
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      JoinedFCWithZTrue, Context.getOrCreateDisjunction(X, Y)));
+
+  // If any of X, Y is false in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
+  // to evaluating the conjunction of the other value and Z
+  auto &JoinedFCWithXFalse =
+      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &False}});
+  auto &JoinedFCWithYFalse =
+      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      JoinedFCWithXFalse, Context.getOrCreateConjunction(Y, Z)));
+  EXPECT_TRUE(Context.equivalentBoolValues(
+      JoinedFCWithYFalse, Context.getOrCreateConjunction(X, Z)));
+
+  // If Z is false in JoinedFC, JoinedFC = (X || Y) && Z must be false
+  auto &JoinedFCWithZFalse =
+      Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &False}});
+  EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithZFalse, False));
+}
+
 } // namespace