From 131f2d202e904a6b83a429edf23770fd6b05ee5b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 25 Feb 2020 17:13:05 -0800 Subject: [PATCH] chore: ignore closures at maxsharing Closures may capture huge objects that user may be unaware. For example, any closure created by the interpreter contains a reference to the `Environment`. @dselsam @kha I don't see many applications for maximizing sharing in values captured by closures. If we want this feature, we should at least wrap the `Environment` and `Decl` using external objects at `mk_stub_closure` at `ir_interpreter.cpp`. --- src/runtime/maxsharing.cpp | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/runtime/maxsharing.cpp b/src/runtime/maxsharing.cpp index 045b1da3d0..71ce0d7a52 100644 --- a/src/runtime/maxsharing.cpp +++ b/src/runtime/maxsharing.cpp @@ -171,7 +171,7 @@ class max_sharing_fn { // We do not maximize sharing for the following kinds of objects case LeanMPZ: case LeanThunk: case LeanTask: case LeanRef: - case LeanExternal: + case LeanExternal: case LeanClosure: m_children.push_back(a); return true; default: @@ -216,12 +216,6 @@ class max_sharing_fn { } } - void visit_closure(b_obj_arg a) { - // TODO(Leo) - lean_inc(a); - save(a, a); - } - void visit_array(b_obj_arg a) { clear_children(); bool missing_children = false; @@ -300,7 +294,7 @@ public: b_obj_arg curr = m_todo.back(); // std::cout << "visiting " << curr << " " << static_cast(lean_ptr_tag(curr)) << "\n"; switch (lean_ptr_tag(curr)) { - case LeanClosure: visit_closure(curr); break; + case LeanClosure: lean_unreachable(); case LeanArray: visit_array(curr); break; case LeanScalarArray: visit_sarray(curr); break; case LeanString: visit_string(curr); break;