diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -183,6 +183,21 @@
   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.
+  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);
@@ -200,6 +215,23 @@
       AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
       llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
 
+  /// 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 &substituteBoolVal(
+      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.
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -158,6 +158,77 @@
   }
 }
 
+BoolValue &DataflowAnalysisContext::substituteBoolVal(
+    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 = substituteBoolVal(Negation.getSubVal(), SubstitutionsCache);
+    Result = &getOrCreateNegationValue(Sub);
+    break;
+  }
+  case Value::Kind::Disjunction: {
+    auto &Disjunct = *cast<DisjunctionValue>(&Val);
+    auto &LeftSub =
+        substituteBoolVal(Disjunct.getLeftSubValue(), SubstitutionsCache);
+    auto &RightSub =
+        substituteBoolVal(Disjunct.getRightSubValue(), SubstitutionsCache);
+    Result = &getOrCreateDisjunctionValue(LeftSub, RightSub);
+    break;
+  }
+  case Value::Kind::Conjunction: {
+    auto &Conjunct = *cast<ConjunctionValue>(&Val);
+    auto &LeftSub =
+        substituteBoolVal(Conjunct.getLeftSubValue(), SubstitutionsCache);
+    auto &RightSub =
+        substituteBoolVal(Conjunct.getRightSubValue(), SubstitutionsCache);
+    Result = &getOrCreateConjunctionValue(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;
+  SubstitutionsCache.insert(Substitutions.begin(), Substitutions.end());
+  return buildAndSubstituteFlowConditionWithCache(Token, SubstitutionsCache);
+}
+
+BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowConditionWithCache(
+    AtomicBoolValue &Token,
+    llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache) {
+  auto DepsIt = FlowConditionDeps.find(&Token);
+  if (DepsIt != FlowConditionDeps.end()) {
+    for (AtomicBoolValue *DepToken : DepsIt->second) {
+      auto &NewDep = buildAndSubstituteFlowConditionWithCache(
+          *DepToken, SubstitutionsCache);
+      SubstitutionsCache[DepToken] = &NewDep;
+    }
+  }
+  auto ConstraintsIt = FlowConditionConstraints.find(&Token);
+  if (ConstraintsIt != FlowConditionConstraints.end()) {
+    auto &Constraints = *ConstraintsIt->second;
+    return substituteBoolVal(Constraints, SubstitutionsCache);
+  }
+  return getBoolLiteralValue(true);
+}
+
 } // namespace dataflow
 } // namespace clang
 
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -169,4 +169,54 @@
   EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
 }
 
+// FIXME: Consider implementing pretty print feature for values for clarity of
+// testing
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionEmptyFC) {
+  auto &FC = Context.makeFlowConditionToken();
+  auto &X = Context.createAtomicBoolValue();
+
+  auto XTrue = llvm::DenseMap<AtomicBoolValue *, BoolValue *>(
+      {{&X, &Context.getBoolLiteralValue(true)}});
+  auto &FCWithXTrue = Context.buildAndSubstituteFlowCondition(FC, XTrue);
+
+  auto XFalse = llvm::DenseMap<AtomicBoolValue *, BoolValue *>(
+      {{&X, &Context.getBoolLiteralValue(false)}});
+  auto &FCWithXFalse = Context.buildAndSubstituteFlowCondition(FC, XFalse);
+
+  auto &FCIndependentOfX =
+      Context.getOrCreateConjunctionValue(FCWithXTrue, FCWithXFalse);
+
+  // FC = {}
+  // Empty flow condition holds regardless of value of boolean X
+  EXPECT_TRUE(Context.flowConditionImplies(FC, FCIndependentOfX));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsDisjunctiveFC1) {
+  auto &FC = Context.makeFlowConditionToken();
+  auto &B = Context.createAtomicBoolValue();
+  auto &X = Context.createAtomicBoolValue();
+  Context.addFlowConditionConstraint(
+      FC, Context.getOrCreateDisjunctionValue(
+              Context.getOrCreateNegationValue(B),
+              Context.getOrCreateConjunctionValue(B, X)));
+
+  auto XTrue = llvm::DenseMap<AtomicBoolValue *, BoolValue *>(
+      {{&X, &Context.getBoolLiteralValue(true)}});
+  auto &FCWithXTrue = Context.buildAndSubstituteFlowCondition(FC, XTrue);
+
+  auto XFalse = llvm::DenseMap<AtomicBoolValue *, BoolValue *>(
+      {{&X, &Context.getBoolLiteralValue(false)}});
+  auto &FCWithXFalse = Context.buildAndSubstituteFlowCondition(FC, XFalse);
+
+  auto &FCIndependentOfX =
+      Context.getOrCreateConjunctionValue(FCWithXTrue, FCWithXFalse);
+
+  // FC = (!B) || (B && X)
+  // The flow condition holds when
+  // 1. B is false, independent of value of X
+  // 2. B is true, and X is true
+  EXPECT_TRUE(Context.flowConditionImplies(
+      FC, Context.getOrCreateDisjunctionValue(FCIndependentOfX, B)));
+}
+
 } // namespace