Skip to content

Tidied up get_main_symbol #1562

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.

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
Show file tree
Hide file tree
Changes from all commits
Commits
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
4 changes: 2 additions & 2 deletions src/java_bytecode/ci_lazy_methods.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -60,9 +60,9 @@ bool ci_lazy_methodst::operator()(
std::vector<irep_idt> method_worklist1;
std::vector<irep_idt> method_worklist2;

auto main_function=
main_function_resultt main_function =
get_main_symbol(symbol_table, main_class, get_message_handler(), true);
if(main_function.stop_convert)
if(!main_function.is_success())
{
// Failed, mark all functions in the given main class(es)
// reaclass_hierarchyable.
Expand Down
4 changes: 2 additions & 2 deletions src/java_bytecode/java_bytecode_language.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -264,8 +264,8 @@ bool java_bytecode_languaget::generate_support_functions(

main_function_resultt res=
get_main_symbol(symbol_table, main_class, get_message_handler());
if(res.stop_convert)
return res.error_found;
if(!res.is_success())
return res.is_error();

// generate the test harness in __CPROVER__start and a call the entry point
return
Expand Down
98 changes: 34 additions & 64 deletions src/java_bytecode/java_entry_point.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -324,9 +324,6 @@ main_function_resultt get_main_symbol(
message_handlert &message_handler,
bool allow_no_body)
{
symbolt symbol;
main_function_resultt res;

messaget message(message_handler);

// find main symbol
Expand All @@ -341,32 +338,25 @@ main_function_resultt get_main_symbol(

if(main_symbol_id==irep_idt())
{
message.error() << "main symbol resolution failed: "
<< error_message << messaget::eom;
res.main_function=symbol;
res.error_found=true;
res.stop_convert=true;
return res;
message.error()
<< "main symbol resolution failed: " << error_message << messaget::eom;
return main_function_resultt::Error;
}

symbol_tablet::symbolst::const_iterator s_it=
symbol_table.symbols.find(main_symbol_id);
const symbolt *symbol = symbol_table.lookup(main_symbol_id);
INVARIANT(
s_it!=symbol_table.symbols.end(),
symbol != nullptr,
"resolve_friendly_method_name should return a symbol-table identifier");

symbol=s_it->second;

// check if it has a body
if(symbol.value.is_nil() && !allow_no_body)
if(symbol->value.is_nil() && !allow_no_body)
{
message.error() << "main method `" << main_class
<< "' has no body" << messaget::eom;
res.main_function=symbol;
res.error_found=true;
res.stop_convert=true;
return res;
message.error()
<< "main method `" << main_class << "' has no body" << messaget::eom;
return main_function_resultt::Error;
}

return *symbol; // Return found function
}
else
{
Expand All @@ -375,69 +365,49 @@ main_function_resultt get_main_symbol(

// are we given a main class?
if(main_class.empty())
{
res.main_function=symbol;
res.error_found=false;
res.stop_convert=true;
return res; // silently ignore
}
return main_function_resultt::NotFound; // silently ignore

std::string entry_method=
id2string(main_class)+".main";
std::string entry_method = id2string(main_class) + ".main";

std::string prefix="java::"+entry_method+":";

// look it up
std::set<irep_idt> matches;
std::set<const symbolt *> matches;

for(symbol_tablet::symbolst::const_iterator
s_it=symbol_table.symbols.begin();
s_it!=symbol_table.symbols.end();
s_it++)
for(const auto &named_symbol : symbol_table.symbols)
{
if(s_it->second.type.id()==ID_code &&
has_prefix(id2string(s_it->first), prefix))
matches.insert(s_it->first);
if(named_symbol.second.type.id() == ID_code
&& has_prefix(id2string(named_symbol.first), prefix))
{
matches.insert(&named_symbol.second);
}
}

if(matches.empty())
{
// Not found, silently ignore
res.main_function=symbol;
res.error_found=false;
res.stop_convert=true;
return res;
}
return main_function_resultt::NotFound;

if(matches.size()>=2)
if(matches.size() > 1)
{
message.error() << "main method in `" << main_class
<< "' is ambiguous" << messaget::eom;
res.main_function=symbolt();
res.error_found=true;
res.stop_convert=true;
return res; // give up with error, no main
message.error()
<< "main method in `" << main_class
<< "' is ambiguous" << messaget::eom;
return main_function_resultt::Error; // give up with error, no main
}

// function symbol
symbol=symbol_table.symbols.find(*matches.begin())->second;
const symbolt &symbol = **matches.begin();

// check if it has a body
if(symbol.value.is_nil() && !allow_no_body)
{
message.error() << "main method `" << main_class
<< "' has no body" << messaget::eom;
res.main_function=symbol;
res.error_found=true;
res.stop_convert=true;
return res; // give up with error
message.error()
<< "main method `" << main_class << "' has no body" << messaget::eom;
return main_function_resultt::Error; // give up with error
}
}

res.main_function=symbol;
res.error_found=false;
res.stop_convert=false;
return res; // give up with error
return symbol; // Return found function
}
}

/// Given the \p symbol_table and the \p main_class to test, this function
Expand Down Expand Up @@ -490,8 +460,8 @@ bool java_entry_point(
messaget message(message_handler);
main_function_resultt res=
get_main_symbol(symbol_table, main_class, message_handler);
if(res.stop_convert)
return res.stop_convert;
if(!res.is_success())
return true;
symbolt symbol=res.main_function;

assert(!symbol.value.is_nil());
Expand Down
34 changes: 30 additions & 4 deletions src/java_bytecode/java_entry_point.h
Original file line number Diff line number Diff line change
Expand Up @@ -26,12 +26,38 @@ bool java_entry_point(
const object_factory_parameterst &object_factory_parameters,
const select_pointer_typet &pointer_type_selector);

typedef struct
struct main_function_resultt
{
enum statust
{
Success,
Error,
NotFound
} status;
symbolt main_function;
bool error_found;
bool stop_convert;
} main_function_resultt;

// Implicit conversion doesn't lose information and allows return of status
// NOLINTNEXTLINE(runtime/explicit)
main_function_resultt(statust status) : status(status)
{
}

// Implicit conversion doesn't lose information and allows return of symbol
// NOLINTNEXTLINE(runtime/explicit)
main_function_resultt(const symbolt &main_function)
: status(Success), main_function(main_function)
{
}

bool is_success() const
{
return status == Success;
}
bool is_error() const
{
return status == Error;
}
};

/// Figures out the entry point of the code to verify
main_function_resultt get_main_symbol(
Expand Down