https://github.com/NagyDonat created https://github.com/llvm/llvm-project/pull/236565
The primary purpose of the `tryRearrange` logic is that it can simplify comparison or additive expressions by combining the constants when both operands are `SymIntExpr`s with additive operators. E.g. the expression `$x - 3 > $y + 2` is rearranged to `$x - $y > 5` (when there is no risk of overflow) and `($x + 2) - ($x - 2)` is rearranged to a constant `4`. However, the logic also activates when one or both operands are not additive `SymIntExpr`s, rearranging e.g. `$x - 3 > $y` to `$x - $y > 3` or even `$x > $y` to `$x - $y > 0`. In addition to the "pure" case, the "mixed" case is useful, becasue it can recognize that `($x + 1) - $x` is always 1 and it can ensure that the `SymIntExpr` is outside which can lead to further simplifications. However, I don't see good justification for the "degenerate" case when neither operand is an additive `SymIntExpr`: "canceling out" operands in `$x - $x` is already covered by the "are the operands identical?" checks, and rearranging `$x > $y` to `$x - $y > 0` _increases_ complexity. (When the top-level operator is additive, the "degenerate" rearrangement is a no-op: `$x - $y` is "rearranged" to `$x - $y`.) On the other hand, `SymIntExpr`s are rarer than opaque conjured/etc. symbols, so this "degenerate" case is probably significantly more common than the other activations of the `tryRearrange` logic. In this change I prevent rearrangement in these "degenerate" cases to reduce the differences between the current default behavior and the mode when `tryRearrange` is enabled. This will make enabling `tryRearrange` by default (which I intend to do in a follow-up commit) less disruptive. The only potential justification for the "degenerate" rearrangement is that it could ensure that we consistently constrain the _difference_ of two symbolic values: if we rearrange `$x > $y + 1` to `$x - $y > 1` and `$x > $y` to `$x - $y > 0`, then both are recorded in the `RangeSet` associated with the `SymSymExpr` `$x - $y`, so the analyzer sees logical relationships between them. However, we are far from _true_ consistency (even `tryRearrange` will change `$x + 1 > $y` to `$y - $x < 1` instead of `$x - $y > -1` to avoid the negative number), so I decided to ignore this aspect _for now_. `IteratorModeling.cpp` contained some very questionable code that relied on the fact that `tryRearrange` rearranges these "degenerate" expressions (those assertions would be triggered if those parts of the iterator checkers were enabled with default analyzer config that disables `tryRearrange`). I decided to completely remove the problematic logic, because although putting constraints on the difference of iterators is a good idea, it was misplaced in a function that is used only for evaluating equality comparisons between iterators. I think this improves the sorry state of the iterator checkers, but I cannot rule out the possibility that it triggers some hidden problem and I'm not willing to dig deep in that heap of unsupported technical debt. ------- @ reviewers: I'm sorry for the length of this PR description :sweat_smile: Although the actual code change is short, the situation is complex and I think everything that I wrote is necessary for understanding the change. From b89c2e9238ce458341c6c4a6e3aa903777682482 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Don=C3=A1t=20Nagy?= <[email protected]> Date: Wed, 28 Oct 2026 16:17:15 +0100 Subject: [PATCH] [analyzer] Disable tryRearrange when it increases complexity The primary purpose of the `tryRearrange` logic is that it can simplify comparison or additive expressions by combining the constants when both operands are `SymIntExpr`s with additive operators. E.g. the expression `$x - 3 > $y + 2` is rearranged to `$x - $y > 5` (when there is no risk of overflow) and `($x + 2) - ($x - 2)` is rearranged to a constant `4`. However, the logic also activates when one or both operands are not additive `SymIntExpr`s, rearranging e.g. `$x - 3 > $y` to `$x - $y > 3` or even `$x > $y` to `$x - $y > 0`. The "mixed" case is useful: it can recognize that `($x + 1) - $x` is always 1 and it can ensure that the `SymIntExpr` is "outside" which can lead to further simplifications. However, I don't see good justification for the "degenerate" case when neither operand is an additive `SymIntExpr`: "canceling out" operands in `$x - $x` is already covered by the "are the operands identical?" checks, and rearranging `$x > $y` to `$x - $y > 0` _increases_ complexity. (When the top-level operator is additive, the "degenerate" rearrangement is a no-op: `$x - $y` is "rearranged" to `$x - $y`.) On the other hand, `SymIntExpr`s are rarer than opaque conjured/etc. symbols, so this "degenerate" case is probably significantly more common than the other activations of the `tryRearrange` logic. In this change I prevent rearrangement in these "degenerate" cases to reduce the differences between the current default behavior and the mode when `tryRearrange` is enabled. This will make enabling `tryRearrange` by default (which I intend to do in a follow-up commit) less disruptive. The only potential justification for the "degenerate" rearrangement is that it could ensure that we consistently constrain the _difference_ of two symbolic values: if we rearrange `$x > $y + 1` to `$x - $y > 1` and `$x > $y` to `$x - $y > 0`, then both are recorded in the `RangeSet` associated with the `SymSymExpr` `$x - $y`, so the analyzer sees logical relationships between them. However, we are far from _true_ consistency (even `tryRearrange` will change `$x + 1 > $y` to `$y - $x < 1` instead of `$x - $y > -1` to avoid the negative number), so I decided to ignore this aspect _for now_. `IteratorModeling.cpp` contained some very questionable code that relied on the fact that `tryRearrange` rearranges these "degenerate" expressions (those assertions would be triggered if those parts of the iterator checkers were enabled with default analyzer config that disables `tryRearrange`). I decided to completely remove the problematic logic, because although putting constraints on the difference of iterators is a good idea, it was misplaced in a function that is used only for evaluating equality comparisons between iterators. I think this improves the sorry state of the iterator checkers, but I cannot rule out the possibility that it triggers some hidden problem and I'm not willing to dig deep in that heap of unsupported technical debt. --- .../Checkers/IteratorModeling.cpp | 30 ++++--------------- .../StaticAnalyzer/Core/SimpleSValBuilder.cpp | 3 ++ .../svalbuilder-rearrange-comparisons.cpp | 12 ++++---- 3 files changed, 15 insertions(+), 30 deletions(-) diff --git a/clang/lib/StaticAnalyzer/Checkers/IteratorModeling.cpp b/clang/lib/StaticAnalyzer/Checkers/IteratorModeling.cpp index bb3920bd17762d..f2a9141bc1f06c 100644 --- a/clang/lib/StaticAnalyzer/Checkers/IteratorModeling.cpp +++ b/clang/lib/StaticAnalyzer/Checkers/IteratorModeling.cpp @@ -793,32 +793,14 @@ ProgramStateRef relateSymbols(ProgramStateRef State, SymbolRef Sym1, SymbolRef Sym2, bool Equal) { auto &SVB = State->getStateManager().getSValBuilder(); - // FIXME: This code should be reworked as follows: - // 1. Subtract the operands using evalBinOp(). - // 2. Assume that the result doesn't overflow. - // 3. Compare the result to 0. - // 4. Assume the result of the comparison. - const auto comparison = - SVB.evalBinOp(State, BO_EQ, nonloc::SymbolVal(Sym1), - nonloc::SymbolVal(Sym2), SVB.getConditionType()); - - assert(isa<DefinedSVal>(comparison) && - "Symbol comparison must be a `DefinedSVal`"); - - auto NewState = State->assume(comparison.castAs<DefinedSVal>(), Equal); - if (!NewState) - return nullptr; + const SVal Cmp = + SVB.evalBinOp(State, BO_EQ, nonloc::SymbolVal(Sym1), + nonloc::SymbolVal(Sym2), SVB.getConditionType()); - if (const auto CompSym = comparison.getAsSymbol()) { - assert(isa<SymIntExpr>(CompSym) && - "Symbol comparison must be a `SymIntExpr`"); - assert(BinaryOperator::isComparisonOp( - cast<SymIntExpr>(CompSym)->getOpcode()) && - "Symbol comparison must be a comparison"); - return assumeNoOverflow(NewState, cast<SymIntExpr>(CompSym)->getLHS(), 2); - } + if (!isa<DefinedSVal>(Cmp)) + return nullptr; - return NewState; + return State->assume(Cmp.castAs<DefinedSVal>(), Equal); } bool isBoundThroughLazyCompoundVal(const Environment &Env, diff --git a/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp b/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp index c89271af525b8e..88413da9681567 100644 --- a/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp +++ b/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp @@ -333,6 +333,9 @@ static std::optional<NonLoc> tryRearrange(ProgramStateRef State, std::tie(LSym, LInt) = decomposeSymbol(LSym, BV); std::tie(RSym, RInt) = decomposeSymbol(RSym, BV); + if (LInt.isZero() && RInt.isZero()) + return std::nullopt; + if (LSym->getType() != CommonTy || RSym->getType() != CommonTy) return std::nullopt; diff --git a/clang/test/Analysis/svalbuilder-rearrange-comparisons.cpp b/clang/test/Analysis/svalbuilder-rearrange-comparisons.cpp index eca6ab0c71befe..01985c95af6f82 100644 --- a/clang/test/Analysis/svalbuilder-rearrange-comparisons.cpp +++ b/clang/test/Analysis/svalbuilder-rearrange-comparisons.cpp @@ -44,7 +44,7 @@ void compare_different_symbol_equal(void) { int x = f(), y = f(); clang_analyzer_denote(x, "$x"); clang_analyzer_denote(y, "$y"); - clang_analyzer_express(x == y); // expected-warning {{$x - $y == 0}} + clang_analyzer_express(x == y); // expected-warning {{$x == $y}} } void compare_different_symbol_plus_left_int_equal(void) { @@ -204,7 +204,7 @@ void compare_different_symbol_less_or_equal(void) { int x = f(), y = f(); clang_analyzer_denote(x, "$x"); clang_analyzer_denote(y, "$y"); - clang_analyzer_express(x <= y); // expected-warning {{$x - $y <= 0}} + clang_analyzer_express(x <= y); // expected-warning {{$x <= $y}} } void compare_different_symbol_plus_left_int_less_or_equal(void) { @@ -365,7 +365,7 @@ void compare_different_symbol_less(void) { clang_analyzer_denote(x, "$x"); clang_analyzer_denote(y, "$y"); clang_analyzer_express(y); // expected-warning {{$y}} - clang_analyzer_express(x < y); // expected-warning {{$x - $y < 0}} + clang_analyzer_express(x < y); // expected-warning {{$x < $y}} } void compare_different_symbol_plus_left_int_less(void) { @@ -541,7 +541,7 @@ void compare_different_symbol_equal_unsigned(void) { clang_analyzer_denote(x, "$x"); clang_analyzer_denote(y, "$y"); clang_analyzer_express(y); // expected-warning {{$y}} - clang_analyzer_express(x == y); // expected-warning {{$x - $y == 0}} + clang_analyzer_express(x == y); // expected-warning {{$x == $y}} } void compare_different_symbol_plus_left_int_equal_unsigned(void) { @@ -694,7 +694,7 @@ void compare_different_symbol_less_or_equal_unsigned(void) { clang_analyzer_denote(x, "$x"); clang_analyzer_denote(y, "$y"); clang_analyzer_express(y); // expected-warning {{$y}} - clang_analyzer_express(x <= y); // expected-warning {{$x - $y <= 0}} + clang_analyzer_express(x <= y); // expected-warning {{$x <= $y}} } void compare_different_symbol_plus_left_int_less_or_equal_unsigned(void) { @@ -847,7 +847,7 @@ void compare_different_symbol_less_unsigned(void) { clang_analyzer_denote(x, "$x"); clang_analyzer_denote(y, "$y"); clang_analyzer_express(y); // expected-warning {{$y}} - clang_analyzer_express(x < y); // expected-warning {{$x - $y < 0}} + clang_analyzer_express(x < y); // expected-warning {{$x < $y}} } void compare_different_symbol_plus_left_int_less_unsigned(void) { _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
