diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 15aab35e1..276fdbd89 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -782,6 +782,8 @@ let generate_get_or_put_ownership_function ~without_ownership_checking ctype (decl, def) +let alloc_sym = Sym.fresh_pretty "cn_alloc" + let mk_alloc_expr (ct_ : C.ctype_) : CF.GenTypes.genTypeCategory A.expression = A.( mk_expr @@ -790,7 +792,7 @@ let mk_alloc_expr (ct_ : C.ctype_) : CF.GenTypes.genTypeCategory A.expression = C.(mk_ctype_pointer no_qualifiers (mk_ctype ct_)), mk_expr (AilEcall - ( mk_expr (AilEident (Sym.fresh_pretty "alloc")), + ( mk_expr (AilEident alloc_sym), [ mk_expr (AilEsizeof (empty_qualifiers, mk_ctype ct_)) ] )) ))) @@ -1094,7 +1096,6 @@ let rec cn_to_ail_expr_aux_internal let res_ident = A.(AilEident res_sym) in let ctype_ = C.(Pointer (empty_qualifiers, mk_ctype (Struct parent_dt.cn_dt_name))) in let res_binding = create_binding res_sym (mk_ctype ctype_) in - let alloc_sym = Sym.fresh_pretty "alloc" in let fn_call = A.( AilEcast @@ -1897,9 +1898,9 @@ let generate_datatype_default_function (cn_datatype : cn_datatype) = -> struct tree * default_struct_tree(void) { - struct tree *res = alloc(sizeof(struct tree)); + struct tree *res = cn_alloc(sizeof(struct tree)); res->tag = TREE_EMPTY; - res->u.tree_empty = alloc(sizeof(struct tree_empty)); + res->u.tree_empty = cn_alloc(sizeof(struct tree_empty)); res->u.tree_empty->k = default_cn_bits_i32(); return res; } diff --git a/runtime/libcn/include/cn-executable/alloc.h b/runtime/libcn/include/cn-executable/alloc.h index ad3a31c54..58f958426 100644 --- a/runtime/libcn/include/cn-executable/alloc.h +++ b/runtime/libcn/include/cn-executable/alloc.h @@ -1,40 +1,26 @@ #ifndef CN_ALLOC #define CN_ALLOC +#include +#include + #ifdef __cplusplus extern "C" { #endif -// enum CNTYPE { -// NODE_CN, -// SEQ, -// HASH_TABLE, -// HT_ENTRY, -// UNSIGNED_INT, -// CN_BOOL, -// CN_POINTER, -// CNTYPE_SIZE -// }; - -void *alloc_(long nbytes, const char *, int); - -#define alloc(x)\ - alloc_(x, __FILE__, __LINE__) -void *zalloc_(long nbytes, const char *, int); -#define zalloc(x)\ - zalloc_(x, __FILE__, __LINE__) +void* cn_alloc(size_t nbytes); -void free_all(void); +void* cn_zalloc(size_t nbytes); -typedef void* alloc_checkpoint; +void cn_free_all(); -alloc_checkpoint alloc_save_checkpoint(void); +typedef uintptr_t cn_alloc_checkpoint; -void free_after(alloc_checkpoint ptr); +cn_alloc_checkpoint cn_alloc_save_checkpoint(void); -// void *alloc_zeros(long nbytes); +void cn_free_after(cn_alloc_checkpoint ptr); #ifdef __cplusplus } diff --git a/runtime/libcn/include/cn-executable/utils.h b/runtime/libcn/include/cn-executable/utils.h index 80b228b25..170a79bac 100644 --- a/runtime/libcn/include/cn-executable/utils.h +++ b/runtime/libcn/include/cn-executable/utils.h @@ -208,7 +208,7 @@ cn_bool *cn_pointer_gt(cn_pointer *i1, cn_pointer *i2); #define CN_GEN_CONVERT(CTYPE, CNTYPE)\ static inline CNTYPE *convert_to_##CNTYPE(CTYPE i) {\ - CNTYPE *ret = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *ret = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ ret->val = i;\ return ret;\ } @@ -248,42 +248,42 @@ cn_bool *cn_pointer_gt(cn_pointer *i1, cn_pointer *i2); #define CN_GEN_ADD(CTYPE, CNTYPE)\ static inline CNTYPE *CNTYPE##_add(CNTYPE *i1, CNTYPE *i2) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = i1->val + i2->val;\ return res;\ } #define CN_GEN_SUB(CTYPE, CNTYPE)\ static inline CNTYPE *CNTYPE##_sub(CNTYPE *i1, CNTYPE *i2) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = i1->val - i2->val;\ return res;\ } #define CN_GEN_MUL(CTYPE, CNTYPE)\ static inline CNTYPE *CNTYPE##_multiply(CNTYPE *i1, CNTYPE *i2) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = i1->val * i2->val;\ return res;\ } #define CN_GEN_DIV(CTYPE, CNTYPE)\ static inline CNTYPE *CNTYPE##_divide(CNTYPE *i1, CNTYPE *i2) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = i1->val / i2->val;\ return res;\ } #define CN_GEN_SHIFT_LEFT(CTYPE, CNTYPE)\ static inline CNTYPE *CNTYPE##_shift_left(CNTYPE *i1, CNTYPE *i2) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = i1->val << i2->val;\ return res;\ } #define CN_GEN_SHIFT_RIGHT(CTYPE, CNTYPE)\ static inline CNTYPE *CNTYPE##_shift_right(CNTYPE *i1, CNTYPE *i2) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = i1->val >> i2->val;\ return res;\ } @@ -301,7 +301,7 @@ cn_bool *cn_pointer_gt(cn_pointer *i1, cn_pointer *i2); /* TODO: Account for UB: https://stackoverflow.com/a/20638659 */ #define CN_GEN_MOD(CTYPE, CNTYPE)\ static inline CNTYPE *CNTYPE##_mod(CNTYPE *i1, CNTYPE *i2) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = i1->val % i2->val;\ if (res->val < 0) {\ res->val = (i2->val < 0) ? res->val - i2->val : res->val + i2->val;\ @@ -312,28 +312,28 @@ cn_bool *cn_pointer_gt(cn_pointer *i1, cn_pointer *i2); #define CN_GEN_REM(CTYPE, CNTYPE)\ static inline CNTYPE *CNTYPE##_rem(CNTYPE *i1, CNTYPE *i2) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = i1->val % i2->val;\ return res;\ } #define CN_GEN_XOR(CTYPE, CNTYPE)\ static inline CNTYPE *CNTYPE##_xor(CNTYPE *i1, CNTYPE *i2) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = i1->val ^ i2->val;\ return res;\ } #define CN_GEN_BWAND(CTYPE, CNTYPE)\ static inline CNTYPE *CNTYPE##_bwand(CNTYPE *i1, CNTYPE *i2) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = i1->val & i2->val;\ return res;\ } #define CN_GEN_BWOR(CTYPE, CNTYPE)\ static inline CNTYPE *CNTYPE##_bwor(CNTYPE *i1, CNTYPE *i2) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = i1->val | i2->val;\ return res;\ } @@ -359,7 +359,7 @@ static inline int ipow(int base, int exp) #define CN_GEN_POW(CTYPE, CNTYPE)\ static inline CNTYPE *CNTYPE##_pow(CNTYPE *i1, CNTYPE *i2) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = ipow(i1->val, i2->val);\ return res;\ } @@ -382,7 +382,7 @@ static inline int ipow(int base, int exp) #define CN_GEN_PTR_ADD(CNTYPE)\ static inline cn_pointer *cn_pointer_add_##CNTYPE(cn_pointer *ptr, CNTYPE *i) {\ - cn_pointer *res = (cn_pointer *) alloc(sizeof(cn_pointer));\ + cn_pointer *res = (cn_pointer *) cn_alloc(sizeof(cn_pointer));\ res->ptr = (char *) ptr->ptr + i->val;\ return res;\ } @@ -392,14 +392,14 @@ static inline int ipow(int base, int exp) #define CN_GEN_CAST_TO_PTR(CNTYPE, INTPTR_TYPE)\ static inline cn_pointer *cast_##CNTYPE##_to_cn_pointer(CNTYPE *i) {\ - cn_pointer *res = (cn_pointer *) alloc(sizeof(cn_pointer));\ + cn_pointer *res = (cn_pointer *) cn_alloc(sizeof(cn_pointer));\ res->ptr = (void *) (INTPTR_TYPE) i->val;\ return res;\ } #define CN_GEN_CAST_FROM_PTR(CTYPE, CNTYPE, INTPTR_TYPE)\ static inline CNTYPE *cast_cn_pointer_to_##CNTYPE(cn_pointer *ptr) {\ - CNTYPE *res = (CNTYPE *) alloc(sizeof(CNTYPE));\ + CNTYPE *res = (CNTYPE *) cn_alloc(sizeof(CNTYPE));\ res->val = (CTYPE) (INTPTR_TYPE) (ptr->ptr);\ return res;\ } @@ -407,7 +407,7 @@ static inline int ipow(int base, int exp) #define CN_GEN_CAST_INT_TYPES(CNTYPE1, CTYPE2, CNTYPE2)\ static inline CNTYPE2 *cast_##CNTYPE1##_to_##CNTYPE2(CNTYPE1 *i) {\ - CNTYPE2 *res = (CNTYPE2 *) alloc(sizeof(CNTYPE2));\ + CNTYPE2 *res = (CNTYPE2 *) cn_alloc(sizeof(CNTYPE2));\ res->val = (CTYPE2) i->val;\ return res;\ } @@ -422,7 +422,7 @@ cn_bool *default_cn_bool(void); #define CN_GEN_MAP_GET(CNTYPE)\ static inline void *cn_map_get_##CNTYPE(cn_map *m, cn_integer *key) { \ - signed long *key_ptr = alloc(sizeof(signed long)); \ + signed long *key_ptr = cn_alloc(sizeof(signed long)); \ *key_ptr = key->val; \ void *res = ht_get(m, key_ptr); \ if (!res) { return (void *) default_##CNTYPE(); } \ diff --git a/runtime/libcn/include/cn-testing/dsl.h b/runtime/libcn/include/cn-testing/dsl.h index f6ee72a49..626c1c45c 100644 --- a/runtime/libcn/include/cn-testing/dsl.h +++ b/runtime/libcn/include/cn-testing/dsl.h @@ -113,7 +113,7 @@ #define CN_GEN_LET_BEGIN(backtracks, var) \ int var##_backtracks = backtracks; \ - alloc_checkpoint var##_checkpoint = alloc_save_checkpoint(); \ + cn_alloc_checkpoint var##_checkpoint = cn_alloc_save_checkpoint(); \ void *var##_alloc_checkpoint = cn_gen_alloc_save(); \ void *var##_ownership_checkpoint = cn_gen_ownership_save(); \ cn_label_##var##_gen: \ @@ -126,7 +126,7 @@ #define CN_GEN_LET_END(backtracks, var, last_var, ...) \ if (cn_gen_backtrack_type() != CN_GEN_BACKTRACK_NONE) { \ cn_label_##var##_backtrack: \ - free_after(var##_checkpoint); \ + cn_free_after(var##_checkpoint); \ cn_gen_alloc_restore(var##_alloc_checkpoint); \ cn_gen_ownership_restore(var##_ownership_checkpoint); \ if (cn_gen_backtrack_relevant_contains((char*)#var)) { \ @@ -199,7 +199,7 @@ } \ tmp##_num_choices /= 2; \ struct cn_gen_int_urn* tmp##_urn = urn_from_array(tmp##_choices, tmp##_num_choices);\ - alloc_checkpoint tmp##_checkpoint = alloc_save_checkpoint(); \ + cn_alloc_checkpoint tmp##_checkpoint = cn_alloc_save_checkpoint(); \ void *tmp##_alloc_checkpoint = cn_gen_alloc_save(); \ void *tmp##_ownership_checkpoint = cn_gen_ownership_save(); \ cn_label_##tmp##_gen: \ @@ -207,7 +207,7 @@ uint64_t tmp = urn_remove(tmp##_urn); \ if (0) { \ cn_label_##tmp##_backtrack: \ - free_after(tmp##_checkpoint); \ + cn_free_after(tmp##_checkpoint); \ cn_gen_alloc_restore(tmp##_alloc_checkpoint); \ cn_gen_ownership_restore(tmp##_ownership_checkpoint); \ if ((cn_gen_backtrack_type() == CN_GEN_BACKTRACK_ASSERT \ @@ -237,7 +237,7 @@ #define CN_GEN_SPLIT_BEGIN(tmp, size, ...) \ int tmp##_backtracks = cn_gen_get_size_split_backtracks_allowed(); \ - alloc_checkpoint tmp##_checkpoint = alloc_save_checkpoint(); \ + cn_alloc_checkpoint tmp##_checkpoint = cn_alloc_save_checkpoint(); \ void *tmp##_alloc_checkpoint = cn_gen_alloc_save(); \ void *tmp##_ownership_checkpoint = cn_gen_ownership_save(); \ cn_label_##tmp##_gen: \ @@ -262,7 +262,7 @@ } \ if (0) { \ cn_label_##tmp##_backtrack: \ - free_after(tmp##_checkpoint); \ + cn_free_after(tmp##_checkpoint); \ cn_gen_alloc_restore(tmp##_alloc_checkpoint); \ cn_gen_ownership_restore(tmp##_ownership_checkpoint); \ if (cn_gen_backtrack_relevant_contains(#tmp)) { \ diff --git a/runtime/libcn/include/cn-testing/test.h b/runtime/libcn/include/cn-testing/test.h index 99ae59ebf..696358e6f 100644 --- a/runtime/libcn/include/cn-testing/test.h +++ b/runtime/libcn/include/cn-testing/test.h @@ -134,7 +134,7 @@ void cn_trap(void); int cn_test_main(int argc, char* argv[]); #define CN_TEST_INIT() \ - free_all(); \ + cn_free_all(); \ reset_error_msg_info(); \ initialise_ownership_ghost_state(); \ initialise_ghost_stack_depth(); \ diff --git a/runtime/libcn/libexec/cn-runtime-single-file.sh b/runtime/libcn/libexec/cn-runtime-single-file.sh index e43642757..371d349fb 100755 --- a/runtime/libcn/libexec/cn-runtime-single-file.sh +++ b/runtime/libcn/libexec/cn-runtime-single-file.sh @@ -26,8 +26,7 @@ while getopts "hnqu" flag; do ;; u) export UBSAN_OPTIONS=halt_on_error=1 - # FIXME: https://github.com/rems-project/cerberus/issues/821 - UBSAN="-fsanitize=undefined -fno-sanitize=alignment" + UBSAN="-fsanitize=undefined" ;; \?) echo_and_err "${USAGE}" diff --git a/runtime/libcn/src/cn-executable/alloc.c b/runtime/libcn/src/cn-executable/alloc.c index 81e01fe2d..898ce2cf5 100644 --- a/runtime/libcn/src/cn-executable/alloc.c +++ b/runtime/libcn/src/cn-executable/alloc.c @@ -1,86 +1,61 @@ #include #include +#include #include #include #include -// #define foo(x)\ -// [ x ] = #x -// const char *kind_str[CNTYPE_SIZE] = { -// foo(NODE_CN), -// foo(SEQ), -// foo(HASH_TABLE), -// // HT_ENTRY, -// foo(UNSIGNED_INT), -// foo(CN_BOOL), -// foo(CN_POINTER), -// }; #define MEM_SIZE (1024 * 1024 * 1024) char buf[MEM_SIZE]; -static void *curr = buf; +static char* curr = buf; // 268,435,449 -/* Allocation function */ -// void *alloc_(long nbytes, const char *str) { -// static unsigned long count[CNTYPE_SIZE]; -// void *res = curr; -// if ((char *) (curr + nbytes) - buf > MEM_SIZE) { -// printf("Out of memory!\n"); -// for (int i = 0; i < CNTYPE_SIZE; i++) { -// printf("%s -> %lu\n", kind_str[i], count[i]); -// } -// exit(1); -// } -// count[kind]++; -// curr += nbytes; -// return res; -// } +void* _cn_aligned_alloc(size_t alignment, size_t nbytes) { + size_t max = (uintptr_t)buf + MEM_SIZE; -void *alloc_(long nbytes, const char *str, int line) { - static unsigned long count; - // printf("Alloc called: %s:%d\n", str, line); - void *res = curr; - if ((char *) curr + nbytes - buf > MEM_SIZE) { + if ((uintptr_t)curr % alignment != 0) { + size_t padding = (alignment - (uintptr_t)curr % alignment) % alignment; + if ((uintptr_t)curr + padding >= max) { + cn_failure(CN_FAILURE_ALLOC); + return NULL; + } + curr += padding; + } + + void* res = curr; + if ((uintptr_t)curr + nbytes > max) { cn_failure(CN_FAILURE_ALLOC); return NULL; } - count++; curr += nbytes; + return res; - //return malloc(nbytes); } -void *zalloc_(long nbytes, const char *str, int line) { - void *p = alloc_(nbytes, str, line); +void* cn_alloc(size_t nbytes) { + return _cn_aligned_alloc(alignof(max_align_t), nbytes); +} + +void* cn_zalloc(size_t nbytes) { + void* p = cn_alloc(nbytes); if (p != NULL) { memset(p, 0, nbytes); } return p; } -void free_all(void) { +void cn_free_all(void) { curr = buf; } -alloc_checkpoint alloc_save_checkpoint(void) { - return curr; +cn_alloc_checkpoint cn_alloc_save_checkpoint(void) { + return (uintptr_t)curr; } -void free_after(alloc_checkpoint ptr) { - curr = ptr; +void cn_free_after(cn_alloc_checkpoint ptr) { + curr = (char*)ptr; } - -// void *alloc_zeros(long nbytes) { -// void *res = alloc(nbytes); -// bzero(res, nbytes); -// return res; -// } - - -// int main(void) { -// return 0; -// } diff --git a/runtime/libcn/src/cn-executable/hash_table.c b/runtime/libcn/src/cn-executable/hash_table.c index e96b74cf5..c79357d12 100644 --- a/runtime/libcn/src/cn-executable/hash_table.c +++ b/runtime/libcn/src/cn-executable/hash_table.c @@ -35,7 +35,7 @@ SOFTWARE. hash_table* ht_create(void) { // Allocate space for hash table struct. - hash_table* table = alloc(sizeof(hash_table)); + hash_table* table = cn_alloc(sizeof(hash_table)); if (table == NULL) { return NULL; } @@ -43,7 +43,7 @@ hash_table* ht_create(void) { table->capacity = INITIAL_CAPACITY; // Allocate (zero'd) space for entry buckets. - table->entries = zalloc(table->capacity * sizeof(ht_entry)); + table->entries = cn_zalloc(table->capacity * sizeof(ht_entry)); if (table->entries == NULL) { // free(table); // error, free table before we return! return NULL; @@ -100,7 +100,7 @@ void* ht_get(hash_table* table, signed long *key) { } signed long *duplicate_key(signed long *key) { - signed long *new_key = alloc(sizeof(signed long)); + signed long *new_key = cn_alloc(sizeof(signed long)); *new_key = *key; return new_key; } @@ -148,7 +148,7 @@ static _Bool ht_expand(hash_table* table) { if (new_capacity < table->capacity) { return 0; // overflow (capacity would be too big) } - ht_entry* new_entries = zalloc(new_capacity * sizeof(ht_entry)); + ht_entry* new_entries = cn_zalloc(new_capacity * sizeof(ht_entry)); if (new_entries == NULL) { return 0; } diff --git a/runtime/libcn/src/cn-executable/utils.c b/runtime/libcn/src/cn-executable/utils.c index 62125092d..bbdb33726 100644 --- a/runtime/libcn/src/cn-executable/utils.c +++ b/runtime/libcn/src/cn-executable/utils.c @@ -70,7 +70,7 @@ void print_error_msg_info(struct cn_error_message_info *info) { } cn_bool *convert_to_cn_bool(_Bool b) { - cn_bool *res = alloc(sizeof(cn_bool)); + cn_bool *res = cn_alloc(sizeof(cn_bool)); if (!res) exit(1); res->val = b; return res; @@ -100,25 +100,25 @@ void cn_assert(cn_bool *cn_b) { /* } */ cn_bool *cn_bool_and(cn_bool *b1, cn_bool *b2) { - cn_bool *res = alloc(sizeof(cn_bool)); + cn_bool *res = cn_alloc(sizeof(cn_bool)); res->val = b1->val && b2->val; return res; } cn_bool *cn_bool_or(cn_bool *b1, cn_bool *b2) { - cn_bool *res = alloc(sizeof(cn_bool)); + cn_bool *res = cn_alloc(sizeof(cn_bool)); res->val = b1->val || b2->val; return res; } cn_bool *cn_bool_implies(cn_bool *b1, cn_bool *b2) { - cn_bool *res = alloc(sizeof(cn_bool)); + cn_bool *res = cn_alloc(sizeof(cn_bool)); res->val = !b1->val || b2->val; return res; } cn_bool *cn_bool_not(cn_bool *b) { - cn_bool *res = alloc(sizeof(cn_bool)); + cn_bool *res = cn_alloc(sizeof(cn_bool)); res->val = !(b->val); return res; } @@ -185,7 +185,7 @@ int ownership_ghost_state_get(signed long *address_key) { } void ownership_ghost_state_set(signed long* address_key, int stack_depth_val) { - int *new_depth = alloc(sizeof(int)); + int *new_depth = cn_alloc(sizeof(int)); *new_depth = stack_depth_val; ht_set(cn_ownership_global_ghost_state, address_key, new_depth); } @@ -225,7 +225,7 @@ void cn_assume_ownership(void *generic_c_ptr, unsigned long size, char *fun) { // cn_printf(CN_LOGGING_INFO, "[CN: assuming ownership (%s)] " FMT_PTR_2 ", size: %lu\n", fun, (uintptr_t) generic_c_ptr, size); //// print_error_msg_info(); for (int i = 0; i < size; i++) { - signed long *address_key = alloc(sizeof(long)); + signed long *address_key = cn_alloc(sizeof(long)); *address_key = ((uintptr_t) generic_c_ptr) + i; /* // cn_printf(CN_LOGGING_INFO, "CN: Assuming ownership for %lu (function: %s)\n", */ /* ((uintptr_t) generic_c_ptr) + i, fun); */ @@ -255,7 +255,7 @@ void cn_get_or_put_ownership(enum OWNERSHIP owned_enum, uintptr_t generic_c_ptr, void c_add_to_ghost_state(uintptr_t ptr_to_local, size_t size, signed long stack_depth) { // cn_printf(CN_LOGGING_INFO, "[C access checking] add local:" FMT_PTR ", size: %lu\n", ptr_to_local, size); for (int i = 0; i < size; i++) { - signed long *address_key = alloc(sizeof(long)); + signed long *address_key = cn_alloc(sizeof(long)); *address_key = ptr_to_local + i; /* // cn_printf(CN_LOGGING_INFO, " off: %d [" FMT_PTR "]\n", i, *address_key); */ ownership_ghost_state_set(address_key, stack_depth); @@ -265,7 +265,7 @@ void c_add_to_ghost_state(uintptr_t ptr_to_local, size_t size, signed long stack void c_remove_from_ghost_state(uintptr_t ptr_to_local, size_t size) { // cn_printf(CN_LOGGING_INFO, "[C access checking] remove local:" FMT_PTR ", size: %lu\n", ptr_to_local, size); for (int i = 0; i < size; i++) { - signed long *address_key = alloc(sizeof(long)); + signed long *address_key = cn_alloc(sizeof(long)); *address_key = ptr_to_local + i; /* // cn_printf(CN_LOGGING_INFO, " off: %d [" FMT_PTR "]\n", i, *address_key); */ ownership_ghost_state_remove(address_key); @@ -302,7 +302,7 @@ void c_ownership_check(char *access_kind, uintptr_t generic_c_ptr, int offset, s // for (int i = 0; i < n; i++) { // uintptr_t fn_local_ptr = va_arg(args, uintptr_t); -// signed long *address_key = alloc(sizeof(long)); +// signed long *address_key = cn_alloc(sizeof(long)); // *address_key = fn_local_ptr; // ghost_state_set(cn_ownership_global_ghost_state, address_key, cn_stack_depth); // } @@ -312,7 +312,7 @@ void c_ownership_check(char *access_kind, uintptr_t generic_c_ptr, int offset, s cn_map *cn_map_set(cn_map *m, cn_integer *key, void *value) { - signed long *key_ptr = alloc(sizeof(signed long)); + signed long *key_ptr = cn_alloc(sizeof(signed long)); *key_ptr = key->val; ht_set(m, key_ptr, value); return m; @@ -402,13 +402,13 @@ cn_bool *cn_map_equality(cn_map *m1, cn_map *m2, cn_bool *(value_equality_fun)(v // TODO (RB) does this need to be in here, or should it be auto-generated? // See https://github.com/rems-project/cerberus/pull/652 for details cn_bool *void_pointer_equality(void *p1, void *p2) { - cn_bool *res = alloc(sizeof(cn_bool)); + cn_bool *res = cn_alloc(sizeof(cn_bool)); res->val = (p1 == p2); return res; } cn_pointer *convert_to_cn_pointer(void *ptr) { - cn_pointer *res = (cn_pointer *) alloc(sizeof(cn_pointer)); + cn_pointer *res = (cn_pointer *) cn_alloc(sizeof(cn_pointer)); res->ptr = ptr; // Carries around an address return res; } @@ -423,7 +423,7 @@ struct cn_error_message_info *make_error_message_info_entry(const char *function char *cn_source_loc, struct cn_error_message_info *parent) { - struct cn_error_message_info *entry = (struct cn_error_message_info *) alloc(sizeof(struct cn_error_message_info)); + struct cn_error_message_info *entry = (struct cn_error_message_info *) cn_alloc(sizeof(struct cn_error_message_info)); entry->function_name = function_name; entry->file_name = file_name; entry->line_number = line_number; @@ -466,13 +466,13 @@ static uint64_t cn_flsl(uint64_t x) cn_bits_u32 *cn_bits_u32_fls(cn_bits_u32 *i1) { - cn_bits_u32 *res = (cn_bits_u32 *) alloc(sizeof(cn_bits_u32)); + cn_bits_u32 *res = (cn_bits_u32 *) cn_alloc(sizeof(cn_bits_u32)); res->val = cn_fls(i1->val); return res; } cn_bits_u64 *cn_bits_u64_flsl(cn_bits_u64 *i1) { - cn_bits_u64 *res = (cn_bits_u64 *) alloc(sizeof(cn_bits_u64)); + cn_bits_u64 *res = (cn_bits_u64 *) cn_alloc(sizeof(cn_bits_u64)); res->val = cn_flsl(i1->val); return res; } diff --git a/runtime/libcn/src/cn-testing/gen_alloc.c b/runtime/libcn/src/cn-testing/gen_alloc.c index 6c19cc70b..19a9f9714 100644 --- a/runtime/libcn/src/cn-testing/gen_alloc.c +++ b/runtime/libcn/src/cn-testing/gen_alloc.c @@ -115,7 +115,7 @@ cn_pointer* cn_gen_alloc(cn_bits_u64* sz) { return convert_to_cn_pointer(NULL); } else { - void* p = alloc(bytes); + void* p = cn_alloc(bytes); update_alloc(p, bytes); return convert_to_cn_pointer(p); } diff --git a/tests/run-cn-test-gen.sh b/tests/run-cn-test-gen.sh index a7753b316..de1bfbfcd 100755 --- a/tests/run-cn-test-gen.sh +++ b/tests/run-cn-test-gen.sh @@ -30,7 +30,7 @@ function separator() { printf '\n\n' } -CONFIGS=("--coverage" "--with-static-hack --coverage --sanitize=undefined --no-sanitize=alignment" "--sized-null" "--random-size-splits" "--random-size-splits --allowed-size-split-backtracks=10") +CONFIGS=("--coverage" "--with-static-hack --coverage --sanitize=undefined" "--sized-null" "--random-size-splits" "--random-size-splits --allowed-size-split-backtracks=10") # For each configuration for CONFIG in "${CONFIGS[@]}"; do