[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