From 99bc069fdd03df69546b3a3bc07e8a8ead006af8 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 3 Sep 2019 14:34:33 +0200 Subject: [PATCH] feat(library/compiler/ir_interpreter): implement IR interpreter --- bin/leanc.in | 4 +- src/library/compiler/CMakeLists.txt | 3 +- src/library/compiler/init_module.cpp | 3 + src/library/compiler/ir.cpp | 17 +- src/library/compiler/ir.h | 17 + src/library/compiler/ir_interpreter.cpp | 594 ++++++++++++++++++++++++ src/library/compiler/ir_interpreter.h | 17 + src/runtime/apply.cpp | 2 +- src/runtime/apply.h | 1 + 9 files changed, 638 insertions(+), 20 deletions(-) create mode 100644 src/library/compiler/ir_interpreter.cpp create mode 100644 src/library/compiler/ir_interpreter.h diff --git a/bin/leanc.in b/bin/leanc.in index 9bed536465..af505f0b33 100644 --- a/bin/leanc.in +++ b/bin/leanc.in @@ -31,7 +31,7 @@ if [[ $use_c == yes ]]; then [ -f $LEAN_CC ] || command -v $LEAN_CC || error "no suitable C compiler found!" # NOTE: leanstatic and leanstdlib are cyclically dependent - $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument + $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp -ldl @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument else # Check C++ compiler for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/g++; do @@ -42,5 +42,5 @@ else [ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!" # NOTE: leanstatic and leanstdlib are cyclically dependent - $LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument + $LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp -ldl @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument fi diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt index 17bfc05471..11912b9749 100644 --- a/src/library/compiler/CMakeLists.txt +++ b/src/library/compiler/CMakeLists.txt @@ -5,4 +5,5 @@ add_library(compiler OBJECT init_module.cpp ## New reduce_arity.cpp closed_term_cache.cpp export_attribute.cpp extern_attribute.cpp borrowed_annotation.cpp init_attribute.cpp eager_lambda_lifting.cpp - struct_cases_on.cpp find_jp.cpp ir.cpp implemented_by_attribute.cpp) + struct_cases_on.cpp find_jp.cpp ir.cpp implemented_by_attribute.cpp + ir_interpreter.cpp) diff --git a/src/library/compiler/init_module.cpp b/src/library/compiler/init_module.cpp index bd5dd65a7d..3270b4687b 100644 --- a/src/library/compiler/init_module.cpp +++ b/src/library/compiler/init_module.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/compiler/borrowed_annotation.h" #include "library/compiler/ll_infer_type.h" #include "library/compiler/ir.h" +#include "library/compiler/ir_interpreter.h" namespace lean { void initialize_compiler_module() { @@ -27,9 +28,11 @@ void initialize_compiler_module() { initialize_borrowed_annotation(); initialize_ll_infer_type(); initialize_ir(); + initialize_ir_interpreter(); } void finalize_compiler_module() { + finalize_ir_interpreter(); finalize_ir(); finalize_ll_infer_type(); finalize_borrowed_annotation(); diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp index 02dd709341..5730656e65 100644 --- a/src/library/compiler/ir.cpp +++ b/src/library/compiler/ir.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/compiler/util.h" #include "library/compiler/llnf.h" #include "library/compiler/extern_attribute.h" +#include "library/compiler/ir.h" namespace lean { namespace ir { @@ -43,22 +44,6 @@ extern "C" object * lean_ir_decl_to_string(object * d); extern "C" object * lean_ir_compile(object * env, object * opts, object * decls); extern "C" object * lean_ir_log_to_string(object * log); extern "C" object * lean_ir_add_decl(object * env, object * decl); -/* -inductive IRType -| float | uint8 | uint16 | uint32 | uint64 | usize -| irrelevant | object | tobject -*/ -enum class type { Float, UInt8, UInt16, UInt32, UInt64, USize, Irrelevant, Object, TObject }; - -typedef nat var_id; -typedef nat jp_id; -typedef name fun_id; -typedef object_ref arg; -typedef object_ref expr; -typedef object_ref param; -typedef object_ref fn_body; -typedef object_ref alt; -typedef object_ref decl; arg mk_var_arg(var_id const & id) { inc(id.raw()); return arg(lean_ir_mk_var_arg(id.raw())); } arg mk_irrelevant_arg() { return arg(irrelevant_arg); } diff --git a/src/library/compiler/ir.h b/src/library/compiler/ir.h index 702ebcbf3d..b2b8ab9789 100644 --- a/src/library/compiler/ir.h +++ b/src/library/compiler/ir.h @@ -10,6 +10,23 @@ Author: Leonardo de Moura #include "library/compiler/util.h" namespace lean { namespace ir { +/* +inductive IRType +| float | uint8 | uint16 | uint32 | uint64 | usize +| irrelevant | object | tobject +*/ +enum class type { Float, UInt8, UInt16, UInt32, UInt64, USize, Irrelevant, Object, TObject }; + +typedef nat var_id; +typedef nat jp_id; +typedef name fun_id; +typedef object_ref arg; +typedef object_ref expr; +typedef object_ref param; +typedef object_ref fn_body; +typedef object_ref alt; +typedef object_ref decl; + typedef object_ref decl; std::string decl_to_string(decl const & d); void test(decl const & d); diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp new file mode 100644 index 0000000000..90a8f96e84 --- /dev/null +++ b/src/library/compiler/ir_interpreter.cpp @@ -0,0 +1,594 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Sebastian Ullrich +*/ +#include +#include +#include +#include "runtime/flet.h" +#include "runtime/apply.h" +#include "library/trace.h" +#include "library/compiler/ir.h" +#include "util/option_ref.h" +#include "util/array_ref.h" +#include "util/nat.h" + +namespace lean { +namespace ir { +typedef object_ref lit_val; +typedef object_ref ctor_info; + +template +inline T const & cnstr_get_ref_t(object_ref const & o, unsigned i) { + static_assert(sizeof(T) == sizeof(object_ref), "unexpected object wrapper size"); + return *reinterpret_cast(&cnstr_get_ref(o.raw(), i)); +} + +bool arg_is_irrelevant(arg const & a) { return is_scalar(a.raw()); } +var_id const & arg_var_id(arg const & a) { lean_assert(!arg_is_irrelevant(a)); return cnstr_get_ref_t(a, 0); } + +enum class lit_val_kind { Num, Str }; +lit_val_kind lit_val_tag(lit_val const & l) { return static_cast(cnstr_tag(l.raw())); } +nat const & lit_val_num(lit_val const & l) { lean_assert(lit_val_tag(l) == lit_val_kind::Num); return cnstr_get_ref_t(l, 0); } +string_ref const & lit_val_str(lit_val const & l) { lean_assert(lit_val_tag(l) == lit_val_kind::Str); return cnstr_get_ref_t(l, 0); } + +name const & ctor_info_name(ctor_info const & c) { return cnstr_get_ref_t(c, 0); } +nat const & ctor_info_idx(ctor_info const & c) { return cnstr_get_ref_t(c, 1); } +nat const & ctor_info_size(ctor_info const & c) { return cnstr_get_ref_t(c, 2); } +nat const & ctor_info_usize(ctor_info const & c) { return cnstr_get_ref_t(c, 3); } +nat const & ctor_info_ssize(ctor_info const & c) { return cnstr_get_ref_t(c, 4); } + +enum class expr_kind { Ctor, Reset, Reuse, Proj, UProj, SProj, FAp, PAp, Ap, Box, Unbox, Lit, IsShared, IsTaggedPtr }; +expr_kind expr_tag(expr const & e) { return static_cast(cnstr_tag(e.raw())); } +ctor_info const & expr_ctor_info(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Ctor); return cnstr_get_ref_t(e, 0); } +array_ref const & expr_ctor_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Ctor); return cnstr_get_ref_t>(e, 1); } +nat const & expr_reset_num_objs(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reset); return cnstr_get_ref_t(e, 0); } +var_id const & expr_reset_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reset); return cnstr_get_ref_t(e, 1); } +var_id const & expr_reuse_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reuse); return cnstr_get_ref_t(e, 0); } +ctor_info const & expr_reuse_ctor(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reuse); return cnstr_get_ref_t(e, 1); } +bool expr_reuse_update_header(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reuse); return cnstr_get_uint8(e.raw(), sizeof(void *) * 3); } +array_ref const & expr_reuse_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reuse); return cnstr_get_ref_t>(e, 2); } +nat const & expr_proj_idx(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Proj); return cnstr_get_ref_t(e, 0); } +var_id const & expr_proj_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Proj); return cnstr_get_ref_t(e, 1); } +nat const & expr_uproj_idx(expr const & e) { lean_assert(expr_tag(e) == expr_kind::UProj); return cnstr_get_ref_t(e, 0); } +var_id const & expr_uproj_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::UProj); return cnstr_get_ref_t(e, 1); } +nat const & expr_sproj_num_objs(expr const & e) { lean_assert(expr_tag(e) == expr_kind::SProj); return cnstr_get_ref_t(e, 0); } +nat const & expr_sproj_offset(expr const & e) { lean_assert(expr_tag(e) == expr_kind::SProj); return cnstr_get_ref_t(e, 1); } +var_id const & expr_sproj_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::SProj); return cnstr_get_ref_t(e, 2); } +fun_id const & expr_fap_fun(expr const & e) { lean_assert(expr_tag(e) == expr_kind::FAp); return cnstr_get_ref_t(e, 0); } +array_ref const & expr_fap_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::FAp); return cnstr_get_ref_t>(e, 1); } +fun_id const & expr_pap_fun(expr const & e) { lean_assert(expr_tag(e) == expr_kind::PAp); return cnstr_get_ref_t(e, 0); } +array_ref const & expr_pap_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::PAp); return cnstr_get_ref_t>(e, 1); } +var_id const & expr_ap_fun(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Ap); return cnstr_get_ref_t(e, 0); } +array_ref const & expr_ap_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Ap); return cnstr_get_ref_t>(e, 1); } +type expr_box_type(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Box); return static_cast(cnstr_get_uint8(e.raw(), sizeof(void *))); } +var_id const & expr_box_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Box); return cnstr_get_ref_t(e, 0); } +var_id const & expr_unbox_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Unbox); return cnstr_get_ref_t(e, 0); } +lit_val const & expr_lit_val(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Lit); return cnstr_get_ref_t(e, 0); } +var_id const & expr_is_shared_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::IsShared); return cnstr_get_ref_t(e, 0); } +var_id const & expr_is_tagged_ptr_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::IsTaggedPtr); return cnstr_get_ref_t(e, 0); } + +typedef object_ref param; +var_id const & param_var(param const & p) { return cnstr_get_ref_t(p, 0); } +bool param_borrow(param const & p) { return cnstr_get_uint8(p.raw(), sizeof(void *)); } + +typedef object_ref alt_core; +enum class alt_core_kind { Ctor, Default }; +alt_core_kind alt_core_tag(alt_core const & a) { return static_cast(cnstr_tag(a.raw())); } +ctor_info const & alt_core_ctor_info(alt_core const & a) { lean_assert(alt_core_tag(a) == alt_core_kind::Ctor); return cnstr_get_ref_t(a, 0); } +fn_body const & alt_core_ctor_cont(alt_core const & a) { lean_assert(alt_core_tag(a) == alt_core_kind::Ctor); return cnstr_get_ref_t(a, 1); } +fn_body const & alt_core_default_cont(alt_core const & a) { lean_assert(alt_core_tag(a) == alt_core_kind::Default); return cnstr_get_ref_t(a, 0); } + +enum class fn_body_kind { VDecl, JDecl, Set, SetTag, USet, SSet, Inc, Dec, Del, MData, Case, Ret, Jmp, Unreachable }; +fn_body_kind fn_body_tag(fn_body const & a) { return is_scalar(a.raw()) ? static_cast(unbox(a.raw())) : static_cast(cnstr_tag(a.raw())); } +var_id const & fn_body_vdecl_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::VDecl); return cnstr_get_ref_t(b, 0); } +type fn_body_vdecl_type(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::VDecl); return static_cast(cnstr_get_uint8(b.raw(), sizeof(void *) * 3)); } +expr const & fn_body_vdecl_expr(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::VDecl); return cnstr_get_ref_t(b, 1); } +fn_body const & fn_body_vdecl_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::VDecl); return cnstr_get_ref_t(b, 2); } +jp_id const & fn_body_jdecl_id(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::JDecl); return cnstr_get_ref_t(b, 0); } +array_ref const & fn_body_jdecl_params(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::JDecl); return cnstr_get_ref_t>(b, 1); } +fn_body const & fn_body_jdecl_body(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::JDecl); return cnstr_get_ref_t(b, 2); } +fn_body const & fn_body_jdecl_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::JDecl); return cnstr_get_ref_t(b, 3); } +var_id const & fn_body_set_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Set); return cnstr_get_ref_t(b, 0); } +nat const & fn_body_set_idx(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Set); return cnstr_get_ref_t(b, 1); } +arg const & fn_body_set_arg(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Set); return cnstr_get_ref_t(b, 2); } +fn_body const & fn_body_set_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Set); return cnstr_get_ref_t(b, 3); } +var_id const & fn_body_set_tag_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SetTag); return cnstr_get_ref_t(b, 0); } +nat const & fn_body_set_tag_cidx(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SetTag); return cnstr_get_ref_t(b, 1); } +fn_body const & fn_body_set_tag_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SetTag); return cnstr_get_ref_t(b, 2); } +var_id const & fn_body_uset_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::USet); return cnstr_get_ref_t(b, 0); } +nat const & fn_body_uset_idx(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::USet); return cnstr_get_ref_t(b, 1); } +var_id const & fn_body_uset_arg(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::USet); return cnstr_get_ref_t(b, 2); } +fn_body const & fn_body_uset_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::USet); return cnstr_get_ref_t(b, 3); } +var_id const & fn_body_sset_target(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t(b, 0); } +nat const & fn_body_sset_num_objs(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t(b, 1); } +nat const & fn_body_sset_offset(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t(b, 2); } +var_id const & fn_body_sset_source(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t(b, 3); } +type fn_body_sset_type(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return static_cast(cnstr_get_uint8(b.raw(), sizeof(void *) * 5)); } +fn_body const & fn_body_sset_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t(b, 4); } +var_id const & fn_body_inc_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Inc); return cnstr_get_ref_t(b, 0); } +nat const & fn_body_inc_val(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Inc); return cnstr_get_ref_t(b, 1); } +bool fn_body_inc_maybe_scalar(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Inc); return static_cast(cnstr_get_uint8(b.raw(), sizeof(void *) * 3)); } +fn_body const & fn_body_inc_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Inc); return cnstr_get_ref_t(b, 2); } +var_id const & fn_body_dec_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Dec); return cnstr_get_ref_t(b, 0); } +nat const & fn_body_dec_val(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Dec); return cnstr_get_ref_t(b, 1); } +bool fn_body_dec_maybe_scalar(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Dec); return static_cast(cnstr_get_uint8(b.raw(), sizeof(void *) * 3)); } +fn_body const & fn_body_dec_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Dec); return cnstr_get_ref_t(b, 2); } +var_id const & fn_body_del_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Del); return cnstr_get_ref_t(b, 0); } +fn_body const & fn_body_del_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Del); return cnstr_get_ref_t(b, 1); } +object_ref const & fn_body_mdata_data(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::MData); return cnstr_get_ref_t(b, 0); } +fn_body const & fn_body_mdata_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::MData); return cnstr_get_ref_t(b, 1); } +name const & fn_body_case_tid(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Case); return cnstr_get_ref_t(b, 0); } +var_id const & fn_body_case_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Case); return cnstr_get_ref_t(b, 1); } +array_ref const & fn_body_case_alts(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Case); return cnstr_get_ref_t>(b, 2); } +arg const & fn_body_ret_arg(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Ret); return cnstr_get_ref_t(b, 0); } +jp_id const & fn_body_jmp_jp(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Jmp); return cnstr_get_ref_t(b, 0); } +array_ref const & fn_body_jmp_args(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Jmp); return cnstr_get_ref_t>(b, 1); } + +typedef object_ref decl; +enum class decl_kind { Fun, Extern }; +decl_kind decl_tag(decl const & a) { return is_scalar(a.raw()) ? static_cast(unbox(a.raw())) : static_cast(cnstr_tag(a.raw())); } +fun_id const & decl_fun_id(decl const & b) { return cnstr_get_ref_t(b, 0); } +array_ref const & decl_params(decl const & b) { return cnstr_get_ref_t>(b, 1); } +type decl_type(decl const & b) { return static_cast(cnstr_get_uint8(b.raw(), sizeof(void *) * 3)); } +fn_body const & decl_fun_body(decl const & b) { lean_assert(decl_tag(b) == decl_kind::Fun); return cnstr_get_ref_t(b, 2); } + +extern "C" object * lean_ir_find_env_decl(object * env, object * n); +option_ref find_env_decl(environment const & env, name const & n) { + return option_ref(lean_ir_find_env_decl(env.to_obj_arg(), n.to_obj_arg())); +} + +static string_ref * g_mangle_prefix = nullptr; +static string_ref * g_boxed_mangled_suffix = nullptr; + +extern "C" object * lean_name_mangle(object * n, object * pre); +string_ref name_mangle(name const & n, string_ref const & pre) { + return string_ref(lean_name_mangle(n.to_obj_arg(), pre.to_obj_arg())); +} + +class interpreter { + std::vector m_arg_stack; + std::vector m_jp_stack; + struct frame { + name m_fn; + size_t m_arg_bp; + size_t m_jp_bp; + }; + std::vector m_call_stack; + environment const & m_env; + + inline frame & get_frame() { + return m_call_stack.back(); + } + + inline object * & var(var_id const & v) { + // variables are 1-indexed + size_t i = get_frame().m_arg_bp + v.get_small_value() - 1; + if (i >= m_arg_stack.size()) { + m_arg_stack.resize(i + 1); + } + return m_arg_stack[i]; + } + + object * eval_arg(arg const & a) { + return arg_is_irrelevant(a) ? box(0) : var(arg_var_id(a)); + } + + object * alloc_ctor(ctor_info const & i, array_ref const & args) { + size_t idx = ctor_info_idx(i).get_small_value(); + size_t size = ctor_info_size(i).get_small_value(); + size_t usize = ctor_info_usize(i).get_small_value(); + size_t ssize = ctor_info_ssize(i).get_small_value(); + if (size == 0 && usize == 0 && ssize == 0) { + return box(idx); + } else { + object *o = alloc_cnstr(idx, size, usize * sizeof(void *) + ssize); + for (size_t i = 0; i < args.size(); i++) { + cnstr_set(o, i, eval_arg(args[i])); + } + return o; + } + } + + object * eval_expr(expr const & e, type t) { + switch (expr_tag(e)) { + case expr_kind::Ctor: + return alloc_ctor(expr_ctor_info(e), expr_ctor_args(e)); + case expr_kind::Reset: { + object * o = var(expr_reset_obj(e)); + if (is_exclusive(o)) { + for (size_t i = 0; i < expr_reset_num_objs(e).get_small_value(); i++) { + cnstr_release(o, i); + } + return o; + } else { + dec_ref(o); + return box(0); + } + } + case expr_kind::Reuse: { + object * o = var(expr_reuse_obj(e)); + if (is_scalar(o)) { + return alloc_ctor(expr_reuse_ctor(e), expr_reuse_args(e)); + } else { + if (expr_reuse_update_header(e)) { + cnstr_set_tag(o, ctor_info_idx(expr_reuse_ctor(e)).get_small_value()); + } + for (size_t i = 0; i < expr_reuse_args(e).size(); i++) { + cnstr_set(o, i, eval_arg(expr_reuse_args(e)[i])); + } + return o; + } + } + case expr_kind::Proj: + return cnstr_get(var(expr_proj_obj(e)), expr_proj_idx(e).get_small_value()); + case expr_kind::UProj: + return box_size_t(cnstr_get_usize(var(expr_uproj_obj(e)), expr_uproj_idx(e).get_small_value())); + case expr_kind::SProj: { + size_t offset = expr_sproj_num_objs(e).get_small_value() * sizeof(void *) + + expr_sproj_offset(e).get_small_value(); + object *o = var(expr_sproj_obj(e)); + switch (t) { + case type::Float: throw exception("floats are not supported yet"); + case type::UInt8: return box(cnstr_get_uint8(o, offset)); + case type::UInt16: return box(cnstr_get_uint16(o, offset)); + case type::UInt32: return box_uint32(cnstr_get_uint32(o, offset)); + case type::UInt64: return box_uint64(cnstr_get_uint64(o, offset)); + default: throw exception("invalid instruction"); + } + } + case expr_kind::FAp: { + // TODO(Sebastian): cache + if (expr_fap_args(e).size()) { + return call(expr_fap_fun(e), expr_fap_args(e)); + } else { + object * r = load(expr_fap_fun(e), t); + mark_persistent(r); + return r; + } + } + case expr_kind::PAp: { + decl d = get_fdecl(expr_pap_fun(e)); + unsigned i = 0; + object * cls; + if (void * p = get_symbol_pointer(expr_pap_fun(e))) { + cls = alloc_closure(p, decl_params(d).size(), expr_pap_args(e).size()); + } else { + cls = alloc_closure(reinterpret_cast(stub_m_aux), 16 + decl_params(d).size(), 16 + expr_pap_args(e).size()); + closure_set(cls, i++, box(reinterpret_cast(this))); + closure_set(cls, i++, d.to_obj_arg()); + for (; i < 16; i++) { + closure_set(cls, i, box(0)); + } + } + for (arg const & a : expr_pap_args(e)) { + closure_set(cls, i++, eval_arg(a)); + } + return cls; + } + case expr_kind::Ap: { + size_t old_size = m_arg_stack.size(); + for (const auto & arg : expr_ap_args(e)) { + m_arg_stack.push_back(eval_arg(arg)); + } + object * r = apply_n(var(expr_ap_fun(e)), expr_ap_args(e).size(), &m_arg_stack[old_size]); + m_arg_stack.resize(old_size); + return r; + } + case expr_kind::Box: + return var(expr_box_obj(e)); + case expr_kind::Unbox: + return var(expr_unbox_obj(e)); + case expr_kind::Lit: + switch (lit_val_tag(expr_lit_val(e))) { + case lit_val_kind::Num: { + nat const & n = lit_val_num(expr_lit_val(e)); + switch (t) { + case type::Float: throw exception("floats are not supported yet"); + case type::UInt8: return n.raw(); + case type::UInt16: return n.raw(); + case type::UInt32: return box_uint32(n.get_small_value()); + case type::UInt64: return box_uint64(n.get_small_value()); + case type::USize: return box_size_t(n.get_small_value()); + case type::Object: + case type::TObject: + return n.to_obj_arg(); + default: + throw exception("invalid instruction"); + } + } + case lit_val_kind::Str: + return lit_val_str(expr_lit_val(e)).to_obj_arg(); + } + case expr_kind::IsShared: + return box(!is_exclusive(var(expr_is_shared_obj(e)))); + case expr_kind::IsTaggedPtr: + return box(!is_scalar(var(expr_is_tagged_ptr_obj(e)))); + default: + throw exception(sstream() << "unexpected instruction kind " << static_cast(expr_tag(e))); + } + } + + object * eval_body(fn_body const & b0) { + // make reference reassignable... + std::reference_wrapper b(b0); + while (true) { + switch (fn_body_tag(b)) { + case fn_body_kind::VDecl: + var(fn_body_vdecl_var(b)) = eval_expr(fn_body_vdecl_expr(b), fn_body_vdecl_type(b)); + b = fn_body_vdecl_cont(b); + break; + case fn_body_kind::JDecl: { + size_t i = get_frame().m_jp_bp + fn_body_jdecl_id(b).get_small_value(); + if (i >= m_jp_stack.size()) { + m_jp_stack.resize(i + 1); + } + m_jp_stack[i] = &b.get(); + b = fn_body_jdecl_cont(b); + break; + } + case fn_body_kind::Set: { + object * o = var(fn_body_set_var(b)); + lean_assert(is_exclusive(o)); + cnstr_set(o, fn_body_set_idx(b).get_small_value(), eval_arg(fn_body_set_arg(b))); + b = fn_body_set_cont(b); + break; + } + case fn_body_kind::SetTag: { + object * o = var(fn_body_set_tag_var(b)); + lean_assert(is_exclusive(o)); + cnstr_set_tag(o, fn_body_set_tag_cidx(b).get_small_value()); + b = fn_body_set_tag_cont(b); + break; + } + case fn_body_kind::USet: { + object * o = var(fn_body_uset_var(b)); + lean_assert(is_exclusive(o)); + cnstr_set_usize(o, fn_body_uset_idx(b).get_small_value(), unbox_size_t(eval_arg(fn_body_uset_arg(b)))); + b = fn_body_uset_cont(b); + break; + } + case fn_body_kind::SSet: { + object * o = var(fn_body_sset_target(b)); + size_t offset = fn_body_sset_num_objs(b).get_small_value() * sizeof(void *) + + fn_body_sset_offset(b).get_small_value(); + object * v = var(fn_body_sset_source(b)); + lean_assert(is_exclusive(o)); + switch (fn_body_sset_type(b)) { + case type::Float: throw exception("floats are not supported yet"); + case type::UInt8: cnstr_set_uint8(o, offset, unbox(v)); break; + case type::UInt16: cnstr_set_uint16(o, offset, unbox(v)); break; + case type::UInt32: cnstr_set_uint32(o, offset, unbox_uint32(v)); break; + case type::UInt64: cnstr_set_uint64(o, offset, unbox_uint64(v)); break; + default: throw exception(sstream() << "invalid instruction"); + } + b = fn_body_sset_cont(b); + break; + } + case fn_body_kind::Inc: + inc(var(fn_body_inc_var(b)), fn_body_inc_val(b).get_small_value()); + b = fn_body_inc_cont(b); + break; + case fn_body_kind::Dec: { + size_t n = fn_body_dec_val(b).get_small_value(); + for (size_t i = 0; i < n; i++) { + dec(var(fn_body_dec_var(b))); + } + b = fn_body_dec_cont(b); + break; + } + case fn_body_kind::Del: + lean_free_object(var(fn_body_del_var(b))); + b = fn_body_del_cont(b); + break; + case fn_body_kind::MData: + b = fn_body_mdata_cont(b); + break; + case fn_body_kind::Case: { + object * o = var(fn_body_case_var(b)); + size_t tag = is_scalar(o) ? unbox(o) : cnstr_tag(o); + for (alt_core const & a : fn_body_case_alts(b)) { + switch (alt_core_tag(a)) { + case alt_core_kind::Ctor: + if (tag == ctor_info_idx(alt_core_ctor_info(a)).get_small_value()) { + b = alt_core_ctor_cont(a); + goto done; + } + break; + case alt_core_kind::Default: + b = alt_core_default_cont(a); + goto done; + } + } + throw exception("incomplete case"); + done: break; + } + case fn_body_kind::Ret: + return eval_arg(fn_body_ret_arg(b)); + case fn_body_kind::Jmp: { + fn_body const & jp = *m_jp_stack[get_frame().m_jp_bp + fn_body_jmp_jp(b).get_small_value()]; + lean_assert(fn_body_jdecl_params(jp).size() == fn_body_jmp_args(b).size()); + for (size_t i = 0; i < fn_body_jdecl_params(jp).size(); i++) { + var(param_var(fn_body_jdecl_params(jp)[i])) = eval_arg(fn_body_jmp_args(b)[i]); + } + b = fn_body_jdecl_body(jp); + break; + } + case fn_body_kind::Unreachable: + throw exception("unreachable code"); + } + } + } + + void push_frame(name const & fn, size_t arg_sp) { + m_call_stack.push_back(frame { fn, arg_sp, m_jp_stack.size() }); + } + + void pop_frame() { + m_arg_stack.resize(get_frame().m_arg_bp); + m_jp_stack.resize(get_frame().m_jp_bp); + m_call_stack.pop_back(); + } + + void * get_symbol_pointer(name const & fn, bool & boxed) { + string_ref mangled = name_mangle(fn, *g_mangle_prefix); + string_ref boxed_mangled(string_append(mangled.to_obj_arg(), g_boxed_mangled_suffix->raw())); + if (void * p_boxed = dlsym(RTLD_DEFAULT, boxed_mangled.data())) { + boxed = true; + return p_boxed; + } else if (void * p = dlsym(RTLD_DEFAULT, mangled.data())) { + boxed = false; + return p; + } else { + return nullptr; + } + } + + void * get_symbol_pointer(name const & fn) { + bool boxed; + return get_symbol_pointer(fn, boxed); + } + + decl get_decl(name const & fn) { + option_ref d = find_env_decl(m_env, fn); + if (!d) { + throw exception(sstream() << "unknown declaration '" << fn << "'"); + } + return d.get().value(); + } + + decl get_fdecl(name const & fn) { + decl d = get_decl(fn); + if (decl_tag(d) == decl_kind::Extern) { + throw exception(sstream() << "unexpected external declaration '" << fn << "'"); + } + return d; + } + + // evaluate 0-ary function + object * load(name const & fn, type t) { + if (void * p = get_symbol_pointer(fn)) { + switch (t) { + case type::Float: throw exception("floats are not supported yet"); + case type::UInt8: return box(*static_cast(p)); + case type::UInt16: return box(*static_cast(p)); + case type::UInt32: return box_uint32(*static_cast(p)); + case type::UInt64: return box_uint64(*static_cast(p)); + case type::USize: return box_size_t(*static_cast(p)); + case type::Object: + case type::TObject: + return *static_cast(p); + default: + throw exception("invalid type"); + } + } else { + // TODO(Sebastian): cache + push_frame(fn, m_arg_stack.size()); + decl d = get_fdecl(fn); + object * r = eval_body(decl_fun_body(d)); + pop_frame(r); + return r; + } + } + + object * call(name const & fn, array_ref const & args) { + size_t old_size = m_arg_stack.size(); + + // evaluate args in old stack frame + for (const auto & arg : args) { + m_arg_stack.push_back(eval_arg(arg)); + } + + decl d = get_decl(fn); + push_frame(fn, old_size); + object * r; + bool boxed; + if (void * p = get_symbol_pointer(fn, boxed)) { + for (size_t i = 0; i < args.size(); i++) { + if (param_borrow(decl_params(d)[i])) { + inc(m_arg_stack[old_size + i]); + } + } + object * cls = alloc_closure(p, 2, 1); + r = curry(cls, args.size(), &m_arg_stack[old_size]); + free_heap_obj(cls); + } else { + if (decl_tag(d) == decl_kind::Extern) { + throw exception(sstream() << "unexpected external declaration '" << fn << "'"); + } + r = eval_body(decl_fun_body(d)); + } + pop_frame(); + return r; + } +public: + explicit interpreter(environment const & env) : m_env(env) {} + + uint32 run_main(int argc, char * argv[]) { + decl d = get_fdecl("main"); + array_ref const & params = decl_params(d); + object * w = io_mk_world(); + m_arg_stack.push_back(w); + if (params.size() == 2) { + lean_object * in = lean_box(0); + int i = argc; + while (i > 1) { + i--; + lean_object * n = lean_alloc_ctor(1, 2, 0); + lean_ctor_set(n, 0, lean_mk_string(argv[i])); + lean_ctor_set(n, 1, in); + in = n; + } + m_arg_stack.push_back(in); + } else { + lean_assert(params.size() == 1); + } + push_frame("main", 0); + w = eval_body(decl_fun_body(d)); + pop_frame(); + if (io_result_is_ok(w)) { + int ret = unbox(io_result_get_value(w)); + dec_ref(w); + return ret; + } else { + io_result_show_error(w); + dec_ref(w); + return 1; + } + } + + object * stub_m(object ** args) { + decl d(args[1]); + size_t old_size = m_arg_stack.size(); + for (size_t i = 0; i < decl_params(d).size(); i++) { + m_arg_stack.push_back(args[16 + i]); + } + push_frame(decl_fun_id(d), old_size); + object * r = eval_body(decl_fun_body(d)); + pop_frame(); + return r; + } + + static object * stub_m_aux(object ** args) { + interpreter * self = reinterpret_cast(unbox(args[0])); + return self->stub_m(args); + } +}; + +uint32 run_main(environment const & env, int argv, char * argc[]) { + return interpreter(env).run_main(argv, argc); +} +} + +void initialize_ir_interpreter() { + ir::g_mangle_prefix = new string_ref("l_"); + ir::g_boxed_mangled_suffix = new string_ref("___boxed"); +} + +void finalize_ir_interpreter() { + delete ir::g_boxed_mangled_suffix; + delete ir::g_mangle_prefix; +} +} diff --git a/src/library/compiler/ir_interpreter.h b/src/library/compiler/ir_interpreter.h new file mode 100644 index 0000000000..93204ee415 --- /dev/null +++ b/src/library/compiler/ir_interpreter.h @@ -0,0 +1,17 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Sebastian Ullrich +*/ +#pragma once +#include "kernel/environment.h" +#include "runtime/object.h" + +namespace lean { +namespace ir { +uint32 run_main(environment const & env, int argv, char * argc[]); +} +void initialize_ir_interpreter(); +void finalize_ir_interpreter(); +} diff --git a/src/runtime/apply.cpp b/src/runtime/apply.cpp index 7041ad9374..dc18c6de44 100644 --- a/src/runtime/apply.cpp +++ b/src/runtime/apply.cpp @@ -74,7 +74,7 @@ typedef obj* (*fn16)(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, #define FN16(f) reinterpret_cast(lean_closure_fun(f)) typedef obj* (*fnn)(obj**); // NOLINT #define FNN(f) reinterpret_cast(lean_closure_fun(f)) -static obj* curry(obj* f, unsigned n, obj** as) { +obj* curry(obj* f, unsigned n, obj** as) { switch (n) { case 0: lean_unreachable(); case 1: return FN1(f)(as[0]); diff --git a/src/runtime/apply.h b/src/runtime/apply.h index 12302d8c1c..391f599570 100644 --- a/src/runtime/apply.h +++ b/src/runtime/apply.h @@ -7,4 +7,5 @@ Author: Leonardo de Moura #pragma once #include "runtime/object.h" namespace lean { +object * curry(object * f, unsigned n, object ** as); }