[clang][dataflow] Add flow condition constraints to Environment

[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 changes to comments.

[ymandel]

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

41

I think S would be easier to read.

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

244–245

253–254

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

35

Why not use try_emplace earlier, to save of one of the lookups?

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

29–32

maybe add another one which simply tests that two calls to createAtomicBoolValue return distinct values (or even just distinct pointers?)

[xazax.hun]

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

41

Initially, I was wondering if we want to make the solver optional to potentially speed up analyses that do not need this capability. But I realized, we could just pass in a dummy no-op solver in those cases so this should be ok.

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

247

Should we move this check to DataflowAnalysisContext to protect against cases where users inadvertently try to call the its methods directly instead of using the Environment?

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

31

Alternatively, we could canonicalize BoolValues, e.g. always having the operand with the smaller address on the left. This could help us doing one less lookup (at the cost of a pointer comparison and sometimes a swap).

[sgatev]

Address reviewers' comments.

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

41

Agreed.

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

247

Done, but kept the implication and bi-conditional helpers in Environment as I'm not sure if we'll need them in DataflowAnalysisContext at this point.

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

31

Agreed. I updated the implementation.

35

Makes sense. I updated the implementation.

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

29–32

Done.

[sgatev]

Address reviewers' comments.

[xazax.hun]

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

44

As far as I understand, we need to do the double lookup (find and later try_emplace) because we do not want to allocate + take ownership when we hit the cache. An alternative is to first do try_emplace with a nullptr and overwrite the value if the emplace was successful. But I guess that also can be confusing, so it is up to you which one would you prefer.

[ymandel]

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

44

good point. I was thinking of the value case. Sorry.

[sgatev]

Address reviewers' comments.

[sgatev]

Thanks!

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

44

Makes sense and I think it doesn't look that bad so let's go with it.

[xazax.hun]

Thanks, this looks wonderful!

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

 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWANALYSISCONTEXT_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWANALYSISCONTEXT_H
 
 #include "clang/AST/Decl.h"
 #include "clang/AST/Expr.h"
+#include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/DenseMap.h"
 #include <cassert>
 #include <memory>
 #include <type_traits>
 #include <utility>
 #include <vector>
 
 namespace clang {
 namespace dataflow {
 
 /// Owns objects that encompass the state of a program and stores context that
 /// is used during dataflow analysis.
 class DataflowAnalysisContext {
 public:
-  DataflowAnalysisContext()
-      : TrueVal(takeOwnership(std::make_unique<AtomicBoolValue>())),
-        FalseVal(takeOwnership(std::make_unique<AtomicBoolValue>())) {}
+  /// Constructs a dataflow analysis context.
+  ///
+  /// Requirements:
+  ///
+  ///  `S` must not be null.
+  DataflowAnalysisContext(std::unique_ptr<Solver> S)
+      : S(std::move(S)), TrueVal(createAtomicBoolValue()),
+        FalseVal(createAtomicBoolValue()) {
+    assert(this->S != nullptr);
+  }
+
+  /// Returns the SAT solver instance that is available in this context.
+  Solver &getSolver() const { return *S; }
 
   /// Takes ownership of `Loc` and returns a reference to it.
   ///
   /// Requirements:
   ///
   ///  `Loc` must not be null.
   template <typename T>
   typename std::enable_if<std::is_base_of<StorageLocation, T>::value, T &>::type
public:
   }
 
   /// Returns a symbolic boolean value that models a boolean literal equal to
   /// `Value`.
   AtomicBoolValue &getBoolLiteralValue(bool Value) const {
     return Value ? TrueVal : FalseVal;
   }
 
+  /// Creates an atomic boolean value.
+  AtomicBoolValue &createAtomicBoolValue() {
+    return takeOwnership(std::make_unique<AtomicBoolValue>());
+  }
+
+  /// Returns a boolean value that represents the conjunction of `LHS` and
+  /// `RHS`. Subsequent calls with the same arguments, regardless of their
+  /// order, will return the same result. If the given boolean values represent
+  /// the same value, the result will be the value itself.
+  BoolValue &getOrCreateConjunctionValue(BoolValue &LHS, BoolValue &RHS);
+
+  /// Returns a boolean value that represents the disjunction of `LHS` and
+  /// `RHS`. Subsequent calls with the same arguments, regardless of their
+  /// order, will return the same result. If the given boolean values represent
+  /// the same value, the result will be the value itself.
+  BoolValue &getOrCreateDisjunctionValue(BoolValue &LHS, BoolValue &RHS);
+
+  /// Returns a boolean value that represents the negation of `Val`. Subsequent
+  /// calls with the same argument will return the same result.
+  BoolValue &getOrCreateNegationValue(BoolValue &Val);
+
 private:
+  std::unique_ptr<Solver> S;
+
   // Storage for the state of a program.
   std::vector<std::unique_ptr<StorageLocation>> Locs;
   std::vector<std::unique_ptr<Value>> Vals;
 
   // Maps from program declarations and statements to storage locations that are
   // assigned to them. These assignments are global (aggregated across all basic
   // blocks) and are used to produce stable storage locations when the same
   // basic blocks are evaluated multiple times. The storage locations that are
   // in scope for a particular basic block are stored in `Environment`.
   llvm::DenseMap<const ValueDecl *, StorageLocation *> DeclToLoc;
   llvm::DenseMap<const Expr *, StorageLocation *> ExprToLoc;
 
   StorageLocation *ThisPointeeLoc = nullptr;
 
-  // FIXME: Add support for boolean expressions.
   AtomicBoolValue &TrueVal;
   AtomicBoolValue &FalseVal;
+
+  // Indices that are used to avoid recreating the same composite boolean
+  // values.
+  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
+      ConjunctionVals;
+  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
+      DisjunctionVals;
+  llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
 };
 
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWANALYSISCONTEXT_H

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

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(); }
+
+  /// 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) {
+    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) {
+    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) {
+    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) {
+    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) {
+    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);
+
 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
   /// creating a cyclic dependency with self-referential pointers/references.
private:
   llvm::DenseMap<const StorageLocation *, Value *> LocToVal;
 
   // Maps locations of struct members to symbolic values of the structs that own
   // them and the decls of the struct members.
   llvm::DenseMap<const StorageLocation *,
                  std::pair<StructValue *, const ValueDecl *>>
       MemberLocToStruct;
 
-  // FIXME: Add flow condition constraints.
+  llvm::DenseSet<BoolValue *> FlowConditionConstraints;
 };
 
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWENVIRONMENT_H

clang/lib/Analysis/FlowSensitive/CMakeLists.txt

 add_clang_library(clangAnalysisFlowSensitive
   ControlFlowContext.cpp
+  DataflowAnalysisContext.cpp
   DataflowEnvironment.cpp
   Transfer.cpp
   TypeErasedDataflowAnalysis.cpp
   WatchedLiteralsSolver.cpp
 
   LINK_LIBS
   clangAnalysis
   clangAST
   )

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

+//===-- DataflowAnalysisContext.cpp -----------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+//  This file defines a DataflowAnalysisContext class that owns objects that
+//  encompass the state of a program and stores context that is used during
+//  dataflow analysis.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include <cassert>
+#include <memory>
+#include <utility>
+
+namespace clang {
+namespace dataflow {
+
+static std::pair<BoolValue *, BoolValue *>
+makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
+  auto Res = std::make_pair(&LHS, &RHS);
+  if (&RHS < &LHS)
+    std::swap(Res.first, Res.second);
+  return Res;
+}
+
+BoolValue &
+DataflowAnalysisContext::getOrCreateConjunctionValue(BoolValue &LHS,
+                                                     BoolValue &RHS) {
+  if (&LHS == &RHS)
+    return LHS;
+
+  auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+                                         nullptr);
+  if (Res.second)
+    Res.first->second =
+        &takeOwnership(std::make_unique<ConjunctionValue>(LHS, RHS));
+  return *Res.first->second;
+}
+
+BoolValue &
+DataflowAnalysisContext::getOrCreateDisjunctionValue(BoolValue &LHS,
+                                                     BoolValue &RHS) {
+  if (&LHS == &RHS)
+    return LHS;
+
+  auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+                                         nullptr);
+  if (Res.second)
+    Res.first->second =
+        &takeOwnership(std::make_unique<DisjunctionValue>(LHS, RHS));
+  return *Res.first->second;
+}
+
+BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) {
+  auto Res = NegationVals.try_emplace(&Val, nullptr);
+  if (Res.second)
+    Res.first->second = &takeOwnership(std::make_unique<NegationValue>(Val));
+  return *Res.first->second;
+}
+
+} // namespace dataflow
+} // namespace clang

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

StorageLocation &Environment::skip(StorageLocation &Loc, SkipPast SP) const {
   llvm_unreachable("bad SkipPast kind");
 }
 
 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) {
+  // 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/unittests/Analysis/FlowSensitive/CMakeLists.txt

 set(LLVM_LINK_COMPONENTS
   FrontendOpenMP
   Support
   )
 
 add_clang_unittest(ClangAnalysisFlowSensitiveTests
+  DataflowAnalysisContextTest.cpp
+  DataflowEnvironmentTest.cpp
   MapLatticeTest.cpp
   MultiVarConstantPropagationTest.cpp
   SingleVarConstantPropagationTest.cpp
   TestingSupport.cpp
   TestingSupportTest.cpp
   TransferTest.cpp
   TypeErasedDataflowAnalysisTest.cpp
   SolverTest.cpp

clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp

+//===- unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp ---===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+#include <memory>
+
+namespace {
+
+using namespace clang;
+using namespace dataflow;
+
+class DataflowAnalysisContextTest : public ::testing::Test {
+protected:
+  DataflowAnalysisContextTest()
+      : Context(std::make_unique<WatchedLiteralsSolver>()) {}
+
+  DataflowAnalysisContext Context;
+};
+
+TEST_F(DataflowAnalysisContextTest,
+       CreateAtomicBoolValueReturnsDistinctValues) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  EXPECT_NE(&X, &Y);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateConjunctionValueReturnsSameExprGivenSameArgs) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &XAndX = Context.getOrCreateConjunctionValue(X, X);
+  EXPECT_EQ(&XAndX, &X);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateConjunctionValueReturnsSameExprOnSubsequentCalls) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &XAndY1 = Context.getOrCreateConjunctionValue(X, Y);
+  auto &XAndY2 = Context.getOrCreateConjunctionValue(X, Y);
+  EXPECT_EQ(&XAndY1, &XAndY2);
+
+  auto &YAndX = Context.getOrCreateConjunctionValue(Y, X);
+  EXPECT_EQ(&XAndY1, &YAndX);
+
+  auto &Z = Context.createAtomicBoolValue();
+  auto &XAndZ = Context.getOrCreateConjunctionValue(X, Z);
+  EXPECT_NE(&XAndY1, &XAndZ);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateDisjunctionValueReturnsSameExprGivenSameArgs) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &XOrX = Context.getOrCreateDisjunctionValue(X, X);
+  EXPECT_EQ(&XOrX, &X);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateDisjunctionValueReturnsSameExprOnSubsequentCalls) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &XOrY1 = Context.getOrCreateDisjunctionValue(X, Y);
+  auto &XOrY2 = Context.getOrCreateDisjunctionValue(X, Y);
+  EXPECT_EQ(&XOrY1, &XOrY2);
+
+  auto &YOrX = Context.getOrCreateDisjunctionValue(Y, X);
+  EXPECT_EQ(&XOrY1, &YOrX);
+
+  auto &Z = Context.createAtomicBoolValue();
+  auto &XOrZ = Context.getOrCreateDisjunctionValue(X, Z);
+  EXPECT_NE(&XOrY1, &XOrZ);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateNegationValueReturnsSameExprOnSubsequentCalls) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &NotX1 = Context.getOrCreateNegationValue(X);
+  auto &NotX2 = Context.getOrCreateNegationValue(X);
+  EXPECT_EQ(&NotX1, &NotX2);
+
+  auto &Y = Context.createAtomicBoolValue();
+  auto &NotY = Context.getOrCreateNegationValue(Y);
+  EXPECT_NE(&NotX1, &NotY);
+}
+
+} // namespace

clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp

+//===- unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp -------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+#include <memory>
+
+namespace {
+
+using namespace clang;
+using namespace dataflow;
+
+class EnvironmentTest : public ::testing::Test {
+  DataflowAnalysisContext Context;
+
+protected:
+  EnvironmentTest()
+      : Context(std::make_unique<WatchedLiteralsSolver>()), Env(Context) {}
+
+  Environment Env;
+};
+
+TEST_F(EnvironmentTest, MakeImplicationReturnsTrueGivenSameArgs) {
+  auto &X = Env.makeAtomicBoolValue();
+  auto &XEqX = Env.makeImplication(X, X);
+  EXPECT_EQ(&XEqX, &Env.getBoolLiteralValue(true));
+}
+
+TEST_F(EnvironmentTest, MakeIffReturnsTrueGivenSameArgs) {
+  auto &X = Env.makeAtomicBoolValue();
+  auto &XEqX = Env.makeIff(X, X);
+  EXPECT_EQ(&XEqX, &Env.getBoolLiteralValue(true));
+}
+
+TEST_F(EnvironmentTest, FlowCondition) {
+  EXPECT_TRUE(Env.flowConditionImplies(Env.getBoolLiteralValue(true)));
+  EXPECT_FALSE(Env.flowConditionImplies(Env.getBoolLiteralValue(false)));
+
+  auto &X = Env.makeAtomicBoolValue();
+  EXPECT_FALSE(Env.flowConditionImplies(X));
+
+  Env.addToFlowCondition(X);
+  EXPECT_TRUE(Env.flowConditionImplies(X));
+
+  auto &NotX = Env.makeNot(X);
+  EXPECT_FALSE(Env.flowConditionImplies(NotX));
+}
+
+} // namespace

clang/unittests/Analysis/FlowSensitive/TestingSupport.h

 #include "clang/AST/Stmt.h"
 #include "clang/ASTMatchers/ASTMatchFinder.h"
 #include "clang/ASTMatchers/ASTMatchers.h"
 #include "clang/ASTMatchers/ASTMatchersInternal.h"
 #include "clang/Analysis/CFG.h"
 #include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
 #include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "clang/Basic/LLVM.h"
 #include "clang/Serialization/PCHContainerOperations.h"
 #include "clang/Tooling/ArgumentsAdjusters.h"
 #include "clang/Tooling/Tooling.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/StringMap.h"
 #include "llvm/ADT/StringRef.h"
llvm::Error checkDataflow(
   if (F == nullptr)
     return llvm::make_error<llvm::StringError>(
         llvm::errc::invalid_argument, "Could not find target function.");
 
   auto CFCtx = ControlFlowContext::build(F, F->getBody(), &F->getASTContext());
   if (!CFCtx)
     return CFCtx.takeError();
 
-  DataflowAnalysisContext DACtx;
+  DataflowAnalysisContext DACtx(std::make_unique<WatchedLiteralsSolver>());
   Environment Env(DACtx, *F);
   auto Analysis = MakeAnalysis(Context, Env);
 
   llvm::Expected<llvm::DenseMap<const clang::Stmt *, std::string>>
       StmtToAnnotations = buildStatementToAnnotationMapping(F, AnnotatedCode);
   if (!StmtToAnnotations)
     return StmtToAnnotations.takeError();
   auto &Annotations = *StmtToAnnotations;

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

 #include "clang/ASTMatchers/ASTMatchFinder.h"
 #include "clang/ASTMatchers/ASTMatchers.h"
 #include "clang/Analysis/CFG.h"
 #include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
 #include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
 #include "clang/Analysis/FlowSensitive/DataflowLattice.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "clang/Tooling/Tooling.h"
 #include "llvm/ADT/Optional.h"
 #include "llvm/ADT/STLExtras.h"
 #include "llvm/ADT/SmallSet.h"
 #include "llvm/ADT/StringRef.h"
 #include "llvm/Support/Error.h"
 #include "llvm/Testing/Support/Error.h"
 #include "gmock/gmock.h"
runAnalysis(llvm::StringRef Code, AnalysisT (*MakeAnalysis)(ASTContext &)) {
 
   Stmt *Body = Func->getBody();
   assert(Body != nullptr);
 
   auto CFCtx = llvm::cantFail(
       ControlFlowContext::build(nullptr, Body, &AST->getASTContext()));
 
   AnalysisT Analysis = MakeAnalysis(AST->getASTContext());
-  DataflowAnalysisContext DACtx;
+  DataflowAnalysisContext DACtx(std::make_unique<WatchedLiteralsSolver>());
   Environment Env(DACtx);
 
   return runDataflowAnalysis(CFCtx, Analysis, Env);
 }
 
 TEST(DataflowAnalysisTest, NoopAnalysis) {
   auto BlockStates = llvm::cantFail(
       runAnalysis<NoopAnalysis>("void target() {}", [](ASTContext &C) {