[CN-Test-Gen] Allocator cleanup and fixes

GaloisInc · Feb 5, 2025 · c935516 · c935516
1 parent ebb66a4
commit c935516
Show file tree

Hide file tree

Showing 11 changed files with 89 additions and 128 deletions.
diff --git 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
@@ -1,40 +1,26 @@
 #ifndef CN_ALLOC
 #define CN_ALLOC
 
+#include <stddef.h>
+#include <stdint.h>
+
 #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
@@ -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,22 +392,22 @@ 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;\
     }
 
 
 #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
@@ -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,15 +199,15 @@
     }                                                                                   \
     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:                                                               \
         ;                                                                               \
     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
@@ -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
@@ -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}"