Skip to content

Commit

Permalink
[CN-Test-Gen] Rewrite ownership and allocation checking (rems-project…
Browse files Browse the repository at this point in the history 
…#674)

No longer connected to CN-Exec ownership tracking or the CN-Exec allocator
  • Loading branch information
@ZippeyKeys12 @vzaliva
ZippeyKeys12 authored and vzaliva committed Dec 4, 2024
1 parent 45bca8a commit d5f3a1b
Show file tree
Hide file tree
Showing 6 changed files with 175 additions and 39 deletions.
16 changes: 15 additions & 1 deletion backend/cn/lib/testGeneration/genCodeGen.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -198,7 +198,21 @@ let rec compile_term
mk_expr (AilEstr (None, [ (loc, [ Sym.pp_string name ]) ]))
));
mk_expr (AilEident last_var)
] )))
]
@ List.map
(fun x ->
mk_expr
(AilEcast
( C.no_qualifiers,
C.pointer_to_char,
mk_expr
(AilEstr
( None,
[ (Locations.other __LOC__, [ Sym.pp_string x ]) ]
)) )))
(List.of_seq
(SymSet.to_seq (SymSet.add pointer (IT.free_vars offset))))
@ [ mk_expr (AilEconst ConstantNull) ] )))
]
in
let b4, s4, e4 = compile_term sigma name rest in
Expand Down
1 change: 1 addition & 0 deletions backend/cn/lib/testGeneration/specTests.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -393,6 +393,7 @@ let compile_script ~(output_dir : string) ~(test_file : string) : Pp.document =
string
[ "if";
"cc";
"-g";
"\"-I${RUNTIME_PREFIX}/include\"";
"-o \"${TEST_DIR}/tests.out\"";
"${TEST_DIR}/" ^ Filename.chop_extension test_file ^ ".o";
Expand Down
16 changes: 15 additions & 1 deletion runtime/libcn/include/cn-testing/alloc.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,25 @@ extern "C" {

void cn_gen_alloc_reset(void);

void* cn_gen_alloc_save(void);

void cn_gen_alloc_restore(void* ptr);

void cn_gen_ownership_reset(void);

void* cn_gen_ownership_save(void);

void cn_gen_ownership_restore(void* ptr);

cn_pointer* cn_gen_alloc(cn_bits_u64* sz);

cn_pointer* cn_gen_aligned_alloc(cn_bits_u64* alignment, cn_bits_u64* sz);

cn_bits_u64* cn_gen_alloc_size(cn_pointer* p);
int cn_gen_alloc_check(void* p, size_t sz);

void cn_gen_ownership_update(void* p, size_t sz);

int cn_gen_ownership_check(cn_pointer* p, size_t sz);

#ifdef __cplusplus
}
Expand Down
35 changes: 28 additions & 7 deletions runtime/libcn/include/cn-testing/dsl.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,29 +38,46 @@
cn_gen_backtrack_relevant_remap_many(from, to); \
}

#define CN_GEN_ASSIGN(p, offset, addr_ty, value, tmp, gen_name, last_var) \
cn_bits_u64* tmp##_size = cn_bits_u64_add( \
#define CN_GEN_ASSIGN(p, offset, addr_ty, value, tmp, gen_name, last_var, ...) \
if (convert_from_cn_pointer(p) == 0) { \
cn_gen_backtrack_assert_failure(); \
cn_gen_backtrack_relevant_add((char*)#p); \
goto cn_label_##last_var##_backtrack; \
} \
void *tmp##_ptr = convert_from_cn_pointer(cn_pointer_add_cn_bits_u64(p, offset)); \
if (!cn_gen_alloc_check(tmp##_ptr, sizeof(addr_ty))) { \
cn_gen_backtrack_relevant_add((char*)#p); \
cn_bits_u64* tmp##_size = cn_bits_u64_add( \
offset, \
convert_to_cn_bits_u64(sizeof(addr_ty))); \
if (!convert_from_cn_bool(cn_bits_u64_le(tmp##_size, cn_gen_alloc_size(p)))) { \
cn_gen_backtrack_relevant_add((char*)#p); \
cn_gen_backtrack_alloc_set(convert_from_cn_bits_u64(tmp##_size)); \
goto cn_label_##last_var##_backtrack; \
} \
void *tmp##_ptr = convert_from_cn_pointer(cn_pointer_add_cn_bits_u64(p, offset)); \
*(addr_ty*)tmp##_ptr = value;
if (!cn_gen_ownership_check(tmp##_ptr, sizeof(addr_ty))) { \
cn_gen_backtrack_assert_failure(); \
char *toAdd[] = { __VA_ARGS__ }; \
cn_gen_backtrack_relevant_add_many(toAdd); \
goto cn_label_##last_var##_backtrack; \
} \
*(addr_ty*)tmp##_ptr = value; \
cn_gen_ownership_update(tmp##_ptr, sizeof(addr_ty));

#define CN_GEN_LET_BEGIN(backtracks, var) \
int var##_backtracks = backtracks; \
cn_label_##var##_gen: \
;
; \
void *var##_alloc_checkpoint = cn_gen_alloc_save(); \
void *var##_ownership_checkpoint = cn_gen_ownership_save();


#define CN_GEN_LET_BODY(ty, var, gen) \
ty* var = gen;

#define CN_GEN_LET_END(backtracks, var, last_var, ...) \
if (cn_gen_backtrack_type() != CN_GEN_BACKTRACK_NONE) { \
cn_label_##var##_backtrack: \
cn_gen_alloc_restore(var##_alloc_checkpoint); \
cn_gen_ownership_restore(var##_ownership_checkpoint); \
if (cn_gen_backtrack_relevant_contains((char*)#var)) { \
char *toAdd[] = { __VA_ARGS__ }; \
cn_gen_backtrack_relevant_add_many(toAdd); \
Expand Down Expand Up @@ -127,9 +144,13 @@
struct int_urn* tmp##_urn = urn_from_array(tmp##_choices, tmp##_num_choices); \
cn_label_##tmp##_gen: \
; \
void *tmp##_alloc_checkpoint = cn_gen_alloc_save(); \
void *tmp##_ownership_checkpoint = cn_gen_ownership_save(); \
uint64_t tmp = urn_remove(tmp##_urn); \
if (0) { \
cn_label_##tmp##_backtrack: \
cn_gen_alloc_restore(tmp##_alloc_checkpoint); \
cn_gen_ownership_restore(tmp##_ownership_checkpoint); \
if (cn_gen_backtrack_type() == CN_GEN_BACKTRACK_ASSERT \
&& tmp##_urn->size != 0) { \
cn_gen_backtrack_reset(); \
Expand Down
3 changes: 2 additions & 1 deletion runtime/libcn/include/cn-testing/test.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,8 @@ int cn_test_main(int argc, char* argv[]);
initialise_ownership_ghost_state(); \
initialise_ghost_stack_depth(); \
cn_gen_backtrack_reset(); \
cn_gen_alloc_reset();
cn_gen_alloc_reset(); \
cn_gen_ownership_reset();

#define CN_TEST_GENERATE(name) ({ \
struct cn_gen_##name##_record* res = cn_gen_##name(); \
Expand Down
143 changes: 114 additions & 29 deletions runtime/libcn/src/cn-testing/gen_alloc.c
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,66 @@
#include "stdlib.h"

#include <cn-executable/utils.h>

#include <cn-testing/prelude.h>

static uint8_t null_in_every = 4;
#define MEM_SIZE (1024 * 1024 * 256)
static char alloc_buf[MEM_SIZE];
static void* alloc_curr = alloc_buf;

void set_null_in_every(uint8_t n) {
null_in_every = n;
void cn_gen_alloc_reset(void) {
alloc_curr = alloc_buf;
}

void* cn_gen_alloc_save(void) {
return alloc_curr;
}

static hash_table* pointer_size_map = 0;
void cn_gen_alloc_restore(void* ptr) {
alloc_curr = ptr;
}

void cn_gen_alloc_reset(void) {
pointer_size_map = ht_create();
static char ownership_buf[MEM_SIZE];
static void* ownership_curr = ownership_buf;

void cn_gen_ownership_reset(void) {
ownership_curr = ownership_buf;
}

void* cn_gen_ownership_save(void) {
return ownership_curr;
}

void cn_gen_ownership_restore(void* ptr) {
ownership_curr = ptr;
}

struct pointer_data {
void* ptr;
size_t sz;
};

static void update_alloc(void* ptr, size_t sz) {
if ((uintptr_t)alloc_curr - (uintptr_t)alloc_buf + sizeof(struct pointer_data) > MEM_SIZE) {
printf("Out of space for allocation metadata!\n");
exit(1);
}
*(struct pointer_data*)alloc_curr = (struct pointer_data){ .ptr = ptr, .sz = sz };
alloc_curr = (char*)alloc_curr + sizeof(struct pointer_data);
}

static void update_ownership(void* ptr, size_t sz) {
if ((uintptr_t)ownership_curr - (uintptr_t)ownership_buf + sizeof(struct pointer_data) > MEM_SIZE) {
printf("Out of space for ownership metadata!\n");
exit(1);
}
*(struct pointer_data*)ownership_curr = (struct pointer_data){ .ptr = ptr, .sz = sz };
ownership_curr = (char*)ownership_curr + sizeof(struct pointer_data);
}

static uint8_t null_in_every = 4;

void set_null_in_every(uint8_t n) {
null_in_every = n;
}

cn_pointer* cn_gen_alloc(cn_bits_u64* sz) {
Expand All @@ -31,17 +78,13 @@ cn_pointer* cn_gen_alloc(cn_bits_u64* sz) {
}
else {
p = alloc(1);
uint64_t* size = alloc(sizeof(uint64_t));
*size = bytes + 1;
ht_set(pointer_size_map, (intptr_t*)&p, size);
update_alloc(p, 1);
}
return convert_to_cn_pointer(p);
}
else {
void* p = alloc(bytes);
uint64_t* size = alloc(sizeof(uint64_t));
*size = bytes;
ht_set(pointer_size_map, (intptr_t*)&p, size);
update_alloc(p, bytes);
return convert_to_cn_pointer(p);
}
}
Expand All @@ -60,37 +103,79 @@ cn_pointer* cn_gen_aligned_alloc(cn_bits_u64* alignment, cn_bits_u64* sz) {

if (bytes == 0) {
void* p;
uint64_t rnd = convert_from_cn_bits_u64(cn_gen_uniform_cn_bits_u64(0));
if ((rnd % 2) == 0) {
uint64_t rnd = convert_from_cn_bits_u8(cn_gen_uniform_cn_bits_u8(null_in_every));
if (rnd == 0) {
p = NULL;
}
else {
p = aligned_alloc(align, 1);
uint64_t* size = alloc(sizeof(uint64_t));
*size = bytes + 1;
ht_set(pointer_size_map, (intptr_t*)&p, size);
update_alloc(p, 1);
}
return convert_to_cn_pointer(p);
}
else {
void* p = aligned_alloc(align, bytes);
uint64_t* size = alloc(sizeof(uint64_t));
*size = bytes;
ht_set(pointer_size_map, (intptr_t*)&p, size);
update_alloc(p, bytes);
return convert_to_cn_pointer(p);
}
}

cn_bits_u64* cn_gen_alloc_size(cn_pointer* p) {
void* ptr = convert_from_cn_pointer(p);
if (ptr == NULL) {
return convert_to_cn_bits_u64(0);
int cn_gen_alloc_check(void* p, size_t sz) {
if (alloc_curr == alloc_buf) {
return 0;
}

uint64_t* value = (uint64_t*)ht_get(pointer_size_map, (signed long*)&ptr);
if (value == NULL) {
return convert_to_cn_bits_u64(0);
int bytes = sz;

struct pointer_data* q = (struct pointer_data*)(
(uintptr_t)alloc_curr - sizeof(struct pointer_data));
for (; (uintptr_t)q >= (uintptr_t)alloc_buf; q--) {
uintptr_t lb = (uintptr_t)q->ptr;
uintptr_t ub = (uintptr_t)q->ptr + q->sz;
if (lb < (uintptr_t)p) {
lb = (uintptr_t)p;
}
if (ub > (uintptr_t)p + sz) {
ub = (uintptr_t)p + sz;
}
if (ub > lb) {
bytes -= (ub - lb);
}

if (bytes == 0) {
return 1;
}
}
assert(bytes >= 0);
return (bytes == 0);
}

void cn_gen_ownership_update(void* p, size_t sz) {
update_ownership(p, sz);
}

int cn_gen_ownership_check(cn_pointer* p, size_t sz) {
if (ownership_curr == ownership_buf) {
return 1;
}

int bytes = sz;

struct pointer_data* q = (struct pointer_data*)(
(uintptr_t)ownership_curr - sizeof(struct pointer_data));
for (; (uintptr_t)q >= (uintptr_t)ownership_buf; q--) {
uintptr_t lb = (uintptr_t)q->ptr;
uintptr_t ub = (uintptr_t)q->ptr + q->sz;
if (lb < (uintptr_t)p) {
lb = (uintptr_t)p;
}
if (ub > (uintptr_t)p + sz) {
ub = (uintptr_t)p + sz;
}
if (ub > lb) {
return 0;
}
}

return convert_to_cn_bits_u64(*value);
return 1;
}

0 comments on commit d5f3a1b

Please sign in to comment.