[PATCH] D122830: [clang][dataflow] Add support for (built-in) (in)equality operators

[Yitzhak Mandelbaum via Phabricator via cfe-commits]

ymandel marked an inline comment as done.
ymandel added inline comments.


================
Comment at: clang/lib/Analysis/FlowSensitive/Transfer.cpp:56
+            Env.getValue(*RHSNorm, SkipPast::Reference)))
+      return Env.makeIff(*LHSValue, *RHSValue);
+
----------------
xazax.hun wrote:
> I think a possible alternative way to handle this is to do some sort of "unification" for the two values. The current approach is superior in the sense that solving and generating constraints are clearly separate. Also this might be better for generating useful error messages. In case the solver ever becomes a bottleneck, I wonder whether replacing this with a unification step would speed things up a bit. 
> Although that would only work for the equality case.
That's a good point. Although I wonder if we could get the best of both worlds by adding a unification pre-step to the solver itself, basically looking for `iff` patterns of this sort. Then, the solver could keep a record of such unifications which it could export for diagnostic purposes.

On a related note, another potential use of unification is in equivalence testing of environments. Instead of strict equality of flow conditions, for example, I could imagine equivalence up to unification (aka. renaming of atoms).


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D122830