Fixing or removing check::BranchCondition

Clang Frontend Static Analyzer
1

TL;DR: The implementation of check::BranchCondition is buggy and it’s barely used, so perhaps it should be completely removed from the analyzer.

Part 1: Incorrect implementation

Recently, while I was working on heuristics for weak loop assumptions I looked into the implementation details of check::BranchCondition and I realized that it is broken.

The relevant part of the logic is the body of ExprEngine::processBranch:

  ExplodedNodeSet CheckersOutSet;
  getCheckerManager().runCheckersForBranchCondition(Condition, CheckersOutSet,
                                                    Pred, *this);
  // We generated only sinks.
  if (CheckersOutSet.empty())
    return;
 
  BranchNodeBuilder builder(CheckersOutSet, Dst, BldCtx, DstT, DstF);
  for (ExplodedNode *PredN : CheckersOutSet) {
    if (PredN->isSink())
      continue;
 
    ProgramStateRef PrevState = PredN->getState();
 
    ProgramStateRef StTrue, StFalse;
    if (const auto KnownCondValueAssumption = assumeCondition(Condition, PredN))
      std::tie(StTrue, StFalse) = *KnownCondValueAssumption;
    else {
      assert(!isa<ObjCForCollectionStmt>(Condition));
      builder.generateNode(PrevState, true, PredN);
      builder.generateNode(PrevState, false, PredN);
      continue;
    }
    if (StTrue && StFalse)
      assert(!isa<ObjCForCollectionStmt>(Condition));
 
    // Process the true branch.
    if (builder.isFeasible(true)) {
      if (StTrue)
        builder.generateNode(StTrue, true, PredN);
      else
        builder.markInfeasible(true);
    }
 
    // Process the false branch.
    if (builder.isFeasible(false)) {
      if (StFalse)
        builder.generateNode(StFalse, false, PredN);
      else
        builder.markInfeasible(false);
    }
  }

This (slightly awkward) code performs the following steps:

  1. It runs the check::BranchCondition checkers and collects the ExplodedNodes produced by them in CheckerOutSet.
  2. It initializes a BranchNodeBuilder builder which will build the “after the branching point” nodes (and will place them in either DstT or DstF).
  3. It loops over the nodes within CheckersOutSet with the loop variable PredN.
  4. For each node PredN it splits the state based on the value of the loop condition and creates successor nodes for the outcomes that are feasible.
  5. If the one of the outcomes was infeasible (e.g. the loop condition cannot be false), we call builder.markInfeasible() which will prevent the production of additional nodes with that outcome.
  6. But these “infeasible” marks are preserved for the next iteration of the for loop, and suppress the generation of nodes with that outcome – even if that outcome would be feasible when starting from the new, different PredN!

I was surprised to see why this incorrect logic was not causing any errors, so I added an assertion which revealed that the LIT test suite doesn’t contain any test code where CheckersOutSet has more than one element, i.e. check::BranchCondition checkers never split the state.

Part 2: Barely used

Then I looked up the checkers that use this callback and it turned out that there are only three of them (not counting CheckerDocumentation.cpp):

UndefBranchChecker.cpp is a very straightforward checker which just says “Branch condition evaluates to a garbage value” when it’s appropriate.

  • This is obviously an useful report, but I don’t see why we have five or so specific UndefinedSomethingResult checkers instead of a single checker that reports every occurrence when an undefined value is used in some way.

TraversalChecker.cpp is apparently a debug dumper utility which was added in 2012 to “Add a test that we are, in fact, doing a DFS on the ExplodedGraph”.

  • Its BranchCondition callback is only used by the single test file traversal-algorithm.mm which could be easily ported to some other callback.

TestAfterDivZeroChecker.cpp is an old alpha checker from 2014, which reports code paths where we use a value as a denominator and then later check whether that value is zero – and for some reason this logic is limited to cases when the “check whether that value is zero” comparison happens in a branch condition.

  • In this checker replacing BranchCondition with PreStmt would be an obvious improvement.
  • However, this checker also has a fundamental issue, so we’re contemplating its complete removal, or, perhaps its rewrite in the dataflow framework. (This is offtopic, so I’m describing it at the end of this post.)

Part 3: The way forward

I can imagine several very different ways to resolve this situation:

  • (A) Write a more complicated, but correct implementation and keep check::BranchCondition to make it available for further checker development.
    My personal impression is that this callback is not very useful, and I don’t think that we should maintain callbacks without compelling use cases.
  • (B) Replace the buggy for loop with an assertion that there was no state split and document the currently upheld invariant that check::BranchCondition must not split the state.
    A lazy solution, can be easily implemented.
  • (C) The same as (B), but migrate away the non-essential checkers and document that only UndefBranchChecker should use check::BranchCondition.
    Cleans up the situation as much as possible without touching the Undef checker family.
  • (D) Completely eliminate check::BranchCondition and replace the overlapping UndefinedSomethingCheckers with an unified UndefinedValueChecker which warns on all code that reads undefined values.
    Radical solution that also simplifies an unrelated part of the codebase.
  • (E) Do nothing.
    Even lazier than (B), this would produce weird incorrect behavior when somebody introduces a check::BranchCondition callback that splits the state. (However, apparently this is not a popular callback, so if we’re lucky it will stay practically unused forever :slight_smile:)

@steakhal @NoQ @Xazax-hun @Szelethus What do you think about this callback? How should we approach this technical debt?

Appendix: the fatal flaw of TestAfterDivZeroChecker

This checker reports situations where a value is used as a denominator and then later there is at least one code path where it’s compared against zero.

However, the logically correct thing would be reporting situations where a value is used as a denominator and then later on every possible code path it’s compared against zero.

For example, consider the following function:

int foo(int a, int b) {
  int c = a / b;
  if (c > 10)
    b = get_new_denominator(a, b);
  // some other logic...
  if (b == 0)
    return c;
  return a / b;
}

Here the check for b == 0 is an idiomatic way to handle cases where the opaque function get_new_denominator returns 0 – but on the single execution path where c > 0 is assumed to be false this triggers TestAfterDivZeroChecker.

This is a fundamental limitation of the path-sensitive framework of the static analyzer, and although we could theoretically find some hacky solutions, I think it would be better to cover this kind of coding error in the dataflow framework where it naturally belongs.

2

I’d vote for option D, getting rid of this checker callback and cleanup whatever used this before.

3

I would also be fine with option D.

4

Thanks for the feedback!

I’ll probably start with removing check::BranchCondition from TestAfterDivZeroChecker.cpp and TraversalChecker.cpp, because that’s (hopefully) low-hanging fruit.

However, I fear that changing UndefBranchChecker a/k/a core.uninitialized.Branch might be difficult from a backwards compatibility POV. (Perhaps I didn’t emphasize this sufficiently, but this is a core checker.)

Right now Undefined values are covered by seven core checkers:

In my opinion it would be more user-friendly to remove these separate checkers and emit all “undefined value used” reports from a single checker (e.g. core.UndefinedValue), because:

  • I don’t see a usecase for selectively enabling/disabling some of these checkers, and they’re all core checkers anyway, so disabling them is not supported.
  • These are all different manifestations of the same “bug type”, so for statistics purposes it’d be more helpful to group all these reports under a single name.
  • Perhaps the single core.UndefinedValue checker would be able to cover some more exotic “use undefined value in a weird expression” cases that don’t belong to any of the existing checkers.

However, replacing seven core checkers with an eighth one would be a major change that would cause artifacts in the analysis history of every user. To mitigate this, we would probably need to do a gradual deprecation/removal that’s staggered over several clang releases.

(By the way, I don’t think that there is a good intermediate step that moves core.uninitalized.Branch away from the check::BranchCondition callback, but doesn’t touch the rest of the undefined value checker zoo.)

@steakhal @Xazax-hun @NoQ @Szelethus WDYT about the future of these “undefined value” checkers?

If you think that unifying them would be an useful change, then I can open a separate discussion thread for it and perhaps start drafting some changes (e.g. commits that mark these checkers as deprecated).

5

We wouldn’t be impacted by the merger of the different undef checkers. I also believe that the current sepaeation and groupping is arbitrary. I always thought of the same issue anyways.

Assuming the report messages and line locations wouldn’t change, this is a good move. Slight changes are also okay, major changes might need some engineering to make the transition easier.

6

If the undef checkers are merged, then I think it would be natural to use the same message for all (or at least most) of their reports. E.g. a current message like “Assigned value is garbage or undefined” is not more informative than a simple “Use of garbage or undefined value” with an error location that points to the RHS of the assignment operator.

However, it would be probably possible to preserve the current messages if that helps the transition.

7

I prefer the keep the messages as is unless there is a UX reason to change them. Also, I don’t think this redundancy is a problem. There are other instances in the analyzer where we e.g., mention which argument of a function is problematic and also highlight the corresponding source region.

8

I prefer the keep the messages as is unless there is a UX reason to change them.

I understand your POV and I agree that for the users it would be neutral or slightly positive to keep the messages.

However, I was hoping that it would be possible to significantly simplify the logic if we move the checkers to a single more general callback (that doesn’t distinguish the various cases).

If we want to keep all the distinct messages all the distinct callbacks that generate them, then we aren’t eliminating the dependency on check::BranchCondition and I don’t think that we’re winning enough to justify the change.

Perhaps it may be possible to write a single-callback unified solution that can still distinguish the different cases and produce fine-tuned messages for them, but I feel that implementing this would be difficult work, and I don’t think that I would have time for implementing this (instead of other, higher priority changes).

On the other fronts I created [analyzer][NFC] Remove check::BranchCondition from debug.DumpTraversal by NagyDonat · Pull Request #113906 · llvm/llvm-project · GitHub to remove check::BranchCondition from TraversalChecker.cpp, but as I looked into TestAfterDivZeroChecker.cpp I realized that there are some situations where this checker legitimately needs check::BranchCondition.

In particular, in the simple testcase

void err_yes(int x) {
  var = 77 / x;
  if (x) {}
}

we probably need a check::BranchCondition callback to detect that the value x (which was already used as a denominator) is implicitly compared against zero. (Perhaps in C++ we’d have an implicit cast to boolean, but in C the only thing that we see is that the int value appears as a branch condition.)

Therefore I don’t think that I can create a short straightforward commit that removes the dependency on check::BranchCondition from this checker.

However, it’s an old alpha checker with several brutal issues:

  • its overall logic is wrong on a theoretical level (as I described in the appendix of my opening post, the path-sensitive model of the analyzer is not suitable for detecting this kind of bug);
  • its code quality is bad (overcomplicated logic, some code duplication etc.);
  • it contains heuristics that are just stupid, e.g. it produces a warning on the following code (where the x >= 0 check is IMO a perfectly normal way of distinguishing the cases where x is positive/negative):
void err_ge(int x) {
  var = 77 / x;
  if (x >= 0) { }
}

… so I think outright removing TestAfterDivZeroChecker.cpp would be a justified decision. What do you think about this?

(Eventually an analogous checker could be implemented in the new dataflow framework – once it becomes stable enough for this application. In our team Viktor Cseh is working on a dataflow-based “reverse null checker” to report cases where a pointer is dereferenced and then later compared against NULL – once that’s ready, its logic could be adapted to get a proper dataflow-based test-after-divzero checker.)

9

I see. I expected it to be relatively simple to distinguish between the different cases based on the AST in most cases. I think it might be OK to not produce 100% the same messages in all cases, but I think we should not make changes negatively affecting our users without a stronger justification. I agree that the code could be simplified that way, but we did not have many problems with these checkers, so I am not sure if these is too much to win here.

Therefore I don’t think that I can create a short straightforward commit that removes the dependency on check::BranchCondition from this checker.

This changes the whole discussion because now it looks like we found a legitimate use case for this callback. I think before just outright removing the old check and proceeding with eliminating the callback we need a justification why we anticipate that other new checks would not need this callback in the future.

I think the question is how often is it useful information that there was a branching on some condition (as opposed to just asking the solver for some information). I wonder if this sort of information is useful in some contexts when it comes to taint analysis.

10

This changes the whole discussion because now it looks like we found a legitimate use case for this callback. I think before just outright removing the old check and proceeding with eliminating the callback we need a justification why we anticipate that other new checks would not need this callback in the future.

I agree, and based on this I’m leaning towards reducing the scope of this cleanup effort:

  • We should still merge the cleanup in TraversalChecker.cpp because it’s just NFC garbage removal.
  • We might want to remove TestAfterDivZeroChecker.cpp because it’s fundamentally flawed after all, but we don’t need to do it as a prerequisite of something else.
  • I’ll probably drop the plans for the unification of the undef value checkers, because it’s a big change for limited gains that are mostly intangible (“elegance” etc.)
  • I’ll refactor the implementation of ExprEngine::processBranch to get rid of the “silently does something crazy” situation. I’ll probably just remove the for loop and add an assertion to verify that there was no state split (which is currently satisfied by all three check::BranchCondition checkers), but giving a correct general implementation (for some potential use in the future) would also be possible.
11

I created github PR #117898 which cleans up dead code connected to BranchNodeBuilder and fixes the buggy implementation of the check::BranchCondition callback in ExprEngine::processBranch. (After this, check:BranchCondition callbacks will be able to “split the state” safely.)

By the way, since my last commit the check::BranchCondition callback was removed from the DumpTraversal checker.

This is probably my last comment in this topic – once my second cleanup commit is merged I’ll be satisfied by the state of this callback. (Of course the removal of TestAfterDivZeroChecker.cpp is still on the table, but that’s only tangentially related to this.)