================
@@ -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});
----------------
kazutakahirata wrote:
May I suggest structured bindings here?
```suggestion
for (auto [A, V] : SA.AtomToVal) {
auto It = SB.AtomToVal.find(A);
if (It != SB.AtomToVal.end() && V == It->second)
AtomToVal.insert({A, V});
```
https://github.com/llvm/llvm-project/pull/231061
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
