From d45cc4cb7bf95adf983d4976845e976beb840ce0 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 26 Jul 2019 20:42:24 +0200 Subject: [PATCH] fix(kernel): manually align unboxed fields --- src/kernel/expr.cpp | 10 +++++----- src/kernel/local_ctx.cpp | 8 ++++---- src/kernel/local_ctx.h | 4 ++-- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index aeff83715b..54b1d3e471 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -136,18 +136,18 @@ inline constexpr unsigned reflected_offset(expr_kind k) { inline constexpr unsigned hash_offset(expr_kind k) { return - k == expr_kind::FVar ? scalar_offset(k) + sizeof(unsigned char) : // for binder_info, TODO(Leo): delete after we remove support for legacy code - k == expr_kind::Lambda ? scalar_offset(k) + sizeof(unsigned char) : // for binder_info - k == expr_kind::Pi ? scalar_offset(k) + sizeof(unsigned char) : // for binder_info + k == expr_kind::FVar ? scalar_offset(k) + sizeof(unsigned) : // for binder_info, TODO(Leo): delete after we remove support for legacy code + k == expr_kind::Lambda ? scalar_offset(k) + sizeof(unsigned) : // for binder_info + k == expr_kind::Pi ? scalar_offset(k) + sizeof(unsigned) : // for binder_info scalar_offset(k); } inline constexpr size_t flags_offset(expr_kind k) { return hash_offset(k) + sizeof(unsigned); } -inline constexpr size_t weight_offset(expr_kind k) { return flags_offset(k) + sizeof(unsigned char); } +inline constexpr size_t weight_offset(expr_kind k) { return flags_offset(k) + sizeof(unsigned); } inline constexpr size_t depth_offset(expr_kind k) { return weight_offset(k) + sizeof(unsigned); } inline constexpr size_t loose_bvar_range_offset(expr_kind k) { return depth_offset(k) + sizeof(unsigned); } /* Size for scalar value area for non recursive expression. */ -inline constexpr size_t expr_scalar_size(expr_kind k) { return flags_offset(k) + sizeof(unsigned char); } +inline constexpr size_t expr_scalar_size(expr_kind k) { return flags_offset(k) + sizeof(unsigned); } /* Size for scalar value area for recursive expression. */ inline constexpr size_t rec_expr_scalar_size(expr_kind k) { return loose_bvar_range_offset(k) + sizeof(unsigned); } diff --git a/src/kernel/local_ctx.cpp b/src/kernel/local_ctx.cpp index f984c87d37..d0c8644ac3 100644 --- a/src/kernel/local_ctx.cpp +++ b/src/kernel/local_ctx.cpp @@ -25,14 +25,14 @@ local_decl::local_decl():object_ref(*g_dummy_decl) {} local_decl::local_decl(unsigned idx, name const & n, name const & un, expr const & t, expr const & v): object_ref(mk_cnstr(0, n, un, t, v, sizeof(unsigned) + sizeof(unsigned char))) { - cnstr_set_scalar(raw(), sizeof(object*)*4, 0); - cnstr_set_scalar(raw(), sizeof(object*)*4+sizeof(unsigned char), idx); + cnstr_set_scalar(raw(), sizeof(object*)*4, idx); + cnstr_set_scalar(raw(), sizeof(object*)*4+sizeof(unsigned), 0); } local_decl::local_decl(unsigned idx, name const & n, name const & un, expr const & t, binder_info bi): object_ref(mk_cnstr(0, n, un, t, object_ref(box(0)), sizeof(unsigned) + sizeof(unsigned char))) { - cnstr_set_scalar(raw(), sizeof(object*)*4, static_cast(bi)); - cnstr_set_scalar(raw(), sizeof(object*)*4+sizeof(unsigned char), idx); + cnstr_set_scalar(raw(), sizeof(object*)*4, idx); + cnstr_set_scalar(raw(), sizeof(object*)*4+sizeof(unsigned), static_cast(bi)); } local_decl::local_decl(local_decl const & d, expr const & t, expr const & v): diff --git a/src/kernel/local_ctx.h b/src/kernel/local_ctx.h index be54d23ef2..a7b4554841 100644 --- a/src/kernel/local_ctx.h +++ b/src/kernel/local_ctx.h @@ -34,8 +34,8 @@ public: if (is_scalar(cnstr_get(raw(), 3))) return none_expr(); else return some_expr(static_cast(cnstr_get_ref(raw(), 3))); } - binder_info get_info() const { return static_cast(cnstr_get_scalar(raw(), sizeof(object*)*4)); } - unsigned get_idx() const { return cnstr_get_scalar(raw(), sizeof(object*)*4+sizeof(unsigned char)); } + unsigned get_idx() const { return cnstr_get_scalar(raw(), sizeof(object*)*4); } + binder_info get_info() const { return static_cast(cnstr_get_scalar(raw(), sizeof(object*)*4+sizeof(unsigned))); } expr mk_ref() const; };