[all-commits] [llvm/llvm-project] 0844f8: [clang][analyzer] Stable order for SymbolRef-keyed...

[Arseniy Zaostrovnykh via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 0844f83fea66332943deed7cdf97b686b2c7c37b
      https://github.com/llvm/llvm-project/commit/0844f83fea66332943deed7cdf97b686b2c7c37b
  Author: Arseniy Zaostrovnykh <necto.ne at gmail.com>
  Date:   2025-01-03 (Fri, 03 Jan 2025)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
    M clang/lib/StaticAnalyzer/Core/SymbolManager.cpp
    M clang/test/Analysis/dump_egraph.cpp
    M clang/test/Analysis/expr-inspection-printState-diseq-info.c
    M clang/test/Analysis/expr-inspection-printState-eq-classes.c
    M clang/test/Analysis/ptr-arith.cpp
    M clang/test/Analysis/symbol-simplification-disequality-info.cpp
    M clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
    M clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
    M clang/test/Analysis/unary-sym-expr.c

  Log Message:
  -----------
  [clang][analyzer] Stable order for SymbolRef-keyed containers (#121551)

Generalize the `SymbolID`s used for `SymbolData` to all `SymExpr`s and
use these IDs for comparison `SymbolRef` keys in various containers,
such as `ConstraintMap`. These IDs are superior to raw pointer values
because they are more controllable and are not randomized across
executions (unlike
[pointers](https://en.wikipedia.org/wiki/Address_space_layout_randomization)).

These IDs order is stable across runs because SymExprs are allocated in
the same order.

Stability of the constraint order is important for the stability of the
analyzer results. I evaluated this change on a set of 200+ open-source C
and C++ projects with the total number of ~78 000 symbolic-execution
issues passing Z3 refutation.

This patch reduced the run-to-run churn (flakiness) in SE issues from
80-90 to 30-40 (out of 78K) in our CSA deployment (in our setting flaky
issues are mostly due to Z3 refutation instability).

Note, most of the issue churn (flakiness) is caused by the mentioned Z3
refutation. With Z3 refutation disabled, issue churn goes down to ~10
issues out of 83K and this patch has no effect on appearing/disappearing
issues between runs. It however, seems to reduce the volatility of the
execution flow: before we had 40-80 issues with changed execution flow,
after - 10-30.

Importantly, this change is necessary for the next step in stabilizing
analysis results by caching Z3 query outcomes between analysis runs
(work in progress).

Across our admittedly noisy CI runs, I detected no significant effect on
memory footprint or analysis time.

CPP-5919



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