[clang] [clang][analyzer] Stabilize path-constraint order by using alloc IDs (PR #121347)

[Balazs Benics via cfe-commits]

steakhal wrote:

Disclaimer: I haven't checked the actual patch, but I'll come back to it :D Maybe next year.
I think I've seen already a variant of this downstream and I generally agreed with the vision. I don't expect much friction on this front, but I'll have a deeper look.

---

> 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).

Does the unstable constraint order only affect Z3 refutation, or did you measure/notice differences in report flakyness even without Z3 refutation? I think it would be great to see the impact of this change, while we eliminate the Z3 from the equation.

---

> I considered using simple incremental ids instead of allocator offsets, but found no advantage. Do you see any?

I'm okay with using allocator offsets for this purpose. That's already a global state, I don't think having another one would really bring much benefit (aka. having a separate global counter for them).

> Would it make sense to unify SymbolData::Sym and SymExpr::AllocID, and maybe get rid of the intermediary SymbolData?

I think SymbolData::Sym and SymExpr::AllocID could be unified. The SymbolData abstraction is useful in general and allows us to differentiate the "source" of the different symbols we have identities for (aka. they are the "interesting" symbols). These are always the "leaves" of the SymExpr trees, so that could be another useful way of looking at SymbolData - once you see that, you won't traverse any deeper.

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