Use FILE * instead of filenames when passing file paths to serializat…

…ion and printing commands (#968)

Previously we were storing a filename in a global variable and then
passing it to a bunch of functions. Each of these functions then had to
call fopen and fclose, which was quite expensive. This PR changes the
behavior so instead we once open a file with fopen at the start of
rewriting, then call a bunch of functions which take a `FILE *` as an
argument, then call fclose once at the end. This gets much better
buffering behavior and reduces the number of syscalls considerably.

When measuring the performance of this code against a "sum to 10k" imp
program with proof hint generation enabled, we saw a time reduction from
3.5m to 2m.

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);
           });
 }
 

include/runtime/header.h

@@ -293,10 +293,9 @@ 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(
     FILE *file, block *subject, char const *sort);
 void printConfigurationInternal(
@@ -325,18 +324,15 @@ string *debug_print_term(block *subject, char const *sort);
 mpz_ptr move_int(mpz_t);
 
 void serializeConfigurations(
-    char const *filename, std::unordered_set<block *, HashBlock, KEq> results);
+    FILE *file, std::unordered_set<block *, HashBlock, KEq> results);
 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);
-void serializeTermToFile(
-    char const *filename, block *subject, char const *sort);
-void serializeRawTermToFile(
-    char const *filename, void *subject, char const *sort);
-void printVariableToFile(char const *filename, char const *varname);
+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 printVariableToFile(FILE *file, char const *varname);
 
 // The following functions have to be generated at kompile time
 // and linked with the interpreter.

runtime/finish_rewriting.ll

@@ -7,10 +7,10 @@ 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
+declare void @fclose(i8*)
 declare i64 @__gmpz_get_ui(%mpz*)
 
 declare i8* @getStderr()
@@ -37,7 +37,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:
@@ -68,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
 }

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)

runtime/main/search.cpp

@@ -11,10 +11,10 @@ uint64_t get_steps(void);
 std::unordered_set<block *, HashBlock, KEq> take_search_steps(
     bool executeToBranch, int64_t depth, int64_t bound, block *subject);
 void printConfigurations(
-    char const *filename, std::unordered_set<block *, HashBlock, KEq> results);
+    FILE *file, std::unordered_set<block *, HashBlock, KEq> results);
 
 void serializeConfigurations(
-    char const *filename, std::unordered_set<block *, HashBlock, KEq> results);
+    FILE *file, std::unordered_set<block *, HashBlock, KEq> results);
 
 static bool hasStatistics = false;
 static bool binaryOutput = false;
@@ -51,13 +51,15 @@ int main(int argc, char **argv) {
   block *input = parseConfiguration(filename);
   std::unordered_set<block *, HashBlock, KEq> 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;
 }

runtime/util/ConfigurationPrinter.cpp

@@ -183,20 +183,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) {
   fmt::print(file, "{}\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
@@ -205,8 +200,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<block *, HashBlock, KEq> results) {
-  FILE *file = fopen(filename, "a");
+    FILE *file, std::unordered_set<block *, HashBlock, KEq> results) {
   auto state = print_state();
 
   writer w = {file, nullptr};
@@ -224,8 +218,6 @@ void printConfigurations(
     }
     sfprintf(&w, ")");
   }
-
-  fclose(file);
 }
 // NOLINTEND(performance-unnecessary-value-param)
 
@@ -253,12 +245,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();
@@ -334,13 +320,8 @@ void printValueOfType(
   }
 }
 
-void printVariableToFile(char const *filename, char const *varname) {
-  FILE *file = fopen(filename, "a");
-
+void printVariableToFile(FILE *file, char const *varname) {
   fmt::print(file, "{}", varname);
   char n = 0;
   fwrite(&n, 1, 1, file);
-  fflush(file);
-
-  fclose(file);
 }

runtime/util/ConfigurationSerializer.cpp

@@ -367,8 +367,7 @@ void serializeConfigurationInternal(
 }
 
 void serializeConfigurations(
-    char const *filename, std::unordered_set<block *, HashBlock, KEq> results) {
-  FILE *file = fopen(filename, "w");
+    FILE *file, std::unordered_set<block *, HashBlock, KEq> results) {
   auto state = serialization_state();
 
   auto w = writer{file, nullptr};
@@ -394,20 +393,16 @@ void serializeConfigurations(
   fwrite(buf, 1, buf_size, file);
 
   free(buf);
-  fclose(file);
 }
 
-void serializeConfigurationToFile(
-    char const *filename, block *subject, bool emit_size) {
+void serializeConfigurationToFile(FILE *file, block *subject, bool emit_size) {
   char *data = nullptr;
   size_t size = 0;
   serializeConfiguration(subject, nullptr, &data, &size, emit_size);
 
-  FILE *file = fopen(filename, "a");
   fwrite(data, 1, size, file);
 
   free(data);
-  fclose(file);
 }
 
 void serializeConfiguration(
@@ -430,38 +425,30 @@ 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) {
+void serializeTermToFile(FILE *file, block *subject, char const *sort) {
   char *data = nullptr;
   size_t size = 0;
   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) {
+void serializeRawTermToFile(FILE *file, void *subject, char const *sort) {
   block *term = constructRawTerm(subject, sort, true);
 
   char *data = nullptr;
   size_t size = 0;
   serializeConfiguration(term, "SortKItem{}", &data, &size, true);
 
-  FILE *file = fopen(filename, "a");
   fwrite(data, 1, size, file);
 
   free(data);
-  fclose(file);
 }
 
 std::shared_ptr<kllvm::KOREPattern>

runtime/util/util.cpp

@@ -38,12 +38,9 @@ block *constructRawTerm(void *subject, char const *sort, bool raw_value) {
   return static_cast<block *>(constructCompositePattern(tag, args));
 }
 
-void printProofHintHeader(char *output_file) {
+void printProofHintHeader(FILE *file) {
   uint32_t version = 4;
-  FILE *file = fopen(output_file, "a");
   fmt::print(file, "HINT");
   fwrite(&version, sizeof(version), 1, file);
-  fflush(file);
-  fclose(file);
 }
 }