From 403b10f3f67778a5acac856e61e9822708695474 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 5 Feb 2024 13:16:55 -0600 Subject: [PATCH 1/6] change serialization and print methods to pass a FILE * --- include/runtime/header.h | 14 +++++++------- runtime/main/search.cpp | 4 ++-- runtime/util/ConfigurationPrinter.cpp | 21 ++++----------------- runtime/util/ConfigurationSerializer.cpp | 16 ++++------------ runtime/util/util.cpp | 5 +---- 5 files changed, 18 insertions(+), 42 deletions(-) diff --git a/include/runtime/header.h b/include/runtime/header.h index 3eb0450b4..2ed4328e8 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -291,8 +291,8 @@ extern "C" { block *parseConfiguration(char const *filename); block *deserializeConfiguration(char *, size_t); -void printConfiguration(char const *filename, block *subject); -void printStatistics(char const *filename, uint64_t steps); +void printConfiguration(FILE *file, block *subject); +void printStatistics(FILE *file, uint64_t steps); string *printConfigurationToString(block *subject); void printConfigurationToFile(FILE *, block *subject); void printSortedConfigurationToFile( @@ -328,13 +328,13 @@ void serializeConfiguration( block *subject, char const *sort, char **data_out, size_t *size_out, bool emit_size); void serializeConfigurationToFile( - char const *filename, block *subject, bool emit_size); -void writeUInt64ToFile(char const *filename, uint64_t i); + FILE *file, block *subject, bool emit_size); +void writeUInt64ToFile(FILE *file, uint64_t i); void serializeTermToFile( - char const *filename, block *subject, char const *sort); + FILE *file, block *subject, char const *sort); void serializeRawTermToFile( - char const *filename, void *subject, char const *sort); -void printVariableToFile(char const *filename, char const *varname); + FILE *file, void *subject, char const *sort); +void printVariableToFile(FILE *file, char const *varname); // The following functions have to be generated at kompile time // and linked with the interpreter. diff --git a/runtime/main/search.cpp b/runtime/main/search.cpp index 4a87d6580..6d6f0fffc 100644 --- a/runtime/main/search.cpp +++ b/runtime/main/search.cpp @@ -11,10 +11,10 @@ uint64_t get_steps(void); std::unordered_set take_search_steps( bool executeToBranch, int64_t depth, int64_t bound, block *subject); void printConfigurations( - char const *filename, std::unordered_set results); + FILE *file, std::unordered_set results); void serializeConfigurations( - char const *filename, std::unordered_set results); + FILE *file, std::unordered_set results); static bool hasStatistics = false; static bool binaryOutput = false; diff --git a/runtime/util/ConfigurationPrinter.cpp b/runtime/util/ConfigurationPrinter.cpp index 0d32b12a3..fbe137d9b 100644 --- a/runtime/util/ConfigurationPrinter.cpp +++ b/runtime/util/ConfigurationPrinter.cpp @@ -221,20 +221,15 @@ void printConfigurationInternal( sfprintf(file, ")"); } -void printStatistics(char const *filename, uint64_t steps) { - FILE *file = fopen(filename, "w"); +void printStatistics(FILE *file, uint64_t steps) { fprintf(file, "%" PRIu64 "\n", steps - 1); // off by one adjustment - fclose(file); } -void printConfiguration(char const *filename, block *subject) { - FILE *file = fopen(filename, "a"); +void printConfiguration(FILE *file, block *subject) { auto state = print_state(); writer w = {file, nullptr}; printConfigurationInternal(&w, subject, nullptr, false, &state); - - fclose(file); } // If the parameter `results` is passed by reference, the ordering induced by @@ -243,8 +238,7 @@ void printConfiguration(char const *filename, block *subject) { // code is not on a hot path. // NOLINTBEGIN(performance-unnecessary-value-param) void printConfigurations( - char const *filename, std::unordered_set results) { - FILE *file = fopen(filename, "a"); + FILE *file, std::unordered_set results) { auto state = print_state(); writer w = {file, nullptr}; @@ -262,8 +256,6 @@ void printConfigurations( } sfprintf(&w, ")"); } - - fclose(file); } // NOLINTEND(performance-unnecessary-value-param) @@ -372,13 +364,8 @@ void printValueOfType( } } -void printVariableToFile(char const *filename, char const *varname) { - FILE *file = fopen(filename, "a"); - +void printVariableToFile(FILE *file, char const *varname) { fprintf(file, "%s", varname); char n = 0; fwrite(&n, 1, 1, file); - fflush(file); - - fclose(file); } diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index c79d7d777..09b6f0345 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -400,16 +400,14 @@ void serializeConfigurations( } void serializeConfigurationToFile( - char const *filename, block *subject, bool emit_size) { + FILE *file, block *subject, bool emit_size) { char *data; size_t size; serializeConfiguration(subject, nullptr, &data, &size, emit_size); - FILE *file = fopen(filename, "a"); fwrite(data, 1, size, file); free(data); - fclose(file); } void serializeConfiguration( @@ -432,38 +430,32 @@ void serializeConfiguration( *size_out = size; } -void writeUInt64ToFile(char const *filename, uint64_t i) { - FILE *file = fopen(filename, "a"); +void writeUInt64ToFile(FILE *file, uint64_t i) { fwrite(&i, 8, 1, file); - fclose(file); } void serializeTermToFile( - char const *filename, block *subject, char const *sort) { + FILE *file, block *subject, char const *sort) { char *data; size_t size; serializeConfiguration(subject, sort, &data, &size, true); - FILE *file = fopen(filename, "a"); fwrite(data, 1, size, file); free(data); - fclose(file); } void serializeRawTermToFile( - char const *filename, void *subject, char const *sort) { + FILE *file, void *subject, char const *sort) { block *term = constructRawTerm(subject, sort, true); char *data; size_t size; serializeConfiguration(term, "SortKItem{}", &data, &size, true); - FILE *file = fopen(filename, "a"); fwrite(data, 1, size, file); free(data); - fclose(file); } std::shared_ptr diff --git a/runtime/util/util.cpp b/runtime/util/util.cpp index 7a01da9d0..06d3adf2f 100644 --- a/runtime/util/util.cpp +++ b/runtime/util/util.cpp @@ -36,12 +36,9 @@ block *constructRawTerm(void *subject, char const *sort, bool raw_value) { return static_cast(constructCompositePattern(tag, args)); } -void printProofHintHeader(char *output_file) { +void printProofHintHeader(FILE *file) { uint32_t version = 4; - FILE *file = fopen(output_file, "a"); fprintf(file, "HINT"); fwrite(&version, sizeof(version), 1, file); - fflush(file); - fclose(file); } } From e0dd0c4b93f5057c0f93d737cbcd0b5f5856574e Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 5 Feb 2024 13:17:28 -0600 Subject: [PATCH 2/6] delete printConfigurationToFile --- include/runtime/header.h | 1 - runtime/finish_rewriting.ll | 3 +-- runtime/util/ConfigurationPrinter.cpp | 6 ------ 3 files changed, 1 insertion(+), 9 deletions(-) diff --git a/include/runtime/header.h b/include/runtime/header.h index 2ed4328e8..379a21786 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -294,7 +294,6 @@ block *deserializeConfiguration(char *, size_t); void printConfiguration(FILE *file, block *subject); void printStatistics(FILE *file, uint64_t steps); string *printConfigurationToString(block *subject); -void printConfigurationToFile(FILE *, block *subject); void printSortedConfigurationToFile( FILE *file, block *subject, char const *sort); void printConfigurationInternal( diff --git a/runtime/finish_rewriting.ll b/runtime/finish_rewriting.ll index 3d7de729a..c64b6f15c 100644 --- a/runtime/finish_rewriting.ll +++ b/runtime/finish_rewriting.ll @@ -7,7 +7,6 @@ target triple = "@BACKEND_TARGET_TRIPLE@" declare void @printStatistics(i8*, i64) declare void @printConfiguration(i8*, %block*) -declare void @printConfigurationToFile(i8*, %block*) declare void @serializeConfigurationToFile(i8*, %block*) declare void @exit(i32) #0 declare void @abort() #0 @@ -37,7 +36,7 @@ define void @finish_rewriting(%block* %subject, i1 %error) #0 { br i1 %isnull, label %abort, label %print abort: %stderr = call i8* @getStderr() - call void @printConfigurationToFile(i8* %stderr, %block* %subject) + call void @printConfiguration(i8* %stderr, %block* %subject) call void @abort() unreachable print: diff --git a/runtime/util/ConfigurationPrinter.cpp b/runtime/util/ConfigurationPrinter.cpp index fbe137d9b..887c00e09 100644 --- a/runtime/util/ConfigurationPrinter.cpp +++ b/runtime/util/ConfigurationPrinter.cpp @@ -283,12 +283,6 @@ string *printConfigurationToString(block *subject) { return hook_BUFFER_toString(buf); } -void printConfigurationToFile(FILE *file, block *subject) { - auto state = print_state(); - writer w = {file, nullptr}; - printConfigurationInternal(&w, subject, nullptr, false, &state); -} - void printSortedConfigurationToFile( FILE *file, block *subject, char const *sort) { auto state = print_state(); From baade45731cfbc06e532734f7d7cb6e2b84fa71b Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 5 Feb 2024 13:17:47 -0600 Subject: [PATCH 3/6] change call sites so they call fopen and fclose --- bindings/python/runtime.cpp | 4 +++- runtime/finish_rewriting.ll | 2 ++ runtime/main/main.ll | 7 +++++-- runtime/main/search.cpp | 8 +++++--- 4 files changed, 15 insertions(+), 6 deletions(-) diff --git a/bindings/python/runtime.cpp b/bindings/python/runtime.cpp index 8683734e7..f904b4c2d 100644 --- a/bindings/python/runtime.cpp +++ b/bindings/python/runtime.cpp @@ -96,7 +96,9 @@ void bind_runtime(py::module_ &m) { .def( "_serialize_raw", [](block *term, std::string const &filename, std::string const &sort) { - serializeRawTermToFile(filename.c_str(), term, sort.c_str()); + FILE *file = fopen(filename.c_str(), "a"); + serializeRawTermToFile(file, term, sort.c_str()); + fclose(file); }); } diff --git a/runtime/finish_rewriting.ll b/runtime/finish_rewriting.ll index c64b6f15c..a6f312aa2 100644 --- a/runtime/finish_rewriting.ll +++ b/runtime/finish_rewriting.ll @@ -10,6 +10,7 @@ declare void @printConfiguration(i8*, %block*) declare void @serializeConfigurationToFile(i8*, %block*) declare void @exit(i32) #0 declare void @abort() #0 +declare void @fclose(i8*) declare i64 @__gmpz_get_ui(%mpz*) declare i8* @getStderr() @@ -67,6 +68,7 @@ exitCode: br label %exit exit: %exit_ui = phi i32 [ %exit_trunc, %exitCode ], [ 113, %tail ] + call void @fclose(i8* %output) call void @exit(i32 %exit_ui) unreachable } diff --git a/runtime/main/main.ll b/runtime/main/main.ll index fa2047e10..3209c28d3 100644 --- a/runtime/main/main.ll +++ b/runtime/main/main.ll @@ -6,6 +6,7 @@ target triple = "@BACKEND_TARGET_TRIPLE@" declare %block* @parseConfiguration(i8*) declare i64 @atol(i8*) +declare i8* @fopen(i8*, i8*) declare %block* @take_steps(i64, %block*) declare void @finish_rewriting(%block*, i1) #0 @@ -19,6 +20,7 @@ declare void @printProofHintHeader(i8*) @proof_out.flag = private constant [15 x i8] c"--proof-output\00" @output_file = external global i8* +@a_str = private constant [2 x i8] c"a\00" @statistics = external global i1 @binary_output = external global i1 @proof_output = external global i1 @@ -87,7 +89,8 @@ entry: %depth = call i64 @atol(i8* %depth_str) %output_ptr = getelementptr inbounds i8*, i8** %argv, i64 3 %output_str = load i8*, i8** %output_ptr - store i8* %output_str, i8** @output_file + %output_file = call i8* @fopen(i8* %output_str, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @a_str, i64 0, i64 0)) + store i8* %output_file, i8** @output_file call void @parse_flags(i32 %argc, i8** %argv) @@ -96,7 +99,7 @@ entry: %proof_output = load i1, i1* @proof_output br i1 %proof_output, label %if, label %else if: - call void @printProofHintHeader(i8* %output_str) + call void @printProofHintHeader(i8* %output_file) br label %else else: %ret = call %block* @parseConfiguration(i8* %filename) diff --git a/runtime/main/search.cpp b/runtime/main/search.cpp index 6d6f0fffc..69071746d 100644 --- a/runtime/main/search.cpp +++ b/runtime/main/search.cpp @@ -51,13 +51,15 @@ int main(int argc, char **argv) { block *input = parseConfiguration(filename); std::unordered_set results = take_search_steps(executeToBranch, depth, bound, input); + FILE *file = fopen(output, "w"); if (hasStatistics) { - printStatistics(output, get_steps()); + printStatistics(file, get_steps()); } if (binaryOutput) { - serializeConfigurations(output, results); + serializeConfigurations(file, results); } else { - printConfigurations(output, results); + printConfigurations(file, results); } + fclose(file); return 0; } From 8cd4c3618aed0c6444013d2ade9e47c329376675 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 5 Feb 2024 14:50:18 -0600 Subject: [PATCH 4/6] fix formatting --- include/runtime/header.h | 9 +++------ runtime/util/ConfigurationSerializer.cpp | 9 +++------ 2 files changed, 6 insertions(+), 12 deletions(-) diff --git a/include/runtime/header.h b/include/runtime/header.h index 379a21786..ff3212e87 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -326,13 +326,10 @@ void serializeConfigurations( void serializeConfiguration( block *subject, char const *sort, char **data_out, size_t *size_out, bool emit_size); -void serializeConfigurationToFile( - FILE *file, block *subject, bool emit_size); +void serializeConfigurationToFile(FILE *file, block *subject, bool emit_size); void writeUInt64ToFile(FILE *file, uint64_t i); -void serializeTermToFile( - FILE *file, block *subject, char const *sort); -void serializeRawTermToFile( - FILE *file, void *subject, char const *sort); +void serializeTermToFile(FILE *file, block *subject, char const *sort); +void serializeRawTermToFile(FILE *file, void *subject, char const *sort); void printVariableToFile(FILE *file, char const *varname); // The following functions have to be generated at kompile time diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index 09b6f0345..2fcc884b8 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -399,8 +399,7 @@ void serializeConfigurations( fclose(file); } -void serializeConfigurationToFile( - FILE *file, block *subject, bool emit_size) { +void serializeConfigurationToFile(FILE *file, block *subject, bool emit_size) { char *data; size_t size; serializeConfiguration(subject, nullptr, &data, &size, emit_size); @@ -434,8 +433,7 @@ void writeUInt64ToFile(FILE *file, uint64_t i) { fwrite(&i, 8, 1, file); } -void serializeTermToFile( - FILE *file, block *subject, char const *sort) { +void serializeTermToFile(FILE *file, block *subject, char const *sort) { char *data; size_t size; serializeConfiguration(subject, sort, &data, &size, true); @@ -445,8 +443,7 @@ void serializeTermToFile( free(data); } -void serializeRawTermToFile( - FILE *file, void *subject, char const *sort) { +void serializeRawTermToFile(FILE *file, void *subject, char const *sort) { block *term = constructRawTerm(subject, sort, true); char *data; From 4da5b4aa57732fc99f455200e2f36184339946af Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 5 Feb 2024 15:42:05 -0600 Subject: [PATCH 5/6] update header file --- include/runtime/header.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/runtime/header.h b/include/runtime/header.h index ff3212e87..4a91be124 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -322,7 +322,7 @@ string *debug_print_term(block *subject, char const *sort); mpz_ptr move_int(mpz_t); void serializeConfigurations( - char const *filename, std::unordered_set results); + FILE *file, std::unordered_set results); void serializeConfiguration( block *subject, char const *sort, char **data_out, size_t *size_out, bool emit_size); From babd3c9fde52c887e292de94c89e4c8e42216ea6 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 5 Feb 2024 16:13:09 -0600 Subject: [PATCH 6/6] fix compile error --- runtime/util/ConfigurationSerializer.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index 2fcc884b8..c723d02c2 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -369,8 +369,7 @@ void serializeConfigurationInternal( } void serializeConfigurations( - char const *filename, std::unordered_set results) { - FILE *file = fopen(filename, "w"); + FILE *file, std::unordered_set results) { auto state = serialization_state(); auto w = writer{file, nullptr}; @@ -396,7 +395,6 @@ void serializeConfigurations( fwrite(buf, 1, buf_size, file); free(buf); - fclose(file); } void serializeConfigurationToFile(FILE *file, block *subject, bool emit_size) {