Set up tooling for verifying C++ code complies with nullability annotations.
PiperOrigin-RevId: 452285783
diff --git a/nullability_verification/BUILD b/nullability_verification/BUILD
new file mode 100644
index 0000000..fb9700b
--- /dev/null
+++ b/nullability_verification/BUILD
@@ -0,0 +1,50 @@
+# Verification for null safety
+
+cc_library(
+ name = "pointer_nullability_lattice",
+ hdrs = ["pointer_nullability_lattice.h"],
+ deps = [
+ "@llvm-project//clang:analysis",
+ "@llvm-project//llvm:Support",
+ ],
+)
+
+cc_library(
+ name = "pointer_nullability_matchers",
+ srcs = ["pointer_nullability_matchers.cc"],
+ hdrs = ["pointer_nullability_matchers.h"],
+ deps = [
+ "@llvm-project//clang:ast_matchers",
+ "@llvm-project//llvm:Support",
+ ],
+)
+
+cc_library(
+ name = "pointer_nullability_analysis",
+ srcs = ["pointer_nullability_analysis.cc"],
+ hdrs = ["pointer_nullability_analysis.h"],
+ deps = [
+ ":pointer_nullability_lattice",
+ ":pointer_nullability_matchers",
+ "//common:check",
+ "@llvm-project//clang:analysis",
+ "@llvm-project//clang:ast",
+ "@llvm-project//clang:ast_matchers",
+ "@llvm-project//clang:basic",
+ "@llvm-project//clang:tooling",
+ ],
+)
+
+cc_test(
+ name = "pointer_nullability_analysis_test",
+ srcs = ["pointer_nullability_analysis_test.cc"],
+ deps = [
+ ":pointer_nullability_analysis",
+ "@llvm-project//clang/unittests:dataflow_testing_support",
+ "@llvm-project//llvm:Support",
+ "@llvm-project//llvm:TestingSupport",
+ "@llvm-project//llvm:gmock",
+ "@llvm-project//llvm:gtest",
+ "@llvm-project//llvm:gtest_main",
+ ],
+)
diff --git a/nullability_verification/pointer_nullability_analysis.cc b/nullability_verification/pointer_nullability_analysis.cc
new file mode 100644
index 0000000..5cde0c3
--- /dev/null
+++ b/nullability_verification/pointer_nullability_analysis.cc
@@ -0,0 +1,139 @@
+// 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_verification/pointer_nullability_analysis.h"
+
+#include <iostream>
+#include <string>
+
+#include "common/check.h"
+#include "nullability_verification/pointer_nullability_lattice.h"
+#include "nullability_verification/pointer_nullability_matchers.h"
+#include "clang/AST/ASTContext.h"
+#include "clang/AST/Expr.h"
+#include "clang/ASTMatchers/ASTMatchFinder.h"
+#include "clang/ASTMatchers/ASTMatchers.h"
+#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/MatchSwitch.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Basic/LLVM.h"
+
+namespace clang {
+namespace tidy {
+namespace nullability {
+
+using ast_matchers::MatchFinder;
+using dataflow::BoolValue;
+using dataflow::Environment;
+using dataflow::MatchSwitchBuilder;
+using dataflow::PointerValue;
+using dataflow::SkipPast;
+using dataflow::TransferState;
+using dataflow::Value;
+
+namespace {
+
+void initialisePointerNullability(
+ const Expr* Expr, const MatchFinder::MatchResult&,
+ TransferState<PointerNullabilityLattice>& State) {
+ if (auto* PointerVal = cast_or_null<PointerValue>(
+ State.Env.getValue(*Expr, SkipPast::Reference))) {
+ if (!State.Lattice.hasPointerNullability(PointerVal)) {
+ State.Lattice.setPointerNullability(PointerVal,
+ &State.Env.makeAtomicBoolValue());
+ }
+ }
+}
+
+void transferDereference(const UnaryOperator* UnaryOp,
+ const MatchFinder::MatchResult&,
+ TransferState<PointerNullabilityLattice>& State) {
+ auto* PointerExpr = UnaryOp->getSubExpr();
+ if (auto* PointerVal = cast_or_null<PointerValue>(
+ State.Env.getValue(*PointerExpr, SkipPast::Reference))) {
+ auto PointerNullability = State.Lattice.getPointerNullability(PointerVal);
+ CHECK(PointerNullability != nullptr);
+ if (State.Env.flowConditionImplies(*PointerNullability)) {
+ return;
+ }
+ }
+ State.Lattice.addViolation(PointerExpr);
+}
+
+void transferNullCheckComparison(
+ const Expr* NullCheck, const Expr* PointerExpr,
+ TransferState<PointerNullabilityLattice>& State) {
+ if (auto* PointerVal = cast_or_null<PointerValue>(
+ State.Env.getValue(*PointerExpr, SkipPast::Reference))) {
+ auto* PointerNullability = State.Lattice.getPointerNullability(PointerVal);
+ CHECK(PointerNullability != nullptr);
+
+ // For binary operations, the dataflow framework automatically creates a
+ // corresponding BoolVal
+ auto* ExistingDFVal =
+ cast_or_null<BoolValue>(State.Env.getValue(*NullCheck, SkipPast::None));
+ CHECK(ExistingDFVal != nullptr);
+ State.Env.addToFlowCondition(
+ State.Env.makeIff(*ExistingDFVal, *PointerNullability));
+ }
+}
+
+void transferNullCheckImplicitCastPtrToBool(
+ const Expr* CastExpr, const MatchFinder::MatchResult&,
+ TransferState<PointerNullabilityLattice>& State) {
+ if (auto* PointerVal = cast_or_null<PointerValue>(State.Env.getValue(
+ *CastExpr->IgnoreImplicit(), SkipPast::Reference))) {
+ auto* PointerNullability = State.Lattice.getPointerNullability(PointerVal);
+ CHECK(PointerNullability != nullptr);
+
+ auto& CastExprLoc = State.Env.createStorageLocation(*CastExpr);
+ State.Env.setValue(CastExprLoc, *PointerNullability);
+ State.Env.setStorageLocation(*CastExpr, CastExprLoc);
+ }
+}
+
+auto buildTransferer() {
+ return MatchSwitchBuilder<TransferState<PointerNullabilityLattice>>()
+ // Initialise nullability state of pointers
+ .CaseOf<Expr>(isPointerExpr(), initialisePointerNullability)
+ // Pointer dereference
+ .CaseOf<UnaryOperator>(isPointerDereference(), transferDereference)
+ // Nullability check
+ .CaseOf<BinaryOperator>(
+ isNEQNullBinOp(/*BindID=*/"pointer"),
+ [](const BinaryOperator* binOp,
+ const MatchFinder::MatchResult& result,
+ TransferState<PointerNullabilityLattice>& State) {
+ transferNullCheckComparison(
+ binOp, result.Nodes.getNodeAs<Expr>("pointer"), State);
+ })
+ .CaseOf<Expr>(isImplicitCastPtrToBool(),
+ transferNullCheckImplicitCastPtrToBool)
+ .Build();
+}
+} // namespace
+
+PointerNullabilityAnalysis::PointerNullabilityAnalysis(ASTContext& Context)
+ : DataflowAnalysis<PointerNullabilityAnalysis, PointerNullabilityLattice>(
+ Context),
+ Transferer(buildTransferer()) {}
+
+void PointerNullabilityAnalysis::transfer(const Stmt* Stmt,
+ PointerNullabilityLattice& Lattice,
+ Environment& Env) {
+ TransferState<PointerNullabilityLattice> State(Lattice, Env);
+ Transferer(*Stmt, getASTContext(), State);
+}
+
+bool PointerNullabilityAnalysis::merge(QualType Type, const Value& Val1,
+ const Environment& Env1,
+ const Value& Val2,
+ const Environment& Env2,
+ Value& MergedVal,
+ Environment& MergedEnv) {
+ return false;
+}
+} // namespace nullability
+} // namespace tidy
+} // namespace clang
diff --git a/nullability_verification/pointer_nullability_analysis.h b/nullability_verification/pointer_nullability_analysis.h
new file mode 100644
index 0000000..f15c358
--- /dev/null
+++ b/nullability_verification/pointer_nullability_analysis.h
@@ -0,0 +1,54 @@
+// 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
+
+#ifndef CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_ANALYSIS_H_
+#define CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_ANALYSIS_H_
+
+#include "nullability_verification/pointer_nullability_lattice.h"
+#include "clang/AST/ASTContext.h"
+#include "clang/AST/Expr.h"
+#include "clang/AST/Stmt.h"
+#include "clang/AST/Type.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
+#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/MatchSwitch.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Tooling/Tooling.h"
+
+namespace clang {
+namespace tidy {
+namespace nullability {
+
+// Current iteration marks lattice unsafe if there exists a pointer
+// dereference
+// TODO(b/233582219): Implement tracking of nullability to distinguish
+// safe/unsafe accesses
+
+class PointerNullabilityAnalysis
+ : public dataflow::DataflowAnalysis<PointerNullabilityAnalysis,
+ PointerNullabilityLattice> {
+ public:
+ explicit PointerNullabilityAnalysis(ASTContext& context);
+
+ static PointerNullabilityLattice initialElement() { return {}; }
+
+ void transfer(const Stmt* Stmt, PointerNullabilityLattice& Lattice,
+ dataflow::Environment& Env);
+
+ bool merge(QualType Type, const dataflow::Value& Val1,
+ const dataflow::Environment& Env1, const dataflow::Value& Val2,
+ const dataflow::Environment& Env2, dataflow::Value& MergedVal,
+ dataflow::Environment& MergedEnv) override;
+
+ private:
+ // Applies transfer functions on statements
+ dataflow::MatchSwitch<dataflow::TransferState<PointerNullabilityLattice>>
+ Transferer;
+};
+} // namespace nullability
+} // namespace tidy
+} // namespace clang
+
+#endif // CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_ANALYSIS_H_
diff --git a/nullability_verification/pointer_nullability_analysis_test.cc b/nullability_verification/pointer_nullability_analysis_test.cc
new file mode 100644
index 0000000..a8ff6c1
--- /dev/null
+++ b/nullability_verification/pointer_nullability_analysis_test.cc
@@ -0,0 +1,151 @@
+// 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_verification/pointer_nullability_analysis.h"
+
+#include <string>
+
+#include "third_party/llvm/llvm-project/clang/unittests/Analysis/FlowSensitive/TestingSupport.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Error.h"
+#include "llvm/Testing/Support/Error.h"
+#include "third_party/llvm/llvm-project/llvm/utils/unittest/googlemock/include/gmock/gmock.h"
+#include "third_party/llvm/llvm-project/llvm/utils/unittest/googletest/include/gtest/gtest.h"
+
+namespace clang {
+namespace tidy {
+namespace nullability {
+namespace {
+
+using ::testing::Pair;
+using ::testing::Test;
+using ::testing::UnorderedElementsAre;
+
+using dataflow::DataflowAnalysisState;
+using dataflow::Environment;
+using dataflow::test::checkDataflow;
+
+MATCHER(IsSafe, "") { return arg.Lattice.isSafe(); }
+MATCHER(IsUnsafe, "") { return !arg.Lattice.isSafe(); }
+
+class PointerNullabilityTest : public Test {
+ protected:
+ template <typename Matcher>
+ void expectDataflow(llvm::StringRef Code, Matcher Expectations) {
+ ASSERT_THAT_ERROR(
+ checkDataflow<PointerNullabilityAnalysis>(
+ Code, "target",
+ [](ASTContext& ASTCtx, Environment&) {
+ return PointerNullabilityAnalysis(ASTCtx);
+ },
+ [&Expectations](
+ llvm::ArrayRef<
+ std::pair<std::string,
+ DataflowAnalysisState<PointerNullabilityLattice>>>
+ Results,
+ ASTContext&) { EXPECT_THAT(Results, Expectations); },
+ {"-fsyntax-only", "-std=c++17"}),
+ llvm::Succeeded());
+ }
+};
+
+TEST_F(PointerNullabilityTest, SafeNoOp) {
+ std::string Code = R"(
+ void target(int* maybeNull) {
+ 1 + 2;
+ /*[[check]]*/
+ }
+ )";
+ expectDataflow(Code, UnorderedElementsAre(Pair("check", IsSafe())));
+}
+
+TEST_F(PointerNullabilityTest, UnsafeUnchecked) {
+ std::string Code = R"(
+ void target(int* maybeNull) {
+ *maybeNull;
+ /*[[check]]*/
+ }
+ )";
+ expectDataflow(Code, UnorderedElementsAre(Pair("check", IsUnsafe())));
+}
+
+TEST_F(PointerNullabilityTest, SafeCheckNEQNull) {
+ std::string NullLiteralOnRight = R"(
+ void target(int* maybeNull) {
+ if (maybeNull != nullptr) {
+ *maybeNull;
+ /*[[check-safe]]*/
+ } else {
+ *maybeNull;
+ /*[[check-unsafe1]]*/
+ }
+ *maybeNull;
+ /*[[check-unsafe2]]*/
+ }
+ )";
+ expectDataflow(NullLiteralOnRight,
+ UnorderedElementsAre(Pair("check-safe", IsSafe()),
+ Pair("check-unsafe1", IsUnsafe()),
+ Pair("check-unsafe2", IsUnsafe())));
+
+ std::string NullLiteralOnLeft = R"(
+ void target(int* maybeNull) {
+ if (nullptr != maybeNull) {
+ *maybeNull;
+ /*[[check-safe]]*/
+ } else {
+ *maybeNull;
+ /*[[check-unsafe1]]*/
+ }
+ *maybeNull;
+ /*[[check-unsafe2]]*/
+ }
+ )";
+ expectDataflow(NullLiteralOnLeft,
+ UnorderedElementsAre(Pair("check-safe", IsSafe()),
+ Pair("check-unsafe1", IsUnsafe()),
+ Pair("check-unsafe2", IsUnsafe())));
+}
+
+TEST_F(PointerNullabilityTest, SafeCheckImplicitCastToBool) {
+ std::string Code = R"(
+ void target(int* maybeNull) {
+ if (maybeNull) {
+ *maybeNull;
+ /*[[check-safe]]*/
+ } else {
+ *maybeNull;
+ /*[[check-unsafe1]]*/
+ }
+ *maybeNull;
+ /*[[check-unsafe2]]*/
+ }
+ )";
+ expectDataflow(Code, UnorderedElementsAre(Pair("check-safe", IsSafe()),
+ Pair("check-unsafe1", IsUnsafe()),
+ Pair("check-unsafe2", IsUnsafe())));
+ std::string NegatedCondition = R"(
+ void target(int* maybeNull) {
+ if (!maybeNull) {
+ *maybeNull;
+ /*[[check-unsafe1]]*/
+ } else {
+ *maybeNull;
+ /*[[check-safe]]*/
+ }
+ *maybeNull;
+ /*[[check-unsafe2]]*/
+ }
+ )";
+ expectDataflow(NegatedCondition,
+ UnorderedElementsAre(Pair("check-safe", IsSafe()),
+ Pair("check-unsafe1", IsUnsafe()),
+ Pair("check-unsafe2", IsUnsafe())));
+}
+
+} // namespace
+} // namespace nullability
+} // namespace tidy
+} // namespace clang
diff --git a/nullability_verification/pointer_nullability_lattice.h b/nullability_verification/pointer_nullability_lattice.h
new file mode 100644
index 0000000..917e075
--- /dev/null
+++ b/nullability_verification/pointer_nullability_lattice.h
@@ -0,0 +1,61 @@
+// 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
+
+#ifndef CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_LATTICE_H_
+#define CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_LATTICE_H_
+
+#include <ostream>
+
+#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseSet.h"
+
+namespace clang {
+namespace tidy {
+namespace nullability {
+class PointerNullabilityLattice {
+ public:
+ PointerNullabilityLattice() = default;
+
+ bool operator==(const PointerNullabilityLattice& Other) const { return true; }
+
+ dataflow::LatticeJoinEffect join(const PointerNullabilityLattice& Other) {
+ return dataflow::LatticeJoinEffect::Unchanged;
+ }
+
+ bool hasPointerNullability(clang::dataflow::PointerValue* PointerVal) {
+ return pointer_nullabilities_.find(PointerVal) !=
+ pointer_nullabilities_.end();
+ }
+
+ dataflow::BoolValue* getPointerNullability(
+ dataflow::PointerValue* PointerVal) {
+ auto search = pointer_nullabilities_.find(PointerVal);
+ return search == pointer_nullabilities_.end() ? nullptr : search->second;
+ }
+
+ void setPointerNullability(dataflow::PointerValue* PointerVal,
+ dataflow::BoolValue* BoolVal) {
+ pointer_nullabilities_[PointerVal] = BoolVal;
+ }
+
+ bool isSafe() const { return violations_.empty(); }
+ void addViolation(const Expr* Violation) { violations_.insert(Violation); }
+
+ private:
+ llvm::DenseSet<const Expr*> violations_;
+ llvm::DenseMap<dataflow::PointerValue*, dataflow::BoolValue*>
+ pointer_nullabilities_;
+};
+
+inline std::ostream& operator<<(std::ostream& OS,
+ const PointerNullabilityLattice& L) {
+ return OS << "Pointer Nullability Lattice";
+}
+} // namespace nullability
+} // namespace tidy
+} // namespace clang
+
+#endif // CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_LATTICE_H_
diff --git a/nullability_verification/pointer_nullability_matchers.cc b/nullability_verification/pointer_nullability_matchers.cc
new file mode 100644
index 0000000..37c4266
--- /dev/null
+++ b/nullability_verification/pointer_nullability_matchers.cc
@@ -0,0 +1,49 @@
+// 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_verification/pointer_nullability_matchers.h"
+
+#include "clang/ASTMatchers/ASTMatchers.h"
+#include "llvm/ADT/StringRef.h"
+
+namespace clang {
+namespace tidy {
+namespace nullability {
+
+using ast_matchers::binaryOperator;
+using ast_matchers::booleanType;
+using ast_matchers::expr;
+using ast_matchers::hasImplicitDestinationType;
+using ast_matchers::hasOperands;
+using ast_matchers::hasOperatorName;
+using ast_matchers::hasSourceExpression;
+using ast_matchers::hasType;
+using ast_matchers::hasUnaryOperand;
+using ast_matchers::ignoringImplicit;
+using ast_matchers::implicitCastExpr;
+using ast_matchers::isAnyPointer;
+using ast_matchers::nullPointerConstant;
+using ast_matchers::unaryOperator;
+using ast_matchers::internal::Matcher;
+
+Matcher<Stmt> isPointerExpr() { return expr(hasType(isAnyPointer())); }
+
+Matcher<Stmt> isPointerDereference() {
+ return unaryOperator(hasOperatorName("*"), hasUnaryOperand(isPointerExpr()));
+}
+
+Matcher<Stmt> isNEQNullBinOp(llvm::StringRef BindID) {
+ return binaryOperator(
+ hasOperatorName("!="),
+ hasOperands(ignoringImplicit(nullPointerConstant()),
+ expr(hasType(isAnyPointer())).bind(BindID)));
+}
+
+Matcher<Stmt> isImplicitCastPtrToBool() {
+ return implicitCastExpr(hasSourceExpression(isPointerExpr()),
+ hasImplicitDestinationType(booleanType()));
+}
+} // namespace nullability
+} // namespace tidy
+} // namespace clang
diff --git a/nullability_verification/pointer_nullability_matchers.h b/nullability_verification/pointer_nullability_matchers.h
new file mode 100644
index 0000000..ed30a23
--- /dev/null
+++ b/nullability_verification/pointer_nullability_matchers.h
@@ -0,0 +1,23 @@
+// 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
+
+#ifndef CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_MATCHERS_H_
+#define CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_MATCHERS_H_
+
+#include "clang/ASTMatchers/ASTMatchersInternal.h"
+
+namespace clang {
+namespace tidy {
+namespace nullability {
+
+ast_matchers::internal::Matcher<Stmt> isPointerExpr();
+ast_matchers::internal::Matcher<Stmt> isPointerDereference();
+ast_matchers::internal::Matcher<Stmt> isNEQNullBinOp(llvm::StringRef BindID);
+ast_matchers::internal::Matcher<Stmt> isImplicitCastPtrToBool();
+
+} // namespace nullability
+} // namespace tidy
+} // namespace clang
+
+#endif // CRUBIT_NULLABILITY_VERIFICATION_POINTER_NULLABILITY_MATCHERS_H_
