[all-commits] [llvm/llvm-project] bb27d5: [analyzer] Don't assume third iteration in loops (...

[Donát Nagy via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: bb27d5e5c6b194a1440b8ac4e5ace68d0ee2a849
      https://github.com/llvm/llvm-project/commit/bb27d5e5c6b194a1440b8ac4e5ace68d0ee2a849
  Author: Donát Nagy <donat.nagy at ericsson.com>
  Date:   2025-01-02 (Thu, 02 Jan 2025)

  Changed paths:
    M clang/docs/ReleaseNotes.rst
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h
    M clang/lib/StaticAnalyzer/Core/CoreEngine.cpp
    M clang/lib/StaticAnalyzer/Core/ExprEngine.cpp
    A clang/test/Analysis/loop-assumptions.c
    M clang/test/Analysis/loop-unrolling.cpp
    M clang/test/Analysis/misc-ps-region-store.m

  Log Message:
  -----------
  [analyzer] Don't assume third iteration in loops (#119388)

This commit ensures that if the loop condition is opaque (the analyzer
cannot determine whether it's true or false) and there were at least two
iterations, then the analyzer doesn't make the unjustified assumption
that it can enter yet another iteration.

Note that the presence of a loop suggests that the developer thought
that two iterations can happen (otherwise an `if` would've been
sufficient), but it does not imply that the developer expected three or
four iterations -- and in fact there are many false positives where a
loop iterates over a two-element (or three-element) data structure, but
the analyzer cannot understand the loop condition and blindly assumes
that there may be three or more iterations. (In particular, analyzing
the FFMPEG project produces 100+ such false positives.)

Moreover, this provides some performance improvements in the sense that
the analyzer won't waste time on traversing the execution paths with 3
or 4 iterations in a loop (which are very similar to the paths with 2
iterations) and therefore will be able to traverse more branches
elsewhere on the `ExplodedGraph`.

This logic is disabled if the user enables the widen-loops analyzer
option (which is disabled by default), because the "simulate one final
iteration after the invalidation" execution path would be suppressed by
the "exit the loop if the loop condition is opaque and there were at
least two iterations" logic. If we want to support loop widening, we
would need to create a follow-up commit which ensures that it "plays
nicely" with this logic.



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications