Add "is_known" synthetic property to null state of PointerValue.
Considering whether a pointer's nullability is known changes the safety criteria for pointer dereferencing - only pointers that are known to be nullable on some path reaching the dereference will be unsafe. Unannotated pointers are treated as nullable pointers which need to be null-checked before dereferencing in this iteration.
PiperOrigin-RevId: 464816394
diff --git a/nullability_verification/pointer_nullability_analysis.cc b/nullability_verification/pointer_nullability_analysis.cc
index 5e1460c..c098111 100644
--- a/nullability_verification/pointer_nullability_analysis.cc
+++ b/nullability_verification/pointer_nullability_analysis.cc
@@ -25,6 +25,7 @@
namespace nullability {
using ast_matchers::MatchFinder;
+using dataflow::AtomicBoolValue;
using dataflow::BoolValue;
using dataflow::Environment;
using dataflow::MatchSwitchBuilder;
@@ -35,51 +36,77 @@
namespace {
+constexpr llvm::StringLiteral kKnown = "is_known";
constexpr llvm::StringLiteral kNotNull = "is_notnull";
-BoolValue& getPointerNotNullProperty(
+std::pair<AtomicBoolValue&, AtomicBoolValue&> getPointerNullState(
const Expr* PointerExpr, TransferState<PointerNullabilityLattice>& State) {
auto* PointerVal =
cast<PointerValue>(State.Env.getValue(*PointerExpr, SkipPast::Reference));
- return *cast<BoolValue>(PointerVal->getProperty(kNotNull));
+ auto& PointerKnown = *cast<AtomicBoolValue>(PointerVal->getProperty(kKnown));
+ auto& PointerNotNull =
+ *cast<AtomicBoolValue>(PointerVal->getProperty(kNotNull));
+ return {PointerKnown, PointerNotNull};
}
-void initPointerNotNullProperty(const Expr* PointerExpr,
- TransferState<PointerNullabilityLattice>& State,
- BoolValue* NotNull = nullptr) {
+void initPointerBoolProperty(PointerValue& PointerVal, llvm::StringRef Name,
+ BoolValue* BoolVal, Environment& Env) {
+ if (PointerVal.getProperty(Name) == nullptr) {
+ PointerVal.setProperty(Name,
+ BoolVal ? *BoolVal : Env.makeAtomicBoolValue());
+ }
+}
+
+/// 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`.
+void initPointerNullState(const Expr* PointerExpr,
+ TransferState<PointerNullabilityLattice>& State,
+ BoolValue* Known, BoolValue* NotNull = nullptr) {
if (auto* PointerVal = cast_or_null<PointerValue>(
State.Env.getValue(*PointerExpr, SkipPast::Reference))) {
- if (PointerVal->getProperty(kNotNull) == nullptr) {
- NotNull = NotNull ? NotNull : &State.Env.makeAtomicBoolValue();
- PointerVal->setProperty(kNotNull, *NotNull);
- }
+ initPointerBoolProperty(*PointerVal, kKnown, Known, State.Env);
+ initPointerBoolProperty(*PointerVal, kNotNull, NotNull, State.Env);
}
}
void transferInitNotNullPointer(
const Expr* NotNullPointer, const MatchFinder::MatchResult&,
TransferState<PointerNullabilityLattice>& State) {
- initPointerNotNullProperty(NotNullPointer, State,
- &State.Env.getBoolLiteralValue(true));
+ initPointerNullState(NotNullPointer, State,
+ /*Known=*/&State.Env.getBoolLiteralValue(true),
+ /*NotNull=*/&State.Env.getBoolLiteralValue(true));
}
void transferInitNullPointer(const Expr* NullPointer,
- const MatchFinder::MatchResult& Result,
+ const MatchFinder::MatchResult&,
TransferState<PointerNullabilityLattice>& State) {
- initPointerNotNullProperty(NullPointer, State,
- &State.Env.getBoolLiteralValue(false));
+ initPointerNullState(NullPointer, State,
+ /*Known=*/&State.Env.getBoolLiteralValue(true),
+ /*NotNull=*/&State.Env.getBoolLiteralValue(false));
}
-void transferInitPointerVariableReference(
+void transferInitNullablePointer(
+ const Expr* NullablePointer,
+ TransferState<PointerNullabilityLattice>& State) {
+ initPointerNullState(NullablePointer, State,
+ /*Known=*/&State.Env.getBoolLiteralValue(true));
+}
+
+void transferInitPointerFromDecl(
const Expr* PointerExpr, const MatchFinder::MatchResult&,
TransferState<PointerNullabilityLattice>& State) {
- initPointerNotNullProperty(PointerExpr, State);
+ // TODO(wyt): Implement processing of nullability annotations. The current
+ // implementation treats unnannotated pointers as nullable.
+ transferInitNullablePointer(PointerExpr, State);
}
void transferPointerAccess(const Expr* PointerExpr,
TransferState<PointerNullabilityLattice>& State) {
- auto& PointerNotNull = getPointerNotNullProperty(PointerExpr, State);
- if (!State.Env.flowConditionImplies(PointerNotNull)) {
+ auto [PointerKnown, PointerNotNull] = getPointerNullState(PointerExpr, State);
+ auto& PointerNotKnownNull = State.Env.makeNot(
+ State.Env.makeAnd(PointerKnown, State.Env.makeNot(PointerNotNull)));
+ if (!State.Env.flowConditionImplies(PointerNotKnownNull)) {
State.Lattice.addViolation(PointerExpr);
}
}
@@ -91,7 +118,7 @@
}
void transferMemberExprInvolvingPointers(
- const MemberExpr* MemberExpr, const MatchFinder::MatchResult&,
+ const MemberExpr* MemberExpr, const MatchFinder::MatchResult& Result,
TransferState<PointerNullabilityLattice>& State) {
if (MemberExpr->isArrow()) {
// Base expr is a pointer, check that (->) access is safe
@@ -99,10 +126,13 @@
}
if (MemberExpr->getType()->isAnyPointerType()) {
// Accessed member is a pointer, initialise its nullability
- initPointerNotNullProperty(MemberExpr, State);
+ transferInitPointerFromDecl(MemberExpr, Result, State);
}
}
+// TODO(wyt): Implement promotion of nullability knownness for initially unknown
+// pointers when there is evidence that it is nullable, for example when the
+// pointer is compared to nullptr, or casted to boolean.
void transferNullCheckComparison(
const BinaryOperator* BinaryOp, const MatchFinder::MatchResult& result,
TransferState<PointerNullabilityLattice>& State) {
@@ -119,27 +149,31 @@
? State.Env.makeNot(PointerComparison)
: PointerComparison;
- auto& LHSNotNull = getPointerNotNullProperty(BinaryOp->getLHS(), State);
- auto& RHSNotNull = getPointerNotNullProperty(BinaryOp->getRHS(), State);
+ auto [LHSKnown, LHSNotNull] = getPointerNullState(BinaryOp->getLHS(), State);
+ auto [RHSKnown, RHSNotNull] = getPointerNullState(BinaryOp->getRHS(), State);
+ 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));
- // !LHS && !RHS => LHS == RHS
+ // nullptr == nullptr
State.Env.addToFlowCondition(State.Env.makeImplication(
- State.Env.makeAnd(State.Env.makeNot(LHSNotNull),
- State.Env.makeNot(RHSNotNull)),
- PointerEQ));
- // !LHS && RHS => LHS != RHS
+ State.Env.makeAnd(LHSKnownNull, RHSKnownNull), PointerEQ));
+ // nullptr != notnull
State.Env.addToFlowCondition(State.Env.makeImplication(
- State.Env.makeAnd(State.Env.makeNot(LHSNotNull), RHSNotNull), PointerNE));
- // LHS && !RHS => LHS != RHS
+ State.Env.makeAnd(LHSKnownNull, RHSKnownNotNull), PointerNE));
+ // notnull != nullptr
State.Env.addToFlowCondition(State.Env.makeImplication(
- State.Env.makeAnd(LHSNotNull, State.Env.makeNot(RHSNotNull)), PointerNE));
+ State.Env.makeAnd(LHSKnownNotNull, RHSKnownNull), PointerNE));
}
void transferNullCheckImplicitCastPtrToBool(
const Expr* CastExpr, const MatchFinder::MatchResult&,
TransferState<PointerNullabilityLattice>& State) {
- auto& PointerNotNull =
- getPointerNotNullProperty(CastExpr->IgnoreImplicit(), State);
+ auto [PointerKnown, PointerNotNull] =
+ getPointerNullState(CastExpr->IgnoreImplicit(), State);
auto& CastExprLoc = State.Env.createStorageLocation(*CastExpr);
State.Env.setValue(CastExprLoc, PointerNotNull);
State.Env.setStorageLocation(*CastExpr, CastExprLoc);
@@ -148,8 +182,7 @@
auto buildTransferer() {
return MatchSwitchBuilder<TransferState<PointerNullabilityLattice>>()
// Handles initialization of the null states of pointers
- .CaseOf<Expr>(isPointerVariableReference(),
- transferInitPointerVariableReference)
+ .CaseOf<Expr>(isPointerVariableReference(), transferInitPointerFromDecl)
.CaseOf<Expr>(isCXXThisExpr(), transferInitNotNullPointer)
.CaseOf<Expr>(isAddrOf(), transferInitNotNullPointer)
.CaseOf<Expr>(isNullPointerLiteral(), transferInitNullPointer)
