[clang][dataflow] Add implementation of a simple boolean model

The new model still uses atomic variables in boolean formulas, but it limits the
environment to accumulating truth values for atomic variables, rather than
the arbitrary formula allowed by the flow condition.

Author: ymand

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,7 +48,7 @@ class StmtToEnvMap {
   const TypeErasedDataflowAnalysisState &CurState;
 };
 
-namespace bool_model {
+namespace sat_bool_model {
 
 BoolValue &freshBoolValue(Environment &Env);
 
@@ -70,7 +70,35 @@ BoolValue &notOp(BoolValue &Sub, Environment &Env);
 // CondVal -- the abstract value representing the condition.
 void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env);
 
-} // namespace bool_model
+} // namespace sat_bool_model
+
+namespace simple_bool_model {
+
+std::optional<bool> getLiteralValue(const Formula &F, const Environment &Env);
+
+BoolValue &freshBoolValue(Environment &Env);
+
+BoolValue &rValueFromLValue(BoolValue &V, Environment &Env);
+
+BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
+
+BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
+
+BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
+
+BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env);
+
+BoolValue &notOp(BoolValue &Sub, Environment &Env);
+
+// Models the transition along a branch edge in the CFG.
+// BranchVal -- the concrete, dynamic branch value -- true for `then` and false
+// for `else`.
+// CondVal -- the abstract value representing the condition.
+void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env);
+
+} // namespace simple_bool_model
+
+namespace bool_model = simple_bool_model;
 
 /// Evaluates `S` and updates `Env` accordingly.
 ///

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

@@ -17,6 +17,7 @@
 #include "clang/AST/DeclCXX.h"
 #include "clang/AST/Type.h"
 #include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/Transfer.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/DenseSet.h"
@@ -706,6 +707,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;
 }
 
@@ -1059,9 +1066,16 @@ void Environment::assume(const Formula &F) {
   DACtx->addFlowConditionConstraint(FlowConditionToken, F);
 }
 
+#if 0
 bool Environment::proves(const Formula &F) const {
   return DACtx->flowConditionImplies(FlowConditionToken, F);
 }
+#else
+bool Environment::proves(const Formula &F) const {
+  auto V = simple_bool_model::getLiteralValue(F, *this);
+  return V.has_value() && *V;
+}
+#endif
 
 bool Environment::allows(const Formula &F) const {
   return DACtx->flowConditionAllows(FlowConditionToken, F);
@@ -1119,6 +1133,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

@@ -569,8 +569,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)));
 }
 

clang/lib/Analysis/FlowSensitive/Transfer.cpp

@@ -81,7 +81,7 @@ static void propagateValueOrStorageLocation(const Expr &From, const Expr &To,
     propagateValue(From, To, Env);
 }
 
-namespace bool_model {
+namespace sat_bool_model {
 
 BoolValue &freshBoolValue(Environment &Env) {
   return Env.makeAtomicBoolValue();
@@ -110,15 +110,145 @@ BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
 BoolValue &notOp(BoolValue &Sub, Environment &Env) { return Env.makeNot(Sub); }
 
 void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env) {
-  if (BranchVal)
-    Env.assume(CondVal.formula());
-  else
-    // The condition must be inverted for the successor that encompasses the
-    // "else" branch, if such exists.
-    Env.assume(Env.makeNot(CondVal).formula());
+  // 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: {
+    ArrayRef<const Formula *> Operands = F.operands();
+    assert(Operands.size() == 1);
+    if (std::optional<bool> Maybe = getLiteralValue(*Operands[0], Env))
+      return !*Maybe;
+    return std::nullopt;
+  }
+  default:
+    return std::nullopt;
+  }
+}
+
+BoolValue &freshBoolValue(Environment &Env) {
+  return Env.makeAtomicBoolValue();
+}
+
+BoolValue &rValueFromLValue(BoolValue &V, Environment &Env) {
+  return unpackValue(V, Env);
+}
+
+BoolValue &logicalOrOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+  // FIXME: check if these optimizations are already built in to the formula
+  // generation.
+  if (auto V = getLiteralValue(LHS.formula(), Env))
+    return *V ? Env.getBoolLiteralValue(true) : RHS;
+  if (auto V = getLiteralValue(RHS.formula(), Env))
+    return *V ? Env.getBoolLiteralValue(true) : LHS;
+  return Env.makeOr(LHS, RHS);
+}
+
+BoolValue &logicalAndOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+  if (auto V = getLiteralValue(LHS.formula(), Env))
+    return *V ? RHS : Env.getBoolLiteralValue(false);
+  if (auto V = getLiteralValue(RHS.formula(), Env))
+    return *V ? LHS : Env.getBoolLiteralValue(false);
+  return Env.makeAnd(LHS, RHS);
+}
+
+BoolValue &eqOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+  if (&LHS.formula() == &RHS.formula())
+    return Env.getBoolLiteralValue(true);
+  if (auto V = getLiteralValue(LHS.formula(), Env))
+    return *V ? RHS : Env.makeNot(RHS);
+  if (auto V = getLiteralValue(RHS.formula(), Env))
+    return *V ? LHS : Env.makeNot(LHS);
+  return Env.makeIff(LHS, RHS);
+}
+
+// FIXME: i think this could be implemented in terms of eqOp.
+BoolValue &neOp(BoolValue &LHS, BoolValue &RHS, Environment &Env) {
+  if (&LHS.formula() == &RHS.formula())
+    return Env.getBoolLiteralValue(false);
+  if (auto V = getLiteralValue(LHS.formula(), Env))
+    return *V ? Env.makeNot(RHS) : RHS;
+  if (auto V = getLiteralValue(RHS.formula(), Env))
+    return *V ? Env.makeNot(LHS) : LHS;
+  return Env.makeNot(Env.makeIff(LHS, RHS));
+}
+
+BoolValue &notOp(BoolValue &Sub, Environment &Env) { return Env.makeNot(Sub); }
+
+// 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) {
+  // TODO: handle literals directly rather than calling getLiteralValue.
+  std::optional<bool> Lit = getLiteralValue(F, Env);
+  if (Lit.has_value())
+    // FIXME: Nothing to do. Could verify no contradiction, but not sure what
+    // we'd do with that here. Need to poison the Env.
+    return;
+
+  switch (F.kind()) {
+  case Formula::AtomRef:
+    // FIXME: check for contradictions
+    Env.setAtomValue(F.getAtom(), AtomVal);
+    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;
+  }
+}
+
+void transferBranch(bool BranchVal, BoolValue &CondVal, Environment &Env) {
+  assumeFormula(BranchVal, CondVal.formula(), Env);
 }
 
-} // namespace bool_model
+} // namespace simple_bool_model
 
 // Unpacks the value (if any) associated with `E` and updates `E` to the new
 // value, if any unpacking occured. Also, does the lvalue-to-rvalue conversion,

clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp

@@ -290,9 +290,7 @@ computeBlockInputState(const CFGBlock &Block, AnalysisContext &AC) {
           // assert ourselves instead of asserting via `cast()` so that we get
           // a more meaningful line number if the assertion fails.
           assert(CondVal != nullptr);
-          BoolValue *AssertedVal =
-              BranchVal ? CondVal : &Copy.Env.makeNot(*CondVal);
-          Copy.Env.assume(AssertedVal->formula());
+          bool_model::transferBranch(BranchVal, *CondVal, Copy.Env);
         }
         AC.Analysis.transferBranchTypeErased(BranchVal, Cond, Copy.Lattice,
                                              Copy.Env);
@@ -463,7 +461,8 @@ transferCFGBlock(const CFGBlock &Block, AnalysisContext &AC,
     // we have *some* value for the condition expression. This ensures that
     // when we extend the flow condition, it actually changes.
     if (State.Env.getValue(*TerminatorCond) == nullptr)
-      State.Env.setValue(*TerminatorCond, State.Env.makeAtomicBoolValue());
+      State.Env.setValue(*TerminatorCond,
+                         bool_model::freshBoolValue(State.Env));
     AC.Log.recordState(State);
   }
 

clang/unittests/Analysis/FlowSensitive/TransferTest.cpp

@@ -6,6 +6,7 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include "clang/Analysis/FlowSensitive/Transfer.h"
 #include "TestingSupport.h"
 #include "clang/AST/ASTContext.h"
 #include "clang/AST/Decl.h"
@@ -35,6 +36,7 @@ using ::testing::Eq;
 using ::testing::IsNull;
 using ::testing::Ne;
 using ::testing::NotNull;
+using ::testing::Optional;
 using ::testing::UnorderedElementsAre;
 
 void runDataflow(
@@ -4331,12 +4333,12 @@ TEST(TransferTest, LoopWithAssignmentConverges) {
     bool foo();
 
     void target() {
-       do {
+      do {
         bool Bar = foo();
         if (Bar) break;
         (void)Bar;
         /*[[p]]*/
-      } while (true);
+     } while (true);
     }
   )";
   // The key property that we are verifying is implicit in `runDataflow` --
@@ -4353,6 +4355,8 @@ TEST(TransferTest, LoopWithAssignmentConverges) {
         ASSERT_THAT(BarDecl, NotNull());
 
         auto &BarVal = getFormula(*BarDecl, Env);
+        ASSERT_EQ(BarVal.kind(), Formula::AtomRef);
+        ASSERT_THAT(Env.getAtomValue(BarVal.getAtom()), Optional(false));
         EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal)));
       });
 }

clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

@@ -286,6 +286,10 @@ TEST_F(DiscardExprStateTest, BooleanOperator) {
   const auto &AndOpState = blockStateForStmt(BlockStates, AndOp);
   EXPECT_EQ(AndOpState.Env.getValue(*AndOp.getLHS()), LHSValue);
   EXPECT_EQ(AndOpState.Env.getValue(*AndOp.getRHS()), RHSValue);
+  // FIXME: this test is too strict. We want to check equivalence not equality;
+  // as is, its a change detector test. Notice that we only evaluate `b1 && b2`
+  // in a context where we know that `b1 is true, so there's a potential
+  // optimization to store only `RHSValue` as the operation's value.
   EXPECT_EQ(AndOpState.Env.getValue(AndOp),
             &AndOpState.Env.makeAnd(*LHSValue, *RHSValue));