Skip to content

Commit

Permalink
[Analyzer][solver] Add dump methods for (dis)equality classes.
Browse files Browse the repository at this point in the history 
This proved to be very useful during debugging.

Differential Revision: https://reviews.llvm.org/D103967
  • Loading branch information
Gabor Marton committed Jun 28, 2021
1 parent ad81dea commit 6f3b775
Show file tree
Hide file tree
Showing 4 changed files with 195 additions and 0 deletions.
138 changes: 138 additions & 0 deletions clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
View file
Expand Up @@ -594,6 +594,11 @@ class EquivalenceClass : public llvm::FoldingSetNode {
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);
Expand Down Expand Up @@ -1414,6 +1419,17 @@ class RangeConstraintManager : public RangedConstraintManager {

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.
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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\": ";
Expand Down Expand Up @@ -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;
}
34 changes: 34 additions & 0 deletions clang/test/Analysis/expr-inspection-printState-diseq-info.c
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: ],
21 changes: 21 additions & 0 deletions clang/test/Analysis/expr-inspection-printState-eq-classes.c
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: ],
2 changes: 2 additions & 0 deletions clang/test/Analysis/expr-inspection.c
View file
Expand Up @@ -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,
Expand Down

0 comments on commit 6f3b775

Please sign in to comment.