Collect evidence for function parameters from observed call sites.

Records Nonnull, Nullable, and Unknown arguments for use in flexible heuristics.

PiperOrigin-RevId: 549105355
Change-Id: Iea59d3ff84987446357d84cdba11df6d6ba8478f
diff --git a/nullability/BUILD b/nullability/BUILD
index 2d4e9c4..7abc7b6 100644
--- a/nullability/BUILD
+++ b/nullability/BUILD
@@ -110,6 +110,7 @@
         ":pointer_nullability",
         "@llvm-project//clang:analysis",
         "@llvm-project//clang:ast",
+        "@llvm-project//clang:basic",
         "@llvm-project//third-party/unittest:gtest",
         "@llvm-project//third-party/unittest:gtest_main",
     ],
diff --git a/nullability/inference/BUILD b/nullability/inference/BUILD
index 7a5efa4..1112c86 100644
--- a/nullability/inference/BUILD
+++ b/nullability/inference/BUILD
@@ -10,7 +10,6 @@
     hdrs = ["collect_evidence.h"],
     deps = [
         ":inference_cc_proto",
-        "@absl//absl/log:check",
         "//nullability:pointer_nullability",
         "//nullability:pointer_nullability_analysis",
         "//nullability:pointer_nullability_lattice",
diff --git a/nullability/inference/collect_evidence.cc b/nullability/inference/collect_evidence.cc
index 9526c48..ac788b6 100644
--- a/nullability/inference/collect_evidence.cc
+++ b/nullability/inference/collect_evidence.cc
@@ -23,10 +23,12 @@
 #include "clang/AST/Stmt.h"
 #include "clang/AST/Type.h"
 #include "clang/Analysis/CFG.h"
+#include "clang/Analysis/FlowSensitive/Arena.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/Formula.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "clang/Basic/LLVM.h"
@@ -74,6 +76,13 @@
 }
 
 namespace {
+bool isInferenceTarget(const FunctionDecl &FD) {
+  // Inferring properties of template instantiations isn't useful in itself.
+  // We can't record them anywhere unless they apply to the template in general.
+  // TODO: work out in what circumstances that would be safe.
+  return !FD.getTemplateInstantiationPattern();
+}
+
 void collectEvidenceFromDereference(
     std::vector<std::pair<PointerTypeNullability, Slot>> InferrableSlots,
     const CFGElement &Element, const PointerNullabilityLattice &Lattice,
@@ -113,11 +122,75 @@
   }
 }
 
+void collectEvidenceFromCallExpr(
+    std::vector<std::pair<PointerTypeNullability, Slot>> InferrableCallerSlots,
+    const CFGElement &Element, const PointerNullabilityLattice &Lattice,
+    const dataflow::Environment &Env,
+    llvm::function_ref<EvidenceEmitter> Emit) {
+  // Is this CFGElement a call to a function?
+  auto CFGStmt = Element.getAs<clang::CFGStmt>();
+  if (!CFGStmt) return;
+  auto *CallExpr = dyn_cast_or_null<clang::CallExpr>(CFGStmt->getStmt());
+  if (!CallExpr || !CallExpr->getCalleeDecl()) return;
+  auto *CalleeDecl =
+      dyn_cast_or_null<clang::FunctionDecl>(CallExpr->getCalleeDecl());
+  if (!CalleeDecl || !isInferenceTarget(*CalleeDecl)) return;
+
+  // For each inferrable parameter of the callee, ...
+  for (unsigned I = 0; I < CalleeDecl->param_size(); ++I) {
+    if (!CalleeDecl->getParamDecl(I)
+             ->getType()
+             .getNonReferenceType()
+             ->isPointerType())
+      return;
+
+    // if we're passing a pointer, ...
+    dataflow::PointerValue *PV =
+        getPointerValueFromExpr(CallExpr->getArg(I), Env);
+    if (!PV) return;
+
+    // TODO: Check if the parameter is annotated. If annotated Nonnull, (instead
+    // of collecting evidence for it?) collect evidence similar to a
+    // dereference, i.e. if the argument is not already proven Nonnull, collect
+    // evidence for a parameter that could be annotated Nonnull as a way to
+    // force the argument to be Nonnull.
+
+    // emit evidence of the parameter's nullability. First, calculate that
+    // nullability based on InferrableSlots for the caller being assigned to
+    // Unknown, to reflect the current annotations and not all possible
+    // annotations for them.
+    dataflow::Arena &A = Env.getDataflowAnalysisContext().arena();
+    const dataflow::Formula *CallerSlotsUnknown = &A.makeLiteral(true);
+    for (auto &[Nullability, Slot] : InferrableCallerSlots) {
+      CallerSlotsUnknown =
+          &A.makeAnd(*CallerSlotsUnknown,
+                     A.makeAnd(A.makeNot(Nullability.Nullable->formula()),
+                               A.makeNot(Nullability.Nonnull->formula())));
+    }
+
+    NullabilityKind ArgNullability =
+        getNullability(*PV, Env, CallerSlotsUnknown);
+    Evidence::Kind ArgEvidenceKind;
+    switch (ArgNullability) {
+      case NullabilityKind::Nullable:
+        ArgEvidenceKind = Evidence::NULLABLE_ARGUMENT;
+        break;
+      case NullabilityKind::NonNull:
+        ArgEvidenceKind = Evidence::NONNULL_ARGUMENT;
+        break;
+      default:
+        ArgEvidenceKind = Evidence::UNKNOWN_ARGUMENT;
+    }
+    Emit(*CalleeDecl, paramSlot(I), ArgEvidenceKind);
+  }
+}
+
 void collectEvidenceFromElement(
     std::vector<std::pair<PointerTypeNullability, Slot>> InferrableSlots,
     const CFGElement &Element, const PointerNullabilityLattice &Lattice,
     const Environment &Env, llvm::function_ref<EvidenceEmitter> Emit) {
   collectEvidenceFromDereference(InferrableSlots, Element, Lattice, Env, Emit);
+  collectEvidenceFromCallExpr(InferrableSlots, Element, Lattice, Env, Emit);
   // TODO: add location information.
   // TODO: add more heuristic collections here
 }
@@ -195,13 +268,6 @@
   }
 }
 
-bool isInferenceTarget(const FunctionDecl &FD) {
-  // Inferring properties of template instantiations isn't useful in itself.
-  // We can't record them anywhere unless they apply to the template in general.
-  // TODO: work out in what circumstances that would be safe.
-  return !FD.getTemplateInstantiationPattern();
-}
-
 EvidenceSites EvidenceSites::discover(ASTContext &Ctx) {
   struct Walker : public RecursiveASTVisitor<Walker> {
     EvidenceSites Out;
diff --git a/nullability/inference/collect_evidence_test.cc b/nullability/inference/collect_evidence_test.cc
index 1fa7375..fc06aed 100644
--- a/nullability/inference/collect_evidence_test.cc
+++ b/nullability/inference/collect_evidence_test.cc
@@ -22,17 +22,20 @@
 
 namespace clang::tidy::nullability {
 namespace {
+using ::testing::_;
+using ::testing::Contains;
 using ::testing::ElementsAre;
 using ::testing::IsEmpty;
+using ::testing::Not;
 using ::testing::UnorderedElementsAre;
 
-MATCHER_P3(isEvidenceMatcher, S, Kind, SymbolMatcher, "") {
-  return arg.slot() == S && arg.kind() == Kind &&
-         SymbolMatcher.Matches(arg.symbol());
+MATCHER_P3(isEvidenceMatcher, SlotMatcher, KindMatcher, SymbolMatcher, "") {
+  return SlotMatcher.Matches(static_cast<Slot>(arg.slot())) &&
+         KindMatcher.Matches(arg.kind()) && SymbolMatcher.Matches(arg.symbol());
 }
 
 testing::Matcher<const Evidence&> evidence(
-    Slot S, Evidence::Kind Kind,
+    testing::Matcher<Slot> S, testing::Matcher<Evidence::Kind> Kind,
     testing::Matcher<const Symbol&> SymbolMatcher = testing::_) {
   return isEvidenceMatcher(S, Kind, SymbolMatcher);
 }
@@ -76,30 +79,31 @@
   return Results;
 }
 
-TEST(InferAnnotationsTest, NoParams) {
+TEST(CollectEvidenceFromImplementationTest, NoParams) {
   static constexpr llvm::StringRef Src = R"cc(
     void target() {}
   )cc";
   EXPECT_THAT(collectEvidenceFromTargetFunction(Src), IsEmpty());
 }
 
-TEST(InferAnnotationsTest, OneParamUnused) {
+TEST(CollectEvidenceFromImplementationTest, OneParamUnused) {
   static constexpr llvm::StringRef Src = R"cc(
     void target(int *p0) {}
   )cc";
   EXPECT_THAT(collectEvidenceFromTargetFunction(Src), IsEmpty());
 }
 
-TEST(InferAnnotationsTest, OneParamUsedWithoutRestriction) {
+TEST(CollectEvidenceFromImplementationTest, OneParamUsedWithoutRestriction) {
   static constexpr llvm::StringRef Src = R"cc(
     void takesUnknown(int *unknown) {}
 
     void target(int *p0) { takesUnknown(p0); }
   )cc";
-  EXPECT_THAT(collectEvidenceFromTargetFunction(Src), IsEmpty());
+  EXPECT_THAT(collectEvidenceFromTargetFunction(Src),
+              Not(Contains(evidence(_, _, functionNamed("target")))));
 }
 
-TEST(InferAnnotationsTest, Deref) {
+TEST(CollectEvidenceFromImplementationTest, Deref) {
   static constexpr llvm::StringRef Src = R"cc(
     void target(int *p0, int *p1) {
       int a = *p0;
@@ -121,7 +125,7 @@
   EXPECT_THAT(collectEvidenceFromTargetFunction(Src), IsEmpty());
 }
 
-TEST(InferAnnotationsTest, DereferenceBeforeAssignment) {
+TEST(CollectEvidenceFromImplementationTest, DereferenceBeforeAssignment) {
   static constexpr llvm::StringRef Src = R"cc(
     void target(int *p) {
       *p;
@@ -134,7 +138,7 @@
                   evidence(paramSlot(0), Evidence::UNCHECKED_DEREFERENCE)));
 }
 
-TEST(InferAnnotationsTest, DereferenceAfterAssignment) {
+TEST(CollectEvidenceFromImplementationTest, DereferenceAfterAssignment) {
   static constexpr llvm::StringRef Src = R"cc(
     void target(int *p) {
       int i = 1;
@@ -145,7 +149,7 @@
   EXPECT_THAT(collectEvidenceFromTargetFunction(Src), IsEmpty());
 }
 
-TEST(InferAnnotationsTest, DerefOfPtrRef) {
+TEST(CollectEvidenceFromImplementationTest, DerefOfPtrRef) {
   static constexpr llvm::StringRef Src = R"cc(
     void target(int *&p0, int *&p1) {
       int a = *p0;
@@ -159,7 +163,7 @@
                   evidence(paramSlot(0), Evidence::UNCHECKED_DEREFERENCE)));
 }
 
-TEST(InferAnnotationsTest, UnrelatedCondition) {
+TEST(CollectEvidenceFromImplementationTest, UnrelatedCondition) {
   static constexpr llvm::StringRef Src = R"cc(
     void target(int *p0, int *p1, int *p2, bool b) {
       if (b) {
@@ -180,7 +184,7 @@
                   evidence(paramSlot(2), Evidence::UNCHECKED_DEREFERENCE)));
 }
 
-TEST(InferAnnotationsTest, LaterDeref) {
+TEST(CollectEvidenceFromImplementationTest, LaterDeref) {
   static constexpr llvm::StringRef Src = R"cc(
     void target(int *p0) {
       if (p0 == nullptr) {
@@ -196,7 +200,7 @@
                   evidence(paramSlot(0), Evidence::UNCHECKED_DEREFERENCE)));
 }
 
-TEST(InferAnnotationsTest, DerefBeforeGuardedDeref) {
+TEST(CollectEvidenceFromImplementationTest, DerefBeforeGuardedDeref) {
   static constexpr llvm::StringRef Src = R"cc(
     void target(int *p0) {
       int a = *p0;
@@ -210,7 +214,7 @@
                   evidence(paramSlot(0), Evidence::UNCHECKED_DEREFERENCE)));
 }
 
-TEST(InferAnnotationsTest, EarlyReturn) {
+TEST(CollectEvidenceFromImplementationTest, EarlyReturn) {
   static constexpr llvm::StringRef Src = R"cc(
     void target(int *p0) {
       if (!p0) {
@@ -222,7 +226,7 @@
   EXPECT_THAT(collectEvidenceFromTargetFunction(Src), IsEmpty());
 }
 
-TEST(InferAnnotationsTest, UnreachableCode) {
+TEST(CollectEvidenceFromImplementationTest, UnreachableCode) {
   static constexpr llvm::StringRef Src = R"cc(
     void target(int *p0, int *p1, int *p2, int *p3) {
       if (true) {
@@ -244,12 +248,79 @@
                   evidence(paramSlot(0), Evidence::UNCHECKED_DEREFERENCE)));
 }
 
-TEST(InferAnnotationsTest, VariableDeclIgnored) {
+TEST(CollectEvidenceFromImplementationTest, NullableArgPassed) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void callee(int *q);
+    void target(Nullable<int *> p) { callee(p); }
+  )cc";
+  EXPECT_THAT(collectEvidenceFromTargetFunction(Src),
+              Contains(evidence(paramSlot(0), Evidence::NULLABLE_ARGUMENT,
+                                functionNamed("callee"))));
+}
+
+TEST(CollectEvidenceFromImplementationTest, NonnullArgPassed) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void callee(int *q);
+    void target(Nonnull<int *> p) { callee(p); }
+  )cc";
+  EXPECT_THAT(collectEvidenceFromTargetFunction(Src),
+              Contains(evidence(paramSlot(0), Evidence::NONNULL_ARGUMENT,
+                                functionNamed("callee"))));
+}
+
+TEST(CollectEvidenceFromImplementationTest, UnknownArgPassed) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void callee(int *q);
+    void target(int *p) { callee(p); }
+  )cc";
+  EXPECT_THAT(collectEvidenceFromTargetFunction(Src),
+              Contains(evidence(paramSlot(0), Evidence::UNKNOWN_ARGUMENT,
+                                functionNamed("callee"))));
+}
+
+TEST(CollectEvidenceFromImplementationTest, CheckedArgPassed) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void callee(int *q);
+    void target(int *p) {
+      if (p) callee(p);
+    }
+  )cc";
+  EXPECT_THAT(collectEvidenceFromTargetFunction(Src),
+              Contains(evidence(paramSlot(0), Evidence::NONNULL_ARGUMENT,
+                                functionNamed("callee"))));
+}
+
+TEST(CollectEvidenceFromImplementationTest, NullptrPassed) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void callee(int* q);
+    void target() {
+      callee(nullptr);
+      int* p = nullptr;
+      callee(nullptr);
+    }
+  )cc";
+  EXPECT_THAT(
+      collectEvidenceFromTargetFunction(Src),
+      UnorderedElementsAre(evidence(paramSlot(0), Evidence::NULLABLE_ARGUMENT,
+                                    functionNamed("callee")),
+                           evidence(paramSlot(0), Evidence::NULLABLE_ARGUMENT,
+                                    functionNamed("callee"))));
+}
+
+TEST(CollectEvidenceFromImplementationTest, NonPtrArgPassed) {
+  static constexpr llvm::StringRef Src = R"cc(
+    void callee(int q);
+    void target(int p) { callee(p); }
+  )cc";
+  EXPECT_THAT(collectEvidenceFromTargetFunction(Src), IsEmpty());
+}
+
+TEST(CollectEvidenceFromDeclarationTest, VariableDeclIgnored) {
   llvm::StringLiteral Src = "Nullable<int *> target;";
   EXPECT_THAT(collectEvidenceFromTargetDecl(Src), IsEmpty());
 }
 
-TEST(InferAnnotationsTest, FunctionDeclReturnType) {
+TEST(CollectEvidenceFromDeclarationTest, FunctionDeclReturnType) {
   llvm::StringLiteral Src = "Nonnull<int *> target();";
   EXPECT_THAT(
       collectEvidenceFromTargetDecl(Src),
@@ -257,14 +328,14 @@
                            functionNamed("target"))));
 }
 
-TEST(InferAnnotationsTest, FunctionDeclParams) {
+TEST(CollectEvidenceFromDeclarationTest, FunctionDeclParams) {
   llvm::StringLiteral Src = "void target(Nullable<int*>, int*, Nonnull<int*>);";
   EXPECT_THAT(collectEvidenceFromTargetDecl(Src),
               ElementsAre(evidence(paramSlot(0), Evidence::ANNOTATED_NULLABLE),
                           evidence(paramSlot(2), Evidence::ANNOTATED_NONNULL)));
 }
 
-TEST(InferAnnotationsTest, FunctionDeclNonTopLevel) {
+TEST(CollectEvidenceFromDeclarationTest, FunctionDeclNonTopLevel) {
   llvm::StringLiteral Src = "Nonnull<int*>** target(Nullable<int*>*);";
   EXPECT_THAT(collectEvidenceFromTargetDecl(Src), IsEmpty());
 }
diff --git a/nullability/inference/inference.proto b/nullability/inference/inference.proto
index d470b12..56ae3df 100644
--- a/nullability/inference/inference.proto
+++ b/nullability/inference/inference.proto
@@ -60,6 +60,12 @@
 
     // A pointer was dereferenced without being checked for null first.
     UNCHECKED_DEREFERENCE = 3;
+    // A Nullable value was passed as an argument.
+    NULLABLE_ARGUMENT = 4;
+    // A Nonnull value was passed as an argument.
+    NONNULL_ARGUMENT = 5;
+    // A value with Unknown nullability was passed as an argument.
+    UNKNOWN_ARGUMENT = 6;
   }
 }
 
diff --git a/nullability/pointer_nullability.cc b/nullability/pointer_nullability.cc
index bff42e2..084c25c 100644
--- a/nullability/pointer_nullability.cc
+++ b/nullability/pointer_nullability.cc
@@ -5,6 +5,7 @@
 #include "nullability/pointer_nullability.h"
 
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Basic/Specifiers.h"
 #include "llvm/ADT/StringRef.h"
@@ -75,21 +76,27 @@
   initPointerBoolProperty(PointerVal, kNull, NullConstraint, Env);
 }
 
-bool isNullable(const PointerValue &PointerVal, const Environment &Env) {
+bool isNullable(const PointerValue &PointerVal, const Environment &Env,
+                const dataflow::Formula *AdditionalConstraints) {
   auto &A = Env.getDataflowAnalysisContext().arena();
   auto [FromNullable, Null] = getPointerNullState(PointerVal);
-  auto &ForseeablyNull = A.makeAnd(FromNullable.formula(), Null.formula());
-  return !Env.flowConditionImplies(A.makeNot(ForseeablyNull));
+  auto *ForseeablyNull = &A.makeAnd(FromNullable.formula(), Null.formula());
+  if (AdditionalConstraints)
+    ForseeablyNull = &A.makeAnd(*AdditionalConstraints, *ForseeablyNull);
+  return !Env.flowConditionImplies(A.makeNot(*ForseeablyNull));
 }
 
 NullabilityKind getNullability(const dataflow::PointerValue &PointerVal,
-                               const dataflow::Environment &Env) {
+                               const dataflow::Environment &Env,
+                               const dataflow::Formula *AdditionalConstraints) {
   auto &A = Env.getDataflowAnalysisContext().arena();
-  auto [FromNullable, Null] = getPointerNullState(PointerVal);
-  if (Env.flowConditionImplies(A.makeNot(Null.formula())))
+  auto *Null = &getPointerNullState(PointerVal).second.formula();
+  if (AdditionalConstraints) Null = &A.makeAnd(*AdditionalConstraints, *Null);
+  if (Env.flowConditionImplies(A.makeNot(*Null)))
     return NullabilityKind::NonNull;
-  return isNullable(PointerVal, Env) ? NullabilityKind::Nullable
-                                     : NullabilityKind::Unspecified;
+  return isNullable(PointerVal, Env, AdditionalConstraints)
+             ? NullabilityKind::Nullable
+             : NullabilityKind::Unspecified;
 }
 
 }  // namespace clang::tidy::nullability
diff --git a/nullability/pointer_nullability.h b/nullability/pointer_nullability.h
index 10ad9fb..3644148 100644
--- a/nullability/pointer_nullability.h
+++ b/nullability/pointer_nullability.h
@@ -106,14 +106,16 @@
 
 /// Returns true if there is evidence that `PointerVal` may hold a nullptr.
 bool isNullable(const dataflow::PointerValue &PointerVal,
-                const dataflow::Environment &Env);
+                const dataflow::Environment &Env,
+                const dataflow::Formula *AdditionalConstraints = nullptr);
 
 /// Returns the strongest provable assertion we can make about `PointerVal`.
 /// If PointerVal may not be null, returns Nonnull.
 /// If PointerVal may be both null and known-nullability, returns Nullable.
 /// Otherwise, returns Unspecified.
-clang::NullabilityKind getNullability(const dataflow::PointerValue &PointerVal,
-                                      const dataflow::Environment &Env);
+clang::NullabilityKind getNullability(
+    const dataflow::PointerValue &PointerVal, const dataflow::Environment &Env,
+    const dataflow::Formula *AdditionalConstraints = nullptr);
 
 /// Returns the strongest provable assertion we can make about the value of
 /// `E` in `Env`.
diff --git a/nullability/pointer_nullability_test.cc b/nullability/pointer_nullability_test.cc
index cf35fe0..f410358 100644
--- a/nullability/pointer_nullability_test.cc
+++ b/nullability/pointer_nullability_test.cc
@@ -11,43 +11,66 @@
 #include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "clang/Basic/Specifiers.h"
 #include "third_party/llvm/llvm-project/third-party/unittest/googletest/include/gtest/gtest.h"
 
 namespace clang::tidy::nullability {
 namespace {
 
-TEST(NullabilityPropertiesTest, Test) {
-  dataflow::DataflowAnalysisContext DACtx(
-      std::make_unique<dataflow::WatchedLiteralsSolver>());
-  dataflow::Environment Env(DACtx);
-
-  auto &True = DACtx.arena().makeLiteral(true);
-  auto &False = DACtx.arena().makeLiteral(false);
-  auto &False2 = DACtx.arena().makeNot(True);
-
-  auto MakePointer =
-      [&](const dataflow::Formula &FromNullable,
-          const dataflow::Formula &Null) -> dataflow::PointerValue & {
+class NullabilityPropertiesTest : public ::testing::Test {
+ protected:
+  dataflow::PointerValue &makePointer(const dataflow::Formula &FromNullable,
+                                      const dataflow::Formula &Null) {
     auto &P = Env.create<dataflow::PointerValue>(
         DACtx.createStorageLocation(QualType()));
     initPointerNullState(P, Env, &Env.arena().makeBoolValue(FromNullable),
                          &Env.arena().makeBoolValue(Null));
     return P;
-  };
+  }
+
+  dataflow::DataflowAnalysisContext DACtx = dataflow::DataflowAnalysisContext(
+      std::make_unique<dataflow::WatchedLiteralsSolver>());
+  dataflow::Environment Env = dataflow::Environment(DACtx);
+};
+
+TEST_F(NullabilityPropertiesTest, Test) {
+  auto &True = DACtx.arena().makeLiteral(true);
+  auto &False = DACtx.arena().makeLiteral(false);
+  auto &False2 = DACtx.arena().makeNot(True);
 
   EXPECT_TRUE(
-      isNullable(MakePointer(/*FromNullable=*/True, /*Null=*/True), Env));
+      isNullable(makePointer(/*FromNullable=*/True, /*Null=*/True), Env));
   EXPECT_FALSE(
-      isNullable(MakePointer(/*FromNullable=*/True, /*Null=*/False), Env));
+      isNullable(makePointer(/*FromNullable=*/True, /*Null=*/False), Env));
   EXPECT_FALSE(
-      isNullable(MakePointer(/*FromNullable=*/False, /*Null=*/True), Env));
+      isNullable(makePointer(/*FromNullable=*/False, /*Null=*/True), Env));
   EXPECT_FALSE(
-      isNullable(MakePointer(/*FromNullable=*/False, /*Null=*/False), Env));
+      isNullable(makePointer(/*FromNullable=*/False, /*Null=*/False), Env));
 
   EXPECT_FALSE(
-      isNullable(MakePointer(/*FromNullable=*/True, /*Null=*/False2), Env));
+      isNullable(makePointer(/*FromNullable=*/True, /*Null=*/False2), Env));
   EXPECT_FALSE(
-      isNullable(MakePointer(/*FromNullable=*/False2, /*Null=*/True), Env));
+      isNullable(makePointer(/*FromNullable=*/False2, /*Null=*/True), Env));
+}
+
+TEST_F(NullabilityPropertiesTest, IsNullableAdditionalConstraints) {
+  auto &FromNullable = Env.makeAtomicBoolValue().formula();
+  auto &Null = Env.makeAtomicBoolValue().formula();
+  EXPECT_TRUE(isNullable(makePointer(FromNullable, Null), Env));
+
+  auto *NotNull = &DACtx.arena().makeNot(Null);
+  EXPECT_FALSE(isNullable(makePointer(FromNullable, Null), Env, NotNull));
+}
+
+TEST_F(NullabilityPropertiesTest, GetNullabilityAdditionalConstraints) {
+  auto &FromNullable = Env.makeAtomicBoolValue().formula();
+  auto &Null = Env.makeAtomicBoolValue().formula();
+  EXPECT_EQ(getNullability(makePointer(FromNullable, Null), Env),
+            NullabilityKind::Nullable);
+
+  auto *NotNull = &DACtx.arena().makeNot(Null);
+  EXPECT_EQ(getNullability(makePointer(FromNullable, Null), Env, NotNull),
+            NullabilityKind::NonNull);
 }
 
 }  // namespace