Skip to content

Commit be62626

Browse files
NeuralCoder3NeuralCoder3
committed
split debug dialect, added filter axiom
1 parent 6f4f899 commit be62626

19 files changed

+424
-31
lines changed

‎dialects/CMakeLists.txt

+10
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,16 @@ add_thorin_dialect(core
4646
INSTALL
4747
)
4848

49+
add_thorin_dialect(tool
50+
SOURCES
51+
tool/tool.cpp
52+
tool/tool.h
53+
tool/passes/set_filter.h
54+
tool/passes/set_filter.cpp
55+
tool/normalizers.cpp
56+
INSTALL
57+
)
58+
4959
add_thorin_dialect(debug
5060
SOURCES
5161
debug/debug.cpp

‎dialects/debug/debug.thorin

-4
Original file line numberDiff line numberDiff line change
@@ -24,10 +24,6 @@
2424
/// Permanently debugs at every construction.
2525
/// Gets removed at codegen preparation.
2626
.ax %debug.dbg_perm: Π [T:*] -> T -> T, normalize_dbg_perm;
27-
/// ### %debug.force
28-
///
29-
/// Forces beta reduction
30-
.ax %debug.force_type: * -> *, normalize_force_type;
3127
///
3228
/// ### %debug.dbg_poly
3329
///

‎dialects/debug/normalizers.cpp

-16
Original file line numberDiff line numberDiff line change
@@ -16,22 +16,6 @@ const Def* normalize_dbg_perm(const Def* type, const Def* callee, const Def* arg
1616
return world.raw_app(callee, arg, dbg);
1717
}
1818

19-
const Def* normalize_force_type(const Def* type, const Def* callee, const Def* arg, const Def* dbg) {
20-
auto& world = type->world();
21-
// debug_print("force_type", arg);
22-
if (auto app = arg->isa<App>()) {
23-
auto callee = app->callee();
24-
auto args = app->arg();
25-
if (auto lam = callee->isa<Lam>()) {
26-
auto res = lam->reduce(args).back(); // ops => filter, result
27-
world.DLOG("force {} : {} with {} : {}", lam, lam->type(), args, args->type());
28-
world.DLOG("res {}", res);
29-
return res;
30-
}
31-
}
32-
return world.raw_app(callee, arg, dbg);
33-
}
34-
3519
THORIN_debug_NORMALIZER_IMPL
3620

3721
} // namespace thorin::debug

‎dialects/direct/direct.thorin

+2-2
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
///
1010
/// ## Dependencies
1111
///
12-
.import debug;
12+
.import tool;
1313
///
1414
/// ## Types
1515
///
@@ -27,4 +27,4 @@
2727
/// the function is not converted; only the call site is changed
2828
///
2929
.ax %direct.cps2ds: Π [T: *, U: *] -> (.Cn [T, .Cn U]) -> (T -> U), normalize_cps2ds;
30-
.ax %direct.cps2ds_dep: Π [T: *, U: T -> *] -> (.Cn [t:T, .Cn (%debug.force_type (U t))]) -> (Π [t:T] -> (%debug.force_type (U t)));
30+
.ax %direct.cps2ds_dep: Π [T: *, U: T -> *] -> (.Cn [t:T, .Cn (%tool.force_type (U t))]) -> (Π [t:T] -> (%tool.force_type (U t)));

‎dialects/direct/passes/ds2cps.cpp

+7-4
Original file line numberDiff line numberDiff line change
@@ -26,14 +26,13 @@ namespace thorin::direct {
2626
// // if (body != b) world().ILOG("changed body of {}", lam);
2727
// }
2828

29-
3029
const Def* DS2CPS::rewrite(const Def* def) {
3130
auto& world = def->world();
32-
if(auto app = def->isa<App>()) {
31+
if (auto app = def->isa<App>()) {
3332
auto callee = app->callee();
3433
// world.DLOG("callee {} : {}", callee, callee->type());
3534
// world.DLOG("arg {} : {}", app->arg(), app->arg()->type());
36-
if(auto lam = callee->isa_nom<Lam>()) {
35+
if (auto lam = callee->isa_nom<Lam>()) {
3736
world.DLOG("encountered lam app");
3837
auto new_lam = rewrite_lam(lam);
3938
auto new_app = world.app(new_lam, app->arg());
@@ -54,7 +53,11 @@ const Def* DS2CPS::rewrite_lam(Lam* lam) {
5453
// ignore ds on type level
5554
if (lam->type()->codom()->isa<Type>()) { return lam; }
5655
// ignore higher order function
57-
if (lam->type()->codom()->isa<Pi>()) { return lam; }
56+
if (lam->type()->codom()->isa<Pi>()) {
57+
// causes segfault in depth
58+
// lam->set_filter(true);
59+
return lam;
60+
}
5861

5962
world().DLOG("rewrite DS function {} : {}", lam, lam->type());
6063

‎dialects/tool/normalizers.cpp

+33
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
#include "thorin/normalize.h"
2+
#include "thorin/world.h"
3+
4+
#include "dialects/tool/tool.h"
5+
6+
namespace thorin::tool {
7+
8+
const Def* normalize_force_type(const Def* type, const Def* callee, const Def* arg, const Def* dbg) {
9+
auto& world = type->world();
10+
// debug_print("force_type", arg);
11+
if (auto app = arg->isa<App>()) {
12+
auto callee = app->callee();
13+
auto args = app->arg();
14+
if (auto lam = callee->isa<Lam>()) {
15+
auto res = lam->reduce(args).back(); // ops => filter, result
16+
world.DLOG("force {} : {} with {} : {}", lam, lam->type(), args, args->type());
17+
world.DLOG("res {}", res);
18+
return res;
19+
}
20+
}
21+
return world.raw_app(callee, arg, dbg);
22+
}
23+
24+
const Def* normalize_set_filter(const Def* type, const Def* callee, const Def* arg, const Def* dbg) {
25+
auto& world = type->world();
26+
// auto [filter, lam] = arg->projs<2>();
27+
28+
return world.raw_app(callee, arg, dbg);
29+
}
30+
31+
THORIN_tool_NORMALIZER_IMPL
32+
33+
} // namespace thorin::tool

‎dialects/tool/passes/set_filter.cpp

+27
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
#include "dialects/tool/passes/set_filter.h"
2+
3+
#include <iostream>
4+
5+
#include <thorin/lam.h>
6+
#include <thorin/tables.h>
7+
8+
#include "dialects/tool/tool.h"
9+
10+
namespace thorin::tool {
11+
12+
const Def* SetFilter::rewrite(const Def* def) {
13+
if (auto set_filter_app = match<set_filter>(def)) {
14+
auto [filter, v] = set_filter_app->args<2>();
15+
world().DLOG("set_filter: {} for expr {}", filter, v);
16+
Lam* lam = curr_nom()->as<Lam>();
17+
world().DLOG("lambda: {}", lam);
18+
world().DLOG("current filter is: {}", lam->filter());
19+
lam->set_filter(filter);
20+
// assert(0);
21+
return v;
22+
}
23+
24+
return def;
25+
}
26+
27+
} // namespace thorin::tool

‎dialects/tool/passes/set_filter.h

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#pragma once
2+
3+
#include <thorin/def.h>
4+
#include <thorin/pass/pass.h>
5+
6+
namespace thorin::tool {
7+
8+
class SetFilter : public RWPass<SetFilter, Lam> {
9+
public:
10+
SetFilter(PassMan& man)
11+
: RWPass(man, "set_filter") {}
12+
13+
const Def* rewrite(const Def*) override;
14+
};
15+
16+
} // namespace thorin::tool

‎dialects/tool/tool.cpp

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include "dialects/tool/tool.h"
2+
3+
#include <thorin/config.h>
4+
#include <thorin/dialects.h>
5+
#include <thorin/pass/pass.h>
6+
7+
#include "dialects/tool/passes/set_filter.h"
8+
9+
using namespace thorin;
10+
11+
/// heart of the dialect
12+
/// registers passes in the different optimization phases
13+
/// as well as normalizers for the axioms
14+
extern "C" THORIN_EXPORT thorin::DialectInfo thorin_get_dialect_info() {
15+
return {"tool",
16+
[](thorin::PipelineBuilder& builder) {
17+
builder.extend_codegen_prep_phase([](PassMan& man) { man.add<thorin::tool::SetFilter>(); });
18+
},
19+
nullptr, [](Normalizers& normalizers) { tool::register_normalizers(normalizers); }};
20+
}

‎dialects/tool/tool.h

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
#pragma once
2+
3+
#include <thorin/world.h>
4+
5+
#include "dialects/tool/autogen.h"
6+
7+
/// add c++ bindings to call the axioms here
8+
/// preferably using inlined functions
9+
namespace thorin::tool {} // namespace thorin::tool

‎dialects/tool/tool.thorin

+25
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
/// # The tool dialect {#tool}
2+
///
3+
/// [TOC]
4+
///
5+
/// A toolkit for gadgets
6+
///
7+
/// ## Dependencies
8+
///
9+
/// none
10+
///
11+
/// ## Types
12+
///
13+
/// none
14+
///
15+
/// ## Operations
16+
///
17+
/// ### %tool.force
18+
///
19+
/// Forces beta reduction
20+
.ax %tool.force_type: * -> *, normalize_force_type;
21+
///
22+
/// ### %tool.set_filter
23+
///
24+
// .ax %tool.set_filter: Π [T: *] -> [%Int 2,T] -> T, normalize_set_filter;
25+
.ax %tool.set_filter: [%Int 2,⊥:★] -> ⊥:★, normalize_set_filter;

‎lit/CMakeLists.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ set(PYTHON_EXECUTABLE ${Python3_EXECUTABLE})
44
configure_file(lit.site.cfg.py.in lit.site.cfg.py @ONLY)
55
add_custom_target(check
66
COMMAND ${PYTHON_EXECUTABLE} "${CMAKE_CURRENT_SOURCE_DIR}/lit" "${CMAKE_CURRENT_BINARY_DIR}" -v
7-
DEPENDS thorin thorin_affine thorin_core thorin_mem thorin_debug thorin_direct thorin_autodiff)
7+
DEPENDS thorin thorin_affine thorin_core thorin_mem thorin_debug thorin_tool thorin_direct thorin_autodiff)
88

99
# We don't want to test python for memory leaks.. :/
1010
# add_test(NAME lit COMMAND python3 "${CMAKE_CURRENT_SOURCE_DIR}/lit" "${CMAKE_CURRENT_BINARY_DIR}" -v)

‎lit/autodiff/call_autodiff.thorin

+74
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
// RUN: rm -f %t.ll ; \
2+
// RUN: %thorin -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
3+
4+
// a call to a autodiff style function
5+
// ./build/bin/thorin -d debug -d direct -d autodiff ./lit/autodiff/multiply_autodiff.thorin --output-thorin - -VVVV
6+
7+
// triple take
8+
/*
9+
eval_thorin () {
10+
./build/bin/thorin -d debug -d direct -d autodiff $1 --output-thorin $2 -VVVV
11+
}
12+
T0=./lit/autodiff/multiply_autodiff.thorin
13+
T1=$(mktemp)
14+
T2=$(mktemp)
15+
eval_thorin $T0 $T1 && \
16+
eval_thorin $T1 $T2 && \
17+
eval_thorin $T2 -
18+
19+
*/
20+
.import core;
21+
.import autodiff;
22+
.import mem;
23+
24+
.let I32 = %Int 4294967296;
25+
26+
.cn g [b:I32, ret: .Cn [I32]] = {
27+
.let c = %core.wrap.mul (0:.Nat, 4294967296:.Nat) (3:I32, b);
28+
ret c
29+
};
30+
31+
.cn f [a:I32, ret: .Cn [I32]] = {
32+
.let b = %core.wrap.mul (0:.Nat, 4294967296:.Nat) (2:I32, a);
33+
// ret b
34+
g (b, ret)
35+
};
36+
37+
.cn .extern main [mem : %mem.M, argc : I32, argv : %mem.Ptr (%mem.Ptr (%Int 256, 0:.Nat), 0:.Nat), return : .Cn [%mem.M, I32]] = {
38+
39+
.cn ret_cont [r:I32,pb:.Cn[I32,.Cn[I32]]] = {
40+
.cn pb_ret_cont [pr:I32] = {
41+
.let c = %core.wrap.mul (0:.Nat, 4294967296:.Nat) (100:I32, r);
42+
.let d = %core.wrap.add (0:.Nat, 4294967296:.Nat) (c, pr);
43+
return (mem, d)
44+
};
45+
// return (mem, r)
46+
pb((1:I32),pb_ret_cont)
47+
};
48+
49+
.let f_diff = %autodiff.autodiff (.Cn [I32,.Cn[I32]]) f;
50+
.let f_diff_cast =
51+
// %core.bitcast
52+
// (
53+
// .Cn [I32, .Cn[I32, .Cn[I32, .Cn[I32]]]],
54+
// %autodiff.autodiff_type (.Cn [I32, .Cn[I32]])
55+
// )
56+
f_diff;
57+
58+
.let c = (42:I32);
59+
f_diff_cast (c,ret_cont)
60+
};
61+
62+
63+
// .let b = %Wrap_mul (0:.Nat, 4294967296:.Nat) (3:I32, a);
64+
65+
// .let c = f (42:I32);
66+
// return (mem, c)
67+
68+
// CHECK-DAG: .cn .extern main _{{[0-9_]+}}::[mem_[[memId:[_0-9]*]]: %mem.M, (%Int 4294967296), %mem.Ptr (%mem.Ptr ((%Int 256), 0:.Nat), 0:.Nat), return_[[returnId:[_0-9]*]]: .Cn [%mem.M, (%Int 4294967296)]] = {
69+
// CHECK-DAG: _[[appId:[_0-9]*]]: ⊥:★ = return_[[returnEtaId:[_0-9]*]] (mem_[[memId]], 42:(%Int 4294967296));
70+
// CHECK-DAG: _[[appId]]
71+
72+
// CHECK-DAG: return_[[returnEtaId]] _[[returnEtaVarId:[0-9_]+]]: [%mem.M, (%Int 4294967296)] = {
73+
// CHECK-DAG: return_[[retAppId:[_0-9]*]]: ⊥:★ = return_[[returnId]] _[[returnEtaVarId]];
74+
// CHECK-DAG: return_[[retAppId]]

‎lit/autodiff/call_autodiff_cont.thorin

+78
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
// RUN: rm -f %t.ll ; \
2+
// RUN: %thorin -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
3+
4+
// a call to a autodiff style function
5+
// ./build/bin/thorin -d debug -d direct -d autodiff ./lit/autodiff/multiply_autodiff.thorin --output-thorin - -VVVV
6+
7+
// triple take
8+
/*
9+
eval_thorin () {
10+
./build/bin/thorin -d debug -d direct -d autodiff $1 --output-thorin $2 -VVVV
11+
}
12+
T0=./lit/autodiff/multiply_autodiff.thorin
13+
T1=$(mktemp)
14+
T2=$(mktemp)
15+
eval_thorin $T0 $T1 && \
16+
eval_thorin $T1 $T2 && \
17+
eval_thorin $T2 -
18+
19+
*/
20+
.import core;
21+
.import autodiff;
22+
.import mem;
23+
24+
.let I32 = %Int 4294967296;
25+
26+
.cn g [a:I32, ret: .Cn [I32]] = {
27+
.let b = %core.wrap.add (0:.Nat, 4294967296:.Nat) (3:I32, a);
28+
ret b
29+
};
30+
31+
// 4(3+2a)
32+
.cn f [a:I32, ret: .Cn [I32]] = {
33+
.cn ret_cont [x:I32] = {
34+
.let b = %core.wrap.mul (0:.Nat, 4294967296:.Nat) (4:I32, a);
35+
ret b
36+
};
37+
.let b = %core.wrap.mul (0:.Nat, 4294967296:.Nat) (2:I32, a);
38+
g (b, ret_cont)
39+
};
40+
41+
.cn .extern main [mem : %mem.M, argc : I32, argv : %mem.Ptr (%mem.Ptr (%Int 256, 0:.Nat), 0:.Nat), return : .Cn [%mem.M, I32]] = {
42+
43+
.cn ret_cont [r:I32,pb:.Cn[I32,.Cn[I32]]] = {
44+
.cn pb_ret_cont [pr:I32] = {
45+
.let c = %core.wrap.mul (0:.Nat, 4294967296:.Nat) (100:I32, r);
46+
.let d = %core.wrap.add (0:.Nat, 4294967296:.Nat) (c, pr);
47+
return (mem, d)
48+
};
49+
// return (mem, r)
50+
pb((1:I32),pb_ret_cont)
51+
};
52+
53+
.let f_diff = %autodiff.autodiff (.Cn [I32,.Cn[I32]]) f;
54+
.let f_diff_cast =
55+
// %core.bitcast
56+
// (
57+
// .Cn [I32, .Cn[I32, .Cn[I32, .Cn[I32]]]],
58+
// %autodiff.autodiff_type (.Cn [I32, .Cn[I32]])
59+
// )
60+
f_diff;
61+
62+
.let c = (42:I32);
63+
f_diff_cast (c,ret_cont)
64+
};
65+
66+
67+
// .let b = %Wrap_mul (0:.Nat, 4294967296:.Nat) (3:I32, a);
68+
69+
// .let c = f (42:I32);
70+
// return (mem, c)
71+
72+
// CHECK-DAG: .cn .extern main _{{[0-9_]+}}::[mem_[[memId:[_0-9]*]]: %mem.M, (%Int 4294967296), %mem.Ptr (%mem.Ptr ((%Int 256), 0:.Nat), 0:.Nat), return_[[returnId:[_0-9]*]]: .Cn [%mem.M, (%Int 4294967296)]] = {
73+
// CHECK-DAG: _[[appId:[_0-9]*]]: ⊥:★ = return_[[returnEtaId:[_0-9]*]] (mem_[[memId]], 42:(%Int 4294967296));
74+
// CHECK-DAG: _[[appId]]
75+
76+
// CHECK-DAG: return_[[returnEtaId]] _[[returnEtaVarId:[0-9_]+]]: [%mem.M, (%Int 4294967296)] = {
77+
// CHECK-DAG: return_[[retAppId:[_0-9]*]]: ⊥:★ = return_[[returnId]] _[[returnEtaVarId]];
78+
// CHECK-DAG: return_[[retAppId]]

0 commit comments

Comments
 (0)