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

feat(library/compiler/llnf): given y := _unbox.n x, mark x as an unboxed scalar if n < sizeof(void*)

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-18 20:52:02 -08:00
parent fe4b1509ba
commit 00aa78fffc
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/compiler/llnf.cpp
View file

@ -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));
}