Refactor NotNull constraint to be Null instead.
This is just a stylistic change to reduce unnecessary negations :)
PiperOrigin-RevId: 487822332
diff --git a/nullability_verification/pointer_nullability.cc b/nullability_verification/pointer_nullability.cc
index 04ba12b..83453df 100644
--- a/nullability_verification/pointer_nullability.cc
+++ b/nullability_verification/pointer_nullability.cc
@@ -19,9 +19,9 @@
/// The nullness information of a pointer is represented by two properties
/// which indicate if a pointer's nullability (i.e., if the pointer can hold
-/// null) is `Known` and if the pointer's value is `NotNull`.
+/// null) is `Known` and if the pointer's value is `Null`.
constexpr llvm::StringLiteral kKnown = "is_known";
-constexpr llvm::StringLiteral kNotNull = "is_notnull";
+constexpr llvm::StringLiteral kNull = "is_null";
NullabilityKind getNullabilityKind(QualType Type, ASTContext& Ctx) {
return Type->getNullability(Ctx).value_or(NullabilityKind::Unspecified);
@@ -36,9 +36,8 @@
std::pair<AtomicBoolValue&, AtomicBoolValue&> getPointerNullState(
const PointerValue& PointerVal, const Environment& Env) {
auto& PointerKnown = *cast<AtomicBoolValue>(PointerVal.getProperty(kKnown));
- auto& PointerNotNull =
- *cast<AtomicBoolValue>(PointerVal.getProperty(kNotNull));
- return {PointerKnown, PointerNotNull};
+ auto& PointerNull = *cast<AtomicBoolValue>(PointerVal.getProperty(kNull));
+ return {PointerKnown, PointerNull};
}
void initPointerBoolProperty(PointerValue& PointerVal, llvm::StringRef Name,
@@ -51,15 +50,15 @@
void initPointerNullState(PointerValue& PointerVal, Environment& Env,
BoolValue* KnownConstraint,
- BoolValue* NotNullConstraint) {
+ BoolValue* NullConstraint) {
initPointerBoolProperty(PointerVal, kKnown, KnownConstraint, Env);
- initPointerBoolProperty(PointerVal, kNotNull, NotNullConstraint, Env);
+ initPointerBoolProperty(PointerVal, kNull, NullConstraint, Env);
}
bool isNullable(const PointerValue& PointerVal, const Environment& Env) {
- auto [PointerKnown, PointerNotNull] = getPointerNullState(PointerVal, Env);
+ auto [PointerKnown, PointerNull] = getPointerNullState(PointerVal, Env);
auto& PointerNotKnownNull =
- Env.makeNot(Env.makeAnd(PointerKnown, Env.makeNot(PointerNotNull)));
+ Env.makeNot(Env.makeAnd(PointerKnown, PointerNull));
return !Env.flowConditionImplies(PointerNotKnownNull);
}
diff --git a/nullability_verification/pointer_nullability.h b/nullability_verification/pointer_nullability.h
index 1f8fc70..9b711bd 100644
--- a/nullability_verification/pointer_nullability.h
+++ b/nullability_verification/pointer_nullability.h
@@ -37,39 +37,39 @@
/// Sets the nullness properties on `PointerVal` if not already initialised.
///
/// The boolean properties may be constrained by specifying `KnownConstraint`
-/// and `NotNullConstraint`. Otherwise, the properties are set to freshly
+/// and `NullConstraint`. Otherwise, the properties are set to freshly
/// created atomic booleans.
void initPointerNullState(dataflow::PointerValue& PointerVal,
dataflow::Environment& Env,
dataflow::BoolValue* KnownConstraint = nullptr,
- dataflow::BoolValue* NotNullConstraint = nullptr);
+ dataflow::BoolValue* NullConstraint = nullptr);
/// Sets the nullness properties on `PointerVal` representing a nullptr if not
/// already initialised.
///
-/// `Known` is constrained to true, `NotNull` is constrained to false.
+/// `Known` is constrained to true, `Null` is constrained to true.
inline void initNullPointer(dataflow::PointerValue& PointerVal,
dataflow::Environment& Env) {
initPointerNullState(PointerVal, Env,
/*KnownConstraint=*/&Env.getBoolLiteralValue(true),
- /*NotNullConstraint=*/&Env.getBoolLiteralValue(false));
+ /*NullConstraint=*/&Env.getBoolLiteralValue(true));
}
/// Sets the nullness properties on `PointerVal` representing a pointer that is
/// not null if not already initialised.
///
-/// `Known` is constrained to true, `NotNull` is constrained to true.
+/// `Known` is constrained to true, `Null` is constrained to false.
inline void initNotNullPointer(dataflow::PointerValue& PointerVal,
dataflow::Environment& Env) {
initPointerNullState(PointerVal, Env,
/*KnownConstraint=*/&Env.getBoolLiteralValue(true),
- /*NotNullConstraint=*/&Env.getBoolLiteralValue(true));
+ /*NullConstraint=*/&Env.getBoolLiteralValue(false));
}
/// Sets the nullness properties on `PointerVal` representing a pointer that is
/// nullable if not already initialised.
///
-/// `Known` is constrained to true, `NotNull` is unconstrained.
+/// `Known` is constrained to true, `Null` is unconstrained.
inline void initNullablePointer(dataflow::PointerValue& PointerVal,
dataflow::Environment& Env) {
initPointerNullState(PointerVal, Env,
@@ -79,7 +79,7 @@
/// Sets the nullness properties on `PointerVal` representing a pointer with
/// unknown nullability if not already initialised.
///
-/// `Known` is constrained to false, `NotNull` is unconstrained.
+/// `Known` is constrained to false, `Null` is unconstrained.
inline void initUnknownPointer(dataflow::PointerValue& PointerVal,
dataflow::Environment& Env) {
initPointerNullState(PointerVal, Env,
diff --git a/nullability_verification/pointer_nullability_analysis.cc b/nullability_verification/pointer_nullability_analysis.cc
index e348993..9bc9720 100644
--- a/nullability_verification/pointer_nullability_analysis.cc
+++ b/nullability_verification/pointer_nullability_analysis.cc
@@ -103,14 +103,14 @@
if (!LHS || !RHS) return;
- auto [LHSKnown, LHSNotNull] = getPointerNullState(*LHS, State.Env);
- auto [RHSKnown, RHSNotNull] = getPointerNullState(*RHS, State.Env);
- auto& LHSKnownNotNull = State.Env.makeAnd(LHSKnown, LHSNotNull);
- auto& RHSKnownNotNull = State.Env.makeAnd(RHSKnown, RHSNotNull);
- auto& LHSKnownNull =
- State.Env.makeAnd(LHSKnown, State.Env.makeNot(LHSNotNull));
- auto& RHSKnownNull =
- State.Env.makeAnd(RHSKnown, State.Env.makeNot(RHSNotNull));
+ auto [LHSKnown, LHSNull] = getPointerNullState(*LHS, State.Env);
+ auto [RHSKnown, RHSNull] = getPointerNullState(*RHS, State.Env);
+ auto& LHSKnownNotNull =
+ State.Env.makeAnd(LHSKnown, State.Env.makeNot(LHSNull));
+ auto& RHSKnownNotNull =
+ State.Env.makeAnd(RHSKnown, State.Env.makeNot(RHSNull));
+ auto& LHSKnownNull = State.Env.makeAnd(LHSKnown, LHSNull);
+ auto& RHSKnownNull = State.Env.makeAnd(RHSKnown, RHSNull);
// nullptr == nullptr
State.Env.addToFlowCondition(State.Env.makeImplication(
@@ -130,10 +130,10 @@
getPointerValueFromExpr(CastExpr->IgnoreImplicit(), State.Env);
if (!PointerVal) return;
- auto [PointerKnown, PointerNotNull] =
+ auto [PointerKnown, PointerNull] =
getPointerNullState(*PointerVal, State.Env);
auto& CastExprLoc = State.Env.createStorageLocation(*CastExpr);
- State.Env.setValue(CastExprLoc, PointerNotNull);
+ State.Env.setValue(CastExprLoc, State.Env.makeNot(PointerNull));
State.Env.setStorageLocation(*CastExpr, CastExprLoc);
}
@@ -226,14 +226,13 @@
return false;
}
- auto [Known1, NotNull1] = getPointerNullState(cast<PointerValue>(Val1), Env1);
- auto [Known2, NotNull2] = getPointerNullState(cast<PointerValue>(Val2), Env2);
+ auto [Known1, Null1] = getPointerNullState(cast<PointerValue>(Val1), Env1);
+ auto [Known2, Null2] = getPointerNullState(cast<PointerValue>(Val2), Env2);
auto& Known = mergeBoolValues(Known1, Env1, Known2, Env2, MergedEnv);
- auto& NotNull = mergeBoolValues(NotNull1, Env1, NotNull2, Env2, MergedEnv);
+ auto& Null = mergeBoolValues(Null1, Env1, Null2, Env2, MergedEnv);
- initPointerNullState(cast<PointerValue>(MergedVal), MergedEnv, &Known,
- &NotNull);
+ initPointerNullState(cast<PointerValue>(MergedVal), MergedEnv, &Known, &Null);
return true;
}
