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 @@ -256,7 +256,7 @@ /// 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 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -20,6 +20,7 @@ #include "llvm/ADT/FoldingSet.h" #include "llvm/ADT/ImmutableSet.h" #include "llvm/ADT/STLExtras.h" +#include "llvm/ADT/SmallSet.h" #include "llvm/Support/Compiler.h" #include "llvm/Support/raw_ostream.h" #include @@ -581,9 +582,20 @@ LLVM_NODISCARD inline ClassSet getDisequalClasses(DisequalityMapTy Map, ClassSet::Factory &Factory) const; + LLVM_NODISCARD static inline Optional areEqual(ProgramStateRef State, + EquivalenceClass First, + EquivalenceClass Second); LLVM_NODISCARD static inline Optional areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second); + LLVM_NODISCARD inline Optional isEqualTo(ProgramStateRef State, + EquivalenceClass Other) const; + + /// 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); @@ -1550,9 +1562,49 @@ return State->set(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 SimplifiedClasses; + // Iterate over all equivalence classes and try to simplify them. + ClassMembersTy Members = State->get(); + for (std::pair ClassToSymbolSet : Members) { + EquivalenceClass Class = ClassToSymbolSet.first; + SymbolSet ClassMembers = ClassToSymbolSet.second; + 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(); + for (std::pair ClassConstraint : Constraints) { + EquivalenceClass Class = ClassConstraint.first; + if (SimplifiedClasses.count(Class)) // Already simplified. + continue; + SymbolSet ClassMembers = Class.getClassMembers(State); + State = Class.simplify(getSValBuilder(), F, State); + if (!State) + return nullptr; + } + + return State; } }; @@ -1588,6 +1640,8 @@ 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(Sym)) return *NontrivialClass; @@ -1865,9 +1919,13 @@ inline Optional 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 EquivalenceClass::areEqual(ProgramStateRef State, + EquivalenceClass First, + EquivalenceClass Second) { // The same equivalence class => symbols are equal. if (First == Second) return true; @@ -1882,6 +1940,45 @@ return llvm::None; } +LLVM_NODISCARD inline Optional +EquivalenceClass::isEqualTo(ProgramStateRef State, + EquivalenceClass Other) const { + return EquivalenceClass::areEqual(State, *this, Other); +} + +// 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 the 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) { + SVal SimplifiedMemberVal = + SVB.simplifySVal(State, SVB.makeSymbolVal(MemberSym)); + SymbolRef SimplifiedMemberSym = SimplifiedMemberVal.getAsSymbol(); + if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) { + ClassSet DisequalClasses = getDisequalClasses(State); + EquivalenceClass ClassOfSimplifiedSym = + EquivalenceClass::find(State, SimplifiedMemberSym); + // We are about to add the newly simplified symbol to the existing + // equivalence class, but they are known to be non-equal. This is a + // contradiction. + // AreEqual = this->areEqual(State, + if (DisequalClasses.contains(ClassOfSimplifiedSym)) + return nullptr; + // 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 --- /dev/null +++ b/clang/test/Analysis/find-binop-constraints.cpp @@ -0,0 +1,145 @@ +// 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; + // Keep the symbols and the constraints! alive. + (void)(a * b * c * d); + clang_analyzer_eval(c == d); // expected-warning{{TRUE}} + 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; + // Keep the symbols and the constraints! alive. + (void)(a * b * c * d); + clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE + return; +}