================
@@ -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) {
----------------
Xazax-hun wrote:
Can we ever reach this with `HasContradiction == true`? We seem to be returning
in the body very eagerly when that is the case.
https://github.com/llvm/llvm-project/pull/231061
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
