From 6b582ca6c3094e8536bd5f2bc428f6bf92602a61 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 4 Oct 2016 01:58:39 -0700
Subject: [PATCH] fix(library/vm/vm): bug at get_constant

---
 src/library/vm/vm.cpp             | 20 +++++++++++++++++++-
 src/library/vm/vm.h               |  2 ++
 tests/lean/run/eval_expr_bug.lean |  6 ++++++
 3 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/eval_expr_bug.lean

diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index a7ac4e085f..bb9d31cf42 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -1695,6 +1695,16 @@ void vm_state::display_stack(std::ostream & out) const {
         out << "[bp]\n";
 }
 
+void vm_state::display_call_stack(std::ostream & out) const {
+    for (frame const & fr : m_call_stack) {
+        out << ">> (fn_idx := " << fr.m_fn_idx << ", num := " << fr.m_num << ", pc := " << fr.m_pc << ", bp: " << fr.m_bp << ")\n";
+    }
+}
+
+void vm_state::display_registers(std::ostream & out) const {
+    out << "pc: " << m_pc << ", bp: " << m_bp << "\n";
+}
+
 void vm_state::run() {
     lean_assert(m_code);
     unsigned init_call_stack_sz = m_call_stack.size();
@@ -1971,8 +1981,11 @@ void vm_state::run() {
                a_1, ... a_n were the arguments for the function call.
                r is the result.
             */
+            lean_assert(!m_call_stack.empty());
             frame const & fr = m_call_stack.back();
             unsigned sz      = m_stack.size();
+            lean_assert(sz - fr.m_num - 1 < m_stack.size());
+            lean_assert(sz - 1 < m_stack.size());
             swap(m_stack[sz - fr.m_num - 1], m_stack[sz - 1]);
             m_stack.resize(sz - fr.m_num);
             m_code   = fr.m_code;
@@ -2131,9 +2144,14 @@ vm_obj vm_state::get_constant(name const & cname) {
     if (auto fn_idx = m_fn_name2idx.find(cname)) {
         vm_decl d = get_decl(*fn_idx);
         if (d.get_arity() == 0) {
-            invoke_fn(*fn_idx);
+            DEBUG_CODE(unsigned stack_sz = m_stack.size(););
+            unsigned saved_pc = m_pc;
+            invoke(d);
+            run();
             vm_obj r = m_stack.back();
             m_stack.pop_back();
+            m_pc = saved_pc;
+            lean_assert(m_stack.size() == stack_sz);
             return r;
         } else {
             return mk_vm_closure(*fn_idx, 0, nullptr);
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index cceb8cb744..bdf601a55d 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -571,6 +571,8 @@ public:
 
     void display_stack(std::ostream & out) const;
     void display(std::ostream & out, vm_obj const & o) const;
+    void display_call_stack(std::ostream & out) const;
+    void display_registers(std::ostream & out) const;
 
     /** \brief Invoke closure \c fn with the given arguments. These procedures are meant to be use by
         C++ generated/extracted code. */
diff --git a/tests/lean/run/eval_expr_bug.lean b/tests/lean/run/eval_expr_bug.lean
new file mode 100644
index 0000000000..f58f437bf1
--- /dev/null
+++ b/tests/lean/run/eval_expr_bug.lean
@@ -0,0 +1,6 @@
+open tactic
+
+meta def a : nat := 10
+
+run_command eval_expr nat (expr.const `a [])
+run_command eval_expr nat (expr.const `a []) >>= trace