[nullabiltiy] Use `proves()` and `assume()` instead of deprecated synonyms.
PiperOrigin-RevId: 577096788
Change-Id: I1c063682252e5bf09c69ae3edff0fe529890a486
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);
}
}
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
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);
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;
}
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));
}
}
