steakhal wrote: > > So, if I understand you correctly, at the 3rd if statement, we should > > canonicalize the symbol we are constraining by walking every sub-symbol and > > substituting it with its equivalent counterpart (if any), by basically with > > its eqclass' representative symbol. > > I am not 100% sure if I'd go that far (doing canonicalization). Symbols carry > a lot of information, like provenance. Bug reporters, or maybe even some > custom checker state might rely on this. I am afraid that replacing/rewriting > like that might have unexpected consequences, nothing we cannot solve, but I > am not sure whether we want to solve them. What I'd suggest is more like > always adding all the constraints to the representative, and lazily > propagating those constraints to the other members of the equivalence > classes, only when we mention them in a constraint. > > This might also be challenging for bug reporters to explain in some > scenarios, but at least we preserve the provenance information. > > @steakhal
It wasn't actually what I had in mind. I wanted to assign constraints to canonicalized symexprs instead of to the symexpr the API gets from the assume call. And for lookups, we would again do the same thing, canonicalize and only then do the lookup - or let the lookup (rather infer do the canonicalization on the fly). So to be explicit, no other component would know what canonicalization happens within the range-based solver. https://github.com/llvm/llvm-project/pull/71284 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
