Set up tooling for verifying C++ code complies with nullability annotations.
PiperOrigin-RevId: 452285783
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
