From f036a7ad166bdace8cc7bd03b8df811e9d1e5ae5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Aug 2018 18:04:16 -0700
Subject: [PATCH] chore(runtime/object): `mk_thunk(c)` should not modify `c`'s
 RC

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)`.
---
 src/runtime/object.h      | 19 +++++++++++--------
 src/tests/util/object.cpp | 25 ++++++++++++++++++++++---
 2 files changed, 33 insertions(+), 11 deletions(-)

diff --git a/src/runtime/object.h b/src/runtime/object.h
index dbf2716fbb..a4fb527c9f 100644
--- a/src/runtime/object.h
+++ b/src/runtime/object.h
@@ -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 */
diff --git a/src/tests/util/object.cpp b/src/tests/util/object.cpp
index ff5fe9d4b0..32fd4b2933 100644
--- a/src/tests/util/object.cpp
+++ b/src/tests/util/object.cpp
@@ -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;
 }