[clang][dataflow] Add reverse null checker

[Discookie]

TITLE: [clang][dataflow] Add null-check after dereference checker

This checker implements a null-pointer analysis checker using the data-flow framework. In particular, the checker finds cases where the pointer's nullability is checked after it has been dereferenced:

int f(int *ptr) {
  *ptr += 20; // note: one of the locations where the pointer's value cannot be null
  
  if (ptr) {
    *ptr += 42; // warning: pointer value is checked even though it cannot be null at this point
    return *ptr;
  }
  return 0;

It currently recognizes the following operations:

• Dereference and arrow operators
• Pointer-to-boolean cast
• Assigning &obj, nullptr and other values

---

Notable limitations:

The checker only supports C++ due to the limitations of the framework (llvm#65301).

Function calls taking a reference of a pointer are not handled yet.
void external(int *&ref);

The note tag is only displayed at one location, and not all operations are supported or displayed.

More examples and limitations in the checker docs.

---

Results on open-source projects:
https://codechecker-demo.eastus.cloudapp.azure.com/Default/runs?run=Discookie_reverse-null

The reference-of-ptr limitation leads to a class of false positives across the tested projects (example).

But the checker also found quite a few true positives, on LLVM: 1 2 3 and a couple more, listed here.

---

This checker corresponds to the the CERT rule EXP34-C, Do not dereference null pointers, example 3.

[github-actions]

⚠️ C/C++ code formatter, clang-format found issues in your code. ⚠️

You can test this locally with the following command:

git-clang-format --diff 35d771fd4ffd300e527da87b8329bd120b220a83 086c092dedf063d327cc118aac56f6d2345208eb -- clang-tools-extra/clang-tidy/bugprone/ReverseNullCheck.cpp clang-tools-extra/clang-tidy/bugprone/ReverseNullCheck.h clang-tools-extra/test/clang-tidy/checkers/bugprone/reverse-null.cpp clang/include/clang/Analysis/FlowSensitive/Models/ReverseNullModel.h clang/lib/Analysis/FlowSensitive/Models/ReverseNullModel.cpp clang/unittests/Analysis/FlowSensitive/ReverseNullModelTest.cpp clang-tools-extra/clang-tidy/bugprone/BugproneTidyModule.cpp

View the diff from clang-format here.

diff --git a/clang-tools-extra/clang-tidy/bugprone/ReverseNullCheck.cpp b/clang-tools-extra/clang-tidy/bugprone/ReverseNullCheck.cpp
index 253bfb130..2fdf8b497 100644
--- a/clang-tools-extra/clang-tidy/bugprone/ReverseNullCheck.cpp
+++ b/clang-tools-extra/clang-tidy/bugprone/ReverseNullCheck.cpp
@@ -32,7 +32,6 @@ using ast_matchers::MatchFinder;
 using dataflow::ReverseNullDiagnoser;
 using dataflow::ReverseNullModel;
 
-
 static constexpr llvm::StringLiteral FuncID("fun");
 
 static std::optional<ReverseNullDiagnoser::ResultType>
@@ -61,19 +60,21 @@ analyzeFunction(const FunctionDecl &FuncDecl, ASTContext &ASTCtx) {
       std::optional<DataflowAnalysisState<ReverseNullModel::Lattice>>>>
       BlockToOutputState = dataflow::runDataflowAnalysis(
           *Context, Analysis, Env,
-          [&ASTCtx, &Diagnoser, &Diagnostics](
-              const CFGElement &Elt,
-              const DataflowAnalysisState<ReverseNullModel::Lattice>
-                  &State) mutable {
+          [&ASTCtx, &Diagnoser,
+           &Diagnostics](const CFGElement &Elt,
+                         const DataflowAnalysisState<ReverseNullModel::Lattice>
+                             &State) mutable {
             auto EltDiagnostics = Diagnoser.diagnose(ASTCtx, &Elt, State.Env);
-            llvm::move(EltDiagnostics.first, std::back_inserter(Diagnostics.first));
-            llvm::move(EltDiagnostics.second, std::back_inserter(Diagnostics.second));
+            llvm::move(EltDiagnostics.first,
+                       std::back_inserter(Diagnostics.first));
+            llvm::move(EltDiagnostics.second,
+                       std::back_inserter(Diagnostics.second));
           });
 
   // FIXME: Port this over into UncheckedOptionalAccessCheck
   if (llvm::Error E = BlockToOutputState.takeError()) {
-    llvm::dbgs() << "Dataflow analysis failed: "
-        << llvm::toString(std::move(E)) << ".\n";
+    llvm::dbgs() << "Dataflow analysis failed: " << llvm::toString(std::move(E))
+                 << ".\n";
     return std::nullopt;
   }
 
@@ -96,8 +97,7 @@ void ReverseNullCheck::registerMatchers(MatchFinder *Finder) {
       this);
 }
 
-void ReverseNullCheck::check(
-    const MatchFinder::MatchResult &Result) {
+void ReverseNullCheck::check(const MatchFinder::MatchResult &Result) {
   // llvm::errs() << "Starting result parse\n";
   if (Result.SourceManager->getDiagnostics().hasUncompilableErrorOccurred())
     return;
@@ -114,7 +114,8 @@ void ReverseNullCheck::check(
       diag(Loc, "pointer value is checked despite dereferencing it earlier");
 
     for (const SourceLocation &Loc : Errors->first)
-      diag(Loc, "pointer value is checked but it can only be null at this point");
+      diag(Loc,
+           "pointer value is checked but it can only be null at this point");
   }
 }
 
diff --git a/clang-tools-extra/clang-tidy/bugprone/ReverseNullCheck.h b/clang-tools-extra/clang-tidy/bugprone/ReverseNullCheck.h
index 2ab182c9a..4295bae75 100644
--- a/clang-tools-extra/clang-tidy/bugprone/ReverseNullCheck.h
+++ b/clang-tools-extra/clang-tidy/bugprone/ReverseNullCheck.h
@@ -20,7 +20,7 @@ class ReverseNullCheck : public ClangTidyCheck {
 public:
   ReverseNullCheck(StringRef Name, ClangTidyContext *Context)
       : ClangTidyCheck(Name, Context) {}
-  
+
   bool isLanguageVersionSupported(const LangOptions &LangOpts) const override {
     return LangOpts.CPlusPlus;
   }
@@ -29,7 +29,7 @@ public:
 };
 
 } // namespace bugprone
-}
-}
+} // namespace tidy
+} // namespace clang
 
 #endif // LLVM_CLANG_TOOLS_EXTRA_CLANG_TIDY_BUGPRONE_REVERSENULLCHECK_H
diff --git a/clang/include/clang/Analysis/FlowSensitive/Models/ReverseNullModel.h b/clang/include/clang/Analysis/FlowSensitive/Models/ReverseNullModel.h
index 9ee8a0d28..683cdfcfb 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Models/ReverseNullModel.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Models/ReverseNullModel.h
@@ -29,7 +29,6 @@
 #include "llvm/ADT/StringRef.h"
 #include "llvm/ADT/Twine.h"
 
-
 namespace clang {
 namespace dataflow {
 
@@ -39,13 +38,13 @@ namespace dataflow {
 // invalidate the analysis. It also could be optimized to drop out-of-scope
 // variables from the map.
 class ReverseNullModel
-    : public DataflowAnalysis<ReverseNullModel,
-                              NoopLattice> {
+    : public DataflowAnalysis<ReverseNullModel, NoopLattice> {
 public:
   struct TransferArgs {
     bool Branch;
     Environment &Env;
   };
+
 private:
   CFGMatchSwitch<Environment> TransferMatchSwitch;
   ASTMatchSwitch<Stmt, TransferArgs> BranchTransferMatchSwitch;
@@ -53,30 +52,27 @@ private:
 public:
   explicit ReverseNullModel(ASTContext &Context);
 
-  static NoopLattice initialElement() {
-    return {};
-  }
+  static NoopLattice initialElement() { return {}; }
 
   static ast_matchers::StatementMatcher ptrValueMatcher();
 
   // Used to initialize the storage locations of function arguments.
   // Required to merge these values within the environment.
-  void initializeFunctionParameters(const ControlFlowContext &CFCtx, Environment &Env);
+  void initializeFunctionParameters(const ControlFlowContext &CFCtx,
+                                    Environment &Env);
 
-  void transfer(const CFGElement &E, NoopLattice &State,
-                Environment &Env);
+  void transfer(const CFGElement &E, NoopLattice &State, Environment &Env);
 
   void transferBranch(bool Branch, const Stmt *E, NoopLattice &State,
-                Environment &Env);
+                      Environment &Env);
 
-  bool merge(QualType Type,
-              const Value &Val1, const Environment &Env1,
-              const Value &Val2, const Environment &Env2,
-              Value &MergedVal, Environment &MergedEnv) override;
+  bool merge(QualType Type, const Value &Val1, const Environment &Env1,
+             const Value &Val2, const Environment &Env2, Value &MergedVal,
+             Environment &MergedEnv) override;
 
-  ComparisonResult compare(QualType Type,
-                           const Value &Val1, const Environment &Env1,
-                           const Value &Val2, const Environment &Env2) override;
+  ComparisonResult compare(QualType Type, const Value &Val1,
+                           const Environment &Env1, const Value &Val2,
+                           const Environment &Env2) override;
 
   Value *widen(QualType Type, Value &Prev, const Environment &PrevEnv,
                Value &Current, Environment &CurrentEnv) override;
@@ -85,17 +81,17 @@ public:
 class ReverseNullDiagnoser {
 public:
   ReverseNullDiagnoser();
-  using ResultType = std::pair<std::vector<SourceLocation>, std::vector<SourceLocation>>;
+  using ResultType =
+      std::pair<std::vector<SourceLocation>, std::vector<SourceLocation>>;
 
   ResultType diagnose(ASTContext &Ctx, const CFGElement *Elt,
-                                       const Environment &Env);
+                      const Environment &Env);
 
 private:
-  CFGMatchSwitch<const Environment, ResultType>
-      DiagnoseMatchSwitch;
+  CFGMatchSwitch<const Environment, ResultType> DiagnoseMatchSwitch;
 };
 
-}
-}
+} // namespace dataflow
+} // namespace clang
 
 #endif // CLANG_ANALYSIS_FLOWSENSITIVE_MODELS_REVERSENULLMODEL_H
diff --git a/clang/lib/Analysis/FlowSensitive/Models/ReverseNullModel.cpp b/clang/lib/Analysis/FlowSensitive/Models/ReverseNullModel.cpp
index 3f0a5f31e..e2e9dbe54 100644
--- a/clang/lib/Analysis/FlowSensitive/Models/ReverseNullModel.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Models/ReverseNullModel.cpp
@@ -37,24 +37,19 @@ constexpr char kVar[] = "var"; // FIXME: Make into prvalue, rvalue
 constexpr char kIsNonnull[] = "is-nonnull";
 constexpr char kIsNull[] = "is-null";
 
-enum class SatisfiabilityResult {
-  Nullptr,
-  Top,
-  True,
-  False,
-  Unknown
-};
+enum class SatisfiabilityResult { Nullptr, Top, True, False, Unknown };
 
 using SR = SatisfiabilityResult;
 
-auto ptrToVar(llvm::StringRef VarName = kVar) { 
-  return traverse(TK_IgnoreUnlessSpelledInSource, 
+auto ptrToVar(llvm::StringRef VarName = kVar) {
+  return traverse(TK_IgnoreUnlessSpelledInSource,
                   declRefExpr(hasType(isAnyPointer())).bind(VarName));
 }
-auto namedPtrToVar(llvm::StringRef name) { 
-  return functionDecl(hasDescendant(declRefExpr(allOf(hasType(isAnyPointer()),
-                     hasDeclaration(namedDecl(hasName(name))))).bind(kVar)
-  )); 
+auto namedPtrToVar(llvm::StringRef name) {
+  return functionDecl(
+      hasDescendant(declRefExpr(allOf(hasType(isAnyPointer()),
+                                      hasDeclaration(namedDecl(hasName(name)))))
+                        .bind(kVar)));
 }
 
 auto derefMatcher() {
@@ -72,56 +67,56 @@ auto arrowMatcher() {
 // FIXME: Deliberately simple - a proper check would only match direct ptr casts
 auto castExprMatcher() {
   return castExpr(hasCastKind(CK_PointerToBoolean),
-                  hasSourceExpression(
-                    ptrToVar()))
+                  hasSourceExpression(ptrToVar()))
       .bind(kCond);
 }
 
-auto nullptrMatcher() {
-  return expr(nullPointerConstant()).bind(kVar);
-}
+auto nullptrMatcher() { return expr(nullPointerConstant()).bind(kVar); }
 
 auto addressofMatcher() {
   return unaryOperator(hasOperatorName("&")).bind(kVar);
 }
 
 auto functionCallMatcher() {
-  return callExpr(hasDeclaration(functionDecl(returns(isAnyPointer())))).bind(kVar);
+  return callExpr(hasDeclaration(functionDecl(returns(isAnyPointer()))))
+      .bind(kVar);
 }
 
-auto anyPointerMatcher() {
-  return expr(hasType(isAnyPointer())).bind(kVar);
-}
+auto anyPointerMatcher() { return expr(hasType(isAnyPointer())).bind(kVar); }
 
 // Only computes simple comparisons against boolean True and False values.
 // Faster, but produces many Unknown values.
-SatisfiabilityResult shallowComputeSatisfiability(BoolValue *Val, const Environment &Env) {
+SatisfiabilityResult shallowComputeSatisfiability(BoolValue *Val,
+                                                  const Environment &Env) {
   if (!Val)
     return SR::Nullptr;
-  
+
   if (isa<TopBoolValue>(Val))
     return SR::Top;
 
   if (Val == &Env.getBoolLiteralValue(true))
     return SR::True;
-  
+
   if (Val == &Env.getBoolLiteralValue(false))
     return SR::False;
 
   return SR::Unknown;
 }
 
-// Computes satisfiability by using the flow condition. Slower, but more precise.
-SatisfiabilityResult computeSatisfiability(BoolValue *Val, const Environment &Env) {
+// Computes satisfiability by using the flow condition. Slower, but more
+// precise.
+SatisfiabilityResult computeSatisfiability(BoolValue *Val,
+                                           const Environment &Env) {
   // Early return with the fast compute values.
-  if (SatisfiabilityResult ShallowResult = shallowComputeSatisfiability(Val, Env);
+  if (SatisfiabilityResult ShallowResult =
+          shallowComputeSatisfiability(Val, Env);
       ShallowResult != SR::Unknown) {
     return ShallowResult;
   }
 
   if (Env.flowConditionImplies(Val->formula()))
     return SR::True;
-  
+
   if (Env.flowConditionImplies(Env.arena().makeNot(Val->formula())))
     return SR::False;
 
@@ -134,14 +129,14 @@ inline BoolValue &getVal(llvm::StringRef Name, Value &RootValue) {
 
 void initializeRootValue(Value &RootValue, Environment &Env) {
 
-    Arena &A = Env.arena();
+  Arena &A = Env.arena();
 
-    BoolValue &IsNull = A.makeAtomValue();
-    BoolValue &IsNonnull = A.makeAtomValue();
-    RootValue.setProperty(kIsNull, IsNull);
-    RootValue.setProperty(kIsNonnull, IsNonnull);
+  BoolValue &IsNull = A.makeAtomValue();
+  BoolValue &IsNonnull = A.makeAtomValue();
+  RootValue.setProperty(kIsNull, IsNull);
+  RootValue.setProperty(kIsNonnull, IsNonnull);
 
-    Env.addToFlowCondition(A.makeOr(IsNull.formula(), IsNonnull.formula()));
+  Env.addToFlowCondition(A.makeOr(IsNull.formula(), IsNonnull.formula()));
 }
 
 void setLValue(const Expr &E, Value &Val, Environment &Env) {
@@ -165,40 +160,41 @@ void setUnknownValue(const Expr &E, Value &Val, Environment &Env) {
 }
 
 Value *getValue(const Expr &Var, Environment &Env) {
-    if (auto *EnvVal = Env.getValue(Var)) {
-        // FIXME: Hack
-        if (!EnvVal->getProperty(kIsNull) && !EnvVal->getProperty(kIsNonnull)) {
-            initializeRootValue(*EnvVal, Env);
-        }
-
-        return EnvVal;
+  if (auto *EnvVal = Env.getValue(Var)) {
+    // FIXME: Hack
+    if (!EnvVal->getProperty(kIsNull) && !EnvVal->getProperty(kIsNonnull)) {
+      initializeRootValue(*EnvVal, Env);
     }
 
-    auto *RootValue = Env.createValue(Var.getType());
+    return EnvVal;
+  }
 
-    if (!RootValue) 
-        return nullptr;
+  auto *RootValue = Env.createValue(Var.getType());
 
-    initializeRootValue(*RootValue, Env);
+  if (!RootValue)
+    return nullptr;
+
+  initializeRootValue(*RootValue, Env);
 
-    setLValue(Var, *RootValue, Env);
+  setLValue(Var, *RootValue, Env);
 
-    return RootValue;
+  return RootValue;
 }
 
 void matchDereferenceExpr(const Stmt *stmt,
                           const MatchFinder::MatchResult &Result,
                           Environment &Env) {
-    const auto *Var = Result.Nodes.getNodeAs<Expr>(kVar);
-    assert(Var != nullptr);
+  const auto *Var = Result.Nodes.getNodeAs<Expr>(kVar);
+  assert(Var != nullptr);
 
-    // FIXME: Optimize
-    auto *RootValue = getValue(*Var, Env);
-    if (!RootValue) {
-       return;
-    }
+  // FIXME: Optimize
+  auto *RootValue = getValue(*Var, Env);
+  if (!RootValue) {
+    return;
+  }
 
-    Env.addToFlowCondition(Env.arena().makeNot(getVal(kIsNull, *RootValue).formula()));
+  Env.addToFlowCondition(
+      Env.arena().makeNot(getVal(kIsNull, *RootValue).formula()));
 }
 
 void matchCastExpr(const CastExpr *cond, const MatchFinder::MatchResult &Result,
@@ -211,109 +207,117 @@ void matchCastExpr(const CastExpr *cond, const MatchFinder::MatchResult &Result,
   auto *RootValue = getValue(*Var, Env);
   if (!RootValue) {
     return;
-    }
+  }
 
-    auto *NewRootValue = Env.createValue(Var->getType());
-    if (!NewRootValue) 
-        return;
+  auto *NewRootValue = Env.createValue(Var->getType());
+  if (!NewRootValue)
+    return;
 
-    setLValue(*Var, *NewRootValue, Env);
+  setLValue(*Var, *NewRootValue, Env);
 
-    Arena &A = Env.arena();
+  Arena &A = Env.arena();
 
-    if (IsNonnullBranch) {
-        BoolValue &IsNonnull = getVal(kIsNonnull, *RootValue);
-        BoolValue &IsNull = getVal(kIsNull, *RootValue);
+  if (IsNonnullBranch) {
+    BoolValue &IsNonnull = getVal(kIsNonnull, *RootValue);
+    BoolValue &IsNull = getVal(kIsNull, *RootValue);
 
-        Env.addToFlowCondition(A.makeNot(IsNull.formula()));
-        NewRootValue->setProperty(kIsNull, Env.getBoolLiteralValue(false));
+    Env.addToFlowCondition(A.makeNot(IsNull.formula()));
+    NewRootValue->setProperty(kIsNull, Env.getBoolLiteralValue(false));
 
-        NewRootValue->setProperty(kIsNonnull, IsNonnull);
-    } else {
-        BoolValue &IsNonnull = getVal(kIsNonnull, *RootValue);
-        BoolValue &IsNull = getVal(kIsNull, *RootValue);
+    NewRootValue->setProperty(kIsNonnull, IsNonnull);
+  } else {
+    BoolValue &IsNonnull = getVal(kIsNonnull, *RootValue);
+    BoolValue &IsNull = getVal(kIsNull, *RootValue);
 
-        NewRootValue->setProperty(kIsNull, IsNull);
+    NewRootValue->setProperty(kIsNull, IsNull);
 
-        Env.addToFlowCondition(A.makeNot(IsNonnull.formula()));
-        NewRootValue->setProperty(kIsNonnull, Env.getBoolLiteralValue(false));
-    }
+    Env.addToFlowCondition(A.makeNot(IsNonnull.formula()));
+    NewRootValue->setProperty(kIsNonnull, Env.getBoolLiteralValue(false));
+  }
 }
 
-void matchNullptrExpr(const Expr *expr, const MatchFinder::MatchResult &Result, Environment &Env) {
-    const auto *PrVar = Result.Nodes.getNodeAs<Expr>(kVar);
-    assert(PrVar != nullptr);
+void matchNullptrExpr(const Expr *expr, const MatchFinder::MatchResult &Result,
+                      Environment &Env) {
+  const auto *PrVar = Result.Nodes.getNodeAs<Expr>(kVar);
+  assert(PrVar != nullptr);
 
-    if (Env.getValue(*PrVar))
-      return;
+  if (Env.getValue(*PrVar))
+    return;
 
-    // FIXME: Nullptr does not create a value
-    auto *RootValue = Env.createValue(PrVar->getType());
-    if (!RootValue) {
-       return;
-    }
+  // FIXME: Nullptr does not create a value
+  auto *RootValue = Env.createValue(PrVar->getType());
+  if (!RootValue) {
+    return;
+  }
 
-    RootValue->setProperty(kIsNull, Env.getBoolLiteralValue(true));
-    RootValue->setProperty(kIsNonnull, Env.getBoolLiteralValue(false));
-    Env.setValue(*PrVar, *RootValue);
+  RootValue->setProperty(kIsNull, Env.getBoolLiteralValue(true));
+  RootValue->setProperty(kIsNonnull, Env.getBoolLiteralValue(false));
+  Env.setValue(*PrVar, *RootValue);
 }
 
-void matchAddressofExpr(const Expr *expr, const MatchFinder::MatchResult &Result, Environment &Env) {
-    const auto *PrVar = Result.Nodes.getNodeAs<Expr>(kVar);
-    assert(PrVar != nullptr);
+void matchAddressofExpr(const Expr *expr,
+                        const MatchFinder::MatchResult &Result,
+                        Environment &Env) {
+  const auto *PrVar = Result.Nodes.getNodeAs<Expr>(kVar);
+  assert(PrVar != nullptr);
 
-    auto *RootValue = Env.createValue(PrVar->getType());
-    if (!RootValue) {
-       return;
-    }
+  auto *RootValue = Env.createValue(PrVar->getType());
+  if (!RootValue) {
+    return;
+  }
 
-    RootValue->setProperty(kIsNull, Env.getBoolLiteralValue(false));
-    RootValue->setProperty(kIsNonnull, Env.getBoolLiteralValue(true));
-    Env.setValue(*PrVar, *RootValue);
+  RootValue->setProperty(kIsNull, Env.getBoolLiteralValue(false));
+  RootValue->setProperty(kIsNonnull, Env.getBoolLiteralValue(true));
+  Env.setValue(*PrVar, *RootValue);
 }
 
-void matchFunctionCallExpr(const Expr *fncall, const MatchFinder::MatchResult &Result, Environment &Env) {
-    // This is not necessarily a prvalue, since operators such as prefix ++ are lvalues.
-    const auto *Var = Result.Nodes.getNodeAs<Expr>(kVar);
-    assert(Var != nullptr);
+void matchFunctionCallExpr(const Expr *fncall,
+                           const MatchFinder::MatchResult &Result,
+                           Environment &Env) {
+  // This is not necessarily a prvalue, since operators such as prefix ++ are
+  // lvalues.
+  const auto *Var = Result.Nodes.getNodeAs<Expr>(kVar);
+  assert(Var != nullptr);
 
-    // Initialize to (Unknown, Unknown)
-    if (Env.getValue(*Var))
-      return;
+  // Initialize to (Unknown, Unknown)
+  if (Env.getValue(*Var))
+    return;
 
-    auto *RootValue = Env.createValue(Var->getType());
-    if (!RootValue)
-       return;
-    
-    initializeRootValue(*RootValue, Env);
-    setUnknownValue(*Var, *RootValue, Env);
+  auto *RootValue = Env.createValue(Var->getType());
+  if (!RootValue)
+    return;
+
+  initializeRootValue(*RootValue, Env);
+  setUnknownValue(*Var, *RootValue, Env);
 }
 
 ReverseNullDiagnoser::ResultType
 diagnoseCastExpr(const CastExpr *Stmt, const MatchFinder::MatchResult &Result,
-               const Environment &Env) {
-    const auto *Var = Result.Nodes.getNodeAs<Expr>(kVar);
-    assert(Var != nullptr);
-
-    Arena &A = Env.arena();
-
-    if (auto *RootValue = Env.getValue(*Var)) {
-        // FIXME: Hack
-        if (RootValue->getProperty(kIsNull) && RootValue->getProperty(kIsNonnull)) {
-            bool IsNull = !Env.flowConditionImplies(A.makeNot(getVal(kIsNull, *RootValue).formula()));
-            bool IsNonnull = !Env.flowConditionImplies(A.makeNot(getVal(kIsNonnull, *RootValue).formula()));
-
-            if (!IsNull && IsNonnull) {
-                return {{}, {Var->getBeginLoc()}};
-            }
-
-            if (IsNull && !IsNonnull) {
-                return {{Var->getBeginLoc()}, {}};
-            }
-        }
+                 const Environment &Env) {
+  const auto *Var = Result.Nodes.getNodeAs<Expr>(kVar);
+  assert(Var != nullptr);
+
+  Arena &A = Env.arena();
+
+  if (auto *RootValue = Env.getValue(*Var)) {
+    // FIXME: Hack
+    if (RootValue->getProperty(kIsNull) && RootValue->getProperty(kIsNonnull)) {
+      bool IsNull = !Env.flowConditionImplies(
+          A.makeNot(getVal(kIsNull, *RootValue).formula()));
+      bool IsNonnull = !Env.flowConditionImplies(
+          A.makeNot(getVal(kIsNonnull, *RootValue).formula()));
+
+      if (!IsNull && IsNonnull) {
+        return {{}, {Var->getBeginLoc()}};
+      }
+
+      if (IsNull && !IsNonnull) {
+        return {{Var->getBeginLoc()}, {}};
+      }
     }
+  }
 
-    return {};
+  return {};
 }
 
 auto buildTransferMatchSwitch() {
@@ -334,7 +338,8 @@ auto buildBranchTransferMatchSwitch() {
 }
 
 auto buildDiagnoseMatchSwitch() {
-  return CFGMatchSwitchBuilder<const Environment, ReverseNullDiagnoser::ResultType>()
+  return CFGMatchSwitchBuilder<const Environment,
+                               ReverseNullDiagnoser::ResultType>()
       .CaseOfCFGStmt<CastExpr>(castExprMatcher(), diagnoseCastExpr)
       .Build();
 }
@@ -344,14 +349,14 @@ auto buildDiagnoseMatchSwitch() {
 ReverseNullModel::ReverseNullModel(ASTContext &Context)
     : DataflowAnalysis<ReverseNullModel, NoopLattice>(Context),
       TransferMatchSwitch(buildTransferMatchSwitch()),
-      BranchTransferMatchSwitch(buildBranchTransferMatchSwitch()) {
-}
+      BranchTransferMatchSwitch(buildBranchTransferMatchSwitch()) {}
 
 ast_matchers::StatementMatcher ReverseNullModel::ptrValueMatcher() {
   return ptrToVar();
 }
 
-void ReverseNullModel::initializeFunctionParameters(const ControlFlowContext &CFCtx, Environment &Env) {
+void ReverseNullModel::initializeFunctionParameters(
+    const ControlFlowContext &CFCtx, Environment &Env) {
   const FunctionDecl &FD = cast<FunctionDecl>(CFCtx.getDecl());
 
   for (const auto *Param : FD.parameters()) {
@@ -381,12 +386,12 @@ void ReverseNullModel::transfer(const CFGElement &E, NoopLattice &State,
   TransferMatchSwitch(E, getASTContext(), Env);
 }
 
-void ReverseNullModel::transferBranch(bool Branch, const Stmt *E, NoopLattice &State,
-                                      Environment &Env) {
+void ReverseNullModel::transferBranch(bool Branch, const Stmt *E,
+                                      NoopLattice &State, Environment &Env) {
   if (!E)
     return;
 
-  TransferArgs Args = { Branch, Env };
+  TransferArgs Args = {Branch, Env};
   BranchTransferMatchSwitch(*E, getASTContext(), Args);
 }
 
@@ -395,310 +400,319 @@ bool ReverseNullModel::merge(QualType Type, const Value &Val1,
                              const Environment &Env1, const Value &Val2,
                              const Environment &Env2, Value &MergedVal,
                              Environment &MergedEnv) {
-    if (!Type->isAnyPointerType())
-      return false; // FIXME: Maybe requires true?
-
-    // Alternative attempt: is any branch is true ie. can be a pointer, merging it is also a pointer
-    const auto FastMergeToTrue = [&](llvm::StringRef Name) -> BoolValue & {
-      BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
-      BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
+  if (!Type->isAnyPointerType())
+    return false; // FIXME: Maybe requires true?
 
-      SatisfiabilityResult lhsResult = computeSatisfiability(lhsVar, Env1);
-      SatisfiabilityResult rhsResult = computeSatisfiability(rhsVar, Env2);
+  // Alternative attempt: is any branch is true ie. can be a pointer, merging it
+  // is also a pointer
+  const auto FastMergeToTrue = [&](llvm::StringRef Name) -> BoolValue & {
+    BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
+    BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
 
-      if (lhsResult == SR::Top || rhsResult == SR::Top) 
-        return MergedEnv.makeTopBoolValue();
-      else if (lhsResult == SR::True || rhsResult == SR::True)
-        return MergedEnv.getBoolLiteralValue(true);
-      
-      if (lhsResult == SR::Nullptr && rhsResult == SR::Nullptr)
-        return MergedEnv.makeAtomicBoolValue();
-      else if (lhsResult == SR::False && rhsResult == SR::False)
-        return MergedEnv.getBoolLiteralValue(false);
+    SatisfiabilityResult lhsResult = computeSatisfiability(lhsVar, Env1);
+    SatisfiabilityResult rhsResult = computeSatisfiability(rhsVar, Env2);
 
+    if (lhsResult == SR::Top || rhsResult == SR::Top)
       return MergedEnv.makeTopBoolValue();
-    };
-    
-    // Attempt 1: Merge different values to Top.
-    const auto FastMergeValues = [&](llvm::StringRef Name) -> BoolValue & {
-      BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
-      BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
+    else if (lhsResult == SR::True || rhsResult == SR::True)
+      return MergedEnv.getBoolLiteralValue(true);
 
-      SatisfiabilityResult lhsResult = computeSatisfiability(lhsVar, Env1);
-      SatisfiabilityResult rhsResult = computeSatisfiability(rhsVar, Env2);
+    if (lhsResult == SR::Nullptr && rhsResult == SR::Nullptr)
+      return MergedEnv.makeAtomicBoolValue();
+    else if (lhsResult == SR::False && rhsResult == SR::False)
+      return MergedEnv.getBoolLiteralValue(false);
 
-      if (lhsResult == SR::Top || rhsResult == SR::Top) 
-        return MergedEnv.makeTopBoolValue();
-      
-      if (lhsResult == SR::Nullptr && rhsResult == SR::Nullptr)
-        return MergedEnv.makeAtomicBoolValue();
+    return MergedEnv.makeTopBoolValue();
+  };
 
-      if (lhsResult == SR::True || rhsResult == SR::True)
-        return MergedEnv.getBoolLiteralValue(true);
-      else if (lhsResult == SR::False && rhsResult == SR::False)
-        return MergedEnv.getBoolLiteralValue(false);
+  // Attempt 1: Merge different values to Top.
+  const auto FastMergeValues = [&](llvm::StringRef Name) -> BoolValue & {
+    BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
+    BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
+
+    SatisfiabilityResult lhsResult = computeSatisfiability(lhsVar, Env1);
+    SatisfiabilityResult rhsResult = computeSatisfiability(rhsVar, Env2);
 
+    if (lhsResult == SR::Top || rhsResult == SR::Top)
       return MergedEnv.makeTopBoolValue();
-    };
 
-    // Attempt 2: Slow evaluation, but only produces simple variables.
-    const auto MergeValues = [&](llvm::StringRef Name) -> BoolValue & {
-      BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
-      BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
+    if (lhsResult == SR::Nullptr && rhsResult == SR::Nullptr)
+      return MergedEnv.makeAtomicBoolValue();
 
-      SatisfiabilityResult lhsResult = computeSatisfiability(lhsVar, Env1);
-      SatisfiabilityResult rhsResult = computeSatisfiability(rhsVar, Env2);
+    if (lhsResult == SR::True || rhsResult == SR::True)
+      return MergedEnv.getBoolLiteralValue(true);
+    else if (lhsResult == SR::False && rhsResult == SR::False)
+      return MergedEnv.getBoolLiteralValue(false);
 
-      // Handle special cases.
-      if (lhsResult == SR::Top || rhsResult == SR::Top) {
-        return MergedEnv.makeTopBoolValue();
-      } else if (lhsResult == rhsResult) {
-        switch (lhsResult) {
-          case SR::Nullptr:
-            return MergedEnv.makeAtomicBoolValue();
-          case SR::Top:
-            return *lhsVar;
-          case SR::True:
-            return MergedEnv.getBoolLiteralValue(true);
-          case SR::False:
-            return MergedEnv.getBoolLiteralValue(false);
-          case SR::Unknown:
-            if (MergedEnv.flowConditionImplies(MergedEnv.arena().makeEquals(lhsVar->formula(), rhsVar->formula())))
-              return *lhsVar;
-            
-            return MergedEnv.makeTopBoolValue();
-        }
-      }
+    return MergedEnv.makeTopBoolValue();
+  };
 
-      return MergedEnv.makeTopBoolValue();
-    };
+  // Attempt 2: Slow evaluation, but only produces simple variables.
+  const auto MergeValues = [&](llvm::StringRef Name) -> BoolValue & {
+    BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
+    BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
 
-    // Attempt 3: Merge to (L or R), a more complex variable
-    const auto SlowMergeValues = [&](llvm::StringRef Name) -> BoolValue & {
-      BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
-      BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
+    SatisfiabilityResult lhsResult = computeSatisfiability(lhsVar, Env1);
+    SatisfiabilityResult rhsResult = computeSatisfiability(rhsVar, Env2);
 
-      SatisfiabilityResult lhsResult = computeSatisfiability(lhsVar, Env1);
-      SatisfiabilityResult rhsResult = computeSatisfiability(rhsVar, Env2);
+    // Handle special cases.
+    if (lhsResult == SR::Top || rhsResult == SR::Top) {
+      return MergedEnv.makeTopBoolValue();
+    } else if (lhsResult == rhsResult) {
+      switch (lhsResult) {
+      case SR::Nullptr:
+        return MergedEnv.makeAtomicBoolValue();
+      case SR::Top:
+        return *lhsVar;
+      case SR::True:
+        return MergedEnv.getBoolLiteralValue(true);
+      case SR::False:
+        return MergedEnv.getBoolLiteralValue(false);
+      case SR::Unknown:
+        if (MergedEnv.flowConditionImplies(MergedEnv.arena().makeEquals(
+                lhsVar->formula(), rhsVar->formula())))
+          return *lhsVar;
 
-      // Handle special cases.
-      if (lhsResult == SR::Top || rhsResult == SR::Top) {
         return MergedEnv.makeTopBoolValue();
-      } else if (lhsResult == rhsResult) {
-        switch (lhsResult) {
-          case SR::Nullptr:
-            return MergedEnv.makeAtomicBoolValue();
-          case SR::Top:
-            return *lhsVar;
-          case SR::True:
-            return MergedEnv.getBoolLiteralValue(true);
-          case SR::False:
-            return MergedEnv.getBoolLiteralValue(false);
-          case SR::Unknown:
-            break;
-        }
       }
-      
-      const Formula *mergedLhsVar;
-      const Formula *mergedRhsVar;
+    }
+
+    return MergedEnv.makeTopBoolValue();
+  };
 
-      Arena &A = MergedEnv.arena();
-      const Formula *lhsToken = &A.makeAtomRef(Env1.getFlowConditionToken());
-      const Formula *rhsToken = &A.makeAtomRef(Env2.getFlowConditionToken());
+  // Attempt 3: Merge to (L or R), a more complex variable
+  const auto SlowMergeValues = [&](llvm::StringRef Name) -> BoolValue & {
+    BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
+    BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
 
+    SatisfiabilityResult lhsResult = computeSatisfiability(lhsVar, Env1);
+    SatisfiabilityResult rhsResult = computeSatisfiability(rhsVar, Env2);
 
+    // Handle special cases.
+    if (lhsResult == SR::Top || rhsResult == SR::Top) {
+      return MergedEnv.makeTopBoolValue();
+    } else if (lhsResult == rhsResult) {
       switch (lhsResult) {
-        case SR::Nullptr:
-        case SR::Top: // would have returned earlier
-          mergedLhsVar = nullptr;
-          break;
-        case SR::True:
-          mergedLhsVar = lhsToken;
-          break;
-        case SR::False:
-          mergedLhsVar = &A.makeNot(*lhsToken);
-          break;
-        case SR::Unknown:
-          mergedLhsVar = &A.makeImplies(*lhsToken, lhsVar->formula());
-          break;
+      case SR::Nullptr:
+        return MergedEnv.makeAtomicBoolValue();
+      case SR::Top:
+        return *lhsVar;
+      case SR::True:
+        return MergedEnv.getBoolLiteralValue(true);
+      case SR::False:
+        return MergedEnv.getBoolLiteralValue(false);
+      case SR::Unknown:
+        break;
       }
+    }
 
-      switch (rhsResult) {
-        case SR::Nullptr:
-        case SR::Top:
-          mergedRhsVar = nullptr;
-          break;
-        case SR::True:
-          mergedRhsVar = rhsToken;
-          break;
-        case SR::False:
-          mergedRhsVar = &A.makeNot(*rhsToken);
-          break;
-        case SR::Unknown:
-          mergedRhsVar = &A.makeImplies(*rhsToken, rhsVar->formula());
-          break;
-      }
+    const Formula *mergedLhsVar;
+    const Formula *mergedRhsVar;
+
+    Arena &A = MergedEnv.arena();
+    const Formula *lhsToken = &A.makeAtomRef(Env1.getFlowConditionToken());
+    const Formula *rhsToken = &A.makeAtomRef(Env2.getFlowConditionToken());
+
+    switch (lhsResult) {
+    case SR::Nullptr:
+    case SR::Top: // would have returned earlier
+      mergedLhsVar = nullptr;
+      break;
+    case SR::True:
+      mergedLhsVar = lhsToken;
+      break;
+    case SR::False:
+      mergedLhsVar = &A.makeNot(*lhsToken);
+      break;
+    case SR::Unknown:
+      mergedLhsVar = &A.makeImplies(*lhsToken, lhsVar->formula());
+      break;
+    }
 
-      if (!lhsVar && !rhsVar)
-        return MergedEnv.makeAtomicBoolValue();
-      else if (!lhsVar)
-        return A.makeBoolValue(*mergedRhsVar);
-      else if (!rhsVar)
-        return A.makeBoolValue(*mergedLhsVar);
-      else
-        return A.makeBoolValue(A.makeOr(*mergedLhsVar, *mergedRhsVar));
-    };
+    switch (rhsResult) {
+    case SR::Nullptr:
+    case SR::Top:
+      mergedRhsVar = nullptr;
+      break;
+    case SR::True:
+      mergedRhsVar = rhsToken;
+      break;
+    case SR::False:
+      mergedRhsVar = &A.makeNot(*rhsToken);
+      break;
+    case SR::Unknown:
+      mergedRhsVar = &A.makeImplies(*rhsToken, rhsVar->formula());
+      break;
+    }
 
-    BoolValue &NonnullValue = FastMergeValues(kIsNonnull);
-    BoolValue &NullValue = FastMergeValues(kIsNull);
+    if (!lhsVar && !rhsVar)
+      return MergedEnv.makeAtomicBoolValue();
+    else if (!lhsVar)
+      return A.makeBoolValue(*mergedRhsVar);
+    else if (!rhsVar)
+      return A.makeBoolValue(*mergedLhsVar);
+    else
+      return A.makeBoolValue(A.makeOr(*mergedLhsVar, *mergedRhsVar));
+  };
 
-    MergedVal.setProperty(kIsNonnull, NonnullValue);
-    MergedVal.setProperty(kIsNull, NullValue);
+  BoolValue &NonnullValue = FastMergeValues(kIsNonnull);
+  BoolValue &NullValue = FastMergeValues(kIsNull);
 
-    MergedEnv.addToFlowCondition(MergedEnv.makeOr(NonnullValue, NullValue).formula());
+  MergedVal.setProperty(kIsNonnull, NonnullValue);
+  MergedVal.setProperty(kIsNull, NullValue);
 
-    return true;
+  MergedEnv.addToFlowCondition(
+      MergedEnv.makeOr(NonnullValue, NullValue).formula());
+
+  return true;
 }
 
-ComparisonResult ReverseNullModel::compare(QualType Type,
-        const Value &Val1, const Environment &Env1,
-        const Value &Val2, const Environment &Env2) {
+ComparisonResult ReverseNullModel::compare(QualType Type, const Value &Val1,
+                                           const Environment &Env1,
+                                           const Value &Val2,
+                                           const Environment &Env2) {
 
-    if (!Type->isAnyPointerType())
-      return ComparisonResult::Unknown;
+  if (!Type->isAnyPointerType())
+    return ComparisonResult::Unknown;
 
-    // Attempt 1: Different values by pointer compare Unknown, Top to Different, same to Same.
-    auto FastCompareValues = [&](llvm::StringRef Name) -> ComparisonResult {
-      BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
-      BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
+  // Attempt 1: Different values by pointer compare Unknown, Top to Different,
+  // same to Same.
+  auto FastCompareValues = [&](llvm::StringRef Name) -> ComparisonResult {
+    BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
+    BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
 
-      SatisfiabilityResult lhsResult = shallowComputeSatisfiability(lhsVar, Env1);
-      SatisfiabilityResult rhsResult = shallowComputeSatisfiability(rhsVar, Env2);
+    SatisfiabilityResult lhsResult = shallowComputeSatisfiability(lhsVar, Env1);
+    SatisfiabilityResult rhsResult = shallowComputeSatisfiability(rhsVar, Env2);
 
-      if (lhsResult == SR::Top || rhsResult == SR::Top)
-        return ComparisonResult::Same; // FIXME: Should this be different?
+    if (lhsResult == SR::Top || rhsResult == SR::Top)
+      return ComparisonResult::Same; // FIXME: Should this be different?
 
-      if (lhsResult == SR::Unknown || rhsResult == SR::Unknown)
-        return ComparisonResult::Unknown;
-      
-      if (lhsResult == rhsResult)
-        return ComparisonResult::Same;
+    if (lhsResult == SR::Unknown || rhsResult == SR::Unknown)
+      return ComparisonResult::Unknown;
 
-      return ComparisonResult::Different;
-    };
+    if (lhsResult == rhsResult)
+      return ComparisonResult::Same;
 
-    // Attempt 2: Evaluate values, but different values compare to Unknown.
-    auto CompareValues = [&](llvm::StringRef Name) -> ComparisonResult {
-      BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
-      BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
+    return ComparisonResult::Different;
+  };
 
-      SatisfiabilityResult lhsResult = computeSatisfiability(lhsVar, Env1);
-      SatisfiabilityResult rhsResult = computeSatisfiability(rhsVar, Env2);
+  // Attempt 2: Evaluate values, but different values compare to Unknown.
+  auto CompareValues = [&](llvm::StringRef Name) -> ComparisonResult {
+    BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
+    BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
 
-      if (lhsResult == SR::Top || rhsResult == SR::Top)
-        return ComparisonResult::Same; // FIXME: Should this be different?
+    SatisfiabilityResult lhsResult = computeSatisfiability(lhsVar, Env1);
+    SatisfiabilityResult rhsResult = computeSatisfiability(rhsVar, Env2);
 
-      if (lhsResult == SR::Unknown || rhsResult == SR::Unknown)
-        return ComparisonResult::Unknown;
-      
-      if (lhsResult == rhsResult)
-        return ComparisonResult::Same;
+    if (lhsResult == SR::Top || rhsResult == SR::Top)
+      return ComparisonResult::Same; // FIXME: Should this be different?
 
-      return ComparisonResult::Different;
-    };
+    if (lhsResult == SR::Unknown || rhsResult == SR::Unknown)
+      return ComparisonResult::Unknown;
 
-    ComparisonResult NullComparison = FastCompareValues(kIsNull);
-    ComparisonResult NonnullComparison = FastCompareValues(kIsNonnull);
+    if (lhsResult == rhsResult)
+      return ComparisonResult::Same;
 
-    if (NullComparison == ComparisonResult::Different || NonnullComparison == ComparisonResult::Different)
-      return ComparisonResult::Different;
+    return ComparisonResult::Different;
+  };
 
-    if (NullComparison == ComparisonResult::Unknown || NonnullComparison == ComparisonResult::Unknown)
-      return ComparisonResult::Unknown;
+  ComparisonResult NullComparison = FastCompareValues(kIsNull);
+  ComparisonResult NonnullComparison = FastCompareValues(kIsNonnull);
 
-    return ComparisonResult::Same;
-}
+  if (NullComparison == ComparisonResult::Different ||
+      NonnullComparison == ComparisonResult::Different)
+    return ComparisonResult::Different;
 
-// Different in that it replaces differing boolean values with Top.
-ComparisonResult compareAndReplace(QualType Type,
-        Value &Val1, const Environment &Env1,
-        Value &Val2, Environment &Env2) {
+  if (NullComparison == ComparisonResult::Unknown ||
+      NonnullComparison == ComparisonResult::Unknown)
+    return ComparisonResult::Unknown;
 
-    if (!Type->isAnyPointerType())
-      return ComparisonResult::Unknown;
+  return ComparisonResult::Same;
+}
 
-    // Attempt 1: Different values by pointer compare Unknown, Top to Different, same to Same.
-    auto FastCompareValues = [&](llvm::StringRef Name) -> ComparisonResult {
-      BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
-      BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
+// Different in that it replaces differing boolean values with Top.
+ComparisonResult compareAndReplace(QualType Type, Value &Val1,
+                                   const Environment &Env1, Value &Val2,
+                                   Environment &Env2) {
 
-      SatisfiabilityResult lhsResult = shallowComputeSatisfiability(lhsVar, Env1);
-      SatisfiabilityResult rhsResult = shallowComputeSatisfiability(rhsVar, Env2);
+  if (!Type->isAnyPointerType())
+    return ComparisonResult::Unknown;
 
-      if (lhsResult == SR::Top || rhsResult == SR::Top) {
-        Val2.setProperty(Name, Env2.makeTopBoolValue());
-        return ComparisonResult::Same; // FIXME: Should this be different?
-      }
+  // Attempt 1: Different values by pointer compare Unknown, Top to Different,
+  // same to Same.
+  auto FastCompareValues = [&](llvm::StringRef Name) -> ComparisonResult {
+    BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
+    BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
 
-      if (lhsResult == SR::Unknown || rhsResult == SR::Unknown)
-        return ComparisonResult::Unknown;
-      
-      if (lhsResult == rhsResult)
-        return ComparisonResult::Same;
+    SatisfiabilityResult lhsResult = shallowComputeSatisfiability(lhsVar, Env1);
+    SatisfiabilityResult rhsResult = shallowComputeSatisfiability(rhsVar, Env2);
 
+    if (lhsResult == SR::Top || rhsResult == SR::Top) {
       Val2.setProperty(Name, Env2.makeTopBoolValue());
-      return ComparisonResult::Different;
-    };
+      return ComparisonResult::Same; // FIXME: Should this be different?
+    }
 
-    // Attempt 2: Evaluate values, but different values compare to Unknown.
-    auto CompareValues = [&](llvm::StringRef Name) -> ComparisonResult {
-      BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
-      BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
+    if (lhsResult == SR::Unknown || rhsResult == SR::Unknown)
+      return ComparisonResult::Unknown;
 
-      SatisfiabilityResult lhsResult = computeSatisfiability(lhsVar, Env1);
-      SatisfiabilityResult rhsResult = computeSatisfiability(rhsVar, Env2);
+    if (lhsResult == rhsResult)
+      return ComparisonResult::Same;
 
-      if (lhsResult == SR::Top || rhsResult == SR::Top) {
-        Val2.setProperty(Name, Env2.makeTopBoolValue());
-        return ComparisonResult::Same; // FIXME: Should this be different?
-      }
+    Val2.setProperty(Name, Env2.makeTopBoolValue());
+    return ComparisonResult::Different;
+  };
 
-      if (lhsResult == SR::Unknown || rhsResult == SR::Unknown)
-        return ComparisonResult::Unknown;
-      
-      if (lhsResult == rhsResult)
-        return ComparisonResult::Same;
+  // Attempt 2: Evaluate values, but different values compare to Unknown.
+  auto CompareValues = [&](llvm::StringRef Name) -> ComparisonResult {
+    BoolValue *lhsVar = cast_or_null<BoolValue>(Val1.getProperty(Name));
+    BoolValue *rhsVar = cast_or_null<BoolValue>(Val2.getProperty(Name));
 
+    SatisfiabilityResult lhsResult = computeSatisfiability(lhsVar, Env1);
+    SatisfiabilityResult rhsResult = computeSatisfiability(rhsVar, Env2);
+
+    if (lhsResult == SR::Top || rhsResult == SR::Top) {
       Val2.setProperty(Name, Env2.makeTopBoolValue());
-      return ComparisonResult::Different;
-    };
+      return ComparisonResult::Same; // FIXME: Should this be different?
+    }
+
+    if (lhsResult == SR::Unknown || rhsResult == SR::Unknown)
+      return ComparisonResult::Unknown;
 
-    ComparisonResult NullComparison = FastCompareValues(kIsNull);
-    ComparisonResult NonnullComparison = FastCompareValues(kIsNonnull);
+    if (lhsResult == rhsResult)
+      return ComparisonResult::Same;
 
-    if (NullComparison == ComparisonResult::Different || NonnullComparison == ComparisonResult::Different)
-      return ComparisonResult::Different;
+    Val2.setProperty(Name, Env2.makeTopBoolValue());
+    return ComparisonResult::Different;
+  };
 
-    if (NullComparison == ComparisonResult::Unknown || NonnullComparison == ComparisonResult::Unknown)
-      return ComparisonResult::Unknown;
+  ComparisonResult NullComparison = FastCompareValues(kIsNull);
+  ComparisonResult NonnullComparison = FastCompareValues(kIsNonnull);
+
+  if (NullComparison == ComparisonResult::Different ||
+      NonnullComparison == ComparisonResult::Different)
+    return ComparisonResult::Different;
 
-    return ComparisonResult::Same;
+  if (NullComparison == ComparisonResult::Unknown ||
+      NonnullComparison == ComparisonResult::Unknown)
+    return ComparisonResult::Unknown;
+
+  return ComparisonResult::Same;
 }
 
-Value *ReverseNullModel::widen(QualType Type,
-                               Value &Prev, const Environment &PrevEnv,
-                               Value &Current, Environment &CurrentEnv) {
-    if (!Type->isAnyPointerType()) 
-      return nullptr;
+Value *ReverseNullModel::widen(QualType Type, Value &Prev,
+                               const Environment &PrevEnv, Value &Current,
+                               Environment &CurrentEnv) {
+  if (!Type->isAnyPointerType())
+    return nullptr;
 
-    switch (compareAndReplace(Type, Prev, PrevEnv, Current, CurrentEnv)) {
-      case ComparisonResult::Same:
-        return &Prev;
-      case ComparisonResult::Unknown:
-        return nullptr;
-      case ComparisonResult::Different:
-        return &Current; // FIXME: Replace with Tops in compareAndReplace
-      }
+  switch (compareAndReplace(Type, Prev, PrevEnv, Current, CurrentEnv)) {
+  case ComparisonResult::Same:
+    return &Prev;
+  case ComparisonResult::Unknown:
+    return nullptr;
+  case ComparisonResult::Different:
+    return &Current; // FIXME: Replace with Tops in compareAndReplace
+  }
 }
 
 ReverseNullDiagnoser::ReverseNullDiagnoser()
diff --git a/clang/unittests/Analysis/FlowSensitive/ReverseNullModelTest.cpp b/clang/unittests/Analysis/FlowSensitive/ReverseNullModelTest.cpp
index 6e4148bf4..4d0b933bc 100644
--- a/clang/unittests/Analysis/FlowSensitive/ReverseNullModelTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ReverseNullModelTest.cpp
@@ -6,7 +6,7 @@
 //
 //===----------------------------------------------------------------------===//
 //
-//  This file defines a test for pointer nullability, specifically focused on 
+//  This file defines a test for pointer nullability, specifically focused on
 //  finding invalid dereferences, and unnecessary null-checks. Only a limited
 //  set of operations are currently recognized.
 //
@@ -14,6 +14,7 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include "clang/Analysis/FlowSensitive/Models/ReverseNullModel.h"
 #include "TestingSupport.h"
 #include "clang/AST/ASTContext.h"
 #include "clang/AST/Decl.h"
@@ -28,7 +29,6 @@
 #include "clang/Analysis/FlowSensitive/DataflowLattice.h"
 #include "clang/Analysis/FlowSensitive/MapLattice.h"
 #include "clang/Analysis/FlowSensitive/NoopLattice.h"
-#include "clang/Analysis/FlowSensitive/Models/ReverseNullModel.h"
 #include "llvm/ADT/StringRef.h"
 #include "llvm/ADT/Twine.h"
 #include "llvm/Support/Error.h"
@@ -61,7 +61,7 @@ constexpr char kBoolInvalid[] = "truefalse";
 constexpr char kBoolUnknown[] = "unknown";
 constexpr char kBoolNullptr[] = "is-nullptr";
 
-std::string debugBoolValue(BoolValue *value, const Environment &Env) { 
+std::string debugBoolValue(BoolValue *value, const Environment &Env) {
   if (value == nullptr) {
     return std::string(kBoolNullptr);
   } else {
@@ -77,46 +77,42 @@ std::string debugBoolValue(BoolValue *value, const Environment &Env) {
 }
 
 auto ptrToVar() { return declRefExpr(hasType(isAnyPointer())).bind(kVar); }
-auto namedPtrToVar(llvm::StringRef name) { 
+auto namedPtrToVar(llvm::StringRef name) {
   return declRefExpr(allOf(hasType(isAnyPointer()),
-                     hasDeclaration(namedDecl(hasName(name)))
-  )).bind(kVar); 
+                           hasDeclaration(namedDecl(hasName(name)))))
+      .bind(kVar);
 }
 
 auto nameToVar(llvm::StringRef name) {
-  return declRefExpr(hasType(isAnyPointer()), hasDeclaration(
-    namedDecl(hasName(name))
-  )).bind(kVar);
+  return declRefExpr(hasType(isAnyPointer()),
+                     hasDeclaration(namedDecl(hasName(name))))
+      .bind(kVar);
 }
 
 auto voidCastMatcher() {
-  return stmt(hasDescendant(castExpr(hasCastKind(CK_ToVoid), 
-    hasSourceExpression(ptrToVar())
-  )));
+  return stmt(hasDescendant(
+      castExpr(hasCastKind(CK_ToVoid), hasSourceExpression(ptrToVar()))));
 }
 
 auto derefMatcher() {
-  return traverse(TK_IgnoreUnlessSpelledInSource,
-    unaryOperator(
-      hasOperatorName("*"),
-      hasUnaryOperand(ptrToVar())
-    )
-  );
+  return traverse(
+      TK_IgnoreUnlessSpelledInSource,
+      unaryOperator(hasOperatorName("*"), hasUnaryOperand(ptrToVar())));
 }
 
 // FIXME: Deliberately simple - a proper check would only match direct ptr casts
 auto castExprMatcher() {
-  return castExpr(hasCastKind(CK_PointerToBoolean), 
-      hasSourceExpression(ptrToVar())).bind(kCond)
-  ;
+  return castExpr(hasCastKind(CK_PointerToBoolean),
+                  hasSourceExpression(ptrToVar()))
+      .bind(kCond);
 }
 
 using ::clang::dataflow::test::AnalysisInputs;
 using ::clang::dataflow::test::AnalysisOutputs;
 using ::clang::dataflow::test::checkDataflow;
 using ::llvm::IsStringMapEntry;
-using ::testing::Pair;
 using ::testing::Args;
+using ::testing::Pair;
 using ::testing::UnorderedElementsAre;
 
 MATCHER_P2(HasNullabilityState, null, nonnull, "") {
@@ -128,14 +124,14 @@ MATCHER_P2(HasNullabilityState, null, nonnull, "") {
              *arg.second) == null;
 }
 
-MATCHER_P3(HoldsVariable, name, output, checks, 
-          ((negation ? "doesn't hold" : "holds") +
+MATCHER_P3(HoldsVariable, name, output, checks,
+           ((negation ? "doesn't hold" : "holds") +
             llvm::StringRef(" a variable in its environment that ") +
-            ::testing::DescribeMatcher<std::pair<Value *, Environment *>>(checks, negation)
-          ).str()) {
+            ::testing::DescribeMatcher<std::pair<Value *, Environment *>>(
+                checks, negation))
+               .str()) {
   auto MatchResults = match(functionDecl(hasDescendant(nameToVar(name))),
-                            *output.Target,
-                            output.ASTCtx);
+                            *output.Target, output.ASTCtx);
   // FIXME: Use gtest functions
   assert(!MatchResults.empty());
 
@@ -143,12 +139,13 @@ MATCHER_P3(HoldsVariable, name, output, checks,
   assert(pointerExpr != nullptr);
 
   const auto *ExprValue = arg.Env.getValue(*pointerExpr);
-  
+
   if (ExprValue == nullptr) {
     return false;
   }
 
-  return ExplainMatchResult(checks, std::pair { ExprValue, &arg.Env }, result_listener);
+  return ExplainMatchResult(checks, std::pair{ExprValue, &arg.Env},
+                            result_listener);
 }
 
 template <typename MatcherFactory>
@@ -166,15 +163,17 @@ void ExpectDataflowResult(llvm::StringRef Code, MatcherFactory Expectations) {
               })
               .withSetupTest([&InitEnv](AnalysisOutputs &AO) {
                 assert(InitEnv && "SetupTest ran at an unexpected time");
-                ReverseNullModel &Analysis = static_cast<ReverseNullModel&>(AO.Analysis);
+                ReverseNullModel &Analysis =
+                    static_cast<ReverseNullModel &>(AO.Analysis);
                 Analysis.initializeFunctionParameters(AO.CFCtx, *InitEnv);
                 return llvm::Error::success();
               })
               .withASTBuildArgs({"-fsyntax-only", "-std=c++17"}),
           /*VerifyResults=*/
-          [&Expectations](const llvm::StringMap<DataflowAnalysisState<
-                              ReverseNullModel::Lattice>> &Results,
-                          const AnalysisOutputs &Output) {
+          [&Expectations](
+              const llvm::StringMap<
+                  DataflowAnalysisState<ReverseNullModel::Lattice>> &Results,
+              const AnalysisOutputs &Output) {
             EXPECT_THAT(Results, Expectations(Output));
           }),
       llvm::Succeeded());
@@ -194,10 +193,12 @@ TEST(ReverseNullTest, DereferenceTypes) {
   )";
   ExpectDataflowResult(Code, [](const AnalysisOutputs &Output) -> auto {
     return UnorderedElementsAre(
-        IsStringMapEntry("p", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolFalse, kBoolTrue))),
-        IsStringMapEntry("q", HoldsVariable("q", Output,
-            HasNullabilityState(kBoolFalse, kBoolTrue))));
+        IsStringMapEntry(
+            "p", HoldsVariable("p", Output,
+                               HasNullabilityState(kBoolFalse, kBoolTrue))),
+        IsStringMapEntry(
+            "q", HoldsVariable("q", Output,
+                               HasNullabilityState(kBoolFalse, kBoolTrue))));
   });
 }
 
@@ -216,9 +217,11 @@ TEST(ReverseNullTest, ConditionalTypes) {
   ExpectDataflowResult(Code, [](const AnalysisOutputs &Output) -> auto {
     return UnorderedElementsAre(
         IsStringMapEntry("p_true", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolFalse, kBoolTrue))),
+                                                 HasNullabilityState(
+                                                     kBoolFalse, kBoolTrue))),
         IsStringMapEntry("p_false", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolTrue, kBoolFalse))));
+                                                  HasNullabilityState(
+                                                      kBoolTrue, kBoolFalse))));
   });
 }
 
@@ -248,17 +251,27 @@ TEST(ReverseNullTest, UnrelatedCondition) {
   ExpectDataflowResult(Code, [](const AnalysisOutputs &Output) -> auto {
     return UnorderedElementsAre(
         IsStringMapEntry("p_b_true", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolFalse, kBoolTrue))),
-        IsStringMapEntry("p_b_false", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolUnknown, kBoolUnknown))),
-        IsStringMapEntry("p_merged", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolUnknown, kBoolUnknown))),
+                                                   HasNullabilityState(
+                                                       kBoolFalse, kBoolTrue))),
+        IsStringMapEntry(
+            "p_b_false",
+            HoldsVariable("p", Output,
+                          HasNullabilityState(kBoolUnknown, kBoolUnknown))),
+        IsStringMapEntry(
+            "p_merged",
+            HoldsVariable("p", Output,
+                          HasNullabilityState(kBoolUnknown, kBoolUnknown))),
         IsStringMapEntry("b_true", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolFalse, kBoolTrue))),
+                                                 HasNullabilityState(
+                                                     kBoolFalse, kBoolTrue))),
         IsStringMapEntry("b_p_true", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolInvalid, kBoolInvalid))), // FIXME
-        IsStringMapEntry("b_p_false", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolInvalid, kBoolInvalid))));
+                                                   HasNullabilityState(
+                                                       kBoolInvalid,
+                                                       kBoolInvalid))), // FIXME
+        IsStringMapEntry(
+            "b_p_false",
+            HoldsVariable("p", Output,
+                          HasNullabilityState(kBoolInvalid, kBoolInvalid))));
   });
 }
 
@@ -287,17 +300,28 @@ TEST(ReverseNullTest, AssignmentOfCommonValues) {
   ExpectDataflowResult(Code, [](const AnalysisOutputs &Output) -> auto {
     return UnorderedElementsAre(
         IsStringMapEntry("p_malloc", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolNullptr, kBoolNullptr))), // FIXME
+                                                   HasNullabilityState(
+                                                       kBoolNullptr,
+                                                       kBoolNullptr))), // FIXME
         IsStringMapEntry("p_true", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolFalse, kBoolTrue))),
+                                                 HasNullabilityState(
+                                                     kBoolFalse, kBoolTrue))),
         IsStringMapEntry("p_false", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolTrue, kBoolFalse))),
-        IsStringMapEntry("p_merge", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolUnknown, kBoolUnknown))),
-        IsStringMapEntry("p_nullptr", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolNullptr, kBoolNullptr))), // FIXME
-        IsStringMapEntry("p_extern", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolUnknown, kBoolUnknown))));
+                                                  HasNullabilityState(
+                                                      kBoolTrue, kBoolFalse))),
+        IsStringMapEntry(
+            "p_merge",
+            HoldsVariable("p", Output,
+                          HasNullabilityState(kBoolUnknown, kBoolUnknown))),
+        IsStringMapEntry(
+            "p_nullptr",
+            HoldsVariable(
+                "p", Output,
+                HasNullabilityState(kBoolNullptr, kBoolNullptr))), // FIXME
+        IsStringMapEntry(
+            "p_extern",
+            HoldsVariable("p", Output,
+                          HasNullabilityState(kBoolUnknown, kBoolUnknown))));
   });
 }
 
@@ -317,9 +341,10 @@ TEST(ReverseNullTest, MergeValues) {
     }
   )";
   ExpectDataflowResult(Code, [](const AnalysisOutputs &Output) -> auto {
-    return UnorderedElementsAre(
-        IsStringMapEntry("p_merge", HoldsVariable("p", Output,
-            HasNullabilityState(kBoolUnknown, kBoolTrue))));
+    return UnorderedElementsAre(IsStringMapEntry(
+        "p_merge",
+        HoldsVariable("p", Output,
+                      HasNullabilityState(kBoolUnknown, kBoolTrue))));
   });
 }
 

[whisperity]

I will detail my high-level comments first before delving into the nitty-gritty of the source code. At face value, and immediately looking at the very first line in the header, I got slapped in the face with the check's name as it stands right now. I really, really do not like it... If I only go off of the check's name and search Google for reverse null, the first possibly related idea (REVERSE_INULL False Positive “Dereference before NULL check" at Synopsys Coverity Community) in the result list is at the 7th position. Granted, other search engines like DDG or Bing show in 1st or 2nd location the "what is difference between REVERSE_INULL and FORWARD_NULL error in coverity scan(static code analysis)?" at Stack Overflow. It begs the question what does I mean in INULL anyway...??? Note, the only answer here is a guy who admittedly "used to work for Synopsys". Also, even with DDG and Bing, most of the results are completely derailing, unrelated things like operator ?./?[] (something I really love, btw...) in C# and whatnot.

The problem here is that to understand from the general name of the check what we are trying to achieve requires either:

• knowing the related Coverity analysis rule
• knowing the theoretical details of dataflow-based analyses

Both of these would mean the user is already seasoned in static analysis. They likely are not, especially when it comes to people who just drive Clang-Tidy through things like coc-clangd or CLion.

Thus, I would like to say that we should give some consideration to the check's name. I think a longer but more informative name (to everyday developers not knowledgeable about this field) would be preferable to a concise but very internal name. Something along the lines of bugprone-null-check-after-dereference? That could capture the meaning nicely.

---

I think we should consider whether this is truly just bug_prone_ in the first place. Assuming the pointer was indeed null, if you have already dereferenced it by the time you reached the condition, you are definitely not null, because otherwise the program "should have" crashed, right? Or am I missing something and this is a too simple overview?

[whisperity]

Partial review for now. Unfortunately, I need to leave my work now, I will likely continue from another location tomorrow, and I do not know whether GitHub saves pending reviews clientside or serverside...

[whisperity]

✏️ (Style nit: stale empty line.)

[whisperity]

(Nit: It would be beneficial if this "limited set" was explained. What important bits that are meaningfully missing?)

[Discookie]

Will be documented.

[whisperity]

✏️ (Style nit: LLVM is now in C++17, so nested namespace specifiers namespace clang::tidy::bugprone could be used instead.)

[whisperity]

(Maybe this could spell "invalid" instead. Thinking about truefalse its not immediately apparent whether this means "true AND false" or "true OR false", and those are not the same things.)

[Discookie]

truefalse was just more convenient, but I will rework the debugBoolValue function that uses this.

[whisperity]

I'm not sure what is the convention for clang/unittests, but similar constructs in Clang-Tidy are usually expressed in the form of static const auto objects allocated directly in the TU for the check's implementation. (For matchers that take a parameter, the AST_MATCHER_P macro creates the appropriate matcher class.)

These factory functions can be simplified:

• For matchers that do not have parameters and do not require imperative logic, a static const(expr?) auto X = matcher(foo()); object that lives only once can express the needed logic.
• For matchers that do require imperative logic, AST_MATCHER can create the appropriately named matcher.
• Similarly, where parameters are needed, AST_MATCHER_P does the same thing.

[Discookie]

Indeed it does do the same thing. Ultimately I think instead of redefining matchers here, the ones from the ReverseNullModel itself should be somehow used.

[whisperity]

What is the hack here? What happens if the hack is removed, or how should it disappear?

[Discookie]

See the other hack.

[whisperity]

What are the semantics of this return value? At the definition of the type alias, it is only said it's a pair of Loc vectors. How is it special if one part of the pair has elements, and how if the other. Is it possible that BOTH vectors will contain an element?

[Discookie]

Not documented, and will most likely be changed. One is for checking when the value is definitely not-null, and the other is for checking when the value is definitely null.

[whisperity]

How is "any pointer" a "function call"?

[Discookie]

Should be named the other way around, fixed.

[whisperity]

Can be a pointer, or can be a null pointer?
Does "can be a pointer" mean that it is not null?

[Discookie]

Can be non-null.

[whisperity]

✏️ (My problem with having a default: here is that this kills -Wswitch, but I guess because not all branches of the switch actually return we can't really do any better than this... ☹️)

[whisperity]

Moreover, I have an architectural question as I just got to where the various alternative heuristics for calculating stuff are implemented. Could we somehow verify that alternates get the same consistent results somehow? If this is not feasible at low-level (i.e., running each alternate and comparing that they report the same value), then perhaps we should keep the alternates until the end so when the checker is ready for real-life testing on projects, we can run different configurations, and compare the user-facing reports from Tidy? Is this a good idea, even, or am I overthinking it? I see somewhere you mentioned things could simply just not conclude (and hey, bugprone-unchecked-optional-access at least used to infinitely hang; it might still do so...), so comparing the results eagerly inside the framework from all alternatives might not be a good idea.

Also, a schematic ASCII art for the lattice would be nice to have. (See the "Why are there 5 values?" question. So far, I don't know.)

[whisperity]

If you can find this tomorrow, pending reviews are saved serverside.

[Discookie]

yay!

[whisperity]

✏️ (Mismatch between file name and what is written in this comment.)

[whisperity]

I think the high-level idea is convincing. In general, the presentation and the understandability of the code need to be improved. I did this review only by reading what's in the code without going into your external presentations and documents. I'm happy to look at them now, but the code in itself should still be capable of explaining what is going on and why it is going on.

[whisperity]

I've started running the check in the usual CI, and so far, there were no findings or no errors, but in TinyXML's xmltest.cpp, Clang-Tidy locked up. Almost constant 100% CPU use... I allowed it to go for 30 minutes at this point. To unblock the CI, I killed the job, so we'll be seeing what the results are for other projects...

There were some more hangs with the same symptoms, which I killed after letting the jobs stagnate for about 15-30 minutes, on libwebm (sample.cpp, sample_muxer.cpp, and mkvparser.cpp), Xerces-C (39 out of 348 hung), bitcoin (11 out of 251), protobuf (16 out of 161, but I think 1 of these were an explicit crash!), Qt (it doesn't even matter how many TUs failed; basically everything kept on hanging, so I killed the full analyze job...), Contour (2 out of 180 hung, +2 quick crashes), RCT2 (33 out of 541, but some of these were quick failing crashes). Likely, the analysis of llvm-project will behave similarly to Qt, and not conclude meaningfully in a reasonable time...

[whisperity]

As discussed earlier today, if the checker is known to be crashy or hangy, we should preemptively forbid clangd from exercising it, as shown in this patch: llvm#69427

[whisperity]

In general, I think the implementation is now much better understandable (also given the fact that this was the 2nd pass over the code). There are some crucial pain points that still need to be improved, however:

1. The diagnostic output should be reviewed, especially this "Can we get to 'the' previous dereference?"-esque questions. If not, then at least the Checker's CPP file should contain a comment about this...
2. The documentation file for the checker has a lot of spotty parts. I tried to give as many comments as I could. There are some conflated terminologies (like safety?) and in general the flow of the explanation is just not a good angle to ease the user into understanding what is going on. We're doing something rather complex and new here (especially this all path / no path "stuff").

I also couldn't find any discussion about the lattice merging strategies. I can't even find my own comment wrt. this, so this might be a significant Mandela effect, but I do remember saying that we should evaluate which strategy is better (if such a comparison can be drawn, even...) and leave only that in the suggested upstream patch. If such comparisons are not possible, then running this or that strategy should be configurable through a checker option. I would still like to have some sort of evaluation even if we can't pronounce a definite "winner".

[whisperity]

(✏️ Style nit: Something went wrong here with the formatting, the line became too long and split.)

[whisperity]

❓ The "reverse null" name remained here. This is not inherently a problem! But perhaps it would be worthwhile to think about renaming this to BackpropagatingNull or ...Nullness instead?

[Discookie]

Renamed to NullCheckAfterDereference, since this diagnoser is specific to the checker, not to the framework.

[whisperity]

🐩 Is this true? Why would it be unsafe? The null conditional is redundant. What's unsafe is the unconditional dereference prior to the condition, right?

[Discookie]

In the first example, I wanted to give the exact warning the checker provides, so later I can expand on the specific edge-cases. Changed unsafe => bugprone where possible though.

[whisperity]

That's actually neat! But it triggers a follow-up question: Here, you mean "analysis" as in the analysis of a single function (as driven by the helper function within the check's implementation), and not the analysis of an entire T.U., right?

[whisperity]

Do we know, or can we know this "earlier" location? Here it would be trivial to give a note: to line 8 (*p = 42), but it might not be that trivial in the framework. Is it worthwhile to pursue this, or is it too troublesome and could only be done as a future, separate patch?

[Discookie]

In a past version of the data-flow framework, storing the location of a previous dereference was possible, but currently I don't think it can be implemented. I do want to get this feature working as well, even if not showing all previous dereferences/assignments, at least showing one, but I haven't found a way to do this yet.

[whisperity]

(Oh yeah I forgot one thing which would end up being in 12881232 locations: in many places the variable names do not follow established LLVM conventions, e.g. lhsResult instead of LHSResult. This is more of a tedious nit than anything significant.)

[whisperity]

I put the reverse-null branch into the CI and the build broke because the tests are not passing. I'm retrying with skipped tests. 😋

[whisperity]

Re #1 (comment)

The analyses re-run in the CI, and I uploaded the results to the usual location, although the "detection status" diff of the reports had gone wrong due to the rename.

Nevertheless, here are the failure statistics. All the tallied failures are due to hung kills. ✅ No crashes! I killed an analysis manually after having observed more than 1 hr of runtime for the file. (CodeChecker analyze SHOULD have a --timeout flag or something like that, but I forgot to configure it.)

• TinyXML: 1/2
• libWebM: 2/12
• Xerces-C: 37/348
• Bitcoin: 11/251
• ProtoBuf: 15/161
• Qt: ❌ The whole job was killed, there is no point executing the checker, everything hangs.
• Contour: 4/180
• ACID: ❌ Build failed.
• OpenRCT2: 20/574
• LLVM: ❌ The whole job was killed, there is no point executing the checker, everything hangs.

[whisperity]

Also, as the checker is known to hang we should position ourselves with this check immediately in a defensive way and add it to the list of forbidden-by-default checks when running through clangd. Please modify the file in the same way as in this commit: e63ab13.

[Discookie]

Changed the used merge/compare algos to the non-fast ones. Unit tests don't pass yet, but I'm debugging it.

[whisperity]

Given the changes in 37d3a78..34bdc9b, I do not have further in-line comments. The high-level comment about detecting and diagnosing the "previous dereference" location is still open.

[Discookie]

Changed the used precision-level within the check, so it would be worth to re-run the tests to see if we can find new results or crashes. Otherwise fixed the inline comments where possible.

I'm going to try a couple more ways to store the previous dereference, hopefully one of them works without too much hassle. I think we could realistically show a single dereference, maybe 2 or 3. However, showing all dereferences would lead to more output lines than a template substitution error.
Maybe there is a better way to visualize the locations of dereferences, but that is a future problem.

[Discookie]

Renamed to NullCheckAfterDereference, since this diagnoser is specific to the checker, not to the framework.

[Discookie]

In the first example, I wanted to give the exact warning the checker provides, so later I can expand on the specific edge-cases. Changed unsafe => bugprone where possible though.

[Discookie]

A "potentially null pointer" in this case would mean that we can show a previous location where the pointer's value was definitely null. This is noisy because the check only knows definite pointer values in simpler cases, and thus this specific extension would have even more false negatives.
Removed the "In the future" section altogether.

[Discookie]

Moved into a dedicated section.

[Discookie]

Still pending, and I would like to write a couple more simple tests in the new testing infrastructure as well.
(The new infra uses tests where instead of checking for a specific null/nonnull state afterwards, the test marks the expected null-state within the inline comments, leading to more readable tests.)

[Discookie]

I don't think this information would be useful for the majority of cases, especially not as an on-by-default message. I could implement a checker option to show this message, but at that point the user can also run -dataflow-log and see more information than what we can provide.

[Discookie]

Done.

[Discookie]

We can destructure the optional, just not inside the if. Done.

[Discookie]

Due to the way we have to run the data-flow framework, we're restricted to always matching the top-level function with clang-tidy. These SourceLocations are always distinct from each other, and they each can be treated as a warning separate from all others.
I'm not sure how I should separate the multiple distinct warnings, in a way where it doesn't break the tools.

[Discookie]

In a past version of the data-flow framework, storing the location of a previous dereference was possible, but currently I don't think it can be implemented. I do want to get this feature working as well, even if not showing all previous dereferences/assignments, at least showing one, but I haven't found a way to do this yet.

[whisperity]

I just came back to checking this patch. I like the way how the warnings were restructured, I think they should be understandable now, and the [Warning, Note...] sequences will synergise well with Tidy's usual format.

Is the code here the most up-to-date? I think we should soon do a new run in the CI for all the major projects we usually test, just to be able to show something on the upstream review.

And we should move the patch over to upstream review as well.

[Discookie]

It is now the latest version, ready to test.

[Discookie]

(As soon as the commit tree syncs anyways.)

[whisperity]

It is now the latest version, ready to test.

I fired up b9fba0444d4ffbb35548fa7dd546157a6160c3c7 in the CI. No issues on any of the C projects so far, but I think this was intended that the check is incapable of dealing with C, so yeah...

I'll come back with the results and the hangs after C++ analyses succeeded. What I can see now is that xmltest.cpp in TinyXML is one of the usual suspects...

[whisperity]

(As soon as the commit tree syncs anyways.)

@Discookie I'm not convinced it will do that without a nudge. Next time you update the patch let's take care and do a separate push to master first and then to the PR branch, maybe it will not get into this botched state in that case.

---

Alright, the analysis concluded over C++ projects. I actually restarted the job (with --timeout 1800, aka. 30 minutes) and specified only the C++ projects from the test set, the grand total time of the full measurement job was 2 d 17 hr. I uploaded the results to the Demo server.

I observed no crashes at all. So all the failures you can see on the run list are from timeouts.

The 30-minute timeout might have been a bit eager, but at least we know that feature works in CodeChecker. This is a per-process timeout, so every time a TU hung for 30 minutes, the Tidy process got terminated. Observing the CI logs (it's CSA-measurements-driver#2923 if you want to check) it seemed that for TUs that do not hang, the analyses execute in a sufficiently dynamic fashion, so maybe a 5-minute timeout would be a more reasonable cut-off for the next test. (I just tried to simulate what I did manually in the past, killing processes after roughly 30 min of runtime... I didn't know about --timeout back then.)

In general, most projects succeeded appropriately. Performance was the worst on Qt, where only 172 TUs out of the 1175 succeeded, taking a whopping 34 hours to execute. LLVM was the second worst (it being on the stand isn't surprising, but Qt lapping it, at first glance, is...) with 23:13 runtime and 687 out of the 3089 jobs failing.

There are quite some new reports, almost 10 per project, except for LLVM, where there were previously no reports but now there are 69.

---

Potential false positives

Here are some of the interesting findings which I think should be mentioned in the documentation (and preferably also with a test with FIXME:) at least. I have not looked at EVERY report!

https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=libwebm_libwebm-1.0.0.27_Discookie_reverse-null&detection-status=New&report-id=3497414&report-hash=e75b81fcd825616e0ec904ffef1c99ac&report-filepath=%2Flocal%2Fpersistent_docker%2FCSA-measurements-driver-2923%2Fmeasurements_workspace%2Flibwebm%2Fmkvparser.cpp

ParseTrackEntry(..., Track*&, ...) takes the pointer by reference so it could have been set to a non-null in that function. So saying the if is redundant because the value was invited to a NULL earlier but there is a potentially mutating call in between.

Dittos

• https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=xerces_v3.2.3_Discookie_reverse-null&detection-status=New&report-id=3503093&report-hash=49d09fe14f7ae0ef6c367a7cdbb0257e&report-filepath=%2Flocal%2Fpersistent_docker%2FCSA-measurements-driver-2923%2Fmeasurements_workspace%2Fxerces%2Fsrc%2Fxercesc%2Futil%2FNetAccessors%2FCurl%2FCurlURLInputStream.cpp
• Maybe also all of these: https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=bitcoin_v0.20.1_Discookie_reverse-null&detection-status=New&is-unique=off&diff-type=New&report-hash=ed8f983af1a368faf625aa32bd337fd1&report-id=3503697&report-filepath=%2Flocal%2Fpersistent_docker%2FCSA-measurements-driver-2923%2Fmeasurements_workspace%2Fbitcoin%2Fsrc%2Futil%2Fstrencodings.cpp
• https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=contour_v0.2.0.173_Discookie_reverse-null&detection-status=New&report-id=3503709&report-hash=6765cd3e42fde24536b24888e18ff7f8&report-filepath=%2Flocal%2Fpersistent_docker%2FCSA-measurements-driver-2923%2Fmeasurements_workspace%2Fcontour%2Fsrc%2Fterminal%2FColor.cpp
• https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=llvm-project_llvmorg-12.0.0_Discookie_reverse-null&detection-status=New&report-id=3503715&report-hash=bf1c8d10b0539a5d031faace3e99266f&report-filepath=%2Flocal%2Fpersistent_docker%2FCSA-measurements-driver-2923%2Fmeasurements_workspace%2Fllvm-project%2Fclang%2Flib%2FParse%2FParser.cpp
• Yeah a lot of cases like this...

True positives

• https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=llvm-project_llvmorg-12.0.0_Discookie_reverse-null&detection-status=New&report-id=3503712&report-hash=63f82f7e62ecfea1c53c1896c29b2ef2&report-filepath=%2Flocal%2Fpersistent_docker%2FCSA-measurements-driver-2923%2Fmeasurements_workspace%2Fllvm-project%2Fclang%2Finclude%2Fclang%2FBasic%2FDiagnostic.h Woweee!

Strange reports

• https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=llvm-project_llvmorg-12.0.0_Discookie_reverse-null&detection-status=New&report-id=3503733&report-hash=08362064e805fb3c0ad0635c33369fb9&report-filepath=%2Flocal%2Fpersistent_docker%2FCSA-measurements-driver-2923%2Fmeasurements_workspace%2Fllvm-project%2Fclang%2Flib%2FSema%2FSemaCoroutine.cpp I have no idea how to understand this one.

[Discookie]

Hm. I thought to check for function calls that return pointers, but not for functions that take pointers as arguments. Will implement.

The strange report is not that strange, but I don't know how better to display it without spans. In the constructor a call is made with &(diagObj->...) as its argument, and this explicitly dereferences diagObj before the function starts.

[whisperity]

The strange report is not that strange, but I don't know how better to display it without spans. In the constructor a call is made with &(diagObj->...) as its argument, and this explicitly dereferences diagObj before the function starts.

I might have linked the wrong one there. That one with the ctor was easy to understand I found another one that was strange.

Anyway the reports are up on the server, you can go through them one by one. But most of them is the T*& case.

[whisperity]

Alright, I've gone over most of the reports one more time. If something was very hard to understand due to complex code, I skipped it!

The false positives stemming from not modelling out ptrs need at least a test case (marked with a FIXME) and a sentence or two with an example about it in the documentation file! There are a lot of cases like such.

Questionable: 1 (Why is the report there at the parameter loc?) 2 (Fuzzy locations here as well) 3 (How can something that is dereferenced only be null???)

Strange and not understandable: 1 2 3 4 5 (all from the same function) 6 7 8 (Is this because it is a result of an &Obj?)

---

Some true positives in the LLVM project (albeit older version!): 1 2 3 4 5

These ones might be worthwhile to have some separate patches to fix, which would double as an immediate proof and reasoning for this check!

[Discookie]

Apparently the questionable reports are because of two reasons. First is that the checker does not put note tags on variable declarations, and the second is that the checker can't check if the note tag is lexically before the warning's location in the current system. The first few strange reports are also caused by this.

Strange 6, 7, and 8 look to be true positives, as &Obj can never be null yep, and in case 7 the pointer is already checked. Note tags are missing from some operations here as well, more note tag locations will be added later.

[whisperity]

[This can be closed.]