[PATCH] D130519: [clang][dataflow] Add explicit "AST" nodes for implications and iff

Gábor Horváth via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Mon Jul 25 15:26:57 PDT 2022


xazax.hun added inline comments.


================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:332
+
+      if (LeftSubVar == RightSubVar) {
+        // `X <=> (A <=> A)` is equvalent to `X` which is already in
----------------
gribozavr2 wrote:
> xazax.hun wrote:
> > xazax.hun wrote:
> > > I wonder why this simplification is done here only for `BiconditionalValue`. Other operations seem to not do these sorts of simplifications. Also, when would we take this branch? `getOrCreateIff` has a special case when both operands are the same. 
> > Oh, looking at the other patch I see it mentioning desugaring. So can desugaring also introduce `Biconditional`s?
> It is also necessary in the other cases due to the precondition of `addClause()`, I'm adding that special handling in a separate patch: https://reviews.llvm.org/D130522
> 
> We would take this branch when someone avoids using the DataflowContext API. So not extremely likely at the moment, but it is a latent bug that can be exposed by some future refactoring.
I see, thanks! 


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D130519



More information about the cfe-commits mailing list