Merge pull request #7634 from thomasspriggs/tas/refactor_goto_binary_write

Clean up implementation of goto binary writing

Author: tautschnig

src/goto-programs/write_goto_binary.cpp

@@ -19,15 +19,12 @@ Author: CM Wintersteiger
 
 #include <goto-programs/goto_model.h>
 
-/// Writes a goto program to disc, using goto binary format
-bool write_goto_binary(
+/// Writes the symbol table to file.
+static void write_symbol_table_binary(
   std::ostream &out,
   const symbol_table_baset &symbol_table,
-  const goto_functionst &goto_functions,
   irep_serializationt &irepconverter)
 {
-  // first write symbol table
-
   write_gb_word(out, symbol_table.symbols.size());
 
   for(const auto &symbol_pair : symbol_table.symbols)
@@ -70,9 +67,45 @@ bool write_goto_binary(
 
     write_gb_word(out, flags);
   }
+}
+
+static void write_instructions_binary(
+  std::ostream &out,
+  irep_serializationt &irepconverter,
+  const std::pair<const irep_idt, goto_functiont> &fct)
+{
+  write_gb_word(out, fct.second.body.instructions.size());
+
+  for(const auto &instruction : fct.second.body.instructions)
+  {
+    irepconverter.reference_convert(instruction.code(), out);
+    irepconverter.reference_convert(instruction.source_location(), out);
+    write_gb_word(out, (long)instruction.type());
+
+    const auto condition =
+      instruction.has_condition() ? instruction.condition() : true_exprt();
+    irepconverter.reference_convert(condition, out);
 
-  // now write functions, but only those with body
+    write_gb_word(out, instruction.target_number);
 
+    write_gb_word(out, instruction.targets.size());
+
+    for(const auto &t_it : instruction.targets)
+      write_gb_word(out, t_it->target_number);
+
+    write_gb_word(out, instruction.labels.size());
+
+    for(const auto &l_it : instruction.labels)
+      irepconverter.write_string_ref(out, l_it);
+  }
+}
+
+/// Writes the functions to file, but only those with non-empty body.
+static void write_goto_functions_binary(
+  std::ostream &out,
+  const goto_functionst &goto_functions,
+  irep_serializationt &irepconverter)
+{
   unsigned cnt=0;
   for(const auto &gf_entry : goto_functions.function_map)
   {
@@ -84,43 +117,27 @@ bool write_goto_binary(
 
   for(const auto &fct : goto_functions.function_map)
   {
-    if(fct.second.body_available())
-    {
-      // Since version 2, goto functions are not converted to ireps,
-      // instead they are saved in a custom binary format
+    if(!fct.second.body_available())
+      continue;
 
-      write_gb_string(out, id2string(fct.first)); // name
-      write_gb_word(out, fct.second.body.instructions.size()); // # instructions
-
-      for(const auto &instruction : fct.second.body.instructions)
-      {
-        irepconverter.reference_convert(instruction.code(), out);
-        irepconverter.reference_convert(instruction.source_location(), out);
-        write_gb_word(out, (long)instruction.type());
-
-        const auto condition =
-          instruction.has_condition() ? instruction.condition() : true_exprt();
-        irepconverter.reference_convert(condition, out);
-
-        write_gb_word(out, instruction.target_number);
-
-        write_gb_word(out, instruction.targets.size());
-
-        for(const auto &t_it : instruction.targets)
-          write_gb_word(out, t_it->target_number);
-
-        write_gb_word(out, instruction.labels.size());
+    // Since version 2, goto functions are not converted to ireps,
+    // instead they are saved in a custom binary format
 
-        for(const auto &l_it : instruction.labels)
-          irepconverter.write_string_ref(out, l_it);
-      }
-    }
+    const auto function_name = id2string(fct.first);
+    write_gb_string(out, function_name);
+    write_instructions_binary(out, irepconverter, fct);
   }
+}
 
-  // irepconverter.output_map(f);
-  // irepconverter.output_string_map(f);
-
-  return false;
+/// Writes a goto program to disc, using goto binary format
+static void write_goto_binary(
+  std::ostream &out,
+  const symbol_table_baset &symbol_table,
+  const goto_functionst &goto_functions,
+  irep_serializationt &irepconverter)
+{
+  write_symbol_table_binary(out, symbol_table, irepconverter);
+  write_goto_functions_binary(out, goto_functions, irepconverter);
 }
 
 /// Writes a goto program to disc
@@ -151,15 +168,19 @@ bool write_goto_binary(
   irep_serializationt irepconverter(irepc);
 
   if(version < GOTO_BINARY_VERSION)
+  {
     throw invalid_command_line_argument_exceptiont(
       "version " + std::to_string(version) + " no longer supported",
       "supported version = " + std::to_string(GOTO_BINARY_VERSION));
-  else if(version > GOTO_BINARY_VERSION)
+  }
+  if(version > GOTO_BINARY_VERSION)
+  {
     throw invalid_command_line_argument_exceptiont(
       "unknown goto binary version " + std::to_string(version),
       "supported version = " + std::to_string(GOTO_BINARY_VERSION));
-  else
-    return write_goto_binary(out, symbol_table, goto_functions, irepconverter);
+  }
+  write_goto_binary(out, symbol_table, goto_functions, irepconverter);
+  return false;
 }
 
 /// Writes a goto program to disc