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

[Yitzhak Mandelbaum via Phabricator via cfe-commits]

ymandel marked 3 inline comments as done.
ymandel added inline comments.


================
Comment at: clang/lib/Analysis/FlowSensitive/Transfer.cpp:53
+  if (auto *LHSValue = dyn_cast_or_null<BoolValue>(
+          Env.getValue(*LHSNorm, SkipPast::Reference)))
+    if (auto *RHSValue = dyn_cast_or_null<BoolValue>(
----------------
sgatev wrote:
> Do we need to skip past references here? If so, then let's add a test that fails if these are changed to `SkipPast::None`.
Yes -- both of the new tests fail when we don't do this. It's actually hard to construct a test that passes without this, since `DeclRefExpr`s of boolean type are `ReferenceValue`.


================
Comment at: clang/lib/Analysis/FlowSensitive/Transfer.cpp:56
+            Env.getValue(*RHSNorm, SkipPast::Reference)))
+      return Env.makeIff(*LHSValue, *RHSValue);
+
----------------
ymandel wrote:
> 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).
I think this connects to our discussion here: https://reviews.llvm.org/D122838?id=419518#inline-1175582

This seems like another example where tracking equivalences in the environment would be beneficial.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D122830