From 716f451aae36b78b53a414340ef0d91eab45f7f5 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 29 Mar 2023 12:30:17 +0100 Subject: [PATCH 1/5] Separate `read_bin_goto_object` into two functions Because it deserialises two separate things and this helps make the functions smaller and separate the two separate steps. --- src/goto-programs/read_bin_goto_object.cpp | 27 +++++++++++++++++----- 1 file changed, 21 insertions(+), 6 deletions(-) diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 93df35689cb..a419d096cd3 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -20,16 +20,13 @@ Date: June 2006 #include "goto_functions.h" #include "write_goto_binary.h" -/// read goto binary format -/// \par parameters: input stream, symbol_table, functions -/// \return true on error, false otherwise -static bool read_bin_goto_object( +static void read_bin_symbol_table_object( std::istream &in, symbol_table_baset &symbol_table, goto_functionst &functions, irep_serializationt &irepconverter) { - std::size_t count = irepconverter.read_gb_word(in); // # of symbols + const std::size_t count = irepconverter.read_gb_word(in); // # of symbols for(std::size_t i=0; i Date: Wed, 29 Mar 2023 19:11:23 +0100 Subject: [PATCH 2/5] Separate the copying parameter identifers So that the symbol table reading function does not need access to the goto functions. --- src/goto-programs/read_bin_goto_object.cpp | 37 ++++++++++++++++------ 1 file changed, 28 insertions(+), 9 deletions(-) diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index a419d096cd3..370e16448f0 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -23,7 +23,6 @@ Date: June 2006 static void read_bin_symbol_table_object( std::istream &in, symbol_table_baset &symbol_table, - goto_functionst &functions, irep_serializationt &irepconverter) { const std::size_t count = irepconverter.read_gb_word(in); // # of symbols @@ -66,17 +65,36 @@ static void read_bin_symbol_table_object( sym.is_extern = (flags &(1 << 1))!=0; sym.is_volatile = (flags &1)!=0; - if(!sym.is_type && sym.type.id()==ID_code) - { - // makes sure there is an empty function for every function symbol - auto entry = functions.function_map.emplace(sym.name, goto_functiont()); - entry.first->second.set_parameter_identifiers(to_code_type(sym.type)); - } - symbol_table.add(sym); } } +/// The serialised form of the goto-model currently includes the parameter +/// identifiers in the symbol table attached to the types of function symbols. +/// However it is not included in the goto functions. Therefore this function is +/// needed to copy the parameter identifiers from the symbol table to the +/// functions. +static void copy_parameter_identifiers( + const symbol_table_baset &symbol_table, + goto_functionst &functions) +{ + for(const auto &name_symbol : symbol_table) + { + const auto &symbol = name_symbol.second; + if(symbol.is_type) + continue; + + const auto code_type = type_try_dynamic_cast(symbol.type); + if(!code_type) + continue; + + // Makes sure there is an empty function for every function symbol. + auto emplaced = + functions.function_map.emplace(symbol.name, goto_functiont()); + emplaced.first->second.set_parameter_identifiers(*code_type); + } +} + static void read_bin_functions_object( std::istream &in, goto_functionst &functions, @@ -180,7 +198,8 @@ static bool read_bin_goto_object( goto_functionst &functions, irep_serializationt &irepconverter) { - read_bin_symbol_table_object(in, symbol_table, functions, irepconverter); + read_bin_symbol_table_object(in, symbol_table, irepconverter); + copy_parameter_identifiers(symbol_table, functions); read_bin_functions_object(in, functions, irepconverter); return false; } From ee431f2f95fcd9dedc8d3358fd58d17e96b419a3 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 29 Mar 2023 19:43:33 +0100 Subject: [PATCH 3/5] Update internal `read_bin_goto_object` function to return `void` This function is not exposed in the header file and it always returns `false` therefore we can apply this simplification. --- src/goto-programs/read_bin_goto_object.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 370e16448f0..4754bbb1fa9 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -191,8 +191,7 @@ static void read_bin_functions_object( /// read goto binary format /// \par parameters: input stream, symbol_table, functions -/// \return true on error, false otherwise -static bool read_bin_goto_object( +static void read_bin_goto_object( std::istream &in, symbol_table_baset &symbol_table, goto_functionst &functions, @@ -201,7 +200,6 @@ static bool read_bin_goto_object( read_bin_symbol_table_object(in, symbol_table, irepconverter); copy_parameter_identifiers(symbol_table, functions); read_bin_functions_object(in, functions, irepconverter); - return false; } /// reads a goto binary file back into a symbol and a function table @@ -269,7 +267,8 @@ bool read_bin_goto_object( } else if(version == GOTO_BINARY_VERSION) { - return read_bin_goto_object(in, symbol_table, functions, irepconverter); + read_bin_goto_object(in, symbol_table, functions, irepconverter); + return false; } else { From f6c9bbeb54038ac81c95d62ebe74e80783719734 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 29 Mar 2023 19:51:43 +0100 Subject: [PATCH 4/5] Mark the end of `read_bin_goto_object` with `UNREACHABLE` The proceding control flow always returns before this point therefore we can use `UNREACHABLE` to make the control flow more explicit. --- src/goto-programs/read_bin_goto_object.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 4754bbb1fa9..0df49104c27 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -279,5 +279,5 @@ bool read_bin_goto_object( } } - return false; + UNREACHABLE; } From 53bb8fdb09d4e2cf7be6d58bb6b9311341464824 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 29 Mar 2023 19:52:55 +0100 Subject: [PATCH 5/5] Declare the `version` variable as `const` Because it is not mutated after it is read from file. --- src/goto-programs/read_bin_goto_object.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 0df49104c27..f31f398bc71 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -256,7 +256,7 @@ bool read_bin_goto_object( // symbol_serializationt symbolconverter(ic); { - std::size_t version=irepconverter.read_gb_word(in); + const std::size_t version = irepconverter.read_gb_word(in); if(version < GOTO_BINARY_VERSION) {