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

[martong]

Summary

This proved to be very useful during debugging.

[martong]

• Change comment

[vsavchenko]

This is definitely useful! Thanks!
I was just wondering if we should add it into the state printer instead. @NoQ what's your take on this?

[NoQ]

Yes we should definitely have as much as possible in the state dump.

[martong]

• Extend printJson to handle equivalency info

[martong]

In D103967#2809590, @NoQ wrote:

Yes we should definitely have as much as possible in the state dump.

Okay, I've updated likewise and added two test files to check them in State->dump.

[steakhal]

I suspect that the exploded-graph-rewriter should be updated as well so that the HTML dumps also carry this information.

[martong]

In D103967#2822287, @steakhal wrote:

I suspect that the exploded-graph-rewriter should be updated as well so that the HTML dumps also carry this information.

I've put that into a separate patch because that change has its own complexity. Plus, I think this patch is meaningful and useful by itself (without the exploded-graph-rewriter changes).
https://reviews.llvm.org/D104917

[vsavchenko]

Awesome, thanks!

[thakis]

This breaks tests on Windows: http://45.33.8.238/win/40864/step_7.txt

Please take a look, and please revert if it takes a while to fix.

[martong]

Thanks for the report @thakis ! This seems to be b/c of the different newline handling in windows. I've committed a change that disables the tests on windows.

[thakis]

Thanks. Looks like it flakily fails on mac too every now and then: http://45.33.8.238/mac/33005/step_7.txt

Maybe you print something in nondeterministic iteration order?

[vsavchenko]

In D103967#2844140, @thakis wrote:

Thanks. Looks like it flakily fails on mac too every now and then: http://45.33.8.238/mac/33005/step_7.txt

Maybe you print something in nondeterministic iteration order?

Yes, I think that the problem is deeper. ClassMembers is llvm::ImmutableSet (i.e. sorted set), and it uses SymbolRef (e.g. pointer values) for sorting. So, it does look like the order can be nondeterministic.
However, when we print constraints, we should see similar problems, but we don't 🤔

[thakis]

Cool, can we revert this for now then? Flakily failing on my m1 bot too: http://45.33.8.238/macm1/12514/step_7.txt

[thakis]

Reverted for now in d5402a2fee5d860e20378f819e200865af3a6113

[thakis]

(here's another flaky failure that was due to this: http://45.33.8.238/mac/33008/step_7.txt )

[martong]

I have changed the dump methods to order the equivalence classes and the disequality info available before printing them out. The ordering is done based on their string representation. This comes necessarily with some performance penalty, though otherwise it is impossible (or practically way too cumbersome) to write deterministic tests. Also, the dump is used either from the debugger or from small test cases or when we create an exploded graph (which is again intended to be used during debugging), so I think that the penalty induced by the sorting won't be an issue.

[martong]

• Change the dump methods to order the equivalence classes and the disequality info available before printing them out

[martong]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2716

Ah, SmallSet is not sorted :( I am gonna have to change this to either std::set or to a sorted vector :(

[martong]

• Use std::set for ordering

[steakhal]

AFAICT this patch does not introduce significant overhead to the exploded graph DOT dumps.
Before the patch, an exploded graph took 12G and about 55 secs for a single top-level function.
After the patch, it increased to 13G, and the runtime remained the same as expected.

Which is about a 1.5 % increase in size in total. TBH I expected slightly higher numbers.

This benchmark was done using a release build with dumps, asserts, and expensive checks.

[martong]

In D103967#2864229, @steakhal wrote:

AFAICT this patch does not introduce significant overhead to the exploded graph DOT dumps.
Before the patch, an exploded graph took 12G and about 55 secs for a single top-level function.
After the patch, it increased to 13G, and the runtime remained the same as expected.

Which is about a 1.5 % increase in size in total. TBH I expected slightly higher numbers.

This benchmark was done using a release build with dumps, asserts, and expensive checks.

Thanks Balázs for the benchmark, this makes me confident to commit. Hopefully this time the tests won't be flaky.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

public:
   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);
 
+  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);
 
   LLVM_NODISCARD QualType getType() const {
     return getRepresentativeSymbol()->getType();
   }
 
public:
   const llvm::APSInt *getSymVal(ProgramStateRef State,
                                 SymbolRef Sym) const override;
 
   ProgramStateRef removeDeadBindings(ProgramStateRef State,
                                      SymbolReaper &SymReaper) override;
 
   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 printDisequalities(raw_ostream &Out, ProgramStateRef State,
+                          const char *NL = "\n", unsigned int Space = 0,
+                          bool IsDot = false) const;
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from RangedConstraintManager.
   //===------------------------------------------------------------------===//
 
   ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
                               const llvm::APSInt &Adjustment) override;
ConstraintMap ento::getConstraintMap(ProgramStateRef State) {
 
   return Result;
 }
 
 //===----------------------------------------------------------------------===//
 //                     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");
   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;
 

 
 //===----------------------------------------------------------------------===//
 // Pretty-printing.
 //===----------------------------------------------------------------------===//
 
 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\": ";
   if (Constraints.isEmpty()) {
     Out << "null," << NL;
     return;
   }
 
for (SymbolRef ClassMember : ClassMembers) {
       Out << "\" }";
     }
   }
   Out << NL;
 
   --Space;
   Indent(Out, Space, IsDot) << "]," << NL;
 }
+
+static std::string toString(const SymbolRef &Sym) {
+  std::string S;
+  llvm::raw_string_ostream O(S);
+  Sym->dumpToStream(O);
+  return O.str();
+}
+
+static std::string toString(ProgramStateRef State, EquivalenceClass Class) {
+  SymbolSet ClassMembers = Class.getClassMembers(State);
+  llvm::SmallVector<SymbolRef, 8> ClassMembersSorted(ClassMembers.begin(),
+                                                     ClassMembers.end());
+  llvm::sort(ClassMembersSorted,
+             [](const SymbolRef &LHS, const SymbolRef &RHS) {
+               return toString(LHS) < toString(RHS);
+             });
+
+  bool FirstMember = true;
+
+  std::string Str;
+  llvm::raw_string_ostream Out(Str);
+  Out << "[ ";
+  for (SymbolRef ClassMember : ClassMembersSorted) {
+    if (FirstMember)
+      FirstMember = false;
+    else
+      Out << ", ";
+    Out << "\"" << ClassMember << "\"";
+  }
+  Out << " ]";
+  return Out.str();
+}
+
+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;
+  }
+
+  std::set<std::string> MembersStr;
+  for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members)
+    MembersStr.insert(toString(State, ClassToSymbolSet.first));
+
+  ++Space;
+  Out << '[' << NL;
+  bool FirstClass = true;
+  for (const std::string &Str : MembersStr) {
+    if (FirstClass) {
+      FirstClass = false;
+    } else {
+      Out << ',';
+      Out << NL;
+    }
+    Indent(Out, Space, IsDot);
+    Out << Str;
+  }
+  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;
+  }
+
+  // Transform the disequality info to an ordered map of
+  // [string -> (ordered set of strings)]
+  using EqClassesStrTy = std::set<std::string>;
+  using DisequalityInfoStrTy = std::map<std::string, EqClassesStrTy>;
+  DisequalityInfoStrTy DisequalityInfoStr;
+  for (std::pair<EquivalenceClass, ClassSet> ClassToDisEqSet : Disequalities) {
+    EquivalenceClass Class = ClassToDisEqSet.first;
+    ClassSet DisequalClasses = ClassToDisEqSet.second;
+    EqClassesStrTy MembersStr;
+    for (EquivalenceClass DisEqClass : DisequalClasses)
+      MembersStr.insert(toString(State, DisEqClass));
+    DisequalityInfoStr.insert({toString(State, Class), MembersStr});
+  }
+
+  ++Space;
+  Out << '[' << NL;
+  bool FirstClass = true;
+  for (std::pair<std::string, EqClassesStrTy> ClassToDisEqSet :
+       DisequalityInfoStr) {
+    const std::string &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\": ";
+    Out << Class;
+    const EqClassesStrTy &DisequalClasses = ClassToDisEqSet.second;
+    if (!DisequalClasses.empty()) {
+      Out << "," << NL;
+      Indent(Out, DisEqSpace, IsDot) << "\"disequal_to\": [" << NL;
+      unsigned int DisEqClassSpace = DisEqSpace + 1;
+      Indent(Out, DisEqClassSpace, IsDot);
+      bool FirstDisEqClass = true;
+      for (const std::string &DisEqClass : DisequalClasses) {
+        if (FirstDisEqClass) {
+          FirstDisEqClass = false;
+        } else {
+          Out << ',' << NL;
+          Indent(Out, DisEqClassSpace, IsDot);
+        }
+        Out << DisEqClass;
+      }
+      Out << "]" << NL;
+    }
+    Indent(Out, Space, IsDot) << "}";
+  }
+  Out << NL;
+
+  --Space;
+  Indent(Out, Space, IsDot) << "]," << NL;
+}

clang/test/Analysis/expr-inspection-printState-diseq-info.c

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

clang/test/Analysis/expr-inspection-printState-eq-classes.c

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

clang/test/Analysis/expr-inspection.c

 // CHECK-NEXT:   "environment": { "pointer": "{{0x[0-9a-f]+}}", "items": [
 // CHECK-NEXT:     { "lctx_id": {{[0-9]+}}, "location_context": "#0 Call", "calling": "foo", "location": null, "items": [
 // CHECK-NEXT:       { "stmt_id": {{[0-9]+}}, "pretty": "clang_analyzer_printState", "value": "&code{clang_analyzer_printState}" }
 // CHECK-NEXT:     ]}
 // CHECK-NEXT:   ]},
 // 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,
 // CHECK-NEXT:   "checker_messages": null
 // CHECK-NEXT: }
 
 struct S {
   int x, y;
 };
 
 void test_field_dumps(struct S s, struct S *p) {
   clang_analyzer_dump_pointer(&s.x); // expected-warning{{&s.x}}
   clang_analyzer_dump_pointer(&p->x); // expected-warning{{&SymRegion{reg_$1<struct S * p>}.x}}
 }