From dc3d7597eef0adc7009cffd46af974bb5870591f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 May 2016 11:51:12 -0700 Subject: [PATCH] chore(library/vm/vm): document VM instructions --- src/frontends/lean/builtin_cmds.cpp | 2 +- src/library/vm/vm.cpp | 210 ++++++++++++++++++++++++++-- src/library/vm/vm.h | 5 +- 3 files changed, 199 insertions(+), 18 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 5c4a2f878b..6ad2626010 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -669,7 +669,7 @@ static environment vm_eval_cmd(parser & p) { vm_state s(p.env()); { timeit timer(p.ios().get_diagnostic_stream(), "vm_eval time"); - s.invoke_global(n); + s.invoke_fn(n); } vm_obj r = s.get(0); display(p.ios().get_regular_stream(), r); diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 0779b04d23..e1226a5598 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -619,14 +619,6 @@ void vm_state::invoke_global(vm_decl const & d) { m_bp = m_stack.size() - d.get_arity(); } -void vm_state::invoke_global_builtin(vm_decl const & d) { - if (d.is_builtin()) { - invoke_builtin(d); - } else { - invoke_global(d); - } -} - void vm_state::run() { lean_assert(m_code); unsigned init_call_stack_sz = m_call_stack.size(); @@ -638,7 +630,9 @@ void vm_state::run() { /* We only trace VM in debug mode */ lean_trace(name({"vm", "run"}), tout() << m_pc << ": "; - instr.display(tout().get_stream(), [&](unsigned idx) { return optional(m_decls[idx].get_name()); }); + instr.display(tout().get_stream(), [&](unsigned idx) { + return optional(m_decls[idx].get_name()); + }); tout() << ", bp: " << m_bp << "\n"; for (unsigned i = 0; i < m_stack.size(); i++) { tout() << i << " := "; @@ -649,10 +643,31 @@ void vm_state::run() { }); switch (instr.op()) { case opcode::Push: + /* Instruction: push i + + stack before, after + ... ... + bp : a_0 bp : a_0 + ... ... + a_i ==> a_i + ... ... + v v + a_i + */ m_stack.push_back(m_stack[m_bp + instr.get_idx()]); m_pc++; goto main_loop; case opcode::Drop: { + /* Instruction: drop n + + stack before, after + ... ... + w w + a_1 ==> v + ... + a_n + v + */ unsigned num = instr.get_num(); unsigned sz = m_stack.size(); lean_assert(sz > num); @@ -662,13 +677,33 @@ void vm_state::run() { goto main_loop; } case opcode::Goto: + /* Instruction: goto pc + + m_pc := pc + */ m_pc = instr.get_goto_pc(); goto main_loop; case opcode::SConstructor: + /** Instruction: scnstr i + + stack before, after + ... ... + v ==> v + #i + */ m_stack.push_back(mk_vm_simple(instr.get_cidx())); m_pc++; goto main_loop; case opcode::Constructor: { + /** Instruction: cnstr i n + + stack before, after + ... ... + v ==> v + a_1 (#i a_1 ... a_n) + ... + a_n + */ unsigned nfields = instr.get_nfields(); unsigned sz = m_stack.size(); vm_obj new_value = mk_vm_constructor(instr.get_cidx(), nfields, m_stack.data() + sz - nfields); @@ -678,6 +713,15 @@ void vm_state::run() { goto main_loop; } case opcode::Closure: { + /** Instruction: closure fn n + + stack before, after + ... ... + v ==> v + a_n (fn a_n ... a_1) + ... + a_1 + */ unsigned nargs = instr.get_nargs(); unsigned sz = m_stack.size(); vm_obj new_value = mk_vm_closure(instr.get_fn_idx(), nargs, m_stack.data() + sz - nargs); @@ -687,10 +731,26 @@ void vm_state::run() { goto main_loop; } case opcode::Num: + /** Instruction: num n + + stack before, after + ... ... + v ==> v + n + */ m_stack.push_back(mk_vm_mpz(instr.get_mpz())); m_pc++; goto main_loop; case opcode::Cases1: { + /** Instruction: cases1 + + stack before, after + ... ... + v ==> v + (#i a_1 ... a_n) a_1 + ... + a_n + */ vm_obj top = m_stack.back(); m_stack.pop_back(); push_fields(top); @@ -698,6 +758,18 @@ void vm_state::run() { goto main_loop; } case opcode::Cases2: { + /** Instruction: cases2 pc1 pc2 + + stack before, after + ... ... + v ==> v + (#i a_1 ... a_n) a_1 + ... + a_n + + m_pc := pc1 if i == 0 + := pc2 if i == 1 + */ vm_obj top = m_stack.back(); m_stack.pop_back(); push_fields(top); @@ -705,6 +777,16 @@ void vm_state::run() { goto main_loop; } case opcode::NatCases: { + /** Instruction: natcases pc1 pc2 + + stack before, after (if n = 0) after (if n > 0) + ... ... ... + v ==> v v + n n-1 + + m_pc := pc1 if n == 0 + := pc2 if otherwise + */ vm_obj top = m_stack.back(); m_stack.pop_back(); if (is_simple(top)) { @@ -730,6 +812,17 @@ void vm_state::run() { } } case opcode::CasesN: { + /** Instruction: casesn pc_0 ... pc_[n-1] + + stack before, after + ... ... + v ==> v + (#i a_1 ... a_n) a_1 + ... + a_n + + m_pc := pc_i + */ vm_obj top = m_stack.back(); m_stack.pop_back(); push_fields(top); @@ -737,6 +830,14 @@ void vm_state::run() { goto main_loop; } case opcode::Proj: { + /** Instruction: proj i + + stack before, after + ... ... + v ==> v + (#i a_0 ... a_{n-1}) a_i + + */ vm_obj top = m_stack.back(); m_stack.pop_back(); m_stack.push_back(cfield(top, instr.get_idx())); @@ -746,6 +847,28 @@ void vm_state::run() { case opcode::Unreachable: throw exception("VM unreachable instruction has been reached"); case opcode::Ret: { + /** + Instruction: ret + + call stack before after + + ... ... + (code, fn_idx, num, pc, bp) ==> + + Restore m_code, m_fn_idx, m_pc, m_bp with top of call stack. + + stack before after + ... ... + v v + a_n r + ... ==> + a_1 + r + + + a_1, ... a_n were the arguments for the function call. + r is the result. + */ frame const & fr = m_call_stack.back(); unsigned sz = m_stack.size(); std::swap(m_stack[sz - fr.m_num - 1], m_stack[sz - 1]); @@ -763,6 +886,26 @@ void vm_state::run() { } } case opcode::Invoke: { + /** + Instruction: invoke n + + Case 1) n + m < fn.arity, where m is the number of arguments in the closure, + and fn is the function stored in the closure. + + stack before after + ... ... + v v + a_n (closure fn a_n ... a_1 b_m ... b_1) + ... ==> + a_1 + (closure fn b_m ... b_1) + + Case 2) n + m == fn.arity and fn is not builtin. + See InvokeGlobal case. + + Case 3) n + m == fn.arity and fn is builtin. + See InvokeBuiltin case. + */ unsigned nargs = instr.get_nargs(); unsigned sz = m_stack.size(); vm_obj closure = m_stack.back(); @@ -776,7 +919,10 @@ void vm_state::run() { std::copy(cfields(closure), cfields(closure) + csz, m_stack.end()); /* Now, stack contains closure arguments + original stack arguments */ if (new_nargs == arity) { - invoke_global_builtin(d); + if (d.is_builtin()) + invoke_builtin(d); + else + invoke_global(d); goto main_loop; } else { /* We don't have sufficient arguments. So, we create a new closure */ @@ -789,30 +935,66 @@ void vm_state::run() { } } case opcode::InvokeGlobal: + /** + Instruction: ginvoke fn + + call stack before after + + ... ==> ... + (fn.m_code, fn.idx, fn.arity, m_pc+1, m_bp) + + Update m_code, m_fn_idx, with fn, and update m_pc := 0, m_bp + + stack before after + ... ... + v v + a_n m_bp : a_n + ... ==> ... + a_1 a_1 + + where n is fn.arity + */ invoke_global(m_decls[instr.get_fn_idx()]); goto main_loop; case opcode::InvokeBuiltin: + /** + Instruction: builtin fn + + stack before after + ... ... + v v + a_n r + ... ==> + a_1 + + where n is fn.arity + + Remark: note that the arguments are in reverse order. + */ invoke_builtin(m_decls[instr.get_fn_idx()]); goto main_loop; } } } -void vm_state::invoke_global(name const & fn) { +void vm_state::invoke_fn(name const & fn) { if (auto r = m_fn_name2idx.find(fn)) { - invoke_global(*r); + invoke_fn(*r); } else { throw exception(sstream() << "VM does not have code for '" << fn << "'"); } } -void vm_state::invoke_global(unsigned fn_idx) { +void vm_state::invoke_fn(unsigned fn_idx) { lean_assert(fn_idx < m_decls.size()); vm_decl const & d = m_decls[fn_idx]; unsigned arity = d.get_arity(); if (arity > m_stack.size()) throw exception("invalid VM function call, data stack does not have enough values"); - invoke_global_builtin(d); + if (d.is_builtin()) + invoke_builtin(d); + else + invoke_global(d); run(); } diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 43f29ae2a7..de66207ce0 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -421,7 +421,6 @@ class vm_state { void push_fields(vm_obj const & obj); void invoke_builtin(vm_decl const & d); void invoke_global(vm_decl const & d); - void invoke_global_builtin(vm_decl const & d); void run(); public: @@ -439,8 +438,8 @@ public: return m_stack[m_bp + idx]; } - void invoke_global(name const & fn); - void invoke_global(unsigned fn_idx); + void invoke_fn(name const & fn); + void invoke_fn(unsigned fn_idx); }; /** \brief Add builtin implementation for the function named \c n. */