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

feat(library/vm/vm): Store position information at vm_decl's

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-11 15:39:16 -08:00
parent b59c10118d
commit e673fa65ba
3 changed files with 31 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/vm_compiler.cpp
View file

@ -353,7 +353,7 @@ static environment vm_compile(environment const & env, buffer<procedure> 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;
}

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

@ -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<vm_local_info> 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<vm_local_info> const & args_info, optional<pos_info> 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<vm_local_info>()));
m_decls.insert(idx, vm_decl(n, idx, e, 0, nullptr, list<vm_local_info>(), optional<pos_info>()));
return idx;
}
void update(name const & n, unsigned code_sz, vm_instr const * code, list<vm_local_info> const & args_info) {
void update(name const & n, unsigned code_sz, vm_instr const * code,
list<vm_local_info> const & args_info, optional<pos_info> 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<vm_decl> 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<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> &) {
senv.update([&](environment const & env) -> environment {
name fn; unsigned code_sz; list<vm_local_info> args_info;
d >> fn;
d >> code_sz;
name fn; unsigned code_sz; list<vm_local_info> args_info; optional<pos_info> pos;
d >> fn >> code_sz >> pos;
args_info = read_list<vm_local_info>(d);
vm_decls ext = get_extension(env);
buffer<vm_instr> 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<vm_local_info> const & args_info) {
environment update_vm_code(environment const & env, name const & fn, unsigned code_sz, vm_instr const * code,
list<vm_local_info> const & args_info, optional<pos_info> 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<vm_local_info> const & args_info) {
environment add_vm_code(environment const & env, name const & fn, expr const & e, unsigned code_sz, vm_instr const * code,
list<vm_local_info> const & args_info, optional<pos_info> 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<vm_decl> get_vm_decl(environment const & env, name const & n) {

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

@ -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<vm_local_info> m_args_info;
optional<pos_info> 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<vm_local_info> const & args_info);
vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code, list<vm_local_info> const & args_info,
optional<pos_info> 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<vm_local_info> 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<vm_local_info> const & args_info,
optional<pos_info> 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<vm_local_info> const & get_args_info() const { lean_assert(is_bytecode()); return m_ptr->m_args_info; }
optional<pos_info> 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<vm_local_info> const & args_info);
environment update_vm_code(environment const & env, name const & fn, unsigned code_sz, vm_instr const * code,
list<vm_local_info> const & args_info, optional<pos_info> 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<vm_local_info> const & args_info);
environment add_vm_code(environment const & env, name const & fn, expr const & e, unsigned code_sz, vm_instr const * code,
list<vm_local_info> const & args_info, optional<pos_info> 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. */