[clang] [clang][dataflow] Factor out built-in boolean model into an explicit module. (PR #82950)

[via cfe-commits]

================
@@ -50,29 +50,206 @@ const Environment *StmtToEnvMap::getEnvironment(const Stmt &S) const {
   return &State->Env;
 }
 
-static BoolValue &evaluateBooleanEquality(const Expr &LHS, const Expr &RHS,
-                                          Environment &Env) {
-  Value *LHSValue = Env.getValue(LHS);
-  Value *RHSValue = Env.getValue(RHS);
+static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
+  if (auto *Top = llvm::dyn_cast<TopBoolValue>(&V)) {
+    auto &A = Env.getDataflowAnalysisContext().arena();
+    return A.makeBoolValue(A.makeAtomRef(Top->getAtom()));
+  }
+  return V;
+}
 
-  if (LHSValue == RHSValue)
-    return Env.getBoolLiteralValue(true);
+static void propagateValue(const Expr &From, const Expr &To, Environment &Env) {
+  if (auto *Val = Env.getValue(From))
+    Env.setValue(To, *Val);
+}
 
-  if (auto *LHSBool = dyn_cast_or_null<BoolValue>(LHSValue))
-    if (auto *RHSBool = dyn_cast_or_null<BoolValue>(RHSValue))
-      return Env.makeIff(*LHSBool, *RHSBool);
+static void propagateStorageLocation(const Expr &From, const Expr &To,
+                                     Environment &Env) {
+  if (auto *Loc = Env.getStorageLocation(From))
+    Env.setStorageLocation(To, *Loc);
+}
+
+// Propagates the value or storage location of `From` to `To` in cases where
+// `From` may be either a glvalue or a prvalue. `To` must be a glvalue iff
+// `From` is a glvalue.
+static void propagateValueOrStorageLocation(const Expr &From, const Expr &To,
+                                            Environment &Env) {
+  assert(From.isGLValue() == To.isGLValue());
+  if (From.isGLValue())
+    propagateStorageLocation(From, To, Env);
+  else
+    propagateValue(From, To, Env);
+}
 
+namespace sat_bool_model {
+
+BoolValue &freshBoolValue(Environment &Env) {
   return Env.makeAtomicBoolValue();
 }
 
-static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
-  if (auto *Top = llvm::dyn_cast<TopBoolValue>(&V)) {
-    auto &A = Env.getDataflowAnalysisContext().arena();
-    return A.makeBoolValue(A.makeAtomRef(Top->getAtom()));
+BoolValue &rValueFromLValue(BoolValue &V, Environment &Env) {
+  return unpackValue(V, Env);
+}
+
+BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+  return Env.makeOr(LHS, RHS);
+}
+
+BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+  return Env.makeAnd(LHS, RHS);
+}
+
+BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+  return Env.makeIff(LHS, RHS);
+}
+
+BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+  return Env.makeNot(Env.makeIff(LHS, RHS));
+}
+
+BoolValue &notOp(BoolValue &Sub, Environment &Env) { return Env.makeNot(Sub); }
+
+void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env) {
+  // The condition must be inverted for the successor that encompasses the
+  // "else" branch, if such exists.
+  BoolValue &AssertedVal = BranchVal ? CondVal : Env.makeNot(CondVal);
+  Env.assume(AssertedVal.formula());
+}
+
+} // namespace sat_bool_model
+
+namespace simple_bool_model {
+
+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: {
----------------
martinboehme wrote:

Why do we need this case? Is it not covered by `neOp()` above? (I.e. are there ever any cases where we actually have `Formula::Not` formulas?)

If we do need this, don't we also need corresponding cases for `Formula::And` and `Formula::Or`?

https://github.com/llvm/llvm-project/pull/82950