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

Arseniy Zaostrovnykh via cfe-commits cfe-commits at lists.llvm.org
Thu Jan 2 08:27:33 PST 2025


necto wrote:


> 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've measured it now, and it seems that it affects the execution flow of issues (from 40-80 updated issues to 10-15 out of 80 K). It doesn't seem to have much effect on the appearing/disappearing issues (although without Z3 refutation there are only ~10 out of 80 K).


> It raises me questions why is the only user of this new field the Constraint manager?
> And if the constraint manager is the only user, why is the SMT-based solver not using this? Should all the other immutableSet/Map benefit from this stability when the key is a SymbolRef?

In an upcoming superceeding PR I generalized it for all structures using `ImutContainerInfo`, but SMT-based solver is using this anyway because it uses `ConstraintsMap` type that I update in this PR.

> Why can't the default Profile changed for SymExpr to automatically "opt-in" this new ordering for the rest of the foldingset-user datastructures, such as DenseSet/Map too?

`Symbol*::Profile` alone can't help here, you need to use it explicitly in `ImutContainerInfo`. However, I failed to implement stable Profile particularly because of the `QualType`s used in some of SymExprs: they do not have stable `Profile` implementation and rely on pointers. I am hesitant to go there as that will be affecting Clang globally and not only CSA.

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


More information about the cfe-commits mailing list