Author: Gabor Marton Date: 2021-06-14T12:19:09+02:00 New Revision: 8ddbb442b6e87efc9c6599280740c6f4fc40963d
URL: https://github.com/llvm/llvm-project/commit/8ddbb442b6e87efc9c6599280740c6f4fc40963d DIFF: https://github.com/llvm/llvm-project/commit/8ddbb442b6e87efc9c6599280740c6f4fc40963d.diff LOG: [Analyzer][solver] Simplify existing eq classes and constraints when a new constraint is added Update `setConstraint` to simplify existing equivalence classes when a new constraint is added. In this patch we iterate over all existing equivalence classes and constraints and try to simplfy them with simplifySVal. This solves problematic cases where we have two symbols in the tree, e.g.: ``` int test_rhs_further_constrained(int x, int y) { if (x + y != 0) return 0; if (y != 0) return 0; clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} clang_analyzer_eval(y == 0); // expected-warning{{TRUE}} return 0; } ``` Differential Revision: https://reviews.llvm.org/D103314 Added: clang/test/Analysis/find-binop-constraints.cpp Modified: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp Removed: ################################################################################ diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h index 4a118074463d..a4957c697c0a 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h @@ -256,7 +256,7 @@ class RangeSet { /// by FoldingSet. void Profile(llvm::FoldingSetNodeID &ID) const { Profile(ID, *this); } - /// getConcreteValue - If a symbol is contrained to equal a specific integer + /// getConcreteValue - If a symbol is constrained to equal a specific integer /// constant then this method returns that value. Otherwise, it returns /// NULL. const llvm::APSInt *getConcreteValue() const { diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp index 1088565d1a23..ac7767f0d3c4 100644 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -21,6 +21,7 @@ #include "llvm/ADT/ImmutableSet.h" #include "llvm/ADT/STLExtras.h" #include "llvm/ADT/StringExtras.h" +#include "llvm/ADT/SmallSet.h" #include "llvm/Support/Compiler.h" #include "llvm/Support/raw_ostream.h" #include <algorithm> @@ -582,9 +583,17 @@ class EquivalenceClass : public llvm::FoldingSetNode { LLVM_NODISCARD inline ClassSet getDisequalClasses(DisequalityMapTy Map, ClassSet::Factory &Factory) const; + LLVM_NODISCARD static inline Optional<bool> areEqual(ProgramStateRef State, + EquivalenceClass First, + EquivalenceClass Second); LLVM_NODISCARD static inline Optional<bool> areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second); + /// Iterate over all symbols and try to simplify them. + LLVM_NODISCARD ProgramStateRef simplify(SValBuilder &SVB, + RangeSet::Factory &F, + ProgramStateRef State); + /// Check equivalence data for consistency. LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED static bool isClassDataConsistent(ProgramStateRef State); @@ -1375,6 +1384,12 @@ RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS, // 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) @@ -1488,6 +1503,9 @@ class RangeConstraintManager : public RangedConstraintManager { // 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, @@ -1554,9 +1572,47 @@ class RangeConstraintManager : public RangedConstraintManager { return State->set<ConstraintRange>(Constraints); } + // Associate a constraint to a symbolic expression. First, we set the + // constraint in the State, then we try to simplify existing symbolic + // expressions based on the newly set constraint. LLVM_NODISCARD inline ProgramStateRef setConstraint(ProgramStateRef State, SymbolRef Sym, RangeSet Constraint) { - return setConstraint(State, EquivalenceClass::find(State, Sym), Constraint); + assert(State); + + State = setConstraint(State, EquivalenceClass::find(State, Sym), Constraint); + if (!State) + return nullptr; + + // We have a chance to simplify existing symbolic values if the new + // constraint is a constant. + if (!Constraint.getConcreteValue()) + return State; + + llvm::SmallSet<EquivalenceClass, 4> SimplifiedClasses; + // Iterate over all equivalence classes and try to simplify them. + ClassMembersTy Members = State->get<ClassMembers>(); + for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members) { + EquivalenceClass Class = ClassToSymbolSet.first; + State = Class.simplify(getSValBuilder(), F, State); + if (!State) + return nullptr; + SimplifiedClasses.insert(Class); + } + + // Trivial equivalence classes (those that have only one symbol member) are + // not stored in the State. Thus, we must skim through the constraints as + // well. And we try to simplify symbols in the constraints. + ConstraintRangeTy Constraints = State->get<ConstraintRange>(); + for (std::pair<EquivalenceClass, RangeSet> ClassConstraint : Constraints) { + EquivalenceClass Class = ClassConstraint.first; + if (SimplifiedClasses.count(Class)) // Already simplified. + continue; + State = Class.simplify(getSValBuilder(), F, State); + if (!State) + return nullptr; + } + + return State; } }; @@ -1592,6 +1648,8 @@ ConstraintMap ento::getConstraintMap(ProgramStateRef State) { inline EquivalenceClass EquivalenceClass::find(ProgramStateRef State, SymbolRef Sym) { + assert(State && "State should not be null"); + assert(Sym && "Symbol should not be null"); // We store far from all Symbol -> Class mappings if (const EquivalenceClass *NontrivialClass = State->get<ClassMap>(Sym)) return *NontrivialClass; @@ -1723,6 +1781,11 @@ EquivalenceClass::mergeImpl(BasicValueFactory &ValueFactory, // 4. Update disequality relations ClassSet DisequalToOther = Other.getDisequalClasses(DisequalityInfo, CF); + // We are about to merge two classes but they are already known to be + // non-equal. This is a contradiction. + if (DisequalToOther.contains(*this)) + return nullptr; + if (!DisequalToOther.isEmpty()) { ClassSet DisequalToThis = getDisequalClasses(DisequalityInfo, CF); DisequalityInfo = DF.remove(DisequalityInfo, Other); @@ -1869,9 +1932,13 @@ inline bool EquivalenceClass::addToDisequalityInfo( inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State, SymbolRef FirstSym, SymbolRef SecondSym) { - EquivalenceClass First = find(State, FirstSym); - EquivalenceClass Second = find(State, SecondSym); + return EquivalenceClass::areEqual(State, find(State, FirstSym), + find(State, SecondSym)); +} +inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State, + EquivalenceClass First, + EquivalenceClass Second) { // The same equivalence class => symbols are equal. if (First == Second) return true; @@ -1886,6 +1953,30 @@ inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State, return llvm::None; } +// Iterate over all symbols and try to simplify them. Once a symbol is +// simplified then we check if we can merge the simplified symbol's equivalence +// 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) { + SymbolSet ClassMembers = getClassMembers(State); + for (const SymbolRef &MemberSym : ClassMembers) { + SymbolRef SimplifiedMemberSym = ::simplify(State, MemberSym); + if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) { + EquivalenceClass ClassOfSimplifiedSym = + EquivalenceClass::find(State, SimplifiedMemberSym); + // 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. + State = merge(SVB.getBasicValueFactory(), F, State, ClassOfSimplifiedSym); + if (!State) + return nullptr; + } + } + return State; +} + inline ClassSet EquivalenceClass::getDisequalClasses(ProgramStateRef State, SymbolRef Sym) { return find(State, Sym).getDisequalClasses(State); diff --git a/clang/test/Analysis/find-binop-constraints.cpp b/clang/test/Analysis/find-binop-constraints.cpp new file mode 100644 index 000000000000..be387a6fb360 --- /dev/null +++ b/clang/test/Analysis/find-binop-constraints.cpp @@ -0,0 +1,163 @@ +// 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_eval(bool); +void clang_analyzer_warnIfReached(); + +int test_legacy_behavior(int x, int y) { + if (y != 0) + return 0; + if (x + y != 0) + return 0; + clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} + clang_analyzer_eval(y == 0); // expected-warning{{TRUE}} + return y / (x + y); // expected-warning{{Division by zero}} +} + +int test_rhs_further_constrained(int x, int y) { + if (x + y != 0) + return 0; + if (y != 0) + return 0; + clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} + clang_analyzer_eval(y == 0); // expected-warning{{TRUE}} + return 0; +} + +int test_lhs_further_constrained(int x, int y) { + if (x + y != 0) + return 0; + if (x != 0) + return 0; + clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} + clang_analyzer_eval(x == 0); // expected-warning{{TRUE}} + return 0; +} + +int test_lhs_and_rhs_further_constrained(int x, int y) { + if (x % y != 1) + return 0; + if (x != 1) + return 0; + if (y != 2) + return 0; + clang_analyzer_eval(x % y == 1); // expected-warning{{TRUE}} + clang_analyzer_eval(y == 2); // expected-warning{{TRUE}} + return 0; +} + +int test_commutativity(int x, int y) { + if (x + y != 0) + return 0; + if (y != 0) + return 0; + clang_analyzer_eval(y + x == 0); // expected-warning{{TRUE}} + clang_analyzer_eval(y == 0); // expected-warning{{TRUE}} + return 0; +} + +int test_binop_when_height_is_2_r(int a, int x, int y, int z) { + switch (a) { + case 1: { + if (x + y + z != 0) + return 0; + if (z != 0) + return 0; + clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}} + clang_analyzer_eval(z == 0); // expected-warning{{TRUE}} + break; + } + case 2: { + if (x + y + z != 0) + return 0; + if (y != 0) + return 0; + clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}} + clang_analyzer_eval(y == 0); // expected-warning{{TRUE}} + break; + } + case 3: { + if (x + y + z != 0) + return 0; + if (x != 0) + return 0; + clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}} + clang_analyzer_eval(x == 0); // expected-warning{{TRUE}} + break; + } + case 4: { + if (x + y + z != 0) + return 0; + if (x + y != 0) + return 0; + clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}} + clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} + break; + } + case 5: { + if (z != 0) + return 0; + if (x + y + z != 0) + return 0; + clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}} + if (y != 0) + return 0; + clang_analyzer_eval(y == 0); // expected-warning{{TRUE}} + clang_analyzer_eval(z == 0); // expected-warning{{TRUE}} + clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}} + break; + } + + } + return 0; +} + +void test_equivalence_classes_are_updated(int a, int b, int c, int d) { + if (a + b != c) + return; + if (a != d) + return; + if (b != 0) + return; + clang_analyzer_eval(c == d); // expected-warning{{TRUE}} + // Keep the symbols and the constraints! alive. + (void)(a * b * c * d); + return; +} + +void test_contradiction(int a, int b, int c, int d) { + if (a + b != c) + return; + if (a == c) + return; + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + + // Bring in the contradiction. + if (b != 0) + return; + clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE + // Keep the symbols and the constraints! alive. + (void)(a * b * c * d); + return; +} + +void test_deferred_contradiction(int e0, int b0, int b1) { + + int e1 = e0 - b0; // e1 is bound to (reg_$0<int e0>) - (reg_$1<int b0>) + (void)(b0 == 2); // bifurcate + + int e2 = e1 - b1; + if (e2 > 0) { // b1 != e1 + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} + // Here, e1 is still bound to (reg_$0<int e0>) - (reg_$1<int b0>) but we + // should be able to simplify it to (reg_$0<int e0>) - 2 and thus realize + // the contradiction. + if (b1 == e1) { + clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE + (void)(b0 * b1 * e0 * e1 * e2); + } + } +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
