[clang][dataflow] Extend flow conditions from block terminators

[sgatev]

Summary

This is part of the implementation of the dataflow analysis framework.
See "[RFC] A dataflow analysis framework for Clang AST" on cfe-dev.

[sgatev]

Minor tweaks.

[xazax.hun]

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

99

MergedEnv? Also, the documentation above gives a short description of the relationship between Val1, Val2, and MergedVal. But it gives little pointers what are we supposed to do with the Environment.

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

123

Is this actually correct? Or did you mean Conjunction?

[xazax.hun]

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

123

Oh, sorry. Just realized the empty set is interpreted as true. In this case this is correct.

[ymandel]

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

154

The current comment gets at the big picture, but focusing on the actual disjunction that is being guarded (that is, just the remaining, unshared clauses) may be better. So, maybe instead point out that "True v (X ^ ...)" is equivalent to "True", since if either val is nullptr it represents "true"?

clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp

111

Can we be more specific? I'd think we need to invert for specifically the successor corresponding to "else" or what not.

[sgatev]

Address reviewers' comments.

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

99

Updated the name and added some pointers in the documentation.

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

154

I added a general comment at the top and modified the comment here to target the specific case.

clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp

111

Yup. Updated the comment to be more specific.

[xazax.hun]

Thanks, with the new comments it is much clearer what is going on!

clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp

89

We only expect || and && to be terminators right? I wonder if we should add an assert so we get notified if the language gets extended with a new operator that we do not support yet.

[sgatev]

Address reviewers' comments.

[sgatev]

clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp

89

Right. Adding an assert here sounds good to me.

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

public:
 
     /// Returns true if and only if `Val1` is equivalent to `Val2`.
     ///
     /// Requirements:
     ///
     ///  `Val1` and `Val2` must be distinct.
     ///
     ///  `Val1` and `Val2` must model values of type `Type`.
+    ///
+    ///  `Val1` and `Val2` must be assigned to the same storage location in
+    ///  `Env1` and `Env2` respectively.
     virtual bool compareEquivalent(QualType Type, const Value &Val1,
-                                   const Value &Val2) {
+                                   const Environment &Env1, const Value &Val2,
+                                   const Environment &Env2) {
       // FIXME: Consider adding QualType to StructValue and removing the Type
       // argument here.
       return false;
     }
 
     /// Modifies `MergedVal` to approximate both `Val1` and `Val2`. This could
     /// be a strict lattice join or a more general widening operation. If this
     /// function returns true, `MergedVal` will be assigned to a storage
     /// location of type `Type` in `Env`.
     ///
     /// Requirements:
     ///
     ///  `Val1` and `Val2` must be distinct.
     ///
     ///  `Val1`, `Val2`, and `MergedVal` must model values of type `Type`.
-    virtual bool merge(QualType Type, const Value &Val1, const Value &Val2,
-                       Value &MergedVal, Environment &Env) {
+    ///
+    ///  `Val1` and `Val2` must be assigned to the same storage location in
+    ///  `Env1` and `Env2` respectively.
+    virtual bool merge(QualType Type, const Value &Val1,
+                       const Environment &Env1, const Value &Val2,
+                       const Environment &Env2, Value &MergedVal,
+                       Environment &Env) {
       return false;
     }
   };
 
   /// Creates an environment that uses `DACtx` to store objects that encompass
   /// the state of a program.
   explicit Environment(DataflowAnalysisContext &DACtx) : DACtx(&DACtx) {}
 
return &LHS == &RHS
                : makeAnd(makeImplication(LHS, RHS), makeImplication(RHS, LHS));
   }
 
   /// Adds `Val` to the set of clauses that constitute the flow condition.
   void addToFlowCondition(BoolValue &Val);
 
   /// Returns true if and only if the clauses that constitute the flow condition
   /// imply that `Val` is true.
-  bool flowConditionImplies(BoolValue &Val);
+  bool flowConditionImplies(BoolValue &Val) const;
 
 private:
   /// Creates a value appropriate for `Type`, if `Type` is supported, otherwise
   /// return null.
   ///
   /// Recursively initializes storage locations and values until it sees a
   /// self-referential pointer or reference type. `Visited` is used to track
   /// which types appeared in the reference/pointer chain in order to avoid

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

for (auto &Entry : Map1) {
     auto It = Map2.find(Entry.first);
     if (It != Map2.end() && Entry.second == It->second)
       Result.insert({Entry.first, Entry.second});
   }
   return Result;
 }
 
 /// Returns true if and only if `Val1` is equivalent to `Val2`.
-static bool equivalentValues(QualType Type, Value *Val1, Value *Val2,
+static bool equivalentValues(QualType Type, Value *Val1,
+                             const Environment &Env1, Value *Val2,
+                             const Environment &Env2,
                              Environment::ValueModel &Model) {
   if (Val1 == Val2)
     return true;
 
   if (auto *IndVal1 = dyn_cast<IndirectionValue>(Val1)) {
     auto *IndVal2 = cast<IndirectionValue>(Val2);
     assert(IndVal1->getKind() == IndVal2->getKind());
     return &IndVal1->getPointeeLoc() == &IndVal2->getPointeeLoc();
   }
 
-  return Model.compareEquivalent(Type, *Val1, *Val2);
+  return Model.compareEquivalent(Type, *Val1, Env1, *Val2, Env2);
 }
 
 /// Initializes a global storage value.
 static void initGlobalVar(const VarDecl &D, Environment &Env) {
   if (!D.hasGlobalStorage() ||
       Env.getStorageLocation(D, SkipPast::None) != nullptr)
     return;
 
if (auto *DS = dyn_cast<DeclStmt>(&S)) {
     }
   } else if (auto *E = dyn_cast<DeclRefExpr>(&S)) {
     initGlobalVar(*E->getDecl(), Env);
   } else if (auto *E = dyn_cast<MemberExpr>(&S)) {
     initGlobalVar(*E->getMemberDecl(), Env);
   }
 }
 
+/// Returns constraints that represent the disjunction of `Constraints1` and
+/// `Constraints2`.
+///
+/// Requirements:
+///
+///  Elements of `Constraints1` and `Constraints2` must not be null.
+llvm::DenseSet<BoolValue *>
+joinConstraints(DataflowAnalysisContext *Context,
+                const llvm::DenseSet<BoolValue *> &Constraints1,
+                const llvm::DenseSet<BoolValue *> &Constraints2) {
+  llvm::DenseSet<BoolValue *> JoinedConstraints;
+
+  if (Constraints1.empty() || Constraints2.empty()) {
+    // Disjunction of empty set and non-empty set is represented as empty set.
+    return JoinedConstraints;
+  }
+
+  BoolValue *Val1 = nullptr;
+  for (BoolValue *Constraint : Constraints1) {
+    if (Constraints2.contains(Constraint)) {
+      // If a constraint is present both in `Constraints1` and `Constraints2` we
+      // can simply add it to the result to avoid unnecessarily expanding the
+      // disjunction expression.
+      JoinedConstraints.insert(Constraint);
+    } else if (Val1 == nullptr) {
+      Val1 = Constraint;
+    } else {
+      Val1 = &Context->getOrCreateConjunctionValue(*Val1, *Constraint);
+    }
+  }
+
+  BoolValue *Val2 = nullptr;
+  for (BoolValue *Constraint : Constraints2) {
+    // Common constraints are added to `JoinedConstraints` above.
+    if (Constraints1.contains(Constraint)) {
+      continue;
+    }
+    if (Val2 == nullptr) {
+      Val2 = Constraint;
+    } else {
+      Val2 = &Context->getOrCreateConjunctionValue(*Val2, *Constraint);
+    }
+  }
+
+  // `X v (X ^ Y ^ ...)` is logically equivalent to `X`. The common conditions
+  // have already been added to the result so we don't have to do anything here
+  // in the cases where only one of the values is null.
+  if (Val1 != nullptr && Val2 != nullptr)
+    JoinedConstraints.insert(
+        &Context->getOrCreateDisjunctionValue(*Val1, *Val2));
+
+  return JoinedConstraints;
+}
+
 Environment::Environment(DataflowAnalysisContext &DACtx,
                          const DeclContext &DeclCtx)
     : Environment(DACtx) {
   if (const auto *FuncDecl = dyn_cast<FunctionDecl>(&DeclCtx)) {
     assert(FuncDecl->getBody() != nullptr);
     initGlobalVars(*FuncDecl->getBody(), *this);
     for (const auto *ParamDecl : FuncDecl->parameters()) {
       assert(ParamDecl != nullptr);
for (auto &Entry : LocToVal) {
     Value *Val = Entry.second;
     assert(Val != nullptr);
 
     auto It = Other.LocToVal.find(Loc);
     if (It == Other.LocToVal.end())
       return false;
     assert(It->second != nullptr);
 
-    if (!equivalentValues(Loc->getType(), Val, It->second, Model))
+    if (!equivalentValues(Loc->getType(), Val, *this, It->second, Other, Model))
       return false;
   }
 
   return true;
 }
 
 LatticeJoinEffect Environment::join(const Environment &Other,
                                     Environment::ValueModel &Model) {
for (auto &Entry : OldLocToVal) {
     Value *Val = Entry.second;
     assert(Val != nullptr);
 
     auto It = Other.LocToVal.find(Loc);
     if (It == Other.LocToVal.end())
       continue;
     assert(It->second != nullptr);
 
-    if (equivalentValues(Loc->getType(), Val, It->second, Model)) {
+    if (equivalentValues(Loc->getType(), Val, *this, It->second, Other,
+                         Model)) {
       LocToVal.insert({Loc, Val});
       continue;
     }
 
     // FIXME: Consider destroying `MergedValue` immediately if
     // `ValueModel::merge` returns false to avoid storing unneeded values in
     // `DACtx`.
     if (Value *MergedVal = createValue(Loc->getType()))
-      if (Model.merge(Loc->getType(), *Val, *It->second, *MergedVal, *this))
+      if (Model.merge(Loc->getType(), *Val, *this, *It->second, Other,
+                      *MergedVal, *this))
         LocToVal.insert({Loc, MergedVal});
   }
   if (OldLocToVal.size() != LocToVal.size())
     Effect = LatticeJoinEffect::Changed;
 
+  FlowConditionConstraints = joinConstraints(DACtx, FlowConditionConstraints,
+                                             Other.FlowConditionConstraints);
+
   return Effect;
 }
 
 StorageLocation &Environment::createStorageLocation(QualType Type) {
   assert(!Type.isNull());
   if (Type->isStructureOrClassType() || Type->isUnionType()) {
     // FIXME: Explore options to avoid eager initialization of fields as some of
     // them might not be needed for a particular analysis.
Value *Environment::createValueUnlessSelfReferential(
     int &CreatedValuesCount) {
   assert(!Type.isNull());
 
   // Allow unlimited fields at depth 1; only cap at deeper nesting levels.
   if ((Depth > 1 && CreatedValuesCount > MaxCompositeValueSize) ||
       Depth > MaxCompositeValueDepth)
     return nullptr;
 
+  if (Type->isBooleanType()) {
+    CreatedValuesCount++;
+    return &makeAtomicBoolValue();
+  }
+
   if (Type->isIntegerType()) {
     CreatedValuesCount++;
     return &takeOwnership(std::make_unique<IntegerValue>());
   }
 
   if (Type->isReferenceType()) {
     CreatedValuesCount++;
     QualType PointeeType = Type->getAs<ReferenceType>()->getPointeeType();
const StorageLocation &Environment::skip(const StorageLocation &Loc,
                                          SkipPast SP) const {
   return skip(*const_cast<StorageLocation *>(&Loc), SP);
 }
 
 void Environment::addToFlowCondition(BoolValue &Val) {
   FlowConditionConstraints.insert(&Val);
 }
 
-bool Environment::flowConditionImplies(BoolValue &Val) {
+bool Environment::flowConditionImplies(BoolValue &Val) const {
   // 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 = {
-      &makeNot(Val), &getBoolLiteralValue(true),
-      &makeNot(getBoolLiteralValue(false))};
+      &DACtx->getOrCreateNegationValue(Val), &getBoolLiteralValue(true),
+      &DACtx->getOrCreateNegationValue(getBoolLiteralValue(false))};
   Constraints.insert(FlowConditionConstraints.begin(),
                      FlowConditionConstraints.end());
   return DACtx->getSolver().solve(std::move(Constraints)) ==
          Solver::Result::Unsatisfiable;
 }
 
 } // namespace dataflow
 } // namespace clang

clang/lib/Analysis/FlowSensitive/Transfer.cpp

case BO_LOr: {
       if (LHSVal == nullptr)
         LHSVal = &Env.takeOwnership(std::make_unique<AtomicBoolValue>());
       if (RHSVal == nullptr)
         RHSVal = &Env.takeOwnership(std::make_unique<AtomicBoolValue>());
 
       auto &Loc = Env.createStorageLocation(*S);
       Env.setStorageLocation(*S, Loc);
       if (S->getOpcode() == BO_LAnd)
-        Env.setValue(Loc, Env.takeOwnership(std::make_unique<ConjunctionValue>(
-                              *LHSVal, *RHSVal)));
+        Env.setValue(Loc, Env.makeAnd(*LHSVal, *RHSVal));
       else
-        Env.setValue(Loc, Env.takeOwnership(std::make_unique<DisjunctionValue>(
-                              *LHSVal, *RHSVal)));
+        Env.setValue(Loc, Env.makeOr(*LHSVal, *RHSVal));
       break;
     }
     default:
       // FIXME: Add support for BO_EQ, BO_NE.
       break;
     }
   }
 
void VisitUnaryOperator(const UnaryOperator *S) {
     case UO_LNot: {
       auto *SubExprVal =
           dyn_cast_or_null<BoolValue>(Env.getValue(*SubExpr, SkipPast::None));
       if (SubExprVal == nullptr)
         break;
 
       auto &ExprLoc = Env.createStorageLocation(*S);
       Env.setStorageLocation(*S, ExprLoc);
-      Env.setValue(ExprLoc, Env.takeOwnership(
-                                std::make_unique<NegationValue>(*SubExprVal)));
+      Env.setValue(ExprLoc, Env.makeNot(*SubExprVal));
       break;
     }
     default:
       break;
     }
   }
 
   void VisitCXXThisExpr(const CXXThisExpr *S) {

clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp

 //===----------------------------------------------------------------------===//
 
 #include <memory>
 #include <system_error>
 #include <utility>
 #include <vector>
 
 #include "clang/AST/DeclCXX.h"
+#include "clang/AST/StmtVisitor.h"
 #include "clang/Analysis/Analyses/PostOrderCFGView.h"
 #include "clang/Analysis/CFG.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
 #include "clang/Analysis/FlowSensitive/DataflowWorklist.h"
 #include "clang/Analysis/FlowSensitive/Transfer.h"
 #include "clang/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/ArrayRef.h"
const Environment *getEnvironment(const Stmt &S) const override {
     return &State.getValue().Env;
   }
 
 private:
   const ControlFlowContext &CFCtx;
   llvm::ArrayRef<llvm::Optional<TypeErasedDataflowAnalysisState>> BlockToState;
 };
 
+/// Returns the index of `Block` in the successors of `Pred`.
+static int blockIndexInPredecessor(const CFGBlock &Pred,
+                                   const CFGBlock &Block) {
+  auto BlockPos = llvm::find_if(
+      Pred.succs(), [&Block](const CFGBlock::AdjacentBlock &Succ) {
+        return Succ && Succ->getBlockID() == Block.getBlockID();
+      });
+  return BlockPos - Pred.succ_begin();
+}
+
+/// Extends the flow condition of an environment based on a terminator
+/// statement.
+class TerminatorVisitor : public ConstStmtVisitor<TerminatorVisitor> {
+public:
+  TerminatorVisitor(const StmtToEnvMap &StmtToEnv, Environment &Env,
+                    int BlockSuccIdx)
+      : StmtToEnv(StmtToEnv), Env(Env), BlockSuccIdx(BlockSuccIdx) {}
+
+  void VisitIfStmt(const IfStmt *S) {
+    auto *Cond = S->getCond()->IgnoreParenImpCasts();
+    assert(Cond != nullptr);
+    extendFlowCondition(*Cond);
+  }
+
+  void VisitWhileStmt(const WhileStmt *S) {
+    auto *Cond = S->getCond()->IgnoreParenImpCasts();
+    assert(Cond != nullptr);
+    extendFlowCondition(*Cond);
+  }
+
+  void VisitBinaryOperator(const BinaryOperator *S) {
+    auto *LHS = S->getLHS()->IgnoreParenImpCasts();
+    assert(LHS != nullptr);
+    extendFlowCondition(*LHS);
+  }
+
+  void VisitConditionalOperator(const ConditionalOperator *S) {
+    auto *Cond = S->getCond()->IgnoreParenImpCasts();
+    assert(Cond != nullptr);
+    extendFlowCondition(*Cond);
+  }
+
+private:
+  void extendFlowCondition(const Expr &Cond) {
+    // The terminator sub-expression might not be evaluated.
+    if (Env.getValue(Cond, SkipPast::None) == nullptr)
+      transfer(StmtToEnv, Cond, Env);
+
+    auto *Val =
+        cast_or_null<BoolValue>(Env.getValue(Cond, SkipPast::Reference));
+    if (Val == nullptr)
+      return;
+
+    // The condition must be inversed in one of the successors.
+    if (BlockSuccIdx == 1)
+      Val = &Env.makeNot(*Val);
+
+    Env.addToFlowCondition(*Val);
+  }
+
+  const StmtToEnvMap &StmtToEnv;
+  Environment &Env;
+  int BlockSuccIdx;
+};
+
 /// Computes the input state for a given basic block by joining the output
 /// states of its predecessors.
 ///
 /// Requirements:
 ///
 ///   All predecessors of `Block` except those with loop back edges must have
 ///   already been transferred. States in `BlockStates` that are set to
 ///   `llvm::None` represent basic blocks that are not evaluated yet.
 static TypeErasedDataflowAnalysisState computeBlockInputState(
     const ControlFlowContext &CFCtx,
-    llvm::ArrayRef<llvm::Optional<TypeErasedDataflowAnalysisState>> BlockStates,
+    std::vector<llvm::Optional<TypeErasedDataflowAnalysisState>> &BlockStates,
     const CFGBlock &Block, const Environment &InitEnv,
     TypeErasedDataflowAnalysis &Analysis) {
   llvm::DenseSet<const CFGBlock *> Preds;
   Preds.insert(Block.pred_begin(), Block.pred_end());
   if (Block.getTerminator().isTemporaryDtorsBranch()) {
     // This handles a special case where the code that produced the CFG includes
     // a conditional operator with a branch that constructs a temporary and
     // calls a destructor annotated as noreturn. The CFG models this as follows:
for (const CFGBlock *Pred : Preds) {
 
     // Skip if `Pred` was not evaluated yet. This could happen if `Pred` has a
     // loop back edge to `Block`.
     const llvm::Optional<TypeErasedDataflowAnalysisState> &MaybePredState =
         BlockStates[Pred->getBlockID()];
     if (!MaybePredState.hasValue())
       continue;
 
-    const TypeErasedDataflowAnalysisState &PredState =
-        MaybePredState.getValue();
+    TypeErasedDataflowAnalysisState PredState = MaybePredState.getValue();
+    if (const Stmt *PredTerminatorStmt = Pred->getTerminatorStmt()) {
+      const StmtToEnvMapImpl StmtToEnv(CFCtx, BlockStates);
+      TerminatorVisitor(StmtToEnv, PredState.Env,
+                        blockIndexInPredecessor(*Pred, Block))
+          .Visit(PredTerminatorStmt);
+    }
+
     if (MaybeState.hasValue()) {
       Analysis.joinTypeErased(MaybeState->Lattice, PredState.Lattice);
       MaybeState->Env.join(PredState.Env, Analysis);
     } else {
-      MaybeState = PredState;
+      MaybeState = std::move(PredState);
     }
   }
   if (!MaybeState.hasValue()) {
     // FIXME: Consider passing `Block` to `Analysis.typeErasedInitialElement()`
     // to enable building analyses like computation of dominators that
     // initialize the state of each basic block differently.
     MaybeState.emplace(Analysis.typeErasedInitialElement(), InitEnv);
   }

clang/unittests/Analysis/FlowSensitive/TransferTest.cpp

runDataflow(
         ASSERT_THAT(FooDecl, NotNull());
 
         EXPECT_EQ(Env.getStorageLocation(*FooDecl, SkipPast::None), nullptr);
       },
       LangStandard::lang_cxx17,
       /*ApplyBuiltinTransfer=*/false);
 }
 
+TEST_F(TransferTest, BoolVarDecl) {
+  std::string Code = R"(
+    void target() {
+      bool Foo;
+      // [[p]]
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                ASSERT_THAT(Results, ElementsAre(Pair("p", _)));
+                const Environment &Env = Results[0].second.Env;
+
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                const StorageLocation *FooLoc =
+                    Env.getStorageLocation(*FooDecl, SkipPast::None);
+                ASSERT_TRUE(isa_and_nonnull<ScalarStorageLocation>(FooLoc));
+
+                const Value *FooVal = Env.getValue(*FooLoc);
+                EXPECT_TRUE(isa_and_nonnull<BoolValue>(FooVal));
+              });
+}
+
 TEST_F(TransferTest, IntVarDecl) {
   std::string Code = R"(
     void target() {
       int Foo;
       // [[p]]
     }
   )";
   runDataflow(
runDataflow(Code,
 
                 EXPECT_EQ(FooVal, &Env.getBoolLiteralValue(true));
                 EXPECT_EQ(BarVal, &Env.getBoolLiteralValue(false));
               });
 }
 
 TEST_F(TransferTest, AssignFromBoolConjunction) {
   std::string Code = R"(
-    void target() {
-      bool Foo = true;
-      bool Bar = true;
+    void target(bool Foo, bool Bar) {
       bool Baz = (Foo) && (Bar);
       // [[p]]
     }
   )";
   runDataflow(
       Code, [](llvm::ArrayRef<
                    std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
                    Results,
runDataflow(
 
         EXPECT_EQ(&BazVal->getLeftSubValue(), FooVal);
         EXPECT_EQ(&BazVal->getRightSubValue(), BarVal);
       });
 }
 
 TEST_F(TransferTest, AssignFromBoolDisjunction) {
   std::string Code = R"(
-    void target() {
-      bool Foo = true;
-      bool Bar = true;
+    void target(bool Foo, bool Bar) {
       bool Baz = (Foo) || (Bar);
       // [[p]]
     }
   )";
   runDataflow(
       Code, [](llvm::ArrayRef<
                    std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
                    Results,

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

if (const auto *E = selectFirst<CXXConstructExpr>(
       auto &ConstructorVal =
           *cast<StructValue>(Env.createValue(Object->getType()));
       ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(true));
       Env.setValue(*ObjectLoc, ConstructorVal);
     }
   }
 
   bool compareEquivalent(QualType Type, const Value &Val1,
-                         const Value &Val2) final {
+                         const Environment &Env1, const Value &Val2,
+                         const Environment &Env2) final {
     // Nothing to say about a value that does not model an `OptionalInt`.
     if (!Type->isRecordType() ||
         Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
       return false;
 
     return cast<StructValue>(&Val1)->getProperty("has_value") ==
            cast<StructValue>(&Val2)->getProperty("has_value");
   }
 
-  bool merge(QualType Type, const Value &Val1, const Value &Val2,
-             Value &MergedVal, Environment &Env) final {
+  bool merge(QualType Type, const Value &Val1, const Environment &Env1,
+             const Value &Val2, const Environment &Env2, Value &MergedVal,
+             Environment &Env) final {
     // Nothing to say about a value that does not model an `OptionalInt`.
     if (!Type->isRecordType() ||
         Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
       return false;
 
     auto *HasValue1 = cast_or_null<BoolValue>(
         cast<StructValue>(&Val1)->getProperty("has_value"));
     if (HasValue1 == nullptr)
runDataflow(Code,
 
                 const auto *FooVal =
                     cast<StructValue>(Env.getValue(*FooDecl, SkipPast::None));
                 EXPECT_EQ(FooVal->getProperty("has_value"),
                           &Env.getBoolLiteralValue(true));
               });
 }
 
+class FlowConditionTest : public Test {
+protected:
+  template <typename Matcher>
+  void runDataflow(llvm::StringRef Code, Matcher Match) {
+    ASSERT_THAT_ERROR(
+        test::checkDataflow<NoopAnalysis>(
+            Code, "target",
+            [](ASTContext &Context, Environment &Env) {
+              return NoopAnalysis(Context, true);
+            },
+            [&Match](
+                llvm::ArrayRef<
+                    std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                    Results,
+                ASTContext &ASTCtx) { Match(Results, ASTCtx); },
+            {"-fsyntax-only", "-std=c++17"}),
+        llvm::Succeeded());
+  }
+};
+
+TEST_F(FlowConditionTest, IfStmtSingleVar) {
+  std::string Code = R"(
+    void target(bool Foo) {
+      if (Foo) {
+        (void)0;
+        /*[[p1]]*/
+      } else {
+        (void)1;
+        /*[[p2]]*/
+      }
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                ASSERT_THAT(Results, ElementsAre(Pair("p2", _), Pair("p1", _)));
+
+                const Environment &Env1 = Results[1].second.Env;
+                auto *FooVal1 =
+                    cast<BoolValue>(Env1.getValue(*FooDecl, SkipPast::None));
+                EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1));
+
+                const Environment &Env2 = Results[0].second.Env;
+                auto *FooVal2 =
+                    cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::None));
+                EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
+              });
+}
+
+TEST_F(FlowConditionTest, IfStmtSingleNegatedVar) {
+  std::string Code = R"(
+    void target(bool Foo) {
+      if (!Foo) {
+        (void)0;
+        /*[[p1]]*/
+      } else {
+        (void)1;
+        /*[[p2]]*/
+      }
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                ASSERT_THAT(Results, ElementsAre(Pair("p2", _), Pair("p1", _)));
+
+                const Environment &Env1 = Results[1].second.Env;
+                auto *FooVal1 =
+                    cast<BoolValue>(Env1.getValue(*FooDecl, SkipPast::None));
+                EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1));
+
+                const Environment &Env2 = Results[0].second.Env;
+                auto *FooVal2 =
+                    cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::None));
+                EXPECT_TRUE(Env2.flowConditionImplies(*FooVal2));
+              });
+}
+
+TEST_F(FlowConditionTest, WhileStmt) {
+  std::string Code = R"(
+    void target(bool Foo) {
+      while (Foo) {
+        (void)0;
+        /*[[p]]*/
+      }
+    }
+  )";
+  runDataflow(
+      Code, [](llvm::ArrayRef<
+                   std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                   Results,
+               ASTContext &ASTCtx) {
+        const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        ASSERT_THAT(Results, ElementsAre(Pair("p", _)));
+        const Environment &Env = Results[0].second.Env;
+
+        auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl, SkipPast::None));
+        EXPECT_TRUE(Env.flowConditionImplies(*FooVal));
+      });
+}
+
+TEST_F(FlowConditionTest, Conjunction) {
+  std::string Code = R"(
+    void target(bool Foo, bool Bar) {
+      if (Foo && Bar) {
+        (void)0;
+        /*[[p1]]*/
+      } else {
+        (void)1;
+        /*[[p2]]*/
+      }
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
+                ASSERT_THAT(BarDecl, NotNull());
+
+                ASSERT_THAT(Results, ElementsAre(Pair("p2", _), Pair("p1", _)));
+
+                const Environment &Env1 = Results[1].second.Env;
+                auto *FooVal1 =
+                    cast<BoolValue>(Env1.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal1 =
+                    cast<BoolValue>(Env1.getValue(*BarDecl, SkipPast::None));
+                EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1));
+                EXPECT_TRUE(Env1.flowConditionImplies(*BarVal1));
+
+                const Environment &Env2 = Results[0].second.Env;
+                auto *FooVal2 =
+                    cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal2 =
+                    cast<BoolValue>(Env2.getValue(*BarDecl, SkipPast::None));
+                EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
+                EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2));
+              });
+}
+
+TEST_F(FlowConditionTest, Disjunction) {
+  std::string Code = R"(
+    void target(bool Foo, bool Bar) {
+      if (Foo || Bar) {
+        (void)0;
+        /*[[p1]]*/
+      } else {
+        (void)1;
+        /*[[p2]]*/
+      }
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
+                ASSERT_THAT(BarDecl, NotNull());
+
+                ASSERT_THAT(Results, ElementsAre(Pair("p2", _), Pair("p1", _)));
+
+                const Environment &Env1 = Results[1].second.Env;
+                auto *FooVal1 =
+                    cast<BoolValue>(Env1.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal1 =
+                    cast<BoolValue>(Env1.getValue(*BarDecl, SkipPast::None));
+                EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1));
+                EXPECT_FALSE(Env1.flowConditionImplies(*BarVal1));
+
+                const Environment &Env2 = Results[0].second.Env;
+                auto *FooVal2 =
+                    cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal2 =
+                    cast<BoolValue>(Env2.getValue(*BarDecl, SkipPast::None));
+                EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
+                EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2));
+              });
+}
+
+TEST_F(FlowConditionTest, NegatedConjunction) {
+  std::string Code = R"(
+    void target(bool Foo, bool Bar) {
+      if (!(Foo && Bar)) {
+        (void)0;
+        /*[[p1]]*/
+      } else {
+        (void)1;
+        /*[[p2]]*/
+      }
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
+                ASSERT_THAT(BarDecl, NotNull());
+
+                ASSERT_THAT(Results, ElementsAre(Pair("p2", _), Pair("p1", _)));
+
+                const Environment &Env1 = Results[1].second.Env;
+                auto *FooVal1 =
+                    cast<BoolValue>(Env1.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal1 =
+                    cast<BoolValue>(Env1.getValue(*BarDecl, SkipPast::None));
+                EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1));
+                EXPECT_FALSE(Env1.flowConditionImplies(*BarVal1));
+
+                const Environment &Env2 = Results[0].second.Env;
+                auto *FooVal2 =
+                    cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal2 =
+                    cast<BoolValue>(Env2.getValue(*BarDecl, SkipPast::None));
+                EXPECT_TRUE(Env2.flowConditionImplies(*FooVal2));
+                EXPECT_TRUE(Env2.flowConditionImplies(*BarVal2));
+              });
+}
+
+TEST_F(FlowConditionTest, DeMorgan) {
+  std::string Code = R"(
+    void target(bool Foo, bool Bar) {
+      if (!(!Foo || !Bar)) {
+        (void)0;
+        /*[[p1]]*/
+      } else {
+        (void)1;
+        /*[[p2]]*/
+      }
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
+                ASSERT_THAT(BarDecl, NotNull());
+
+                ASSERT_THAT(Results, ElementsAre(Pair("p2", _), Pair("p1", _)));
+
+                const Environment &Env1 = Results[1].second.Env;
+                auto *FooVal1 =
+                    cast<BoolValue>(Env1.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal1 =
+                    cast<BoolValue>(Env1.getValue(*BarDecl, SkipPast::None));
+                EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1));
+                EXPECT_TRUE(Env1.flowConditionImplies(*BarVal1));
+
+                const Environment &Env2 = Results[0].second.Env;
+                auto *FooVal2 =
+                    cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal2 =
+                    cast<BoolValue>(Env2.getValue(*BarDecl, SkipPast::None));
+                EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
+                EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2));
+              });
+}
+
+TEST_F(FlowConditionTest, Join) {
+  std::string Code = R"(
+    void target(bool Foo, bool Bar) {
+      if (Bar) {
+        if (!Foo)
+          return;
+      } else {
+        if (!Foo)
+          return;
+      }
+      (void)0;
+      /*[[p]]*/
+    }
+  )";
+  runDataflow(
+      Code, [](llvm::ArrayRef<
+                   std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                   Results,
+               ASTContext &ASTCtx) {
+        ASSERT_THAT(Results, ElementsAre(Pair("p", _)));
+
+        const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        const Environment &Env = Results[0].second.Env;
+        auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl, SkipPast::None));
+        EXPECT_TRUE(Env.flowConditionImplies(*FooVal));
+      });
+}
+
 } // namespace