From 752b54085b8a080c1f2c473f10325b33400c8188 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 Jan 2015 12:36:56 -0800 Subject: [PATCH] refactor(kernel/type_checker): type checker should not unfold macros, but sign an error if a untrusted macro is used Now, we unfold untrusted macros outside of the Lean kernel. --- src/frontends/lean/builtin_cmds.cpp | 3 +- src/frontends/lean/decl_cmds.cpp | 24 ++++- src/frontends/lean/theorem_queue.cpp | 2 + src/kernel/type_checker.cpp | 15 +-- src/library/CMakeLists.txt | 2 +- src/library/kernel_bindings.cpp | 8 +- src/library/module.cpp | 2 + src/library/unfold_macros.cpp | 154 +++++++++++++++++++++++++++ src/library/unfold_macros.h | 21 ++++ 9 files changed, 210 insertions(+), 21 deletions(-) create mode 100644 src/library/unfold_macros.cpp create mode 100644 src/library/unfold_macros.h diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 5a2bd33d22..61b7761b1e 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -431,7 +431,8 @@ static environment add_abbrev(parser & p, environment const & env, name const & name const & ns = get_namespace(env); name full_id = ns + id; p.add_abbrev_index(full_id, d); - environment new_env = module::add(env, check(env, mk_definition(env, full_id, decl.get_univ_params(), decl.get_type(), value, opaque))); + environment new_env = + module::add(env, check(env, mk_definition(env, full_id, decl.get_univ_params(), decl.get_type(), value, opaque))); if (full_id != id) new_env = add_expr_alias_rec(new_env, id, full_id); return new_env; diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 7e8eb52237..00fe5e0dd2 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -20,6 +20,7 @@ Author: Leonardo de Moura #include "library/reducible.h" #include "library/coercion.h" #include "library/class.h" +#include "library/unfold_macros.h" #include "library/definitional/equations.h" #include "frontends/lean/parser.h" #include "frontends/lean/class.h" @@ -129,12 +130,13 @@ static environment declare_var(parser & p, environment env, lean_assert(k == variable_kind::Constant || k == variable_kind::Axiom); name const & ns = get_namespace(env); name full_n = ns + n; + expr new_type = unfold_untrusted_macros(env, type); if (k == variable_kind::Axiom) { - env = module::add(env, check(env, mk_axiom(full_n, ls, type))); - p.add_decl_index(full_n, pos, get_axiom_tk(), type); + env = module::add(env, check(env, mk_axiom(full_n, ls, new_type))); + p.add_decl_index(full_n, pos, get_axiom_tk(), new_type); } else { - env = module::add(env, check(env, mk_constant_assumption(full_n, ls, type))); - p.add_decl_index(full_n, pos, get_variable_tk(), type); + env = module::add(env, check(env, mk_constant_assumption(full_n, ls, new_type))); + p.add_decl_index(full_n, pos, get_variable_tk(), new_type); } if (!ns.is_anonymous()) env = add_expr_alias(env, n, full_n); @@ -671,6 +673,9 @@ class definition_cmd_fn { try { level_param_names c_ls; expr c_type, c_value; std::tie(c_ls, c_type, c_value) = *it; + // cache may have been created using a different trust level + c_type = unfold_untrusted_macros(m_env, c_type); + c_value = unfold_untrusted_macros(m_env, c_value); if (m_kind == Theorem) { cd = check(m_env, mk_theorem(m_real_name, c_ls, c_type, c_value)); if (!m_p.keep_new_thms()) { @@ -768,6 +773,12 @@ class definition_cmd_fn { lean_assert(aux_values.size() == m_aux_types.size()); if (aux_values.size() != m_real_aux_names.size()) throw exception("invalid declaration, failed to compile auxiliary declarations"); + m_type = unfold_untrusted_macros(m_env, m_type); + m_value = unfold_untrusted_macros(m_env, m_value); + for (unsigned i = 0; i < aux_values.size(); i++) { + m_aux_types[i] = unfold_untrusted_macros(m_env, m_aux_types[i]); + aux_values[i] = unfold_untrusted_macros(m_env, aux_values[i]); + } if (is_definition()) { m_env = module::add(m_env, check(m_env, mk_definition(m_env, m_real_name, new_ls, m_type, m_value, m_is_opaque))); @@ -798,6 +809,7 @@ class definition_cmd_fn { std::tie(m_type, new_ls) = m_p.elaborate_type(m_type, list(), clear_pre_info); check_no_metavar(m_env, m_real_name, m_type, true); m_ls = append(m_ls, new_ls); + m_type = unfold_untrusted_macros(m_env, m_type); expr type_as_is = m_p.save_pos(mk_as_is(m_type), type_pos); if (!m_p.collecting_info() && m_kind == Theorem && m_p.num_threads() > 1) { // Add as axiom, and create a task to prove the theorem. @@ -806,6 +818,8 @@ class definition_cmd_fn { m_env = module::add(m_env, check(m_env, mk_axiom(m_real_name, m_ls, m_type))); } else { std::tie(m_type, m_value, new_ls) = m_p.elaborate_definition(m_name, type_as_is, m_value, m_is_opaque); + m_type = unfold_untrusted_macros(m_env, m_type); + m_value = unfold_untrusted_macros(m_env, m_value); new_ls = append(m_ls, new_ls); auto cd = check(m_env, mk_theorem(m_real_name, new_ls, m_type, m_value)); if (m_kind == Theorem) { @@ -821,6 +835,8 @@ class definition_cmd_fn { } else { std::tie(m_type, m_value, new_ls) = m_p.elaborate_definition(m_name, m_type, m_value, m_is_opaque); new_ls = append(m_ls, new_ls); + m_type = unfold_untrusted_macros(m_env, m_type); + m_value = unfold_untrusted_macros(m_env, m_value); m_env = module::add(m_env, check(m_env, mk_definition(m_env, m_real_name, new_ls, m_type, m_value, m_is_opaque))); m_p.cache_definition(m_real_name, pre_type, pre_value, new_ls, m_type, m_value); diff --git a/src/frontends/lean/theorem_queue.cpp b/src/frontends/lean/theorem_queue.cpp index 94c022f865..f4f5ba22df 100644 --- a/src/frontends/lean/theorem_queue.cpp +++ b/src/frontends/lean/theorem_queue.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "library/unfold_macros.h" #include "kernel/type_checker.h" #include "frontends/lean/theorem_queue.h" #include "frontends/lean/parser.h" @@ -19,6 +20,7 @@ void theorem_queue::add(environment const & env, name const & n, level_param_nam bool is_opaque = true; // theorems are always opaque std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v, is_opaque); new_ls = append(ls, new_ls); + value = unfold_untrusted_macros(env, value); auto r = check(env, mk_theorem(n, new_ls, type, value)); m_parser.cache_definition(n, t, v, new_ls, type, value); return r; diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 555ed28e14..0c6e05f5a5 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -192,19 +192,10 @@ pair type_checker::infer_macro(expr const & e, bool infer_ expr t = tcs.first; constraint_seq cs = tcs.second; if (!infer_only && def.trust_level() >= m_env.trust_lvl()) { - optional m = expand_macro(e); - if (!m) - throw_kernel_exception(m_env, "failed to expand macro", e); - pair tmcs = infer_type_core(*m, infer_only); - cs = cs + tmcs.second; - simple_delayed_justification jst([=]() { return mk_macro_jst(e); }); - pair bcs = is_def_eq(t, tmcs.first, jst); - if (!bcs.first) - throw_kernel_exception(m_env, g_macro_error_msg, e); - return mk_pair(t, bcs.second + cs); - } else { - return mk_pair(t, cs); + throw_kernel_exception(m_env, "declaration contains macro with trust-level higher than the one allowed " + "(possible solution: unfold macro, or increase trust-level)", e); } + return mk_pair(t, cs); } pair type_checker::infer_lambda(expr const & _e, bool infer_only) { diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 18e3922a2e..eef1617103 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -11,6 +11,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp typed_expr.cpp let.cpp type_util.cpp protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp - local_context.cpp choice_iterator.cpp pp_options.cpp) + local_context.cpp choice_iterator.cpp pp_options.cpp unfold_macros.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 9b6a73f843..50629a28f3 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -31,6 +31,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/reducible.h" #include "library/print.h" +#include "library/unfold_macros.h" // Lua Bindings for the Kernel classes. We do not include the Lua // bindings in the kernel because we do not want to inflate the Kernel. @@ -1905,14 +1906,15 @@ static int type_check(lua_State * L) { static int add_declaration(lua_State * L) { int nargs = lua_gettop(L); optional d; + environment const & env = to_environment(L, 1); if (nargs == 2) { - d = check(to_environment(L, 1), to_declaration(L, 2)); + d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2))); } else if (nargs == 3) { - d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3)); + d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2)), to_name_generator(L, 3)); } else { name_set extra_opaque = to_name_set(L, 4); extra_opaque_pred pred([=](name const & n) { return extra_opaque.contains(n); }); - d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), pred); + d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2)), to_name_generator(L, 3), pred); } return push_environment(L, module::add(to_environment(L, 1), *d)); } diff --git a/src/library/module.cpp b/src/library/module.cpp index 198a04973b..0302ea9d67 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -23,6 +23,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/sorry.h" #include "library/kernel_serializer.h" +#include "library/unfold_macros.h" #include "version.h" #ifndef LEAN_ASYNCH_IMPORT_THEOREM @@ -357,6 +358,7 @@ struct import_modules_fn { declaration decl = read_declaration(d, midx); lean_assert(!decl.is_definition() || decl.get_module_idx() == midx); environment env = m_senv.env(); + decl = unfold_untrusted_macros(env, decl); if (decl.get_name() == get_sorry_name() && has_sorry(env)) return; if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) { diff --git a/src/library/unfold_macros.cpp b/src/library/unfold_macros.cpp new file mode 100644 index 0000000000..28206b06c3 --- /dev/null +++ b/src/library/unfold_macros.cpp @@ -0,0 +1,154 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/interrupt.h" +#include "kernel/type_checker.h" +#include "kernel/find_fn.h" +#include "kernel/expr_maps.h" +#include "kernel/instantiate.h" +#include "kernel/abstract.h" +#include "library/unfold_macros.h" +#include "library/replace_visitor.h" +#include "library/generic_exception.h" + +namespace lean { +class unfold_untrusted_macros_fn { + typedef expr_bi_struct_map cache; + + type_checker m_tc; + unsigned m_trust_lvl; + cache m_cache; + + expr save_result(expr const & e, expr && r) { + m_cache.insert(std::make_pair(e, r)); + return r; + } + + expr visit_macro(expr const & e) { + buffer new_args; + for (unsigned i = 0; i < macro_num_args(e); i++) + new_args.push_back(visit(macro_arg(e, i))); + auto def = macro_def(e); + expr r = update_macro(e, new_args.size(), new_args.data()); + if (def.trust_level() >= m_trust_lvl) { + if (optional new_r = m_tc.expand_macro(r)) { + return *new_r; + } else { + throw_generic_exception("failed to expand macro", e); + } + } else { + return r; + } + } + + expr visit_app(expr const & e) { + expr new_f = visit(app_fn(e)); + expr new_v = visit(app_arg(e)); + return update_app(e, new_f, new_v); + } + + expr visit_binding(expr e) { + expr_kind k = e.kind(); + buffer es; + buffer ls; + while (e.kind() == k) { + expr d = visit(instantiate_rev(binding_domain(e), ls.size(), ls.data())); + expr l = mk_local(m_tc.mk_fresh_name(), binding_name(e), d, binding_info(e)); + ls.push_back(l); + es.push_back(e); + e = binding_body(e); + } + e = visit(instantiate_rev(e, ls.size(), ls.data())); + expr r = abstract_locals(e, ls.size(), ls.data()); + while (!ls.empty()) { + expr d = mlocal_type(ls.back()); + ls.pop_back(); + d = abstract_locals(d, ls.size(), ls.data()); + r = update_binding(es.back(), d, r); + es.pop_back(); + } + return r; + } + + expr visit(expr const & e) { + switch (e.kind()) { + case expr_kind::Sort: case expr_kind::Constant: + case expr_kind::Var: case expr_kind::Meta: + case expr_kind::Local: + return e; + default: + break; + } + + check_system("unfold macros"); + auto it = m_cache.find(e); + if (it != m_cache.end()) + return it->second; + + switch (e.kind()) { + case expr_kind::Sort: case expr_kind::Constant: + case expr_kind::Var: case expr_kind::Meta: + case expr_kind::Local: + lean_unreachable(); + case expr_kind::Macro: + return save_result(e, visit_macro(e)); + case expr_kind::App: + return save_result(e, visit_app(e)); + case expr_kind::Lambda: case expr_kind::Pi: + return save_result(e, visit_binding(e)); + } + lean_unreachable(); + } + +public: + unfold_untrusted_macros_fn(environment const & env): + m_tc(env), m_trust_lvl(env.trust_lvl()) {} + + expr operator()(expr const & e) { return visit(e); } +}; + +bool contains_untrusted_macro(unsigned trust_lvl, expr const & e) { + return static_cast(find(e, [&](expr const & e, unsigned) { + return is_macro(e) && macro_def(e).trust_level() >= trust_lvl; + })); +} + +expr unfold_untrusted_macros(environment const & env, expr const & e) { + if (contains_untrusted_macro(env.trust_lvl(), e)) { + return unfold_untrusted_macros_fn(env)(e); + } else { + return e; + } +} + +bool contains_untrusted_macro(unsigned trust_lvl, declaration const & d) { + if (contains_untrusted_macro(trust_lvl, d.get_type())) + return true; + return (d.is_definition() || d.is_theorem()) && contains_untrusted_macro(trust_lvl, d.get_value()); +} + +declaration unfold_untrusted_macros(environment const & env, declaration const & d) { + if (contains_untrusted_macro(env.trust_lvl(), d)) { + expr new_t = unfold_untrusted_macros(env, d.get_type()); + if (d.is_theorem()) { + expr new_v = unfold_untrusted_macros(env, d.get_value()); + return mk_theorem(d.get_name(), d.get_univ_params(), new_t, new_v, d.get_module_idx()); + } else if (d.is_definition()) { + expr new_v = unfold_untrusted_macros(env, d.get_value()); + return mk_definition(d.get_name(), d.get_univ_params(), new_t, new_v, + d.is_opaque(), d.get_weight(), d.get_module_idx(), d.use_conv_opt()); + } else if (d.is_axiom()) { + return mk_axiom(d.get_name(), d.get_univ_params(), new_t); + } else if (d.is_constant_assumption()) { + return mk_constant_assumption(d.get_name(), d.get_univ_params(), new_t); + } else { + lean_unreachable(); + } + } else { + return d; + } +} +} diff --git a/src/library/unfold_macros.h b/src/library/unfold_macros.h new file mode 100644 index 0000000000..d5eba9bb8f --- /dev/null +++ b/src/library/unfold_macros.h @@ -0,0 +1,21 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/environment.h" + +namespace lean { +/** \brief Unfold any macro occurring in \c e that has trust level higher than the one + allowed in \c env. + + \remark We use this function before sending declarations to the kernel. + The kernel refuses any expression containing "untrusted" macros, i.e., + macros with trust level higher than the one allowed. +*/ +expr unfold_untrusted_macros(environment const & env, expr const & e); + +declaration unfold_untrusted_macros(environment const & env, declaration const & d); +}