[clang][dataflow] Add support for correlated branches to optional model

[sgatev]

Summary

Add support for correlated branches to the std::optional dataflow model.

[ymandel]

Thanks! Looks good overall, just the one question about loops.

clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp

694–696

What's the plan for loops? This will increase the size of the constraint on every iteration, preventing termination.

[xazax.hun]

clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp

694–696

I have nothing to add, just a brain dump. In this particular case, the analysis domain has infinite chains, the size of the Boolean formulas can increase indefinitely (at least syntactically). The canonical solution to deal with infinite chains is to do a widening operation such that the widened state over approximates both the state of the old and the new iteration. A very simple way of doing this would be to simply erase all knowledge we accumulated about the Boolean value. On the other hand, I wonder if it is often possible to do something smarter. There might be cases when the value is syntactically larger in the new iteration but actually it has the exact same truth table. The solver might be able to show this. On the other hand, if the loop generates new Boolean symbols in each iteration, we have little hope fore that.

[xazax.hun]

Actually, I think in most cases we want to be consistent on how to merge bool values. So I wonder whether instead of reimplementing the merge operation in this check we should just call a function that does the work. And the same function should be used within the engine to merge states after if statements and so on.

[ymandel]

In D125931#3525699, @xazax.hun wrote:

Actually, I think in most cases we want to be consistent on how to merge bool values. So I wonder whether instead of reimplementing the merge operation in this check we should just call a function that does the work. And the same function should be used within the engine to merge states after if statements and so on.

Agreed. I think we made a mistake with bools, to be honest, in supporting correlated conditions, given our lack of distinction between join and widen -- something I didn't appreciate fully at the time of the patch. I propose:

1. In this patch, we go with a widening operation, but put the relevant logic in the core, so it can be reused for booleans in general.
2. Follow up with a patch that uses the new logic for general booleans.

clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp

694–696

I have nothing to add, just a brain dump. In this particular case, the analysis domain has infinite chains, the size of the Boolean formulas can increase indefinitely (at least syntactically). The canonical solution to deal with infinite chains is to do a widening operation such that the widened state over approximates both the state of the old and the new iteration. A very simple way of doing this would be to simply erase all knowledge we accumulated about the Boolean value. On the other hand, I wonder if it is often possible to do something smarter. There might be cases when the value is syntactically larger in the new iteration but actually it has the exact same truth table. The solver might be able to show this. On the other hand, if the loop generates new Boolean symbols in each iteration, we have little hope fore that.

Agreed. In our internal implementation, we have something like this -- it consults the solver to see if the two are logically equivalent. That loses the (subtle) support for correlated conditions. However, until we have more precise support for widening (that is, separate from merge), I think this is the only way to go to ensure that loop analysis terminates.

[xazax.hun]

In D125931#3527584, @ymandel wrote:

1. In this patch, we go with a widening operation, but put the relevant logic in the core, so it can be reused for booleans in general.

Depending on how much simplicity are we willing to sacrifice, doing a merge here might be OK. We only need widening to ensure the convergence of loops. Some frameworks are doing the regular merge operator for joins in the CFG and only use the widening operator along the back edges. This way they can be a bit more precise while preserving convergence.

[sgatev]

Rebase main.

[sgatev]

clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp

694–696

After discussing this, we decided to go for the internal implementation which is tested on a large codebase and commit to smarter merging that preserves flow condition information only after testing it extensively. I have updated the patch accordingly, please take a look.

[ymandel]

I love the tests (pretty cool examples of what can be handled). Thanks for the thoroughness!

clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp

174

I believe you can relax this to Value because setProperty is no longer specific to StructValue.

289–291

I think this is no longer necessary now that we don't rely on StructValue for the getProperty call.

700

MergedVal is enough here, assuming the changes suggested above.

[sgatev]

Address comments.

[sgatev]

clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp

174

I did that intentionally because I still think it makes sense to assert that an optional is modeled as a StructValue. I haven't thought about where and how it'd be best to assert that though so I'll happily remove the casts for now.

[ymandel]

clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp

174

Sounds good. I had the same thought. But, it occurs to me that at this point, are we using the StructValue at all? If not, then the only reason we expect it to be a StructValue is because we know the optional type is a record type. But, that's not an assumption of our model. So, maybe we should be agnostic to the underlying representation?

[xazax.hun]

clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp

288

I wonder whether NonEmpty is clearer than Engaged. I think Engaged can also be OK, but we probably want to have a comment somewhere to explain the terminology.

700

Would it make sense to have the converese? I.e., when both optionals are empty, create an empty optional here. While currently this modeling does not distinguish between unchecked and empty optionals it might be handy in the future. Although I am also happy with this as is, not adding any code that does not have any utility as of today.

[sgatev]

Address comments.

[sgatev]

clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp

174

Agreed. Let's not assume a StructValue representation unless it's necessary.

288

Sounds good. I went with isEmptyOptional and isNonEmptyOptional.

700

Good idea! I think this can be useful. I added the code and a test case based on dead code:

if (b) {
  opt = std::nullopt;
} else {
  opt = std::nullopt;
}
if (opt.has_value()) {
  // unreachable
}

clang/include/clang/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.h

public:
 
   static SourceLocationsLattice initialElement() {
     return SourceLocationsLattice();
   }
 
   void transfer(const Stmt *Stmt, SourceLocationsLattice &State,
                 Environment &Env);
 
+  bool compareEquivalent(QualType Type, const Value &Val1,
+                         const Environment &Env1, const Value &Val2,
+                         const Environment &Env2) override;
+
+  bool merge(QualType Type, const Value &Val1, const Environment &Env1,
+             const Value &Val2, const Environment &Env2, Value &MergedVal,
+             Environment &MergedEnv) override;
+
 private:
   MatchSwitch<TransferState<SourceLocationsLattice>> TransferMatchSwitch;
 };
 
 } // namespace dataflow
 } // namespace clang
 
 #endif // CLANG_ANALYSIS_FLOWSENSITIVE_MODELS_UNCHECKEDOPTIONALACCESSMODEL_H

clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp

return binaryOperation(hasOperatorName("!="),
                                ComparesToSame(integerLiteral(equals(0)))));
 }
 
 auto isCallReturningOptional() {
   return callExpr(hasType(qualType(anyOf(
       optionalOrAliasType(), referenceType(pointee(optionalOrAliasType()))))));
 }
 
+/// Sets `HasValueVal` as the symbolic value that represents the "has_value"
+/// property of the optional value `OptionalVal`.
+void setHasValue(Value &OptionalVal, BoolValue &HasValueVal) {
+  OptionalVal.setProperty("has_value", HasValueVal);
+}
+
 /// Creates a symbolic value for an `optional` value using `HasValueVal` as the
 /// symbolic value of its "has_value" property.
 StructValue &createOptionalValue(Environment &Env, BoolValue &HasValueVal) {
   auto OptionalVal = std::make_unique<StructValue>();
-  OptionalVal->setProperty("has_value", HasValueVal);
+  setHasValue(*OptionalVal, HasValueVal);
   return Env.takeOwnership(std::move(OptionalVal));
 }
 
 /// Returns the symbolic value that represents the "has_value" property of the
 /// optional value `OptionalVal`. Returns null if `OptionalVal` is null.
 BoolValue *getHasValue(Environment &Env, Value *OptionalVal) {
   if (OptionalVal != nullptr) {
     auto *HasValueVal =

 }
 
 void initializeOptionalReference(const Expr *OptionalExpr,
                                  const MatchFinder::MatchResult &,
                                  LatticeTransferState &State) {
   if (auto *OptionalVal =
           State.Env.getValue(*OptionalExpr, SkipPast::Reference)) {
     if (OptionalVal->getProperty("has_value") == nullptr) {
-      OptionalVal->setProperty("has_value", State.Env.makeAtomicBoolValue());
+      setHasValue(*OptionalVal, State.Env.makeAtomicBoolValue());
     }
   }
 }
 
+/// Returns true if and only if `OptionalVal` is initialized and known to be
+/// empty in `Env.
+bool isEmptyOptional(const Value &OptionalVal, const Environment &Env) {
+  auto *HasValueVal =
+      cast_or_null<BoolValue>(OptionalVal.getProperty("has_value"));
+  return HasValueVal != nullptr &&
+         Env.flowConditionImplies(Env.makeNot(*HasValueVal));
+}
+
+/// Returns true if and only if `OptionalVal` is initialized and known to be
+/// non-empty in `Env.
+bool isNonEmptyOptional(const Value &OptionalVal, const Environment &Env) {
+  auto *HasValueVal =
+      cast_or_null<BoolValue>(OptionalVal.getProperty("has_value"));
+  return HasValueVal != nullptr && Env.flowConditionImplies(*HasValueVal);
+}
+
 void transferUnwrapCall(const Expr *UnwrapExpr, const Expr *ObjectExpr,
                         LatticeTransferState &State) {
   if (auto *OptionalVal =
           State.Env.getValue(*ObjectExpr, SkipPast::ReferenceThenPointer)) {
     if (State.Env.getStorageLocation(*UnwrapExpr, SkipPast::None) == nullptr)
       if (auto *Loc = maybeInitializeOptionalValueMember(
               UnwrapExpr->getType(), *OptionalVal, State.Env))
         State.Env.setStorageLocation(*UnwrapExpr, *Loc);

 
 void UncheckedOptionalAccessModel::transfer(const Stmt *S,
                                             SourceLocationsLattice &L,
                                             Environment &Env) {
   LatticeTransferState State(L, Env);
   TransferMatchSwitch(*S, getASTContext(), State);
 }
 
+bool UncheckedOptionalAccessModel::compareEquivalent(QualType Type,
+                                                     const Value &Val1,
+                                                     const Environment &Env1,
+                                                     const Value &Val2,
+                                                     const Environment &Env2) {
+  return isNonEmptyOptional(Val1, Env1) == isNonEmptyOptional(Val2, Env2);
+}
+
+bool UncheckedOptionalAccessModel::merge(QualType Type, const Value &Val1,
+                                         const Environment &Env1,
+                                         const Value &Val2,
+                                         const Environment &Env2,
+                                         Value &MergedVal,
+                                         Environment &MergedEnv) {
+  if (!IsOptionalType(Type))
+    return true;
+
+  auto &HasValueVal = MergedEnv.makeAtomicBoolValue();
+  if (isNonEmptyOptional(Val1, Env1) && isNonEmptyOptional(Val2, Env2))
+    MergedEnv.addToFlowCondition(HasValueVal);
+  else if (isEmptyOptional(Val1, Env1) && isEmptyOptional(Val2, Env2))
+    MergedEnv.addToFlowCondition(MergedEnv.makeNot(HasValueVal));
+  setHasValue(MergedVal, HasValueVal);
+  return true;
+}
+
 } // namespace dataflow
 } // namespace clang

clang/unittests/Analysis/FlowSensitive/UncheckedOptionalAccessModelTest.cpp

ExpectLatticeChecksFor(R"(
     void target($ns::$optional<int> *opt) {
       opt->emplace(0);
       opt->value();
       /*[[check]]*/
     }
   )",
                          UnorderedElementsAre(Pair("check", "safe")));
 
-  // FIXME: Add tests that call `emplace` in conditional branches.
+  // FIXME: Add tests that call `emplace` in conditional branches:
+  //  ExpectLatticeChecksFor(
+  //      R"(
+  //    #include "unchecked_optional_access_test.h"
+  //
+  //    void target($ns::$optional<int> opt, bool b) {
+  //      if (b) {
+  //        opt.emplace(0);
+  //      }
+  //      if (b) {
+  //        opt.value();
+  //        /*[[check-1]]*/
+  //      } else {
+  //        opt.value();
+  //        /*[[check-2]]*/
+  //      }
+  //    }
+  //  )",
+  //      UnorderedElementsAre(Pair("check-1", "safe"),
+  //                           Pair("check-2", "unsafe: input.cc:12:9")));
 }
 
 TEST_P(UncheckedOptionalAccessTest, Reset) {
   ExpectLatticeChecksFor(
       R"(
     #include "unchecked_optional_access_test.h"
 
     void target() {
void target($ns::$optional<int> &opt) {
         opt.reset();
         opt.value();
         /*[[check]]*/
       }
     }
   )",
       UnorderedElementsAre(Pair("check", "unsafe: input.cc:7:9")));
 
-  // FIXME: Add tests that call `reset` in conditional branches.
+  // FIXME: Add tests that call `reset` in conditional branches:
+  //  ExpectLatticeChecksFor(
+  //      R"(
+  //    #include "unchecked_optional_access_test.h"
+  //
+  //    void target(bool b) {
+  //      $ns::$optional<int> opt = $ns::make_optional(0);
+  //      if (b) {
+  //        opt.reset();
+  //      }
+  //      if (b) {
+  //        opt.value();
+  //        /*[[check-1]]*/
+  //      } else {
+  //        opt.value();
+  //        /*[[check-2]]*/
+  //      }
+  //    }
+  //  )",
+  //      UnorderedElementsAre(Pair("check-1", "unsafe: input.cc:10:9"),
+  //                           Pair("check-2", "safe")));
 }
 
 TEST_P(UncheckedOptionalAccessTest, ValueAssignment) {
   ExpectLatticeChecksFor(R"(
     #include "unchecked_optional_access_test.h"
 
     struct Foo {};
 
void target() {
       *x = $ns::nullopt;
       (*x).value();
       /*[[check]]*/
     }
   )",
       UnorderedElementsAre(Pair("check", "unsafe: input.cc:12:7")));
 }
 
+TEST_P(UncheckedOptionalAccessTest, CorrelatedBranches) {
+  ExpectLatticeChecksFor(R"code(
+    #include "unchecked_optional_access_test.h"
+
+    void target(bool b, $ns::$optional<int> opt) {
+      if (b || opt.has_value()) {
+        if (!b) {
+          opt.value();
+          /*[[check-1]]*/
+        }
+      }
+    }
+  )code",
+                         UnorderedElementsAre(Pair("check-1", "safe")));
+
+  ExpectLatticeChecksFor(R"code(
+    #include "unchecked_optional_access_test.h"
+
+    void target(bool b, $ns::$optional<int> opt) {
+      if (b && !opt.has_value()) return;
+      if (b) {
+        opt.value();
+        /*[[check-2]]*/
+      }
+    }
+  )code",
+                         UnorderedElementsAre(Pair("check-2", "safe")));
+
+  ExpectLatticeChecksFor(
+      R"code(
+    #include "unchecked_optional_access_test.h"
+
+    void target(bool b, $ns::$optional<int> opt) {
+      if (opt.has_value()) b = true;
+      if (b) {
+        opt.value();
+        /*[[check-3]]*/
+      }
+    }
+  )code",
+      UnorderedElementsAre(Pair("check-3", "unsafe: input.cc:7:9")));
+
+  ExpectLatticeChecksFor(R"code(
+    #include "unchecked_optional_access_test.h"
+
+    void target(bool b, $ns::$optional<int> opt) {
+      if (b) return;
+      if (opt.has_value()) b = true;
+      if (b) {
+        opt.value();
+        /*[[check-4]]*/
+      }
+    }
+  )code",
+                         UnorderedElementsAre(Pair("check-4", "safe")));
+
+  ExpectLatticeChecksFor(R"(
+    #include "unchecked_optional_access_test.h"
+
+    void target(bool b, $ns::$optional<int> opt) {
+      if (opt.has_value() == b) {
+        if (b) {
+          opt.value();
+          /*[[check-5]]*/
+        }
+      }
+    }
+  )",
+                         UnorderedElementsAre(Pair("check-5", "safe")));
+
+  ExpectLatticeChecksFor(R"(
+    #include "unchecked_optional_access_test.h"
+
+    void target(bool b, $ns::$optional<int> opt) {
+      if (opt.has_value() != b) {
+        if (!b) {
+          opt.value();
+          /*[[check-6]]*/
+        }
+      }
+    }
+  )",
+                         UnorderedElementsAre(Pair("check-6", "safe")));
+
+  ExpectLatticeChecksFor(R"(
+    #include "unchecked_optional_access_test.h"
+
+    void target(bool b) {
+      $ns::$optional<int> opt1 = $ns::nullopt;
+      $ns::$optional<int> opt2;
+      if (b) {
+        opt2 = $ns::nullopt;
+      } else {
+        opt2 = $ns::nullopt;
+      }
+      if (opt2.has_value()) {
+        opt1.value();
+        /*[[check]]*/
+      }
+    }
+  )",
+                         UnorderedElementsAre(Pair("check", "safe")));
+
+  // FIXME: Add support for operator==.
+  // ExpectLatticeChecksFor(R"(
+  //   #include "unchecked_optional_access_test.h"
+  //
+  //   void target($ns::$optional<int> opt1, $ns::$optional<int> opt2) {
+  //     if (opt1 == opt2) {
+  //       if (opt1.has_value()) {
+  //         opt2.value();
+  //         /*[[check-7]]*/
+  //       }
+  //     }
+  //   }
+  // )",
+  //                     UnorderedElementsAre(Pair("check-7", "safe")));
+}
+
+TEST_P(UncheckedOptionalAccessTest, JoinDistinctValues) {
+  ExpectLatticeChecksFor(
+      R"code(
+    #include "unchecked_optional_access_test.h"
+
+    void target(bool b) {
+      $ns::$optional<int> opt;
+      if (b) {
+        opt = Make<$ns::$optional<int>>();
+      } else {
+        opt = Make<$ns::$optional<int>>();
+      }
+      if (opt.has_value()) {
+        opt.value();
+        /*[[check-1]]*/
+      } else {
+        opt.value();
+        /*[[check-2]]*/
+      }
+    }
+  )code",
+      UnorderedElementsAre(Pair("check-1", "safe"),
+                           Pair("check-2", "unsafe: input.cc:15:9")));
+
+  ExpectLatticeChecksFor(R"code(
+    #include "unchecked_optional_access_test.h"
+
+    void target(bool b) {
+      $ns::$optional<int> opt;
+      if (b) {
+        opt = Make<$ns::$optional<int>>();
+        if (!opt.has_value()) return;
+      } else {
+        opt = Make<$ns::$optional<int>>();
+        if (!opt.has_value()) return;
+      }
+      opt.value();
+      /*[[check-3]]*/
+    }
+  )code",
+                         UnorderedElementsAre(Pair("check-3", "safe")));
+
+  ExpectLatticeChecksFor(
+      R"code(
+    #include "unchecked_optional_access_test.h"
+
+    void target(bool b) {
+      $ns::$optional<int> opt;
+      if (b) {
+        opt = Make<$ns::$optional<int>>();
+        if (!opt.has_value()) return;
+      } else {
+        opt = Make<$ns::$optional<int>>();
+      }
+      opt.value();
+      /*[[check-4]]*/
+    }
+  )code",
+      UnorderedElementsAre(Pair("check-4", "unsafe: input.cc:12:7")));
+
+  ExpectLatticeChecksFor(
+      R"code(
+    #include "unchecked_optional_access_test.h"
+
+    void target(bool b) {
+      $ns::$optional<int> opt;
+      if (b) {
+        opt = 1;
+      } else {
+        opt = 2;
+      }
+      opt.value();
+      /*[[check-5]]*/
+    }
+  )code",
+      UnorderedElementsAre(Pair("check-5", "safe")));
+
+  ExpectLatticeChecksFor(
+      R"code(
+    #include "unchecked_optional_access_test.h"
+
+    void target(bool b) {
+      $ns::$optional<int> opt;
+      if (b) {
+        opt = 1;
+      } else {
+        opt = Make<$ns::$optional<int>>();
+      }
+      opt.value();
+      /*[[check-6]]*/
+    }
+  )code",
+      UnorderedElementsAre(Pair("check-6", "unsafe: input.cc:11:7")));
+}
+
+TEST_P(UncheckedOptionalAccessTest, ReassignValueInLoop) {
+  ExpectLatticeChecksFor(R"(
+    #include "unchecked_optional_access_test.h"
+
+    void target() {
+      $ns::$optional<int> opt = 3;
+      while (Make<bool>()) {
+        opt.value();
+        /*[[check-1]]*/
+      }
+    }
+  )",
+                         UnorderedElementsAre(Pair("check-1", "safe")));
+
+  ExpectLatticeChecksFor(R"(
+    #include "unchecked_optional_access_test.h"
+
+    void target() {
+      $ns::$optional<int> opt = 3;
+      while (Make<bool>()) {
+        opt.value();
+        /*[[check-2]]*/
+
+        opt = Make<$ns::$optional<int>>();
+        if (!opt.has_value()) return;
+      }
+    }
+  )",
+                         UnorderedElementsAre(Pair("check-2", "safe")));
+
+  ExpectLatticeChecksFor(
+      R"(
+    #include "unchecked_optional_access_test.h"
+
+    void target() {
+      $ns::$optional<int> opt = 3;
+      while (Make<bool>()) {
+        opt.value();
+        /*[[check-3]]*/
+
+        opt = Make<$ns::$optional<int>>();
+      }
+    }
+  )",
+      UnorderedElementsAre(Pair("check-3", "unsafe: input.cc:7:9")));
+
+  ExpectLatticeChecksFor(
+      R"(
+    #include "unchecked_optional_access_test.h"
+
+    void target() {
+      $ns::$optional<int> opt = 3;
+      while (Make<bool>()) {
+        opt.value();
+        /*[[check-4]]*/
+
+        opt = Make<$ns::$optional<int>>();
+        if (!opt.has_value()) continue;
+      }
+    }
+  )",
+      UnorderedElementsAre(Pair("check-4", "unsafe: input.cc:7:9")));
+}
+
 // FIXME: Add support for:
 // - constructors (copy, move)
 // - assignment operators (default, copy, move)
 // - invalidation (passing optional by non-const reference/pointer)