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

chore(runtime): fix assertions

Browse source
This commit is contained in:
Leonardo de Moura 2018-08-28 10:32:04 -07:00
parent 4d6da3dd69
commit 3e528a9b67
3 changed files with 10 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/runtime/object.cpp
View file

@ -139,7 +139,7 @@ void del(object * o) {
#if 0
static object * sarray_ensure_capacity(object * o, size_t extra) {
lean_assert(!is_shared(o));
lean_assert(!is_heap_obj(o) || !is_shared(o));
size_t sz = sarray_size(o);
size_t cap = sarray_capacity(o);
if (sz + extra > cap) {
@ -161,7 +161,7 @@ static object * sarray_ensure_capacity(object * o, size_t extra) {
static inline char * w_string_data(object * o) { lean_assert(is_string(o)); return reinterpret_cast<char *>(o) + sizeof(string_object); }
static object * string_ensure_capacity(object * o, size_t extra) {
lean_assert(!is_shared(o));
lean_assert(!is_heap_obj(o) || !is_shared(o));
size_t sz = string_size(o);
size_t cap = string_capacity(o);
if (sz + extra > cap) {
@ -195,7 +195,7 @@ object * mk_string(std::string const & s) {
}
object * string_push(object * s, unsigned c) {
lean_assert(!is_shared(s));
lean_assert(!is_heap_obj(s) || !is_shared(s));
object * r = string_ensure_capacity(s, 5);
size_t sz = string_size(r);
unsigned consumed = push_unicode_scalar(w_string_data(r) + sz - 1, c);
@ -206,7 +206,7 @@ object * string_push(object * s, unsigned c) {
}
object * string_append(object * s1, object * s2) {
lean_assert(!is_shared(s1));
lean_assert(!is_heap_obj(s1) || !is_shared(s1));
lean_assert(s1 != s2);
size_t sz1 = string_size(s1);
size_t sz2 = string_size(s2);

11
src/runtime/object.h
View file

@ -174,7 +174,6 @@ void del(object * o);
static_assert(sizeof(atomic<rc_type>) == sizeof(rc_type), "atomic<rc_type> and rc_type must have the same size"); // NOLINT
inline void * alloc_heap_object(size_t sz) {
void * r = malloc(sizeof(rc_type) + sz);
*static_cast<rc_type *>(r) = 1;
@ -268,7 +267,7 @@ inline T obj_data(object * o, size_t offset) {
/* Set object data of type T */
template<typename T>
inline void obj_set_data(object * o, size_t offset, T v) {
lean_assert(!is_shared(o));
lean_assert(!is_heap_obj(o) || !is_shared(o));
lean_assert(obj_header_size(o) <= offset);
lean_assert(offset + sizeof(T) <= obj_byte_size(o));
*(reinterpret_cast<T *>(reinterpret_cast<char *>(o) + offset)) = v;
@ -439,7 +438,7 @@ template<typename T> inline T cnstr_scalar(b_obj_arg o, size_t offset) {
}
/* Update constructor field `i` */
inline void cnstr_set_obj(u_obj_arg o, unsigned i, obj_arg v) {
lean_assert(!is_shared(o));
lean_assert(!is_heap_obj(o) || !is_shared(o));
lean_assert(i < cnstr_num_objs(o));
obj_set_data(o, sizeof(constructor_object) + sizeof(object*)*i, v); // NOLINT
}
@ -479,12 +478,12 @@ inline b_obj_res array_obj(b_obj_arg o, size_t i) {
}
inline void array_set_size(u_obj_arg o, size_t sz) {
lean_assert(is_array(o));
lean_assert(!is_shared(o));
lean_assert(!is_heap_obj(o) || !is_shared(o));
lean_assert(sz <= array_capacity(o));
to_array(o)->m_size = sz;
}
inline void array_set_obj(u_obj_arg o, size_t i, obj_arg v) {
lean_assert(!is_shared(o));
lean_assert(!is_heap_obj(o) || !is_shared(o));
lean_assert(i < array_size(o));
obj_set_data(o, sizeof(array_object) + sizeof(object*)*i, v); // NOLINT
}
@ -502,7 +501,7 @@ template<typename T> void sarray_set_data(u_obj_arg o, size_t i, T v) {
}
inline void sarray_set_size(u_obj_arg o, size_t sz) {
lean_assert(is_sarray(o));
lean_assert(!is_shared(o));
lean_assert(!is_heap_obj(o) || !is_shared(o));
lean_assert(sz <= sarray_capacity(o));
to_sarray(o)->m_size = sz;
}

2
src/util/object_ref.h
View file

@ -14,7 +14,7 @@ class object_ref {
object * m_obj;
public:
object_ref():m_obj(box(0)) {}
explicit object_ref(object * o):m_obj(o) { lean_assert(is_scalar(o) || get_rc(o) > 0); }
explicit object_ref(object * o):m_obj(o) { lean_assert(is_scalar(o) || !is_heap_obj(o) || get_rc(o) > 0); }
object_ref(object_ref const & s):m_obj(s.m_obj) { inc(m_obj); }
object_ref(object_ref && s):m_obj(s.m_obj) { s.m_obj = box(0); }
~object_ref() { dec(m_obj); }