Author: Gabor Marton Date: 2021-10-14T17:53:29+02:00 New Revision: ac3edc5af09947210d8f8d25ddd7e42379ef6454
URL: https://github.com/llvm/llvm-project/commit/ac3edc5af09947210d8f8d25ddd7e42379ef6454 DIFF: https://github.com/llvm/llvm-project/commit/ac3edc5af09947210d8f8d25ddd7e42379ef6454.diff LOG: [analyzer][solver] Handle simplification to ConcreteInt The solver's symbol simplification mechanism was not able to handle cases when a symbol is simplified to a concrete integer. This patch adds the capability. E.g., in the attached lit test case, the original symbol is `c + 1` and it has a `[0, 0]` range associated with it. Then, a new condition `c == 0` is assumed, so a new range constraint `[0, 0]` comes in for `c` and simplification kicks in. `c + 1` becomes `0 + 1`, but the associated range is `[0, 0]`, so now we are able to realize the contradiction. Differential Revision: https://reviews.llvm.org/D110913 Added: clang/test/Analysis/solver-sym-simplification-concreteint.c Modified: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp Removed: ################################################################################ diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h index c1d2b4665f1d3..599e4ec812a1b 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h @@ -389,11 +389,22 @@ class RangedConstraintManager : public SimpleConstraintManager { 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. We use this function in the family of assumeSymNE/EQ/LT/../GE +/// functions where we can work only with symbols. Use the other function +/// (simplifyToSVal) if you are interested in a simplification that may yield +/// a concrete constant value. 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 index 8299486938850..d1113569c59db 100644 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -2106,7 +2106,20 @@ EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F, ProgramStateRef State, EquivalenceClass Class) { SymbolSet ClassMembers = Class.getClassMembers(State); for (const SymbolRef &MemberSym : ClassMembers) { - SymbolRef SimplifiedMemberSym = ento::simplify(State, MemberSym); + + const SVal SimplifiedMemberVal = simplifyToSVal(State, MemberSym); + const SymbolRef SimplifiedMemberSym = SimplifiedMemberVal.getAsSymbol(); + + // The symbol is collapsed to a constant, check if the current State is + // still feasible. + if (const auto CI = SimplifiedMemberVal.getAs<nonloc::ConcreteInt>()) { + const llvm::APSInt &SV = CI->getValue(); + const RangeSet *ClassConstraint = getConstraint(State, Class); + // We have found a contradiction. + if (ClassConstraint && !ClassConstraint->contains(SV)) + return nullptr; + } + 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 index d227c025fb203..80f3054a5a37f 100644 --- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp @@ -226,9 +226,13 @@ void RangedConstraintManager::computeAdjustment(SymbolRef &Sym, } } -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 index 0000000000000..bfd25eb4f59e5 --- /dev/null +++ b/clang/test/Analysis/solver-sym-simplification-concreteint.c @@ -0,0 +1,40 @@ +// 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_infeasible(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(); // no-warning + + // Keep the symbols and the constraints! alive. + (void)(b * c); + return; +} + +void test_simplification_to_concrete_int_feasible(int b, int c) { + if (c + b != 0) + return; + // c + b == 0 + if (b != 1) + return; + // b == 1 --> c + 1 == 0 + if (c != -1) + return; + // c == -1 --> -1 + 1 == 0 OK + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + clang_analyzer_eval(c == -1); // expected-warning{{TRUE}} + + // Keep the symbols and the constraints! alive. + (void)(b * c); + return; +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
