Skip to content

Clean up implementation of goto binary writing #7634

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Mar 29, 2023
Merged

Clean up implementation of goto binary writing #7634

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
da6be77
Split `write_goto_binary` into two functions
thomasspriggs Mar 29, 2023
021f3d1
Remove commented out calls to non-existant outputs
thomasspriggs Mar 29, 2023
4890204
Update internal `write_goto_binary` to return `void`
thomasspriggs Mar 29, 2023
df8461d
Invert condition on body availability check
thomasspriggs Mar 29, 2023
aa61489
Separate out a `write_instructions_binary` function
thomasspriggs Mar 29, 2023
69ec03b
Separate out `function_name` varable
thomasspriggs Mar 29, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
105 changes: 63 additions & 42 deletions src/goto-programs/write_goto_binary.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
{
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down