fix(kernel/environment): add weak reference to environment objects

We need weak references to environment objects because the environment has a reference to the type_checker and the type_checker has a reference back to the environment. Before, we were breaking the cycle using an "environment const &". This was a dangerous hack because the environment smart pointer passed to the type_checker could be on the stack. The weak_ref is much safer.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/frontend.cpp

@@ -352,7 +352,11 @@ struct lean_extension_initializer {
 
 static lean_extension_initializer g_lean_extension_initializer;
 
-static lean_extension & to_ext(environment const & env) {
+static lean_extension const & to_ext(environment const & env) {
+    return env.get_extension<lean_extension>(g_lean_extension_initializer.m_extid);
+}
+
+static lean_extension & to_ext(environment & env) {
     return env.get_extension<lean_extension>(g_lean_extension_initializer.m_extid);
 }
 

src/frontends/lean/frontend.h

@@ -33,6 +33,8 @@ public:
 
     environment const & get_environment() const { return m_env; }
     operator environment const &() const { return get_environment(); }
+    environment & get_environment() { return m_env; }
+    operator environment &() { return get_environment(); }
 
     /**
        @name Environment API
@@ -179,6 +181,8 @@ public:
     /*@{*/
     state const & get_state() const { return m_state; }
     operator state const &() const { return m_state; }
+    state & get_state() { return m_state; }
+    operator state &() { return m_state; }
     options get_options() const { return m_state.get_options(); }
     void set_options(options const & opts) { return m_state.set_options(opts); }
     template<typename T> void set_option(name const & n, T const & v) { m_state.set_option(n, v); }

src/kernel/environment.cpp

@@ -65,14 +65,12 @@ struct environment::imp {
     // Object management
     std::vector<object>                  m_objects;
     object_dictionary                    m_object_dictionary;
-    type_checker                         m_type_checker;
+    std::unique_ptr<type_checker>        m_type_checker;
 
     std::vector<std::unique_ptr<extension>> m_extensions;
     friend class extension;
 
-    extension & get_extension_core(unsigned extid, environment const & env) {
+    extension & get_extension_core(unsigned extid) {
-        if (has_children())
-            throw read_only_environment_exception(env);
         if (extid >= m_extensions.size())
             m_extensions.resize(extid+1);
         if (!m_extensions[extid]) {
@@ -288,9 +286,9 @@ struct environment::imp {
         infer_universe and infer_type expect an environment instead of environment::imp.
     */
     void check_type(name const & n, expr const & t, expr const & v, environment const & env) {
-        m_type_checker.check_type(t);
+        m_type_checker->check_type(t);
-        expr v_t = m_type_checker.infer_type(v);
+        expr v_t = m_type_checker->infer_type(v);
-        if (!m_type_checker.is_convertible(v_t, t))
+        if (!m_type_checker->is_convertible(v_t, t))
             throw def_type_mismatch_exception(env, n, t, v, v_t);
     }
 
@@ -335,7 +333,7 @@ struct environment::imp {
     */
     void add_definition(name const & n, expr const & v, bool opaque, environment const & env) {
         check_name(n, env);
-        expr v_t = m_type_checker.infer_type(v);
+        expr v_t = m_type_checker->infer_type(v);
         unsigned w = get_max_weight(v) + 1;
         register_named_object(mk_definition(n, v_t, v, opaque, w));
     }
@@ -349,14 +347,14 @@ struct environment::imp {
     /** \brief Add new axiom. */
     void add_axiom(name const & n, expr const & t, environment const & env) {
         check_name(n, env);
-        m_type_checker.check_type(t);
+        m_type_checker->check_type(t);
         register_named_object(mk_axiom(n, t));
     }
 
     /** \brief Add new variable. */
     void add_var(name const & n, expr const & t, environment const & env) {
         check_name(n, env);
-        m_type_checker.check_type(t);
+        m_type_checker->check_type(t);
         register_named_object(mk_var_decl(n, t));
     }
 
@@ -381,11 +379,11 @@ struct environment::imp {
     }
 
     expr infer_type(expr const & e, context const & ctx) {
-        return m_type_checker.infer_type(e, ctx);
+        return m_type_checker->infer_type(e, ctx);
     }
 
     expr normalize(expr const & e, context const & ctx) {
-        return m_type_checker.get_normalizer()(e, ctx);
+        return m_type_checker->get_normalizer()(e, ctx);
     }
 
     /** \brief Display universal variable constraints and objects stored in this environment and its parents. */
@@ -400,19 +398,17 @@ struct environment::imp {
     }
 
     void set_interrupt(bool flag) {
-        m_type_checker.set_interrupt(flag);
+        m_type_checker->set_interrupt(flag);
     }
 
-    imp(environment const & env):
+    imp():
-        m_num_children(0),
+        m_num_children(0) {
-        m_type_checker(env) {
         init_uvars();
     }
 
-    imp(std::shared_ptr<imp> const & parent, environment const & env):
+    imp(std::shared_ptr<imp> const & parent):
         m_num_children(0),
-        m_parent(parent),
+        m_parent(parent) {
-        m_type_checker(env) {
         m_parent->inc_children();
     }
 
@@ -423,12 +419,14 @@ struct environment::imp {
 };
 
 environment::environment():
-    m_ptr(new imp(*this)) {
+    m_ptr(new imp()) {
+    m_ptr->m_type_checker.reset(new type_checker(*this));
 }
 
 // used when creating a new child environment
 environment::environment(std::shared_ptr<imp> const & parent, bool):
-    m_ptr(new imp(parent, *this)) {
+    m_ptr(new imp(parent)) {
+    m_ptr->m_type_checker.reset(new type_checker(*this));
 }
 
 // used when creating a reference to the parent environment
@@ -532,8 +530,12 @@ void environment::set_interrupt(bool flag) {
     m_ptr->set_interrupt(flag);
 }
 
-environment::extension & environment::get_extension_core(unsigned extid) const {
+environment::extension const & environment::get_extension_core(unsigned extid) const {
-    return m_ptr->get_extension_core(extid, *this);
+    return m_ptr->get_extension_core(extid);
+}
+
+environment::extension & environment::get_extension_core(unsigned extid) {
+    return m_ptr->get_extension_core(extid);
 }
 
 environment::extension::extension():

src/kernel/environment.h

@@ -23,7 +23,6 @@ private:
     void check_type(name const & n, expr const & t, expr const & v);
     environment(std::shared_ptr<imp> const & parent, bool);
     explicit environment(std::shared_ptr<imp> const & ptr);
-    explicit environment(imp * new_ptr);
     unsigned get_num_objects(bool local) const;
     object const & get_object(unsigned i, bool local) const;
 public:
@@ -253,7 +252,8 @@ public:
     static unsigned register_extension(mk_extension mk);
 
 private:
-    extension & get_extension_core(unsigned extid) const;
+    extension const & get_extension_core(unsigned extid) const;
+    extension & get_extension_core(unsigned extid);
 
 public:
     /**
@@ -261,10 +261,22 @@ public:
        The token is the value returned by \c register_extension.
     */
     template<typename Ext>
-    Ext & get_extension(unsigned extid) const {
+    Ext const & get_extension(unsigned extid) const {
+        extension const & ext = get_extension_core(extid);
+        lean_assert(dynamic_cast<Ext const *>(&ext) != nullptr);
+        return static_cast<Ext const &>(ext);
+    }
+
+    template<typename Ext>
+    Ext & get_extension(unsigned extid) {
         extension & ext = get_extension_core(extid);
         lean_assert(dynamic_cast<Ext*>(&ext) != nullptr);
         return static_cast<Ext&>(ext);
     }
+
+public:
+    typedef std::weak_ptr<imp> weak_ref;
+    weak_ref to_weak_ref() const { return weak_ref(m_ptr); }
+    environment(weak_ref const & r):m_ptr(r) { lean_assert(!r.expired()); }
 };
 }

src/kernel/normalizer.cpp

@@ -69,12 +69,14 @@ value_stack extend(value_stack const & s, svalue const & v) { return cons(v, s);
 class normalizer::imp {
     typedef scoped_map<expr, svalue, expr_hash, expr_eqp> cache;
 
-    environment const &  m_env;
+    environment::weak_ref m_env;
-    context              m_ctx;
+    context               m_ctx;
-    cache                m_cache;
+    cache                 m_cache;
-    unsigned             m_max_depth;
+    unsigned              m_max_depth;
-    unsigned             m_depth;
+    unsigned              m_depth;
-    volatile bool        m_interrupted;
+    volatile bool         m_interrupted;
+
+    environment env() const { return environment(m_env); }
 
     /**
         \brief Auxiliary object for saving the current context.
@@ -179,7 +181,7 @@ class normalizer::imp {
         flet<unsigned> l(m_depth, m_depth+1);
         check_interrupted(m_interrupted);
         if (m_depth > m_max_depth)
-            throw kernel_exception(m_env, "normalizer maximum recursion depth exceeded");
+            throw kernel_exception(env(), "normalizer maximum recursion depth exceeded");
         bool shared = false;
         if (is_shared(a)) {
             shared = true;
@@ -197,7 +199,7 @@ class normalizer::imp {
             r = lookup(s, var_idx(a));
             break;
         case expr_kind::Constant: {
-            object const & obj = m_env.get_object(const_name(a));
+            object const & obj = env().get_object(const_name(a));
             if (obj.is_definition() && !obj.is_opaque()) {
                 r = normalize(obj.get_value(), value_stack(), 0);
             } else {
@@ -291,7 +293,7 @@ class normalizer::imp {
 
 public:
     imp(environment const & env, unsigned max_depth):
-        m_env(env) {
+        m_env(env.to_weak_ref()) {
         m_interrupted    = false;
         m_max_depth      = max_depth;
         m_depth          = 0;

src/kernel/type_checker.cpp

@@ -22,7 +22,7 @@ class type_checker::imp {
     typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
     typedef buffer<unification_constraint> unification_constraints;
 
-    environment const &       m_env;
+    environment::weak_ref     m_env;
     cache                     m_cache;
     normalizer                m_normalizer;
     context                   m_ctx;
@@ -31,6 +31,10 @@ class type_checker::imp {
     unification_constraints * m_uc;
     volatile bool             m_interrupted;
 
+    environment env() const {
+        return environment(m_env);
+    }
+
     expr normalize(expr const & e, context const & ctx) {
         return m_normalizer(e, ctx);
     }
@@ -59,7 +63,7 @@ class type_checker::imp {
             m_uc->push_back(mk_eq_constraint(ctx, r, p, jst));
             return p;
         }
-        throw function_expected_exception(m_env, ctx, s);
+        throw function_expected_exception(env(), ctx, s);
     }
 
     expr check_type(expr const & e, expr const & s, context const & ctx) {
@@ -77,7 +81,7 @@ class type_checker::imp {
             m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, jst));
             return u;
         }
-        throw type_expected_exception(m_env, ctx, s);
+        throw type_expected_exception(env(), ctx, s);
     }
 
     expr infer_type_core(expr const & e, context const & ctx) {
@@ -99,11 +103,11 @@ class type_checker::imp {
                 else
                     return m_menv->get_type(e);
             } else {
-                throw unexpected_metavar_occurrence(m_env, e);
+                throw unexpected_metavar_occurrence(env(), e);
             }
             break;
         case expr_kind::Constant:
-            r = m_env.get_object(const_name(e)).get_type();
+            r = env().get_object(const_name(e)).get_type();
             break;
         case expr_kind::Var:
             r = lookup(ctx, var_idx(e));
@@ -125,7 +129,7 @@ class type_checker::imp {
                 expr const & c_t = arg_types[i];
                 auto mk_justification = [&](){ return mk_app_type_match_justification(ctx, e, i); }; // thunk for creating justification object if needed
                 if (!is_convertible(c_t, abst_domain(f_t), ctx, mk_justification))
-                    throw app_type_mismatch_exception(m_env, ctx, e, arg_types.size(), arg_types.data());
+                    throw app_type_mismatch_exception(env(), ctx, e, arg_types.size(), arg_types.data());
                 if (closed(abst_body(f_t)))
                     f_t = abst_body(f_t);
                 else if (closed(c))
@@ -182,7 +186,7 @@ class type_checker::imp {
                 check_type(ty, let_type(e), ctx); // check if it is really a type
                 auto mk_justification = [&](){ return mk_def_type_match_justification(ctx, let_name(e), let_value(e)); }; // thunk for creating justification object if needed
                 if (!is_convertible(lt, let_type(e), ctx, mk_justification))
-                    throw def_type_mismatch_exception(m_env, ctx, let_name(e), let_type(e), let_value(e), lt);
+                    throw def_type_mismatch_exception(env(), ctx, let_name(e), let_type(e), let_value(e), lt);
             }
             {
                 cache::mk_scope sc(m_cache);
@@ -194,11 +198,11 @@ class type_checker::imp {
         case expr_kind::Value: {
             // Check if the builtin value (or its set) is declared in the environment.
             name const & n = to_value(e).get_name();
-            object const & obj = m_env.get_object(n);
+            object const & obj = env().get_object(n);
             if (obj && ((obj.is_builtin() && obj.get_value() == e) || (obj.is_builtin_set() && obj.in_builtin_set(e)))) {
                 r = to_value(e).get_type();
             } else {
-                throw invalid_builtin_value_reference(m_env, e);
+                throw invalid_builtin_value_reference(env(), e);
             }
             break;
         }
@@ -218,7 +222,7 @@ class type_checker::imp {
             expr const * e = &expected;
             while (true) {
                 if (is_type(*e) && is_type(*g)) {
-                    if (m_env.is_ge(ty_level(*e), ty_level(*g)))
+                    if (env().is_ge(ty_level(*e), ty_level(*g)))
                         return true;
                 }
 
@@ -275,7 +279,7 @@ class type_checker::imp {
 
 public:
     imp(environment const & env):
-        m_env(env),
+        m_env(env.to_weak_ref()),
         m_normalizer(env) {
         m_menv           = nullptr;
         m_menv_timestamp = 0;