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

refactor(library/compiler/llnf): memory cell reuse instruction set

Browse source
This commit is contained in:
Leonardo de Moura 2018-10-31 09:35:22 -07:00
parent 67a78d1c76
commit 12a01d101c
6 changed files with 156 additions and 306 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
src/library/compiler/emit_bytecode.cpp
View file

@ -166,6 +166,17 @@ class emit_bytecode_fn {
emit(mk_constructor_instr(cidx, get_app_num_args(e)));
}
void compile_reuse(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
buffer<expr> args;
expr const & fn = get_app_args(e, args);
lean_assert(is_llnf_reuse(fn));
unsigned cidx, ssz;
is_llnf_reuse(fn, cidx, ssz);
if (ssz != 0) throw_no_unboxed_support();
compile_args(args.size(), args.data(), bpz, m);
emit(mk_reuse_instr(cidx, get_app_num_args(e) - 1));
}
void compile_external(name const & n, buffer<expr> & args, unsigned bpz, name_map<unsigned> const & m) {
// Not sure if this is the best approach, trying to lazy load the required
// dynamic libraries.
@ -208,34 +219,13 @@ class emit_bytecode_fn {
emit(mk_proj_instr(idx));
}
void compile_updt(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
expr fn = app_fn(app_fn(e));
expr s = app_arg(app_fn(e));
expr v = app_arg(e);
unsigned idx;
is_llnf_updt(fn, idx);
compile(s, bpz, m);
bpz++;
compile(v, bpz, m);
emit(mk_updt_instr(idx));
}
void compile_updt_cidx(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
expr fn = app_fn(e);
expr s = app_arg(e);
unsigned idx;
is_llnf_updt_cidx(fn, idx);
compile(s, bpz, m);
emit(mk_updt_cidx_instr(idx));
}
void compile_reset(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
expr fn = app_fn(e);
expr s = app_arg(e);
unsigned idx;
is_llnf_reset(fn, idx);
unsigned n;
is_llnf_reset(fn, n);
compile(s, bpz, m);
emit(mk_reset_instr(idx));
emit(mk_reset_instr(n));
}
void compile_app(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
@ -244,12 +234,10 @@ class emit_bytecode_fn {
compile_cases_on(e, bpz, m);
} else if (is_llnf_cnstr(fn)) {
compile_cnstr(e, bpz, m);
} else if (is_llnf_reuse(fn)) {
compile_reuse(e, bpz, m);
} else if (is_llnf_proj(fn)) {
compile_proj(e, bpz, m);
} else if (is_llnf_updt(fn)) {
compile_updt(e, bpz, m);
} else if (is_llnf_updt_cidx(fn)) {
compile_updt_cidx(e, bpz, m);
} else if (is_llnf_reset(fn)) {
compile_reset(e, bpz, m);
} else if (is_sorry(e)) {

252
src/library/compiler/llnf.cpp
View file

@ -17,6 +17,7 @@ Author: Leonardo de Moura
namespace lean {
static name * g_cnstr = nullptr;
static name * g_reuse = nullptr;
static name * g_reset = nullptr;
static name * g_updt = nullptr;
static name * g_updt_cidx = nullptr;
@ -52,14 +53,11 @@ static bool is_llnf_binary_primitive(expr const & e, name const & prefix, unsign
expr mk_llnf_cnstr(unsigned cidx, unsigned scalar_sz) { return mk_constant(name(name(*g_cnstr, cidx), scalar_sz)); }
bool is_llnf_cnstr(expr const & e, unsigned & cidx, unsigned & ssz) { return is_llnf_binary_primitive(e, *g_cnstr, cidx, ssz); }
expr mk_llnf_reset(unsigned i) { return mk_constant(name(*g_reset, i)); }
bool is_llnf_reset(expr const & e, unsigned & i) { return is_llnf_unary_primitive(e, *g_reset, i); }
expr mk_llnf_reuse(unsigned cidx, unsigned scalar_sz) { return mk_constant(name(name(*g_reuse, cidx), scalar_sz)); }
bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & ssz) { return is_llnf_binary_primitive(e, *g_reuse, cidx, ssz); }
expr mk_llnf_updt(unsigned i) { return mk_constant(name(*g_updt, i)); }
bool is_llnf_updt(expr const & e, unsigned & i) { return is_llnf_unary_primitive(e, *g_updt, i); }
expr mk_llnf_updt_cidx(unsigned cidx) { return mk_constant(name(*g_updt_cidx, cidx)); }
bool is_llnf_updt_cidx(expr const & e, unsigned & cidx) { return is_llnf_unary_primitive(e, *g_updt_cidx, cidx); }
expr mk_llnf_reset(unsigned n) { return mk_constant(name(*g_reset, n)); }
bool is_llnf_reset(expr const & e, unsigned & n) { return is_llnf_unary_primitive(e, *g_reset, n); }
expr mk_llnf_updt_u8(unsigned offset) { return mk_constant(name(*g_updt_u8, offset)); }
bool is_llnf_updt_u8(expr const & e, unsigned & offset) { return is_llnf_unary_primitive(e, *g_updt_u8, offset); }
@ -384,55 +382,22 @@ class to_llnf_fn {
return mk_app(mk_llnf_reset(idx), major);
}
expr mk_updt(expr const & major, unsigned idx, expr const & v) {
return mk_app(mk_llnf_updt(idx), major, v);
bool is_reuse_app(expr const & e) {
unsigned i, s;
return is_llnf_reuse(get_app_fn(e), i, s) && get_app_num_args(e) == 2;
}
expr mk_updt_cidx(expr const & major, unsigned cidx) {
return mk_app(mk_llnf_updt_cidx(cidx), major);
}
bool is_updt_app(expr const & e) {
bool is_updt_scalar(expr const & e) {
unsigned x;
return is_llnf_updt(get_app_fn(e), x) && get_app_num_args(e) == 2;
return
is_llnf_updt_u8(e, x) ||
is_llnf_updt_u16(e, x) ||
is_llnf_updt_u32(e, x) ||
is_llnf_updt_u64(e, x);
}
bool is_updt_cidx_app(expr const & e) {
unsigned x;
return is_llnf_updt_cidx(get_app_fn(e), x) && get_app_num_args(e) == 1;
}
expr find(expr const & e) const {
if (is_fvar(e)) {
if (optional<local_decl> decl = m_lctx.find_local_decl(e)) {
optional<expr> v = decl->get_value();
if (v) return find(*v);
}
} else if (is_mdata(e)) {
return find(mdata_expr(e));
}
return e;
}
/* Return true if `a` is of the form `_proj.<idx> e` */
bool is_proj_of(expr a, expr const & e, unsigned idx) {
a = find(a);
unsigned a_idx;
return is_app(a) && is_llnf_proj(app_fn(a), a_idx) && a_idx == idx && app_arg(a) == e;
}
/* Return true if `a` is of the form `_proj_u<size>.<offset> e` */
bool is_scalar_proj_of(expr a, expr const & e, unsigned size, unsigned offset) {
a = find(a);
unsigned a_offset;
if (!is_app(a) || app_arg(a) != e) return false;
switch (size) {
case 1: return is_llnf_proj_u8(app_fn(a), a_offset) && a_offset == offset;
case 2: return is_llnf_proj_u16(app_fn(a), a_offset) && a_offset == offset;
case 4: return is_llnf_proj_u32(app_fn(a), a_offset) && a_offset == offset;
case 8: return is_llnf_proj_u64(app_fn(a), a_offset) && a_offset == offset;
}
return false;
bool is_updt_scalar_app(expr const & e) {
return is_updt_scalar(get_app_fn(e)) && get_app_num_args(e) == 1;
}
/* Auxiliary functor for replacing constructor applications with update operations. */
@ -440,8 +405,6 @@ class to_llnf_fn {
to_llnf_fn & m_owner;
expr const & m_major;
cnstr_info const & m_cinfo;
/* `m_used_fields[i]` is true if the field `i` is used in the minor premise. */
buffer<bool> const & m_to_reset_fields;
/* `m_major` may be replaced/reused many times in different branches, but we
only have to reset fields once. */
bool m_reset{false};
@ -450,6 +413,32 @@ class to_llnf_fn {
environment const & env() { return m_owner.env(); }
expr find(expr const & e) const {
if (is_fvar(e)) {
if (optional<local_decl> decl = m_owner.m_lctx.find_local_decl(e)) {
optional<expr> v = decl->get_value();
if (v) return find(*v);
}
} else if (is_mdata(e)) {
return find(mdata_expr(e));
}
return e;
}
/* Return true if `a` is of the form `_proj_u<size>.<offset> e` */
bool is_scalar_proj_of(expr a, expr const & e, unsigned size, unsigned offset) {
a = find(a);
unsigned a_offset;
if (!is_app(a) || app_arg(a) != e) return false;
switch (size) {
case 1: return is_llnf_proj_u8(app_fn(a), a_offset) && a_offset == offset;
case 2: return is_llnf_proj_u16(app_fn(a), a_offset) && a_offset == offset;
case 4: return is_llnf_proj_u32(app_fn(a), a_offset) && a_offset == offset;
case 8: return is_llnf_proj_u64(app_fn(a), a_offset) && a_offset == offset;
}
return false;
}
expr visit_constructor(expr const & e) {
buffer<expr> args;
expr const & k = get_app_args(e, args);
@ -465,62 +454,31 @@ class to_llnf_fn {
}
constructor_val k_val = env().get(const_name(k)).to_constructor_val();
unsigned nparams = k_val.get_nparams();
/* See `mark_to_reset_fields` */
expr r;
if (!m_reset) {
r = m_major;
unsigned j = nparams;
unsigned i = 0;
unsigned idx = 0;
for (field_info const & info : k_info.m_field_info) {
lean_assert(j == i + nparams);
if (info.m_kind == field_info::Object) {
if (m_to_reset_fields[i]) {
expr new_updt = m_owner.mk_reset(r, idx);
r = m_owner.mk_let_decl(mk_enf_object_type(), new_updt);
}
idx++;
}
i++;
j++;
}
m_major_after_reset = m_owner.mk_reset(m_major, k_info.m_num_objs);
m_major_after_reset = m_owner.mk_let_decl(mk_enf_object_type(), m_major_after_reset);
m_reset = true;
m_major_after_reset = r;
} else {
r = m_major_after_reset;
}
expr r = m_major_after_reset;
/* Remark: note that we do not create let-declarations here for the following updates.
We will flatten them later when we visit the minor premise. */
/* Update constructor cidx if needed. */
if (k_info.m_cidx != m_cinfo.m_cidx) {
r = m_owner.mk_updt_cidx(r, k_info.m_cidx);
}
/* Update fields with new values. */
unsigned offset = k_info.m_num_objs * sizeof(void*);
buffer<expr> obj_args;
unsigned j = nparams;
unsigned i = 0;
unsigned idx = 0;
for (field_info const & info : k_info.m_field_info) {
lean_assert(j == i + nparams);
switch (info.m_kind) {
case field_info::Irrelevant:
break;
case field_info::Object:
if (m_to_reset_fields[i] || !m_owner.is_proj_of(args[j], m_major, idx)) {
r = m_owner.mk_updt(r, idx, args[j]);
}
idx++;
break;
case field_info::Scalar:
if (!m_owner.is_scalar_proj_of(args[j], m_major, info.m_size, offset)) {
if (info.m_kind == field_info::Object) {
obj_args.push_back(args[j]);
}
j++;
}
r = mk_app(mk_app(mk_llnf_reuse(k_info.m_cidx, k_info.m_scalar_sz), r), obj_args);
unsigned offset = k_info.m_num_objs * sizeof(void*);
for (field_info const & info : k_info.m_field_info) {
if (info.m_kind == field_info::Scalar) {
if (!is_scalar_proj_of(args[j], m_major, info.m_size, offset)) {
r = m_owner.mk_scalar_updt(r, info.m_size, offset, args[j]);
}
offset += info.m_size;
break;
}
j++;
i++;
}
m_replaced = true;
return r;
@ -575,98 +533,16 @@ class to_llnf_fn {
}
public:
replace_cnstr_fn(to_llnf_fn & owner, expr const & major, cnstr_info const & cinfo, buffer<bool> const & to_reset_fields):
m_owner(owner), m_major(major), m_cinfo(cinfo), m_to_reset_fields(to_reset_fields) {}
replace_cnstr_fn(to_llnf_fn & owner, expr const & major, cnstr_info const & cinfo):
m_owner(owner), m_major(major), m_cinfo(cinfo) {}
expr operator()(expr const & e) { return visit(e); }
};
/* Auxiliary methods used to implement `try_update_opt`. We say a field needs to be reset at the beginning of a major
premise if it is used in a non tail call.
We "reset" the field to create new opportunites for destructive updates.
For example, consider the following sequence of instructions in low-level normal form without `reset` operations.
```
map_add_1 :=
λ xs, @list.cases_on xs
_cnstr.0.0
(let _x_1 := _proj.0 xs,
_x_2 := _proj.1 xs,
_x_5 := nat.add _x_1 1,
_x_6 := map_add_1 _x_2,
_x_7 := _updt.0 xs _x_5
in _updt.1 _x_7 _x_6)
```
After the instruction `_x_2 := _proj.1 xs`, there are at least two references to the tail of `xs`: `_x_2` and the one
on `xs`. So, the recursive call `map_add_1 _x_2` will not be able to perform destructive updates.
Now consider the version that uses `reset` operations.
```
map_add_1 :=
λ xs, @list.cases_on xs
_cnstr.0.0
(let _x_1 := _proj.0 xs,
_x_2 := _proj.1 xs,
_x_3 := _reset.0 xs,
_x_4 := _reset.1 _x_3,
_x_5 := nat.add _x_1 1,
_x_6 := map_add_1 _x_2,
_x_7 := _updt.0 _x_4_x_5
in _updt.1 _x_7 _x_6)
```
The reset operations will decrease the reference counter of `xs` head and tail.
Note that the operation `_x_3 := _reset.0 xs` is wasteful since `nat.add` never performs destructive updates.
In the future, we may consider a better `mark_to_reset_fields` that avoids these unnecessary reset operations.
Remark: `reset` operations may also help to reduce memory contention.
*/
void mark_to_reset_fields(expr const & e0, buffer<expr> const & fields, buffer<bool> & result) {
buffer<pair<expr, bool>> todo;
todo.emplace_back(e0, true);
expr e; bool tail;
while (!todo.empty()) {
std::tie(e, tail) = todo.back();
todo.pop_back();
if (!has_fvar(e))
continue;
switch (e.kind()) {
case expr_kind::FVar:
if (!tail) {
for (unsigned i = 0; i < fields.size(); i++) {
if (is_fvar(fields[i]) && e == fields[i])
result[i] = true;
}
}
break;
case expr_kind::Let:
todo.emplace_back(let_body(e), tail);
todo.emplace_back(let_value(e), false);
break;
case expr_kind::Lambda:
todo.emplace_back(binding_body(e), tail);
break;
case expr_kind::Proj:
todo.emplace_back(proj_expr(e), tail);
break;
case expr_kind::App: {
buffer<expr> args;
expr const & fn = get_app_args(e, args);
todo.emplace_back(fn, tail);
for (expr const & arg : args)
todo.emplace_back(arg, tail);
break;
}
default:
break;
}
}
}
expr try_update_opt(expr const & minor, expr const & major, cnstr_info const & cinfo, buffer<expr> const & fields) {
expr try_update_opt(expr const & minor, expr const & major, cnstr_info const & cinfo) {
if (cinfo.m_num_objs == 0 && cinfo.m_scalar_sz == 0) return minor;
if (!is_fvar(major)) return minor;
if (has_fvar(minor, major)) return minor;
buffer<bool> to_reset_fields;
to_reset_fields.resize(fields.size(), false);
mark_to_reset_fields(minor, fields, to_reset_fields);
return replace_cnstr_fn(*this, major, cinfo, to_reset_fields)(minor);
return replace_cnstr_fn(*this, major, cinfo)(minor);
}
expr visit_cases(expr const & e) {
@ -724,7 +600,7 @@ class to_llnf_fn {
minor = binding_body(minor);
}
minor = instantiate_rev(minor, fields.size(), fields.data());
minor = try_update_opt(minor, major, cinfo, fields);
minor = try_update_opt(minor, major, cinfo);
minor = visit(minor);
if (!is_enf_unreachable(minor)) {
/* If `minor` is not the constructor `i`, then this "cases_on" application is not the identity. */
@ -869,9 +745,9 @@ class to_llnf_fn {
return visit_cases(e);
} else if (is_constructor_app(env(), e)) {
return visit_constructor(e);
} else if (is_updt_app(e)) {
} else if (is_updt_scalar_app(e)) {
return flat_app(e);
} else if (is_updt_cidx_app(e)) {
} else if (is_reuse_app(e)) {
return flat_app(e);
} else {
return visit_app_default(e);
@ -906,6 +782,7 @@ expr to_llnf(environment const & env, expr const & e, bool unboxed) {
void initialize_llnf() {
g_cnstr = new name("_cnstr");
g_reuse = new name("_reuse");
g_reset = new name("_reset");
g_updt = new name("_updt");
g_updt_cidx = new name("_updt_cidx");
@ -927,6 +804,7 @@ void initialize_llnf() {
void finalize_llnf() {
delete g_cnstr;
delete g_reuse;
delete g_reset;
delete g_updt;
delete g_updt_u8;

8
src/library/compiler/llnf.h
View file

@ -13,16 +13,14 @@ namespace lean {
expr to_llnf(environment const & env, expr const & e, bool unboxed_data = false);
bool is_llnf_cnstr(expr const & e, unsigned & cidx, unsigned & ssz);
bool is_llnf_reset(expr const & e, unsigned & i);
bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & ssz);
bool is_llnf_reset(expr const & e, unsigned & n);
bool is_llnf_proj(expr const & e, unsigned & idx);
bool is_llnf_updt(expr const & e, unsigned & i);
bool is_llnf_updt_cidx(expr const & e, unsigned & cidx);
inline bool is_llnf_cnstr(expr const & e) { unsigned d1, d2; return is_llnf_cnstr(e, d1, d2); }
inline bool is_llnf_reuse(expr const & e) { unsigned d1, d2; return is_llnf_reuse(e, d1, d2); }
inline bool is_llnf_reset(expr const & e) { unsigned i; return is_llnf_reset(e, i); }
inline bool is_llnf_proj(expr const & e) { unsigned d; return is_llnf_proj(e, d); }
inline bool is_llnf_updt(expr const & e) { unsigned i; return is_llnf_updt(e, i); }
inline bool is_llnf_updt_cidx(expr const & e) { unsigned i; return is_llnf_updt_cidx(e, i); }
void initialize_llnf();
void finalize_llnf();

2
src/library/vm/optimize.cpp
View file

@ -102,7 +102,7 @@ class live_vars_fn {
case opcode::Proj: case opcode::Apply: case opcode::InvokeGlobal:
case opcode::InvokeBuiltin: case opcode::InvokeCFun:
case opcode::Closure: case opcode::Expr: case opcode::LocalInfo:
case opcode::Reset: case opcode::Updt: case opcode::UpdtCidx:
case opcode::Reset: case opcode::Reuse:
s = collect(pc+1);
break;
case opcode::Push: case opcode::Move:

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

@ -525,14 +525,13 @@ void vm_instr::display(std::ostream & out) const {
switch (m_op) {
case opcode::Push: out << "push " << m_idx; break;
case opcode::Move: out << "move " << m_idx; break;
case opcode::Reset: out << "reset " << m_idx; break;
case opcode::Updt: out << "updt " << m_idx; break;
case opcode::UpdtCidx: out << "updt_cidx " << m_idx; break;
case opcode::Reset: out << "reset " << m_num; break;
case opcode::Ret: out << "ret"; break;
case opcode::Drop: out << "drop " << m_num; break;
case opcode::Goto: out << "goto " << m_pc[0]; break;
case opcode::SConstructor: out << "scnstr #" << m_cidx; break;
case opcode::Constructor: out << "cnstr #" << m_cidx << " " << m_nfields; break;
case opcode::Reuse: out << "reuse #" << m_cidx << " " << m_nfields; break;
case opcode::Num: out << "num " << *m_mpz; break;
case opcode::String: out << "str_lit \"" << *m_str << "\""; break;
case opcode::Unreachable: out << "unreachable"; break;
@ -621,21 +620,9 @@ vm_instr mk_move_instr(unsigned idx) {
return r;
};
vm_instr mk_reset_instr(unsigned idx) {
vm_instr mk_reset_instr(unsigned n) {
vm_instr r(opcode::Reset);
r.m_idx = idx;
return r;
};
vm_instr mk_updt_instr(unsigned idx) {
vm_instr r(opcode::Updt);
r.m_idx = idx;
return r;
};
vm_instr mk_updt_cidx_instr(unsigned idx) {
vm_instr r(opcode::UpdtCidx);
r.m_idx = idx;
r.m_num = n;
return r;
};
@ -670,6 +657,13 @@ vm_instr mk_constructor_instr(unsigned cidx, unsigned nfields) {
return r;
}
vm_instr mk_reuse_instr(unsigned cidx, unsigned nfields) {
vm_instr r(opcode::Reuse);
r.m_cidx = cidx;
r.m_nfields = nfields;
return r;
}
vm_instr mk_num_instr(mpz const & v) {
if (v < LEAN_VM_MAX_SMALL_NAT) {
vm_instr r(opcode::SConstructor);
@ -781,10 +775,9 @@ void vm_instr::copy_args(vm_instr const & i) {
m_nargs = i.m_nargs;
break;
case opcode::Push: case opcode::Move: case opcode::Proj:
case opcode::Reset: case opcode::Updt: case opcode::UpdtCidx:
m_idx = i.m_idx;
break;
case opcode::Drop:
case opcode::Drop: case opcode::Reset:
m_num = i.m_num;
break;
case opcode::Goto:
@ -802,7 +795,7 @@ void vm_instr::copy_args(vm_instr const & i) {
case opcode::SConstructor:
m_cidx = i.m_cidx;
break;
case opcode::Constructor:
case opcode::Constructor: case opcode::Reuse:
m_cidx = i.m_cidx;
m_nfields = i.m_nfields;
break;
@ -895,10 +888,9 @@ void vm_instr::serialize(serializer & s, std::function<name(unsigned)> const & i
s << idx2name(m_fn_idx) << m_nargs;
break;
case opcode::Push: case opcode::Move: case opcode::Proj:
case opcode::Reset: case opcode::Updt: case opcode::UpdtCidx:
s << m_idx;
break;
case opcode::Drop:
case opcode::Drop: case opcode::Reset:
s << m_num;
break;
case opcode::Goto:
@ -916,7 +908,7 @@ void vm_instr::serialize(serializer & s, std::function<name(unsigned)> const & i
case opcode::SConstructor:
s << m_cidx;
break;
case opcode::Constructor:
case opcode::Constructor: case opcode::Reuse:
s << m_cidx << m_nfields;
break;
case opcode::Num:
@ -968,10 +960,6 @@ static vm_instr read_vm_instr(deserializer & d) {
return mk_move_instr(d.read_unsigned());
case opcode::Reset:
return mk_reset_instr(d.read_unsigned());
case opcode::Updt:
return mk_updt_instr(d.read_unsigned());
case opcode::UpdtCidx:
return mk_updt_cidx_instr(d.read_unsigned());
case opcode::Proj:
return mk_proj_instr(d.read_unsigned());
case opcode::Drop:
@ -991,6 +979,9 @@ static vm_instr read_vm_instr(deserializer & d) {
case opcode::Constructor:
idx = d.read_unsigned();
return mk_constructor_instr(idx, d.read_unsigned());
case opcode::Reuse:
idx = d.read_unsigned();
return mk_reuse_instr(idx, d.read_unsigned());
case opcode::Num:
return mk_num_instr(d.read_mpz());
case opcode::String:
@ -2848,54 +2839,22 @@ void vm_state::run() {
goto main_loop;
}
case opcode::Reset: {
/* Instruction: reset idx
/* Instruction: reset n
stack before, after
... ...
s s' (s.idx := ())
s s'
*/
unsigned idx = instr.get_idx();
unsigned n = instr.get_num();
vm_obj & s = m_stack.back();
if (s.raw()->get_rc() > 1) {
s = mk_vm_constructor(cidx(s), csize(s), cfields(s));
s = mk_vm_simple(0);
} else {
vm_obj * fields = const_cast<vm_obj*>(to_composite(s)->fields());
for (unsigned i = 0; i < n; i++) {
fields[i] = mk_vm_simple(0);
}
}
const_cast<vm_obj*>(to_composite(s)->fields())[idx] = mk_vm_simple(0);
m_pc++;
goto main_loop;
}
case opcode::Updt: {
/* Instruction: updt idx
stack before, after
... ...
s s' (s.idx := v)
v ==>
*/
unsigned idx = instr.get_idx();
unsigned sz = m_stack.size();
vm_obj & s = m_stack[sz-2];
vm_obj & v = m_stack[sz-1];
if (s.raw()->get_rc() > 1) {
s = mk_vm_constructor(cidx(s), csize(s), cfields(s));
}
std::swap(const_cast<vm_obj*>(to_composite(s)->fields())[idx], v);
m_stack.pop_back();
m_pc++;
goto main_loop;
}
case opcode::UpdtCidx: {
/* Instruction: updt_cidx cidx
stack before, after
... ...
s ==> s' (s.cidx := cidx)
*/
unsigned idx = instr.get_idx();
vm_obj & s = m_stack.back();
if (s.raw()->get_rc() > 1) {
s = mk_vm_constructor(cidx(s), csize(s), cfields(s));
}
const_cast<vm_composite*>(to_composite(s))->m_idx = idx;
m_pc++;
goto main_loop;
}
@ -2933,7 +2892,37 @@ void vm_state::run() {
vm_obj new_value = mk_vm_constructor(instr.get_cidx(), nfields, m_stack.data() + sz - nfields);
m_stack.resize(sz - nfields + 1);
swap(m_stack.back(), new_value);
if (m_debugging) shrink_stack_info();
m_pc++;
goto main_loop;
}
case opcode::Reuse: {
/** Instruction: reuse i n
stack before, after
... ...
v ==> v
cell (#i a_1 ... a_n)
a_1
...
a_n
*/
unsigned nfields = instr.get_nfields();
unsigned sz = m_stack.size();
lean_vm_check(nfields + 1 <= sz);
vm_obj & cell = m_stack[sz - nfields - 1];
vm_obj * src = m_stack.data() + sz - nfields;
if (is_simple(cell)) {
vm_obj new_value = mk_vm_constructor(instr.get_cidx(), nfields, src);
m_stack.resize(sz - nfields);
swap(m_stack.back(), new_value);
} else {
const_cast<vm_composite*>(to_composite(cell))->m_idx = instr.get_cidx();
vm_obj * fields = const_cast<vm_obj*>(to_composite(cell)->fields());
for (unsigned i = 0; i < nfields; i++) {
swap(fields[i], src[i]);
}
m_stack.resize(sz - nfields);
}
m_pc++;
goto main_loop;
}

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

@ -315,7 +315,7 @@ enum class opcode {
Cases2, CasesN, Proj,
Apply, InvokeGlobal, InvokeBuiltin, InvokeCFun,
Closure, Unreachable, Expr, LocalInfo,
Reset, Updt, UpdtCidx
Reset, Reuse
};
/** \brief VM instructions */
@ -326,9 +326,9 @@ class vm_instr {
unsigned m_fn_idx; /* InvokeGlobal, InvokeBuiltin, InvokeCFun and Closure. */
unsigned m_nargs; /* Closure */
};
/* Push, Move, Proj, Reset, Updt, UpdtCidx */
/* Push, Move, Proj */
unsigned m_idx;
/* Drop */
/* Drop, Reset */
unsigned m_num;
/* Goto and Cases2 */
struct {
@ -338,10 +338,10 @@ class vm_instr {
struct {
unsigned * m_npcs;
};
/* Constructor, SConstructor */
/* Constructor, SConstructor, Reuse */
struct {
unsigned m_cidx;
unsigned m_nfields; /* only used by Constructor */
unsigned m_nfields; /* only used by Constructor and Reuse */
};
/* Num */
mpz * m_mpz;
@ -363,6 +363,7 @@ class vm_instr {
friend vm_instr mk_goto_instr(unsigned pc);
friend vm_instr mk_sconstructor_instr(unsigned cidx);
friend vm_instr mk_constructor_instr(unsigned cidx, unsigned nfields);
friend vm_instr mk_reuse_instr(unsigned cidx, unsigned nfields);
friend vm_instr mk_num_instr(mpz const & v);
friend vm_instr mk_string_instr(std::string const & v);
friend vm_instr mk_ret_instr();
@ -376,9 +377,7 @@ class vm_instr {
friend vm_instr mk_closure_instr(unsigned fn_idx, unsigned n);
friend vm_instr mk_expr_instr(expr const &e);
friend vm_instr mk_local_info_instr(unsigned idx, name const & n, optional<expr> const & e);
friend vm_instr mk_updt_instr(unsigned idx);
friend vm_instr mk_reset_instr(unsigned idx);
friend vm_instr mk_updt_cidx_instr(unsigned cidx);
friend vm_instr mk_reset_instr(unsigned n);
void release_memory();
void copy_args(vm_instr const & i);
@ -406,13 +405,12 @@ public:
}
unsigned get_idx() const {
lean_assert(m_op == opcode::Push || m_op == opcode::Move || m_op == opcode::Proj ||
m_op == opcode::Reset || m_op == opcode::Updt || m_op == opcode::UpdtCidx);
lean_assert(m_op == opcode::Push || m_op == opcode::Move || m_op == opcode::Proj);
return m_idx;
}
unsigned get_num() const {
lean_assert(m_op == opcode::Drop);
lean_assert(m_op == opcode::Drop || m_op == opcode::Reset);
return m_num;
}
@ -456,12 +454,12 @@ public:
}
unsigned get_cidx() const {
lean_assert(m_op == opcode::Constructor || m_op == opcode::SConstructor);
lean_assert(m_op == opcode::Constructor || m_op == opcode::SConstructor || m_op == opcode::Reuse);
return m_cidx;
}
unsigned get_nfields() const {
lean_assert(m_op == opcode::Constructor);
lean_assert(m_op == opcode::Constructor || m_op == opcode::Reuse);
return m_nfields;
}
@ -506,6 +504,7 @@ vm_instr mk_proj_instr(unsigned n);
vm_instr mk_goto_instr(unsigned pc);
vm_instr mk_sconstructor_instr(unsigned cidx);
vm_instr mk_constructor_instr(unsigned cidx, unsigned nfields);
vm_instr mk_reuse_instr(unsigned cidx, unsigned nfields);
vm_instr mk_num_instr(mpz const & v);
vm_instr mk_string_instr(std::string const & v);
vm_instr mk_ret_instr();
@ -519,9 +518,7 @@ vm_instr mk_invoke_builtin_instr(unsigned fn_idx);
vm_instr mk_closure_instr(unsigned fn_idx, unsigned n);
vm_instr mk_expr_instr(expr const &e);
vm_instr mk_local_info_instr(unsigned idx, name const & n, optional<expr> const & e);
vm_instr mk_reset_instr(unsigned idx);
vm_instr mk_updt_instr(unsigned idx);
vm_instr mk_updt_cidx_instr(unsigned cidx);
vm_instr mk_reset_instr(unsigned n);
class vm_state;
class vm_instr;