diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 8bf6359cf0..a8945c49ee 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -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 diff --git a/src/library/vm.cpp b/src/library/vm.cpp new file mode 100644 index 0000000000..ac0d532f62 --- /dev/null +++ b/src/library/vm.cpp @@ -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 & 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 & 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(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 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; +} +} diff --git a/src/library/vm.h b/src/library/vm.h new file mode 100644 index 0000000000..cd3567d64e --- /dev/null +++ b/src/library/vm.h @@ -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 +#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 & 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(obj) & 1) == 0) +#define LEAN_VM_BOX(num) (reinterpret_cast((num << 1) | 1)) +#define LEAN_VM_UNBOX(obj) (reinterpret_cast(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(reinterpret_cast(this)+sizeof(vm_composite)); + } + friend vm_obj_cell; + void dealloc(buffer & 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(reinterpret_cast(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(o.raw()); +} +inline vm_mpz * to_mpz_core(vm_obj const & o) { lean_assert(is_mpz(o)); return static_cast(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(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(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 m_stack; + std::vector 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(); +}