[clang][dataflow] Factor out built-in boolean model into an explicit module.

clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h

@@ -500,6 +500,9 @@ class Environment {
     return cast_or_null<T>(getValue(E));
   }
 
+  std::optional<bool> getAtomValue(Atom A) const;
+  void setAtomValue(Atom A, bool);
+
   // FIXME: should we deprecate the following & call arena().create() directly?
 
   /// Creates a `T` (some subclass of `Value`), forwarding `args` to the
@@ -720,6 +723,7 @@ class Environment {
   // deterministic sequence. This in turn produces deterministic SAT formulas.
   llvm::MapVector<const Expr *, Value *> ExprToVal;
   llvm::MapVector<const StorageLocation *, Value *> LocToVal;
+  llvm::MapVector<Atom, bool> AtomToVal;
 
   Atom FlowConditionToken;
 };

clang/include/clang/Analysis/FlowSensitive/Transfer.h

@@ -48,6 +48,12 @@ class StmtToEnvMap {
   const TypeErasedDataflowAnalysisState &CurState;
 };
 
+namespace bool_model {
+
+BoolValue &freshBoolValue(Environment &Env);
+
+} // namespace bool_model
+
 /// Evaluates `S` and updates `Env` accordingly.
 ///
 /// Requirements:

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

@@ -29,6 +29,169 @@
 namespace clang {
 namespace dataflow {
 
+namespace simple_bool_model {
+static std::optional<bool> getLiteralValue(const Formula &F,
+                                           const Environment &Env) {
+  switch (F.kind()) {
+  case Formula::AtomRef:
+    return Env.getAtomValue(F.getAtom());
+  case Formula::Literal:
+    return F.literal();
+  case Formula::Not: {
+    ArrayRef<const Formula *> Operands = F.operands();
+    assert(Operands.size() == 1);
+    if (std::optional<bool> Maybe = getLiteralValue(*Operands[0], Env))
+      return !*Maybe;
+    return std::nullopt;
+  }
+  case Formula::And: {
+    ArrayRef<const Formula *> Operands = F.operands();
+    assert(Operands.size() == 2);
+    auto &LHS = *Operands[0];
+    auto &RHS = *Operands[1];
+    if (std::optional<bool> Left = getLiteralValue(LHS, Env))
+      return !*Left ? Left : getLiteralValue(RHS, Env);
+    if (std::optional<bool> Right = getLiteralValue(RHS, Env); Right == false)
+      return Right;
+    return std::nullopt;
+  }
+  case Formula::Or: {
+    ArrayRef<const Formula *> Operands = F.operands();
+    assert(Operands.size() == 2);
+    auto &LHS = *Operands[0];
+    auto &RHS = *Operands[1];
+    if (std::optional<bool> Left = getLiteralValue(LHS, Env))
+      return *Left ? Left : getLiteralValue(RHS, Env);
+    if (std::optional<bool> Right = getLiteralValue(RHS, Env); Right == true)
+      return Right;
+    return std::nullopt;
+  }
+  case Formula::Equal: {
+    ArrayRef<const Formula *> Operands = F.operands();
+    assert(Operands.size() == 2);
+    auto &LHS = *Operands[0];
+    auto &RHS = *Operands[1];
+    if (&LHS == &RHS)
+      return true;
+    auto V_L = getLiteralValue(LHS, Env);
+    return V_L.has_value() && V_L == getLiteralValue(RHS, Env);
+  }
+  default:
+    return std::nullopt;
+  }
+}
+
+// Updates atom settings in `Env` based on the formula. `AtomVal` indicates the
+// value to use for atoms encountered in the formula.
+static void assumeFormula(bool AtomVal, const Formula &F, Environment &Env) {
+  switch (F.kind()) {
+  case Formula::AtomRef:
+    // FIXME: if the atom is set to a different value, mark the block as
+    // unreachable.
+    Env.setAtomValue(F.getAtom(), AtomVal);
+    break;
+  case Formula::Literal:
+    // FIXME: if the literal is `false`, mark the block as unreachable.
+    break;
+  case Formula::Not: {
+    ArrayRef<const Formula *> Operands = F.operands();
+    assert(Operands.size() == 1);
+    assumeFormula(!AtomVal, *Operands[0], Env);
+    break;
+  }
+  case Formula::And: {
+    if (AtomVal == true) {
+      ArrayRef<const Formula *> Operands = F.operands();
+      assert(Operands.size() == 2);
+      assumeFormula(true, *Operands[0], Env);
+      assumeFormula(true, *Operands[1], Env);
+    }
+    break;
+  }
+  case Formula::Or: {
+    if (AtomVal == false) {
+      // Interpret the negated "or" as "and" of negated operands.
+      ArrayRef<const Formula *> Operands = F.operands();
+      assert(Operands.size() == 2);
+      assumeFormula(false, *Operands[0], Env);
+      assumeFormula(false, *Operands[1], Env);
+    }
+    break;
+  }
+  case Formula::Equal: {
+    ArrayRef<const Formula *> Operands = F.operands();
+    assert(Operands.size() == 2);
+    auto &LHS = *Operands[0];
+    auto &RHS = *Operands[1];
+    if (auto V = getLiteralValue(LHS, Env)) {
+      assumeFormula(AtomVal == *V, RHS, Env);
+    } else if (auto V = getLiteralValue(RHS, Env)) {
+      assumeFormula(AtomVal == *V, LHS, Env);
+    }
+    break;
+  }
+  default:
+    break;
+  }
+}
+
+BoolValue &join(BoolValue &Val1, const Environment &Env1, BoolValue &Val2,
+                const Environment &Env2, Environment &JoinedEnv) {
+  if (auto V1 = getLiteralValue(Val1.formula(), Env1);
+      V1.has_value() && V1 == getLiteralValue(Val2.formula(), Env2))
+    return JoinedEnv.getBoolLiteralValue(*V1);
+  return JoinedEnv.makeAtomicBoolValue();
+}
+
+void assume(Environment &Env, const Formula &F) {
+  assumeFormula(/*AtomVal*/ true, F, Env);
+}
+
+bool allows(const Environment &Env, const Formula &F) {
+  auto V = getLiteralValue(F, Env);
+  // We are conservative in the negative direction: if we can't determine the
+  // value, assume it is allowed.
+  return V.value_or(true);
+}
+
+bool proves(const Environment &Env, const Formula &F) {
+  auto V = getLiteralValue(F, Env);
+  return V.value_or(false);
+}
+} // namespace simple_bool_model
+
+namespace sat_bool_model {
+BoolValue &join(BoolValue &Val1, const Environment &Env1, BoolValue &Val2,
+                const Environment &Env2, Environment &JoinedEnv) {
+  auto &A = JoinedEnv.arena();
+  auto &JoinedVal = JoinedEnv.makeAtomicBoolValue();
+  auto &JoinedFormula = JoinedVal.formula();
+  JoinedEnv.assume(
+      A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
+                         A.makeEquals(JoinedFormula, Val1.formula())),
+               A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()),
+                         A.makeEquals(JoinedFormula, Val2.formula()))));
+  return JoinedVal;
+}
+
+void assume(Environment &Env, const Formula &F) {
+  Env.getDataflowAnalysisContext().addFlowConditionConstraint(
+      Env.getFlowConditionToken(), F);
+}
+
+bool allows(const Environment &Env, const Formula &F) {
+  return Env.getDataflowAnalysisContext().flowConditionAllows(
+      Env.getFlowConditionToken(), F);
+}
+
+bool proves(const Environment &Env, const Formula &F) {
+  return Env.getDataflowAnalysisContext().flowConditionImplies(
+      Env.getFlowConditionToken(), F);
+}
+} // namespace sat_bool_model
+
+namespace bool_model = simple_bool_model;
+
 // FIXME: convert these to parameters of the analysis or environment. Current
 // settings have been experimentaly validated, but only for a particular
 // analysis.
@@ -129,16 +292,9 @@ static Value *joinDistinctValues(QualType Type, Value &Val1,
     // if (o.has_value())
     //   x = o.value();
     // ```
-    auto &Expr1 = cast<BoolValue>(Val1).formula();
-    auto &Expr2 = cast<BoolValue>(Val2).formula();
-    auto &A = JoinedEnv.arena();
-    auto &JoinedVal = A.makeAtomRef(A.makeAtom());
-    JoinedEnv.assume(
-        A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
-                           A.makeEquals(JoinedVal, Expr1)),
-                 A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()),
-                           A.makeEquals(JoinedVal, Expr2))));
-    return &A.makeBoolValue(JoinedVal);
+    auto &B1 = cast<BoolValue>(Val1);
+    auto &B2 = cast<BoolValue>(Val2);
+    return &bool_model::join(B1, Env1, B2, Env2, JoinedEnv);
   }
 
   Value *JoinedVal = nullptr;
@@ -706,6 +862,12 @@ Environment Environment::join(const Environment &EnvA, const Environment &EnvB,
     JoinedEnv.ExprToLoc = joinExprMaps(EnvA.ExprToLoc, EnvB.ExprToLoc);
   }
 
+  for (auto &Entry : EnvA.AtomToVal) {
+    auto It = EnvB.AtomToVal.find(Entry.first);
+    if (It != EnvB.AtomToVal.end() && Entry.second == It->second)
+      JoinedEnv.AtomToVal.insert({Entry.first, Entry.second});
+  }
+
   return JoinedEnv;
 }
 
@@ -1056,16 +1218,14 @@ StorageLocation &Environment::createObjectInternal(const ValueDecl *D,
   return Loc;
 }
 
-void Environment::assume(const Formula &F) {
-  DACtx->addFlowConditionConstraint(FlowConditionToken, F);
-}
+void Environment::assume(const Formula &F) { bool_model::assume(*this, F); }
 
 bool Environment::proves(const Formula &F) const {
-  return DACtx->flowConditionImplies(FlowConditionToken, F);
+  return bool_model::proves(*this, F);
 }
 
 bool Environment::allows(const Formula &F) const {
-  return DACtx->flowConditionAllows(FlowConditionToken, F);
+  return bool_model::allows(*this, F);
 }
 
 void Environment::dump(raw_ostream &OS) const {
@@ -1120,6 +1280,15 @@ void Environment::dump() const {
   dump(llvm::dbgs());
 }
 
+std::optional<bool> Environment::getAtomValue(Atom A) const {
+  auto It = AtomToVal.find(A);
+  if (It == AtomToVal.end())
+    return std::nullopt;
+  return It->second;
+}
+
+void Environment::setAtomValue(Atom A, bool b) { AtomToVal[A] = b; }
+
 RecordStorageLocation *getImplicitObjectLocation(const CXXMemberCallExpr &MCE,
                                                  const Environment &Env) {
   Expr *ImplicitObject = MCE.getImplicitObjectArgument();

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

@@ -653,8 +653,7 @@ const Formula &evaluateEquality(Arena &A, const Formula &EqVal,
   //    If neither is set, then they are equal.
   // We rewrite b) as !EqVal => (LHS v RHS), for a more compact formula.
   return A.makeAnd(
-      A.makeImplies(EqVal, A.makeOr(A.makeAnd(LHS, RHS),
-                                    A.makeAnd(A.makeNot(LHS), A.makeNot(RHS)))),
+      A.makeImplies(EqVal, A.makeEquals(LHS, RHS)),
       A.makeImplies(A.makeNot(EqVal), A.makeOr(LHS, RHS)));
 }