From fa19b3c94de687ecbcdbc8ba53e88472efb3778a Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 1 Mar 2017 10:33:26 +0100
Subject: [PATCH] fix(library/vm/vm): prevent segfault in out-of-memory
 conditions

---
 src/library/vm/vm.cpp | 26 +++++++++++++++++++++++++-
 src/library/vm/vm.h   | 16 ++--------------
 2 files changed, 27 insertions(+), 15 deletions(-)

diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index 1e53e71d1a..6039b5dd76 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -1368,6 +1368,31 @@ vm_state::vm_state(environment const & env, options const & opts):
 vm_state::~vm_state() {
 }
 
+vm_decl const & vm_state::get_decl(unsigned idx) const {
+    lean_assert(idx < m_decl_vector.size());
+    vm_decl const & d = m_decl_vector[idx];
+    if (d) return d;
+    if (auto d_ = m_decl_map.find(idx)) {
+        const_cast<vm_state *>(this)->m_decl_vector[idx] = *d_;
+    } else {
+        lean_unreachable();
+    }
+    return m_decl_vector[idx];
+}
+
+vm_cases_function const & vm_state::get_builtin_cases(unsigned idx) const {
+    lean_assert(idx < m_builtin_cases_vector.size());
+    vm_cases_function const & fn = m_builtin_cases_vector[idx];
+    if (fn != nullptr) return fn;
+    if (auto fn_ = m_builtin_cases_map.find(idx)) {
+        const_cast<vm_state *>(this)->m_builtin_cases_vector[idx] = *fn_;
+    } else {
+        lean_unreachable();
+    }
+    return m_builtin_cases_vector[idx];
+}
+
+
 struct vm_state::debugger_state {
     vm_state m_vm;
     vm_obj   m_state;
@@ -3316,7 +3341,6 @@ optional<name> vm_state::curr_fn() const {
     else
         return optional<name>(m_decl_map.find(m_fn_idx)->get_name());
 }
-
 #if defined(LEAN_MULTI_THREAD)
 static name * g_profiler      = nullptr;
 static name * g_profiler_freq = nullptr;
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index fd83b5055b..d84834e3a4 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -668,21 +668,9 @@ class vm_state {
     void execute(vm_instr const * code);
     vm_obj invoke_closure(vm_obj const & fn, unsigned nargs);
 
-    vm_decl const & get_decl(unsigned idx) const {
-        lean_assert(idx < m_decl_vector.size());
-        vm_decl const & d = m_decl_vector[idx];
-        if (d) return d;
-        const_cast<vm_state*>(this)->m_decl_vector[idx] = *m_decl_map.find(idx);
-        return m_decl_vector[idx];
-    }
+    vm_decl const & get_decl(unsigned idx) const;
 
-    vm_cases_function const & get_builtin_cases(unsigned idx) const {
-        lean_assert(idx < m_builtin_cases_vector.size());
-        vm_cases_function const & fn = m_builtin_cases_vector[idx];
-        if (fn != nullptr) return fn;
-        const_cast<vm_state*>(this)->m_builtin_cases_vector[idx] = *m_builtin_cases_map.find(idx);
-        return m_builtin_cases_vector[idx];
-    }
+    vm_cases_function const & get_builtin_cases(unsigned idx) const;
 
 public:
     vm_state(environment const & env, options const & opts);