From 00aa78fffc7bfc37d6156e3a2ec99863290a0f94 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Feb 2019 20:52:02 -0800 Subject: [PATCH] feat(library/compiler/llnf): given `y := _unbox.n x`, mark `x` as an unboxed scalar if `n < sizeof(void*)` --- src/library/compiler/llnf.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp index 137c4ef4a1..21001bb503 100644 --- a/src/library/compiler/llnf.cpp +++ b/src/library/compiler/llnf.cpp @@ -2026,6 +2026,12 @@ class explicit_rc_fn { expr mk_fvar(name const & n, expr const & type, expr const & val) { expr new_fvar = m_lctx.mk_local_decl(ngen(), n, type, val); m_fvars.push_back(new_fvar); + unsigned nbytes = 0; + /* If val is _unbox.nbytes(x), then x is a boxed scalar value if nbytes is small. */ + if (is_llnf_unbox(get_app_fn(val), nbytes) && (nbytes < sizeof(void*))) { + expr x = app_arg(val); + m_is_scalar.insert(fvar_name(x)); + } if (should_mark_as_borrowed(val)) { m_is_borrowed.insert(fvar_name(new_fvar)); }