max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: potential Array.get!Internal leaks part 2 (#13148)

Browse source 
Part 2 for #13147, adding the necessary constant semantics to the
interpreter.
This commit is contained in:
Henrik Böving 2026-03-27 03:51:39 +01:00 • committed by GitHub
parent bc5210d52a
commit fee2d7a6e8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/ir_interpreter.cpp
View file

@ -882,9 +882,6 @@ private:
auto cached_entry = m_constant_cache.find(fn);
if (cached_entry != m_constant_cache.end()) {
auto cached = cached_entry->second;
if (!cached.m_is_scalar) {
inc(cached.m_val.m_obj);
}
return cached.m_val;
}
auto o_entry = g_init_globals->find(fn);
@ -931,9 +928,6 @@ private:
lean_always_assert(fn_body_tag(decl_fun_body(e.m_decl)) != fn_body_kind::Unreachable);
value r = eval_body(decl_fun_body(e.m_decl));
pop_frame(r, decl_type(e.m_decl));
if (!type_is_scalar(t)) {
inc(r.m_obj);
}
m_constant_cache.insert({ fn, constant_cache_entry { type_is_scalar(t), r } });
return r;
}
@ -1073,7 +1067,11 @@ public:
unsigned arity = decl_params(e.m_decl).size();
object * r;
if (arity == 0) {
r = box_t(load(fn, decl_type(e.m_decl)), decl_type(e.m_decl));
type t = decl_type(e.m_decl);
r = box_t(load(fn, t), t);
if (!type_is_scalar(t)) {
inc(r);
}
} else {
// First allocate a closure with zero fixed parameters. This is slightly wasteful in the under-application
// case, but simpler to handle.