diff --git a/nullability/BUILD b/nullability/BUILD
index 3c2eb9f..8fc6c50 100644
--- a/nullability/BUILD
+++ b/nullability/BUILD
@@ -5,7 +5,10 @@
 cc_library(
     name = "pointer_nullability_lattice",
     hdrs = ["pointer_nullability_lattice.h"],
-    visibility = ["//nullability/test:__pkg__"],
+    visibility = [
+        "//nullability/inference:__pkg__",
+        "//nullability/test:__pkg__",
+    ],
     deps = [
         ":type_nullability",
         "@absl//absl/container:flat_hash_map",
@@ -19,6 +22,9 @@
     name = "pointer_nullability_matchers",
     srcs = ["pointer_nullability_matchers.cc"],
     hdrs = ["pointer_nullability_matchers.h"],
+    visibility = [
+        "//nullability/inference:__pkg__",
+    ],
     deps = [
         "@llvm-project//clang:ast",
         "@llvm-project//clang:ast_matchers",
@@ -29,7 +35,10 @@
     name = "pointer_nullability_analysis",
     srcs = ["pointer_nullability_analysis.cc"],
     hdrs = ["pointer_nullability_analysis.h"],
-    visibility = ["//nullability/test:__pkg__"],
+    visibility = [
+        "//nullability/inference:__pkg__",
+        "//nullability/test:__pkg__",
+    ],
     deps = [
         ":pointer_nullability",
         ":pointer_nullability_lattice",
@@ -82,7 +91,10 @@
     name = "pointer_nullability",
     srcs = ["pointer_nullability.cc"],
     hdrs = ["pointer_nullability.h"],
-    visibility = ["//nullability/test:__pkg__"],
+    visibility = [
+        "//nullability/inference:__pkg__",
+        "//nullability/test:__pkg__",
+    ],
     deps = [
         "@llvm-project//clang:analysis",
         "@llvm-project//clang:ast",
@@ -109,7 +121,10 @@
     name = "type_nullability",
     srcs = ["type_nullability.cc"],
     hdrs = ["type_nullability.h"],
-    visibility = ["//nullability/test:__pkg__"],
+    visibility = [
+        "//nullability/inference:__pkg__",
+        "//nullability/test:__pkg__",
+    ],
     deps = [
         "@absl//absl/log:check",
         "@llvm-project//clang:ast",
diff --git a/nullability/inference/BUILD b/nullability/inference/BUILD
index 69e1465..67af447 100644
--- a/nullability/inference/BUILD
+++ b/nullability/inference/BUILD
@@ -5,12 +5,112 @@
 package(default_applicable_licenses = ["//:license"])
 
 cc_library(
-    name = "pointer_model",
-    hdrs = ["pointer_model.h"],
+    name = "infer_nullability_constraints",
+    srcs = ["infer_nullability_constraints.cc"],
+    hdrs = ["infer_nullability_constraints.h"],
     deps = [
-        "@absl//absl/container:flat_hash_set",
+        ":inference_cc_proto",
+        ":resolve_constraints",
+        ":safety_constraint_generator",
+        "//nullability:pointer_nullability",
+        "//nullability:pointer_nullability_analysis",
+        "//nullability:pointer_nullability_lattice",
+        "//nullability:type_nullability",
+        "@absl//absl/log:check",
         "@llvm-project//clang:analysis",
+        "@llvm-project//clang:ast",
         "@llvm-project//clang:basic",
+        "@llvm-project//llvm:Support",
+    ],
+)
+
+cc_test(
+    name = "infer_nullability_constraints_test",
+    srcs = ["infer_nullability_constraints_test.cc"],
+    deps = [
+        ":analyze_target_for_test",
+        ":infer_nullability_constraints",
+        ":inference_cc_proto",
+        "@absl//absl/log:check",
+        "@com_google_googletest//:gtest_main",
+        "@llvm-project//clang:analysis",
+        "@llvm-project//clang:ast",
+        "@llvm-project//clang:ast_matchers",
+        "@llvm-project//llvm:Support",
+    ],
+)
+
+cc_library(
+    name = "resolve_constraints",
+    srcs = ["resolve_constraints.cc"],
+    hdrs = ["resolve_constraints.h"],
+    deps = [
+        ":inference_cc_proto",
+        "//nullability:pointer_nullability",
+        "@llvm-project//clang:analysis",
+        "@llvm-project//llvm:Support",
+    ],
+)
+
+cc_library(
+    name = "safety_constraint_generator",
+    srcs = ["safety_constraint_generator.cc"],
+    hdrs = ["safety_constraint_generator.h"],
+    deps = [
+        "//nullability:pointer_nullability",
+        "//nullability:pointer_nullability_lattice",
+        "//nullability:pointer_nullability_matchers",
+        "@llvm-project//clang:analysis",
+        "@llvm-project//clang:ast",
+        "@llvm-project//clang:ast_matchers",
+        "@llvm-project//llvm:Support",
+    ],
+)
+
+cc_library(
+    name = "analyze_target_for_test",
+    testonly = True,
+    srcs = ["analyze_target_for_test.cc"],
+    hdrs = ["analyze_target_for_test.h"],
+    deps = [
+        "@absl//absl/log:check",
+        "@llvm-project//clang:ast",
+        "@llvm-project//clang:ast_matchers",
+        "@llvm-project//clang:testing",
+        "@llvm-project//llvm:Support",
+    ],
+)
+
+cc_test(
+    name = "resolve_constraints_test",
+    srcs = ["resolve_constraints_test.cc"],
+    deps = [
+        ":inference_cc_proto",
+        ":resolve_constraints",
+        "//nullability:pointer_nullability",
+        "@com_google_googletest//:gtest_main",
+        "@llvm-project//clang:analysis",
+        "@llvm-project//clang:ast",
+        "@llvm-project//llvm:Support",
+    ],
+)
+
+cc_test(
+    name = "safety_constraint_generator_test",
+    srcs = ["safety_constraint_generator_test.cc"],
+    deps = [
+        ":analyze_target_for_test",
+        ":safety_constraint_generator",
+        "//nullability:pointer_nullability",
+        "//nullability:pointer_nullability_analysis",
+        "//nullability:pointer_nullability_lattice",
+        "@absl//absl/log:check",
+        "@com_google_googletest//:gtest_main",
+        "@llvm-project//clang:analysis",
+        "@llvm-project//clang:ast",
+        "@llvm-project//clang:ast_matchers",
+        "@llvm-project//clang:basic",
+        "@llvm-project//llvm:Support",
     ],
 )
 
diff --git a/nullability/inference/analyze_target_for_test.cc b/nullability/inference/analyze_target_for_test.cc
new file mode 100644
index 0000000..3a61e07
--- /dev/null
+++ b/nullability/inference/analyze_target_for_test.cc
@@ -0,0 +1,73 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "nullability/inference/analyze_target_for_test.h"
+
+#include <functional>
+#include <utility>
+
+#include "absl/log/check.h"
+#include "clang/AST/Decl.h"
+#include "clang/ASTMatchers/ASTMatchFinder.h"
+#include "clang/ASTMatchers/ASTMatchers.h"
+#include "clang/Testing/TestAST.h"
+#include "llvm/ADT/STLFunctionalExtras.h"
+#include "llvm/ADT/StringRef.h"
+
+namespace clang::tidy::nullability {
+namespace {
+using ::clang::ast_matchers::compoundStmt;
+using ::clang::ast_matchers::functionDecl;
+using ::clang::ast_matchers::hasBody;
+using ::clang::ast_matchers::hasName;
+using ::clang::ast_matchers::MatchFinder;
+
+// Simplifies creation of MatchCallbacks.
+class CallbackAdapter : public clang::ast_matchers::MatchFinder::MatchCallback {
+ public:
+  explicit CallbackAdapter(
+      std::function<void(const clang::ast_matchers::MatchFinder::MatchResult&)>
+          Callback)
+      : StoredCallback(std::move(Callback)) {
+    CHECK(StoredCallback);
+  }
+
+  void run(
+      const clang::ast_matchers::MatchFinder::MatchResult& result) override {
+    StoredCallback(result);
+  };
+
+ private:
+  std::function<void(const clang::ast_matchers::MatchFinder::MatchResult&)>
+      StoredCallback;
+};
+}  // namespace
+
+void analyzeTargetForTest(
+    llvm::StringRef Source,
+    llvm::function_ref<void(const clang::FunctionDecl&,
+                            const MatchFinder::MatchResult&)>
+        AnalysisCallback) {
+  int MatchesForFunctionDeclarationsNamedTarget = 0;
+  CallbackAdapter adapter([&, AnalysisCallback](
+                              const MatchFinder::MatchResult& result) mutable {
+    ++MatchesForFunctionDeclarationsNamedTarget;
+    const auto* MaybeFunc = result.Nodes.getNodeAs<clang::FunctionDecl>("func");
+    CHECK(MaybeFunc);
+    AnalysisCallback(*MaybeFunc, result);
+  });
+  MatchFinder Finder;
+  Finder.addMatcher(
+      functionDecl(hasName("Target"), hasBody(compoundStmt())).bind("func"),
+      &adapter);
+  clang::TestInputs Inputs(Source);
+  Inputs.FileName = "main.cc";
+  clang::TestAST Ast(Inputs);
+  Finder.matchAST(Ast.context());
+  QCHECK_EQ(MatchesForFunctionDeclarationsNamedTarget, 1)
+      << "Source must match exactly 1 function named 'Target' that has a "
+         "definition";
+}
+
+}  // namespace clang::tidy::nullability
diff --git a/nullability/inference/analyze_target_for_test.h b/nullability/inference/analyze_target_for_test.h
new file mode 100644
index 0000000..a29bb5b
--- /dev/null
+++ b/nullability/inference/analyze_target_for_test.h
@@ -0,0 +1,24 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#ifndef CRUBIT_NULLABILITY_INFERENCE_ANALYZE_TARGET_FOR_TEST_H_
+#define CRUBIT_NULLABILITY_INFERENCE_ANALYZE_TARGET_FOR_TEST_H_
+
+#include "clang/AST/Decl.h"
+#include "clang/ASTMatchers/ASTMatchFinder.h"
+#include "llvm/ADT/STLFunctionalExtras.h"
+#include "llvm/ADT/StringRef.h"
+
+namespace clang::tidy::nullability {
+
+void analyzeTargetForTest(
+    llvm::StringRef Source,
+    llvm::function_ref<
+        void(const clang::FunctionDecl&,
+             const clang::ast_matchers::MatchFinder::MatchResult&)>
+        AnalysisCallback);
+
+}  // namespace clang::tidy::nullability
+
+#endif  // CRUBIT_NULLABILITY_INFERENCE_ANALYZE_TARGET_FOR_TEST_H_
diff --git a/nullability/inference/infer_nullability_constraints.cc b/nullability/inference/infer_nullability_constraints.cc
new file mode 100644
index 0000000..1221739
--- /dev/null
+++ b/nullability/inference/infer_nullability_constraints.cc
@@ -0,0 +1,125 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "nullability/inference/infer_nullability_constraints.h"
+
+#include <optional>
+#include <vector>
+
+#include "absl/log/check.h"
+#include "nullability/inference/inference.proto.h"
+#include "nullability/inference/resolve_constraints.h"
+#include "nullability/inference/safety_constraint_generator.h"
+#include "nullability/pointer_nullability.h"
+#include "nullability/pointer_nullability_analysis.h"
+#include "nullability/pointer_nullability_lattice.h"
+#include "nullability/type_nullability.h"
+#include "clang/AST/ASTContext.h"
+#include "clang/AST/Decl.h"
+#include "clang/AST/DeclBase.h"
+#include "clang/AST/Stmt.h"
+#include "clang/AST/Type.h"
+#include "clang/Analysis/CFG.h"
+#include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "clang/Basic/LLVM.h"
+#include "clang/Basic/Specifiers.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/Support/Errc.h"
+#include "llvm/Support/Error.h"
+#include "llvm/Support/raw_ostream.h"
+
+namespace clang::tidy::nullability {
+
+namespace {
+using ::clang::dataflow::DataflowAnalysisContext;
+using ::clang::dataflow::Environment;
+using ::clang::dataflow::PointerValue;
+using ::clang::dataflow::Value;
+
+std::optional<NullabilityConstraint> inferNullabilityConstraint(
+    const clang::ParmVarDecl& P, const Environment& Environment,
+    const SafetyConstraintGenerator& SafetyConstraintGenerator) {
+  auto* Val = clang::dyn_cast_or_null<PointerValue>(Environment.getValue(P));
+  // If there's no PointerValue or its null state wasn't evaluated by the
+  // analysis, produce no facts.
+  if (!Val || !hasPointerNullState(*Val)) {
+    return std::nullopt;
+  }
+
+  // Parameters already annotated NonNull must be NonNull. This enables
+  // production of edits to synchronize the annotation from definition to all
+  // declarations.
+  if (isNonNullAnnotated(P.getType())) {
+    NullabilityConstraint Constraint;
+    Constraint.set_must_be_nonnull(true);
+    return Constraint;
+  }
+
+  return resolveConstraints(SafetyConstraintGenerator.constraints(), *Val);
+}
+}  // namespace
+
+bool isNonNullAnnotated(clang::QualType Type) {
+  CHECK(Type.getNonReferenceType()->isPointerType());
+  if (const TypeNullability Nullability =
+          getNullabilityAnnotationsFromType(Type);
+      !Nullability.empty()) {
+    return Nullability[0] == clang::NullabilityKind::NonNull;
+  }
+  return false;
+}
+
+llvm::Expected<llvm::DenseMap<const clang::Decl*, NullabilityConstraint>>
+inferNullabilityConstraints(const clang::FunctionDecl& Func,
+                            clang::ASTContext& Context) {
+  // We want to make sure we use the declaration that the body comes from,
+  // otherwise we will see references to `ParmVarDecl`s from a different
+  // declaration.
+  const clang::FunctionDecl* DeclWithBody = nullptr;
+  if (!Func.getBody(DeclWithBody)) {
+    return llvm::make_error<llvm::StringError>(llvm::errc::invalid_argument,
+                                               "Function has no body.");
+  }
+  CHECK(DeclWithBody);
+
+  llvm::DenseMap<const clang::Decl*, NullabilityConstraint> Results;
+  llvm::Expected<clang::dataflow::ControlFlowContext> ControlFlowContext =
+      clang::dataflow::ControlFlowContext::build(*DeclWithBody);
+  if (!ControlFlowContext) return Results;
+
+  DataflowAnalysisContext AnalysisContext(
+      std::make_unique<clang::dataflow::WatchedLiteralsSolver>());
+  Environment Environment(AnalysisContext, *DeclWithBody);
+  PointerNullabilityAnalysis Analysis(Context);
+  SafetyConstraintGenerator SafetyConstraintGenerator;
+
+  llvm::Expected<std::vector<std::optional<
+      clang::dataflow::DataflowAnalysisState<PointerNullabilityLattice>>>>
+      BlockToOutputStateOrError = clang::dataflow::runDataflowAnalysis(
+          *ControlFlowContext, Analysis, Environment,
+          [&SafetyConstraintGenerator, &Context](
+              const clang::CFGElement& Element,
+              const clang::dataflow::DataflowAnalysisState<
+                  PointerNullabilityLattice>& State) {
+            SafetyConstraintGenerator.collectConstraints(Element, State,
+                                                         Context);
+          });
+  if (!BlockToOutputStateOrError) {
+    return Results;
+  }
+
+  for (const auto* P : DeclWithBody->parameters()) {
+    CHECK(P != nullptr);
+    if (std::optional<NullabilityConstraint> Constraint =
+            inferNullabilityConstraint(*P, Environment,
+                                       SafetyConstraintGenerator))
+      Results[P] = *Constraint;
+  }
+  return Results;
+}
+}  // namespace clang::tidy::nullability
diff --git a/nullability/inference/infer_nullability_constraints.h b/nullability/inference/infer_nullability_constraints.h
new file mode 100644
index 0000000..374e077
--- /dev/null
+++ b/nullability/inference/infer_nullability_constraints.h
@@ -0,0 +1,36 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#ifndef CRUBIT_NULLABILITY_INFERENCE_INFER_NULLABILITY_CONSTRAINTS_H_
+#define CRUBIT_NULLABILITY_INFERENCE_INFER_NULLABILITY_CONSTRAINTS_H_
+
+#include "nullability/inference/inference.proto.h"
+#include "clang/AST/ASTContext.h"
+#include "clang/AST/Decl.h"
+#include "clang/AST/DeclBase.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/Support/Error.h"
+
+namespace clang::tidy::nullability {
+
+// Collects constraints on nullability annotations that could be added to the
+// types of Func's parameters based on the function's behavior and our
+// definition of null-safety.
+llvm::Expected<llvm::DenseMap<const clang::Decl*, NullabilityConstraint>>
+inferNullabilityConstraints(const clang::FunctionDecl& Func,
+                           clang::ASTContext& Context);
+
+// Returns whether `Type` is annotated as non-nullable at the outermost pointer
+// layer.
+//
+// e.g. returns true for int* _Nonnull,
+// but returns false for int * _Nonnull *.
+//
+// Requires that `Type` is a pointer type or reference to a pointer type,
+// possibly nested, but not e.g. a container of pointers.
+bool isNonNullAnnotated(clang::QualType Type);
+
+}  // namespace clang::tidy::nullability
+
+#endif  // CRUBIT_NULLABILITY_INFERENCE_INFER_NULLABILITY_CONSTRAINTS_H_
diff --git a/nullability/inference/infer_nullability_constraints_test.cc b/nullability/inference/infer_nullability_constraints_test.cc
new file mode 100644
index 0000000..24e6c00
--- /dev/null
+++ b/nullability/inference/infer_nullability_constraints_test.cc
@@ -0,0 +1,285 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "nullability/inference/infer_nullability_constraints.h"
+
+#include <string>
+#include <utility>
+
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+#include "absl/log/check.h"
+#include "nullability/inference/analyze_target_for_test.h"
+#include "nullability/inference/inference.proto.h"
+#include "clang/AST/Decl.h"
+#include "clang/AST/Expr.h"
+#include "clang/ASTMatchers/ASTMatchFinder.h"
+#include "clang/Analysis/CFG.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/STLFunctionalExtras.h"
+#include "llvm/ADT/StringRef.h"
+
+namespace clang::tidy::nullability {
+namespace {
+
+using ::clang::ast_matchers::MatchFinder;
+using ::testing::EqualsProto;
+using ::testing::IsEmpty;
+using ::testing::Pair;
+using ::testing::UnorderedElementsAre;
+
+using InferredNullabilityConstraints =
+    llvm::DenseMap<const clang::Decl*, NullabilityConstraint>;
+
+InferredNullabilityConstraints inferAnnotationsForTargetFunction(
+    llvm::StringRef Source) {
+  InferredNullabilityConstraints Constraints;
+  analyzeTargetForTest(
+      Source, [&Constraints](const clang::FunctionDecl& Func,
+                             const MatchFinder::MatchResult& Result) mutable {
+        auto Results = inferNullabilityConstraints(Func, *Result.Context);
+        CHECK(Results);
+        Constraints = std::move(*Results);
+      });
+  return Constraints;
+}
+
+MATCHER_P(Parameter, Name, std::string("is a parameter named ") + Name) {
+  const auto* Param = clang::dyn_cast_or_null<clang::ParmVarDecl>(arg);
+  if (!Param) {
+    return false;
+  }
+
+  const auto* Identifier = Param->getIdentifier();
+  if (!Identifier) {
+    return false;
+  }
+
+  return testing::ExplainMatchResult(testing::StrEq(Name),
+                                     Identifier->getName(), result_listener);
+}
+
+TEST(InferAnnotationsTest, NoParams) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target() {}
+  )cc";
+  EXPECT_THAT(inferAnnotationsForTargetFunction(Src), IsEmpty());
+}
+
+TEST(InferAnnotationsTest, OneParamUnused) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p0) {}
+  )cc";
+  EXPECT_THAT(inferAnnotationsForTargetFunction(Src), IsEmpty());
+}
+
+TEST(InferAnnotationsTest, OneParamUsedWithoutRestriction) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void TakesUnknown(int* unknown) {}
+
+    void Target(int* p0) { TakesUnknown(p0); }
+  )cc";
+  EXPECT_THAT(
+      inferAnnotationsForTargetFunction(Src),
+      UnorderedElementsAre(
+          Pair(Parameter("p0"), EqualsProto(R"pb(must_be_nonnull: false)pb"))));
+}
+
+TEST(InferAnnotationsTest, Deref) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p0, int* p1) {
+      int a = *p0;
+      if (p1 != nullptr) {
+        int b = *p1;
+      }
+    }
+  )cc";
+  EXPECT_THAT(
+      inferAnnotationsForTargetFunction(Src),
+      UnorderedElementsAre(
+          Pair(Parameter("p0"), EqualsProto(R"pb(must_be_nonnull: true)pb")),
+          Pair(Parameter("p1"), EqualsProto(R"pb(must_be_nonnull: false)pb"))));
+}
+
+TEST(InferAnnotationsTest, DereferenceBeforeAssignment) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p) {
+      *p;
+      int i = 1;
+      p = &i;
+    }
+  )cc";
+  EXPECT_THAT(
+      inferAnnotationsForTargetFunction(Src),
+      UnorderedElementsAre(
+          Pair(Parameter("p"), EqualsProto(R"pb(must_be_nonnull: true)pb"))));
+}
+
+TEST(InferAnnotationsTest, DereferenceAfterAssignment) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p) {
+      int i = 1;
+      p = &i;
+      *p;
+    }
+  )cc";
+  EXPECT_THAT(
+      inferAnnotationsForTargetFunction(Src),
+      UnorderedElementsAre(
+          Pair(Parameter("p"), EqualsProto(R"pb(must_be_nonnull: false)pb"))));
+}
+
+TEST(InferAnnotationsTest, DerefOfPtrRef) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int*& p0, int*& p1) {
+      int a = *p0;
+      if (p1 != nullptr) {
+        int b = *p1;
+      }
+    }
+  )cc";
+  EXPECT_THAT(
+      inferAnnotationsForTargetFunction(Src),
+      UnorderedElementsAre(
+          Pair(Parameter("p0"), EqualsProto(R"pb(must_be_nonnull: true)pb")),
+          Pair(Parameter("p1"), EqualsProto(R"pb(must_be_nonnull: false)pb"))));
+}
+
+TEST(InferAnnotationsTest, UnrelatedCondition) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p0, int* p1, int* p2, bool b) {
+      if (b) {
+        int a = *p0;
+        int b = *p1;
+      } else {
+        int a = *p0;
+        int c = *p2;
+      }
+    }
+  )cc";
+  EXPECT_THAT(
+      inferAnnotationsForTargetFunction(Src),
+      UnorderedElementsAre(
+          Pair(Parameter("p0"), EqualsProto(R"pb(must_be_nonnull: true)pb")),
+          Pair(Parameter("p1"), EqualsProto(R"pb(must_be_nonnull: true)pb")),
+          Pair(Parameter("p2"), EqualsProto(R"pb(must_be_nonnull: true)pb"))));
+}
+
+TEST(InferAnnotationsTest, LaterDeref) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p0) {
+      if (p0 == nullptr) {
+        (void)0;
+      } else {
+        (void)0;
+      }
+      int a = *p0;
+    }
+  )cc";
+  EXPECT_THAT(
+      inferAnnotationsForTargetFunction(Src),
+      UnorderedElementsAre(
+          Pair(Parameter("p0"), EqualsProto(R"pb(must_be_nonnull: true)pb"))));
+}
+
+TEST(InferAnnotationsTest, DerefBeforeGuardedDeref) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p0) {
+      int a = *p0;
+      if (p0 != nullptr) {
+        int b = *p0;
+      }
+    }
+  )cc";
+  EXPECT_THAT(
+      inferAnnotationsForTargetFunction(Src),
+      UnorderedElementsAre(
+          Pair(Parameter("p0"), EqualsProto(R"pb(must_be_nonnull: true)pb"))));
+}
+
+TEST(InferAnnotationsTest, EarlyReturn) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p0) {
+      if (!p0) {
+        return;
+      }
+      int a = *p0;
+    }
+  )cc";
+  EXPECT_THAT(
+      inferAnnotationsForTargetFunction(Src),
+      UnorderedElementsAre(
+          Pair(Parameter("p0"), EqualsProto(R"pb(must_be_nonnull: false)pb"))));
+}
+
+TEST(InferAnnotationsTest, UnreachableCode) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p0, int* p1, int* p2, int* p3) {
+      if (true) {
+        int a = *p0;
+      } else {
+        int a = *p1;
+      }
+
+      if (false) {
+        int a = *p2;
+      }
+
+      return;
+      int a = *p3;
+    }
+  )cc";
+  EXPECT_THAT(
+      inferAnnotationsForTargetFunction(Src),
+      UnorderedElementsAre(
+          Pair(Parameter("p0"), EqualsProto(R"pb(must_be_nonnull: true)pb"))));
+}
+
+TEST(InferAnnotationsTest,
+     RequiresNonNullWhenAnnotatedWithClangNullabilityAttributeAtDefinition) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* unannotated, int* _Nonnull non_null,
+                int* _Nonnull* only_inner_layer_nonnull) {
+      unannotated;
+      non_null;
+      only_inner_layer_nonnull;
+    }
+  )cc";
+  EXPECT_THAT(inferAnnotationsForTargetFunction(Src),
+              UnorderedElementsAre(
+                  Pair(Parameter("unannotated"),
+                       EqualsProto(R"pb(must_be_nonnull: false)pb")),
+                  Pair(Parameter("non_null"), EqualsProto(R"pb(must_be_nonnull:
+                                                                   true)pb")),
+                  Pair(Parameter("only_inner_layer_nonnull"),
+                       EqualsProto(R"pb(must_be_nonnull: false)pb"))));
+}
+
+TEST(InferAnnotationsTest,
+     RequiresNonNullWhenAnnotatedWithClangAnnotationAtDefinition) {
+  static constexpr llvm::StringRef Src = R"cc(
+    namespace custom {
+    template <class T>
+    using NonNull [[clang::annotate("Nonnull")]] = T;
+    }  // namespace custom
+
+    void Target(int* unannotated, custom::NonNull<int*> non_null,
+                custom::NonNull<int*>* only_inner_layer_nonnull) {
+      unannotated;
+      non_null;
+      only_inner_layer_nonnull;
+    }
+  )cc";
+  EXPECT_THAT(inferAnnotationsForTargetFunction(Src),
+              UnorderedElementsAre(
+                  Pair(Parameter("unannotated"),
+                       EqualsProto(R"pb(must_be_nonnull: false)pb")),
+                  Pair(Parameter("non_null"), EqualsProto(R"pb(must_be_nonnull:
+                                                                   true)pb")),
+                  Pair(Parameter("only_inner_layer_nonnull"),
+                       EqualsProto(R"pb(must_be_nonnull: false)pb"))));
+}
+
+}  // namespace
+}  // namespace clang::tidy::nullability
diff --git a/nullability/inference/pointer_model.h b/nullability/inference/pointer_model.h
deleted file mode 100644
index 9a54af9..0000000
--- a/nullability/inference/pointer_model.h
+++ /dev/null
@@ -1,31 +0,0 @@
-// Part of the Crubit project, under the Apache License v2.0 with LLVM
-// Exceptions. See /LICENSE for license information.
-// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-
-#ifndef CRUBIT_NULLABILITY_INFERENCE_POINTER_MODEL_H_
-#define CRUBIT_NULLABILITY_INFERENCE_POINTER_MODEL_H_
-
-#include <optional>
-
-#include "absl/container/flat_hash_set.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
-#include "clang/Basic/SourceLocation.h"
-
-namespace clang {
-namespace tidy {
-namespace nullability {
-
-// Models a single pointer value with respect to inferred nullability.
-struct PointerModel {
-  // The first location where the pointer is unconditionally dereferenced.
-  std::optional<clang::SourceLocation> UnconditionalDereference;
-
-  // The set of flow conditions under which this pointer was dereferenced.
-  absl::flat_hash_set<clang::dataflow::AtomicBoolValue*> DerefFlowConditions;
-};
-
-}  // namespace nullability
-}  // namespace tidy
-}  // namespace clang
-
-#endif  // CRUBIT_NULLABILITY_INFERENCE_POINTER_MODEL_H_
diff --git a/nullability/inference/resolve_constraints.cc b/nullability/inference/resolve_constraints.cc
new file mode 100644
index 0000000..56c357c
--- /dev/null
+++ b/nullability/inference/resolve_constraints.cc
@@ -0,0 +1,63 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "nullability/inference/resolve_constraints.h"
+
+#include "nullability/inference/inference.proto.h"
+#include "nullability/pointer_nullability.h"
+#include "clang/Analysis/FlowSensitive/Solver.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "llvm/ADT/DenseSet.h"
+
+namespace clang::tidy::nullability {
+namespace {
+bool isSatisfiable(
+    const llvm::DenseSet<clang::dataflow::BoolValue*>& ConstraintSet) {
+  clang::dataflow::WatchedLiteralsSolver Solver;
+  return Solver.solve(ConstraintSet).getStatus() ==
+         clang::dataflow::Solver::Result::Status::Satisfiable;
+}
+
+bool isUnsatisfiable(
+    const llvm::DenseSet<clang::dataflow::BoolValue*>& ConstraintSet) {
+  clang::dataflow::WatchedLiteralsSolver Solver;
+  return Solver.solve(ConstraintSet).getStatus() ==
+         clang::dataflow::Solver::Result::Status::Unsatisfiable;
+}
+}  // namespace
+
+NullabilityConstraint resolveConstraints(
+    const llvm::DenseSet<clang::dataflow::BoolValue*>& SafetyConstraints,
+    const clang::dataflow::PointerValue& Pointer) {
+  // If the safety constraints are satisfiable, then we can potentially
+  // add annotations that are necessary for them to be satisfied. If they
+  // are not all satisfiable together, we need to prune conditions in a
+  // targeted way to do the best we can with the code we have.
+  // TODO(b/268440048) Handle unsatisfiable safety constraints
+  if (!isSatisfiable(SafetyConstraints)) return {};
+
+  clang::dataflow::AtomicBoolValue& IsNull =
+      getPointerNullState(Pointer).second;
+  auto SafetyConstraintsAndIsNull = SafetyConstraints;
+  SafetyConstraintsAndIsNull.insert(&IsNull);
+
+  // If the safety constraints are satisfiable, but the conjunction of
+  // the safety constraints and this pointer being null is not
+  // satisfiable, then the safety constraints imply that the pointer
+  // must be Nonnull.
+  //
+  // Example code behaviors that could create safety conditions implying
+  // Nonnull:
+  // - For return values, a Nonnull variable assigned to the return
+  //  value of the function under analysis.
+  // - For a parameter, an unconditional dereference.
+  // TODO(b/268440048) implement safety constraints that imply Nonnull.
+  // The examples above are not implemented.
+  NullabilityConstraint NullabilityConstraint;
+  NullabilityConstraint.set_must_be_nonnull(
+      isUnsatisfiable(SafetyConstraintsAndIsNull));
+  return NullabilityConstraint;
+}
+}  // namespace clang::tidy::nullability
diff --git a/nullability/inference/resolve_constraints.h b/nullability/inference/resolve_constraints.h
new file mode 100644
index 0000000..6208940
--- /dev/null
+++ b/nullability/inference/resolve_constraints.h
@@ -0,0 +1,29 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+// An API for resolving constraints on a pointer type's nullability that are
+// implied by given safety constraints.
+//
+// Intended for use with a complete set of safety constraints generated by a
+// SafetyConstraintGenerator.
+
+#ifndef CRUBIT_NULLABILITY_INFERENCE_RESOLVE_CONSTRAINTS_H_
+#define CRUBIT_NULLABILITY_INFERENCE_RESOLVE_CONSTRAINTS_H_
+
+#include "nullability/inference/inference.proto.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseSet.h"
+
+namespace clang::tidy::nullability {
+// Resolve `SafetyConstraints` into implied constraints on the nullability
+// annotation for the pointer declaration represented by `Pointer`.
+//
+// Requires that `Pointer` has null state properties as set by
+// PointerNullabilityAnalysis.
+NullabilityConstraint resolveConstraints(
+    const llvm::DenseSet<clang::dataflow::BoolValue*>& SafetyConstraints,
+    const clang::dataflow::PointerValue& Pointer);
+}  // namespace clang::tidy::nullability
+
+#endif  // CRUBIT_NULLABILITY_INFERENCE_RESOLVE_CONSTRAINTS_H_
diff --git a/nullability/inference/resolve_constraints_test.cc b/nullability/inference/resolve_constraints_test.cc
new file mode 100644
index 0000000..254f18a
--- /dev/null
+++ b/nullability/inference/resolve_constraints_test.cc
@@ -0,0 +1,74 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "nullability/inference/resolve_constraints.h"
+
+#include <memory>
+
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+#include "nullability/inference/inference.proto.h"
+#include "nullability/pointer_nullability.h"
+#include "clang/AST/Type.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/StorageLocation.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "llvm/ADT/DenseSet.h"
+
+namespace clang::tidy::nullability {
+namespace {
+using ::testing::EqualsProto;
+
+class ResolveConstraintsTest : public testing::Test {
+ public:
+  ResolveConstraintsTest()
+      : StorageLocation(clang::dataflow::StorageLocation::Kind::Scalar,
+                        clang::QualType()),
+        Pointer(StorageLocation),
+        DataflowAnalysisContext(
+            std::make_unique<clang::dataflow::WatchedLiteralsSolver>()),
+        Environment(DataflowAnalysisContext) {
+    initUnknownPointer(Pointer, Environment);
+  }
+
+  clang::dataflow::StorageLocation StorageLocation;
+  clang::dataflow::PointerValue Pointer;
+  clang::dataflow::DataflowAnalysisContext DataflowAnalysisContext;
+  clang::dataflow::Environment Environment;
+};
+
+TEST_F(ResolveConstraintsTest, EmptyConstraintsDoNotImplyNonNull) {
+  const llvm::DenseSet<clang::dataflow::BoolValue*> Constraints;
+  EXPECT_FALSE(resolveConstraints(Constraints, Pointer).must_be_nonnull());
+}
+
+TEST_F(ResolveConstraintsTest, ArbitraryBooleanConstraintsDoNotImplyNonNull) {
+  clang::dataflow::AtomicBoolValue Atom1;
+  clang::dataflow::AtomicBoolValue Atom2;
+  const llvm::DenseSet<clang::dataflow::BoolValue*> Constraints = {&Atom1,
+                                                                   &Atom2};
+  EXPECT_FALSE(resolveConstraints(Constraints, Pointer).must_be_nonnull());
+}
+
+TEST_F(ResolveConstraintsTest, UnsatisfiableConstraintsProducesDefaultValues) {
+  clang::dataflow::AtomicBoolValue Atom1;
+  clang::dataflow::BoolValue& NotAtom1 = Environment.makeNot(Atom1);
+  const llvm::DenseSet<clang::dataflow::BoolValue*> Constraints = {&Atom1,
+                                                                   &NotAtom1};
+  EXPECT_THAT(resolveConstraints(Constraints, Pointer),
+              EqualsProto(NullabilityConstraint::default_instance()));
+}
+
+TEST_F(ResolveConstraintsTest, NotIsNullConstraintImpliesNonNull) {
+  auto& is_null = getPointerNullState(Pointer).second;
+  auto& not_is_null = Environment.makeNot(is_null);
+  const llvm::DenseSet<clang::dataflow::BoolValue*> Constraints = {
+      &not_is_null};
+  EXPECT_TRUE(resolveConstraints(Constraints, Pointer).must_be_nonnull());
+}
+
+}  // namespace
+}  // namespace clang::tidy::nullability
diff --git a/nullability/inference/safety_constraint_generator.cc b/nullability/inference/safety_constraint_generator.cc
new file mode 100644
index 0000000..e5291c6
--- /dev/null
+++ b/nullability/inference/safety_constraint_generator.cc
@@ -0,0 +1,76 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "nullability/inference/safety_constraint_generator.h"
+
+#include "nullability/pointer_nullability.h"
+#include "nullability/pointer_nullability_matchers.h"
+#include "clang/AST/ASTContext.h"
+#include "clang/AST/Expr.h"
+#include "clang/ASTMatchers/ASTMatchFinder.h"
+#include "clang/Analysis/CFG.h"
+#include "clang/Analysis/FlowSensitive/CFGMatchSwitch.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
+#include "clang/Analysis/FlowSensitive/MatchSwitch.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseSet.h"
+
+namespace clang::tidy::nullability {
+namespace {
+clang::dataflow::BoolValue* collectFromDereference(
+    const clang::UnaryOperator* Op,
+    const clang::ast_matchers::MatchFinder::MatchResult&,
+    const clang::dataflow::TransferStateForDiagnostics<
+        SafetyConstraintGenerator::LatticeType>& State) {
+  if (clang::dataflow::PointerValue* DereferencedValue =
+          getPointerValueFromExpr(Op->getSubExpr(), State.Env)) {
+    auto& NotIsNull =
+        State.Env.makeNot(getPointerNullState(*DereferencedValue).second);
+    // If the flow condition at this point in the code implies that the
+    // dereferenced value is not null, we can avoid collecting complex flow
+    // condition tokens and recognize that regardless of any annotation we could
+    // add, the current value is safe to be dereferenced.
+    if (!State.Env.flowConditionImplies(NotIsNull)) {
+      // If the flow condition is not enough to imply that the dereferenced
+      // value is not null, we need to constrain it to be so, and can avoid
+      // collecting complex flow condition tokens by simply collecting !is_null.
+      //
+      // Intuition suggests the alternative of unconditionally collecting the
+      // safety condition FlowConditions => !null or the equivalent
+      // !(FlowConditions && null), but these can potentially be satisfied by
+      // the not-fully-constrained flow conditions being false and the value
+      // being null. That expression being satisfiable doesn't mean that it is
+      // provably true in all cases. We are collecting safety constraints for
+      // which satisfiability is required and of which collective satisfiability
+      // is sufficient for null-safety.
+      return &NotIsNull;
+    }
+  }
+  return nullptr;
+}
+
+auto buildConstraintCollector() {
+  return clang::dataflow::CFGMatchSwitchBuilder<
+             const clang::dataflow::TransferStateForDiagnostics<
+                 SafetyConstraintGenerator::LatticeType>,
+             clang::dataflow::BoolValue*>()
+      .CaseOfCFGStmt<clang::UnaryOperator>(isPointerDereference(),
+                                           collectFromDereference)
+      .Build();
+}
+}  // namespace
+
+SafetyConstraintGenerator::SafetyConstraintGenerator()
+    : ConstraintCollector(buildConstraintCollector()) {}
+
+void SafetyConstraintGenerator::collectConstraints(
+    const clang::CFGElement& Element,
+    const clang::dataflow::DataflowAnalysisState<LatticeType>& State,
+    clang::ASTContext& Context) {
+  if (auto* Constraint =
+          ConstraintCollector(Element, Context, {State.Lattice, State.Env})) {
+    Constraints.insert(Constraint);
+  }
+}
+}  // namespace clang::tidy::nullability
diff --git a/nullability/inference/safety_constraint_generator.h b/nullability/inference/safety_constraint_generator.h
new file mode 100644
index 0000000..e137988
--- /dev/null
+++ b/nullability/inference/safety_constraint_generator.h
@@ -0,0 +1,68 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#ifndef CRUBIT_NULLABILITY_INFERENCE_SAFETY_CONSTRAINT_GENERATOR_H_
+#define CRUBIT_NULLABILITY_INFERENCE_SAFETY_CONSTRAINT_GENERATOR_H_
+
+#include "nullability/pointer_nullability_lattice.h"
+#include "clang/AST/ASTContext.h"
+#include "clang/AST/Expr.h"
+#include "clang/Analysis/CFG.h"
+#include "clang/Analysis/FlowSensitive/CFGMatchSwitch.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
+#include "clang/Analysis/FlowSensitive/MatchSwitch.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseSet.h"
+
+namespace clang::tidy::nullability {
+// Collects constraints that must be satisfiable to make a piece of code
+// null-safe.
+//
+// The nullability properties resulting from prospective new annotations can
+// then be combined with the constraints to determine if there is only one valid
+// annotation for an unannotated nullability slot.
+//
+// Intended for use with PointerNullabilityAnalysis, a DataflowAnalysis which
+// stores nullability information in properties on PointerValues. The boolean
+// expressions collected by CollectConstraints will utilize the boolean
+// expressions stored in those properties.
+class SafetyConstraintGenerator {
+ public:
+  using LatticeType = PointerNullabilityLattice;
+
+  SafetyConstraintGenerator();
+
+  // Collects constraints implied by pointer usage in `Element`.
+  //
+  // Intended for use as a PostVisitCFG after running
+  // PointerNullabilityAnalysis. Assumes that `State` includes pointer
+  // nullability state as set by PointerNullabilityAnalysis.
+  void collectConstraints(
+      const clang::CFGElement& Element,
+      const clang::dataflow::DataflowAnalysisState<LatticeType>& State,
+      clang::ASTContext& Context);
+
+  // Retrieves constraints gathered thus far. Until all analyzed CFGElements
+  // have been processed by `collectConstraints`, the return value will not
+  // represent all safety constraints implied by the code.
+  //
+  // Intended for use after the completion of the DataflowAnalysis and
+  // PostVisitCFG process.
+  //
+  // Constraints take the form of boolean expressions that must be satisfiable
+  // in order for the processed code to be null-safe.
+  const llvm::DenseSet<clang::dataflow::BoolValue*>& constraints() const {
+    return Constraints;
+  }
+
+ private:
+  llvm::DenseSet<clang::dataflow::BoolValue*> Constraints;
+  clang::dataflow::CFGMatchSwitch<
+      const clang::dataflow::TransferStateForDiagnostics<LatticeType>,
+      clang::dataflow::BoolValue*>
+      ConstraintCollector;
+};
+}  // namespace clang::tidy::nullability
+
+#endif  // CRUBIT_NULLABILITY_INFERENCE_SAFETY_CONSTRAINT_GENERATOR_H_
diff --git a/nullability/inference/safety_constraint_generator_test.cc b/nullability/inference/safety_constraint_generator_test.cc
new file mode 100644
index 0000000..ca0fe44
--- /dev/null
+++ b/nullability/inference/safety_constraint_generator_test.cc
@@ -0,0 +1,215 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "nullability/inference/safety_constraint_generator.h"
+
+#include <memory>
+#include <optional>
+#include <vector>
+
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+#include "absl/log/check.h"
+#include "nullability/inference/analyze_target_for_test.h"
+#include "nullability/pointer_nullability.h"
+#include "nullability/pointer_nullability_analysis.h"
+#include "nullability/pointer_nullability_lattice.h"
+#include "clang/AST/Decl.h"
+#include "clang/ASTMatchers/ASTMatchFinder.h"
+#include "clang/Analysis/CFG.h"
+#include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Error.h"
+
+namespace clang::tidy::nullability {
+namespace {
+
+using ::testing::AllOf;
+using ::testing::IsEmpty;
+using ::testing::Not;
+using ::testing::SizeIs;
+using ::testing::UnorderedElementsAre;
+
+// Analyzes the to-be-matched code snippet with PointerNullabilityAnalysis, and
+// then matches against the constraints produced by SafetyConstraintGenerator
+// for the snippet.
+//
+// `ConstraintsMatcherProducer` should be a function taking the Environment
+// and a vector of PointerValue* representing the Target function's parameters
+// and returning a matcher for the generated constraints. This allows for
+// matching of the constraints against individual parameter null state
+// properties.
+MATCHER_P(ProducesSafetyConstraints, ConstraintsMatcherProducer, "") {
+  bool Success = false;
+  auto MatcherProducer = ConstraintsMatcherProducer;
+  analyzeTargetForTest(
+      arg, [&Success, &MatcherProducer, &result_listener](
+               const clang::FunctionDecl& Func,
+               const clang::ast_matchers::MatchFinder::MatchResult& Result) {
+        QCHECK(Func.hasBody()) << "Matched function has no body.";
+        QCHECK(Result.Context) << "Missing ASTContext from match result.";
+        llvm::Expected<clang::dataflow::ControlFlowContext> ControlFlowContext =
+            clang::dataflow::ControlFlowContext::build(Func);
+        clang::dataflow::DataflowAnalysisContext AnalysisContext(
+            std::make_unique<clang::dataflow::WatchedLiteralsSolver>());
+        clang::dataflow::Environment Environment(AnalysisContext, Func);
+        PointerNullabilityAnalysis Analysis(*Result.Context);
+        SafetyConstraintGenerator Generator;
+        llvm::Expected<std::vector<std::optional<
+            clang::dataflow::DataflowAnalysisState<PointerNullabilityLattice>>>>
+            BlockToOutputStateOrError = clang::dataflow::runDataflowAnalysis(
+                *ControlFlowContext, Analysis, Environment,
+                [&Generator, &Result](
+                    const clang::CFGElement& Element,
+                    const clang::dataflow::DataflowAnalysisState<
+                        PointerNullabilityLattice>& State) {
+                  Generator.collectConstraints(Element, State, *Result.Context);
+                });
+
+        QCHECK(BlockToOutputStateOrError)
+            << "No output state from dataflow analysis.";
+
+        // TODO(b/268440048) When we can retrieve the improved atoms
+        // representing annotations, stop using the Environment to retrieve the
+        // initial Environment PointerValues, which won't work for local
+        // variables down the road.
+        std::vector<clang::dataflow::PointerValue*> ParamDeclPointerValues;
+        for (const auto* P : Func.parameters()) {
+          CHECK(P != nullptr);
+          auto* Val = clang::dyn_cast_or_null<clang::dataflow::PointerValue>(
+              Environment.getValue(*P));
+          if (Val) {
+            ParamDeclPointerValues.push_back(Val);
+          }
+        }
+        Success = ExplainMatchResult(
+            MatcherProducer(Environment, ParamDeclPointerValues),
+            Generator.constraints(), result_listener);
+      });
+  return Success;
+}
+
+TEST(SafetyConstraintGenerator, GeneratesNoConstraintsForEmptyFunctionDefn) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target() {}
+  )cc";
+  EXPECT_THAT(Src, ProducesSafetyConstraints(
+                       [](auto Environment, auto ParamPointerValues) {
+                         return IsEmpty();
+                       }));
+}
+
+TEST(SafetyConstraintGenerator, GeneratesNoConstraintsForUnusedParam) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p) {}
+  )cc";
+  EXPECT_THAT(Src, ProducesSafetyConstraints(
+                       [](auto Environment, auto ParamPointerValues) {
+                         return IsEmpty();
+                       }));
+}
+
+TEST(SafetyConstraintGenerator, GeneratesNotIsNullConstraintForDeref) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p) { *p; }
+  )cc";
+  EXPECT_THAT(Src, ProducesSafetyConstraints([](auto Environment,
+                                                auto ParamPointerValues) {
+                return UnorderedElementsAre(&Environment.makeNot(
+                    getPointerNullState(*ParamPointerValues[0]).second));
+              }));
+}
+
+TEST(SafetyConstraintGenerator,
+     GeneratesNotIsNullConstraintForImproperlyGuardedDeref) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p) {
+      if (p == nullptr) *p;
+    }
+  )cc";
+  EXPECT_THAT(Src, ProducesSafetyConstraints([](auto Environment,
+                                                auto ParamPointerValues) {
+                return UnorderedElementsAre(&Environment.makeNot(
+                    getPointerNullState(*ParamPointerValues[0]).second));
+              }));
+}
+
+TEST(SafetyConstraintGenerator, GeneratesConstraintsForAllParams) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p, int* q, int* r) {
+      *p;
+      *q;
+      *r;
+    }
+  )cc";
+  EXPECT_THAT(Src, ProducesSafetyConstraints([](auto Environment,
+                                                auto ParamPointerValues) {
+                return UnorderedElementsAre(
+                    &Environment.makeNot(
+                        getPointerNullState(*ParamPointerValues[0]).second),
+                    &Environment.makeNot(
+                        getPointerNullState(*ParamPointerValues[1]).second),
+                    &Environment.makeNot(
+                        getPointerNullState(*ParamPointerValues[2]).second));
+              }));
+}
+
+TEST(SafetyConstraintGenerator, DoesntGenerateConstraintForNullCheckedPtr) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void Target(int* p) {
+      if (p) *p;
+      if (p != nullptr) *p;
+    }
+  )cc";
+  EXPECT_THAT(Src, ProducesSafetyConstraints(
+                       [](auto Environment, auto ParamPointerValues) {
+                         return IsEmpty();
+                       }));
+}
+
+TEST(SafetyConstraintGenerator,
+     ConstrainsParameterIfDereferencedBeforeAssignment) {
+  static constexpr llvm::StringRef Src = R"cc(
+    int* getPtr();
+
+    void Target(int* p) {
+      *p;
+      p = getPtr();
+    }
+  )cc";
+  EXPECT_THAT(Src, ProducesSafetyConstraints([](auto Environment,
+                                                auto ParamPointerValues) {
+                return UnorderedElementsAre(&Environment.makeNot(
+                    getPointerNullState(*ParamPointerValues[0]).second));
+              }));
+}
+
+TEST(SafetyConstraintGenerator,
+     DoesNotConstrainParameterIfDereferencedAfterAssignment) {
+  static constexpr llvm::StringRef Src = R"cc(
+    int* getPtr();
+
+    void Target(int* p) {
+      p = getPtr();
+      *p;
+    }
+  )cc";
+  EXPECT_THAT(
+      Src,
+      ProducesSafetyConstraints([](auto Environment, auto ParamPointerValues) {
+        return AllOf(SizeIs(1),
+                     // TODO(b/268440048) Figure out how to access and assert
+                     // equality for the constraint that this is.
+                     Not(UnorderedElementsAre(&Environment.makeNot(
+                         getPointerNullState(*ParamPointerValues[0]).second))));
+      }));
+}
+}  // namespace
+}  // namespace clang::tidy::nullability