feat(library): add VM objects and instructions
This commit is contained in:
Leonardo de Moura
parent
6cb8e82fef
commit
2daf9c8d59
3 changed files with 580 additions and 1 deletions
|
|
@ -14,7 +14,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
|
|||
abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp
|
||||
attribute_manager.cpp error_handling.cpp unification_hint.cpp defeq_simp_lemmas.cpp
|
||||
defeq_simplifier.cpp proof_irrel_expr_manager.cpp
|
||||
local_context.cpp metavar_context.cpp type_context.cpp
|
||||
local_context.cpp metavar_context.cpp type_context.cpp vm.cpp
|
||||
# Legacy -- The following files will be eventually deleted
|
||||
normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp
|
||||
unifier.cpp match.cpp class_instance_resolution.cpp old_type_context.cpp
|
||||
|
|
|
|||
299
src/library/vm.cpp
Normal file
299
src/library/vm.cpp
Normal file
|
|
@ -0,0 +1,299 @@
|
|||
/*
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "library/vm.h"
|
||||
|
||||
namespace lean {
|
||||
void vm_obj_cell::dec_ref(vm_obj & o, buffer<vm_obj_cell*> & todelete) {
|
||||
if (LEAN_VM_IS_PTR(o.m_data)) {
|
||||
vm_obj_cell * c = o.steal_ptr();
|
||||
if (c->dec_ref_core())
|
||||
todelete.push_back(c);
|
||||
}
|
||||
}
|
||||
|
||||
DEF_THREAD_MEMORY_POOL(get_vm_composite_allocator_1, sizeof(vm_composite) + sizeof(vm_obj));
|
||||
DEF_THREAD_MEMORY_POOL(get_vm_composite_allocator_2, sizeof(vm_composite) + 2*sizeof(vm_obj));
|
||||
DEF_THREAD_MEMORY_POOL(get_vm_composite_allocator_3, sizeof(vm_composite) + 3*sizeof(vm_obj));
|
||||
DEF_THREAD_MEMORY_POOL(get_vm_composite_allocator_4, sizeof(vm_composite) + 4*sizeof(vm_obj));
|
||||
DEF_THREAD_MEMORY_POOL(get_vm_composite_allocator_5, sizeof(vm_composite) + 5*sizeof(vm_obj));
|
||||
DEF_THREAD_MEMORY_POOL(get_vm_composite_allocator_6, sizeof(vm_composite) + 6*sizeof(vm_obj));
|
||||
DEF_THREAD_MEMORY_POOL(get_vm_composite_allocator_7, sizeof(vm_composite) + 7*sizeof(vm_obj));
|
||||
DEF_THREAD_MEMORY_POOL(get_vm_composite_allocator_8, sizeof(vm_composite) + 8*sizeof(vm_obj));
|
||||
|
||||
vm_composite::vm_composite(vm_obj_kind k, unsigned idx, unsigned sz, vm_obj const * data):
|
||||
vm_obj_cell(k), m_idx(idx), m_size(sz) {
|
||||
vm_obj * fields = get_field_ptr();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
fields[i] = data[i];
|
||||
}
|
||||
|
||||
static vm_obj mk_vm_composite(vm_obj_kind k, unsigned idx, unsigned sz, vm_obj const * data) {
|
||||
lean_assert(k == vm_obj_kind::Constructor || k == vm_obj_kind::Closure);
|
||||
switch (sz) {
|
||||
case 1: return vm_obj(new (get_vm_composite_allocator_1().allocate()) vm_composite(k, idx, sz, data));
|
||||
case 2: return vm_obj(new (get_vm_composite_allocator_2().allocate()) vm_composite(k, idx, sz, data));
|
||||
case 3: return vm_obj(new (get_vm_composite_allocator_3().allocate()) vm_composite(k, idx, sz, data));
|
||||
case 4: return vm_obj(new (get_vm_composite_allocator_4().allocate()) vm_composite(k, idx, sz, data));
|
||||
case 5: return vm_obj(new (get_vm_composite_allocator_5().allocate()) vm_composite(k, idx, sz, data));
|
||||
case 6: return vm_obj(new (get_vm_composite_allocator_6().allocate()) vm_composite(k, idx, sz, data));
|
||||
case 7: return vm_obj(new (get_vm_composite_allocator_7().allocate()) vm_composite(k, idx, sz, data));
|
||||
case 8: return vm_obj(new (get_vm_composite_allocator_8().allocate()) vm_composite(k, idx, sz, data));
|
||||
default:
|
||||
char * mem = new char[sizeof(vm_composite) + sz * sizeof(vm_obj)];
|
||||
return vm_obj(new (mem) vm_composite(k, idx, sz, data));
|
||||
}
|
||||
}
|
||||
|
||||
void vm_composite::dealloc(buffer<vm_obj_cell*> & todelete) {
|
||||
unsigned sz = m_size;
|
||||
vm_obj * fields = get_field_ptr();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
dec_ref(fields[i], todelete);
|
||||
}
|
||||
this->~vm_composite();
|
||||
switch (sz) {
|
||||
case 1: get_vm_composite_allocator_1().recycle(this); break;
|
||||
case 2: get_vm_composite_allocator_2().recycle(this); break;
|
||||
case 3: get_vm_composite_allocator_3().recycle(this); break;
|
||||
case 4: get_vm_composite_allocator_4().recycle(this); break;
|
||||
case 5: get_vm_composite_allocator_5().recycle(this); break;
|
||||
case 6: get_vm_composite_allocator_6().recycle(this); break;
|
||||
case 7: get_vm_composite_allocator_7().recycle(this); break;
|
||||
case 8: get_vm_composite_allocator_8().recycle(this); break;
|
||||
default: delete[] reinterpret_cast<char*>(this); break;
|
||||
}
|
||||
}
|
||||
|
||||
vm_obj mk_vm_constructor(unsigned cidx, unsigned sz, vm_obj const * data) {
|
||||
return mk_vm_composite(vm_obj_kind::Constructor, cidx, sz, data);
|
||||
}
|
||||
|
||||
vm_obj mk_vm_closure(unsigned fn_idx, unsigned sz, vm_obj const * data) {
|
||||
return mk_vm_composite(vm_obj_kind::Closure, fn_idx, sz, data);
|
||||
}
|
||||
|
||||
DEF_THREAD_MEMORY_POOL(get_vm_mpz_allocator, sizeof(vm_mpz));
|
||||
|
||||
vm_mpz::vm_mpz(mpz const & v):
|
||||
vm_obj_cell(vm_obj_kind::MPZ),
|
||||
m_value(v) {
|
||||
}
|
||||
|
||||
vm_obj mk_vm_mpz(mpz const & v) {
|
||||
return vm_obj(new (get_vm_mpz_allocator().allocate()) vm_mpz(v));
|
||||
}
|
||||
|
||||
void vm_mpz::dealloc() {
|
||||
this->~vm_mpz();
|
||||
get_vm_mpz_allocator().recycle(this);
|
||||
}
|
||||
|
||||
vm_obj mk_vm_external(vm_external * cell) {
|
||||
lean_assert(cell);
|
||||
lean_assert(cell->get_rc() == 0);
|
||||
return vm_obj(cell);
|
||||
}
|
||||
|
||||
void vm_obj_cell::dealloc() {
|
||||
try {
|
||||
buffer<vm_obj_cell*> todo;
|
||||
todo.push_back(this);
|
||||
while (!todo.empty()) {
|
||||
vm_obj_cell * it = todo.back();
|
||||
todo.pop_back();
|
||||
lean_assert(it->get_rc() == 0);
|
||||
switch (it->kind()) {
|
||||
case vm_obj_kind::Simple: lean_unreachable();
|
||||
case vm_obj_kind::Constructor: to_composite(it)->dealloc(todo); break;
|
||||
case vm_obj_kind::Closure: to_composite(it)->dealloc(todo); break;
|
||||
case vm_obj_kind::MPZ: to_mpz_core(it)->dealloc(); break;
|
||||
case vm_obj_kind::External: delete to_external(it); break;
|
||||
}
|
||||
}
|
||||
} catch (std::bad_alloc&) {
|
||||
// We need this catch, because push_back may fail when expanding the buffer.
|
||||
// In this case, we avoid the crash, and "accept" the memory leak.
|
||||
}
|
||||
}
|
||||
|
||||
vm_instr mk_push_instr(unsigned idx) {
|
||||
vm_instr r(opcode::Push);
|
||||
r.m_idx = idx;
|
||||
return r;
|
||||
};
|
||||
|
||||
vm_instr mk_drop_instr(unsigned n) {
|
||||
vm_instr r(opcode::Drop);
|
||||
r.m_num = n;
|
||||
return r;
|
||||
}
|
||||
|
||||
vm_instr mk_goto_instr(unsigned pc) {
|
||||
vm_instr r(opcode::Goto);
|
||||
r.m_pc = pc;
|
||||
return r;
|
||||
}
|
||||
|
||||
vm_instr mk_sconstructor_instr(unsigned cidx) {
|
||||
vm_instr r(opcode::SConstructor);
|
||||
r.m_cidx = cidx;
|
||||
return r;
|
||||
}
|
||||
|
||||
vm_instr mk_constructor_instr(unsigned cidx, unsigned nfields) {
|
||||
vm_instr r(opcode::Constructor);
|
||||
r.m_cidx = cidx;
|
||||
r.m_nfields = nfields;
|
||||
return r;
|
||||
}
|
||||
|
||||
vm_instr mk_num_instr(mpz const & v) {
|
||||
vm_instr r(opcode::Num);
|
||||
r.m_mpz = new mpz(v);
|
||||
return r;
|
||||
}
|
||||
|
||||
vm_instr mk_ret_instr() { return vm_instr(opcode::Ret); }
|
||||
|
||||
vm_instr mk_cases1_instr() { return vm_instr(opcode::Cases1); }
|
||||
|
||||
vm_instr mk_nat_cases_instr(unsigned pc) {
|
||||
vm_instr r(opcode::NatCases);
|
||||
r.m_pc = pc;
|
||||
return r;
|
||||
}
|
||||
|
||||
vm_instr mk_cases2_instr(unsigned pc) {
|
||||
vm_instr r(opcode::Cases2);
|
||||
r.m_pc = pc;
|
||||
return r;
|
||||
}
|
||||
|
||||
vm_instr mk_casesn_instr(unsigned num_pc, unsigned const * pcs) {
|
||||
lean_assert(num_pc >= 2);
|
||||
vm_instr r(opcode::CasesN);
|
||||
r.m_npcs = new unsigned[num_pc + 1];
|
||||
r.m_npcs[0] = num_pc;
|
||||
for (unsigned i = 0; i < num_pc; i++)
|
||||
r.m_npcs[i+1] = pcs[i];
|
||||
return r;
|
||||
}
|
||||
|
||||
vm_instr mk_invoke_instr(unsigned n) {
|
||||
vm_instr r(opcode::Invoke);
|
||||
r.m_num = n;
|
||||
return r;
|
||||
}
|
||||
|
||||
vm_instr mk_invoke_global_instr(unsigned fn_idx, unsigned n) {
|
||||
vm_instr r(opcode::InvokeGlobal);
|
||||
r.m_fn_idx = fn_idx;
|
||||
r.m_nargs = n;
|
||||
return r;
|
||||
}
|
||||
|
||||
vm_instr mk_closure_instr(unsigned fn_idx, unsigned n) {
|
||||
vm_instr r(opcode::Closure);
|
||||
r.m_fn_idx = fn_idx;
|
||||
r.m_nargs = n;
|
||||
return r;
|
||||
}
|
||||
|
||||
void vm_instr::copy_args(vm_instr const & i) {
|
||||
switch (i.m_op) {
|
||||
case opcode::InvokeGlobal: case opcode::Closure:
|
||||
m_fn_idx = i.m_fn_idx;
|
||||
m_nargs = i.m_nargs;
|
||||
break;
|
||||
case opcode::Push:
|
||||
m_idx = i.m_idx;
|
||||
break;
|
||||
case opcode::Invoke: case opcode::Drop:
|
||||
m_num = i.m_num;
|
||||
break;
|
||||
case opcode::Goto: case opcode::Cases2: case opcode::NatCases:
|
||||
m_pc = i.m_pc;
|
||||
break;
|
||||
case opcode::CasesN:
|
||||
m_npcs = new unsigned[i.m_npcs[0] + 1];
|
||||
for (unsigned j = 0; j < m_npcs[0] + 1; j++)
|
||||
m_npcs[j] = i.m_npcs[j];
|
||||
break;
|
||||
case opcode::SConstructor:
|
||||
m_cidx = i.m_cidx;
|
||||
break;
|
||||
case opcode::Constructor:
|
||||
m_cidx = i.m_cidx;
|
||||
m_nfields = i.m_nfields;
|
||||
break;
|
||||
case opcode::Num:
|
||||
m_mpz = new mpz(*i.m_mpz);
|
||||
break;
|
||||
case opcode::Ret: case opcode::Cases1:
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
vm_instr::vm_instr(vm_instr const & i):
|
||||
m_op(i.m_op) {
|
||||
copy_args(i);
|
||||
}
|
||||
|
||||
vm_instr::vm_instr(vm_instr && i):
|
||||
m_op(i.m_op) {
|
||||
switch (m_op) {
|
||||
case opcode::Num:
|
||||
m_mpz = i.m_mpz;
|
||||
i.m_mpz = nullptr;
|
||||
break;
|
||||
case opcode::CasesN:
|
||||
m_npcs = i.m_npcs;
|
||||
i.m_npcs = nullptr;
|
||||
break;
|
||||
default:
|
||||
copy_args(i);
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
vm_instr::~vm_instr() {
|
||||
switch (m_op) {
|
||||
case opcode::Num:
|
||||
delete m_mpz;
|
||||
break;
|
||||
case opcode::CasesN:
|
||||
delete[] m_npcs;
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
vm_instr & vm_instr::operator=(vm_instr const & s) {
|
||||
m_op = s.m_op;
|
||||
copy_args(s);
|
||||
return *this;
|
||||
}
|
||||
|
||||
vm_instr & vm_instr::operator=(vm_instr && s) {
|
||||
m_op = s.m_op;
|
||||
switch (m_op) {
|
||||
case opcode::Num:
|
||||
m_mpz = s.m_mpz;
|
||||
s.m_mpz = nullptr;
|
||||
break;
|
||||
case opcode::CasesN:
|
||||
m_npcs = s.m_npcs;
|
||||
s.m_npcs = nullptr;
|
||||
break;
|
||||
default:
|
||||
copy_args(s);
|
||||
break;
|
||||
}
|
||||
return *this;
|
||||
}
|
||||
}
|
||||
280
src/library/vm.h
Normal file
280
src/library/vm.h
Normal file
|
|
@ -0,0 +1,280 @@
|
|||
/*
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <memory>
|
||||
#include "util/debug.h"
|
||||
#include "util/rc.h"
|
||||
#include "util/numerics/mpz.h"
|
||||
#include "kernel/environment.h"
|
||||
|
||||
namespace lean {
|
||||
class vm_obj;
|
||||
enum class vm_obj_kind { Simple, Constructor, Closure, MPZ, External };
|
||||
|
||||
/** \brief Base class for VM objects.
|
||||
|
||||
\remark Simple objects are encoded as tagged pointers. */
|
||||
class vm_obj_cell {
|
||||
protected:
|
||||
MK_LEAN_RC(); // Declare m_rc counter
|
||||
vm_obj_kind m_kind;
|
||||
void dealloc();
|
||||
void dec_ref(vm_obj & o, buffer<vm_obj_cell*> & todelete);
|
||||
vm_obj_cell(vm_obj_kind k):m_rc(0), m_kind(k) {}
|
||||
public:
|
||||
vm_obj_kind kind() const { return m_kind; }
|
||||
};
|
||||
|
||||
#define LEAN_VM_IS_PTR(obj) ((reinterpret_cast<size_t>(obj) & 1) == 0)
|
||||
#define LEAN_VM_BOX(num) (reinterpret_cast<vm_obj_cell*>((num << 1) | 1))
|
||||
#define LEAN_VM_UNBOX(obj) (reinterpret_cast<size_t>(obj) >> 1)
|
||||
|
||||
/** \brief VM object */
|
||||
class vm_obj {
|
||||
vm_obj_cell * m_data;
|
||||
friend class vm_obj_cell;
|
||||
vm_obj_cell * steal_ptr() {
|
||||
lean_assert(LEAN_VM_IS_PTR(m_data)); vm_obj_cell * r = m_data; m_data = LEAN_VM_BOX(0); return r;
|
||||
}
|
||||
public:
|
||||
vm_obj():m_data(LEAN_VM_BOX(0)) {
|
||||
static_assert(sizeof(vm_obj) == sizeof(void *), "unexpected class obj size"); // NOLINT
|
||||
}
|
||||
vm_obj(unsigned cidx):m_data(LEAN_VM_BOX(cidx)) {}
|
||||
vm_obj(vm_obj_cell * c):m_data(c) { m_data->inc_ref(); }
|
||||
vm_obj(vm_obj const & o):m_data(o.m_data) { if (LEAN_VM_IS_PTR(m_data)) m_data->inc_ref(); }
|
||||
vm_obj(vm_obj && o):m_data(o.m_data) { o.m_data = LEAN_VM_BOX(0); }
|
||||
~vm_obj() { if (LEAN_VM_IS_PTR(m_data)) m_data->dec_ref(); }
|
||||
|
||||
vm_obj & operator=(vm_obj const & s) {
|
||||
if (LEAN_VM_IS_PTR(s.m_data))
|
||||
s.m_data->inc_ref();
|
||||
auto new_data = s.m_data;
|
||||
if (LEAN_VM_IS_PTR(m_data))
|
||||
m_data->dec_ref();
|
||||
m_data = new_data;
|
||||
return *this;
|
||||
}
|
||||
|
||||
vm_obj & operator=(vm_obj && s) {
|
||||
if (LEAN_VM_IS_PTR(m_data))
|
||||
m_data->dec_ref();
|
||||
m_data = s.m_data;
|
||||
s.m_data = LEAN_VM_BOX(0);
|
||||
return *this;
|
||||
}
|
||||
|
||||
vm_obj_kind kind() const {
|
||||
return LEAN_VM_IS_PTR(m_data) ? m_data->kind() : vm_obj_kind::Simple;
|
||||
}
|
||||
|
||||
vm_obj_cell * raw() const {
|
||||
lean_assert(LEAN_VM_IS_PTR(m_data));
|
||||
return m_data;
|
||||
}
|
||||
};
|
||||
|
||||
class vm_composite : public vm_obj_cell {
|
||||
unsigned m_idx;
|
||||
unsigned m_size;
|
||||
vm_obj * get_field_ptr() {
|
||||
return reinterpret_cast<vm_obj *>(reinterpret_cast<char *>(this)+sizeof(vm_composite));
|
||||
}
|
||||
friend vm_obj_cell;
|
||||
void dealloc(buffer<vm_obj_cell*> & todelete);
|
||||
public:
|
||||
vm_composite(vm_obj_kind k, unsigned idx, unsigned sz, vm_obj const * data);
|
||||
unsigned size() const { return m_size; }
|
||||
unsigned idx() const { return m_idx; }
|
||||
vm_obj const * fields() const {
|
||||
return reinterpret_cast<vm_obj const *>(reinterpret_cast<char const *>(this)+sizeof(vm_composite));
|
||||
}
|
||||
};
|
||||
|
||||
class vm_mpz : public vm_obj_cell {
|
||||
mpz m_value;
|
||||
friend vm_obj_cell;
|
||||
void dealloc();
|
||||
public:
|
||||
vm_mpz(mpz const & v);
|
||||
mpz const & get_value() const { return m_value; }
|
||||
};
|
||||
|
||||
class vm_external : public vm_obj_cell {
|
||||
public:
|
||||
virtual ~vm_external() = 0;
|
||||
};
|
||||
|
||||
// =======================================
|
||||
// Constructors
|
||||
vm_obj mk_vm_simple(unsigned cidx);
|
||||
vm_obj mk_vm_constructor(unsigned cidx, unsigned sz, vm_obj const * args);
|
||||
vm_obj mk_vm_closure(unsigned fnidx, unsigned sz, vm_obj const * args);
|
||||
vm_obj mk_vm_mpz(mpz const & n);
|
||||
vm_obj mk_vm_external(vm_external * cell);
|
||||
/* helper functions for creating natural numbers */
|
||||
vm_obj mk_vm_nat(unsigned n);
|
||||
vm_obj mk_vm_nat(mpz const & n);
|
||||
// =======================================
|
||||
|
||||
// =======================================
|
||||
// Testers
|
||||
inline vm_obj_kind kind(vm_obj const & o) { return o.kind(); }
|
||||
inline bool is_simple(vm_obj const & o) { return !LEAN_VM_IS_PTR(o.raw()); }
|
||||
inline bool is_constructor(vm_obj const & o) { return kind(o) == vm_obj_kind::Constructor; }
|
||||
inline bool is_closure(vm_obj const & o) { return kind(o) == vm_obj_kind::Closure; }
|
||||
inline bool is_composite(vm_obj const & o) { return is_constructor(o) || is_closure(o); }
|
||||
inline bool is_mpz(vm_obj const & o) { return kind(o) == vm_obj_kind::MPZ; }
|
||||
inline bool is_external(vm_obj const & o) { return kind(o) == vm_obj_kind::External; }
|
||||
bool is_small_nat(vm_obj const & o);
|
||||
// =======================================
|
||||
|
||||
// =======================================
|
||||
// Casting
|
||||
inline vm_composite * to_composite(vm_obj const & o) {
|
||||
lean_assert(is_composite(o)); return static_cast<vm_composite*>(o.raw());
|
||||
}
|
||||
inline vm_mpz * to_mpz_core(vm_obj const & o) { lean_assert(is_mpz(o)); return static_cast<vm_mpz*>(o.raw()); }
|
||||
inline mpz const & to_mpz(vm_obj const & o) { return to_mpz_core(o)->get_value(); }
|
||||
inline vm_external * to_external(vm_obj const & o) { lean_assert(is_external(o)); return static_cast<vm_external*>(o.raw()); }
|
||||
// =======================================
|
||||
|
||||
// =======================================
|
||||
// Accessors
|
||||
inline unsigned cidx(vm_obj const & o) {
|
||||
lean_assert(is_simple(o) || is_constructor(o));
|
||||
return LEAN_VM_IS_PTR(o.raw()) ? to_composite(o.raw())->idx() : static_cast<unsigned>(LEAN_VM_UNBOX(o.raw()));
|
||||
}
|
||||
inline unsigned csize(vm_obj const & o) { lean_assert(is_composite(o)); return to_composite(o)->size(); }
|
||||
inline unsigned cfn_idx(vm_obj const & o) { lean_assert(is_closure(o)); return to_composite(o)->idx(); }
|
||||
inline vm_obj const * cfields(vm_obj const & o) {
|
||||
lean_assert(is_composite(o)); return to_composite(o)->fields();
|
||||
}
|
||||
inline vm_obj const & cfield(vm_obj const & o, unsigned i) { lean_assert(i < csize(o)); return cfields(o)[i]; }
|
||||
// =======================================
|
||||
|
||||
/** \brief VM instruction opcode */
|
||||
enum class opcode {
|
||||
Push, Ret, Drop, Goto,
|
||||
SConstructor, Constructor, Num,
|
||||
Cases1, Cases2, CasesN, NatCases,
|
||||
Invoke, InvokeGlobal, Closure
|
||||
};
|
||||
|
||||
/** \brief VM instructions */
|
||||
class vm_instr {
|
||||
opcode m_op;
|
||||
union {
|
||||
/* InvokeGlobal and Closure */
|
||||
struct {
|
||||
unsigned m_fn_idx;
|
||||
unsigned m_nargs;
|
||||
};
|
||||
/* Push */
|
||||
unsigned m_idx;
|
||||
/* Invoke, Drop */
|
||||
unsigned m_num;
|
||||
/* Goto, Cases2 and NatCases */
|
||||
unsigned m_pc;
|
||||
/* CasesN */
|
||||
unsigned * m_npcs;
|
||||
/* Constructor, SConstructor */
|
||||
struct {
|
||||
unsigned m_cidx;
|
||||
unsigned m_nfields; /* only used by Constructor */
|
||||
};
|
||||
/* Num */
|
||||
mpz * m_mpz;
|
||||
};
|
||||
/* Ret and Cases1 do not have arguments */
|
||||
friend vm_instr mk_push_instr(unsigned idx);
|
||||
friend vm_instr mk_drop_instr(unsigned n);
|
||||
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_num_instr(mpz const & v);
|
||||
friend vm_instr mk_ret_instr();
|
||||
friend vm_instr mk_cases1_instr();
|
||||
friend vm_instr mk_nat_cases_instr(unsigned pc);
|
||||
friend vm_instr mk_cases2_instr(unsigned pc);
|
||||
friend vm_instr mk_casesn_instr(unsigned num_pc, unsigned const * pcs);
|
||||
friend vm_instr mk_invoke_instr(unsigned n);
|
||||
friend vm_instr mk_invoke_global_instr(unsigned fn_idx, unsigned n);
|
||||
friend vm_instr mk_closure_instr(unsigned fn_idx, unsigned n);
|
||||
|
||||
void copy_args(vm_instr const & i);
|
||||
public:
|
||||
vm_instr(opcode op):m_op(op) {}
|
||||
vm_instr(vm_instr const & i);
|
||||
vm_instr(vm_instr && i);
|
||||
~vm_instr();
|
||||
|
||||
vm_instr & operator=(vm_instr const & s);
|
||||
vm_instr & operator=(vm_instr && s);
|
||||
};
|
||||
|
||||
vm_instr mk_push_instr(unsigned idx);
|
||||
vm_instr mk_drop_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_num_instr(mpz const & v);
|
||||
vm_instr mk_ret_instr();
|
||||
vm_instr mk_cases1_instr();
|
||||
vm_instr mk_nat_cases_instr(unsigned pc);
|
||||
vm_instr mk_cases2_instr(unsigned pc);
|
||||
vm_instr mk_casesn_instr(unsigned num_pc, unsigned const * pcs);
|
||||
vm_instr mk_invoke_instr(unsigned n);
|
||||
vm_instr mk_invoke_global_instr(unsigned fn_idx, unsigned n);
|
||||
vm_instr mk_closure_instr(unsigned fn_idx, unsigned n);
|
||||
|
||||
/** \brief Datastructure for storing the compiled bytecode */
|
||||
class vm_decls;
|
||||
|
||||
/** \brief Virtual machine for executing VM bytecode. */
|
||||
class vm_state {
|
||||
environment m_env;
|
||||
vm_decls const & m_decls;
|
||||
vm_instr const * m_code; /* code of the current function being executed */
|
||||
unsigned m_fn_idx; /* function idx being executed */
|
||||
unsigned m_pc; /* program counter */
|
||||
unsigned m_bp; /* base pointer */
|
||||
struct frame {
|
||||
vm_instr const * m_code;
|
||||
unsigned m_fn_idx;
|
||||
unsigned m_num;
|
||||
unsigned m_pc;
|
||||
unsigned m_bp;
|
||||
};
|
||||
std::vector<vm_obj> m_stack;
|
||||
std::vector<frame> m_call_stack;
|
||||
public:
|
||||
vm_state(environment const & env);
|
||||
environment const & env() const { return m_env; }
|
||||
/** \brief Push object into the data stack */
|
||||
void push(vm_obj const & o) { m_stack.push_back(o); }
|
||||
/** \brief Retrieve object from the call stack */
|
||||
vm_obj const & get(unsigned idx) const { lean_assert(m_bp + idx < m_stack.size()); return m_stack[m_bp + idx]; }
|
||||
|
||||
void invoke(unsigned n);
|
||||
void invoke_global(name const & fn);
|
||||
void invoke_global(unsigned fn_idx);
|
||||
};
|
||||
|
||||
typedef void (*vm_function)(vm_state & s);
|
||||
|
||||
/** \brief Add builtin implementation for the function named \c n. */
|
||||
void declare_vm_builtin(name const & n, vm_function fn);
|
||||
|
||||
environment add_vm_code(environment const & env, name const & fn, expr const & e, unsigned code_sz, vm_instr const * code);
|
||||
|
||||
/** \brief Return true iff \c fn is a VM function in the given environment. */
|
||||
bool is_vm_function(environment const & env, name const & fn);
|
||||
|
||||
void initialize_vm();
|
||||
void finalize_vm();
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue