max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/vm/vm): bug at vm_index_manager?

Browse source 
@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.
This commit is contained in:
Leonardo de Moura 2016-12-22 18:14:02 -08:00
parent eefd4cd6ab
commit e5c4231248
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/vm/vm.cpp
View file

@ -3298,7 +3298,7 @@ public:
return static_cast<unsigned>(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<name> find_vm_name(unsigned idx) {

2
src/library/vm/vm.h
View file

@ -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<name> find_vm_name(unsigned idx);
/** \brief Reserve an index for the given function in the VM, the expression