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

Add support for correlated branches to the std::optional dataflow model. Differential Revision: https://reviews.llvm.org/D125931 Reviewed-by: ymandel, xazax.hun
llvm · Jun 15, 2022 · 8fcdd62 · 8fcdd62
1 parent 8c7b64b
commit 8fcdd62
Show file tree

Hide file tree

Showing 3 changed files with 378 additions and 4 deletions.
diff --git a/clang/include/clang/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.h b/clang/include/clang/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.h
@@ -59,6 +59,14 @@ class UncheckedOptionalAccessModel
   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;
 };

diff --git a/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp b/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
@@ -169,11 +169,17 @@ auto isCallReturningOptional() {
       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));
 }
 
@@ -274,11 +280,28 @@ void initializeOptionalReference(const Expr *OptionalExpr,
   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 =
@@ -651,5 +674,31 @@ void UncheckedOptionalAccessModel::transfer(const Stmt *S,
   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