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

[Dmitri Gribenko via Phabricator via cfe-commits]

gribozavr2 added inline comments.


================
Comment at: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:157
+  TopValue &createTop() {
+    return takeOwnership(std::make_unique<TopValue>());
+  }
----------------
Should we be creating a new top every time, or should it be a singleton like true and false?

It seems like we explicitly don't care about its identity (or else it would be isomorphic to AtomicBool).


================
Comment at: clang/include/clang/Analysis/FlowSensitive/Value.h:97
+/// formulas.
+class TopValue final : public BoolValue {
+public:
----------------
Here and throughout the patch: since we might have a top for other kinds of values, WDYT about renaming this type to TopBoolValue? Similarly createTop -> createTopBool ?


================
Comment at: clang/include/clang/Analysis/FlowSensitive/Value.h:102
+  static bool classof(const Value *Val) { return Val->getKind() == Kind::Top; }
+};
+
----------------
Since TopValue is a BoolValue, can we form say a ConjunctionValue where LHS or RHS is Top?

What if we create such a conjunction twice? It seems like such conjunctions would incorrectly compare equal, even though each Top will be replaced with a unique fresh variable.

Would it make sense to change our factory functions for boolean formulas to eagerly open Top?

Then we wouldn't need a recursive walk in unpackValue().


================
Comment at: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp:378
+    if (Val == It->second || (Val->getKind() == Value::Kind::Top &&
+                              It->second->getKind() == Value::Kind::Top)) {
       JoinedEnv.LocToVal.insert({Loc, Val});
----------------
isa<Top>


================
Comment at: clang/lib/Analysis/FlowSensitive/Transfer.cpp:76
+  case Value::Kind::AtomicBool:
+    return V;
+
----------------
llvm_unreachable(); because this can't happen, V is a BoolValue.


================
Comment at: clang/lib/Analysis/FlowSensitive/Transfer.cpp:123-124
+  return &UnpackedVal;
+}
+
+
----------------



================
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;
----------------



================
Comment at: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:469
 
+static bool isTop(Value &V) { return V.getKind() == Value::Kind::Top; }
+static bool isAtomic(Value &V) {
----------------
`isa<Top>(...)`? and `isa<AtomicBool>(...)` below?


================
Comment at: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:621
+        EXPECT_EQ(GetFooValue(Env3)->getProperty("has_value")->getKind(),
+                  Value::Kind::Top);
       });
----------------
`EXPECT_TRUE(isa<Top>(...))` ?


================
Comment at: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1193
+                         const Environment &Env2) final {
+    // Changes to a sounds approximation, which allows us to test whether we can
+    // (soundly) converge for some loops.
----------------



================
Comment at: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1220-1221
+
+    // void target(bool Foo) {
+    void target() {
+      bool Foo = makeTop();
----------------



================
Comment at: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1292
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isTop(*FooVal2));
+
----------------



================
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]]*/
+
----------------
Similarly in tests below.

`if (false)` theoretically could be handled in a special way in future and could be folded away during CFG construction.


================
Comment at: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1436-1440
+        const ValueDecl *Zab1Decl = findValueDecl(AO.ASTCtx, "Zab1");
+        ASSERT_THAT(Zab1Decl, NotNull());
+
+        const ValueDecl *Zab2Decl = findValueDecl(AO.ASTCtx, "Zab2");
+        ASSERT_THAT(Zab2Decl, NotNull());
----------------
Zab1Decl, Zab2Decl are unused apart from the NotNull check (which does not seem interesting to me).


================
Comment at: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1454
+      });
+}
+
----------------
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.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D135397