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 <benicsbal...@gmail.com> Date: Sat, 4 Nov 2023 13:44:28 +0100 Subject: [PATCH 1/3] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions 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 contradiction with any of the equivalent alternatives, then intersecting all these RangeSets should never be empty - aka. there should be a value satisfying the constraints we have. It costs around `|eqclass(X)| + |eqclass(y)|`. The approach has its limitations, as demonstrated by `gh_62215_contradicting_nested_right_equivalent`, where we would need to apply the same logic, but on a sub-expression of a direct operand. Before the patch, line 90, 100, and 112 would be reachable; and become unreachable after this. Line 127 will remain still reachable, but keep in mind that when cross-checking with Z3 (aka. Z3 refutation), then all 4 reports would be eliminated. The idea comes from https://github.com/llvm/llvm-project/issues/62215#issuecomment-1792878474 Fixes #62215 --- .../Core/RangeConstraintManager.cpp | 53 +++++++++++++++++++ clang/test/Analysis/constraint-assignor.c | 48 +++++++++++++++++ 2 files changed, 101 insertions(+) diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp index 5de99384449a4c8..d631369e895d3a9 100644 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -2067,6 +2067,12 @@ class ConstraintAssignor : public ConstraintAssignorBase<ConstraintAssignor> { return Assignor.assign(CoS, NewConstraint); } + /// Check if using an equivalent operand alternative would lead to + /// contradiction. + /// If a contradiction is witnessed, returns false; otherwise returns true. + bool handleEquivalentAlternativeSymOperands(const SymSymExpr *SymSym, + RangeSet Constraint); + /// Handle expressions like: a % b != 0. template <typename SymT> bool handleRemainderOp(const SymT *Sym, RangeSet Constraint) { @@ -2218,11 +2224,58 @@ bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym, return true; } +bool ConstraintAssignor::handleEquivalentAlternativeSymOperands( + const SymSymExpr *SymSym, RangeSet Constraint) { + SymbolRef LHS = SymSym->getLHS(); + SymbolRef RHS = SymSym->getRHS(); + EquivalenceClass LHSClass = EquivalenceClass::find(State, LHS); + EquivalenceClass RHSClass = EquivalenceClass::find(State, RHS); + SymbolSet SymbolsEqWithLHS = LHSClass.getClassMembers(State); + SymbolSet SymbolsEqWithRHS = RHSClass.getClassMembers(State); + llvm::SmallVector<SymSymExpr, 10> AlternativeSymSyms; + + // Gather left alternatives. + for (SymbolRef AlternativeLHS : SymbolsEqWithLHS) { + if (AlternativeLHS == LHS) + continue; + AlternativeSymSyms.emplace_back(AlternativeLHS, SymSym->getOpcode(), RHS, + SymSym->getType()); + } + + // Gather right alternatives. + for (SymbolRef AlternativeRHS : SymbolsEqWithRHS) { + if (AlternativeRHS == RHS) + continue; + AlternativeSymSyms.emplace_back(LHS, SymSym->getOpcode(), AlternativeRHS, + SymSym->getType()); + } + + // Crosscheck the inferred ranges. + for (SymSymExpr AltSymSym : AlternativeSymSyms) { + RangeSet AltSymSymConstrant = + SymbolicRangeInferrer::inferRange(RangeFactory, State, &AltSymSym); + Constraint = intersect(RangeFactory, Constraint, AltSymSymConstrant); + + // Check if we witnessed a contradiction with the equivalent alternative + // operand. + if (Constraint.isEmpty()) { + State = nullptr; + return false; + } + } + return true; +} + bool ConstraintAssignor::assignSymSymExprToRangeSet(const SymSymExpr *Sym, RangeSet Constraint) { if (!handleRemainderOp(Sym, Constraint)) return false; + if (const auto *SymSym = dyn_cast<SymSymExpr>(Sym); + SymSym && !handleEquivalentAlternativeSymOperands(SymSym, Constraint)) { + return false; + } + std::optional<bool> ConstraintAsBool = interpreteAsBool(Constraint); if (!ConstraintAsBool) diff --git a/clang/test/Analysis/constraint-assignor.c b/clang/test/Analysis/constraint-assignor.c index 8210e576c98bd21..d5078b406e12601 100644 --- a/clang/test/Analysis/constraint-assignor.c +++ b/clang/test/Analysis/constraint-assignor.c @@ -82,3 +82,51 @@ void remainder_with_adjustment_of_composit_lhs(int x, int y) { clang_analyzer_eval(x + y != -1); // expected-warning{{TRUE}} (void)(x * y); // keep the constraints alive. } + +void gh_62215(int x, int y, int z) { + if (x != y) return; // x == y + if (z <= x) return; // z > x + if (z >= y) return; // z < y + clang_analyzer_warnIfReached(); // no-warning: This should be dead code. + (void)(x + y + z); // keep the constraints alive. +} + +void gh_62215_contradicting_right_equivalent(int x, int y, int z) { + if (x == y && z > x) { + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + + // `z < y` should mean the same thing as `z < x`, which would contradict with `z > x` + if (z < y) { + clang_analyzer_warnIfReached(); // no-warning: dead code + } + } + (void)(x + y + z); // keep the constraints alive. +} + +void gh_62215_contradicting_left_equivalent(int x, int y, int z) { + if (x == y && z > x) { + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + + // `y > z` should mean the same thing as `x > z`, which would contradict with `z > x` + if (y > z) { + clang_analyzer_warnIfReached(); // no-warning + } + } + (void)(x + y + z); // keep the constraints alive. +} + +void gh_62215_contradicting_nested_right_equivalent(int x, int y, int z) { + if (y > 1 && y < 10) { // y: [2,9] + if (x == y && z > x) { + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + + // `z < (y - 1)` should mean the same thing as `z < (x - 1)`, which + // should contradict with `z > x` (assuming x,y: [2,9]) + if (z < (y - 1)) { + // FIXME: This should be dead code. + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} Z3 crosscheck eliminate this btw + } + } + } + (void)(x + y + z); // keep the constraints alive. +} >From ca847b0f127d88465268244dd5280eaac9aa4ad3 Mon Sep 17 00:00:00 2001 From: Balazs Benics <benicsbal...@gmail.com> Date: Mon, 6 Nov 2023 12:39:49 +0100 Subject: [PATCH 2/3] Fix variable name typo --- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp index d631369e895d3a9..607064dd639442d 100644 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -2252,9 +2252,9 @@ bool ConstraintAssignor::handleEquivalentAlternativeSymOperands( // Crosscheck the inferred ranges. for (SymSymExpr AltSymSym : AlternativeSymSyms) { - RangeSet AltSymSymConstrant = + RangeSet AltSymSymConstraint = SymbolicRangeInferrer::inferRange(RangeFactory, State, &AltSymSym); - Constraint = intersect(RangeFactory, Constraint, AltSymSymConstrant); + Constraint = intersect(RangeFactory, Constraint, AltSymSymConstraint); // Check if we witnessed a contradiction with the equivalent alternative // operand. >From 8425981742aa705999b5c598cd132c6b420d400c Mon Sep 17 00:00:00 2001 From: Balazs Benics <benicsbal...@gmail.com> Date: Mon, 6 Nov 2023 12:53:54 +0100 Subject: [PATCH 3/3] Add FIXME about explaining why we are not doing cross-product --- .../StaticAnalyzer/Core/RangeConstraintManager.cpp | 10 ++++++++++ clang/test/Analysis/constraint-assignor.c | 11 +++++++++++ 2 files changed, 21 insertions(+) diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp index 607064dd639442d..e70abd5d418d5c3 100644 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -2234,6 +2234,16 @@ bool ConstraintAssignor::handleEquivalentAlternativeSymOperands( SymbolSet SymbolsEqWithRHS = RHSClass.getClassMembers(State); llvm::SmallVector<SymSymExpr, 10> AlternativeSymSyms; + // FIXME: We don't do a full cross-product (leftAlts x rightAlts) to try all + // possible combinations, instead what we do is: + // (LHS OP rightAlts) union (leftAlts OP RHS) + + // We don't do it, because it still wouldn't be enough. For example, if a + // sub-symbol of an operand should be substituted to discover the + // contradiction. Doing a cross-product of the operand alternatives is likely + // too expensive for the practical gain, let alone doing the cross-product + // with all possible equivalent sub-symbols - but I haven't measured. + // Gather left alternatives. for (SymbolRef AlternativeLHS : SymbolsEqWithLHS) { if (AlternativeLHS == LHS) diff --git a/clang/test/Analysis/constraint-assignor.c b/clang/test/Analysis/constraint-assignor.c index d5078b406e12601..a88a01afef0358c 100644 --- a/clang/test/Analysis/constraint-assignor.c +++ b/clang/test/Analysis/constraint-assignor.c @@ -115,6 +115,17 @@ void gh_62215_contradicting_left_equivalent(int x, int y, int z) { (void)(x + y + z); // keep the constraints alive. } +void gh_62215_left_and_right(int x, int y, int z, int w) { + if (x != y) return; // x == y + if (z != w) return; // z == w + if (z <= x) return; // z > x + if (w >= y) return; // w < y + // FIXME: We fail to recognize that `w` and `y` are equivalent with `x` and `z` + // respectively and recognize the contradiction. + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} should be dead code + (void)(x + y + z + w); +} + void gh_62215_contradicting_nested_right_equivalent(int x, int y, int z) { if (y > 1 && y < 10) { // y: [2,9] if (x == y && z > x) { _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits