================
@@ -40,6 +44,481 @@
namespace clang {
namespace dataflow {
+namespace {
+
+class SimpleBoolModel : public Environment::BoolModel {
+public:
+ SimpleBoolModel() : BoolModel(BoolModelKind::Simple) {}
+
+ static bool classof(const BoolModel *M) {
+ return M->getKind() == BoolModelKind::Simple;
+ }
+
+ std::unique_ptr<BoolModel> clone() const override {
+ return std::make_unique<SimpleBoolModel>(*this);
+ }
+
+ void onFork() override {}
+
+ void assume(const Formula &F) override {
+ if (HasContradiction)
+ return;
+ unsigned PrevSize = AtomToVal.size();
+ // Given that F is assumed true, see if we can force the assignment
+ // of any atoms and ultimately reduce F to a literal (if possible).
+ // For example, if F is `A && B`, we will force `A` and `B` to be true.
+ // If F is `A || B`, we will only force an assignment if one of A or B is
+ // already known to be false.
+ assumeFormula(/*AssumedVal=*/true, F);
+ if (HasContradiction)
+ return;
+
+ // Retain `F` in `AssumedFormulas` only if it has not yet been reduced to a
+ // known truth value in `AtomToVal` (e.g., `A || B` or `A == B` where
+ // neither side is known yet).
+ //
+ // - Why save unresolved formulas: a compound formula (like
+ // `EqVal => (LHS == RHS)` from a comparison expression) is often assumed
+ // while its atoms are still unknown; when we later follow a branch that
+ // fixes one of those atoms, the propagation loop below can reduce the
+ // saved formula to concrete `AtomToVal` entries.
+ //
+ // - Skipping formulas that already evaluate to `true` avoids bloating
+ // `AssumedFormulas` with single-atom and conjunctive assumptions that
are
+ // already fully represented by `AtomToVal` (though it also drops
+ // disjunctive formulas that were reduced using a branch-local atom, such
+ // as on the RHS of a short-circuit `&&` or `||`).
+ // TODO(jvoung): We may want to retain some disjunctive formulas, but
+ // would need to profile and see how much it helps vs how much it costs.
+ if (std::optional<bool> Val = getLiteralValue(F)) {
+ if (!*Val) {
+ HasContradiction = true;
+ return;
+ }
+ } else {
+ AssumedFormulas.insert(&F);
+ }
+
+ if (AtomToVal.size() == PrevSize)
+ return;
+
+ // Propagate newly learned atom values through any pending assumed
formulas.
+ // Note: Do not remove formulas from `AssumedFormulas` when they evaluate
to
+ // `true` in a branch, because the atoms that satisfied them may be
+ // branch-local and discarded at a subsequent `join`, where the formula
+ // itself still holds on both branches.
+ bool Changed = true;
+ while (Changed && !HasContradiction) {
+ Changed = false;
+ for (const Formula *Pending : AssumedFormulas) {
+ unsigned Before = AtomToVal.size();
+ assumeFormula(/*AssumedVal=*/true, *Pending);
+ if (HasContradiction)
+ return;
+ if (getLiteralValue(*Pending) == false) {
+ HasContradiction = true;
+ return;
+ }
+ if (AtomToVal.size() > Before)
+ Changed = true;
+ }
+ }
+ }
+
+ bool proves(const Formula &F) const override {
+ if (HasContradiction)
+ return true;
+ auto V = getLiteralValue(F);
+ return V.value_or(false);
+ }
+
+ bool allows(const Formula &F) const override {
+ if (HasContradiction)
+ return false;
+ auto V = getLiteralValue(F);
+ // We are conservative in the negative direction: if we can't determine the
+ // value, assume it is allowed.
+ return V.value_or(true);
+ }
+
+ BoolValue &joinBoolValues(BoolValue &Val1, const BoolModel &Model1,
+ BoolValue &Val2, const BoolModel &Model2,
+ Environment &JoinedEnv) override {
+ const auto &S1 = cast<SimpleBoolModel>(Model1);
+ const auto &S2 = cast<SimpleBoolModel>(Model2);
+ if (S1.HasContradiction && !S2.HasContradiction)
+ return Val2;
+ if (S2.HasContradiction && !S1.HasContradiction)
+ return Val1;
+ if (auto V1 = S1.getLiteralValue(Val1.formula());
+ V1.has_value() && V1 == S2.getLiteralValue(Val2.formula()))
+ return JoinedEnv.getBoolLiteralValue(*V1);
+ return JoinedEnv.makeAtomicBoolValue();
+ }
+
+ void join(const BoolModel &ModelA, const BoolModel &ModelB) override {
+ const auto &SA = cast<SimpleBoolModel>(ModelA);
+ const auto &SB = cast<SimpleBoolModel>(ModelB);
+ AtomToVal.clear();
+ AssumedFormulas.clear();
+ HasContradiction = false;
+
+ if (SA.HasContradiction && SB.HasContradiction) {
+ HasContradiction = true;
+ } else if (SA.HasContradiction) {
+ AtomToVal = SB.AtomToVal;
+ AssumedFormulas = SB.AssumedFormulas;
+ } else if (SB.HasContradiction) {
+ AtomToVal = SA.AtomToVal;
+ AssumedFormulas = SA.AssumedFormulas;
+ } else {
+ // Intersect the AtomToVal maps.
+ for (const auto &Entry : SA.AtomToVal) {
+ auto It = SB.AtomToVal.find(Entry.first);
+ if (It != SB.AtomToVal.end() && Entry.second == It->second)
+ AtomToVal.insert({Entry.first, Entry.second});
+ }
+
+ // Keep assumed formulas that hold on both branches: either because both
+ // environments still carry `F` as an unresolved formula, or because one
+ // branch carries `F` and the other branch's `AtomToVal` assignments
+ // already prove `F`. Any branch-local formulas not proved by the other
+ // branch are dropped here, which shrinks `AssumedFormulas` at joins.
+ for (const Formula *F : SA.AssumedFormulas) {
+ if (SB.AssumedFormulas.contains(F) || SB.proves(*F))
+ AssumedFormulas.insert(F);
+ }
+ for (const Formula *F : SB.AssumedFormulas) {
+ if (SA.proves(*F))
+ AssumedFormulas.insert(F);
+ }
+ }
+ }
+
+ LatticeEffect widen(const BoolModel &PrevModel) override {
+ const auto &PrevSimple = cast<SimpleBoolModel>(PrevModel);
+ SimpleBoolModel Widened;
+ Widened.join(*this, PrevSimple);
+ LatticeEffect Effect = Widened.isEquivalentTo(PrevSimple)
+ ? LatticeEffect::Unchanged
+ : LatticeEffect::Changed;
+ *this = std::move(Widened);
+ return Effect;
+ }
+
+ bool isEquivalentTo(const BoolModel &Other) const override {
+ const auto &OtherSimple = cast<SimpleBoolModel>(Other);
+ if (HasContradiction != OtherSimple.HasContradiction)
+ return false;
+ if (HasContradiction)
+ return true;
+ if (AtomToVal.size() != OtherSimple.AtomToVal.size() ||
+ AssumedFormulas != OtherSimple.AssumedFormulas)
+ return false;
+ return llvm::all_of(AtomToVal, [&](const auto &Entry) {
+ return OtherSimple.getAtomValue(Entry.first) == Entry.second;
+ });
+ }
+
+ Atom getFlowConditionToken() const override {
+ llvm_unreachable(
+ "getFlowConditionToken() is only supported in SatBoolModel");
+ }
+
+ void dump(raw_ostream &OS) const override {
+ OS << "SimpleBoolModel:\n";
+ OS << " HasContradiction: " << HasContradiction << "\n";
+ OS << " AtomToVal:\n";
+ for (auto [A, V] : AtomToVal)
+ OS << " " << A << " = " << (V ? "true" : "false") << "\n";
+ OS << " AssumedFormulas:\n";
+ for (const Formula *F : AssumedFormulas)
+ OS << " " << *F << "\n";
+ }
+
+private:
+ std::optional<bool> getAtomValue(Atom A) const {
+ auto It = AtomToVal.find(A);
+ if (It == AtomToVal.end())
+ return std::nullopt;
+ return It->second;
+ }
+
+ void setAtomValue(Atom A, bool B) { AtomToVal[A] = B; }
+
+ std::optional<bool> getLiteralValue(const Formula &F) const {
+ switch (F.kind()) {
+ case Formula::AtomRef:
+ return 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]))
+ 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))
+ return !*Left ? Left : getLiteralValue(RHS);
+ if (std::optional<bool> Right = getLiteralValue(RHS); 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))
+ return *Left ? Left : getLiteralValue(RHS);
+ if (std::optional<bool> Right = getLiteralValue(RHS); Right == true)
+ return Right;
+ return std::nullopt;
+ }
+ case Formula::Implies: {
+ 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))
+ return !*Left ? true : getLiteralValue(RHS);
+ if (std::optional<bool> Right = getLiteralValue(RHS); Right == true)
+ return true;
+ 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;
+ if ((LHS.kind() == Formula::Not && LHS.operands()[0] == &RHS) ||
+ (RHS.kind() == Formula::Not && RHS.operands()[0] == &LHS))
+ return false;
+ auto V_L = getLiteralValue(LHS);
+ if (!V_L.has_value())
+ return std::nullopt;
+ auto V_R = getLiteralValue(RHS);
+ if (!V_R.has_value())
+ return std::nullopt;
+ return *V_L == *V_R;
+ }
+ }
+ }
+
+ // Updates atom assignments under the assumption that subformula `F`
+ // evaluates to `AssumedVal` (i.e., `F == AssumedVal`).
+ //
+ // Top-level `assume(F)` starts with `AssumedVal = true`, and recursive
+ // calls flip `AssumedVal` when traversing negations (`Formula::Not`) or
+ // comparisons (`Formula::Equal`) against known boolean values.
+ //
+ // For example:
+ // - for `assume(!A)`, then `A` must be `false`
+ // - for `assume(A && B)`, then both `A` and `B` must be `true`.
+ void assumeFormula(bool AssumedVal, const Formula &F) {
+ if (HasContradiction)
+ return;
+ switch (F.kind()) {
+ case Formula::AtomRef: {
+ // Base case: `F` is a single atom, so assuming `F == AssumedVal`
directly
+ // binds this atom to `AssumedVal`, or marks the environment as having a
+ // contradiction if the atom was already bound to the opposite value.
+ Atom A = F.getAtom();
+ if (std::optional<bool> Existing = getAtomValue(A)) {
+ if (*Existing != AssumedVal)
+ HasContradiction = true;
+ break;
+ }
+ setAtomValue(A, AssumedVal);
----------------
kazutakahirata wrote:
Could we avoid duplicate hash lookups? If you are OK with `try_emplace` here,
you can remove `setAtomValue` above.
```suggestion
auto [It, Inserted] = AtomToVal.try_emplace(F.getAtom(), AssumedVal);
if (!Inserted && It->second != AssumedVal)
HasContradiction = true;
break;
```
https://github.com/llvm/llvm-project/pull/231061
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
