diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h @@ -389,11 +389,19 @@ static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment); }; -/// Try to simplify a given symbolic expression's associated value based on the -/// constraints in State. This is needed because the Environment bindings are -/// not getting updated when a new constraint is added to the State. +/// Try to simplify a given symbolic expression based on the constraints in +/// State. This is needed because the Environment bindings are not getting +/// updated when a new constraint is added to the State. If the symbol is +/// simplified to a non-symbol (e.g. to a constant) then the original symbol +/// is returned. SymbolRef simplify(ProgramStateRef State, SymbolRef Sym); +/// Try to simplify a given symbolic expression's associated `SVal` based on the +/// constraints in State. This is very similar to `simplify`, but this function +/// always returns the simplified SVal. The simplified SVal might be a single +/// constant (i.e. `ConcreteInt`). +SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym); + } // namespace ento } // namespace clang diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -2106,7 +2106,19 @@ ProgramStateRef State, EquivalenceClass Class) { SymbolSet ClassMembers = Class.getClassMembers(State); for (const SymbolRef &MemberSym : ClassMembers) { - SymbolRef SimplifiedMemberSym = ento::simplify(State, MemberSym); + + SymbolRef SimplifiedMemberSym = nullptr; + SVal SimplifiedMemberVal = simplifyToSVal(State, MemberSym); + if (const auto CI = SimplifiedMemberVal.getAs()) { + const llvm::APSInt &SV = CI->getValue(); + const RangeSet *ClassConstraint = getConstraint(State, Class); + // We have found a contradiction. + if (ClassConstraint && !ClassConstraint->contains(SV)) + return nullptr; + } else { + SimplifiedMemberSym = SimplifiedMemberVal.getAsSymbol(); + } + if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) { // The simplified symbol should be the member of the original Class, // however, it might be in another existing class at the moment. We diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp --- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp @@ -226,9 +226,13 @@ } } -SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) { +SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym) { SValBuilder &SVB = State->getStateManager().getSValBuilder(); - SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym)); + return SVB.simplifySVal(State, SVB.makeSymbolVal(Sym)); +} + +SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) { + SVal SimplifiedVal = simplifyToSVal(State, Sym); if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol()) return SimplifiedSym; return Sym; diff --git a/clang/test/Analysis/solver-sym-simplification-concreteint.c b/clang/test/Analysis/solver-sym-simplification-concreteint.c new file mode 100644 --- /dev/null +++ b/clang/test/Analysis/solver-sym-simplification-concreteint.c @@ -0,0 +1,22 @@ +// RUN: %clang_analyze_cc1 %s \ +// RUN: -analyzer-checker=core \ +// RUN: -analyzer-checker=debug.ExprInspection \ +// RUN: -analyzer-config eagerly-assume=false \ +// RUN: -verify + +void clang_analyzer_warnIfReached(); +void clang_analyzer_eval(); + +void test_simplification_to_concrete_int(int b, int c) { + if (c + b != 0) // c + b == 0 + return; + if (b != 1) // b == 1 --> c + 1 == 0 + return; + if (c != 1) // c == 1 --> 1 + 1 == 0 contradiction + return; + clang_analyzer_warnIfReached(); // expected-no-diagnostics + + // Keep the symbols and the constraints! alive. + (void)(b * c); + return; +}