All nullability vectors can now store symbolic nullability
This means symbolic nullability fully participates in our non-flow-sensitive
type analysis.
This opens the door to inferring non-top-level nullability slots (e.g.
params of type `vector<int*>`), although actually binding variables to those
slots is not yet implemented.
Moreover it gives us a way to describe potential "nullability casts" uniformly across verification + inference. (Verification checks these, inference uses these to identify safety conditions). These are captured by the nullvec of the source, the nullvec of the target, and the nullability of the PointerValue if applicable (to implement exceptions like "if pointer is provably nonnull, allow cast from nullable<T> to nonnull<T>".
In inference, either the source or the target nullabilty may have symbolic entries.
While I had envisioned nullvec entries always being (nonnull, nullable) pairs of
BoolValues, this proved too unergonomic.
Instead the new PointerTypeNullability class is explicitly either a concrete
nonnull/nullable/unspecifed state, or a symbolic nullability.
PiperOrigin-RevId: 549175681
Change-Id: I9d10f8c44faaade2a35ca6ea138845c5d71c819f
diff --git a/nullability/BUILD b/nullability/BUILD
index 7abc7b6..fe0a564 100644
--- a/nullability/BUILD
+++ b/nullability/BUILD
@@ -126,6 +126,7 @@
],
deps = [
"@absl//absl/log:check",
+ "@llvm-project//clang:analysis",
"@llvm-project//clang:ast",
"@llvm-project//clang:basic",
"@llvm-project//llvm:Support",
diff --git a/nullability/inference/collect_evidence.cc b/nullability/inference/collect_evidence.cc
index ac788b6..75fcb65 100644
--- a/nullability/inference/collect_evidence.cc
+++ b/nullability/inference/collect_evidence.cc
@@ -116,7 +116,7 @@
// any one of which would be sufficient if annotated Nonnull.
for (auto &[Nullability, Slot] : InferrableSlots) {
auto &SlotNonnullImpliesDerefValueNonnull =
- A.makeImplies(Nullability.Nonnull->formula(), NotIsNull);
+ A.makeImplies(Nullability.isNonnull(A), NotIsNull);
if (Env.flowConditionImplies(SlotNonnullImpliesDerefValueNonnull))
Emit(*Env.getCurrentFunc(), Slot, Evidence::UNCHECKED_DEREFERENCE);
}
@@ -162,10 +162,9 @@
dataflow::Arena &A = Env.getDataflowAnalysisContext().arena();
const dataflow::Formula *CallerSlotsUnknown = &A.makeLiteral(true);
for (auto &[Nullability, Slot] : InferrableCallerSlots) {
- CallerSlotsUnknown =
- &A.makeAnd(*CallerSlotsUnknown,
- A.makeAnd(A.makeNot(Nullability.Nullable->formula()),
- A.makeNot(Nullability.Nonnull->formula())));
+ CallerSlotsUnknown = &A.makeAnd(
+ *CallerSlotsUnknown, A.makeAnd(A.makeNot(Nullability.isNullable(A)),
+ A.makeNot(Nullability.isNonnull(A))));
}
NullabilityKind ArgNullability =
@@ -198,7 +197,7 @@
std::optional<Evidence::Kind> evidenceKindFromDeclaredType(QualType T) {
if (!T.getNonReferenceType()->isPointerType()) return std::nullopt;
auto Nullability = getNullabilityAnnotationsFromType(T);
- switch (Nullability.front()) {
+ switch (Nullability.front().concrete()) {
default:
return std::nullopt;
case NullabilityKind::NonNull:
diff --git a/nullability/pointer_nullability_analysis.cc b/nullability/pointer_nullability_analysis.cc
index c6b97ff..13d42c4 100644
--- a/nullability/pointer_nullability_analysis.cc
+++ b/nullability/pointer_nullability_analysis.cc
@@ -6,6 +6,7 @@
#include <optional>
#include <string>
+#include <utility>
#include <vector>
#include "absl/log/check.h"
@@ -22,6 +23,7 @@
#include "clang/AST/Type.h"
#include "clang/ASTMatchers/ASTMatchFinder.h"
#include "clang/ASTMatchers/ASTMatchers.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
#include "clang/Analysis/FlowSensitive/CFGMatchSwitch.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/Analysis/FlowSensitive/Value.h"
@@ -233,39 +235,51 @@
});
}
-NullabilityKind getPointerNullability(const Expr *E,
- PointerNullabilityAnalysis::Lattice &L) {
- QualType ExprType = E->getType();
- std::optional<NullabilityKind> Nullability = ExprType->getNullability();
+PointerTypeNullability getPointerTypeNullability(
+ const Expr *E, PointerNullabilityAnalysis::Lattice &L) {
+ // TODO: handle this in non-flow-sensitive transfer instead
+ if (auto FromClang = E->getType()->getNullability();
+ FromClang && *FromClang != NullabilityKind::Unspecified)
+ return *FromClang;
- // If the expression's type does not contain nullability information, it may
- // be a template instantiation. Look up the nullability in the
- // `ExprToNullability` map.
- if (Nullability.value_or(NullabilityKind::Unspecified) ==
- NullabilityKind::Unspecified) {
- if (auto MaybeNullability = L.getExprNullability(E)) {
- if (!MaybeNullability->empty()) {
- // Return the nullability of the topmost pointer in the type.
- Nullability = (*MaybeNullability)[0];
- }
- }
+ if (const auto *NonFlowSensitive = L.getExprNullability(E)) {
+ if (!NonFlowSensitive->empty())
+ // Return the nullability of the topmost pointer in the type.
+ return NonFlowSensitive->front();
}
- return Nullability.value_or(NullabilityKind::Unspecified);
+
+ return NullabilityKind::Unspecified;
}
-void initPointerFromAnnotations(
+void initPointerFromTypeNullability(
PointerValue &PointerVal, const Expr *E,
TransferState<PointerNullabilityLattice> &State) {
- NullabilityKind Nullability = getPointerNullability(E, State.Lattice);
- switch (Nullability) {
- case NullabilityKind::NonNull:
- initNotNullPointer(PointerVal, State.Env);
- break;
- case NullabilityKind::Nullable:
- initNullablePointer(PointerVal, State.Env);
- break;
- default:
- initUnknownPointer(PointerVal, State.Env);
+ 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);
+ }
}
}
@@ -285,35 +299,14 @@
}
}
-const PointerTypeNullability *getOverriddenNullability(
- const Expr *E, PointerNullabilityLattice &Lattice) {
- if (const auto *DRE = dyn_cast<DeclRefExpr>(E))
- return Lattice.getDeclNullability(DRE->getDecl());
- if (const auto *ME = dyn_cast<MemberExpr>(E))
- return Lattice.getDeclNullability(ME->getMemberDecl());
- return nullptr;
-}
-
void transferFlowSensitivePointer(
const Expr *PointerExpr, const MatchFinder::MatchResult &Result,
TransferState<PointerNullabilityLattice> &State) {
- auto &Env = State.Env;
- auto &A = Env.arena();
- if (auto *PointerVal = getPointerValueFromExpr(PointerExpr, Env)) {
- if (auto *Override = getOverriddenNullability(PointerExpr, State.Lattice)) {
- // from_nullable = nullable
- initPointerNullState(*PointerVal, Env, Override->Nullable);
- // nonnull => !is_null
- auto [FromNullable, IsNull] = getPointerNullState(*PointerVal);
- Env.addToFlowCondition(A.makeImplies(Override->Nonnull->formula(),
- A.makeNot(IsNull.formula())));
- } else {
- initPointerFromAnnotations(*PointerVal, PointerExpr, State);
- }
- }
+ if (auto *PointerVal = getPointerValueFromExpr(PointerExpr, State.Env))
+ initPointerFromTypeNullability(*PointerVal, PointerExpr, State);
}
-// TODO(b/233582219): Implement promotion of nullability knownness for initially
+// TODO(b/233582219): Implement promotion of nullability 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 transferFlowSensitiveNullCheckComparison(
@@ -394,7 +387,7 @@
PointerVal =
cast<PointerValue>(State.Env.createValue(CallExpr->getType()));
}
- initPointerFromAnnotations(*PointerVal, CallExpr, State);
+ initPointerFromTypeNullability(*PointerVal, CallExpr, State);
if (Loc != nullptr)
State.Env.setValue(*Loc, *PointerVal);
@@ -405,11 +398,26 @@
}
}
+// If nullability for the decl D has been overridden, patch N to reflect it.
+// (N is the nullability of an access to D).
+void overrideNullabilityFromDecl(const ValueDecl *D,
+ PointerNullabilityLattice &Lattice,
+ TypeNullability &N) {
+ // For now, overrides are always for pointer values only, and override only
+ // the top-level nullability.
+ if (auto *PN = Lattice.getDeclNullability(D)) {
+ CHECK(!N.empty());
+ N.front() = *PN;
+ }
+}
+
void transferNonFlowSensitiveDeclRefExpr(
const DeclRefExpr *DRE, const MatchFinder::MatchResult &MR,
TransferState<PointerNullabilityLattice> &State) {
computeNullability(DRE, State, [&] {
- return getNullabilityAnnotationsFromType(DRE->getType());
+ auto Nullability = getNullabilityAnnotationsFromType(DRE->getType());
+ overrideNullabilityFromDecl(DRE->getDecl(), State.Lattice, Nullability);
+ return Nullability;
});
}
@@ -429,8 +437,11 @@
if (ME->hasPlaceholderType(BuiltinType::BoundMember)) {
MemberType = ME->getMemberDecl()->getType();
}
- return substituteNullabilityAnnotationsInClassTemplate(
+ auto Nullability = substituteNullabilityAnnotationsInClassTemplate(
MemberType, BaseNullability, ME->getBase()->getType());
+ overrideNullabilityFromDecl(ME->getMemberDecl(), State.Lattice,
+ Nullability);
+ return Nullability;
});
}
@@ -726,10 +737,7 @@
PointerTypeNullability PointerNullabilityAnalysis::assignNullabilityVariable(
const ValueDecl *D, dataflow::Arena &A) {
auto [It, Inserted] = NFS.DeclTopLevelNullability.try_emplace(D);
- if (Inserted) {
- It->second.Nonnull = &A.makeAtomValue();
- It->second.Nullable = &A.makeAtomValue();
- }
+ if (Inserted) It->second = PointerTypeNullability::createSymbolic(A);
return It->second;
}
diff --git a/nullability/pointer_nullability_analysis.h b/nullability/pointer_nullability_analysis.h
index f739683..ca94c8a 100644
--- a/nullability/pointer_nullability_analysis.h
+++ b/nullability/pointer_nullability_analysis.h
@@ -5,6 +5,8 @@
#ifndef CRUBIT_NULLABILITY_POINTER_NULLABILITY_ANALYSIS_H_
#define CRUBIT_NULLABILITY_POINTER_NULLABILITY_ANALYSIS_H_
+#include <utility>
+
#include "nullability/pointer_nullability_lattice.h"
#include "nullability/type_nullability.h"
#include "clang/AST/ASTContext.h"
@@ -14,6 +16,7 @@
#include "clang/Analysis/FlowSensitive/CFGMatchSwitch.h"
#include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Value.h"
namespace clang {
@@ -50,15 +53,17 @@
// from_nullable = false
//
// However, if we bind p's nullability to a variable:
- // [p_nonnull, p_nullable] = assignNullabilityVariable(p)
+ // pn = assignNullabilityVariable(p)
// Then the flow condition at dereference includes:
- // from_nullable = p_nullable
- // p_nonnull => !is_null
+ // from_nullable = pn.Nullable
+ // pn.Nonnull => !is_null
// Logically connecting dereferenced values and possible invariants on p
// allows us to infer p's proper annotations (here: Nonnull).
//
// For now, only the top-level nullability is assigned, and the returned
// variables are only associated with direct reads of pointer values from D.
+ //
+ // The returned nullability is guaranteed to be symbolic.
PointerTypeNullability assignNullabilityVariable(const ValueDecl *D,
dataflow::Arena &);
diff --git a/nullability/pointer_nullability_analysis_test.cc b/nullability/pointer_nullability_analysis_test.cc
index 8190d97..ef84a92 100644
--- a/nullability/pointer_nullability_analysis_test.cc
+++ b/nullability/pointer_nullability_analysis_test.cc
@@ -62,7 +62,7 @@
auto &A = DACtx.arena();
auto CFCtx = dataflow::ControlFlowContext::build(*Target);
PointerNullabilityAnalysis Analysis(AST.context());
- auto [PNonnull, PNullable] = Analysis.assignNullabilityVariable(P, A);
+ auto PN = Analysis.assignNullabilityVariable(P, A);
auto ExitState = std::move(
*cantFail(dataflow::runDataflowAnalysis(
*CFCtx, Analysis, dataflow::Environment(DACtx, *Target)))
@@ -74,18 +74,18 @@
auto [RetFromNullable, RetNull] = getPointerNullState(*Ret);
// The param nullability hasn't been fixed.
- EXPECT_EQ(std::nullopt, evaluate(PNonnull->formula(), ExitState.Env));
- EXPECT_EQ(std::nullopt, evaluate(PNullable->formula(), ExitState.Env));
+ 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));
// However, the two are linked as expected.
- EXPECT_EQ(true, evaluate(A.makeImplies(PNonnull->formula(),
+ EXPECT_EQ(true, evaluate(A.makeImplies(PN.isNonnull(A),
A.makeNot(RetNull.formula())),
ExitState.Env));
- EXPECT_EQ(true, evaluate(A.makeEquals(PNullable->formula(),
- RetFromNullable.formula()),
- ExitState.Env));
+ EXPECT_EQ(true,
+ evaluate(A.makeEquals(PN.isNullable(A), RetFromNullable.formula()),
+ ExitState.Env));
}
} // namespace
diff --git a/nullability/pointer_nullability_lattice.h b/nullability/pointer_nullability_lattice.h
index e8e0226..9a70c8e 100644
--- a/nullability/pointer_nullability_lattice.h
+++ b/nullability/pointer_nullability_lattice.h
@@ -23,6 +23,8 @@
struct NonFlowSensitiveState {
absl::flat_hash_map<const Expr *, TypeNullability> ExprToNullability;
// Overridden symbolic nullability for pointer-typed decls.
+ // These are set by PointerNullabilityAnalysis::assignNullabilityVariable,
+ // and take precedence over the declared type.
absl::flat_hash_map<const ValueDecl *, PointerTypeNullability>
DeclTopLevelNullability;
};
diff --git a/nullability/test/BUILD b/nullability/test/BUILD
index ac6d664..d8aab60 100644
--- a/nullability/test/BUILD
+++ b/nullability/test/BUILD
@@ -213,6 +213,11 @@
],
)
+nullability_test(
+ name = "symbolic_nullability",
+ srcs = ["symbolic_nullability.cc"],
+)
+
cc_test(
name = "templates",
srcs = ["templates.cc"],
diff --git a/nullability/test/nullability_test.cc b/nullability/test/nullability_test.cc
index 7050b4c..eb590a2 100644
--- a/nullability/test/nullability_test.cc
+++ b/nullability/test/nullability_test.cc
@@ -40,14 +40,17 @@
#include "clang/AST/ASTTypeTraits.h"
#include "clang/AST/CanonicalType.h"
#include "clang/AST/Decl.h"
+#include "clang/AST/DeclTemplate.h"
#include "clang/AST/Expr.h"
#include "clang/AST/RecursiveASTVisitor.h"
#include "clang/AST/Type.h"
#include "clang/AST/TypeLoc.h"
#include "clang/Analysis/CFG.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
#include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
#include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "clang/Basic/Diagnostic.h"
#include "clang/Basic/LLVM.h"
@@ -59,7 +62,7 @@
#include "clang/Tooling/CompilationDatabase.h"
#include "clang/Tooling/StandaloneExecution.h"
#include "clang/Tooling/Tooling.h"
-#include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/SmallString.h"
#include "llvm/ADT/StringExtras.h"
#include "llvm/ADT/StringRef.h"
@@ -113,9 +116,8 @@
}
void diagnoseType(SourceLocation Call, SourceRange Arg, CanQualType WantCanon,
- CanQualType GotCanon,
- llvm::ArrayRef<NullabilityKind> WantNulls,
- llvm::ArrayRef<NullabilityKind> GotNulls) {
+ CanQualType GotCanon, const TypeNullability &WantNulls,
+ const TypeNullability &GotNulls) {
if (WantCanon != GotCanon) {
Diags.Report(Call, WrongTypeCanonical) << WantCanon << GotCanon;
} else if (WantNulls != GotNulls) {
@@ -170,9 +172,54 @@
using AnalysisState =
const dataflow::DataflowAnalysisState<PointerNullabilityLattice>;
+// Maps the IDs of symbolic nullability variables (like "X" for symbolic::X)
+// onto the actual symbolic nullability variables used in the analysis.
+using SymbolicMap = llvm::DenseMap<StringRef, PointerTypeNullability>;
+
+// If T is a symbolic nullability alias, return its ID.
+// e.g. "X" if the alias is marked [[clang::annotate("symbolic_nullability:X")]]
+std::optional<StringRef> getSymbolicID(TemplateDecl *TD) {
+ if (!TD || !isa<TypeAliasTemplateDecl>(TD)) return std::nullopt;
+ if (const auto *Annotate = TD->getTemplatedDecl()->getAttr<AnnotateAttr>()) {
+ StringRef Annotation = Annotate->getAnnotation();
+ if (Annotation.consume_front("symbolic_nullability:")) return Annotation;
+ }
+ return std::nullopt;
+}
+
+// We've seen a type<T>(expr) assertion, extract the nullability vector for T.
+TypeNullability getAssertedTypeNullability(QualType T, SymbolicMap &Symbolic,
+ dataflow::Arena &A) {
+ return getNullabilityAnnotationsFromType(
+ T,
+ // Given type< Nonnull<symbolic::X<Nullable<int*>*>*> >(...)
+ // usual vector: [Nonnull, Unspecified, Nullable]
+ // we want: [Nonnull, Symbolic, Nullable].
+ // We know symbolic::X<T>'s definition is T. When we see the substitution
+ // of Nullable<int*>* into T, we find its vector [Unspecified, Nullable]
+ // and replace the outer nullability for the symbolic one.
+ [&](const SubstTemplateTypeParmType *T)
+ -> std::optional<TypeNullability> {
+ if (auto ID =
+ getSymbolicID(dyn_cast<TemplateDecl>(T->getAssociatedDecl()))) {
+ auto Sym = Symbolic[*ID];
+ if (!Sym.isSymbolic())
+ // The test didn't bind anything to e.g. symbolic::X, but now wants
+ // to assert that some expression has this type!
+ // Create a variable now so we have something to assert against.
+ // That way the test will fail with a reasonable error message.
+ Sym = Symbolic[*ID] = PointerTypeNullability::createSymbolic(A);
+ auto Result = getAssertedTypeNullability(T->desugar(), Symbolic, A);
+ Result.front() = Sym;
+ return Result;
+ }
+ return std::nullopt;
+ });
+}
+
// Match any special assertions, check the condition, diagnose on failure.
void diagnoseCall(const CallExpr &CE, const ASTContext &Ctx, Diagnoser &Diags,
- const AnalysisState &State) {
+ const AnalysisState &State, SymbolicMap &Symbolic) {
if (auto Want = getAssertedNullability(CE); Want && CE.getNumArgs() == 1) {
auto &Arg = *CE.getArgs()[0];
auto Got = getNullability(&Arg, State.Env);
@@ -183,7 +230,8 @@
auto &Got = *CE.getArgs()[0];
auto WantCanon = Ctx.getCanonicalType(*Want);
auto GotCanon = Ctx.getCanonicalType(Got.getType());
- auto WantNulls = getNullabilityAnnotationsFromType(*Want);
+ auto WantNulls = getAssertedTypeNullability(
+ *Want, Symbolic, State.Env.getDataflowAnalysisContext().arena());
TypeNullability GotNulls = unspecifiedNullability(&Got);
if (const auto *GN = State.Lattice.getExprNullability(&Got)) GotNulls = *GN;
Diags.diagnoseType(CE.getBeginLoc(), Got.getSourceRange(), WantCanon,
@@ -191,6 +239,21 @@
}
}
+// Bind nullability variables for params marked symbolic::X<> etc.
+// Returns the map from symbolic ID => nullability variables.
+SymbolicMap bindSymbolicNullability(const FunctionDecl &Func,
+ PointerNullabilityAnalysis &Analysis,
+ dataflow::Arena &A) {
+ SymbolicMap Result;
+ for (const auto *Param : Func.parameters()) {
+ // For now, only support symbolic on the top level of parameter types.
+ if (auto *TST = Param->getType()->getAs<TemplateSpecializationType>())
+ if (auto I = getSymbolicID(TST->getTemplateName().getAsTemplateDecl()))
+ Result.try_emplace(*I, Analysis.assignNullabilityVariable(Param, A));
+ }
+ return Result;
+}
+
// To run a test, we simply run the nullability analysis, and then walk the
// CFG afterwards looking for calls to our assertions - nullable() etc.
// These each assert properties attached to the analysis state at that point.
@@ -209,12 +272,13 @@
auto &Ctx = Func.getDeclContext()->getParentASTContext();
auto CFCtx = require(dataflow::ControlFlowContext::build(Func));
PointerNullabilityAnalysis Analysis(Ctx);
+ auto Symbolic = bindSymbolicNullability(Func, Analysis, DACtx.arena());
require(
runDataflowAnalysis(CFCtx, Analysis, dataflow::Environment(DACtx, Func),
[&](const CFGElement &Elt, AnalysisState &State) {
if (auto CS = Elt.getAs<CFGStmt>())
if (auto *CE = dyn_cast<CallExpr>(CS->getStmt()))
- diagnoseCall(*CE, Ctx, Diags, State);
+ diagnoseCall(*CE, Ctx, Diags, State, Symbolic);
}));
}
diff --git a/nullability/test/nullability_test.h b/nullability/test/nullability_test.h
index 82e9186..dbd2a25 100644
--- a/nullability/test/nullability_test.h
+++ b/nullability/test/nullability_test.h
@@ -73,6 +73,28 @@
template <typename T>
using Nonnull [[clang::annotate("Nonnull")]] = T;
+// Marker annotations for pointer types whose nullability is symbolic.
+// This means we track it as a variable: without assuming a specific value.
+//
+// Example:
+// void target(symbolic::X<int *> p) {
+// type<Nonnull<symbolic::X<int *> *>(&p);
+// }
+//
+// When this appears:
+// - in a declaration (e.g. a function param): the decl's nullability is bound
+// to a variable
+// - in a type<...>() assertion: asserts that the nullability of the
+// expression matches that variable.
+//
+// (For now we only provide two symbolic variables, this can be extended).
+namespace symbolic {
+template <typename T>
+using X [[clang::annotate("symbolic_nullability:X")]] = T;
+template <typename T>
+using Y [[clang::annotate("symbolic_nullability:Y")]] = T;
+} // namespace symbolic
+
// Generic factory for generating values of arbitrary types and nullability.
//
// `make<Nullable<int*>>()` is a value whose type in the AST is `int*` (no
diff --git a/nullability/test/nullability_test_test.sh b/nullability/test/nullability_test_test.sh
index 807168f..4a5cf7e 100755
--- a/nullability/test/nullability_test_test.sh
+++ b/nullability/test/nullability_test_test.sh
@@ -44,7 +44,29 @@
echo "Should have failed bad type() test!"
exit 1
fi
-command -v grep && grep "static nullability is \[_Nullable\], expected \[_Nonnull\]" $LOG
+cat $LOG
+command -v grep && grep "static nullability is \[Nullable\], expected \[NonNull\]" $LOG
+
+cat >$SOURCE <<EOF
+ template <class Expected, class Actual> void type(Actual) {}
+ namespace symbolic {
+ template <class T> using A [[clang::annotate("symbolic_nullability:A")]] = T;
+ }
+
+ [[clang::annotate("test")]] void badSymbolicType1(symbolic::A<int *> x) {
+ type<int *_Nonnull>(x);
+ }
+ [[clang::annotate("test")]] void badSymbolicType2(int ** _Nullable y) {
+ type<symbolic::A<int *>*>(y);
+ }
+EOF
+if $DRIVER $SOURCE -- > $LOG; then
+ echo "Should have failed bad symbolic type() test!"
+ exit 1
+fi
+cat $LOG
+command -v grep && grep "static nullability is \[Symbolic(.*)\], expected \[NonNull\]" $LOG
+command -v grep && grep "static nullability is \[Nullable, Unspecified\], expected \[Unspecified, Symbolic(.*)\]" $LOG
cat >$SOURCE <<EOF
[[clang::annotate("test")]] int x;
diff --git a/nullability/test/symbolic_nullability.cc b/nullability/test/symbolic_nullability.cc
new file mode 100644
index 0000000..c4d6c9a
--- /dev/null
+++ b/nullability/test/symbolic_nullability.cc
@@ -0,0 +1,11 @@
+// Part of the Crubit project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "nullability_test.h"
+
+TEST void symbolicNullability(symbolic::X<int *> p, symbolic::Y<int *> q) {
+ type<symbolic::X<int *>>(p);
+ type<Nonnull<symbolic::X<int *> *>>(&p);
+ type<symbolic::Y<int *>>(q);
+}
diff --git a/nullability/type_nullability.cc b/nullability/type_nullability.cc
index e3762cf..73f9ce7 100644
--- a/nullability/type_nullability.cc
+++ b/nullability/type_nullability.cc
@@ -5,6 +5,7 @@
#include "nullability/type_nullability.h"
#include <optional>
+#include <vector>
#include "absl/log/check.h"
#include "clang/AST/ASTContext.h"
@@ -15,19 +16,37 @@
#include "clang/AST/TemplateName.h"
#include "clang/AST/Type.h"
#include "clang/AST/TypeVisitor.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
#include "clang/Basic/LLVM.h"
#include "clang/Basic/Specifiers.h"
#include "llvm/Support/SaveAndRestore.h"
+#include "llvm/Support/ScopedPrinter.h"
namespace clang::tidy::nullability {
+PointerTypeNullability PointerTypeNullability::createSymbolic(
+ dataflow::Arena &A) {
+ PointerTypeNullability Symbolic;
+ Symbolic.Symbolic = true;
+ Symbolic.Nonnull = A.makeAtom();
+ Symbolic.Nullable = A.makeAtom();
+ return Symbolic;
+}
+
+llvm::raw_ostream &operator<<(llvm::raw_ostream &OS,
+ const PointerTypeNullability &PN) {
+ // TODO: should symbolic nullabilities have names?
+ if (PN.isSymbolic())
+ return OS << "Symbolic(Nonnull=" << PN.Nonnull << ", "
+ << "Nullable=" << PN.Nullable << ")";
+ return OS << PN.concrete();
+}
+
std::string nullabilityToString(const TypeNullability &Nullability) {
std::string Result = "[";
llvm::interleave(
Nullability,
- [&](const NullabilityKind n) {
- Result += getNullabilitySpelling(n).str();
- },
+ [&](const PointerTypeNullability &PN) { Result += llvm::to_string(PN); },
[&] { Result += ", "; });
Result += "]";
return Result;
@@ -428,7 +447,7 @@
QualType T,
llvm::function_ref<GetTypeParamNullability> SubstituteTypeParam) {
struct Walker : NullabilityWalker<Walker> {
- std::vector<NullabilityKind> Annotations;
+ std::vector<PointerTypeNullability> Annotations;
llvm::function_ref<GetTypeParamNullability> SubstituteTypeParam;
void report(const PointerType *, NullabilityKind NK) {
@@ -496,7 +515,7 @@
QualType VisitPointerType(const PointerType *PT) {
CHECK(!Nullability.empty())
<< "Nullability vector too short at " << QualType(PT, 0).getAsString();
- NullabilityKind NK = Nullability.front();
+ NullabilityKind NK = Nullability.front().concrete();
Nullability = Nullability.drop_front();
QualType Rebuilt = Ctx.getPointerType(Visit(PT->getPointeeType()));
@@ -549,7 +568,7 @@
}
private:
- ArrayRef<NullabilityKind> Nullability;
+ ArrayRef<PointerTypeNullability> Nullability;
ASTContext &Ctx;
};
diff --git a/nullability/type_nullability.h b/nullability/type_nullability.h
index 55ba0e0..3c753dd 100644
--- a/nullability/type_nullability.h
+++ b/nullability/type_nullability.h
@@ -26,18 +26,78 @@
#define CRUBIT_NULLABILITY_TYPE_NULLABILITY_H_
#include <string>
+#include <tuple>
#include <utility>
+#include "absl/log/check.h"
#include "clang/AST/ASTContext.h"
#include "clang/AST/Expr.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Basic/LLVM.h"
#include "clang/Basic/Specifiers.h"
-namespace clang::dataflow {
-class BoolValue;
-}
namespace clang::tidy::nullability {
+/// Describes the nullability contract of a pointer "slot" within a type.
+///
+/// This may be concrete: nullable/non-null/unknown nullability.
+/// Or may be symbolic: this nullability is being inferred, and the presence
+/// of a "nullable" annotation is bound to a SAT variable
+class PointerTypeNullability {
+ // If concrete: NK is set, others are default.
+ // If symbolic: NK=Unspecified, Symbolic=true, Nonnull/Nullable are set.
+ NullabilityKind NK = NullabilityKind::Unspecified;
+ bool Symbolic = false;
+ dataflow::Atom Nonnull{0};
+ dataflow::Atom Nullable{0};
+
+ public:
+ PointerTypeNullability(NullabilityKind NK = NullabilityKind::Unspecified)
+ : NK(NK) {}
+ // Creates a symbolic nullability variable.
+ // A owns the underlying SAT variables nonnullAtom() and nullableAtom().
+ static PointerTypeNullability createSymbolic(dataflow::Arena &A);
+
+ // Returns the concrete nullability, or Unspecified if symbolic.
+ NullabilityKind concrete() const { return NK; }
+
+ // Returns symbolic nullability atoms.
+ // Requires: isSymbolic().
+ dataflow::Atom nonnullAtom() const {
+ CHECK(isSymbolic());
+ return Nonnull;
+ }
+
+ dataflow::Atom nullableAtom() const {
+ CHECK(isSymbolic());
+ return Nullable;
+ }
+
+ bool isSymbolic() const { return Symbolic; }
+
+ // Returns the condition under which this slot is non-null.
+ const dataflow::Formula &isNonnull(dataflow::Arena &A) const {
+ return Symbolic ? A.makeAtomRef(Nonnull)
+ : A.makeLiteral(NK == NullabilityKind::NonNull);
+ }
+
+ // Returns the condition under which this slot is nullable.
+ const dataflow::Formula &isNullable(dataflow::Arena &A) const {
+ return Symbolic ? A.makeAtomRef(Nullable)
+ : A.makeLiteral(NK == NullabilityKind::Nullable);
+ }
+
+ friend bool operator==(const PointerTypeNullability &L,
+ const PointerTypeNullability &R) {
+ return std::tie(L.NK, L.Nonnull, L.Nullable) ==
+ std::tie(R.NK, R.Nonnull, R.Nullable);
+ }
+
+ friend llvm::raw_ostream &operator<<(llvm::raw_ostream &,
+ const PointerTypeNullability &);
+};
+
/// Externalized nullability of a clang::Type.
///
/// Each pointer type nested inside is mapped to a nullability.
@@ -53,18 +113,7 @@
///
/// The concrete representation is currently the nullability of each nested
/// PointerType encountered in a preorder traversal of the canonical type.
-using TypeNullability = std::vector<NullabilityKind>;
-
-/// Describes the nullability of a pointer "slot" within a type.
-///
-/// This may represent a concrete NullabilityKind,
-/// e.g. NullabilityKind::NonNull = {Nonnull=true, Nullable=false}
-/// Or it may be symbolic: e.g. Nonnull may be an AtomicBoolValue which we want
-/// to infer, and which may be connected to SAT constraints.
-struct PointerTypeNullability {
- dataflow::BoolValue *Nonnull; // True if this slot is marked non-null.
- dataflow::BoolValue *Nullable; // True if this slot is marked nullable.
-};
+using TypeNullability = std::vector<PointerTypeNullability>;
/// Returns the `NullabilityKind` corresponding to the nullability annotation on
/// `Type` if present. Otherwise, returns `NullabilityKind::Unspecified`.
@@ -92,6 +141,7 @@
ASTContext &);
/// Returns an equivalent type annotated with the provided nullability.
/// Any existing sugar (including nullability) is discarded.
+/// Symbolic nullability is not annotated.
/// rebuildWithNullability(int *, {Nullable}) ==> int * _Nullable.
QualType rebuildWithNullability(QualType, const TypeNullability &,
ASTContext &);
