[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-12-28 Thread via cfe-commits
DonatNagyE wrote: I'd like to abstain from deciding this question. Personally I don't like the idea that we add yet another hack that'll remain in the codebase forever and slows down all other development efforts in this area (as contributors who want to understand this logic will need to

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-12-28 Thread Balazs Benics via cfe-commits
steakhal wrote: > I'm not opposed to landing this PR in llvm-18 (we have it, and it improves > the user experience), but I wouldn't like to have it in llvm-19 and later. To clarify my intentions, I wanted to land this as it resolves user complaints (as fixing an open issue), at a likely

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-12-28 Thread via cfe-commits
DonatNagyE wrote: Hmm, I would prefer a cleaner, more "theoretical" improvement of the equivalence class handling instead of this "add yet another patch that covers many, but not all cases" approach. I'm not opposed to landing this PR in llvm-18 (we have it, and it improves the user

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-12-28 Thread Balazs Benics via cfe-commits
steakhal wrote: Any objections for landing this PR? Or should we postpone this for llvm-19? https://github.com/llvm/llvm-project/pull/71284 ___ cfe-commits mailing list cfe-commits@lists.llvm.org

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-07 Thread Gabor Marton via cfe-commits
martong wrote: > it'd be good to "strengthen" the equality classes and ensure that we assign > the same RangeSet to each member of an EQClass (or, in other words, we assign > the RangeSet to an EQClass instead of an individual symbol). RangeSets (i.e. constraints) are assigned to EQClasses,

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-06 Thread Gábor Horváth via cfe-commits
Xazax-hun wrote: > So to be explicit, no other component would know what canonicalization > happens within the range-based solver. Oh, I see! Thanks for the clarification, this sounds good to me. https://github.com/llvm/llvm-project/pull/71284 ___

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-06 Thread Balazs Benics via cfe-commits
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. >

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-06 Thread Gábor Horváth via cfe-commits
Xazax-hun 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

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-06 Thread via cfe-commits
DonatNagyE wrote: > I think we haven't discussed yet the approach of applying the constraint to > every eqclass member. That would feel like defeating the purpose of eqclasses > at all. I only mentioned it because from a high-level perspective it's equivalent to applying the constraint on

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-06 Thread Balazs Benics via cfe-commits
https://github.com/steakhal updated https://github.com/llvm/llvm-project/pull/71284 >From 92ece501b340c3a2a52b5a4614ddb70bb3e35c93 Mon Sep 17 00:00:00 2001 From: Balazs Benics Date: Sat, 4 Nov 2023 13:44:28 +0100 Subject: [PATCH 1/3] [analyzer][solver] On SymSym RelOps, check EQClass members

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-06 Thread Balazs Benics via cfe-commits
steakhal wrote: > @DonatNagyE The most straightforward issue that I see is that (if I > understand the code correctly) the intersected constraint (the value of the > variable `Constraint` at the end of > `handleEquivalentAlternativeSymOperands()`) is just discarded after checking > that

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-06 Thread via cfe-commits
@@ -2218,11 +2224,58 @@ bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym, return true; } +bool ConstraintAssignor::handleEquivalentAlternativeSymOperands( +const SymSymExpr *SymSym, RangeSet Constraint) { + SymbolRef LHS = SymSym->getLHS(); +

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-06 Thread via cfe-commits
https://github.com/DonatNagyE edited 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

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-06 Thread via cfe-commits
https://github.com/DonatNagyE commented: This is a good and important improvement of the analysis results, so I support merging it (with some very minor changes), but I feel that it's a "practical, but incomplete" band-aid instead of a systemic improvement that fits into the architecture.

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-06 Thread Balazs Benics via cfe-commits
steakhal wrote: > I think every time we need to iterate over all member of an equivalence > class, we might do something wrong. The point of the equivalence class would > be to make sure those elements are equivalent. One way to avoid iteration > would be to always use the representative of

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-05 Thread Gábor Horváth via cfe-commits
Xazax-hun wrote: I think every time we need to iterate over all member of an equivalence class, we might do something wrong. The point of the equivalence class would be to make sure those elements are equivalent. One way to avoid iteration would be to always use the representative of the

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-04 Thread Balazs Benics via cfe-commits
steakhal wrote: For crossreference: I raised some related questions around having void casts artificially keeping constraints and symbols alive at discuss: https://discourse.llvm.org/t/range-based-solver-and-eager-symbol-garbage-collection/74670 https://github.com/llvm/llvm-project/pull/71284

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-04 Thread via cfe-commits
llvmbot wrote: @llvm/pr-subscribers-clang-static-analyzer-1 Author: Balazs Benics (steakhal) Changes The idea is that if we see a `X RELOP Y` being constrained to a RangeSet `S`, then check the eqclasses of X and Y respectively and for `X' RELOP Y'` SymSymExprs and try to infer their

[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

2023-11-04 Thread Balazs Benics via cfe-commits
https://github.com/steakhal created https://github.com/llvm/llvm-project/pull/71284 The idea is that if we see a `X RELOP Y` being constrained to a RangeSet `S`, then check the eqclasses of X and Y respectively and for `X' RELOP Y'` SymSymExprs and try to infer their ranges. If there is no