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

feat(util/lean_obj): add static_assert's to make the assumptions used in the object GC explicit

Browse source
This commit is contained in:
Leonardo de Moura 2018-04-20 11:16:58 -07:00
parent a7688a10b8
commit 5cac9ee01d
2 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/lean_obj.cpp
View file

@ -37,11 +37,15 @@ size_t obj_header_size(lean_obj * o) {
/* We use the field m_rc to implement a linked list of lean objects to be deleted.
This hack is safe because m_rc has type uintptr_t. */
static_assert(sizeof(atomic<rc_type>) == sizeof(lean_obj*), "unexpected atomic<rc_type> size, the object GC assumes these two types have the same size");
inline lean_obj * get_next(lean_obj * o) {
static_assert(o == static_cast<void*>(&(o->m_rc)), "the object GC relies on the fact that the first field of a structure is stored at offset 0");
return *reinterpret_cast<lean_obj**>(o);
}
inline void set_next(lean_obj * o, lean_obj * n) {
static_assert(o == static_cast<void*>(&(o->m_rc)), "the object GC relies on the fact that the first field of a structure is stored at offset 0");
*reinterpret_cast<lean_obj**>(o) = n;
}

8
src/util/lean_obj.h
View file

@ -189,7 +189,13 @@ inline lean_obj * alloc_mpz(mpz const & m) {
return new lean_mpz(m);
}
/* The memory associated with all Lean objects but mpz and external can be deallocated using `free`. */
/* The memory associated with all Lean objects but `lean_mpz` and `lean_external` can be deallocated using `free`.
All fields in these objects are integral types, but `std::atomic<uintptr_t> m_rc`.
However, `std::atomic<Integral>` has a trivial destructor.
In the C++ reference manual (http://en.cppreference.com/w/cpp/atomic/atomic), we find the following sentence:
"Additionally, the resulting std::atomic<Integral> specialization has standard layout, a trivial default constructor,
and a trivial destructor." */
inline void dealloc_mpz(lean_obj * o) { delete to_mpz(o); }
inline void dealloc_external(lean_obj * o) { delete to_external(o); }