[clang] [clang][analyzer] Stable order for SymbolRef-keyed containers (PR #121551)

Arseniy Zaostrovnykh via cfe-commits cfe-commits at lists.llvm.org
Fri Jan 3 04:48:53 PST 2025


necto wrote:

> That being said, do we know how exactly the unstable addresses result in unstable results?

One mechanism that we studied in the past weeks is the SMT issue refutation: assertion order is that of the constraint order in the `ConstraintMap`, and it turns out Z3 runs a query differently depending on the order of the assertions.

There are likely other mechanisms, for example, the SymbolRef `EquivalenceClass` in RangeConstraintManager is an `ImmutableMap<SymbolRef, ...>`. With different ordering, the constraint manager might choose a different representative `SymbolRef` for a given class. This is speculative, though.

> By the way, the Python language (where performance is not prioritized) rules out these subtle bugs by recording the order of insertion within its `dict` (associative map) datatype and using that as the iteration order.

Interesting parallel, as this patch is applying the same strategy for SymbolRef maps


https://github.com/llvm/llvm-project/pull/121551


More information about the cfe-commits mailing list