Skip to content

De-duplicate initialize_goto_model's code [blocks: #5837] #6697

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 1 commit into from
Feb 28, 2022
Merged

De-duplicate initialize_goto_model's code [blocks: #5837] #6697

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
103 changes: 15 additions & 88 deletions jbmc/src/java_bytecode/lazy_goto_model.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,17 +5,17 @@

#include "lazy_goto_model.h"

#include "java_bytecode_language.h"
#include <util/config.h>
#include <util/exception_utils.h>
#include <util/journalling_symbol_table.h>
#include <util/options.h>

#include <goto-programs/initialize_goto_model.h>
#include <goto-programs/read_goto_binary.h>
#include <goto-programs/rebuild_goto_start_function.h>

#include <langapi/mode.h>

#include <util/config.h>
#include <util/exception_utils.h>
#include <util/journalling_symbol_table.h>
#include <util/options.h>
#include "java_bytecode_language.h"

#ifdef _MSC_VER
# include <util/unicode.h>
Expand Down Expand Up @@ -164,93 +164,20 @@ void lazy_goto_modelt::initialize(
}
else
{
for(const auto &filename : sources)
{
#ifdef _MSC_VER
std::ifstream infile(widen(filename));
#else
std::ifstream infile(filename);
#endif

if(!infile)
{
throw system_exceptiont(
"failed to open input file '" + filename + '\'');
}

language_filet &lf = add_language_file(filename);
lf.language = get_language_from_filename(filename);

if(lf.language == nullptr)
{
throw invalid_source_file_exceptiont(
"failed to figure out type of file '" + filename + '\'');
}

languaget &language = *lf.language;
language.set_message_handler(message_handler);
language.set_language_options(options);

msg.status() << "Parsing " << filename << messaget::eom;

if(language.parse(infile, filename))
{
throw invalid_source_file_exceptiont("PARSING ERROR");
}

lf.get_modules();
}

msg.status() << "Converting" << messaget::eom;

if(language_files.typecheck(symbol_table))
{
throw invalid_source_file_exceptiont("CONVERSION ERROR");
}
initialize_from_source_files(
sources, options, language_files, symbol_table, message_handler);
}

if(read_objects_and_link(binaries, *goto_model, message_handler))
throw incorrect_goto_program_exceptiont{"failed to read/link goto model"};

bool binaries_provided_start =
symbol_table.has_symbol(goto_functionst::entry_point());

bool entry_point_generation_failed = false;

if(binaries_provided_start && options.is_set("function"))
{
// The goto binaries provided already contain a __CPROVER_start
// function that may be tied to a different entry point `function`.
// Hence, we will rebuild the __CPROVER_start function.

// Get the language annotation of the existing __CPROVER_start function.
std::unique_ptr<languaget> language =
get_entry_point_language(symbol_table, options, message_handler);

// To create a new entry point we must first remove the old one
remove_existing_entry_point(symbol_table);

// Create the new entry-point
entry_point_generation_failed =
language->generate_support_functions(symbol_table);

// Remove the function from the goto functions so it is copied back in
// from the symbol table during goto_convert
if(!entry_point_generation_failed)
unload(goto_functionst::entry_point());
}
else if(!binaries_provided_start)
{
// Allow all language front-ends to try to provide the user-specified
// (--function) entry-point, or some language-specific default:
entry_point_generation_failed =
language_files.generate_support_functions(symbol_table);
}

if(entry_point_generation_failed)
{
throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
}
set_up_custom_entry_point(
language_files,
symbol_table,
[this](const irep_idt &id) { goto_functions.unload(id); },
options,
false,
message_handler);

// stupid hack
config.set_object_bits_from_symbol_table(symbol_table);
Expand Down
5 changes: 0 additions & 5 deletions jbmc/src/java_bytecode/lazy_goto_model.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -183,11 +183,6 @@ class lazy_goto_modelt : public abstract_goto_modelt
/// Eagerly loads all functions from the symbol table.
void load_all_functions() const;

void unload(const irep_idt &name) const
{
goto_functions.unload(name);
}

language_filet &add_language_file(const std::string &filename)
{
return language_files.add_file(filename);
Expand Down
151 changes: 92 additions & 59 deletions src/goto-programs/initialize_goto_model.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,13 +34,13 @@ Author: Daniel Kroening, [email protected]
/// Generate an entry point that calls a function with the given name, based on
/// the functions language mode in the symbol table
static bool generate_entry_point_for_function(
const irep_idt &entry_function_name,
const optionst &options,
goto_modelt &goto_model,
symbol_tablet &symbol_table,
message_handlert &message_handler)
{
auto const entry_function_sym =
goto_model.symbol_table.lookup(entry_function_name);
const irep_idt &entry_function_name = options.get_option("function");
CHECK_RETURN(!entry_function_name.empty());
auto const entry_function_sym = symbol_table.lookup(entry_function_name);
if(entry_function_sym == nullptr)
{
throw invalid_command_line_argument_exceptiont{
Expand All @@ -54,42 +54,23 @@ static bool generate_entry_point_for_function(
CHECK_RETURN(entry_language != nullptr);
entry_language->set_message_handler(message_handler);
entry_language->set_language_options(options);
return entry_language->generate_support_functions(goto_model.symbol_table);
return entry_language->generate_support_functions(symbol_table);
}

goto_modelt initialize_goto_model(
const std::vector<std::string> &files,
message_handlert &message_handler,
const optionst &options)
void initialize_from_source_files(
const std::list<std::string> &sources,
const optionst &options,
language_filest &language_files,
symbol_tablet &symbol_table,
message_handlert &message_handler)
{
messaget msg(message_handler);
if(files.empty())
{
throw invalid_command_line_argument_exceptiont(
"missing program argument",
"filename",
"one or more paths to program files");
}

std::list<std::string> binaries, sources;

for(const auto &file : files)
{
if(is_goto_binary(file, message_handler))
binaries.push_back(file);
else
sources.push_back(file);
}
if(sources.empty())
return;

language_filest language_files;
language_files.set_message_handler(message_handler);

goto_modelt goto_model;
messaget msg(message_handler);

if(!sources.empty())
for(const auto &filename : sources)
{
for(const auto &filename : sources)
{
#ifdef _MSC_VER
std::ifstream infile(widen(filename));
#else
Expand All @@ -107,8 +88,8 @@ goto_modelt initialize_goto_model(

if(lf.language==nullptr)
{
throw invalid_source_file_exceptiont(
"Failed to figure out type of file '" + filename + '\'');
throw invalid_command_line_argument_exceptiont{
"Failed to figure out type of file", filename};
}

languaget &language=*lf.language;
Expand All @@ -119,75 +100,127 @@ goto_modelt initialize_goto_model(

if(language.parse(infile, filename))
{
throw invalid_source_file_exceptiont("PARSING ERROR");
throw invalid_input_exceptiont("PARSING ERROR");
}

lf.get_modules();
}

msg.status() << "Converting" << messaget::eom;

if(language_files.typecheck(goto_model.symbol_table))
if(language_files.typecheck(symbol_table))
{
throw invalid_source_file_exceptiont("CONVERSION ERROR");
throw invalid_input_exceptiont("CONVERSION ERROR");
}
}

if(read_objects_and_link(binaries, goto_model, message_handler))
{
throw invalid_source_file_exceptiont{
"failed to read object or link in files"};
}
}

bool binaries_provided_start=
goto_model.symbol_table.has_symbol(goto_functionst::entry_point());
void set_up_custom_entry_point(
language_filest &language_files,
symbol_tablet &symbol_table,
const std::function<void(const irep_idt &)> &unload,
const optionst &options,
bool try_mode_lookup,
message_handlert &message_handler)
{
bool binaries_provided_start =
symbol_table.has_symbol(goto_functionst::entry_point());

bool entry_point_generation_failed=false;

if(binaries_provided_start && options.is_set("function"))
{
// The goto binaries provided already contain a __CPROVER_start
// function that may be tied to a different entry point `function`.
// Hence, we will rebuild the __CPROVER_start function.

// Get the language annotation of the existing __CPROVER_start function.
std::unique_ptr<languaget> language = get_entry_point_language(
goto_model.symbol_table, options, message_handler);
std::unique_ptr<languaget> language =
get_entry_point_language(symbol_table, options, message_handler);

// To create a new entry point we must first remove the old one
remove_existing_entry_point(goto_model.symbol_table);
remove_existing_entry_point(symbol_table);

// Create the new entry-point
entry_point_generation_failed =
language->generate_support_functions(goto_model.symbol_table);
language->generate_support_functions(symbol_table);

// Remove the function from the goto functions so it is copied back in
// from the symbol table during goto_convert
if(!entry_point_generation_failed)
goto_model.unload(goto_functionst::entry_point());
unload(goto_functionst::entry_point());
}
else if(!binaries_provided_start)
{
if(options.is_set("function"))
if(try_mode_lookup && options.is_set("function"))
{
// no entry point is present; Use the mode of the specified entry function
// to generate one
entry_point_generation_failed = generate_entry_point_for_function(
options.get_option("function"), options, goto_model, message_handler);
options, symbol_table, message_handler);
}
if(entry_point_generation_failed || !options.is_set("function"))
if(
!try_mode_lookup || entry_point_generation_failed ||
!options.is_set("function"))
{
// Allow all language front-ends to try to provide the user-specified
// (--function) entry-point, or some language-specific default:
entry_point_generation_failed =
language_files.generate_support_functions(goto_model.symbol_table);
language_files.generate_support_functions(symbol_table);
}
}

if(entry_point_generation_failed)
{
throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
throw invalid_input_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
}
}

goto_modelt initialize_goto_model(
const std::vector<std::string> &files,
message_handlert &message_handler,
const optionst &options)
{
messaget msg(message_handler);
if(files.empty())
{
throw invalid_command_line_argument_exceptiont(
"missing program argument",
"filename",
"one or more paths to program files");
}

std::list<std::string> binaries, sources;

for(const auto &file : files)
{
if(is_goto_binary(file, message_handler))
binaries.push_back(file);
else
sources.push_back(file);
}

language_filest language_files;
language_files.set_message_handler(message_handler);

goto_modelt goto_model;

initialize_from_source_files(
sources, options, language_files, goto_model.symbol_table, message_handler);

if(read_objects_and_link(binaries, goto_model, message_handler))
throw incorrect_goto_program_exceptiont{"failed to read/link goto model"};

set_up_custom_entry_point(
language_files,
goto_model.symbol_table,
[&goto_model](const irep_idt &id) { goto_model.goto_functions.unload(id); },
options,
true,
message_handler);

if(language_files.final(goto_model.symbol_table))
{
throw invalid_source_file_exceptiont("FINAL STAGE CONVERSION ERROR");
throw invalid_input_exceptiont("FINAL STAGE CONVERSION ERROR");
}

msg.status() << "Generating GOTO Program" << messaget::eom;
Expand Down
Loading