Skip to content

Commit

Permalink
[CN-Exec] Enable setting of logging level
Browse files Browse the repository at this point in the history 
In the case of random testing, we don't want all of these logs, except for a failing input. We can disable logging, test many inputs and if we find a failing one, we re-enable logging and rerun that input.
  • Loading branch information
@ZippeyKeys12
ZippeyKeys12 committed Sep 30, 2024
1 parent 5d94a72 commit 072521d
Show file tree
Hide file tree
Showing 2 changed files with 59 additions and 39 deletions.
8 changes: 8 additions & 0 deletions runtime/libcn/include/cn-executable/utils.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,14 @@
extern "C" {
#endif

enum cn_logging_level {
CN_LOGGING_NONE = 0,
CN_LOGGING_INFO = 1
};

/** Sets the logging level, returning the previous one */
enum cn_logging_level set_cn_logging_level(enum cn_logging_level new_level);

struct cn_error_message_info {
const char *function_name;
char *file_name;
Expand Down
90 changes: 51 additions & 39 deletions runtime/libcn/src/utils.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,18 @@ ownership_ghost_state* cn_ownership_global_ghost_state;
signed long cn_stack_depth;
struct cn_error_message_info error_msg_info;

static enum cn_logging_level logging_level = CN_LOGGING_INFO;

enum cn_logging_level set_cn_logging_level(enum cn_logging_level new_level) {
enum cn_logging_level old_level = logging_level;
logging_level = new_level;
return old_level;
}

#define cn_printf(level, ...)\
if (logging_level >= level) {\
printf(__VA_ARGS__);\
}

void cn_exit_aux(void) {
exit(SIGABRT);
Expand All @@ -25,7 +37,7 @@ void reset_cn_exit_cb(void) {
}

void print_error_msg_info(void) {
printf("Function: %s, %s:%d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
cn_printf(CN_LOGGING_INFO, "Function: %s, %s:%d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
}

cn_bool *convert_to_cn_bool(_Bool b) {
Expand All @@ -40,19 +52,19 @@ _Bool convert_from_cn_bool(cn_bool *b) {
}

void cn_assert(cn_bool *cn_b) {
printf("[CN: assertion] function %s, file %s, line %d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
cn_printf(CN_LOGGING_INFO, "[CN: assertion] function %s, file %s, line %d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
if (!(cn_b->val)) {
printf("CN assertion failed: function %s, file %s, line %d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
cn_printf(CN_LOGGING_INFO, "CN assertion failed: function %s, file %s, line %d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
if (error_msg_info.cn_source_loc) {
printf("CN source location: \n%s\n", error_msg_info.cn_source_loc);
cn_printf(CN_LOGGING_INFO, "CN source location: \n%s\n", error_msg_info.cn_source_loc);
}
cn_exit();
}
}

void c_ghost_assert(cn_bool *cn_b) {
if (!(cn_b->val)) {
printf("C memory access failed: function %s, file %s, line %d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
cn_printf(CN_LOGGING_INFO, "C memory access failed: function %s, file %s, line %d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
cn_exit();
}
}
Expand Down Expand Up @@ -113,18 +125,18 @@ void ghost_stack_depth_decr(void) {
print_error_msg_info();
// leak checking
hash_table_iterator it = ht_iterator(cn_ownership_global_ghost_state);
printf("CN pointers leaked at (%ld) stack-depth: ", cn_stack_depth);
cn_printf(CN_LOGGING_INFO, "CN pointers leaked at (%ld) stack-depth: ", cn_stack_depth);
_Bool leaked = false;
while (ht_next(&it)) {
intptr_t *key = it.key;
int *depth = it.value;
_Bool fine = *depth <= cn_stack_depth;
if (!fine) {
leaked = true;
printf(FMT_PTR_2 " (%d),", *key, *depth);
cn_printf(CN_LOGGING_INFO, FMT_PTR_2 " (%d),", *key, *depth);
}
}
printf("\n");
cn_printf(CN_LOGGING_INFO, "\n");
c_ghost_assert(convert_to_cn_bool(!leaked));
}

Expand All @@ -150,27 +162,27 @@ void ownership_ghost_state_remove(signed long* address_key) {
void dump_ownership_state()
{
hash_table_iterator it = ht_iterator(cn_ownership_global_ghost_state);
printf("BEGIN ownership state\n");
cn_printf(CN_LOGGING_INFO, "BEGIN ownership state\n");
while (ht_next(&it)) {
int depth = it.value ? *(int*)it.value : -1;
printf("[%#lx] => depth: %d\n", *it.key, depth);
cn_printf(CN_LOGGING_INFO, "[%#lx] => depth: %d\n", *it.key, depth);
}
printf("END\n");
cn_printf(CN_LOGGING_INFO, "END\n");
}


void cn_get_ownership(uintptr_t generic_c_ptr, size_t size) {
printf("[CN: getting ownership] " FMT_PTR_2 ", size: %lu\n", generic_c_ptr, size);
cn_printf(CN_LOGGING_INFO, "[CN: getting ownership] " FMT_PTR_2 ", size: %lu\n", generic_c_ptr, size);
//print_error_msg_info();
for (int i = 0; i < size; i++) {
signed long *address_key = alloc(sizeof(long));
*address_key = generic_c_ptr + i;
/* printf(" off: %d [" FMT_PTR_2 "] (function: %s)\n", i, *address_key, error_msg_info.function_name); */
/* cn_printf(CN_LOGGING_INFO, " off: %d [" FMT_PTR_2 "] (function: %s)\n", i, *address_key, error_msg_info.function_name); */
int curr_depth = ownership_ghost_state_get(address_key);
if (curr_depth != cn_stack_depth - 1) {
printf("CN memory access failed: function %s, file %s, line %d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
printf(" ==> "FMT_PTR"[%d] ("FMT_PTR") -- currently at level: %ld\n", generic_c_ptr, i, (uintptr_t)((char*)generic_c_ptr + i), cn_stack_depth);
printf(" ==> owned at level : %d\n", curr_depth);
cn_printf(CN_LOGGING_INFO, "CN memory access failed: function %s, file %s, line %d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
cn_printf(CN_LOGGING_INFO, " ==> "FMT_PTR"[%d] ("FMT_PTR") -- currently at level: %ld\n", generic_c_ptr, i, (uintptr_t)((char*)generic_c_ptr + i), cn_stack_depth);
cn_printf(CN_LOGGING_INFO, " ==> owned at level : %d\n", curr_depth);
//dump_ownership_state();
cn_exit();
}
Expand All @@ -180,16 +192,16 @@ void cn_get_ownership(uintptr_t generic_c_ptr, size_t size) {
}

void cn_put_ownership(uintptr_t generic_c_ptr, size_t size) {
printf("[CN: returning ownership] " FMT_PTR_2 ", size: %lu\n", generic_c_ptr, size);
cn_printf(CN_LOGGING_INFO, "[CN: returning ownership] " FMT_PTR_2 ", size: %lu\n", generic_c_ptr, size);
//print_error_msg_info();
for (int i = 0; i < size; i++) {
signed long *address_key = alloc(sizeof(long));
*address_key = generic_c_ptr + i;
int curr_depth = ownership_ghost_state_get(address_key);
if (curr_depth != cn_stack_depth) {
printf("CN memory access failed: function %s, file %s, line %d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
printf(" ==> "FMT_PTR"[%d] ("FMT_PTR") -- currently at level: %ld\n", generic_c_ptr, i, (uintptr_t)((char*)generic_c_ptr + i), cn_stack_depth);
printf(" ==> owned at level: %d\n", curr_depth);
cn_printf(CN_LOGGING_INFO, "CN memory access failed: function %s, file %s, line %d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
cn_printf(CN_LOGGING_INFO, " ==> "FMT_PTR"[%d] ("FMT_PTR") -- currently at level: %ld\n", generic_c_ptr, i, (uintptr_t)((char*)generic_c_ptr + i), cn_stack_depth);
cn_printf(CN_LOGGING_INFO, " ==> owned at level: %d\n", curr_depth);
//dump_ownership_state();
cn_exit();
}
Expand All @@ -199,12 +211,12 @@ void cn_put_ownership(uintptr_t generic_c_ptr, size_t size) {
}

void cn_assume_ownership(void *generic_c_ptr, unsigned long size, char *fun) {
printf("[CN: assuming ownership (%s)] " FMT_PTR_2 ", size: %lu\n", fun, (uintptr_t) generic_c_ptr, size);
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));
*address_key = ((uintptr_t) generic_c_ptr) + i;
/* printf("CN: Assuming ownership for %lu (function: %s)\n", */
/* cn_printf(CN_LOGGING_INFO, "CN: Assuming ownership for %lu (function: %s)\n", */
/* ((uintptr_t) generic_c_ptr) + i, fun); */
ownership_ghost_state_set(address_key, cn_stack_depth);
}
Expand All @@ -229,40 +241,40 @@ void cn_check_ownership(enum OWNERSHIP owned_enum, uintptr_t generic_c_ptr, size


void c_add_local_to_ghost_state(uintptr_t ptr_to_local, size_t size) {
printf("[C access checking] add local:" FMT_PTR ", size: %lu\n", ptr_to_local, size);
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));
*address_key = ptr_to_local + i;
/* printf(" off: %d [" FMT_PTR "]\n", i, *address_key); */
/* cn_printf(CN_LOGGING_INFO, " off: %d [" FMT_PTR "]\n", i, *address_key); */
ownership_ghost_state_set(address_key, cn_stack_depth);
}
}

void c_remove_local_from_ghost_state(uintptr_t ptr_to_local, size_t size) {
printf("[C access checking] remove local:" FMT_PTR ", size: %lu\n", ptr_to_local, 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));
*address_key = ptr_to_local + i;
/* printf(" off: %d [" FMT_PTR "]\n", i, *address_key); */
/* cn_printf(CN_LOGGING_INFO, " off: %d [" FMT_PTR "]\n", i, *address_key); */
ownership_ghost_state_remove(address_key);
}
}

void c_ownership_check(uintptr_t generic_c_ptr, int offset) {
signed long address_key = 0;
printf("C: Checking ownership for [ " FMT_PTR " .. " FMT_PTR " ] -- ", generic_c_ptr, generic_c_ptr + offset);
cn_printf(CN_LOGGING_INFO, "C: Checking ownership for [ " FMT_PTR " .. " FMT_PTR " ] -- ", generic_c_ptr, generic_c_ptr + offset);
for (int i = 0; i<offset; i++) {
address_key = generic_c_ptr + i;
int curr_depth = ownership_ghost_state_get(&address_key);
if (curr_depth != cn_stack_depth) {
printf("C memory access failed: function %s, file %s, line %d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
printf(" ==> "FMT_PTR"[%d] ("FMT_PTR") -- cn_stack_depth: %ld\n", generic_c_ptr, i, (uintptr_t)((char*)generic_c_ptr + i), cn_stack_depth);
printf(" ==> curr_depth: %d\n", curr_depth);
cn_printf(CN_LOGGING_INFO, "C memory access failed: function %s, file %s, line %d\n", error_msg_info.function_name, error_msg_info.file_name, error_msg_info.line_number);
cn_printf(CN_LOGGING_INFO, " ==> "FMT_PTR"[%d] ("FMT_PTR") -- cn_stack_depth: %ld\n", generic_c_ptr, i, (uintptr_t)((char*)generic_c_ptr + i), cn_stack_depth);
cn_printf(CN_LOGGING_INFO, " ==> curr_depth: %d\n", curr_depth);
cn_exit();
}
// c_ghost_assert(convert_to_cn_bool(curr_depth == cn_stack_depth));
}
printf("\n");
cn_printf(CN_LOGGING_INFO, "\n");
}

/* TODO: Need address of and size of every stack-allocated variable - could store in struct and pass through. But this is an optimisation */
Expand Down Expand Up @@ -358,7 +370,7 @@ cn_bool *cn_map_subset(cn_map *m1, cn_map *m2, cn_bool *(value_equality_fun)(voi
if (!val2) return convert_to_cn_bool(0);

if (convert_from_cn_bool(cn_bool_not(value_equality_fun(val1, val2)))) {
printf("Values not equal!\n");
cn_printf(CN_LOGGING_INFO, "Values not equal!\n");
return convert_to_cn_bool(0);
}
}
Expand Down Expand Up @@ -392,7 +404,7 @@ void update_error_message_info_(const char *function_name, char *file_name, int
}

void initialise_error_msg_info_(const char *function_name, char *file_name, int line_number) {
printf("Initialising error message info\n");
cn_printf(CN_LOGGING_INFO, "Initialising error message info\n");
error_msg_info.function_name = function_name;
error_msg_info.file_name = file_name;
error_msg_info.line_number = line_number;
Expand Down Expand Up @@ -432,7 +444,7 @@ void *cn_aligned_alloc(size_t align, size_t size)
cn_assume_ownership((void*) p, size, str);
return p;
} else {
printf("aligned_alloc failed\n");
cn_printf(CN_LOGGING_INFO, "aligned_alloc failed\n");
return p;
}
}
Expand All @@ -445,7 +457,7 @@ void *cn_malloc(unsigned long size)
cn_assume_ownership((void*) p, size, str);
return p;
} else {
printf("malloc failed\n");
cn_printf(CN_LOGGING_INFO, "malloc failed\n");
return p;
}
}
Expand All @@ -458,14 +470,14 @@ void *cn_calloc(size_t num, size_t size)
cn_assume_ownership((void*) p, num*size, str);
return p;
} else {
printf("calloc failed\n");
cn_printf(CN_LOGGING_INFO, "calloc failed\n");
return p;
}
}

void cn_free_sized(void* malloced_ptr, size_t size)
{
printf("[CN: freeing ownership] " FMT_PTR ", size: %lu\n", (uintptr_t) malloced_ptr, size);
cn_printf(CN_LOGGING_INFO, "[CN: freeing ownership] " FMT_PTR ", size: %lu\n", (uintptr_t) malloced_ptr, size);
for (int i = 0; i < size; i++) {
signed long *address_key = alloc(sizeof(long));
*address_key = (uintptr_t) malloced_ptr + i;
Expand All @@ -478,11 +490,11 @@ void cn_free_sized(void* malloced_ptr, size_t size)

void cn_print_u64(const char *str, unsigned long u)
{
printf("\n\nprint %s: %20lx, %20lu\n\n", str, u, u);
cn_printf(CN_LOGGING_INFO, "\n\nprint %s: %20lx, %20lu\n\n", str, u, u);
}

void cn_print_nr_u64(int i, unsigned long u)
{
printf("\n\nprint %d: %20lx, %20lu\n", i, u, u);
cn_printf(CN_LOGGING_INFO, "\n\nprint %d: %20lx, %20lu\n", i, u, u);
}

0 comments on commit 072521d

Please sign in to comment.