max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(runtime/object): mk_thunk(c) should not modify c's RC

Browse source 
This is useful when we are generating a function that does not use the
"borrow semantics" for an argument `c` which is used in `mk_thunk(c)`.
This commit is contained in:
Leonardo de Moura 2018-08-10 18:04:16 -07:00
parent 6eb598268d
commit f036a7ad16
2 changed files with 33 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/runtime/object.h
View file

@ -334,22 +334,25 @@ inline thunk_object::thunk_object(object * c):
object(object_kind::Thunk), m_closure(c), m_value(nullptr) {
/* Remark: the implementation relies on the fact that nullptr is not a valid lean object. */
lean_assert(is_closure(c));
inc_ref(c);
}
inline object * alloc_thunk(object * c) {
/* Remark: `c`'s RC is not modified. Result object has RC == 1. */
inline object * mk_thunk(object * c) {
return new (malloc(sizeof(thunk_object))) thunk_object(c); // NOLINT
}
object * apply_1(object * f, object * a1);
/* Primitive for implementing the IR instruction for thunk.get : thunk A -> A
The `t`'s RC is not modified, and the result object RC should not be consumed by caller. */
inline object * thunk_get(object * t) {
if (object * r = to_thunk(t)->m_value)
return r;
object * r = apply_1(to_thunk(t)->m_closure, box(0));
lean_assert(r != nullptr); /* Closure must return a valid lean object */
to_thunk(t)->m_value = r;
return r;
if (object * r = to_thunk(t)->m_value)
return r;
object * r = apply_1(to_thunk(t)->m_closure, box(0));
lean_assert(r != nullptr); /* Closure must return a valid lean object */
to_thunk(t)->m_value = r;
return r;
}
/* String */

25
src/tests/util/object.cpp
View file

@ -15,9 +15,14 @@ object * f(object *) {
return box(10);
}
object_ref mk_thunk_ref(object_ref const & c) {
inc(c.raw());
return object_ref(mk_thunk(c.raw()));
}
static void tst1() {
object_ref c(alloc_closure(f, 1, 0));
object_ref t(alloc_thunk(c.raw()));
object_ref t = mk_thunk_ref(c);
object * r1 = thunk_get(t.raw());
object * r2 = thunk_get(t.raw());
std::cout << "thunk value: " << unbox(r1) << "\n";
@ -37,7 +42,7 @@ static void tst2() {
object * r2 = apply_1(c.raw(), box(0));
lean_assert(unbox(r1) == 1);
lean_assert(unbox(r2) == 2);
object_ref t(alloc_thunk(c.raw()));
object_ref t = mk_thunk_ref(c);
object * r3 = thunk_get(t.raw());
object * r4 = thunk_get(t.raw());
lean_assert(unbox(r3) == 3);
@ -57,7 +62,7 @@ object * h(object *) {
Lean object. */
static void tst3() {
object_ref c(alloc_closure(h, 1, 0));
object_ref t(alloc_thunk(c.raw()));
object_ref t = mk_thunk_ref(c);
lean_assert(g_h_counter == 0);
object * r3 = thunk_get(t.raw());
lean_assert(g_h_counter == 1);
@ -67,12 +72,26 @@ static void tst3() {
lean_assert(unbox(r4) == 0);
}
object * r(object *) {
return mk_string("hello world");
}
static void tst4() {
object_ref c(alloc_closure(r, 1, 0));
object_ref t = mk_thunk_ref(c);
object * r3 = thunk_get(t.raw());
object * r4 = thunk_get(t.raw());
lean_assert(string_eq(r3, "hello world"));
lean_assert(string_eq(r4, "hello world"));
}
int main() {
save_stack_info();
initialize_util_module();
tst1();
tst2();
tst3();
tst4();
finalize_util_module();
return has_violations() ? 1 : 0;
}