From 83aaf64318815dd7eaecbc473de9beb5601bfcbf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 30 Nov 2013 00:44:31 -0800
Subject: [PATCH] fix(library/tactic): memory leaks

Proof/Cex builders and tactics implemented in Lua had a "strong reference" to script_state. If they are stored in the Lua state, then we get a cyclic reference.
That is, script_state points to these objects, and they point back to script_state.

To avoid this memory leak, this commit defines a weak reference for script_state objects. The Proof/Cex builders and tactics now store a weak reference to the Lua state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/tactic/cex_builder.cpp   | 2 +-
 src/library/tactic/proof_builder.cpp | 2 +-
 src/library/tactic/tactic.cpp        | 4 ++--
 src/util/script_state.cpp            | 6 ++++--
 src/util/script_state.h              | 6 +++++-
 5 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/src/library/tactic/cex_builder.cpp b/src/library/tactic/cex_builder.cpp
index c64a9b657d..40ad65ffde 100644
--- a/src/library/tactic/cex_builder.cpp
+++ b/src/library/tactic/cex_builder.cpp
@@ -17,7 +17,7 @@ cex_builder & cex_builder::operator=(cex_builder && s) { LEAN_MOVE_REF(cex_build
 DECL_UDATA(cex_builder)
 
 static int mk_cex_builder(lua_State * L) {
-    script_state S = to_script_state(L);
+    script_state::weak_ref S = to_script_state(L).to_weak_ref();
     luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun
     luaref ref(L, 1);
     return push_cex_builder(L,
diff --git a/src/library/tactic/proof_builder.cpp b/src/library/tactic/proof_builder.cpp
index 50b999473b..3e363323e5 100644
--- a/src/library/tactic/proof_builder.cpp
+++ b/src/library/tactic/proof_builder.cpp
@@ -81,7 +81,7 @@ static const struct luaL_Reg assignment_m[] = {
 DECL_UDATA(proof_builder);
 
 static int mk_proof_builder(lua_State * L) {
-    script_state S = to_script_state(L);
+    script_state::weak_ref S = to_script_state(L).to_weak_ref();
     luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun
     luaref ref(L, 1);
     return push_proof_builder(L,
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 25c23f32e1..5ad86446f2 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -440,7 +440,7 @@ static int tactic_solve(lua_State * L) {
 
 static int mk_lua_tactic01(lua_State * L) {
     luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun
-    script_state S = to_script_state(L);
+    script_state::weak_ref S = to_script_state(L).to_weak_ref();
     luaref ref(L, 1);
     return push_tactic(L,
                        mk_tactic01([=](environment const & env, io_state const & ios, proof_state const & s) -> optional<proof_state> {
@@ -484,7 +484,7 @@ static int mk_lua_tactic01(lua_State * L) {
 
 static int mk_lua_cond_tactic(lua_State * L, tactic t1, tactic t2) {
     luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun
-    script_state S = to_script_state(L);
+    script_state::weak_ref S = to_script_state(L).to_weak_ref();
     luaref ref(L, 1);
     return push_tactic(L,
                        mk_tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp
index 3172b4e4c8..949ae31a5a 100644
--- a/src/util/script_state.cpp
+++ b/src/util/script_state.cpp
@@ -111,8 +111,10 @@ script_state::script_state():
     m_ptr->save_weak_ptr(m_ptr);
 }
 
-script_state::script_state(std::weak_ptr<imp> const & ptr):m_ptr(ptr.lock()) {
-    lean_assert(m_ptr);
+script_state::script_state(weak_ref const & r) {
+    if (r.expired())
+        throw exception("weak reference to script_state object has expired (i.e., it has been deleted)");
+    m_ptr = r.lock();
 }
 
 script_state::~script_state() {
diff --git a/src/util/script_state.h b/src/util/script_state.h
index d77afdcfd4..2fd84c9980 100644
--- a/src/util/script_state.h
+++ b/src/util/script_state.h
@@ -19,15 +19,19 @@ public:
     struct imp;
 private:
     std::shared_ptr<imp> m_ptr;
-    script_state(std::weak_ptr<imp> const & ptr);
     friend script_state to_script_state(lua_State * L);
     std::mutex & get_mutex();
     lua_State * get_state();
     friend class data_channel;
 public:
+    typedef std::weak_ptr<imp> weak_ref;
+
     script_state();
+    script_state(weak_ref const & r);
     ~script_state();
 
+    weak_ref to_weak_ref() const { return weak_ref(m_ptr); }
+
     /**
        \brief Execute the file with the given name.
        This method throws an exception if an error occurs.