[nullabiltiy] Use `proves()` and `assume()` instead of deprecated synonyms.

PiperOrigin-RevId: 577096788
Change-Id: I1c063682252e5bf09c69ae3edff0fe529890a486

nullability/inference/collect_evidence.cc

diff --git a/nullability/inference/collect_evidence.cc b/nullability/inference/collect_evidence.cc
index 6cf2abf..669e4bb 100644
--- a/nullability/inference/collect_evidence.cc
+++ b/nullability/inference/collect_evidence.cc
@@ -140,7 +140,7 @@
 
   // If the flow conditions already imply that Value is not null, then we don't
   // have any new evidence of a necessary annotation.
-  if (Env.flowConditionImplies(NotIsNull)) return;
+  if (Env.proves(NotIsNull)) return;
 
   // Otherwise, if an inferable slot being annotated Nonnull would imply that
   // Value is not null, then we have evidence suggesting that slot should be
@@ -150,7 +150,7 @@
   for (auto &[Nullability, Slot] : InferableSlots) {
     auto &SlotNonnullImpliesValueNonnull =
         A.makeImplies(Nullability.isNonnull(A), NotIsNull);
-    if (Env.flowConditionImplies(SlotNonnullImpliesValueNonnull))
+    if (Env.proves(SlotNonnullImpliesValueNonnull))
       Emit(*Env.getCurrentFunc(), Slot, EvidenceKind, Loc);
   }
 }

nullability/pointer_nullability.cc

diff --git a/nullability/pointer_nullability.cc b/nullability/pointer_nullability.cc
index 8235860..83ee3fb 100644
--- a/nullability/pointer_nullability.cc
+++ b/nullability/pointer_nullability.cc
@@ -122,7 +122,7 @@
   if (AdditionalConstraints)
     ForseeablyNull = &A.makeAnd(*ForseeablyNull, *AdditionalConstraints);
 
-  return !Env.flowConditionImplies(A.makeNot(*ForseeablyNull));
+  return Env.allows(*ForseeablyNull);
 }
 
 NullabilityKind getNullability(const dataflow::PointerValue &PointerVal,
@@ -131,8 +131,7 @@
   auto &A = Env.getDataflowAnalysisContext().arena();
   if (auto *Null = getPointerNullState(PointerVal).IsNull) {
     if (AdditionalConstraints) Null = &A.makeAnd(*AdditionalConstraints, *Null);
-    if (Env.flowConditionImplies(A.makeNot(*Null)))
-      return NullabilityKind::NonNull;
+    if (Env.proves(A.makeNot(*Null))) return NullabilityKind::NonNull;
   }
   return isNullable(PointerVal, Env, AdditionalConstraints)
              ? NullabilityKind::Nullable

nullability/pointer_nullability_analysis.cc

diff --git a/nullability/pointer_nullability_analysis.cc b/nullability/pointer_nullability_analysis.cc
index 3791a87..cab631f 100644
--- a/nullability/pointer_nullability_analysis.cc
+++ b/nullability/pointer_nullability_analysis.cc
@@ -395,13 +395,12 @@
                         : PointerComparison;
 
   // nullptr == nullptr
-  State.Env.addToFlowCondition(
-      A.makeImplies(A.makeAnd(*LHSNull, *RHSNull), PointerEQ));
+  State.Env.assume(A.makeImplies(A.makeAnd(*LHSNull, *RHSNull), PointerEQ));
   // nullptr != notnull
-  State.Env.addToFlowCondition(
+  State.Env.assume(
       A.makeImplies(A.makeAnd(*LHSNull, A.makeNot(*RHSNull)), PointerNE));
   // notnull != nullptr
-  State.Env.addToFlowCondition(
+  State.Env.assume(
       A.makeImplies(A.makeAnd(A.makeNot(*LHSNull), *RHSNull), PointerNE));
 }
 
@@ -955,18 +954,17 @@
   // path taken - this simplifies the flow condition tracked in `MergedEnv`.
   // Otherwise, information about which path was taken is used to associate
   // `MergedBool` with `Bool1` and `Bool2`.
-  if (Env1.flowConditionImplies(*Bool1) && Env2.flowConditionImplies(*Bool2)) {
-    MergedEnv.addToFlowCondition(MergedBool);
-  } else if (Env1.flowConditionImplies(A.makeNot(*Bool1)) &&
-             Env2.flowConditionImplies(A.makeNot(*Bool2))) {
-    MergedEnv.addToFlowCondition(A.makeNot(MergedBool));
+  if (Env1.proves(*Bool1) && Env2.proves(*Bool2)) {
+    MergedEnv.assume(MergedBool);
+  } else if (Env1.proves(A.makeNot(*Bool1)) && Env2.proves(A.makeNot(*Bool2))) {
+    MergedEnv.assume(A.makeNot(MergedBool));
   } else {
     // TODO(b/233582219): Flow conditions are not necessarily mutually
     // exclusive, a fix is in order: https://reviews.llvm.org/D130270. Update
     // this section when the patch is commited.
     auto FC1 = Env1.getFlowConditionToken();
     auto FC2 = Env2.getFlowConditionToken();
-    MergedEnv.addToFlowCondition(A.makeOr(
+    MergedEnv.assume(A.makeOr(
         A.makeAnd(A.makeAtomRef(FC1), A.makeEquals(MergedBool, *Bool1)),
         A.makeAnd(A.makeAtomRef(FC2), A.makeEquals(MergedBool, *Bool2))));
   }
@@ -1006,15 +1004,14 @@
   if (auto *FromNullable =
           mergeFormulas(Nullability1.FromNullable, Env1,
                         Nullability2.FromNullable, Env2, MergedEnv))
-    MergedEnv.addToFlowCondition(
+    MergedEnv.assume(
         A.makeEquals(*MergedNullability.FromNullable, *FromNullable));
   else
     forgetFromNullable(MergedPointerVal, Ctx);
 
   if (auto *Null = mergeFormulas(Nullability1.IsNull, Env1, Nullability2.IsNull,
                                  Env2, MergedEnv))
-    MergedEnv.addToFlowCondition(
-        A.makeEquals(*MergedNullability.IsNull, *Null));
+    MergedEnv.assume(A.makeEquals(*MergedNullability.IsNull, *Null));
   else
     forgetIsNull(MergedPointerVal, Ctx);
 

nullability/pointer_nullability_analysis_test.cc

diff --git a/nullability/pointer_nullability_analysis_test.cc b/nullability/pointer_nullability_analysis_test.cc
index 1bc46f8..d19943a 100644
--- a/nullability/pointer_nullability_analysis_test.cc
+++ b/nullability/pointer_nullability_analysis_test.cc
@@ -33,8 +33,8 @@
 
 std::optional<bool> evaluate(const dataflow::Formula &B,
                              dataflow::Environment &Env) {
-  if (Env.flowConditionImplies(B)) return true;
-  if (Env.flowConditionImplies(Env.arena().makeNot(B))) return false;
+  if (Env.proves(B)) return true;
+  if (Env.proves(Env.arena().makeNot(B))) return false;
   return std::nullopt;
 }
 

nullability/pointer_nullability_test.cc

diff --git a/nullability/pointer_nullability_test.cc b/nullability/pointer_nullability_test.cc
index 9060082..ffe1f22 100644
--- a/nullability/pointer_nullability_test.cc
+++ b/nullability/pointer_nullability_test.cc
@@ -49,7 +49,7 @@
     EXPECT_TRUE(isNullable(NullableButNotNull, Env));
     auto *IsNull = getPointerNullState(NullableButNotNull).IsNull;
     ASSERT_NE(IsNull, nullptr);
-    Env.addToFlowCondition(A.makeNot(*IsNull));
+    Env.assume(A.makeNot(*IsNull));
     EXPECT_FALSE(isNullable(NullableButNotNull, Env));
   }
 
@@ -57,7 +57,7 @@
     auto &NullableAndNull = makePointer(NullabilityKind::Nullable);
     auto *IsNull = getPointerNullState(NullableAndNull).IsNull;
     ASSERT_NE(IsNull, nullptr);
-    Env.addToFlowCondition(*IsNull);
+    Env.assume(*IsNull);
     EXPECT_TRUE(isNullable(NullableAndNull, Env));
   }
 
@@ -66,7 +66,7 @@
     EXPECT_FALSE(isNullable(NonnullAndNotNull, Env));
     auto *IsNull = getPointerNullState(NonnullAndNotNull).IsNull;
     ASSERT_NE(IsNull, nullptr);
-    Env.addToFlowCondition(A.makeNot(*IsNull));
+    Env.assume(A.makeNot(*IsNull));
     EXPECT_FALSE(isNullable(NonnullAndNotNull, Env));
   }
 
@@ -77,7 +77,7 @@
     auto &NonnullAndNull = makePointer(NullabilityKind::NonNull);
     auto *IsNull = getPointerNullState(NonnullAndNull).IsNull;
     ASSERT_NE(IsNull, nullptr);
-    Env.addToFlowCondition(*IsNull);
+    Env.assume(*IsNull);
     EXPECT_FALSE(isNullable(NonnullAndNull, Env));
   }
 }