Author: Gabor Marton Date: 2021-10-27T16:48:55+02:00 New Revision: 888af47095d5a7121c1d78566df59c292f30ceaf
URL: https://github.com/llvm/llvm-project/commit/888af47095d5a7121c1d78566df59c292f30ceaf DIFF: https://github.com/llvm/llvm-project/commit/888af47095d5a7121c1d78566df59c292f30ceaf.diff LOG: [Analyzer][solver] Simplification: reorganize equalities with adjustment Initiate the reorganization of the equality information during symbol simplification. E.g., if we bump into `c + 1 == 0` during simplification then we'd like to express that `c == -1`. It makes sense to do this only with `SymIntExpr`s. Reviewed By: steakhal Differential Revision: https://reviews.llvm.org/D111642 Added: clang/test/Analysis/solver-sym-simplification-adjustment.c Modified: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp Removed: ################################################################################ diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp index e75a207ee86ab..77f97da4322b3 100644 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -602,10 +602,9 @@ class EquivalenceClass : public llvm::FoldingSetNode { areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second); /// Iterate over all symbols and try to simplify them. - LLVM_NODISCARD static inline ProgramStateRef simplify(SValBuilder &SVB, - RangeSet::Factory &F, - ProgramStateRef State, - EquivalenceClass Class); + LLVM_NODISCARD static inline ProgramStateRef + simplify(SValBuilder &SVB, RangeSet::Factory &F, RangedConstraintManager &RCM, + ProgramStateRef State, EquivalenceClass Class); void dumpToStream(ProgramStateRef State, raw_ostream &os) const; LLVM_DUMP_METHOD void dump(ProgramStateRef State) const { @@ -1729,7 +1728,8 @@ bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym, ClassMembersTy Members = State->get<ClassMembers>(); for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members) { EquivalenceClass Class = ClassToSymbolSet.first; - State = EquivalenceClass::simplify(Builder, RangeFactory, State, Class); + State = + EquivalenceClass::simplify(Builder, RangeFactory, RCM, State, Class); if (!State) return false; SimplifiedClasses.insert(Class); @@ -1743,7 +1743,8 @@ bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym, EquivalenceClass Class = ClassConstraint.first; if (SimplifiedClasses.count(Class)) // Already simplified. continue; - State = EquivalenceClass::simplify(Builder, RangeFactory, State, Class); + State = + EquivalenceClass::simplify(Builder, RangeFactory, RCM, State, Class); if (!State) return false; } @@ -2126,9 +2127,9 @@ inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State, // class to this class. This way, we simplify not just the symbols but the // classes as well: we strive to keep the number of the classes to be the // absolute minimum. -LLVM_NODISCARD ProgramStateRef -EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F, - ProgramStateRef State, EquivalenceClass Class) { +LLVM_NODISCARD ProgramStateRef EquivalenceClass::simplify( + SValBuilder &SVB, RangeSet::Factory &F, RangedConstraintManager &RCM, + ProgramStateRef State, EquivalenceClass Class) { SymbolSet ClassMembers = Class.getClassMembers(State); for (const SymbolRef &MemberSym : ClassMembers) { @@ -2149,9 +2150,30 @@ EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F, // The simplified symbol should be the member of the original Class, // however, it might be in another existing class at the moment. We // have to merge these classes. + ProgramStateRef OldState = State; State = merge(F, State, MemberSym, SimplifiedMemberSym); if (!State) return nullptr; + // No state change, no merge happened actually. + if (OldState == State) + continue; + + // Initiate the reorganization of the equality information. E.g., if we + // have `c + 1 == 0` then we'd like to express that `c == -1`. It makes + // sense to do this only with `SymIntExpr`s. + // TODO Handle `IntSymExpr` as well, once computeAdjustment can handle + // them. + if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SimplifiedMemberSym)) { + if (const RangeSet *ClassConstraint = getConstraint(State, Class)) { + // Overestimate the individual Ranges with the RangeSet' lowest and + // highest values. + State = RCM.assumeSymInclusiveRange( + State, SIE, ClassConstraint->getMinValue(), + ClassConstraint->getMaxValue(), /*InRange=*/true); + if (!State) + return nullptr; + } + } } } return State; diff --git a/clang/test/Analysis/solver-sym-simplification-adjustment.c b/clang/test/Analysis/solver-sym-simplification-adjustment.c new file mode 100644 index 0000000000000..f83e9a4f1fcd1 --- /dev/null +++ b/clang/test/Analysis/solver-sym-simplification-adjustment.c @@ -0,0 +1,111 @@ +// 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_adjustment_concrete_int(int b, int c) { + if (b < 0 || b > 1) // b: [0,1] + return; + if (c < -1 || c > 1) // c: [-1,1] + return; + if (c + b != 0) // c + b == 0 + return; + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + if (b != 1) // b == 1 --> c + 1 == 0 --> c == -1 + return; + 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; +} + +void test_simplification_adjustment_range(int b, int c) { + if (b < 0 || b > 1) // b: [0,1] + return; + if (c < -1 || c > 1) // c: [-1,1] + return; + if (c + b < -1 || c + b > 0) // c + b: [-1,0] + return; + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + if (b != 1) // b == 1 --> c + 1: [-1,0] --> c: [-2,-1] + return; + // c: [-2,-1] is intersected with the + // already associated range which is [-1,1], + // thus we get c: [-1,-1] + 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; +} + +void test_simplification_adjustment_to_infeasible_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 --> c == -1 contradiction + clang_analyzer_eval(b == 0); // expected-warning{{TRUE}} + clang_analyzer_eval(c == 0); // expected-warning{{TRUE}} + // Keep the symbols and the constraints! alive. + (void)(b * c); + return; + } + clang_analyzer_warnIfReached(); // no warning + + // Keep the symbols and the constraints! alive. + (void)(b * c); + return; +} + +void test_simplification_adjustment_to_infeassible_range(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 < -1 || c + b > 0) // c + b: [-1,0] + return; + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + if (b != 1) // b == 1 --> c + 1: [-1,0] --> c: [-2,-1] contradiction + return; + clang_analyzer_warnIfReached(); // no warning + + // Keep the symbols and the constraints! alive. + (void)(b * c); + return; +} + +void test_simplification_adjusment_no_infinite_loop(int a, int b, int c) { + if (a == b) // a != b + return; + if (c != 0) // c == 0 + return; + + if (b != 0) // b == 0 + return; + // The above simplification of `b == 0` could result in an infinite loop + // unless we detect that the State is unchanged. + // The loop: + // 1) Simplification of the trivial equivalence class + // "symbol": "(reg_$0<int a>) == (reg_$1<int b>)", "range": "{ [0, 0] }" + // results in + // "symbol": "(reg_$0<int a>) == 0", "range": "{ [0, 0] }" } + // which in turn creates a non-trivial equivalence class + // [ "(reg_$0<int a>) == (reg_$1<int b>)", "(reg_$0<int a>) == 0" ] + // 2) We call assumeSymInclusiveRange("(reg_$0<int a>) == 0") + // and that calls **simplify** on the associated non-trivial equivalence + // class. During the simplification the State does not change, we reached + // the fixpoint. + + (void)(a * b * c); +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
