[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.

[Yitzhak Mandelbaum via Phabricator via cfe-commits]

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


================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:237-238
+      case Value::Kind::Top:
+        // Nothing more to do. Each `Top` instance will be mapped to a fresh
+        // variable and is thereafter anonymous.
+        break;
----------------
gribozavr2 wrote:
> 
regarding the latter clause -- its freedom *does* affect satisfiability. e.g.` A || Top` is trivially satisfiable. I'm just going to drop the "and ...".


================
Comment at: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:527-528
+    auto *Prop2 = Val2.getProperty("has_value");
+    return Prop1 == Prop2 || (Prop1 != nullptr && Prop2 != nullptr &&
+                              isTop(*Prop1) && isTop(*Prop2));
   }
----------------
xazax.hun wrote:
> I feel like this logic is repeated multiple times. I wonder if we should define an `operator==` for `const BoolValue*`.
Agreed.  I want to wait until we settle on the representation and then we can consider this operator. But, if we end up with a singleton Top then I think we can hold off.


================
Comment at: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1192
+                         const Environment &Env1, const Value &Val2,
+                         const Environment &Env2) final {
+    // Changes to a sounds approximation, which allows us to test whether we can
----------------
xazax.hun wrote:
> Nit: I usually prefer marking whole classes final rather than individual virtual methods, but feel free to leave as is.
Good point. I was following what's done elsewhere in the file -- I think we should update all or nothing. that said, if you mark the class final, then what do you do with each method? nothing or `override`?


================
Comment at: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1302-1311
+    void target(bool Cond) {
+      bool Foo = makeTop();
+      // Force a new block.
+      if (false) return;
+      (void)0;
+      /*[[p1]]*/
+
----------------
gribozavr2 wrote:
> Similarly in tests below.
> 
> `if (false)` theoretically could be handled in a special way in future and could be folded away during CFG construction.
Sure. I went with a different name since it's playing a very specific role that's not related to the test in the way that `Cond` is.


================
Comment at: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1454
+      });
+}
+
----------------
gribozavr2 wrote:
> Could you add a variant of this test?
> 
> ```
>     void target(bool Cond) {
>       bool Foo = makeTop();
>       // Force a new block.
>       if (false) return;
>       (void)0;
>       /*[[p1]]*/
> 
>       bool Zab;
>       if (Cond) {
>         Zab = Foo;
>       } else {
>         Zab = Foo;
>       }
>       (void)0;
>       if (Zab == Foo) { return; }
>       /*[[p2]]*/
>     }
> ```
> 
> Show the loss of precision by checking that the flow condition for p2 is satisfiable.
Added, but there's no loss of precision and so the test demonstrates that. My initial instinct was that there would be loss, but the guard of `Cond` actually preserves the precision. The cost is complexity -- Zab is a fresh atomic and the flow condition encoded enough information to recover its equivalence to `Foo`. But, it is not _equal_ to `Foo`, which would be nice.

The case where we lose precision is a loop, where the incoming edge doesn't carry a condition.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D135397