[Analyzer][solver] Add dump methods for (dis)equality classes.

This proved to be very useful during debugging.

Differential Revision: https://reviews.llvm.org/D103967
This commit is contained in:
Gabor Marton 2021-06-09 17:03:47 +02:00
parent ad81dea9f6
commit 6f3b775c3e
4 changed files with 195 additions and 0 deletions

View File

@ -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<ConstraintRange>();
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<ClassMembers>();
Indent(Out, Space, IsDot) << "\"equivalence_classes\": ";
if (Members.isEmpty()) {
Out << "null," << NL;
return;
}
++Space;
Out << '[' << NL;
bool FirstClass = true;
for (std::pair<EquivalenceClass, SymbolSet> 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<DisequalityMap>();
Indent(Out, Space, IsDot) << "\"disequality_info\": ";
if (Disequalities.isEmpty()) {
Out << "null," << NL;
return;
}
++Space;
Out << '[' << NL;
bool FirstClass = true;
for (std::pair<EquivalenceClass, ClassSet> 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;
}

View File

@ -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<int b1>" ],
// CHECK-NEXT: "disequal_to": [
// CHECK-NEXT: [ "(reg_$0<int e0>) - 2" ],
// CHECK-NEXT: [ "reg_$3<int c0>" ]]
// CHECK-NEXT: },
// CHECK-NEXT: {
// CHECK-NEXT: "class": [ "(reg_$0<int e0>) - 2" ],
// CHECK-NEXT: "disequal_to": [
// CHECK-NEXT: [ "reg_$2<int b1>" ]]
// CHECK-NEXT: },
// CHECK-NEXT: {
// CHECK-NEXT: "class": [ "reg_$3<int c0>" ],
// CHECK-NEXT: "disequal_to": [
// CHECK-NEXT: [ "reg_$2<int b1>" ]]
// CHECK-NEXT: }
// CHECK-NEXT: ],

View File

@ -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<int a>", "(reg_$0<int a>) + (reg_$1<int b>)", "reg_$2<int c>", "reg_$3<int d>" ],
// CHECK-NEXT: [ "((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)", "(reg_$0<int a>) != (reg_$2<int c>)" ]
// CHECK-NEXT: ],

View File

@ -38,6 +38,8 @@ void foo(int x) {
// CHECK-NEXT: "constraints": [
// CHECK-NEXT: { "symbol": "reg_$0<int x>", "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,