[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

103

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

113

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

103

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

113

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

91

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

91

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`.
+    /// 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 `MergedEnv`.
+    ///
+    /// `Env1` and `Env2` can be used to query child values and path condition
+    /// implications of `Val1` and `Val2` respectively.
     ///
     /// 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 &MergedEnv) {
       return false;
     }
   };
 
   /// Creates an environment that uses `DACtx` to store objects that encompass
   /// the state of a program.
   explicit Environment(DataflowAnalysisContext &DACtx) : DACtx(&DACtx) {}
 
public:
 
   /// Returns a symbolic boolean value that models a boolean literal equal to
   /// `Value`
   AtomicBoolValue &getBoolLiteralValue(bool Value) const {
     return DACtx->getBoolLiteralValue(Value);
   }
 
   /// Returns an atomic boolean value.
-  BoolValue &makeAtomicBoolValue() { return DACtx->createAtomicBoolValue(); }
+  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) {
+  BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) const {
     return DACtx->getOrCreateConjunctionValue(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) {
+  BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS) const {
     return DACtx->getOrCreateDisjunctionValue(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) {
+  BoolValue &makeNot(BoolValue &Val) const {
     return DACtx->getOrCreateNegationValue(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) {
+  BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) const {
     return &LHS == &RHS ? getBoolLiteralValue(true) : makeOr(makeNot(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) {
+  BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) const {
     return &LHS == &RHS
                ? getBoolLiteralValue(true)
                : 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:
+///
+///  The 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) {
+  // `(X ^ Y) v (X ^ Z)` is logically equivalent to `X ^ (Y v Z)`. Therefore, to
+  // avoid unnecessarily expanding the resulting set of constraints, we will add
+  // all common constraints of `Constraints1` and `Constraints2` directly and
+  // add a disjunction of the constraints that are not common.
+
+  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)) {
+      // Add common constraints directly to `JoinedConstraints`.
+      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);
+    }
+  }
+
+  // An empty set of constraints (represented as a null value) is interpreted as
+  // `true` and `true v X` is logically equivalent to `true` so we need to add a
+  // constraint only if both `Val1` and `Val2` are not 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))};
   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/OperationKinds.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"
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/None.h"
 #include "llvm/ADT/Optional.h"
+#include "llvm/ADT/STLExtras.h"
 #include "llvm/Support/Error.h"
 
 namespace clang {
 namespace dataflow {
 
 class StmtToEnvMapImpl : public StmtToEnvMap {
 public:
   StmtToEnvMapImpl(
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) {
+    assert(S->getOpcode() == BO_LAnd || S->getOpcode() == BO_LOr);
+    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 inverted for the successor that encompasses the
+    // "else" branch, if such exists.
+    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 &MergedEnv) 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