MimIR
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
add_mem.cpp
Go to the documentation of this file.
2
3#include <mim/util/util.h>
4
5#include "mim/plug/mem/mem.h"
6
7// TODO make parametric in address space
8
9namespace mim::plug::mem::phase {
10
12 // Collect the lams whose ABI is pinned: everything (transitively) reachable from an axm-app argument
13 // (combiners, affine index mappings, initial accumulators of `%matrix.map_reduce_aff`, …).
14 auto queue = unique_queue<DefSet>();
15 auto pinned = unique_queue<DefSet>();
16 for (auto mut : old_world().externals().muts())
17 queue.push(mut);
18
19 while (!queue.empty()) {
20 auto def = queue.pop();
21
22 if (auto app = def->isa<App>(); app && app->axm())
23 for (auto arg : app->arg()->projs())
24 if (auto lam = arg->isa_mut<Lam>()) pinned.push(lam);
25
26 for (auto d : def->deps())
27 queue.push(d);
28 }
29
30 while (!pinned.empty()) {
31 auto def = pinned.pop();
32 if (auto lam = def->isa_mut<Lam>()) preserved_.emplace(lam);
33 for (auto d : def->deps())
34 pinned.push(d);
35 }
36
38}
39
40const Def* AddMem::rewrite(const Def* old_def) {
41 auto new_def = Rewriter::rewrite(old_def);
42 // Rewrite every memory operand to the current memory - after threading the operand's producers, which
43 // advances curr_mem_ along the way. Placeholders (`⊥`/`⊤ : %mem.M 0`) are thereby spliced into the chain.
44 if (curr_mem_ && !preserving_ && !is_bootstrapping() && !old_def->isa_mut() && isa_mem(old_def)) return curr_mem_;
45 return new_def;
46}
47
48const Def* AddMem::rewrite_imm_Pi(const Pi* pi) {
49 auto new_pi = Rewriter::rewrite_imm_Pi(pi)->as<Pi>();
50 if (is_bootstrapping() || preserving_) return new_pi;
51
52 // Only continuations are mem-extended; a pi that already threads memory is left alone.
53 if (Pi::isa_cn(pi) && !has_leading_mem(pi)) {
54 auto& w = new_world();
55 auto mem = w.call<mem::M>(0);
56 auto dom = new_pi->dom();
57
58 // A dependent domain refers to its own Var.
59 // So prepending a leading mem shifts every component's index by one.
60 // Rebuild the domain as a fresh mutable Sigma and remap the old domain-Var to the shifted components of the new
61 // one. Otherwise the dependent references dangle (see issue #177).
62 if (auto [sigma, old_var] = dom->isa_binder<Sigma>(); sigma) {
63 auto n = sigma->num_ops();
64 auto new_sigma = w.mut_sigma(sigma->type(), n + 1);
65 new_sigma->set(0, mem);
66 // Component `i` may only refer to earlier components, whose (index-shifted) new Vars are already
67 // set - so build the substitution per component; padding slots `≥ i` are never extracted.
68 for (size_t i = 0; i != n; ++i) {
69 auto shift = w.tuple(DefVec(n, [&](size_t j) { return j < i ? new_sigma->var(n + 1, j + 1) : mem; }));
70 auto rw = VarRewriter(old_var, shift);
71 new_sigma->set(i + 1, rw.rewrite(sigma->op(i)));
72 }
73 return w.cn(new_sigma);
74 }
75
76 auto new_dom = DefVec();
77 new_dom.emplace_back(mem);
78 for (size_t i = 0, e = new_pi->num_doms(); i != e; ++i)
79 new_dom.emplace_back(new_pi->dom(i));
80 return w.cn(new_dom);
81 }
82 return new_pi;
83}
84
86 if (is_bootstrapping() || preserving_) return Rewriter::rewrite_mut_Lam(old_lam);
87
88 // Pinned ABI (an axm-app argument and everything below it): rewrite verbatim - no memory threaded or added.
89 if (preserved_.contains(old_lam)) {
90 auto _ = Restore(preserving_, true);
91 return Rewriter::rewrite_mut_Lam(old_lam);
92 }
93
94 auto new_lam = new_world().mut_lam(rewrite(old_lam->type())->as<Pi>())->set(old_lam->dbg());
95 map(old_lam, new_lam);
96
97 // Map the parameters, accounting for a possibly inserted leading mem var.
98 if (auto n = old_lam->num_vars(); n != 0) {
99 auto offset = new_lam->num_doms() - old_lam->num_doms(); // 1 iff we prepended a mem var
100 for (size_t i = 0; i != n; ++i)
101 map(old_lam->var(i), new_lam->var(i + offset)->set(old_lam->var(i)->dbg()));
102 // A use of the whole parameter tuple is reconstructed from the new (shifted) components.
103 if (n > 1)
104 map(old_lam->var(), new_world().tuple(DefVec(n, [&](size_t i) { return new_lam->var(i + offset); })));
105 }
106
107 if (!old_lam->is_set()) return new_lam;
108
109 // The body's current memory is this lam's (leading or grouped) mem parameter - or none for direct-style fns.
110 auto _ = Restore(curr_mem_, mem::mem_var(new_lam));
111 new_lam->set(rewrite(old_lam->filter()), rewrite(old_lam->body()));
112 return new_lam;
113}
114
115const Def* AddMem::rewrite_imm_App(const App* app) {
116 if (is_bootstrapping() || preserving_ || !curr_mem_) return Rewriter::rewrite_imm_App(app);
117
118 auto& w = new_world();
119 // Rewrite the argument before the callee (as the base Rewriter does). This threads the current memory
120 // through the argument's memory effects first; and because operands are rewritten before their users, a
121 // shared memory operation is anchored in the scope that consumes its result mem (its own scope) rather
122 // than one that merely reuses its non-mem result. curr_mem_ then holds the memory *after* the argument.
123 auto new_arg = rewrite(app->arg());
124 auto mem = curr_mem_;
125 auto new_callee = rewrite(app->callee());
126
127 auto old_pi = app->callee()->type()->isa<Pi>();
128 auto new_pi = new_callee->type()->isa<Pi>();
129 if (old_pi && new_pi && new_pi->num_doms() == old_pi->num_doms() + 1) {
130 // The callee gained a leading mem parameter: splice the current memory in front of the arguments.
131 auto n = old_pi->num_doms();
132 auto args = DefVec(n + 1);
133 args[0] = mem;
134 for (size_t i = 0; i != n; ++i)
135 args[i + 1] = new_arg->proj(n, i);
136 new_arg = w.tuple(args);
137 }
138
139 auto new_app = w.app(new_callee, new_arg);
140 advance_mem(new_app);
141 return new_app;
142}
143
145 if (is_bootstrapping() || preserving_ || !curr_mem_) return Rewriter::rewrite_imm_Tuple(tuple);
146
147 // The current memory must be threaded through the operands in the right order, because a memory operand
148 // (which resolves to the *current* memory) is positioned freely relative to the operands that establish
149 // the real ordering. Rewrite in three groups:
150 // 1. plain values first - e.g. the `buf` of a buffer op's `(⊥ : %mem.M 0, buf)` argument, whose memory
151 // effects must precede the memory operand;
152 // 2. memory operands next - now resolving to the up-to-date current memory;
153 // 3. continuation values last - their bodies run later, so a shared memory operation they capture must
154 // already have been anchored (threaded) in this scope by the memory operands above.
155 auto rank = [](const Def* op) { return isa_mem(op) ? 1 : (op->type() && Pi::isa_cn(op->type()) ? 2 : 0); };
156
157 auto& w = new_world();
158 auto n = tuple->num_ops();
159 auto new_ops = DefVec(n);
160 for (int r = 0; r != 3; ++r)
161 for (size_t i = 0; i != n; ++i)
162 if (rank(tuple->op(i)) == r) new_ops[i] = rewrite(tuple->op(i));
163 return w.tuple(rewrite(tuple->type()), new_ops);
164}
165
166void AddMem::advance_mem(const Def* def) {
167 if (auto m = mem_def(def)) curr_mem_ = m;
168}
169
170} // namespace mim::plug::mem::phase
const Axm * axm() const
Definition lam.h:291
const Def * callee() const
Definition lam.h:276
const Def * arg() const
Definition lam.h:285
Base class for all Defs.
Definition def.h:261
bool is_set() const
Yields true if empty or the last op is set.
Definition def.cpp:308
Def * set(size_t i, const Def *)
Successively set from left to right.
Definition def.cpp:276
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
Definition def.h:527
const Def * var(nat_t a, nat_t i) noexcept
Definition def.h:441
nat_t num_vars() noexcept
Definition def.h:441
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.cpp:491
Dbg dbg() const
Definition def.h:556
A function.
Definition lam.h:110
const Def * filter() const
Definition lam.h:122
Lam * set(Filter filter, const Def *body)
Definition lam.cpp:29
const Pi * type() const
Definition lam.h:130
const Def * body() const
Definition lam.h:123
const Vector< std::string > & args()
Command-line arguments passed to this Phase's plugin via -X <plugin>:<arg>.
Definition phase.cpp:23
A dependent function type.
Definition lam.h:14
static const Pi * isa_cn(const Def *d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
Definition lam.h:47
World & new_world()
Create new Defs into this.
Definition phase.h:368
bool is_bootstrapping() const
Returns whether we are currently bootstrapping (rewriting annexes).
Definition phase.h:356
void start() override
Actual entry.
Definition phase.cpp:128
World & old_world()
Get old Defs from here.
Definition phase.h:367
RAII guard that restores ref to its current value at the end of the scope.
Definition util.h:177
virtual const Def * map(const Def *old_def, const Def *new_def)
Definition rewrite.h:45
virtual const Def * rewrite(const Def *)
Definition rewrite.cpp:56
A dependent tuple type.
Definition tuple.h:22
Data constructor for a Sigma.
Definition tuple.h:70
Extends Rewriter for variable substitution.
Definition rewrite.h:107
Lam * mut_lam(const Pi *pi)
Definition world.h:388
const Def * rewrite_imm_Tuple(const Tuple *) override
Definition add_mem.cpp:144
const Def * rewrite_imm_Pi(const Pi *) override
Definition add_mem.cpp:48
const Def * rewrite(const Def *) override
Definition add_mem.cpp:40
const Def * rewrite_mut_Lam(Lam *) override
Definition add_mem.cpp:85
const Def * rewrite_imm_App(const App *) override
Definition add_mem.cpp:115
void start() override
Actual entry.
Definition add_mem.cpp:11
The mem Plugin
Definition mem.h:11
bool has_leading_mem(const Pi *pi)
Does pi already thread memory - a leading mem.M, either directly or grouped as the first component of...
Definition mem.h:33
const Def * mem_var(Lam *lam)
Returns the memory argument of a function if it has one.
Definition mem.h:55
const Def * mem_def(const Def *def)
Returns the (first) element of type mem.M a from the given tuple.
Definition mem.h:42
const App * isa_mem(const Def *def)
If def is a mem.M-typed value, yields its memory type mem.M a; otherwise nullptr.
Definition mem.h:26
The tuple Plugin
Vector< const Def * > DefVec
Definition def.h:79