From 66117ae26e1f63242495b83b7a26ccb9792aaf70 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Michae=20D=C3=B6rr?= Date: Fri, 13 Dec 2024 14:20:18 +0100 Subject: [PATCH 1/3] add count solver argument --- .gitignore | 1 + src/trusted/main_check.c | 66 +++--- src/trusted/trusted_checker.c | 380 +++++++++++++++++----------------- src/trusted/trusted_checker.h | 16 +- src/trusted/trusted_utils.c | 365 ++++++++++++++++---------------- src/trusted/trusted_utils.h | 129 ++++++------ 6 files changed, 485 insertions(+), 472 deletions(-) create mode 100644 .gitignore diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..07ed706 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +build/* \ No newline at end of file diff --git a/src/trusted/main_check.c b/src/trusted/main_check.c index 43526c4..cda8f87 100644 --- a/src/trusted/main_check.c +++ b/src/trusted/main_check.c @@ -1,32 +1,34 @@ - -#include // for bool, false -#include // for fflush, stdout -#include "trusted_checker.h" // for tc_init, tc_run -#include "trusted_utils.h" // for trusted_utils_try_match_arg, trusted_ut... -#if IMPCHECK_WRITE_DIRECTIVES -#include -#include "../writer.h" -#endif - -int main(int argc, char *argv[]) { - - const char *fifo_directives = "", *fifo_feedback = ""; - bool check_model = false, lenient = false; - for (int i = 1; i < argc; i++) { - trusted_utils_try_match_arg(argv[i], "-fifo-directives=", &fifo_directives); - trusted_utils_try_match_arg(argv[i], "-fifo-feedback=", &fifo_feedback); - trusted_utils_try_match_flag(argv[i], "-check-model", &check_model); - trusted_utils_try_match_flag(argv[i], "-lenient", &lenient); - } - -#if IMPCHECK_WRITE_DIRECTIVES - char output_path[512]; - snprintf(output_path, 512, "directives.%i.impcheck", getpid()); - writer_init(output_path); -#endif - - tc_init(fifo_directives, fifo_feedback); - int res = tc_run(check_model, lenient); - fflush(stdout); - return res; -} + +#include // for bool, false +#include // for fflush, stdout +#include "trusted_checker.h" // for tc_init, tc_run +#include "trusted_utils.h" // for trusted_utils_try_match_arg, trusted_ut... +#if IMPCHECK_WRITE_DIRECTIVES +#include +#include "../writer.h" +#endif + +int main(int argc, char *argv[]) { + + const char *fifo_directives = "", *fifo_feedback = ""; + bool check_model = false, lenient = false; + u64 num_solvers = 0; + for (int i = 1; i < argc; i++) { + trusted_utils_try_match_arg(argv[i], "-fifo-directives=", &fifo_directives); + trusted_utils_try_match_arg(argv[i], "-fifo-feedback=", &fifo_feedback); + trusted_utils_try_match_num(argv[i], "-num-solvers=", &num_solvers); + trusted_utils_try_match_flag(argv[i], "-check-model", &check_model); + trusted_utils_try_match_flag(argv[i], "-lenient", &lenient); + } + +#if IMPCHECK_WRITE_DIRECTIVES + char output_path[512]; + snprintf(output_path, 512, "directives.%i.impcheck", getpid()); + writer_init(output_path); +#endif + + tc_init(fifo_directives, fifo_feedback, num_solvers); + int res = tc_run(check_model, lenient); + fflush(stdout); + return res; +} diff --git a/src/trusted/trusted_checker.c b/src/trusted/trusted_checker.c index cf69fae..d50b36a 100644 --- a/src/trusted/trusted_checker.c +++ b/src/trusted/trusted_checker.c @@ -1,189 +1,191 @@ - -#include // for bool, true, false -#include // for fclose, fflush_unlocked, fopen, snprintf -#include // for free -#include // for clock, CLOCKS_PER_SEC, clock_t -#include "top_check.h" // for top_check_commit_formula_sig, top_check_d... -#include "trusted_utils.h" // for trusted_utils_read_int, trusted_utils_log... -#include "checker_interface.h" - -// Instantiate int_vec -#define TYPE int -#define TYPED(THING) int_ ## THING -#include "vec.h" -#undef TYPED -#undef TYPE - -// Instantiate u64_vec -#define TYPE u64 -#define TYPED(THING) u64_ ## THING -#include "vec.h" -#undef TYPED -#undef TYPE - -FILE* input; // named pipe -FILE* output; // named pipe -int nb_vars; // # variables in formula -signature formula_sig; // formula signature - -bool do_logging = true; - -// Buffering. -signature buf_sig; -struct int_vec* buf_lits; -struct u64_vec* buf_hints; - - -void say(bool ok) { - trusted_utils_write_char(ok ? TRUSTED_CHK_RES_ACCEPT : TRUSTED_CHK_RES_ERROR, output); -#if IMPCHECK_FLUSH_ALWAYS - UNLOCKED_IO(fflush)(output); -#endif -} -void say_with_flush(bool ok) { - say(ok); - UNLOCKED_IO(fflush)(output); -} - -void read_literals(int nb_lits) { - int_vec_reserve(buf_lits, nb_lits); - trusted_utils_read_ints(buf_lits->data, nb_lits, input); -} - -void read_hints(int nb_hints) { - u64_vec_reserve(buf_hints, nb_hints); - trusted_utils_read_uls(buf_hints->data, nb_hints, input); -} - -void tc_init(const char* fifo_in, const char* fifo_out) { - input = fopen(fifo_in, "r"); - if (!input) trusted_utils_exit_eof(); - output = fopen(fifo_out, "w"); - if (!output) trusted_utils_exit_eof(); - buf_lits = int_vec_init(1 << 14); - buf_hints = u64_vec_init(1 << 14); -} - -void tc_end() { - free(buf_hints); - free(buf_lits); - fclose(output); - fclose(input); -} - -int tc_run(bool check_model, bool lenient) { - clock_t start = clock(); - - u64 nb_produced = 0, nb_imported = 0, nb_deleted = 0; - - bool reported_error = false; - - while (true) { - int c = trusted_utils_read_char(input); - if (c == TRUSTED_CHK_CLS_PRODUCE) { - - // parse - const u64 id = trusted_utils_read_ul(input); - const int nb_lits = trusted_utils_read_int(input); - read_literals(nb_lits); - const int nb_hints = trusted_utils_read_int(input); - read_hints(nb_hints); - const bool share = trusted_utils_read_bool(input); - // forward to checker - bool res = top_check_produce(id, buf_lits->data, nb_lits, - buf_hints->data, nb_hints, share ? buf_sig : 0); - // respond - say(res); - if (share) trusted_utils_write_sig(buf_sig, output); -#if IMPCHECK_FLUSH_ALWAYS - UNLOCKED_IO(fflush)(output); -#endif - nb_produced++; - - } else if (c == TRUSTED_CHK_CLS_IMPORT) { - - // parse - const u64 id = trusted_utils_read_ul(input); - const int nb_lits = trusted_utils_read_int(input); - read_literals(nb_lits); - trusted_utils_read_sig(buf_sig, input); - // forward to checker - bool res = top_check_import(id, buf_lits->data, nb_lits, buf_sig); - // respond - say(res); - nb_imported++; - - } else if (c == TRUSTED_CHK_CLS_DELETE) { - - // parse - const int nb_hints = trusted_utils_read_int(input); - read_hints(nb_hints); - // forward to checker - bool res = top_check_delete(buf_hints->data, nb_hints); - // respond - say(res); - nb_deleted += nb_hints; - - } else if (c == TRUSTED_CHK_LOAD) { - - const int nb_lits = trusted_utils_read_int(input); - read_literals(nb_lits); - for (int i = 0; i < nb_lits; i++) top_check_load(buf_lits->data[i]); - // NO FEEDBACK - - } else if (c == TRUSTED_CHK_INIT) { - - nb_vars = trusted_utils_read_int(input); - top_check_init(nb_vars, check_model, lenient); - trusted_utils_read_sig(formula_sig, input); - top_check_commit_formula_sig(formula_sig); - say_with_flush(true); - - } else if (c == TRUSTED_CHK_END_LOAD) { - - say_with_flush(top_check_end_load()); - - } else if (c == TRUSTED_CHK_VALIDATE_UNSAT) { - - bool res = top_check_validate_unsat(buf_sig); - say(res); - trusted_utils_write_sig(buf_sig, output); - UNLOCKED_IO(fflush)(output); - if (res) trusted_utils_log("UNSAT validated"); - - } else if (c == TRUSTED_CHK_VALIDATE_SAT) { - - const int model_size = trusted_utils_read_int(input); - int* model = trusted_utils_malloc(sizeof(int) * model_size); // exits if error - trusted_utils_read_ints(model, model_size, input); - bool res = top_check_validate_sat(model, model_size, buf_sig); - say(res); - trusted_utils_write_sig(buf_sig, output); - UNLOCKED_IO(fflush)(output); - if (res) trusted_utils_log("SAT validated"); - free(model); - - } else if (c == TRUSTED_CHK_TERMINATE) { - - say_with_flush(true); - break; - - } else { - trusted_utils_log_err("Invalid directive!"); - break; - } - - if (MALLOB_UNLIKELY(!top_check_valid())) { - if (!reported_error) { - trusted_utils_log_err(trusted_utils_msgstr); - reported_error = true; - } - } - } - - float elapsed = (float) (clock() - start) / CLOCKS_PER_SEC; - snprintf(trusted_utils_msgstr, 512, "cpu:%.3f prod:%lu imp:%lu del:%lu", elapsed, nb_produced, nb_imported, nb_deleted); - trusted_utils_log(trusted_utils_msgstr); - - return 0; -} + +#include // for bool, true, false +#include // for fclose, fflush_unlocked, fopen, snprintf +#include // for free +#include // for clock, CLOCKS_PER_SEC, clock_t +#include "top_check.h" // for top_check_commit_formula_sig, top_check_d... +#include "trusted_utils.h" // for trusted_utils_read_int, trusted_utils_log... +#include "checker_interface.h" + +// Instantiate int_vec +#define TYPE int +#define TYPED(THING) int_ ## THING +#include "vec.h" +#undef TYPED +#undef TYPE + +// Instantiate u64_vec +#define TYPE u64 +#define TYPED(THING) u64_ ## THING +#include "vec.h" +#undef TYPED +#undef TYPE + +FILE* input; // named pipe +FILE* output; // named pipe +int nb_vars; // # variables in formula +signature formula_sig; // formula signature +u64 nb_solvers; // number of solvers + +bool do_logging = true; + +// Buffering. +signature buf_sig; +struct int_vec* buf_lits; +struct u64_vec* buf_hints; + + +void say(bool ok) { + trusted_utils_write_char(ok ? TRUSTED_CHK_RES_ACCEPT : TRUSTED_CHK_RES_ERROR, output); +#if IMPCHECK_FLUSH_ALWAYS + UNLOCKED_IO(fflush)(output); +#endif +} +void say_with_flush(bool ok) { + say(ok); + UNLOCKED_IO(fflush)(output); +} + +void read_literals(int nb_lits) { + int_vec_reserve(buf_lits, nb_lits); + trusted_utils_read_ints(buf_lits->data, nb_lits, input); +} + +void read_hints(int nb_hints) { + u64_vec_reserve(buf_hints, nb_hints); + trusted_utils_read_uls(buf_hints->data, nb_hints, input); +} + +void tc_init(const char* fifo_in, const char* fifo_out, u64 num_solvers) { + input = fopen(fifo_in, "r"); + if (!input) trusted_utils_exit_eof(); + output = fopen(fifo_out, "w"); + if (!output) trusted_utils_exit_eof(); + buf_lits = int_vec_init(1 << 14); + buf_hints = u64_vec_init(1 << 14); + nb_solvers = num_solvers; +} + +void tc_end() { + free(buf_hints); + free(buf_lits); + fclose(output); + fclose(input); +} + +int tc_run(bool check_model, bool lenient) { + clock_t start = clock(); + + u64 nb_produced = 0, nb_imported = 0, nb_deleted = 0; + + bool reported_error = false; + + while (true) { + int c = trusted_utils_read_char(input); + if (c == TRUSTED_CHK_CLS_PRODUCE) { + + // parse + const u64 id = trusted_utils_read_ul(input); + const int nb_lits = trusted_utils_read_int(input); + read_literals(nb_lits); + const int nb_hints = trusted_utils_read_int(input); + read_hints(nb_hints); + const bool share = trusted_utils_read_bool(input); + // forward to checker + bool res = top_check_produce(id, buf_lits->data, nb_lits, + buf_hints->data, nb_hints, share ? buf_sig : 0); + // respond + say(res); + if (share) trusted_utils_write_sig(buf_sig, output); +#if IMPCHECK_FLUSH_ALWAYS + UNLOCKED_IO(fflush)(output); +#endif + nb_produced++; + + } else if (c == TRUSTED_CHK_CLS_IMPORT) { + + // parse + const u64 id = trusted_utils_read_ul(input); + const int nb_lits = trusted_utils_read_int(input); + read_literals(nb_lits); + trusted_utils_read_sig(buf_sig, input); + // forward to checker + bool res = top_check_import(id, buf_lits->data, nb_lits, buf_sig); + // respond + say(res); + nb_imported++; + + } else if (c == TRUSTED_CHK_CLS_DELETE) { + + // parse + const int nb_hints = trusted_utils_read_int(input); + read_hints(nb_hints); + // forward to checker + bool res = top_check_delete(buf_hints->data, nb_hints); + // respond + say(res); + nb_deleted += nb_hints; + + } else if (c == TRUSTED_CHK_LOAD) { + + const int nb_lits = trusted_utils_read_int(input); + read_literals(nb_lits); + for (int i = 0; i < nb_lits; i++) top_check_load(buf_lits->data[i]); + // NO FEEDBACK + + } else if (c == TRUSTED_CHK_INIT) { + + nb_vars = trusted_utils_read_int(input); + top_check_init(nb_vars, check_model, lenient); + trusted_utils_read_sig(formula_sig, input); + top_check_commit_formula_sig(formula_sig); + say_with_flush(true); + + } else if (c == TRUSTED_CHK_END_LOAD) { + + say_with_flush(top_check_end_load()); + + } else if (c == TRUSTED_CHK_VALIDATE_UNSAT) { + + bool res = top_check_validate_unsat(buf_sig); + say(res); + trusted_utils_write_sig(buf_sig, output); + UNLOCKED_IO(fflush)(output); + if (res) trusted_utils_log("UNSAT validated"); + + } else if (c == TRUSTED_CHK_VALIDATE_SAT) { + + const int model_size = trusted_utils_read_int(input); + int* model = trusted_utils_malloc(sizeof(int) * model_size); // exits if error + trusted_utils_read_ints(model, model_size, input); + bool res = top_check_validate_sat(model, model_size, buf_sig); + say(res); + trusted_utils_write_sig(buf_sig, output); + UNLOCKED_IO(fflush)(output); + if (res) trusted_utils_log("SAT validated"); + free(model); + + } else if (c == TRUSTED_CHK_TERMINATE) { + + say_with_flush(true); + break; + + } else { + trusted_utils_log_err("Invalid directive!"); + break; + } + + if (MALLOB_UNLIKELY(!top_check_valid())) { + if (!reported_error) { + trusted_utils_log_err(trusted_utils_msgstr); + reported_error = true; + } + } + } + + float elapsed = (float) (clock() - start) / CLOCKS_PER_SEC; + snprintf(trusted_utils_msgstr, 512, "cpu:%.3f prod:%lu imp:%lu del:%lu n_s:%lu", elapsed, nb_produced, nb_imported, nb_deleted, nb_solvers); + trusted_utils_log(trusted_utils_msgstr); + + return 0; +} diff --git a/src/trusted/trusted_checker.h b/src/trusted/trusted_checker.h index 1bce9e0..b0ad7fd 100644 --- a/src/trusted/trusted_checker.h +++ b/src/trusted/trusted_checker.h @@ -1,8 +1,8 @@ - -#pragma once - -#include - -void tc_init(const char* fifo_in, const char* fifo_out); -void tc_end(); -int tc_run(bool check_model, bool lenient); + +#pragma once + +#include + +void tc_init(const char* fifo_in, const char* fifo_out, unsigned long num_solvers); +void tc_end(); +int tc_run(bool check_model, bool lenient); diff --git a/src/trusted/trusted_utils.c b/src/trusted/trusted_utils.c index 4784964..db88792 100644 --- a/src/trusted/trusted_utils.c +++ b/src/trusted/trusted_utils.c @@ -1,179 +1,186 @@ - -#include "trusted_utils.h" -#include -#include -#if IMPCHECK_WRITE_DIRECTIVES -#include "../writer.h" -#endif -#include -#include // exit -#include // getpid - -char trusted_utils_msgstr[512] = ""; - -void trusted_utils_log(const char* msg) { - printf("c [TRUSTED_CORE %i] %s\n", getpid(), msg); -} -void trusted_utils_log_err(const char* msg) { - printf("c [TRUSTED_CORE %i] [ERROR] %s\n", getpid(), msg); -} - -void trusted_utils_exit_eof() { - trusted_utils_log("end-of-file - terminating"); - exit(0); -} -void exit_oom() { - trusted_utils_log("allocation failed - terminating"); - exit(0); -} - -bool begins_with(const char* str, const char* prefix) { - u64 i = 0; - while (true) { - if (prefix[i] == '\0') return true; - if (str[i] == '\0') return prefix[i] == '\0'; - if (str[i] != prefix[i]) return false; - i++; - } -} -void trusted_utils_try_match_arg(const char* arg, const char* opt, const char** out) { - if (begins_with(arg, opt)) *out = arg+strlen(opt); -} -void trusted_utils_try_match_flag(const char* arg, const char* opt, bool* out) { - if (begins_with(arg, opt)) *out = true; -} - -void trusted_utils_copy_bytes(u8* to, const u8* from, u64 nb_bytes) { - for (u64 i = 0; i < nb_bytes; i++) to[i] = from[i]; -} - -bool trusted_utils_equal_signatures(const u8* left, const u8* right) { - for (u64 i = 0; i < SIG_SIZE_BYTES; i++) - if (left[i] != right[i]) return false; - return true; -} - -void* trusted_utils_malloc(u64 size) { - void* res = malloc(size); - if (!res) exit_oom(); - return res; -} -void* trusted_utils_realloc(void* from, u64 new_size) { - void* res = realloc(from, new_size); - if (!res) exit_oom(); - return res; -} -void* trusted_utils_calloc(u64 nb_objs, u64 size_per_obj) { - void* res = calloc(nb_objs, size_per_obj); - if (!res) exit_oom(); - return res; -} - -bool trusted_utils_read_bool(FILE* file) { - int res = UNLOCKED_IO(fgetc)(file); - if (res == EOF) trusted_utils_exit_eof(); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_bool(res ? 1 : 0); -#endif - return res ? 1 : 0; -} -int trusted_utils_read_char(FILE* file) { - int res = UNLOCKED_IO(fgetc)(file); - if (res == EOF) trusted_utils_exit_eof(); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_char(res); -#endif - return res; -} -void trusted_utils_read_objs(void* data, size_t size, size_t nb_objs, FILE* file) { - u64 nb_read = UNLOCKED_IO(fread)(data, size, nb_objs, file); - if (nb_read < nb_objs) trusted_utils_exit_eof(); -} -int trusted_utils_read_int(FILE* file) { - int i; - trusted_utils_read_objs(&i, sizeof(int), 1, file); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_int(i); -#endif - return i; -} -void trusted_utils_read_ints(int* data, u64 nb_ints, FILE* file) { - trusted_utils_read_objs(data, sizeof(int), nb_ints, file); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_ints(data, nb_ints); -#endif -} -u64 trusted_utils_read_ul(FILE* file) { - u64 u; - trusted_utils_read_objs(&u, sizeof(u64), 1, file); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_ul(u); -#endif - return u; -} -void trusted_utils_read_uls(u64* data, u64 nb_uls, FILE* file) { - trusted_utils_read_objs(data, sizeof(u64), nb_uls, file); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_uls(data, nb_uls); -#endif -} -void trusted_utils_read_sig(u8* out_sig, FILE* file) { - signature dummy; - if (!out_sig) out_sig = dummy; - trusted_utils_read_objs(out_sig, sizeof(int), 4, file); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_sig(out_sig); -#endif -} - -void trusted_utils_write_char(char c, FILE* file) { - int res = UNLOCKED_IO(fputc)(c, file); - if (res == EOF) trusted_utils_exit_eof(); -} -void trusted_utils_write_bool(bool b, FILE* file) { - int res = UNLOCKED_IO(fputc)(b ? 1 : 0, file); - if (res == EOF) trusted_utils_exit_eof(); -} -void write_objs(const void* data, size_t size, size_t nb_objs, FILE* file) { - u64 nb_read = UNLOCKED_IO(fwrite)(data, size, nb_objs, file); - if (nb_read < nb_objs) trusted_utils_exit_eof(); -} -void trusted_utils_write_int(int i, FILE* file) { - write_objs(&i, sizeof(int), 1, file); -} -void trusted_utils_write_ints(const int* data, u64 nb_ints, FILE* file) { - write_objs(data, sizeof(int), nb_ints, file); -} -void trusted_utils_write_ul(u64 u, FILE* file) { - write_objs(&u, sizeof(u64), 1, file); -} -void trusted_utils_write_uls(const u64* data, u64 nb_uls, FILE* file) { - write_objs(data, sizeof(u64), nb_uls, file); -} -void trusted_utils_write_sig(const u8* sig, FILE* file) { - write_objs(sig, sizeof(int), 4, file); -} - -void trusted_utils_sig_to_str(const u8* sig, char* out) { - for (int charpos = 0; charpos < SIG_SIZE_BYTES; charpos++) { - char val1 = (sig[charpos] >> 4) & 0x0f; - char val2 = sig[charpos] & 0x0f; - assert(val1 >= 0 && val1 < 16); - assert(val2 >= 0 && val2 < 16); - out[2*charpos+0] = val1>=10 ? 'a'+val1-10 : '0'+val1; - out[2*charpos+1] = val2>=10 ? 'a'+val2-10 : '0'+val2; - } - out[SIG_SIZE_BYTES*2] = '\0'; -} - -bool trusted_utils_str_to_sig(const char* str, u8* out) { - for (int bytepos = 0; bytepos < SIG_SIZE_BYTES; bytepos++) { - const char* hex_pair = str + bytepos*2; - char hex1 = hex_pair[0]; char hex2 = hex_pair[1]; - int byte = 16 * (hex1 >= '0' && hex1 <= '9' ? hex1-'0' : 10+hex1-'a') - + (hex2 >= '0' && hex2 <= '9' ? hex2-'0' : 10+hex2-'a'); - if (byte < 0 || byte >= 256) return false; - out[bytepos] = (u8) byte; - } - return true; -} + +#include "trusted_utils.h" +#include +#include +#if IMPCHECK_WRITE_DIRECTIVES +#include "../writer.h" +#endif +#include +#include // exit +#include // getpid + +char trusted_utils_msgstr[512] = ""; + +void trusted_utils_log(const char* msg) { + printf("c [TRUSTED_CORE %i] %s\n", getpid(), msg); +} +void trusted_utils_log_err(const char* msg) { + printf("c [TRUSTED_CORE %i] [ERROR] %s\n", getpid(), msg); +} + +void trusted_utils_exit_eof() { + trusted_utils_log("end-of-file - terminating"); + exit(0); +} +void exit_oom() { + trusted_utils_log("allocation failed - terminating"); + exit(0); +} + +bool begins_with(const char* str, const char* prefix) { + u64 i = 0; + while (true) { + if (prefix[i] == '\0') return true; + if (str[i] == '\0') return prefix[i] == '\0'; + if (str[i] != prefix[i]) return false; + i++; + } +} + +void trusted_utils_try_match_arg(const char* arg, const char* opt, const char** out) { + if (begins_with(arg, opt)) *out = arg + strlen(opt); +} + +void trusted_utils_try_match_num(const char* arg, const char* opt, u64* out) { + const char* start_of_number = arg + strlen(opt); + if (begins_with(arg, opt)) *out = strtol( start_of_number, NULL, 10); +} + +void trusted_utils_try_match_flag(const char* arg, const char* opt, bool* out) { + if (begins_with(arg, opt)) *out = true; +} + +void trusted_utils_copy_bytes(u8* to, const u8* from, u64 nb_bytes) { + for (u64 i = 0; i < nb_bytes; i++) to[i] = from[i]; +} + +bool trusted_utils_equal_signatures(const u8* left, const u8* right) { + for (u64 i = 0; i < SIG_SIZE_BYTES; i++) + if (left[i] != right[i]) return false; + return true; +} + +void* trusted_utils_malloc(u64 size) { + void* res = malloc(size); + if (!res) exit_oom(); + return res; +} +void* trusted_utils_realloc(void* from, u64 new_size) { + void* res = realloc(from, new_size); + if (!res) exit_oom(); + return res; +} +void* trusted_utils_calloc(u64 nb_objs, u64 size_per_obj) { + void* res = calloc(nb_objs, size_per_obj); + if (!res) exit_oom(); + return res; +} + +bool trusted_utils_read_bool(FILE* file) { + int res = UNLOCKED_IO(fgetc)(file); + if (res == EOF) trusted_utils_exit_eof(); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_bool(res ? 1 : 0); +#endif + return res ? 1 : 0; +} +int trusted_utils_read_char(FILE* file) { + int res = UNLOCKED_IO(fgetc)(file); + if (res == EOF) trusted_utils_exit_eof(); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_char(res); +#endif + return res; +} +void trusted_utils_read_objs(void* data, size_t size, size_t nb_objs, FILE* file) { + u64 nb_read = UNLOCKED_IO(fread)(data, size, nb_objs, file); + if (nb_read < nb_objs) trusted_utils_exit_eof(); +} +int trusted_utils_read_int(FILE* file) { + int i; + trusted_utils_read_objs(&i, sizeof(int), 1, file); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_int(i); +#endif + return i; +} +void trusted_utils_read_ints(int* data, u64 nb_ints, FILE* file) { + trusted_utils_read_objs(data, sizeof(int), nb_ints, file); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_ints(data, nb_ints); +#endif +} +u64 trusted_utils_read_ul(FILE* file) { + u64 u; + trusted_utils_read_objs(&u, sizeof(u64), 1, file); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_ul(u); +#endif + return u; +} +void trusted_utils_read_uls(u64* data, u64 nb_uls, FILE* file) { + trusted_utils_read_objs(data, sizeof(u64), nb_uls, file); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_uls(data, nb_uls); +#endif +} +void trusted_utils_read_sig(u8* out_sig, FILE* file) { + signature dummy; + if (!out_sig) out_sig = dummy; + trusted_utils_read_objs(out_sig, sizeof(int), 4, file); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_sig(out_sig); +#endif +} + +void trusted_utils_write_char(char c, FILE* file) { + int res = UNLOCKED_IO(fputc)(c, file); + if (res == EOF) trusted_utils_exit_eof(); +} +void trusted_utils_write_bool(bool b, FILE* file) { + int res = UNLOCKED_IO(fputc)(b ? 1 : 0, file); + if (res == EOF) trusted_utils_exit_eof(); +} +void write_objs(const void* data, size_t size, size_t nb_objs, FILE* file) { + u64 nb_read = UNLOCKED_IO(fwrite)(data, size, nb_objs, file); + if (nb_read < nb_objs) trusted_utils_exit_eof(); +} +void trusted_utils_write_int(int i, FILE* file) { + write_objs(&i, sizeof(int), 1, file); +} +void trusted_utils_write_ints(const int* data, u64 nb_ints, FILE* file) { + write_objs(data, sizeof(int), nb_ints, file); +} +void trusted_utils_write_ul(u64 u, FILE* file) { + write_objs(&u, sizeof(u64), 1, file); +} +void trusted_utils_write_uls(const u64* data, u64 nb_uls, FILE* file) { + write_objs(data, sizeof(u64), nb_uls, file); +} +void trusted_utils_write_sig(const u8* sig, FILE* file) { + write_objs(sig, sizeof(int), 4, file); +} + +void trusted_utils_sig_to_str(const u8* sig, char* out) { + for (int charpos = 0; charpos < SIG_SIZE_BYTES; charpos++) { + char val1 = (sig[charpos] >> 4) & 0x0f; + char val2 = sig[charpos] & 0x0f; + assert(val1 >= 0 && val1 < 16); + assert(val2 >= 0 && val2 < 16); + out[2*charpos+0] = val1>=10 ? 'a'+val1-10 : '0'+val1; + out[2*charpos+1] = val2>=10 ? 'a'+val2-10 : '0'+val2; + } + out[SIG_SIZE_BYTES*2] = '\0'; +} + +bool trusted_utils_str_to_sig(const char* str, u8* out) { + for (int bytepos = 0; bytepos < SIG_SIZE_BYTES; bytepos++) { + const char* hex_pair = str + bytepos*2; + char hex1 = hex_pair[0]; char hex2 = hex_pair[1]; + int byte = 16 * (hex1 >= '0' && hex1 <= '9' ? hex1-'0' : 10+hex1-'a') + + (hex2 >= '0' && hex2 <= '9' ? hex2-'0' : 10+hex2-'a'); + if (byte < 0 || byte >= 256) return false; + out[bytepos] = (u8) byte; + } + return true; +} diff --git a/src/trusted/trusted_utils.h b/src/trusted/trusted_utils.h index 6f41481..99f702d 100644 --- a/src/trusted/trusted_utils.h +++ b/src/trusted/trusted_utils.h @@ -1,64 +1,65 @@ - -#pragma once - -#include // for _DEFAULT_SOURCE -#include // for bool -#include // for FILE - -#ifdef _MSC_VER -# define MALLOB_LIKELY(condition) condition -# define MALLOB_UNLIKELY(condition) condition -#else -# define MALLOB_LIKELY(condition) __builtin_expect(condition, 1) -# define MALLOB_UNLIKELY(condition) __builtin_expect(condition, 0) -#endif - -#if /* glibc >= 2.19: */ _DEFAULT_SOURCE || /* glibc <= 2.19: */ _SVID_SOURCE || _BSD_SOURCE -#define UNLOCKED_IO(fun) fun##_unlocked -#else -#define UNLOCKED_IO(fun) fun -#endif - -typedef unsigned long u64; -typedef unsigned int u32; -typedef unsigned char u8; - -#define SIG_SIZE_BYTES 16 -typedef u8 signature[SIG_SIZE_BYTES]; -#define TRUSTED_CHK_MAX_BUF_SIZE (1<<14) - -extern char trusted_utils_msgstr[512]; - -void trusted_utils_log(const char* msg); -void trusted_utils_log_err(const char* msg); - -void trusted_utils_exit_eof(); - -void trusted_utils_try_match_arg(const char* arg, const char* opt, const char** out); -void trusted_utils_try_match_flag(const char* arg, const char* opt, bool* out); - -void trusted_utils_copy_bytes(u8* to, const u8* from, u64 nb_bytes); -bool trusted_utils_equal_signatures(const u8* left, const u8* right); - -void* trusted_utils_malloc(u64 size); -void* trusted_utils_realloc(void* from, u64 new_size); -void* trusted_utils_calloc(u64 nb_objs, u64 size_per_obj); - -bool trusted_utils_read_bool(FILE* file); -int trusted_utils_read_char(FILE* file); -int trusted_utils_read_int(FILE* file); -void trusted_utils_read_ints(int* data, u64 nb_ints, FILE* file); -u64 trusted_utils_read_ul(FILE* file); -void trusted_utils_read_uls(u64* data, u64 nb_uls, FILE* file); -void trusted_utils_read_sig(u8* out_sig, FILE* file); - -void trusted_utils_write_bool(bool b, FILE* file); -void trusted_utils_write_char(char c, FILE* file); -void trusted_utils_write_int(int i, FILE* file); -void trusted_utils_write_ints(const int* data, u64 nb_ints, FILE* file); -void trusted_utils_write_ul(u64 u, FILE* file); -void trusted_utils_write_uls(const u64* data, u64 nb_uls, FILE* file); -void trusted_utils_write_sig(const u8* sig, FILE* file); - -void trusted_utils_sig_to_str(const u8* sig, char* out); -bool trusted_utils_str_to_sig(const char* str, u8* out); + +#pragma once + +#include // for _DEFAULT_SOURCE +#include // for bool +#include // for FILE + +#ifdef _MSC_VER +# define MALLOB_LIKELY(condition) condition +# define MALLOB_UNLIKELY(condition) condition +#else +# define MALLOB_LIKELY(condition) __builtin_expect(condition, 1) +# define MALLOB_UNLIKELY(condition) __builtin_expect(condition, 0) +#endif + +#if /* glibc >= 2.19: */ _DEFAULT_SOURCE || /* glibc <= 2.19: */ _SVID_SOURCE || _BSD_SOURCE +#define UNLOCKED_IO(fun) fun##_unlocked +#else +#define UNLOCKED_IO(fun) fun +#endif + +typedef unsigned long u64; +typedef unsigned int u32; +typedef unsigned char u8; + +#define SIG_SIZE_BYTES 16 +typedef u8 signature[SIG_SIZE_BYTES]; +#define TRUSTED_CHK_MAX_BUF_SIZE (1<<14) + +extern char trusted_utils_msgstr[512]; + +void trusted_utils_log(const char* msg); +void trusted_utils_log_err(const char* msg); + +void trusted_utils_exit_eof(); + +void trusted_utils_try_match_arg(const char* arg, const char* opt, const char** out); +void trusted_utils_try_match_num(const char* arg, const char* opt, u64* out); +void trusted_utils_try_match_flag(const char* arg, const char* opt, bool* out); + +void trusted_utils_copy_bytes(u8* to, const u8* from, u64 nb_bytes); +bool trusted_utils_equal_signatures(const u8* left, const u8* right); + +void* trusted_utils_malloc(u64 size); +void* trusted_utils_realloc(void* from, u64 new_size); +void* trusted_utils_calloc(u64 nb_objs, u64 size_per_obj); + +bool trusted_utils_read_bool(FILE* file); +int trusted_utils_read_char(FILE* file); +int trusted_utils_read_int(FILE* file); +void trusted_utils_read_ints(int* data, u64 nb_ints, FILE* file); +u64 trusted_utils_read_ul(FILE* file); +void trusted_utils_read_uls(u64* data, u64 nb_uls, FILE* file); +void trusted_utils_read_sig(u8* out_sig, FILE* file); + +void trusted_utils_write_bool(bool b, FILE* file); +void trusted_utils_write_char(char c, FILE* file); +void trusted_utils_write_int(int i, FILE* file); +void trusted_utils_write_ints(const int* data, u64 nb_ints, FILE* file); +void trusted_utils_write_ul(u64 u, FILE* file); +void trusted_utils_write_uls(const u64* data, u64 nb_uls, FILE* file); +void trusted_utils_write_sig(const u8* sig, FILE* file); + +void trusted_utils_sig_to_str(const u8* sig, char* out); +bool trusted_utils_str_to_sig(const char* str, u8* out); From f0ec5e34a4ed04196ae465c83da7d4524e0f2bd7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Michae=20D=C3=B6rr?= Date: Mon, 16 Dec 2024 17:45:26 +0100 Subject: [PATCH 2/3] line endings --- src/trusted/main_check.c | 68 +++--- src/trusted/trusted_checker.c | 382 +++++++++++++++++----------------- src/trusted/trusted_checker.h | 16 +- src/trusted/trusted_utils.c | 372 ++++++++++++++++----------------- src/trusted/trusted_utils.h | 130 ++++++------ 5 files changed, 484 insertions(+), 484 deletions(-) diff --git a/src/trusted/main_check.c b/src/trusted/main_check.c index cda8f87..d9a2662 100644 --- a/src/trusted/main_check.c +++ b/src/trusted/main_check.c @@ -1,34 +1,34 @@ - -#include // for bool, false -#include // for fflush, stdout -#include "trusted_checker.h" // for tc_init, tc_run -#include "trusted_utils.h" // for trusted_utils_try_match_arg, trusted_ut... -#if IMPCHECK_WRITE_DIRECTIVES -#include -#include "../writer.h" -#endif - -int main(int argc, char *argv[]) { - - const char *fifo_directives = "", *fifo_feedback = ""; - bool check_model = false, lenient = false; - u64 num_solvers = 0; - for (int i = 1; i < argc; i++) { - trusted_utils_try_match_arg(argv[i], "-fifo-directives=", &fifo_directives); - trusted_utils_try_match_arg(argv[i], "-fifo-feedback=", &fifo_feedback); - trusted_utils_try_match_num(argv[i], "-num-solvers=", &num_solvers); - trusted_utils_try_match_flag(argv[i], "-check-model", &check_model); - trusted_utils_try_match_flag(argv[i], "-lenient", &lenient); - } - -#if IMPCHECK_WRITE_DIRECTIVES - char output_path[512]; - snprintf(output_path, 512, "directives.%i.impcheck", getpid()); - writer_init(output_path); -#endif - - tc_init(fifo_directives, fifo_feedback, num_solvers); - int res = tc_run(check_model, lenient); - fflush(stdout); - return res; -} + +#include // for bool, false +#include // for fflush, stdout +#include "trusted_checker.h" // for tc_init, tc_run +#include "trusted_utils.h" // for trusted_utils_try_match_arg, trusted_ut... +#if IMPCHECK_WRITE_DIRECTIVES +#include +#include "../writer.h" +#endif + +int main(int argc, char *argv[]) { + + const char *fifo_directives = "", *fifo_feedback = ""; + bool check_model = false, lenient = false; + u64 num_solvers = 0; + for (int i = 1; i < argc; i++) { + trusted_utils_try_match_arg(argv[i], "-fifo-directives=", &fifo_directives); + trusted_utils_try_match_arg(argv[i], "-fifo-feedback=", &fifo_feedback); + trusted_utils_try_match_num(argv[i], "-num-solvers=", &num_solvers); + trusted_utils_try_match_flag(argv[i], "-check-model", &check_model); + trusted_utils_try_match_flag(argv[i], "-lenient", &lenient); + } + +#if IMPCHECK_WRITE_DIRECTIVES + char output_path[512]; + snprintf(output_path, 512, "directives.%i.impcheck", getpid()); + writer_init(output_path); +#endif + + tc_init(fifo_directives, fifo_feedback, num_solvers); + int res = tc_run(check_model, lenient); + fflush(stdout); + return res; +} diff --git a/src/trusted/trusted_checker.c b/src/trusted/trusted_checker.c index d50b36a..9e06976 100644 --- a/src/trusted/trusted_checker.c +++ b/src/trusted/trusted_checker.c @@ -1,191 +1,191 @@ - -#include // for bool, true, false -#include // for fclose, fflush_unlocked, fopen, snprintf -#include // for free -#include // for clock, CLOCKS_PER_SEC, clock_t -#include "top_check.h" // for top_check_commit_formula_sig, top_check_d... -#include "trusted_utils.h" // for trusted_utils_read_int, trusted_utils_log... -#include "checker_interface.h" - -// Instantiate int_vec -#define TYPE int -#define TYPED(THING) int_ ## THING -#include "vec.h" -#undef TYPED -#undef TYPE - -// Instantiate u64_vec -#define TYPE u64 -#define TYPED(THING) u64_ ## THING -#include "vec.h" -#undef TYPED -#undef TYPE - -FILE* input; // named pipe -FILE* output; // named pipe -int nb_vars; // # variables in formula -signature formula_sig; // formula signature -u64 nb_solvers; // number of solvers - -bool do_logging = true; - -// Buffering. -signature buf_sig; -struct int_vec* buf_lits; -struct u64_vec* buf_hints; - - -void say(bool ok) { - trusted_utils_write_char(ok ? TRUSTED_CHK_RES_ACCEPT : TRUSTED_CHK_RES_ERROR, output); -#if IMPCHECK_FLUSH_ALWAYS - UNLOCKED_IO(fflush)(output); -#endif -} -void say_with_flush(bool ok) { - say(ok); - UNLOCKED_IO(fflush)(output); -} - -void read_literals(int nb_lits) { - int_vec_reserve(buf_lits, nb_lits); - trusted_utils_read_ints(buf_lits->data, nb_lits, input); -} - -void read_hints(int nb_hints) { - u64_vec_reserve(buf_hints, nb_hints); - trusted_utils_read_uls(buf_hints->data, nb_hints, input); -} - -void tc_init(const char* fifo_in, const char* fifo_out, u64 num_solvers) { - input = fopen(fifo_in, "r"); - if (!input) trusted_utils_exit_eof(); - output = fopen(fifo_out, "w"); - if (!output) trusted_utils_exit_eof(); - buf_lits = int_vec_init(1 << 14); - buf_hints = u64_vec_init(1 << 14); - nb_solvers = num_solvers; -} - -void tc_end() { - free(buf_hints); - free(buf_lits); - fclose(output); - fclose(input); -} - -int tc_run(bool check_model, bool lenient) { - clock_t start = clock(); - - u64 nb_produced = 0, nb_imported = 0, nb_deleted = 0; - - bool reported_error = false; - - while (true) { - int c = trusted_utils_read_char(input); - if (c == TRUSTED_CHK_CLS_PRODUCE) { - - // parse - const u64 id = trusted_utils_read_ul(input); - const int nb_lits = trusted_utils_read_int(input); - read_literals(nb_lits); - const int nb_hints = trusted_utils_read_int(input); - read_hints(nb_hints); - const bool share = trusted_utils_read_bool(input); - // forward to checker - bool res = top_check_produce(id, buf_lits->data, nb_lits, - buf_hints->data, nb_hints, share ? buf_sig : 0); - // respond - say(res); - if (share) trusted_utils_write_sig(buf_sig, output); -#if IMPCHECK_FLUSH_ALWAYS - UNLOCKED_IO(fflush)(output); -#endif - nb_produced++; - - } else if (c == TRUSTED_CHK_CLS_IMPORT) { - - // parse - const u64 id = trusted_utils_read_ul(input); - const int nb_lits = trusted_utils_read_int(input); - read_literals(nb_lits); - trusted_utils_read_sig(buf_sig, input); - // forward to checker - bool res = top_check_import(id, buf_lits->data, nb_lits, buf_sig); - // respond - say(res); - nb_imported++; - - } else if (c == TRUSTED_CHK_CLS_DELETE) { - - // parse - const int nb_hints = trusted_utils_read_int(input); - read_hints(nb_hints); - // forward to checker - bool res = top_check_delete(buf_hints->data, nb_hints); - // respond - say(res); - nb_deleted += nb_hints; - - } else if (c == TRUSTED_CHK_LOAD) { - - const int nb_lits = trusted_utils_read_int(input); - read_literals(nb_lits); - for (int i = 0; i < nb_lits; i++) top_check_load(buf_lits->data[i]); - // NO FEEDBACK - - } else if (c == TRUSTED_CHK_INIT) { - - nb_vars = trusted_utils_read_int(input); - top_check_init(nb_vars, check_model, lenient); - trusted_utils_read_sig(formula_sig, input); - top_check_commit_formula_sig(formula_sig); - say_with_flush(true); - - } else if (c == TRUSTED_CHK_END_LOAD) { - - say_with_flush(top_check_end_load()); - - } else if (c == TRUSTED_CHK_VALIDATE_UNSAT) { - - bool res = top_check_validate_unsat(buf_sig); - say(res); - trusted_utils_write_sig(buf_sig, output); - UNLOCKED_IO(fflush)(output); - if (res) trusted_utils_log("UNSAT validated"); - - } else if (c == TRUSTED_CHK_VALIDATE_SAT) { - - const int model_size = trusted_utils_read_int(input); - int* model = trusted_utils_malloc(sizeof(int) * model_size); // exits if error - trusted_utils_read_ints(model, model_size, input); - bool res = top_check_validate_sat(model, model_size, buf_sig); - say(res); - trusted_utils_write_sig(buf_sig, output); - UNLOCKED_IO(fflush)(output); - if (res) trusted_utils_log("SAT validated"); - free(model); - - } else if (c == TRUSTED_CHK_TERMINATE) { - - say_with_flush(true); - break; - - } else { - trusted_utils_log_err("Invalid directive!"); - break; - } - - if (MALLOB_UNLIKELY(!top_check_valid())) { - if (!reported_error) { - trusted_utils_log_err(trusted_utils_msgstr); - reported_error = true; - } - } - } - - float elapsed = (float) (clock() - start) / CLOCKS_PER_SEC; - snprintf(trusted_utils_msgstr, 512, "cpu:%.3f prod:%lu imp:%lu del:%lu n_s:%lu", elapsed, nb_produced, nb_imported, nb_deleted, nb_solvers); - trusted_utils_log(trusted_utils_msgstr); - - return 0; -} + +#include // for bool, true, false +#include // for fclose, fflush_unlocked, fopen, snprintf +#include // for free +#include // for clock, CLOCKS_PER_SEC, clock_t +#include "top_check.h" // for top_check_commit_formula_sig, top_check_d... +#include "trusted_utils.h" // for trusted_utils_read_int, trusted_utils_log... +#include "checker_interface.h" + +// Instantiate int_vec +#define TYPE int +#define TYPED(THING) int_ ## THING +#include "vec.h" +#undef TYPED +#undef TYPE + +// Instantiate u64_vec +#define TYPE u64 +#define TYPED(THING) u64_ ## THING +#include "vec.h" +#undef TYPED +#undef TYPE + +FILE* input; // named pipe +FILE* output; // named pipe +int nb_vars; // # variables in formula +signature formula_sig; // formula signature +u64 nb_solvers; // number of solvers + +bool do_logging = true; + +// Buffering. +signature buf_sig; +struct int_vec* buf_lits; +struct u64_vec* buf_hints; + + +void say(bool ok) { + trusted_utils_write_char(ok ? TRUSTED_CHK_RES_ACCEPT : TRUSTED_CHK_RES_ERROR, output); +#if IMPCHECK_FLUSH_ALWAYS + UNLOCKED_IO(fflush)(output); +#endif +} +void say_with_flush(bool ok) { + say(ok); + UNLOCKED_IO(fflush)(output); +} + +void read_literals(int nb_lits) { + int_vec_reserve(buf_lits, nb_lits); + trusted_utils_read_ints(buf_lits->data, nb_lits, input); +} + +void read_hints(int nb_hints) { + u64_vec_reserve(buf_hints, nb_hints); + trusted_utils_read_uls(buf_hints->data, nb_hints, input); +} + +void tc_init(const char* fifo_in, const char* fifo_out, u64 num_solvers) { + input = fopen(fifo_in, "r"); + if (!input) trusted_utils_exit_eof(); + output = fopen(fifo_out, "w"); + if (!output) trusted_utils_exit_eof(); + buf_lits = int_vec_init(1 << 14); + buf_hints = u64_vec_init(1 << 14); + nb_solvers = num_solvers; +} + +void tc_end() { + free(buf_hints); + free(buf_lits); + fclose(output); + fclose(input); +} + +int tc_run(bool check_model, bool lenient) { + clock_t start = clock(); + + u64 nb_produced = 0, nb_imported = 0, nb_deleted = 0; + + bool reported_error = false; + + while (true) { + int c = trusted_utils_read_char(input); + if (c == TRUSTED_CHK_CLS_PRODUCE) { + + // parse + const u64 id = trusted_utils_read_ul(input); + const int nb_lits = trusted_utils_read_int(input); + read_literals(nb_lits); + const int nb_hints = trusted_utils_read_int(input); + read_hints(nb_hints); + const bool share = trusted_utils_read_bool(input); + // forward to checker + bool res = top_check_produce(id, buf_lits->data, nb_lits, + buf_hints->data, nb_hints, share ? buf_sig : 0); + // respond + say(res); + if (share) trusted_utils_write_sig(buf_sig, output); +#if IMPCHECK_FLUSH_ALWAYS + UNLOCKED_IO(fflush)(output); +#endif + nb_produced++; + + } else if (c == TRUSTED_CHK_CLS_IMPORT) { + + // parse + const u64 id = trusted_utils_read_ul(input); + const int nb_lits = trusted_utils_read_int(input); + read_literals(nb_lits); + trusted_utils_read_sig(buf_sig, input); + // forward to checker + bool res = top_check_import(id, buf_lits->data, nb_lits, buf_sig); + // respond + say(res); + nb_imported++; + + } else if (c == TRUSTED_CHK_CLS_DELETE) { + + // parse + const int nb_hints = trusted_utils_read_int(input); + read_hints(nb_hints); + // forward to checker + bool res = top_check_delete(buf_hints->data, nb_hints); + // respond + say(res); + nb_deleted += nb_hints; + + } else if (c == TRUSTED_CHK_LOAD) { + + const int nb_lits = trusted_utils_read_int(input); + read_literals(nb_lits); + for (int i = 0; i < nb_lits; i++) top_check_load(buf_lits->data[i]); + // NO FEEDBACK + + } else if (c == TRUSTED_CHK_INIT) { + + nb_vars = trusted_utils_read_int(input); + top_check_init(nb_vars, check_model, lenient); + trusted_utils_read_sig(formula_sig, input); + top_check_commit_formula_sig(formula_sig); + say_with_flush(true); + + } else if (c == TRUSTED_CHK_END_LOAD) { + + say_with_flush(top_check_end_load()); + + } else if (c == TRUSTED_CHK_VALIDATE_UNSAT) { + + bool res = top_check_validate_unsat(buf_sig); + say(res); + trusted_utils_write_sig(buf_sig, output); + UNLOCKED_IO(fflush)(output); + if (res) trusted_utils_log("UNSAT validated"); + + } else if (c == TRUSTED_CHK_VALIDATE_SAT) { + + const int model_size = trusted_utils_read_int(input); + int* model = trusted_utils_malloc(sizeof(int) * model_size); // exits if error + trusted_utils_read_ints(model, model_size, input); + bool res = top_check_validate_sat(model, model_size, buf_sig); + say(res); + trusted_utils_write_sig(buf_sig, output); + UNLOCKED_IO(fflush)(output); + if (res) trusted_utils_log("SAT validated"); + free(model); + + } else if (c == TRUSTED_CHK_TERMINATE) { + + say_with_flush(true); + break; + + } else { + trusted_utils_log_err("Invalid directive!"); + break; + } + + if (MALLOB_UNLIKELY(!top_check_valid())) { + if (!reported_error) { + trusted_utils_log_err(trusted_utils_msgstr); + reported_error = true; + } + } + } + + float elapsed = (float) (clock() - start) / CLOCKS_PER_SEC; + snprintf(trusted_utils_msgstr, 512, "cpu:%.3f prod:%lu imp:%lu del:%lu n_s:%lu", elapsed, nb_produced, nb_imported, nb_deleted, nb_solvers); + trusted_utils_log(trusted_utils_msgstr); + + return 0; +} diff --git a/src/trusted/trusted_checker.h b/src/trusted/trusted_checker.h index b0ad7fd..0f66068 100644 --- a/src/trusted/trusted_checker.h +++ b/src/trusted/trusted_checker.h @@ -1,8 +1,8 @@ - -#pragma once - -#include - -void tc_init(const char* fifo_in, const char* fifo_out, unsigned long num_solvers); -void tc_end(); -int tc_run(bool check_model, bool lenient); + +#pragma once + +#include + +void tc_init(const char* fifo_in, const char* fifo_out, unsigned long num_solvers); +void tc_end(); +int tc_run(bool check_model, bool lenient); diff --git a/src/trusted/trusted_utils.c b/src/trusted/trusted_utils.c index db88792..1a71ea7 100644 --- a/src/trusted/trusted_utils.c +++ b/src/trusted/trusted_utils.c @@ -1,186 +1,186 @@ - -#include "trusted_utils.h" -#include -#include -#if IMPCHECK_WRITE_DIRECTIVES -#include "../writer.h" -#endif -#include -#include // exit -#include // getpid - -char trusted_utils_msgstr[512] = ""; - -void trusted_utils_log(const char* msg) { - printf("c [TRUSTED_CORE %i] %s\n", getpid(), msg); -} -void trusted_utils_log_err(const char* msg) { - printf("c [TRUSTED_CORE %i] [ERROR] %s\n", getpid(), msg); -} - -void trusted_utils_exit_eof() { - trusted_utils_log("end-of-file - terminating"); - exit(0); -} -void exit_oom() { - trusted_utils_log("allocation failed - terminating"); - exit(0); -} - -bool begins_with(const char* str, const char* prefix) { - u64 i = 0; - while (true) { - if (prefix[i] == '\0') return true; - if (str[i] == '\0') return prefix[i] == '\0'; - if (str[i] != prefix[i]) return false; - i++; - } -} - -void trusted_utils_try_match_arg(const char* arg, const char* opt, const char** out) { - if (begins_with(arg, opt)) *out = arg + strlen(opt); -} - -void trusted_utils_try_match_num(const char* arg, const char* opt, u64* out) { - const char* start_of_number = arg + strlen(opt); - if (begins_with(arg, opt)) *out = strtol( start_of_number, NULL, 10); -} - -void trusted_utils_try_match_flag(const char* arg, const char* opt, bool* out) { - if (begins_with(arg, opt)) *out = true; -} - -void trusted_utils_copy_bytes(u8* to, const u8* from, u64 nb_bytes) { - for (u64 i = 0; i < nb_bytes; i++) to[i] = from[i]; -} - -bool trusted_utils_equal_signatures(const u8* left, const u8* right) { - for (u64 i = 0; i < SIG_SIZE_BYTES; i++) - if (left[i] != right[i]) return false; - return true; -} - -void* trusted_utils_malloc(u64 size) { - void* res = malloc(size); - if (!res) exit_oom(); - return res; -} -void* trusted_utils_realloc(void* from, u64 new_size) { - void* res = realloc(from, new_size); - if (!res) exit_oom(); - return res; -} -void* trusted_utils_calloc(u64 nb_objs, u64 size_per_obj) { - void* res = calloc(nb_objs, size_per_obj); - if (!res) exit_oom(); - return res; -} - -bool trusted_utils_read_bool(FILE* file) { - int res = UNLOCKED_IO(fgetc)(file); - if (res == EOF) trusted_utils_exit_eof(); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_bool(res ? 1 : 0); -#endif - return res ? 1 : 0; -} -int trusted_utils_read_char(FILE* file) { - int res = UNLOCKED_IO(fgetc)(file); - if (res == EOF) trusted_utils_exit_eof(); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_char(res); -#endif - return res; -} -void trusted_utils_read_objs(void* data, size_t size, size_t nb_objs, FILE* file) { - u64 nb_read = UNLOCKED_IO(fread)(data, size, nb_objs, file); - if (nb_read < nb_objs) trusted_utils_exit_eof(); -} -int trusted_utils_read_int(FILE* file) { - int i; - trusted_utils_read_objs(&i, sizeof(int), 1, file); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_int(i); -#endif - return i; -} -void trusted_utils_read_ints(int* data, u64 nb_ints, FILE* file) { - trusted_utils_read_objs(data, sizeof(int), nb_ints, file); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_ints(data, nb_ints); -#endif -} -u64 trusted_utils_read_ul(FILE* file) { - u64 u; - trusted_utils_read_objs(&u, sizeof(u64), 1, file); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_ul(u); -#endif - return u; -} -void trusted_utils_read_uls(u64* data, u64 nb_uls, FILE* file) { - trusted_utils_read_objs(data, sizeof(u64), nb_uls, file); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_uls(data, nb_uls); -#endif -} -void trusted_utils_read_sig(u8* out_sig, FILE* file) { - signature dummy; - if (!out_sig) out_sig = dummy; - trusted_utils_read_objs(out_sig, sizeof(int), 4, file); -#ifdef IMPCHECK_WRITE_DIRECTIVES - write_sig(out_sig); -#endif -} - -void trusted_utils_write_char(char c, FILE* file) { - int res = UNLOCKED_IO(fputc)(c, file); - if (res == EOF) trusted_utils_exit_eof(); -} -void trusted_utils_write_bool(bool b, FILE* file) { - int res = UNLOCKED_IO(fputc)(b ? 1 : 0, file); - if (res == EOF) trusted_utils_exit_eof(); -} -void write_objs(const void* data, size_t size, size_t nb_objs, FILE* file) { - u64 nb_read = UNLOCKED_IO(fwrite)(data, size, nb_objs, file); - if (nb_read < nb_objs) trusted_utils_exit_eof(); -} -void trusted_utils_write_int(int i, FILE* file) { - write_objs(&i, sizeof(int), 1, file); -} -void trusted_utils_write_ints(const int* data, u64 nb_ints, FILE* file) { - write_objs(data, sizeof(int), nb_ints, file); -} -void trusted_utils_write_ul(u64 u, FILE* file) { - write_objs(&u, sizeof(u64), 1, file); -} -void trusted_utils_write_uls(const u64* data, u64 nb_uls, FILE* file) { - write_objs(data, sizeof(u64), nb_uls, file); -} -void trusted_utils_write_sig(const u8* sig, FILE* file) { - write_objs(sig, sizeof(int), 4, file); -} - -void trusted_utils_sig_to_str(const u8* sig, char* out) { - for (int charpos = 0; charpos < SIG_SIZE_BYTES; charpos++) { - char val1 = (sig[charpos] >> 4) & 0x0f; - char val2 = sig[charpos] & 0x0f; - assert(val1 >= 0 && val1 < 16); - assert(val2 >= 0 && val2 < 16); - out[2*charpos+0] = val1>=10 ? 'a'+val1-10 : '0'+val1; - out[2*charpos+1] = val2>=10 ? 'a'+val2-10 : '0'+val2; - } - out[SIG_SIZE_BYTES*2] = '\0'; -} - -bool trusted_utils_str_to_sig(const char* str, u8* out) { - for (int bytepos = 0; bytepos < SIG_SIZE_BYTES; bytepos++) { - const char* hex_pair = str + bytepos*2; - char hex1 = hex_pair[0]; char hex2 = hex_pair[1]; - int byte = 16 * (hex1 >= '0' && hex1 <= '9' ? hex1-'0' : 10+hex1-'a') - + (hex2 >= '0' && hex2 <= '9' ? hex2-'0' : 10+hex2-'a'); - if (byte < 0 || byte >= 256) return false; - out[bytepos] = (u8) byte; - } - return true; -} + +#include "trusted_utils.h" +#include +#include +#if IMPCHECK_WRITE_DIRECTIVES +#include "../writer.h" +#endif +#include +#include // exit +#include // getpid + +char trusted_utils_msgstr[512] = ""; + +void trusted_utils_log(const char* msg) { + printf("c [TRUSTED_CORE %i] %s\n", getpid(), msg); +} +void trusted_utils_log_err(const char* msg) { + printf("c [TRUSTED_CORE %i] [ERROR] %s\n", getpid(), msg); +} + +void trusted_utils_exit_eof() { + trusted_utils_log("end-of-file - terminating"); + exit(0); +} +void exit_oom() { + trusted_utils_log("allocation failed - terminating"); + exit(0); +} + +bool begins_with(const char* str, const char* prefix) { + u64 i = 0; + while (true) { + if (prefix[i] == '\0') return true; + if (str[i] == '\0') return prefix[i] == '\0'; + if (str[i] != prefix[i]) return false; + i++; + } +} + +void trusted_utils_try_match_arg(const char* arg, const char* opt, const char** out) { + if (begins_with(arg, opt)) *out = arg + strlen(opt); +} + +void trusted_utils_try_match_num(const char* arg, const char* opt, u64* out) { + const char* start_of_number = arg + strlen(opt); + if (begins_with(arg, opt)) *out = strtol( start_of_number, NULL, 10); +} + +void trusted_utils_try_match_flag(const char* arg, const char* opt, bool* out) { + if (begins_with(arg, opt)) *out = true; +} + +void trusted_utils_copy_bytes(u8* to, const u8* from, u64 nb_bytes) { + for (u64 i = 0; i < nb_bytes; i++) to[i] = from[i]; +} + +bool trusted_utils_equal_signatures(const u8* left, const u8* right) { + for (u64 i = 0; i < SIG_SIZE_BYTES; i++) + if (left[i] != right[i]) return false; + return true; +} + +void* trusted_utils_malloc(u64 size) { + void* res = malloc(size); + if (!res) exit_oom(); + return res; +} +void* trusted_utils_realloc(void* from, u64 new_size) { + void* res = realloc(from, new_size); + if (!res) exit_oom(); + return res; +} +void* trusted_utils_calloc(u64 nb_objs, u64 size_per_obj) { + void* res = calloc(nb_objs, size_per_obj); + if (!res) exit_oom(); + return res; +} + +bool trusted_utils_read_bool(FILE* file) { + int res = UNLOCKED_IO(fgetc)(file); + if (res == EOF) trusted_utils_exit_eof(); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_bool(res ? 1 : 0); +#endif + return res ? 1 : 0; +} +int trusted_utils_read_char(FILE* file) { + int res = UNLOCKED_IO(fgetc)(file); + if (res == EOF) trusted_utils_exit_eof(); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_char(res); +#endif + return res; +} +void trusted_utils_read_objs(void* data, size_t size, size_t nb_objs, FILE* file) { + u64 nb_read = UNLOCKED_IO(fread)(data, size, nb_objs, file); + if (nb_read < nb_objs) trusted_utils_exit_eof(); +} +int trusted_utils_read_int(FILE* file) { + int i; + trusted_utils_read_objs(&i, sizeof(int), 1, file); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_int(i); +#endif + return i; +} +void trusted_utils_read_ints(int* data, u64 nb_ints, FILE* file) { + trusted_utils_read_objs(data, sizeof(int), nb_ints, file); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_ints(data, nb_ints); +#endif +} +u64 trusted_utils_read_ul(FILE* file) { + u64 u; + trusted_utils_read_objs(&u, sizeof(u64), 1, file); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_ul(u); +#endif + return u; +} +void trusted_utils_read_uls(u64* data, u64 nb_uls, FILE* file) { + trusted_utils_read_objs(data, sizeof(u64), nb_uls, file); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_uls(data, nb_uls); +#endif +} +void trusted_utils_read_sig(u8* out_sig, FILE* file) { + signature dummy; + if (!out_sig) out_sig = dummy; + trusted_utils_read_objs(out_sig, sizeof(int), 4, file); +#ifdef IMPCHECK_WRITE_DIRECTIVES + write_sig(out_sig); +#endif +} + +void trusted_utils_write_char(char c, FILE* file) { + int res = UNLOCKED_IO(fputc)(c, file); + if (res == EOF) trusted_utils_exit_eof(); +} +void trusted_utils_write_bool(bool b, FILE* file) { + int res = UNLOCKED_IO(fputc)(b ? 1 : 0, file); + if (res == EOF) trusted_utils_exit_eof(); +} +void write_objs(const void* data, size_t size, size_t nb_objs, FILE* file) { + u64 nb_read = UNLOCKED_IO(fwrite)(data, size, nb_objs, file); + if (nb_read < nb_objs) trusted_utils_exit_eof(); +} +void trusted_utils_write_int(int i, FILE* file) { + write_objs(&i, sizeof(int), 1, file); +} +void trusted_utils_write_ints(const int* data, u64 nb_ints, FILE* file) { + write_objs(data, sizeof(int), nb_ints, file); +} +void trusted_utils_write_ul(u64 u, FILE* file) { + write_objs(&u, sizeof(u64), 1, file); +} +void trusted_utils_write_uls(const u64* data, u64 nb_uls, FILE* file) { + write_objs(data, sizeof(u64), nb_uls, file); +} +void trusted_utils_write_sig(const u8* sig, FILE* file) { + write_objs(sig, sizeof(int), 4, file); +} + +void trusted_utils_sig_to_str(const u8* sig, char* out) { + for (int charpos = 0; charpos < SIG_SIZE_BYTES; charpos++) { + char val1 = (sig[charpos] >> 4) & 0x0f; + char val2 = sig[charpos] & 0x0f; + assert(val1 >= 0 && val1 < 16); + assert(val2 >= 0 && val2 < 16); + out[2*charpos+0] = val1>=10 ? 'a'+val1-10 : '0'+val1; + out[2*charpos+1] = val2>=10 ? 'a'+val2-10 : '0'+val2; + } + out[SIG_SIZE_BYTES*2] = '\0'; +} + +bool trusted_utils_str_to_sig(const char* str, u8* out) { + for (int bytepos = 0; bytepos < SIG_SIZE_BYTES; bytepos++) { + const char* hex_pair = str + bytepos*2; + char hex1 = hex_pair[0]; char hex2 = hex_pair[1]; + int byte = 16 * (hex1 >= '0' && hex1 <= '9' ? hex1-'0' : 10+hex1-'a') + + (hex2 >= '0' && hex2 <= '9' ? hex2-'0' : 10+hex2-'a'); + if (byte < 0 || byte >= 256) return false; + out[bytepos] = (u8) byte; + } + return true; +} diff --git a/src/trusted/trusted_utils.h b/src/trusted/trusted_utils.h index 99f702d..11e9753 100644 --- a/src/trusted/trusted_utils.h +++ b/src/trusted/trusted_utils.h @@ -1,65 +1,65 @@ - -#pragma once - -#include // for _DEFAULT_SOURCE -#include // for bool -#include // for FILE - -#ifdef _MSC_VER -# define MALLOB_LIKELY(condition) condition -# define MALLOB_UNLIKELY(condition) condition -#else -# define MALLOB_LIKELY(condition) __builtin_expect(condition, 1) -# define MALLOB_UNLIKELY(condition) __builtin_expect(condition, 0) -#endif - -#if /* glibc >= 2.19: */ _DEFAULT_SOURCE || /* glibc <= 2.19: */ _SVID_SOURCE || _BSD_SOURCE -#define UNLOCKED_IO(fun) fun##_unlocked -#else -#define UNLOCKED_IO(fun) fun -#endif - -typedef unsigned long u64; -typedef unsigned int u32; -typedef unsigned char u8; - -#define SIG_SIZE_BYTES 16 -typedef u8 signature[SIG_SIZE_BYTES]; -#define TRUSTED_CHK_MAX_BUF_SIZE (1<<14) - -extern char trusted_utils_msgstr[512]; - -void trusted_utils_log(const char* msg); -void trusted_utils_log_err(const char* msg); - -void trusted_utils_exit_eof(); - -void trusted_utils_try_match_arg(const char* arg, const char* opt, const char** out); -void trusted_utils_try_match_num(const char* arg, const char* opt, u64* out); -void trusted_utils_try_match_flag(const char* arg, const char* opt, bool* out); - -void trusted_utils_copy_bytes(u8* to, const u8* from, u64 nb_bytes); -bool trusted_utils_equal_signatures(const u8* left, const u8* right); - -void* trusted_utils_malloc(u64 size); -void* trusted_utils_realloc(void* from, u64 new_size); -void* trusted_utils_calloc(u64 nb_objs, u64 size_per_obj); - -bool trusted_utils_read_bool(FILE* file); -int trusted_utils_read_char(FILE* file); -int trusted_utils_read_int(FILE* file); -void trusted_utils_read_ints(int* data, u64 nb_ints, FILE* file); -u64 trusted_utils_read_ul(FILE* file); -void trusted_utils_read_uls(u64* data, u64 nb_uls, FILE* file); -void trusted_utils_read_sig(u8* out_sig, FILE* file); - -void trusted_utils_write_bool(bool b, FILE* file); -void trusted_utils_write_char(char c, FILE* file); -void trusted_utils_write_int(int i, FILE* file); -void trusted_utils_write_ints(const int* data, u64 nb_ints, FILE* file); -void trusted_utils_write_ul(u64 u, FILE* file); -void trusted_utils_write_uls(const u64* data, u64 nb_uls, FILE* file); -void trusted_utils_write_sig(const u8* sig, FILE* file); - -void trusted_utils_sig_to_str(const u8* sig, char* out); -bool trusted_utils_str_to_sig(const char* str, u8* out); + +#pragma once + +#include // for _DEFAULT_SOURCE +#include // for bool +#include // for FILE + +#ifdef _MSC_VER +# define MALLOB_LIKELY(condition) condition +# define MALLOB_UNLIKELY(condition) condition +#else +# define MALLOB_LIKELY(condition) __builtin_expect(condition, 1) +# define MALLOB_UNLIKELY(condition) __builtin_expect(condition, 0) +#endif + +#if /* glibc >= 2.19: */ _DEFAULT_SOURCE || /* glibc <= 2.19: */ _SVID_SOURCE || _BSD_SOURCE +#define UNLOCKED_IO(fun) fun##_unlocked +#else +#define UNLOCKED_IO(fun) fun +#endif + +typedef unsigned long u64; +typedef unsigned int u32; +typedef unsigned char u8; + +#define SIG_SIZE_BYTES 16 +typedef u8 signature[SIG_SIZE_BYTES]; +#define TRUSTED_CHK_MAX_BUF_SIZE (1<<14) + +extern char trusted_utils_msgstr[512]; + +void trusted_utils_log(const char* msg); +void trusted_utils_log_err(const char* msg); + +void trusted_utils_exit_eof(); + +void trusted_utils_try_match_arg(const char* arg, const char* opt, const char** out); +void trusted_utils_try_match_num(const char* arg, const char* opt, u64* out); +void trusted_utils_try_match_flag(const char* arg, const char* opt, bool* out); + +void trusted_utils_copy_bytes(u8* to, const u8* from, u64 nb_bytes); +bool trusted_utils_equal_signatures(const u8* left, const u8* right); + +void* trusted_utils_malloc(u64 size); +void* trusted_utils_realloc(void* from, u64 new_size); +void* trusted_utils_calloc(u64 nb_objs, u64 size_per_obj); + +bool trusted_utils_read_bool(FILE* file); +int trusted_utils_read_char(FILE* file); +int trusted_utils_read_int(FILE* file); +void trusted_utils_read_ints(int* data, u64 nb_ints, FILE* file); +u64 trusted_utils_read_ul(FILE* file); +void trusted_utils_read_uls(u64* data, u64 nb_uls, FILE* file); +void trusted_utils_read_sig(u8* out_sig, FILE* file); + +void trusted_utils_write_bool(bool b, FILE* file); +void trusted_utils_write_char(char c, FILE* file); +void trusted_utils_write_int(int i, FILE* file); +void trusted_utils_write_ints(const int* data, u64 nb_ints, FILE* file); +void trusted_utils_write_ul(u64 u, FILE* file); +void trusted_utils_write_uls(const u64* data, u64 nb_uls, FILE* file); +void trusted_utils_write_sig(const u8* sig, FILE* file); + +void trusted_utils_sig_to_str(const u8* sig, char* out); +bool trusted_utils_str_to_sig(const char* str, u8* out); From 7d5c825c1af316fb87f575e07eede49a61ceba04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Michae=20D=C3=B6rr?= Date: Wed, 18 Dec 2024 16:35:47 +0100 Subject: [PATCH 3/3] delete space --- src/trusted/trusted_utils.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/trusted/trusted_utils.c b/src/trusted/trusted_utils.c index 1a71ea7..4357a7e 100644 --- a/src/trusted/trusted_utils.c +++ b/src/trusted/trusted_utils.c @@ -43,7 +43,7 @@ void trusted_utils_try_match_arg(const char* arg, const char* opt, const char** void trusted_utils_try_match_num(const char* arg, const char* opt, u64* out) { const char* start_of_number = arg + strlen(opt); - if (begins_with(arg, opt)) *out = strtol( start_of_number, NULL, 10); + if (begins_with(arg, opt)) *out = strtol(start_of_number, NULL, 10); } void trusted_utils_try_match_flag(const char* arg, const char* opt, bool* out) {