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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
