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 @@ -384,6 +384,11 @@ 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. +SymbolRef simplify(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 @@ -1389,12 +1389,6 @@ // Constraint manager implementation details //===----------------------------------------------------------------------===// -static SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) { - SValBuilder &SVB = State->getStateManager().getSValBuilder(); - SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym)); - return SimplifiedVal.getAsSymbol(); -} - class RangeConstraintManager : public RangedConstraintManager { public: RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB) @@ -1519,9 +1513,6 @@ // This is an infeasible assumption. return nullptr; - if (SymbolRef SimplifiedSym = simplify(State, Sym)) - Sym = SimplifiedSym; - if (ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint)) { if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) { // If the original assumption is not Sym + Adjustment !=/ Int, @@ -1987,7 +1978,7 @@ SValBuilder &SVB, RangeSet::Factory &F, ProgramStateRef State) { SymbolSet ClassMembers = getClassMembers(State); for (const SymbolRef &MemberSym : ClassMembers) { - SymbolRef SimplifiedMemberSym = ::simplify(State, MemberSym); + SymbolRef SimplifiedMemberSym = ::clang::ento::simplify(State, MemberSym); if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) { EquivalenceClass ClassOfSimplifiedSym = EquivalenceClass::find(State, SimplifiedMemberSym); @@ -2313,7 +2304,6 @@ return St; llvm::APSInt Point = AdjustmentType.convert(Int) - Adjustment; - RangeSet New = getRange(St, Sym); New = F.deletePoint(New, Point); 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 @@ -23,12 +23,14 @@ ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption) { + Sym = simplify(State, Sym); + // Handle SymbolData. - if (isa(Sym)) { + if (isa(Sym)) return assumeSymUnsupported(State, Sym, Assumption); - // Handle symbolic expression. - } else if (const SymIntExpr *SIE = dyn_cast(Sym)) { + // Handle symbolic expression. + if (const SymIntExpr *SIE = dyn_cast(Sym)) { // We can only simplify expressions whose RHS is an integer. BinaryOperator::Opcode op = SIE->getOpcode(); @@ -93,6 +95,9 @@ ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange( ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) { + + Sym = simplify(State, Sym); + // Get the type used for calculating wraparound. BasicValueFactory &BVF = getBasicVals(); APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType()); @@ -121,6 +126,8 @@ ProgramStateRef RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, bool Assumption) { + Sym = simplify(State, Sym); + BasicValueFactory &BVF = getBasicVals(); QualType T = Sym->getType(); @@ -219,5 +226,13 @@ } } +SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) { + SValBuilder &SVB = State->getStateManager().getSValBuilder(); + SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym)); + if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol()) + return SimplifiedSym; + return Sym; +} + } // end of namespace ento } // end of namespace clang diff --git a/clang/test/Analysis/solver-sym-simplification-no-crash.c b/clang/test/Analysis/solver-sym-simplification-no-crash.c new file mode 100644 --- /dev/null +++ b/clang/test/Analysis/solver-sym-simplification-no-crash.c @@ -0,0 +1,26 @@ +// RUN: %clang_analyze_cc1 %s \ +// RUN: -analyzer-checker=core \ +// RUN: -analyzer-checker=debug.ExprInspection \ +// RUN: -verify + +// Here, we test that symbol simplification in the solver does not produce any +// crashes. + +// expected-no-diagnostics + +static int a, b; +static long c; + +static void f(int i, int j) +{ + (void)(j <= 0 && i ? i : j); +} + +static void g(void) +{ + int d = a - b | (c < 0); + for (;;) + { + f(d ^ c, c); + } +} diff --git a/clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c b/clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c new file mode 100644 --- /dev/null +++ b/clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c @@ -0,0 +1,29 @@ +// RUN: %clang_analyze_cc1 %s \ +// RUN: -analyzer-checker=core \ +// RUN: -analyzer-checker=debug.ExprInspection \ +// RUN: -verify + +// Here we test that the range based solver equivalency tracking mechanism +// assigns a properly typed range to the simplified symbol. + +void clang_analyzer_printState(); +void clang_analyzer_eval(int); + +void f(int a0, int b0, int c) +{ + int a1 = a0 - b0; + int b1 = (unsigned)a1 + c; + if (c == 0) { + + int d = 7L / b1; // ... + // At this point b1 is considered non-zero, which results in a new + // constraint for $a0 - $b0 + $c. The type of this sym is unsigned, + // however, the simplified sym is $a0 - $b0 and its type is signed. + // This is probably the result of the inherent improper handling of + // casts. Anyway, Range assignment for constraints use this type + // information. Therefore, we must make sure that first we simplify the + // symbol and only then we assign the range. + + clang_analyzer_eval(a0 - b0 != 0); // expected-warning{{TRUE}} + } +}