From e673fa65ba4a0f42071f3ae7dcfceecdab4a9e46 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 11 Nov 2016 15:39:16 -0800 Subject: [PATCH] feat(library/vm/vm): Store position information at vm_decl's --- src/library/compiler/vm_compiler.cpp | 2 +- src/library/vm/vm.cpp | 34 +++++++++++++++------------- src/library/vm/vm.h | 17 ++++++++++---- 3 files changed, 31 insertions(+), 22 deletions(-) diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index a42f75b7f3..2b16f44dba 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -353,7 +353,7 @@ static environment vm_compile(environment const & env, buffer const & optimize(new_env, code); lean_trace(name({"compiler", "optimize_bytecode"}), tout() << " " << p.m_name << " " << arity << "\n"; display_vm_code(tout().get_stream(), new_env, code.size(), code.data());); - new_env = update_vm_code(new_env, p.m_name, code.size(), code.data(), args_info); + new_env = update_vm_code(new_env, p.m_name, code.size(), code.data(), args_info, p.m_pos); } return new_env; } diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 2b3fe6ce07..b8beffb52f 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -682,8 +682,10 @@ vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_func vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfunction fn): m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(arity), m_cfn(fn) {} -vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code, list const & args_info): - m_rc(0), m_kind(vm_decl_kind::Bytecode), m_name(n), m_idx(idx), m_expr(e), m_arity(0), m_args_info(args_info), +vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code, + list const & args_info, optional const & pos): + m_rc(0), m_kind(vm_decl_kind::Bytecode), m_name(n), m_idx(idx), m_expr(e), m_arity(0), + m_args_info(args_info), m_pos(pos), m_code_size(code_sz) { expr it = e; while (is_lambda(it)) { @@ -816,15 +818,16 @@ struct vm_decls : public environment_extension { unsigned idx = m_next_decl_idx; m_next_decl_idx++; m_name2idx.insert(n, idx); - m_decls.insert(idx, vm_decl(n, idx, e, 0, nullptr, list())); + m_decls.insert(idx, vm_decl(n, idx, e, 0, nullptr, list(), optional())); return idx; } - void update(name const & n, unsigned code_sz, vm_instr const * code, list const & args_info) { + void update(name const & n, unsigned code_sz, vm_instr const * code, + list const & args_info, optional const & pos) { lean_assert(m_name2idx.contains(n)); unsigned idx = *m_name2idx.find(n); vm_decl const * d = m_decls.find(idx); - m_decls.insert(idx, vm_decl(n, idx, d->get_expr(), code_sz, code, args_info)); + m_decls.insert(idx, vm_decl(n, idx, d->get_expr(), code_sz, code, args_info, pos)); } }; @@ -941,11 +944,9 @@ static void reserve_reader(deserializer & d, shared_environment & senv, }); } - - void serialize_code(serializer & s, unsigned fidx, unsigned_map const & decls) { vm_decl const * d = decls.find(fidx); - s << d->get_name() << d->get_code_size(); + s << d->get_name() << d->get_code_size() << d->get_pos_info(); write_list(s, d->get_args_info()); vm_instr const * code = d->get_code(); auto fn = [&](unsigned idx) { return decls.find(idx)->get_name(); }; @@ -958,23 +959,23 @@ static void code_reader(deserializer & d, shared_environment & senv, std::function &, std::function &) { senv.update([&](environment const & env) -> environment { - name fn; unsigned code_sz; list args_info; - d >> fn; - d >> code_sz; + name fn; unsigned code_sz; list args_info; optional pos; + d >> fn >> code_sz >> pos; args_info = read_list(d); vm_decls ext = get_extension(env); buffer code; for (unsigned i = 0; i < code_sz; i++) { code.push_back(read_vm_instr(d, ext.m_name2idx)); } - ext.update(fn, code_sz, code.data(), args_info); + ext.update(fn, code_sz, code.data(), args_info, pos); return update(env, ext); }); } -environment update_vm_code(environment const & env, name const & fn, unsigned code_sz, vm_instr const * code, list const & args_info) { +environment update_vm_code(environment const & env, name const & fn, unsigned code_sz, vm_instr const * code, + list const & args_info, optional const & pos) { vm_decls ext = get_extension(env); - ext.update(fn, code_sz, code, args_info); + ext.update(fn, code_sz, code, args_info, pos); environment new_env = update(env, ext); unsigned fidx = *ext.m_name2idx.find(fn); return module::add(new_env, *g_vm_code_key, [=](environment const & env, serializer & s) { @@ -982,9 +983,10 @@ environment update_vm_code(environment const & env, name const & fn, unsigned co }); } -environment add_vm_code(environment const & env, name const & fn, expr const & e, unsigned code_sz, vm_instr const * code, list const & args_info) { +environment add_vm_code(environment const & env, name const & fn, expr const & e, unsigned code_sz, vm_instr const * code, + list const & args_info, optional const & pos) { environment new_env = reserve_vm_index(env, fn, e); - return update_vm_code(new_env, fn, code_sz, code, args_info); + return update_vm_code(new_env, fn, code_sz, code, args_info, pos); } optional get_vm_decl(environment const & env, name const & n) { diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 6e08156411..72323819a4 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "util/serializer.h" #include "util/numerics/mpz.h" #include "kernel/environment.h" +#include "kernel/pos_info_provider.h" namespace lean { class vm_obj; @@ -450,6 +451,7 @@ struct vm_decl_cell { expr m_expr; unsigned m_arity; list m_args_info; + optional m_pos; union { struct { unsigned m_code_size; @@ -460,7 +462,8 @@ struct vm_decl_cell { }; vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn); vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfunction fn); - vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code, list const & args_info); + vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code, list const & args_info, + optional const & pos); ~vm_decl_cell(); void dealloc(); }; @@ -475,8 +478,9 @@ public: vm_decl(new vm_decl_cell(n, idx, arity, fn)) {} vm_decl(name const & n, unsigned idx, unsigned arity, vm_cfunction fn): vm_decl(new vm_decl_cell(n, idx, arity, fn)) {} - vm_decl(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code, list const & args_info): - vm_decl(new vm_decl_cell(n, idx, e, code_sz, code, args_info)) {} + vm_decl(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code, list const & args_info, + optional const & pos): + vm_decl(new vm_decl_cell(n, idx, e, code_sz, code, args_info, pos)) {} vm_decl(vm_decl const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } vm_decl(vm_decl && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } ~vm_decl() { if (m_ptr) m_ptr->dec_ref(); } @@ -501,6 +505,7 @@ public: vm_cfunction get_cfn() const { lean_assert(is_cfun()); return m_ptr->m_cfn; } expr const & get_expr() const { lean_assert(is_bytecode()); return m_ptr->m_expr; } list const & get_args_info() const { lean_assert(is_bytecode()); return m_ptr->m_args_info; } + optional const & get_pos_info() const { lean_assert(is_bytecode()); return m_ptr->m_pos; } }; /** \brief Virtual machine for executing VM bytecode. */ @@ -731,10 +736,12 @@ environment reserve_vm_index(environment const & env, name const & fn, expr cons /** \brief Add bytcode for the function named \c fn in \c env. \remark The index for \c fn must have been reserved using reserve_vm_index. */ -environment update_vm_code(environment const & env, name const & fn, unsigned code_sz, vm_instr const * code, list const & args_info); +environment update_vm_code(environment const & env, name const & fn, unsigned code_sz, vm_instr const * code, + list const & args_info, optional const & pos); /** \brief Combines reserve_vm_index and update_vm_code */ -environment add_vm_code(environment const & env, name const & fn, expr const & e, unsigned code_sz, vm_instr const * code, list const & args_info); +environment add_vm_code(environment const & env, name const & fn, expr const & e, unsigned code_sz, vm_instr const * code, + list const & args_info, optional const & pos); /** \brief Return the internal idx for the given constant. Return none if the constant is not builtin nor it has code associated with it. */