diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp index 8c5ecffbcc1..cb7d43de9e8 100644 --- a/src/goto-programs/write_goto_binary.cpp +++ b/src/goto-programs/write_goto_binary.cpp @@ -19,15 +19,12 @@ Author: CM Wintersteiger #include -/// 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 &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