From e5c4231248baf0db7bd6f06cb7832ddb88fe6dbf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Dec 2016 18:14:02 -0800 Subject: [PATCH] fix(library/vm/vm): bug at vm_index_manager? @gebner, I have been experiencing crashes that are hard to reproduce. I think one of the problems was that get_vm_name was returning a `name const &`. I think this may produce a memory access violation in the following scenario: 1- Thread 1 invokes get_vm_name, and gets a reference R. This is a reference to a memory cell in the vector m_idx2name. 2- Thread 2 invokes get_vm_index, and it triggers a vector resize operation. After the resize, reference R is invalid. 3- Thread 1 crashes trying to access R. --- src/library/vm/vm.cpp | 4 ++-- src/library/vm/vm.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 695d9b1164..2aae4ac143 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -3298,7 +3298,7 @@ public: return static_cast(m_idx2name.size()); } - name const & get_name(unsigned idx) { + name get_name(unsigned idx) { shared_lock lock(m_mutex); lean_assert(idx < m_idx2name.size()); return m_idx2name.at(idx); @@ -3321,7 +3321,7 @@ unsigned get_vm_index(name const & n) { unsigned get_vm_index_bound() { return g_vm_index_manager->get_index_bound(); } -name const & get_vm_name(unsigned idx) { +name get_vm_name(unsigned idx) { return g_vm_index_manager->get_name(idx); } optional find_vm_name(unsigned idx) { diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index a435a3ba80..5982accc74 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -828,7 +828,7 @@ environment add_native(environment const & env, name const & n, unsigned arity, unsigned get_vm_index(name const & n); unsigned get_vm_index_bound(); -name const & get_vm_name(unsigned idx); +name get_vm_name(unsigned idx); optional find_vm_name(unsigned idx); /** \brief Reserve an index for the given function in the VM, the expression