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 @@ -387,11 +387,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 @@ -2096,7 +2096,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,38 @@ +// 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 (b < 0 || b > 1) // b: [0,1] + return; + if (c < 0 || c > 1) // c: [0,1] + return; + if (c + b != 0) // c + b == 0 + return; + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + if (b != 1) // b == 1 --> c + 1 == 0 + return; + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + + // After the simplification with b==1 we have a constraint + // c+1==0 but we do not reorder this equality to c==-1. Besides we have another + // constraint that we inherited from a previous State, this is c: [0, 1] + // Now, when we query c==-1 then the latter constraint is found, thus + // resulting in an infeasible state + clang_analyzer_eval(c == -1); // expected-warning{{FALSE}} + + // c == 0 --> 0 + 1 == 0 contradiction + clang_analyzer_eval(c == 0); // expected-warning{{FALSE}} + + // c == 1 --> 1 + 1 == 0 contradiction + clang_analyzer_eval(c != 0); // expected-warning{{FALSE}} + + // Keep the symbols and the constraints! alive. + (void)(b * c); + return; +}