[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

2537

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 inline ClassSet
   getDisequalClasses(ProgramStateRef State) const;
   LLVM_NODISCARD inline ClassSet
   getDisequalClasses(DisequalityMapTy Map, ClassSet::Factory &Factory) const;
 
   LLVM_NODISCARD static inline Optional<bool>
   areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);
 
+  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();
   }
 
private:
   /// This is a unique identifier of the class.
   uintptr_t ID;
 };
 
 //===----------------------------------------------------------------------===//
 //                             Constraint functions
 //===----------------------------------------------------------------------===//
 
+/// Dump all equivalence classes.
+LLVM_DUMP_METHOD static void dumpEqToStream(ProgramStateRef State,
+                                            raw_ostream &os) {
+  ClassMembersTy Members = State->get<ClassMembers>();
+  for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members) {
+    EquivalenceClass Class = ClassToSymbolSet.first;
+    Class.dumpToStream(State, os);
+    os << "\n";
+  }
+}
+LLVM_DUMP_METHOD static void dumpEq(ProgramStateRef State) {
+  dumpEqToStream(State, llvm::errs());
+}
+
+/// Dump all equivalence classes along with their disequivalent classes if they
+/// have any.
+LLVM_DUMP_METHOD static void dumpDisEqToStream(ProgramStateRef State,
+                                               raw_ostream &os) {
+  DisequalityMapTy Disequalities = State->get<DisequalityMap>();
+  for (std::pair<EquivalenceClass, ClassSet> ClassToDisEqSet : Disequalities) {
+    EquivalenceClass Class = ClassToDisEqSet.first;
+    Class.dumpToStream(State, os);
+    ClassSet DisequalClasses = ClassToDisEqSet.second;
+    if (!DisequalClasses.isEmpty()) {
+      for (EquivalenceClass DisEqClass : DisequalClasses) {
+        os << "DisequalTo:\n";
+        DisEqClass.dumpToStream(State, os);
+      }
+    }
+    os << "\n";
+  }
+}
+LLVM_DUMP_METHOD static void dumpDisEq(ProgramStateRef State) {
+  dumpDisEqToStream(State, llvm::errs());
+}
+
+//===----------------------------------------------------------------------===//
+//                             Constraint functions
+//===----------------------------------------------------------------------===//
+
 LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED bool
 areFeasible(ConstraintRangeTy Constraints) {
   return llvm::none_of(
       Constraints,
       [](const std::pair<EquivalenceClass, RangeSet> &ClassConstraint) {
         return ClassConstraint.second.isEmpty();
       });
 }
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) {
   // We store far from all Symbol -> Class mappings
   if (const EquivalenceClass *NontrivialClass = State->get<ClassMap>(Sym))
     return *NontrivialClass;
 
   // This is a trivial class of Sym.
   return Sym;
for (SymbolRef ClassMember : ClassMembers) {
       P.second.dump(Out);
       Out << "\" }";
     }
   }
   Out << NL;
 
   --Space;
   Indent(Out, Space, IsDot) << "]," << NL;
 }