From 90260e005eba9395f0cdd2ea915bf70fdc44df6f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Feb 2019 08:52:11 -0800 Subject: [PATCH] feat(library/compiler/emit_bytecode): ignore unknown decls cc @kha --- src/library/compiler/emit_bytecode.cpp | 45 +++++++++++++++++++------- src/library/vm/vm.cpp | 23 +++++++++++-- 2 files changed, 55 insertions(+), 13 deletions(-) diff --git a/src/library/compiler/emit_bytecode.cpp b/src/library/compiler/emit_bytecode.cpp index 1ca3ef136b..912dd8ec18 100644 --- a/src/library/compiler/emit_bytecode.cpp +++ b/src/library/compiler/emit_bytecode.cpp @@ -17,6 +17,11 @@ Author: Leonardo de Moura #include "library/vm/optimize.h" #include "library/compiler/llnf.h" #include "library/compiler/util.h" +#include "library/compiler/extern_attribute.h" + +/* Uncomment the following line to ignore unknown declarations, and use a default `not_implemented` declaration that just + throws an exception. */ +#define LEAN_IGNORE_UNKNOWN_DECLS namespace lean { class emit_bytecode_fn { @@ -91,15 +96,36 @@ class emit_bytecode_fn { emit_apply_instr(args.size() - 1); } + vm_decl get_vm_decl(name const & fn) { + if (optional decl = ::lean::get_vm_decl(m_env, fn)) { + return *decl; + } else { +#if defined(LEAN_IGNORE_UNKNOWN_DECLS) + if (optional arity = get_extern_constant_arity(m_env, fn)) { + switch (*arity) { + case 1: return *::lean::get_vm_decl(m_env, "not_implemented_1"); + case 2: return *::lean::get_vm_decl(m_env, "not_implemented_2"); + case 3: return *::lean::get_vm_decl(m_env, "not_implemented_3"); + case 4: return *::lean::get_vm_decl(m_env, "not_implemented_4"); + case 5: return *::lean::get_vm_decl(m_env, "not_implemented_5"); + case 6: return *::lean::get_vm_decl(m_env, "not_implemented_6"); + case 7: return *::lean::get_vm_decl(m_env, "not_implemented_7"); + case 8: return *::lean::get_vm_decl(m_env, "not_implemented_8"); + } + } +#endif + throw_unknown_constant(fn); + } + } + void compile_closure(expr const & e, unsigned bpz, vdecls const & m) { buffer args; get_app_args(e, args); lean_assert(is_constant(args[0])); - optional decl = get_vm_decl(m_env, const_name(args[0])); - if (!decl) throw_unknown_constant(const_name(args[0])); - lean_assert(decl->get_arity() > args.size() - 1); + vm_decl decl = get_vm_decl(const_name(args[0])); + lean_assert(decl.get_arity() > args.size() - 1); compile_rev_args(args.size() - 1, args.data() + 1, bpz, m); - emit(mk_closure_instr(decl->get_idx(), args.size() - 1)); + emit(mk_closure_instr(decl.get_idx(), args.size() - 1)); } void compile_constant(expr const & e) { @@ -114,10 +140,8 @@ class emit_bytecode_fn { } else if (is_llnf_cnstr(e, cidx, nusizes, ssz)) { if (ssz != 0) throw_no_unboxed_support(); emit(mk_sconstructor_instr(cidx)); - } else if (optional decl = get_vm_decl(m_env, n)) { - compile_global(*decl, 0, nullptr, 0, vdecls()); } else { - throw_unknown_constant(n); + compile_global(get_vm_decl(n), 0, nullptr, 0, vdecls()); } } @@ -246,16 +270,15 @@ class emit_bytecode_fn { compile_rev_args(args.size() - 1, args.data() + 1, bpz, m); emit(mk_invoke_jp_instr(d->m_pc, d->m_idx, args.size() - 1)); } else if (is_sorry(e)) { - compile_global(*get_vm_decl(m_env, "sorry"), 0, nullptr, bpz, m); + compile_global(get_vm_decl("sorry"), 0, nullptr, bpz, m); } else { buffer args; get_app_args(e, args); lean_assert(is_constant(fn)); lean_assert(!is_enf_neutral(fn)); lean_assert(!is_enf_unreachable(fn)); - optional decl = get_vm_decl(m_env, const_name(fn)); - if (!decl) throw_unknown_constant(const_name(fn)); - compile_global(*decl, args.size(), args.data(), bpz, m); + vm_decl decl = get_vm_decl(const_name(fn)); + compile_global(decl, args.size(), args.data(), bpz, m); } } diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 08638a6008..ce03d40754 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -1368,10 +1368,11 @@ environment add_vm_code(environment const & env, name const & fn, unsigned arity optional get_vm_decl(environment const & env, name const & n) { vm_decls const & ext = get_extension(env); - if (auto decl = ext.m_decls.find(get_vm_index(n))) + if (auto decl = ext.m_decls.find(get_vm_index(n))) { return optional(*decl); - else + } else { return optional(); + } } constexpr unsigned g_null_fn_idx = -1; @@ -3638,6 +3639,16 @@ optional find_vm_name(unsigned idx) { return g_vm_index_manager->find_name(idx); } +vm_obj not_implemented_1(vm_obj const &) { throw exception("not implemented yet"); } +vm_obj not_implemented_2(vm_obj const &, vm_obj const &) { throw exception("not implemented yet"); } +vm_obj not_implemented_3(vm_obj const &, vm_obj const &, vm_obj const &) { throw exception("not implemented yet"); } +vm_obj not_implemented_4(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &) { throw exception("not implemented yet"); } +vm_obj not_implemented_5(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &) { throw exception("not implemented yet"); } +vm_obj not_implemented_6(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &) { throw exception("not implemented yet"); } +vm_obj not_implemented_7(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &) { throw exception("not implemented yet"); } +vm_obj not_implemented_8(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &) { throw exception("not implemented yet"); } + + void initialize_vm_core() { g_vm_index_manager = new vm_index_manager; g_vm_builtins = new name_map>(); @@ -3648,6 +3659,14 @@ void initialize_vm_core() { register_trace_class("vm"); register_trace_class({"vm", "run"}); }); + DECLARE_VM_BUILTIN(name({"not_implemented_1"}), not_implemented_1); + DECLARE_VM_BUILTIN(name({"not_implemented_2"}), not_implemented_2); + DECLARE_VM_BUILTIN(name({"not_implemented_3"}), not_implemented_3); + DECLARE_VM_BUILTIN(name({"not_implemented_4"}), not_implemented_4); + DECLARE_VM_BUILTIN(name({"not_implemented_5"}), not_implemented_5); + DECLARE_VM_BUILTIN(name({"not_implemented_6"}), not_implemented_6); + DECLARE_VM_BUILTIN(name({"not_implemented_7"}), not_implemented_7); + DECLARE_VM_BUILTIN(name({"not_implemented_8"}), not_implemented_8); } void finalize_vm_core() {