[PATCH] D82445: [analyzer][solver] Track symbol equivalence

[Artem Dergachev via Phabricator via cfe-commits]

NoQ accepted this revision.
NoQ added a comment.
This revision is now accepted and ready to land.

🎉!

I vaguely remember that we talked offline about a few nasty test cases that with casts and overflows, would it make sense to add them? Like, even if they don't pass yet, they may prove valuable.



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1472
+  // path compression when dealing with immutability.  That means that we
+  // compress paths every time we do merges.  It also means that we loose
+  // the main amortized complexity benefit from the original data structure.
----------------
"lose"!


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1487
+    //       we shouldn't generate ranges incompatible with equivalence classes.
+    //       However, at the moment, due to imperfections in the solver, it is
+    //       possible and the merge function can also return infeasible states
----------------
"I am the solver!!!"

I guess what you're trying to say is that every time there's an infeasible state here, technically one of the `infer()` functions had a chance to prevent it (not necessarily easily).


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D82445/new/

https://reviews.llvm.org/D82445