Rework PointerNullState APIs
These now return Formulas instead of BoolValues, which drops the requirement
to be atomic bools, and opens the door to true/false becoming Formula primitives
rather than Atoms in the framework (and formula simplification).
The connection between nonnull annotations and the is_null property is now
expressed as a global invariant, so it works properly when is_null is neither
exactly true/false nor unconstrained - i.e. when it's restricted by a symbolic
nullability variable in inference.
PiperOrigin-RevId: 567282695
Change-Id: I2e8ac1c173c8bb1526a357d3eafc08935ec8a2da
diff --git a/nullability/BUILD b/nullability/BUILD
index 0ee6158..7b06d42 100644
--- a/nullability/BUILD
+++ b/nullability/BUILD
@@ -100,6 +100,7 @@
"//nullability/test:__pkg__",
],
deps = [
+ ":type_nullability",
"@llvm-project//clang:analysis",
"@llvm-project//clang:ast",
"@llvm-project//clang:basic",
@@ -112,6 +113,7 @@
srcs = ["pointer_nullability_test.cc"],
deps = [
":pointer_nullability",
+ ":type_nullability",
"@llvm-project//clang:analysis",
"@llvm-project//clang:ast",
"@llvm-project//clang:basic",
diff --git a/nullability/inference/collect_evidence.cc b/nullability/inference/collect_evidence.cc
index 3505d0c..330bf33 100644
--- a/nullability/inference/collect_evidence.cc
+++ b/nullability/inference/collect_evidence.cc
@@ -126,8 +126,7 @@
getPointerValueFromExpr(Target, Env);
if (!DereferencedValue) return;
auto &A = Env.getDataflowAnalysisContext().arena();
- auto &NotIsNull =
- A.makeNot(getPointerNullState(*DereferencedValue).second.formula());
+ auto &NotIsNull = A.makeNot(getPointerNullState(*DereferencedValue).IsNull);
// If the flow conditions already imply the dereferenced value is not null,
// then we don't have any new evidence of a necessary annotation.
diff --git a/nullability/pointer_nullability.cc b/nullability/pointer_nullability.cc
index 2d86787..495b72e 100644
--- a/nullability/pointer_nullability.cc
+++ b/nullability/pointer_nullability.cc
@@ -4,9 +4,12 @@
#include "nullability/pointer_nullability.h"
-#include <utility>
+#include <cassert>
+#include <optional>
+#include "nullability/type_nullability.h"
#include "clang/AST/Type.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"
@@ -18,7 +21,9 @@
using dataflow::AtomicBoolValue;
using dataflow::BoolValue;
+using dataflow::DataflowAnalysisContext;
using dataflow::Environment;
+using dataflow::Formula;
using dataflow::PointerValue;
using dataflow::Value;
@@ -41,41 +46,55 @@
PointerVal.getProperty(kNull) != nullptr;
}
-std::pair<AtomicBoolValue &, AtomicBoolValue &> getPointerNullState(
- const PointerValue &PointerVal) {
+PointerNullState getPointerNullState(const PointerValue &PointerVal) {
auto &FromNullable =
*cast<AtomicBoolValue>(PointerVal.getProperty(kFromNullable));
auto &Null = *cast<AtomicBoolValue>(PointerVal.getProperty(kNull));
- return {FromNullable, Null};
+ return {FromNullable.formula(), Null.formula()};
}
-void initPointerBoolProperty(PointerValue &PointerVal, llvm::StringRef Name,
- BoolValue *BoolVal, Environment &Env) {
- if (PointerVal.getProperty(Name) != nullptr) return;
- // The property must always be a non-null boolean atom.
- if (!isa_and_nonnull<AtomicBoolValue>(BoolVal)) {
- auto &Atom = Env.makeAtomicBoolValue();
- if (BoolVal)
- Env.addToFlowCondition(
- Env.arena().makeEquals(Atom.formula(), BoolVal->formula()));
- BoolVal = &Atom;
+static bool tryCreatePointerNullState(PointerValue &PointerVal,
+ dataflow::Arena &A,
+ const Formula *FromNullable = nullptr,
+ const Formula *IsNull = nullptr) {
+ // TODO: for now we assume that we have both nullability properties, or none.
+ // We'll need to relax this when properties can be independently widened away.
+ if (hasPointerNullState(PointerVal)) return false;
+ if (!FromNullable) FromNullable = &A.makeAtomRef(A.makeAtom());
+ if (!IsNull) IsNull = &A.makeAtomRef(A.makeAtom());
+ PointerVal.setProperty(kFromNullable, A.makeBoolValue(*FromNullable));
+ PointerVal.setProperty(kNull, A.makeBoolValue(*IsNull));
+ return true;
+}
+
+void initPointerNullState(PointerValue &PointerVal,
+ DataflowAnalysisContext &Ctx,
+ std::optional<PointerTypeNullability> Source) {
+ auto &A = Ctx.arena();
+ if (tryCreatePointerNullState(PointerVal, A,
+ Source ? &Source->isNullable(A) : nullptr)) {
+ // The symbolic/nonnull check is not needed for correctness, but it avoids
+ // adding meaningless (false => !null) invariant clauses.
+ // TODO: remove this once such clauses are recognized and dropped.
+ if (Source &&
+ (Source->isSymbolic() || Source == NullabilityKind::NonNull)) {
+ const Formula &IsNull = getPointerNullState(PointerVal).IsNull;
+ Ctx.addInvariant(A.makeImplies(Source->isNonnull(A), A.makeNot(IsNull)));
+ }
}
- PointerVal.setProperty(Name, BoolVal ? *BoolVal : Env.makeAtomicBoolValue());
}
-void initPointerNullState(PointerValue &PointerVal, Environment &Env,
- BoolValue *FromNullableConstraint,
- BoolValue *NullConstraint) {
- initPointerBoolProperty(PointerVal, kFromNullable, FromNullableConstraint,
- Env);
- initPointerBoolProperty(PointerVal, kNull, NullConstraint, Env);
+void initNullPointer(PointerValue &PointerVal, DataflowAnalysisContext &Ctx) {
+ tryCreatePointerNullState(PointerVal, Ctx.arena(),
+ /*FromNullable=*/&Ctx.arena().makeLiteral(true),
+ /*IsNull=*/&Ctx.arena().makeLiteral(true));
}
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());
+ auto *ForseeablyNull = &A.makeAnd(FromNullable, Null);
if (AdditionalConstraints)
ForseeablyNull = &A.makeAnd(*AdditionalConstraints, *ForseeablyNull);
return !Env.flowConditionImplies(A.makeNot(*ForseeablyNull));
@@ -85,7 +104,7 @@
const dataflow::Environment &Env,
const dataflow::Formula *AdditionalConstraints) {
auto &A = Env.getDataflowAnalysisContext().arena();
- auto *Null = &getPointerNullState(PointerVal).second.formula();
+ auto *Null = &getPointerNullState(PointerVal).IsNull;
if (AdditionalConstraints) Null = &A.makeAnd(*AdditionalConstraints, *Null);
if (Env.flowConditionImplies(A.makeNot(*Null)))
return NullabilityKind::NonNull;
diff --git a/nullability/pointer_nullability.h b/nullability/pointer_nullability.h
index 7dfef80..8e156bb 100644
--- a/nullability/pointer_nullability.h
+++ b/nullability/pointer_nullability.h
@@ -13,12 +13,15 @@
// (e.g. a nullptr literal, or a reference to a Nullable-annotated variable)
// If this is false, dereferencing may be safe: we don't know the contract.
-#include <utility>
+#include <optional>
+#include "nullability/type_nullability.h"
#include "clang/AST/ASTContext.h"
#include "clang/AST/ASTDumper.h"
#include "clang/AST/Expr.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/Basic/Specifiers.h"
@@ -39,70 +42,47 @@
// PointerNullabilityAnalysis, not by the dataflow framework.
bool hasPointerNullState(const dataflow::PointerValue &PointerVal);
+/// The properties representing nullness information for a pointer.
+///
+/// We attach these properties to every PointerValue taken by an expression.
+struct PointerNullState {
+ /// Did the pointer come from a known-nullable source?
+ const dataflow::Formula &FromNullable;
+ /// Is the pointer's value null?
+ const dataflow::Formula &IsNull;
+ // These are independent: sources with unknown nullability can yield nullptr!
+};
+
/// Returns the properties representing the nullness information of a pointer.
-///
-/// The first indicates if the pointer's value is from a known-nullable source.
-/// The second indicates if the pointer's value is null.
-///
-/// These are independent: sources with unknown nullability can yield nullptr.
-std::pair<dataflow::AtomicBoolValue &, dataflow::AtomicBoolValue &>
-getPointerNullState(const dataflow::PointerValue &PointerVal);
+PointerNullState getPointerNullState(const dataflow::PointerValue &PointerVal);
-/// Sets the nullness properties on `PointerVal` if not already initialised.
+/// Creates the nullness properties on `PointerVal` if not already initialised.
///
-/// The boolean properties may be constrained by `FromNullableConstraint`
-/// and `NullConstraint`. Otherwise, the properties are set to freshly
-/// created atomic booleans.
-void initPointerNullState(dataflow::PointerValue &PointerVal,
- dataflow::Environment &Env,
- dataflow::BoolValue *FromNullableConstraint = nullptr,
- dataflow::BoolValue *NullConstraint = nullptr);
+/// We call this when the framework produces a PointerValue for an expression.
+/// This ensures that the variable has usable "from nullable" and "is null"
+/// boolean variables, and that they are constrained based on the *original*
+/// source of the PointerValue.
+///
+/// For example:
+/// Unknown<int> *x = makeNullable();
+/// ~~~~~~~~~~~~~~ <-- initPointerNullState(Nullable)
+/// *x;
+/// ~ <-- initPointerNullState(Unknown) - no effect, already initialized
+///
+/// The constraints are added to the context as a non-flow-sensitive invariant,
+/// so the source nullability may not depend on flow-sensitive information.
+///
+/// (We assume that the framework will not provide the same pointer from
+/// different initial sources, so the `Source` nullability is the same
+/// regardless of block evaluation order).
+void initPointerNullState(
+ dataflow::PointerValue &PointerVal, dataflow::DataflowAnalysisContext &Ctx,
+ std::optional<PointerTypeNullability> Source = std::nullopt);
-/// Sets the nullness properties on `PointerVal` representing a nullptr if not
-/// already initialised.
-///
-/// `Known` is constrained to true, `Null` is constrained to true.
-inline void initNullPointer(dataflow::PointerValue &PointerVal,
- dataflow::Environment &Env) {
- initPointerNullState(
- PointerVal, Env,
- /*FromNullableConstraint=*/&Env.getBoolLiteralValue(true),
- /*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, `Null` is constrained to false.
-inline void initNotNullPointer(dataflow::PointerValue &PointerVal,
- dataflow::Environment &Env) {
- initPointerNullState(
- PointerVal, Env,
- /*FromNullableConstraint=*/&Env.getBoolLiteralValue(false),
- /*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, `Null` is unconstrained.
-inline void initNullablePointer(dataflow::PointerValue &PointerVal,
- dataflow::Environment &Env) {
- initPointerNullState(
- PointerVal, Env,
- /*FromNullableConstraint=*/&Env.getBoolLiteralValue(true));
-}
-
-/// Sets the nullness properties on `PointerVal` representing a pointer with
-/// unknown nullability if not already initialised.
-///
-/// `Known` is constrained to false, `Null` is unconstrained.
-inline void initUnknownPointer(dataflow::PointerValue &PointerVal,
- dataflow::Environment &Env) {
- initPointerNullState(
- PointerVal, Env,
- /*FromNullableConstraint=*/&Env.getBoolLiteralValue(false));
-}
+/// Variant of initPointerNullState, where the pointer is guaranteed null.
+/// (This is flow-insensitive, but PointerTypeNullability can't represent it).
+void initNullPointer(dataflow::PointerValue &PointerVal,
+ dataflow::DataflowAnalysisContext &Ctx);
/// Returns true if there is evidence that `PointerVal` may hold a nullptr.
bool isNullable(const dataflow::PointerValue &PointerVal,
diff --git a/nullability/pointer_nullability_analysis.cc b/nullability/pointer_nullability_analysis.cc
index 25fc9ea..2624727 100644
--- a/nullability/pointer_nullability_analysis.cc
+++ b/nullability/pointer_nullability_analysis.cc
@@ -40,6 +40,7 @@
using dataflow::BoolValue;
using dataflow::CFGMatchSwitchBuilder;
using dataflow::Environment;
+using dataflow::Formula;
using dataflow::PointerValue;
using dataflow::StorageLocation;
using dataflow::TransferState;
@@ -264,40 +265,15 @@
void initPointerFromTypeNullability(
PointerValue &PointerVal, const Expr *E,
TransferState<PointerNullabilityLattice> &State) {
- if (auto Nullability = getPointerTypeNullability(E, State.Lattice);
- Nullability.isSymbolic()) {
- auto &Arena = State.Env.getDataflowAnalysisContext().arena();
- auto &Nonnull = Nullability.isNonnull(Arena);
- auto &Nullable = Nullability.isNullable(Arena);
- // from_nullable = nullable
- initPointerNullState(PointerVal, State.Env, &Arena.makeBoolValue(Nullable));
- // nonnull => !is_null
- auto [FromNullable, IsNull] = getPointerNullState(PointerVal);
- State.Env.addToFlowCondition(
- Arena.makeImplies(Nonnull, Arena.makeNot(IsNull.formula())));
- } else {
- // TODO: The above code should also handle concrete nullability correctly.
- // But right now, the formulas it creates are overcomplicated.
- // Eliminate this case once we simplify true/false in formulas, and
- // make addToFlowCondition(true) a no-op.
- switch (Nullability.concrete()) {
- case NullabilityKind::NonNull:
- initNotNullPointer(PointerVal, State.Env);
- break;
- case NullabilityKind::Nullable:
- initNullablePointer(PointerVal, State.Env);
- break;
- default:
- initUnknownPointer(PointerVal, State.Env);
- }
- }
+ initPointerNullState(PointerVal, State.Env.getDataflowAnalysisContext(),
+ getPointerTypeNullability(E, State.Lattice));
}
void transferFlowSensitiveNullPointer(
const Expr *NullPointer, const MatchFinder::MatchResult &,
TransferState<PointerNullabilityLattice> &State) {
if (auto *PointerVal = getPointerValueFromExpr(NullPointer, State.Env)) {
- initNullPointer(*PointerVal, State.Env);
+ initNullPointer(*PointerVal, State.Env.getDataflowAnalysisContext());
}
}
@@ -305,7 +281,8 @@
const Expr *NotNullPointer, const MatchFinder::MatchResult &,
TransferState<PointerNullabilityLattice> &State) {
if (auto *PointerVal = getPointerValueFromExpr(NotNullPointer, State.Env)) {
- initNotNullPointer(*PointerVal, State.Env);
+ initPointerNullState(*PointerVal, State.Env.getDataflowAnalysisContext(),
+ NullabilityKind::NonNull);
}
}
@@ -330,26 +307,24 @@
if (!LHS || !RHS) return;
if (!hasPointerNullState(*LHS) || !hasPointerNullState(*RHS)) return;
- BoolValue &LHSNullVal = getPointerNullState(*LHS).second;
- BoolValue &RHSNullVal = getPointerNullState(*RHS).second;
- auto &LHSNull = LHSNullVal.formula();
- auto &RHSNull = RHSNullVal.formula();
+ auto &LHSNull = getPointerNullState(*LHS).IsNull;
+ auto &RHSNull = getPointerNullState(*RHS).IsNull;
// Special case: Are we comparing against `nullptr`?
// We can avoid modifying the flow condition in this case and simply propagate
// the nullability of the other operand (potentially with a negation).
if (&LHSNull == &A.makeLiteral(true)) {
if (BinaryOp->getOpcode() == BO_EQ)
- State.Env.setValue(*BinaryOp, RHSNullVal);
+ State.Env.setValue(*BinaryOp, A.makeBoolValue(RHSNull));
else
- State.Env.setValue(*BinaryOp, State.Env.makeNot(RHSNullVal));
+ State.Env.setValue(*BinaryOp, A.makeBoolValue(A.makeNot(RHSNull)));
return;
}
if (&RHSNull == &A.makeLiteral(true)) {
if (BinaryOp->getOpcode() == BO_EQ)
- State.Env.setValue(*BinaryOp, LHSNullVal);
+ State.Env.setValue(*BinaryOp, A.makeBoolValue(LHSNull));
else
- State.Env.setValue(*BinaryOp, State.Env.makeNot(LHSNullVal));
+ State.Env.setValue(*BinaryOp, A.makeBoolValue(A.makeNot(LHSNull)));
return;
}
@@ -380,12 +355,13 @@
void transferFlowSensitiveNullCheckImplicitCastPtrToBool(
const Expr *CastExpr, const MatchFinder::MatchResult &,
TransferState<PointerNullabilityLattice> &State) {
+ auto &A = State.Env.arena();
auto *PointerVal =
getPointerValueFromExpr(CastExpr->IgnoreImplicit(), State.Env);
if (!PointerVal) return;
- auto [FromNullable, PointerNull] = getPointerNullState(*PointerVal);
- State.Env.setValue(*CastExpr, State.Env.makeNot(PointerNull));
+ auto Nullability = getPointerNullState(*PointerVal);
+ State.Env.setValue(*CastExpr, A.makeBoolValue(A.makeNot(Nullability.IsNull)));
}
void initializeOutputParameter(const Expr *Arg, dataflow::Environment &Env,
@@ -426,7 +402,8 @@
auto *InnerPointer =
cast<PointerValue>(Env.createValue(ParamTy->getPointeeType()));
- initUnknownPointer(*InnerPointer, Env);
+ initPointerNullState(*InnerPointer, Env.getDataflowAnalysisContext(),
+ NullabilityKind::Unspecified);
Env.setValue(*Loc, *InnerPointer);
}
@@ -857,9 +834,11 @@
FlowSensitiveTransferer(Elt, getASTContext(), State);
}
-static BoolValue &mergeBoolValues(BoolValue &Bool1, const Environment &Env1,
- BoolValue &Bool2, const Environment &Env2,
- Environment &MergedEnv) {
+static const Formula &mergeFormulas(const Formula &Bool1,
+ const Environment &Env1,
+ const Formula &Bool2,
+ const Environment &Env2,
+ Environment &MergedEnv) {
if (&Bool1 == &Bool2) {
return Bool1;
}
@@ -872,11 +851,10 @@
// 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.formula()) &&
- Env2.flowConditionImplies(Bool2.formula())) {
+ if (Env1.flowConditionImplies(Bool1) && Env2.flowConditionImplies(Bool2)) {
MergedEnv.addToFlowCondition(MergedBool);
- } else if (Env1.flowConditionImplies(A.makeNot(Bool1.formula())) &&
- Env2.flowConditionImplies(A.makeNot(Bool2.formula()))) {
+ } else if (Env1.flowConditionImplies(A.makeNot(Bool1)) &&
+ Env2.flowConditionImplies(A.makeNot(Bool2))) {
MergedEnv.addToFlowCondition(A.makeNot(MergedBool));
} else {
// TODO(b/233582219): Flow conditions are not necessarily mutually
@@ -884,13 +862,11 @@
// this section when the patch is commited.
auto FC1 = Env1.getFlowConditionToken();
auto FC2 = Env2.getFlowConditionToken();
- MergedEnv.addToFlowCondition(
- A.makeOr(A.makeAnd(A.makeAtomRef(FC1),
- A.makeEquals(MergedBool, Bool1.formula())),
- A.makeAnd(A.makeAtomRef(FC2),
- A.makeEquals(MergedBool, Bool2.formula()))));
+ MergedEnv.addToFlowCondition(A.makeOr(
+ A.makeAnd(A.makeAtomRef(FC1), A.makeEquals(MergedBool, Bool1)),
+ A.makeAnd(A.makeAtomRef(FC2), A.makeEquals(MergedBool, Bool2))));
}
- return A.makeBoolValue(MergedBool);
+ return MergedBool;
}
bool PointerNullabilityAnalysis::merge(QualType Type, const Value &Val1,
@@ -908,15 +884,22 @@
return false;
}
- auto [FromNullable1, Null1] = getPointerNullState(cast<PointerValue>(Val1));
- auto [FromNullable2, Null2] = getPointerNullState(cast<PointerValue>(Val2));
+ auto Nullability1 = getPointerNullState(cast<PointerValue>(Val1));
+ auto Nullability2 = getPointerNullState(cast<PointerValue>(Val2));
auto &FromNullable =
- mergeBoolValues(FromNullable1, Env1, FromNullable2, Env2, MergedEnv);
- auto &Null = mergeBoolValues(Null1, Env1, Null2, Env2, MergedEnv);
+ mergeFormulas(Nullability1.FromNullable, Env1, Nullability2.FromNullable,
+ Env2, MergedEnv);
+ auto &Null = mergeFormulas(Nullability1.IsNull, Env1, Nullability2.IsNull,
+ Env2, MergedEnv);
- initPointerNullState(cast<PointerValue>(MergedVal), MergedEnv, &FromNullable,
- &Null);
+ initPointerNullState(cast<PointerValue>(MergedVal),
+ MergedEnv.getDataflowAnalysisContext());
+ auto MergedNullability = getPointerNullState(cast<PointerValue>(MergedVal));
+ auto &A = MergedEnv.arena();
+ MergedEnv.addToFlowCondition(
+ A.makeEquals(MergedNullability.FromNullable, FromNullable));
+ MergedEnv.addToFlowCondition(A.makeEquals(MergedNullability.IsNull, Null));
return true;
}
diff --git a/nullability/pointer_nullability_analysis_test.cc b/nullability/pointer_nullability_analysis_test.cc
index ef84a92..61eb15d 100644
--- a/nullability/pointer_nullability_analysis_test.cc
+++ b/nullability/pointer_nullability_analysis_test.cc
@@ -71,21 +71,20 @@
auto *Ret =
dyn_cast_or_null<dataflow::PointerValue>(ExitState.Env.getReturnValue());
ASSERT_NE(Ret, nullptr);
- auto [RetFromNullable, RetNull] = getPointerNullState(*Ret);
+ auto State = getPointerNullState(*Ret);
// The param nullability hasn't been fixed.
EXPECT_EQ(std::nullopt, evaluate(PN.isNonnull(A), ExitState.Env));
EXPECT_EQ(std::nullopt, evaluate(PN.isNullable(A), ExitState.Env));
// Nor has the the nullability of the returned pointer.
- EXPECT_EQ(std::nullopt, evaluate(RetFromNullable.formula(), ExitState.Env));
- EXPECT_EQ(std::nullopt, evaluate(RetNull.formula(), ExitState.Env));
+ EXPECT_EQ(std::nullopt, evaluate(State.FromNullable, ExitState.Env));
+ EXPECT_EQ(std::nullopt, evaluate(State.IsNull, ExitState.Env));
// However, the two are linked as expected.
- EXPECT_EQ(true, evaluate(A.makeImplies(PN.isNonnull(A),
- A.makeNot(RetNull.formula())),
- ExitState.Env));
EXPECT_EQ(true,
- evaluate(A.makeEquals(PN.isNullable(A), RetFromNullable.formula()),
+ evaluate(A.makeImplies(PN.isNonnull(A), A.makeNot(State.IsNull)),
ExitState.Env));
+ EXPECT_EQ(true, evaluate(A.makeEquals(PN.isNullable(A), State.FromNullable),
+ ExitState.Env));
}
} // namespace
diff --git a/nullability/pointer_nullability_test.cc b/nullability/pointer_nullability_test.cc
index f410358..67e47de 100644
--- a/nullability/pointer_nullability_test.cc
+++ b/nullability/pointer_nullability_test.cc
@@ -6,6 +6,7 @@
#include <memory>
+#include "nullability/type_nullability.h"
#include "clang/AST/Type.h"
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/Formula.h"
@@ -19,12 +20,17 @@
class NullabilityPropertiesTest : public ::testing::Test {
protected:
- dataflow::PointerValue &makePointer(const dataflow::Formula &FromNullable,
- const dataflow::Formula &Null) {
+ dataflow::PointerValue &makePointer(PointerTypeNullability N) {
auto &P = Env.create<dataflow::PointerValue>(
DACtx.createStorageLocation(QualType()));
- initPointerNullState(P, Env, &Env.arena().makeBoolValue(FromNullable),
- &Env.arena().makeBoolValue(Null));
+ initPointerNullState(P, DACtx, N);
+ return P;
+ }
+
+ dataflow::PointerValue &makeNullPointer() {
+ auto &P = Env.create<dataflow::PointerValue>(
+ DACtx.createStorageLocation(QualType()));
+ initNullPointer(P, DACtx);
return P;
}
@@ -34,43 +40,46 @@
};
TEST_F(NullabilityPropertiesTest, Test) {
- auto &True = DACtx.arena().makeLiteral(true);
- auto &False = DACtx.arena().makeLiteral(false);
- auto &False2 = DACtx.arena().makeNot(True);
+ auto &A = DACtx.arena();
- EXPECT_TRUE(
- isNullable(makePointer(/*FromNullable=*/True, /*Null=*/True), Env));
- EXPECT_FALSE(
- isNullable(makePointer(/*FromNullable=*/True, /*Null=*/False), Env));
- EXPECT_FALSE(
- isNullable(makePointer(/*FromNullable=*/False, /*Null=*/True), Env));
- EXPECT_FALSE(
- isNullable(makePointer(/*FromNullable=*/False, /*Null=*/False), Env));
+ EXPECT_TRUE(isNullable(makeNullPointer(), Env));
- EXPECT_FALSE(
- isNullable(makePointer(/*FromNullable=*/True, /*Null=*/False2), Env));
- EXPECT_FALSE(
- isNullable(makePointer(/*FromNullable=*/False2, /*Null=*/True), Env));
+ auto &NullableButNotNull = makePointer(NullabilityKind::Nullable);
+ EXPECT_TRUE(isNullable(NullableButNotNull, Env));
+ Env.addToFlowCondition(
+ A.makeNot(getPointerNullState(NullableButNotNull).IsNull));
+ EXPECT_FALSE(isNullable(NullableButNotNull, Env));
+
+ auto &NullableAndNull = makePointer(NullabilityKind::Nullable);
+ Env.addToFlowCondition(getPointerNullState(NullableAndNull).IsNull);
+ EXPECT_TRUE(isNullable(NullableAndNull, Env));
+
+ auto &NonnullAndNotNull = makePointer(NullabilityKind::NonNull);
+ EXPECT_FALSE(isNullable(NonnullAndNotNull, Env));
+ Env.addToFlowCondition(
+ A.makeNot(getPointerNullState(NonnullAndNotNull).IsNull));
+ EXPECT_FALSE(isNullable(NonnullAndNotNull, Env));
+
+ // This is a little surprising: if a pointer comes from a non-null source but
+ // is dynamically discovered to be definitely null, we still don't consider
+ // it nullable.
+ auto &NonnullAndNull = makePointer(NullabilityKind::NonNull);
+ Env.addToFlowCondition(getPointerNullState(NonnullAndNotNull).IsNull);
+ EXPECT_FALSE(isNullable(NonnullAndNull, 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));
+ auto &P = makePointer(NullabilityKind::Nullable);
+ EXPECT_TRUE(isNullable(P, Env));
+ auto *NotNull = &DACtx.arena().makeNot(getPointerNullState(P).IsNull);
+ EXPECT_FALSE(isNullable(P, 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);
+ auto &P = makePointer(NullabilityKind::Nullable);
+ EXPECT_EQ(getNullability(P, Env), NullabilityKind::Nullable);
+ auto *NotNull = &DACtx.arena().makeNot(getPointerNullState(P).IsNull);
+ EXPECT_EQ(getNullability(P, Env, NotNull), NullabilityKind::NonNull);
}
} // namespace
