From 6f3b775c3e9c685f74ecbe2ce1a94af52cc17c2f Mon Sep 17 00:00:00 2001 From: Gabor Marton Date: Wed, 9 Jun 2021 17:03:47 +0200 Subject: [PATCH] [Analyzer][solver] Add dump methods for (dis)equality classes. This proved to be very useful during debugging. Differential Revision: https://reviews.llvm.org/D103967 --- .../Core/RangeConstraintManager.cpp | 138 ++++++++++++++++++ .../expr-inspection-printState-diseq-info.c | 34 +++++ .../expr-inspection-printState-eq-classes.c | 21 +++ clang/test/Analysis/expr-inspection.c | 2 + 4 files changed, 195 insertions(+) create mode 100644 clang/test/Analysis/expr-inspection-printState-diseq-info.c create mode 100644 clang/test/Analysis/expr-inspection-printState-eq-classes.c diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp index 6d17bcb8b87f..27367ff5ae80 100644 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -594,6 +594,11 @@ public: RangeSet::Factory &F, ProgramStateRef State); + void dumpToStream(ProgramStateRef State, raw_ostream &os) const; + LLVM_DUMP_METHOD void dump(ProgramStateRef State) const { + dumpToStream(State, llvm::errs()); + } + /// Check equivalence data for consistency. LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED static bool isClassDataConsistent(ProgramStateRef State); @@ -1414,6 +1419,17 @@ public: void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n", unsigned int Space = 0, bool IsDot = false) const override; + void printConstraints(raw_ostream &Out, ProgramStateRef State, + const char *NL = "\n", unsigned int Space = 0, + bool IsDot = false) const; + void printEquivalenceClasses(raw_ostream &Out, ProgramStateRef State, + const char *NL = "\n", unsigned int Space = 0, + bool IsDot = false) const; + void printEquivalenceClass(raw_ostream &Out, ProgramStateRef State, + EquivalenceClass Class) const; + void printDisequalities(raw_ostream &Out, ProgramStateRef State, + const char *NL = "\n", unsigned int Space = 0, + bool IsDot = false) const; //===------------------------------------------------------------------===// // Implementation for interface from RangedConstraintManager. @@ -1637,6 +1653,15 @@ ConstraintMap ento::getConstraintMap(ProgramStateRef State) { // EqualityClass implementation details //===----------------------------------------------------------------------===// +LLVM_DUMP_METHOD void EquivalenceClass::dumpToStream(ProgramStateRef State, + raw_ostream &os) const { + SymbolSet ClassMembers = getClassMembers(State); + for (const SymbolRef &MemberSym : ClassMembers) { + MemberSym->dump(); + os << "\n"; + } +} + inline EquivalenceClass EquivalenceClass::find(ProgramStateRef State, SymbolRef Sym) { assert(State && "State should not be null"); @@ -2483,6 +2508,16 @@ ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange( void RangeConstraintManager::printJson(raw_ostream &Out, ProgramStateRef State, const char *NL, unsigned int Space, bool IsDot) const { + printConstraints(Out, State, NL, Space, IsDot); + printEquivalenceClasses(Out, State, NL, Space, IsDot); + printDisequalities(Out, State, NL, Space, IsDot); +} + +void RangeConstraintManager::printConstraints(raw_ostream &Out, + ProgramStateRef State, + const char *NL, + unsigned int Space, + bool IsDot) const { ConstraintRangeTy Constraints = State->get(); Indent(Out, Space, IsDot) << "\"constraints\": "; @@ -2516,3 +2551,106 @@ void RangeConstraintManager::printJson(raw_ostream &Out, ProgramStateRef State, --Space; Indent(Out, Space, IsDot) << "]," << NL; } + +void RangeConstraintManager::printEquivalenceClass( + raw_ostream &Out, ProgramStateRef State, EquivalenceClass Class) const { + bool FirstMember = true; + SymbolSet ClassMembers = Class.getClassMembers(State); + Out << "[ "; + for (SymbolRef ClassMember : ClassMembers) { + if (FirstMember) + FirstMember = false; + else + Out << ", "; + Out << "\"" << ClassMember << "\""; + } + Out << " ]"; +} + +void RangeConstraintManager::printEquivalenceClasses(raw_ostream &Out, + ProgramStateRef State, + const char *NL, + unsigned int Space, + bool IsDot) const { + ClassMembersTy Members = State->get(); + + Indent(Out, Space, IsDot) << "\"equivalence_classes\": "; + if (Members.isEmpty()) { + Out << "null," << NL; + return; + } + + ++Space; + Out << '[' << NL; + bool FirstClass = true; + for (std::pair ClassToSymbolSet : Members) { + EquivalenceClass Class = ClassToSymbolSet.first; + + if (FirstClass) { + FirstClass = false; + } else { + Out << ','; + Out << NL; + } + Indent(Out, Space, IsDot); + printEquivalenceClass(Out, State, Class); + } + Out << NL; + + --Space; + Indent(Out, Space, IsDot) << "]," << NL; +} + +void RangeConstraintManager::printDisequalities(raw_ostream &Out, + ProgramStateRef State, + const char *NL, + unsigned int Space, + bool IsDot) const { + DisequalityMapTy Disequalities = State->get(); + + Indent(Out, Space, IsDot) << "\"disequality_info\": "; + if (Disequalities.isEmpty()) { + Out << "null," << NL; + return; + } + + ++Space; + Out << '[' << NL; + bool FirstClass = true; + for (std::pair ClassToDisEqSet : Disequalities) { + EquivalenceClass Class = ClassToDisEqSet.first; + if (FirstClass) { + FirstClass = false; + } else { + Out << ','; + Out << NL; + } + Indent(Out, Space, IsDot) << "{" << NL; + unsigned int DisEqSpace = Space + 1; + Indent(Out, DisEqSpace, IsDot) << "\"class\": "; + printEquivalenceClass(Out, State, Class); + ClassSet DisequalClasses = ClassToDisEqSet.second; + if (!DisequalClasses.isEmpty()) { + Out << "," << NL; + Indent(Out, DisEqSpace, IsDot) << "\"disequal_to\": [" << NL; + unsigned int DisEqClassSpace = DisEqSpace + 1; + Indent(Out, DisEqClassSpace, IsDot); + bool FirstDisEqClass = true; + for (EquivalenceClass DisEqClass : DisequalClasses) { + if (FirstDisEqClass) { + FirstDisEqClass = false; + } else { + Out << ',' << NL; + Indent(Out, DisEqClassSpace, IsDot); + } + printEquivalenceClass(Out, State, DisEqClass); + } + Out << "]" << NL; + } + Indent(Out, Space, IsDot) << "}"; + } + Out << NL; + + --Space; + Indent(Out, Space, IsDot) << "]," << NL; +} diff --git a/clang/test/Analysis/expr-inspection-printState-diseq-info.c b/clang/test/Analysis/expr-inspection-printState-diseq-info.c new file mode 100644 index 000000000000..fe2ee324105f --- /dev/null +++ b/clang/test/Analysis/expr-inspection-printState-diseq-info.c @@ -0,0 +1,34 @@ +// RUN: %clang_analyze_cc1 \ +// RUN: -analyzer-checker=debug.ExprInspection %s 2>&1 | FileCheck %s + +void clang_analyzer_printState(); + +void test_disequality_info(int e0, int b0, int b1, int c0) { + int e1 = e0 - b0; + if (b0 == 2) { + int e2 = e1 - b1; + if (e2 > 0) { + if (b1 != c0) + clang_analyzer_printState(); + } + } +} + +// CHECK: "disequality_info": [ +// CHECK-NEXT: { +// CHECK-NEXT: "class": [ "reg_$2" ], +// CHECK-NEXT: "disequal_to": [ +// CHECK-NEXT: [ "(reg_$0) - 2" ], +// CHECK-NEXT: [ "reg_$3" ]] +// CHECK-NEXT: }, +// CHECK-NEXT: { +// CHECK-NEXT: "class": [ "(reg_$0) - 2" ], +// CHECK-NEXT: "disequal_to": [ +// CHECK-NEXT: [ "reg_$2" ]] +// CHECK-NEXT: }, +// CHECK-NEXT: { +// CHECK-NEXT: "class": [ "reg_$3" ], +// CHECK-NEXT: "disequal_to": [ +// CHECK-NEXT: [ "reg_$2" ]] +// CHECK-NEXT: } +// CHECK-NEXT: ], diff --git a/clang/test/Analysis/expr-inspection-printState-eq-classes.c b/clang/test/Analysis/expr-inspection-printState-eq-classes.c new file mode 100644 index 000000000000..5b40ac5cd47e --- /dev/null +++ b/clang/test/Analysis/expr-inspection-printState-eq-classes.c @@ -0,0 +1,21 @@ +// RUN: %clang_analyze_cc1 \ +// RUN: -analyzer-checker=debug.ExprInspection %s 2>&1 | FileCheck %s + +void clang_analyzer_printState(); + +void test_equivalence_classes(int a, int b, int c, int d) { + if (a + b != c) + return; + if (a != d) + return; + if (b != 0) + return; + clang_analyzer_printState(); + (void)(a * b * c * d); + return; +} + +// CHECK: "equivalence_classes": [ +// CHECK-NEXT: [ "reg_$0", "(reg_$0) + (reg_$1)", "reg_$2", "reg_$3" ], +// CHECK-NEXT: [ "((reg_$0) + (reg_$1)) != (reg_$2)", "(reg_$0) != (reg_$2)" ] +// CHECK-NEXT: ], diff --git a/clang/test/Analysis/expr-inspection.c b/clang/test/Analysis/expr-inspection.c index 283fa9bdb724..76118a76e71c 100644 --- a/clang/test/Analysis/expr-inspection.c +++ b/clang/test/Analysis/expr-inspection.c @@ -38,6 +38,8 @@ void foo(int x) { // CHECK-NEXT: "constraints": [ // CHECK-NEXT: { "symbol": "reg_$0", "range": "{ [-2147483648, 13] }" } // CHECK-NEXT: ], +// CHECK-NEXT: "equivalence_classes": null, +// CHECK-NEXT: "disequality_info": null, // CHECK-NEXT: "dynamic_types": null, // CHECK-NEXT: "dynamic_casts": null, // CHECK-NEXT: "constructing_objects": null,