Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feature/infer3 #103

Closed
wants to merge 17 commits into from
Closed
19 changes: 14 additions & 5 deletions .github/workflows/doxygen.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,20 +16,29 @@ jobs:
with:
submodules: recursive

- name: Install newest g++, graphviz
- name: Install newest g++, graphviz, texlive
run: |
sudo add-apt-repository -y ppa:ubuntu-toolchain-r/test
sudo apt-get update
sudo apt-get install g++-11 graphviz
sudo apt-get install g++-11 graphviz texlive-latex-base texlive-fonts-recommended texlive-fonts-extra texlive-latex-extra

export CXX=g++-11

- name: Install Doxygen
run: |
wget https://www.doxygen.nl/files/doxygen-1.9.4.linux.bin.tar.gz
tar xf doxygen-1.9.4.linux.bin.tar.gz
wget https://www.doxygen.nl/files/doxygen-1.9.5.linux.bin.tar.gz
tar xf doxygen-1.9.5.linux.bin.tar.gz

- name: Install Ghostscript
run: |
mkdir -p ${HOME}/.local/bin
echo "${HOME}/.local/bin" >> $GITHUB_PATH
wget https://github.com/ArtifexSoftware/ghostpdl-downloads/releases/download/gs1000/ghostscript-10.0.0-linux-x86_64.tgz
tar xf ghostscript-10.0.0-linux-x86_64.tgz
mv ghostscript-10.0.0-linux-x86_64/gs-1000-linux-x86_64 ${HOME}/.local/bin/gs

- name: Configure
run: CXX=g++-11 cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=Debug -DTHORIN_BUILD_DOCS=ON -DDOXYGEN_EXECUTABLE=${{github.workspace}}/doxygen-1.9.4/bin/doxygen
run: CXX=g++-11 cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=Debug -DTHORIN_BUILD_DOCS=ON -DDOXYGEN_EXECUTABLE=${{github.workspace}}/doxygen-1.9.5/bin/doxygen

- name: Build
run: cmake --build ${{github.workspace}}/build -v --target docs
Expand Down
2 changes: 1 addition & 1 deletion dialects/affine/passes/lower_for.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ const Def* LowerFor::rewrite(const Def* def) {
auto if_else = w.nom_lam(if_else_cn, nullptr);
if_else->app(false, brk, acc);

auto cmp = core::op(core::icmp::ul, iter, end);
auto cmp = w.call(core::icmp::ul, {iter, end});
for_lam->branch(false, cmp, new_body, if_else, w.tuple());
}

Expand Down
8 changes: 4 additions & 4 deletions dialects/clos/pass/rw/clos2sjlj.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -87,9 +87,9 @@ Lam* Clos2SJLJ::get_throw(const Def* dom) {
auto [m0, env, var] = split(tlam->var());
auto [jbuf, rbuf, tag] = env->projs<3>();
auto [m1, r] = mem::op_alloc(var->type(), m0)->projs<2>();
auto m2 = mem::op_store(m1, r, var);
auto m2 = world().call<mem::store>({m1, r, var});
rbuf = core::op_bitcast(mem::type_ptr(mem::type_ptr(var->type())), rbuf);
auto m3 = mem::op_store(m2, rbuf, r);
auto m3 = world().call<mem::store>({m2, rbuf, r});
tlam->set(false, op_longjmp(m3, jbuf, tag));
ignore_.emplace(tlam);
}
Expand All @@ -105,9 +105,9 @@ Lam* Clos2SJLJ::get_lpad(Lam* lam, const Def* rb) {
auto pi = w.cn(w.sigma({mem::type_mem(w), env_type}));
lpad = w.nom_lam(pi, w.dbg("lpad"));
auto [m, env, __] = split(lpad->var());
auto [m1, arg_ptr] = mem::op_load(m, rb)->projs<2>();
auto [m1, arg_ptr] = world().call<mem::load>({m, rb})->projs<2>();
arg_ptr = core::op_bitcast(mem::type_ptr(dom), arg_ptr);
auto [m2, args] = mem::op_load(m1, arg_ptr)->projs<2>();
auto [m2, args] = world().call<mem::load>({m1, arg_ptr})->projs<2>();
auto full_args = (lam->num_doms() == 3) ? rebuild(m2, env, {args}) : rebuild(m2, env, args->ops());
lpad->app(false, lam, full_args);
ignore_.emplace(lpad);
Expand Down
4 changes: 2 additions & 2 deletions dialects/clos/phase/lower_typed_clos.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ Lam* LowerTypedClos::make_stub(Lam* lam, enum Mode mode, bool adjust_bb_type) {
const Def* env =
new_lam->var(Clos_Env_Param, (mode != No_Env) ? w.dbg("closure_env") : lam->var(Clos_Env_Param)->dbg());
if (mode == Box) {
auto env_mem = mem::op_load(lcm, env);
auto env_mem = world().call<mem::load>({lcm, env});
lcm = w.extract(env_mem, 0_u64, w.dbg("mem"));
env = w.extract(env_mem, 1_u64, w.dbg("closure_env"));
} else if (mode == Unbox) {
Expand Down Expand Up @@ -122,7 +122,7 @@ const Def* LowerTypedClos::rewrite(const Def* def) {
auto mem_ptr = (c.get() == clos::esc) ? mem::op_alloc(env->type(), lcm_) : mem::op_slot(env->type(), lcm_);
auto mem = w.extract(mem_ptr, 0_u64);
auto env_ptr = mem_ptr->proj(1_u64, w.dbg(fn->name() + "_env"));
lcm_ = mem::op_store(mem, env_ptr, env);
lcm_ = world().call<mem::store>({mem, env_ptr, env});
map(lvm_, lcm_);
env = env_ptr;
}
Expand Down
19 changes: 12 additions & 7 deletions dialects/core/be/ll/ll.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -497,13 +497,18 @@ std::string Emitter::emit_bb(BB& bb, const Def* def) {
unreachable();
} else if (def->isa<Bot>()) {
return "undef";
} else if (auto bit = match<core::bit2>(def)) {
auto [a, b] = bit->args<2>([this](auto def) { return emit(def); });
auto t = convert(bit->type());

auto neg = [&](std::string_view x) { return bb.assign(name + ".neg", "xor {} 0, {}", t, x); };

switch (bit.id()) {
} else if (auto bit1 = match<core::bit1>(def)) {
assert(bit1.id() == core::bit1::neg);
auto x = emit(bit1->arg());
auto t = convert(bit1->type());
return bb.assign(name, "xor {} -1, {}", t, x);
} else if (auto bit2 = match<core::bit2>(def)) {
auto [a, b] = bit2->args<2>([this](auto def) { return emit(def); });
auto t = convert(bit2->type());

auto neg = [&](std::string_view x) { return bb.assign(name + ".neg", "xor {} -1, {}", t, x); };

switch (bit2.id()) {
// clang-format off
case core::bit2::_and: return bb.assign(name, "and {} {}, {}", t, a, b);
case core::bit2:: _or: return bb.assign(name, "or {} {}, {}", t, a, b);
Expand Down
75 changes: 19 additions & 56 deletions dialects/core/core.h
Original file line number Diff line number Diff line change
Expand Up @@ -42,130 +42,98 @@ enum RMode : nat_t {
};
}

inline const Def* rinfer(const Def* def) { return force<Real>(def->type())->arg(); }
inline const Def* rinfer(Refer def) { return refer(force<Real>(refer(def->type()))->arg()); }

/// @name fn - these guys yield the final function to be invoked for the various operations
///@{
inline const Def* fn(bit2 o, const Def* mod, const Def* dbg = {}) {
World& w = mod->world();
return w.app(w.ax(o), mod, dbg);
}
inline const Def* fn(icmp o, const Def* mod, const Def* dbg = {}) {
World& w = mod->world();
return w.app(w.ax(o), mod, dbg);
}
inline const Def* fn(shr o, const Def* mod, const Def* dbg = {}) {
World& w = mod->world();
return w.app(w.ax(o), mod, dbg);
}
inline const Def* fn(wrap o, const Def* wmode, const Def* mod, const Def* dbg = {}) {
inline const Def* fn(wrap o, Refer wmode, Refer mod, Refer dbg = {}) {
World& w = mod->world();
return w.app(w.ax(o), {wmode, mod}, dbg);
}
inline const Def* fn(div o, const Def* mod, const Def* dbg = {}) {
World& w = mod->world();
return w.app(w.ax(o), mod, dbg);
}
inline const Def* fn(rop o, const Def* rmode, const Def* width, const Def* dbg = {}) {
inline const Def* fn(rop o, Refer rmode, Refer width, Refer dbg = {}) {
World& w = rmode->world();
return w.app(w.ax(o), {rmode, width}, dbg);
}
inline const Def* fn(rcmp o, const Def* rmode, const Def* width, const Def* dbg = {}) {
inline const Def* fn(rcmp o, Refer rmode, Refer width, Refer dbg = {}) {
World& w = rmode->world();
return w.app(w.ax(o), {rmode, width}, dbg);
}
inline const Def* fn(conv o, const Def* dst_w, const Def* src_w, const Def* dbg = {}) {
inline const Def* fn(conv o, Refer dst_w, Refer src_w, Refer dbg = {}) {
World& w = dst_w->world();
return w.app(w.ax(o), {dst_w, src_w}, dbg);
}
inline const Def* fn_bitcast(const Def* dst_t, const Def* src_t, const Def* dbg = {}) {
inline const Def* fn_bitcast(Refer dst_t, Refer src_t, Refer dbg = {}) {
World& w = dst_t->world();
return w.app(w.ax<bitcast>(), {dst_t, src_t}, dbg);
}
///@}

/// @name op - these guys build the final function application for the various operations
///@{
inline const Def* op(bit2 o, const Def* a, const Def* b, const Def* dbg = {}) {
World& w = a->world();
return w.app(fn(o, w.iinfer(a)), {a, b}, dbg);
}
inline const Def* op(icmp o, const Def* a, const Def* b, const Def* dbg = {}) {
World& w = a->world();
return w.app(fn(o, w.iinfer(a)), {a, b}, dbg);
}
inline const Def* op(shr o, const Def* a, const Def* b, const Def* dbg = {}) {
World& w = a->world();
return w.app(fn(o, w.iinfer(a)), {a, b}, dbg);
}
inline const Def* op(wrap o, const Def* wmode, const Def* a, const Def* b, const Def* dbg = {}) {
inline const Def* op(wrap o, Refer wmode, Refer a, Refer b, Refer dbg = {}) {
World& w = a->world();
return w.app(fn(o, wmode, w.iinfer(a)), {a, b}, dbg);
}
inline const Def* op(div o, const Def* mem, const Def* a, const Def* b, const Def* dbg = {}) {
World& w = mem->world();
return w.app(fn(o, w.iinfer(a)), {mem, a, b}, dbg);
}
inline const Def* op(rop o, const Def* rmode, const Def* a, const Def* b, const Def* dbg = {}) {
inline const Def* op(rop o, Refer rmode, Refer a, Refer b, Refer dbg = {}) {
World& w = rmode->world();
return w.app(fn(o, rmode, rinfer(a)), {a, b}, dbg);
}
inline const Def* op(rcmp o, const Def* rmode, const Def* a, const Def* b, const Def* dbg = {}) {
inline const Def* op(rcmp o, Refer rmode, Refer a, Refer b, Refer dbg = {}) {
World& w = rmode->world();
return w.app(fn(o, rmode, rinfer(a)), {a, b}, dbg);
}

template<class O>
const Def* op(O o, nat_t mode, const Def* a, const Def* b, const Def* dbg = {}) {
const Def* op(O o, nat_t mode, Refer a, Refer b, Refer dbg = {}) {
World& w = a->world();
return op(o, w.lit_nat(mode), a, b, dbg);
}

inline const Def* get_size(const Def* type) {
inline Refer get_size(Refer type) {
if (auto size = Idx::size(type)) return size;
if (auto real = match<Real>(type)) return real->arg();
unreachable();
}

inline const Def* op(conv o, const Def* dst_type, const Def* src, const Def* dbg = {}) {
inline const Def* op(conv o, Refer dst_type, Refer src, Refer dbg = {}) {
World& w = dst_type->world();
auto d = get_size(dst_type);
auto s = get_size(src->type());
return w.app(fn(o, d, s), src, dbg);
}
inline const Def* op(trait o, const Def* type, const Def* dbg = {}) {
inline const Def* op(trait o, Refer type, Refer dbg = {}) {
World& w = type->world();
return w.app(w.ax(o), type, dbg);
}
inline const Def* op_bitcast(const Def* dst_type, const Def* src, const Def* dbg = {}) {
inline const Def* op_bitcast(Refer dst_type, Refer src, Refer dbg = {}) {
World& w = dst_type->world();
return w.app(fn_bitcast(dst_type, src->type()), src, dbg);
}
inline const Def* op(pe o, const Def* def, const Def* dbg = {}) {
inline const Def* op(pe o, Refer def, Refer dbg = {}) {
World& w = def->world();
return w.app(w.app(w.ax(o), def->type()), def, dbg);
}
///@}

/// @name extract helper
///@{
inline const Def* extract_unsafe(const Def* d, const Def* i, const Def* dbg = {}) {
inline const Def* extract_unsafe(Refer d, Refer i, Refer dbg = {}) {
World& w = d->world();
return w.extract(d, op(conv::u2u, w.type_idx(as_lit(d->unfold_type()->arity())), i, dbg), dbg);
}
inline const Def* extract_unsafe(const Def* d, u64 i, const Def* dbg = {}) {
inline const Def* extract_unsafe(Refer d, u64 i, Refer dbg = {}) {
World& w = d->world();
return extract_unsafe(d, w.lit_idx(0_u64, i), dbg);
}
///@}

/// @name insert helper
///@{
inline const Def* insert_unsafe(const Def* d, const Def* i, const Def* val, const Def* dbg = {}) {
inline const Def* insert_unsafe(Refer d, Refer i, Refer val, Refer dbg = {}) {
World& w = d->world();
return w.insert(d, op(conv::u2u, w.type_idx(as_lit(d->unfold_type()->arity())), i), val, dbg);
}
inline const Def* insert_unsafe(const Def* d, u64 i, const Def* val, const Def* dbg = {}) {
inline const Def* insert_unsafe(Refer d, u64 i, Refer val, Refer dbg = {}) {
World& w = d->world();
return insert_unsafe(d, w.lit_idx(0_u64, i), val, dbg);
}
Expand Down Expand Up @@ -207,11 +175,6 @@ inline const Lit* lit_real(World& w, nat_t width, r64 val, const Def* dbg = {})

/// @name wrappers for unary operations
///@{
inline const Def* op_negate(const Def* a, const Def* dbg = {}) {
World& w = a->world();
auto s = as_lit(w.iinfer(a));
return op(bit2::_xor, w.lit_idx(s, s - 1_u64), a, dbg);
}
inline const Def* op_wminus(const Def* wmode, const Def* a, const Def* dbg = {}) {
World& w = a->world();
auto s = as_lit(w.iinfer(a));
Expand Down
25 changes: 13 additions & 12 deletions dialects/core/normalizers.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -258,8 +258,9 @@ static const Def* merge_cmps(std::array<std::array<u64, 2>, 2> tab, const Def* a
static_assert(sizeof(sub_t) == 1, "if this ever changes, please adjust the logic below");
static constexpr size_t num_bits = std::bit_width(Axiom::Num<Id> - 1_u64);

auto a_cmp = match<Id>(a);
auto b_cmp = match<Id>(b);
auto a_cmp = match<Id>(a);
auto b_cmp = match<Id>(b);
auto& world = a->world();

if (a_cmp && b_cmp && a_cmp->args() == b_cmp->args()) {
// push sub bits of a_cmp and b_cmp through truth table
Expand All @@ -273,7 +274,7 @@ static const Def* merge_cmps(std::array<std::array<u64, 2>, 2> tab, const Def* a
if constexpr (std::is_same_v<Id, rcmp>)
return op(rcmp(res), /*rmode*/ a_cmp->decurry()->arg(0), a_cmp->arg(0), a_cmp->arg(1), dbg);
else
return op(icmp(Axiom::Base<icmp> | res), a_cmp->arg(0), a_cmp->arg(1), dbg);
return world.call(icmp(Axiom::Base<icmp> | res), {a_cmp->arg(0), a_cmp->arg(1)}, dbg);
}

return nullptr;
Expand All @@ -292,7 +293,7 @@ static const Def* merge_cmps(std::array<std::array<u64, 2>, 2> tab, const Def* a
/// ```
template<class Id>
static const Def*
reassociate(Id id, World& /*world*/, [[maybe_unused]] const App* ab, const Def* a, const Def* b, const Def* dbg) {
reassociate(Id id, World& world, [[maybe_unused]] const App* ab, const Def* a, const Def* b, const Def* dbg) {
if (!is_associative(id)) return nullptr;

auto la = a->isa<Lit>();
Expand Down Expand Up @@ -324,7 +325,7 @@ reassociate(Id id, World& /*world*/, [[maybe_unused]] const App* ab, const Def*
// if we reassociate Wraps, we have to forget about nsw/nuw
make_op = [&](const Def* a, const Def* b) { return op(id, WMode::none, a, b, dbg); };
} else {
make_op = [&](const Def* a, const Def* b) { return op(id, a, b, dbg); };
make_op = [&](const Def* a, const Def* b) { return world.call(id, {a, b}, dbg); };
}

if (la && lz) return make_op(make_op(la, lz), w); // (1)
Expand Down Expand Up @@ -483,8 +484,8 @@ const Def* normalize_bit1(const Def* type, const Def* c, const Def* a, const Def
auto l = isa_lit(a);

switch (id) {
case bit1::f: return world.lit_idx(*s, 0);
case bit1::t: return world.lit_idx(*s, *s - 1_u64);
case bit1::f: return world.lit(type, 0);
case bit1::t: return world.lit(type, *s - 1_u64);
case bit1::id: return a;
default: break;
}
Expand Down Expand Up @@ -516,10 +517,10 @@ const Def* normalize_bit2(const Def* type, const Def* c, const Def* arg, const D
case bit2:: t: if (w) return world.lit(type, *w-1_u64); break;
case bit2:: a: return a;
case bit2:: b: return b;
case bit2:: na: return op_negate(a, dbg);
case bit2:: nb: return op_negate(b, dbg);
case bit2:: ciff: return op(bit2:: iff, b, a, dbg);
case bit2::nciff: return op(bit2::niff, b, a, dbg);
case bit2:: na: return world.call(bit1::neg, a, dbg);
case bit2:: nb: return world.call(bit1::neg, b, dbg);
case bit2:: ciff: return world.call(bit2:: iff, {b, a}, dbg);
case bit2::nciff: return world.call(bit2::niff, {b, a}, dbg);
default: break;
}

Expand All @@ -541,7 +542,7 @@ const Def* normalize_bit2(const Def* type, const Def* c, const Def* arg, const D
if (!x && !y) return world.lit(type, 0);
if ( x && y) return w ? world.lit(type, *w-1_u64) : nullptr;
if (!x && y) return a;
if ( x && !y && id != bit2::_xor) return op_negate(a, dbg);
if ( x && !y && id != bit2::_xor) return world.call(bit1::neg, a, dbg);
return nullptr;
};
// clang-format on
Expand Down
Loading