Skip to content
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

Clean up usage of messaget in *_parse_options classes #4515

Merged
merged 4 commits into from
Apr 11, 2019
Merged

Clean up usage of messaget in *_parse_options classes #4515

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
1e8f5b1
janalyzer_parse_options is not a message
romainbrenguier Apr 10, 2019
a6a06ae
goto_diff_parse_options is not a message
romainbrenguier Apr 10, 2019
af22270
jdiff_parse_options is not a message
romainbrenguier Apr 10, 2019
f9b461a
Remove redundant logger field
romainbrenguier Apr 10, 2019
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
87 changes: 48 additions & 39 deletions jbmc/src/janalyzer/janalyzer_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,6 @@ Author: Daniel Kroening, [email protected]

janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
: parse_options_baset(JANALYZER_OPTIONS, argc, argv, ui_message_handler),
messaget(ui_message_handler),
ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION)
{
}
Expand Down Expand Up @@ -260,7 +259,8 @@ void janalyzer_parse_optionst::get_command_line_options(optionst &options)
if(!options.get_bool_option("domain set"))
{
// Default to constants as it is light-weight but useful
status() << "Domain not specified, defaulting to --constants" << eom;
log.status() << "Domain not specified, defaulting to --constants"
<< messaget::eom;
options.set_option("constants", true);
}
}
Expand Down Expand Up @@ -343,31 +343,33 @@ int janalyzer_parse_optionst::doit()

optionst options;
get_command_line_options(options);
eval_verbosity(
messaget::eval_verbosity(
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);

//
// Print a banner
//
status() << "JANALYZER version " << CBMC_VERSION << " " << sizeof(void *) * 8
<< "-bit " << config.this_architecture() << " "
<< config.this_operating_system() << eom;
log.status() << "JANALYZER version " << CBMC_VERSION << " "
<< sizeof(void *) * 8 << "-bit " << config.this_architecture()
<< " " << config.this_operating_system() << messaget::eom;

register_languages();

if(cmdline.args.size() > 1)
{
error() << "Only one .class, .jar or .gbf file should be directly "
"specified on the command-line. To force loading another another class "
"use '--java-load-class somepackage.SomeClass' or "
"'--lazy-methods-extra-entry-point somepackage.SomeClass.method' along "
"with '--classpath'"
<< messaget::eom;
log.error() << "Only one .class, .jar or .gbf file should be directly "
"specified on the command-line. To force loading another "
"another class "
"use '--java-load-class somepackage.SomeClass' or "
"'--lazy-methods-extra-entry-point "
"somepackage.SomeClass.method' along "
"with '--classpath'"
<< messaget::eom;
return CPROVER_EXIT_USAGE_ERROR;
}

goto_model =
initialize_goto_model(cmdline.args, get_message_handler(), options);
initialize_goto_model(cmdline.args, log.get_message_handler(), options);

if(process_goto_program(options))
return CPROVER_EXIT_INTERNAL_ERROR;
Expand All @@ -386,7 +388,7 @@ int janalyzer_parse_optionst::doit()
{
show_goto_functions(
goto_model,
get_message_handler(),
log.get_message_handler(),
get_ui(),
cmdline.isset("list-goto-functions"));
return CPROVER_EXIT_SUCCESS;
Expand All @@ -404,14 +406,15 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)

if(cmdline.isset("show-taint"))
{
taint_analysis(goto_model, taint_file, get_message_handler(), true, "");
taint_analysis(
goto_model, taint_file, log.get_message_handler(), true, "");
return CPROVER_EXIT_SUCCESS;
}
else
{
std::string json_file = cmdline.get_value("json");
bool result = taint_analysis(
goto_model, taint_file, get_message_handler(), false, json_file);
goto_model, taint_file, log.get_message_handler(), false, json_file);
return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS;
}
}
Expand All @@ -432,7 +435,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
std::ofstream ofs(json_file);
if(!ofs)
{
error() << "Failed to open json output `" << json_file << "'" << eom;
log.error() << "Failed to open json output `" << json_file << "'"
<< messaget::eom;
return CPROVER_EXIT_INTERNAL_ERROR;
}

Expand All @@ -457,7 +461,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
std::ofstream ofs(json_file);
if(!ofs)
{
error() << "Failed to open json output `" << json_file << "'" << eom;
log.error() << "Failed to open json output `" << json_file << "'"
<< messaget::eom;
return CPROVER_EXIT_INTERNAL_ERROR;
}

Expand All @@ -482,7 +487,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
std::ofstream ofs(json_file);
if(!ofs)
{
error() << "Failed to open json output `" << json_file << "'" << eom;
log.error() << "Failed to open json output `" << json_file << "'"
<< messaget::eom;
return CPROVER_EXIT_INTERNAL_ERROR;
}

Expand Down Expand Up @@ -513,7 +519,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)

if(cmdline.isset("show-properties"))
{
show_properties(goto_model, get_message_handler(), get_ui());
show_properties(goto_model, log.get_message_handler(), get_ui());
return CPROVER_EXIT_SUCCESS;
}

Expand All @@ -532,28 +538,29 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)

if(!out)
{
error() << "Failed to open output file `" << outfile << "'" << eom;
log.error() << "Failed to open output file `" << outfile << "'"
<< messaget::eom;
return CPROVER_EXIT_INTERNAL_ERROR;
}

// Build analyzer
status() << "Selecting abstract domain" << eom;
log.status() << "Selecting abstract domain" << messaget::eom;
namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
std::unique_ptr<ai_baset> analyzer(build_analyzer(options, ns));

if(analyzer == nullptr)
{
status() << "Task / Interpreter / Domain combination not supported"
<< messaget::eom;
log.status() << "Task / Interpreter / Domain combination not supported"
<< messaget::eom;
return CPROVER_EXIT_INTERNAL_ERROR;
}

// Run
status() << "Computing abstract states" << eom;
log.status() << "Computing abstract states" << messaget::eom;
(*analyzer)(goto_model);

// Perform the task
status() << "Performing task" << eom;
log.status() << "Performing task" << messaget::eom;
bool result = true;
if(options.get_bool_option("show"))
{
Expand All @@ -563,12 +570,12 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
else if(options.get_bool_option("verify"))
{
result = static_verifier(
goto_model, *analyzer, options, get_message_handler(), out);
goto_model, *analyzer, options, log.get_message_handler(), out);
}
else if(options.get_bool_option("simplify"))
{
result = static_simplifier(
goto_model, *analyzer, options, get_message_handler(), out);
goto_model, *analyzer, options, log.get_message_handler(), out);
}
else if(options.get_bool_option("unreachable-instructions"))
{
Expand All @@ -587,7 +594,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
}
else
{
error() << "Unhandled task" << eom;
log.error() << "Unhandled task" << messaget::eom;
return CPROVER_EXIT_INTERNAL_ERROR;
}

Expand All @@ -596,7 +603,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
}

// Final defensive error case
error() << "no analysis option given -- consider reading --help" << eom;
log.error() << "no analysis option given -- consider reading --help"
<< messaget::eom;
return CPROVER_EXIT_USAGE_ERROR;
}

Expand All @@ -605,23 +613,24 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
try
{
// remove function pointers
status() << "Removing function pointers and virtual functions" << eom;
log.status() << "Removing function pointers and virtual functions"
<< messaget::eom;
remove_function_pointers(
get_message_handler(), goto_model, cmdline.isset("pointer-check"));
log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));

// Java virtual functions -> explicit dispatch tables:
remove_virtual_functions(goto_model);

// remove Java throw and catch
// This introduces instanceof, so order is important:
remove_exceptions_using_instanceof(goto_model, get_message_handler());
remove_exceptions_using_instanceof(goto_model, log.get_message_handler());

// Java instanceof -> clsid comparison:
class_hierarchyt class_hierarchy(goto_model.symbol_table);
remove_instanceof(goto_model, class_hierarchy, get_message_handler());
remove_instanceof(goto_model, class_hierarchy, log.get_message_handler());

// do partial inlining
status() << "Partial Inlining" << eom;
log.status() << "Partial Inlining" << messaget::eom;
goto_partial_inline(goto_model, ui_message_handler);

// remove returns, gcc vectors, complex
Expand All @@ -630,7 +639,7 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
remove_complex(goto_model);

// add generic checks
status() << "Generic Property Instrumentation" << eom;
log.status() << "Generic Property Instrumentation" << messaget::eom;
goto_check(options, goto_model);

// recalculate numbers, etc.
Expand All @@ -642,13 +651,13 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)

catch(const char *e)
{
error() << e << eom;
log.error() << e << messaget::eom;
return true;
}

catch(const std::string &e)
{
error() << e << eom;
log.error() << e << messaget::eom;
return true;
}

Expand All @@ -659,7 +668,7 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)

catch(const std::bad_alloc &)
{
error() << "Out of memory" << eom;
log.error() << "Out of memory" << messaget::eom;
return true;
}

Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/janalyzer/janalyzer_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ class optionst;
JAVA_BYTECODE_LANGUAGE_OPTIONS
// clang-format on

class janalyzer_parse_optionst : public parse_options_baset, public messaget
class janalyzer_parse_optionst : public parse_options_baset
{
public:
virtual int doit() override;
Expand Down
30 changes: 15 additions & 15 deletions jbmc/src/jdiff/jdiff_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,6 @@ Author: Peter Schrammel

jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
: parse_options_baset(JDIFF_OPTIONS, argc, argv, ui_message_handler),
messaget(ui_message_handler),
ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION)
{
}
Expand Down Expand Up @@ -186,19 +185,19 @@ int jdiff_parse_optionst::doit()

optionst options;
get_command_line_options(options);
eval_verbosity(
messaget::eval_verbosity(
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);

//
// Print a banner
//
status() << "JDIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8
<< "-bit " << config.this_architecture() << " "
<< config.this_operating_system() << eom;
log.status() << "JDIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8
<< "-bit " << config.this_architecture() << " "
<< config.this_operating_system() << messaget::eom;

if(cmdline.args.size() != 2)
{
error() << "Please provide two programs to compare" << eom;
log.error() << "Please provide two programs to compare" << messaget::eom;
return CPROVER_EXIT_INCORRECT_TASK;
}

Expand Down Expand Up @@ -226,12 +225,12 @@ int jdiff_parse_optionst::doit()
{
show_goto_functions(
goto_model1,
get_message_handler(),
log.get_message_handler(),
ui_message_handler.get_ui(),
cmdline.isset("list-goto-functions"));
show_goto_functions(
goto_model2,
get_message_handler(),
log.get_message_handler(),
ui_message_handler.get_ui(),
cmdline.isset("list-goto-functions"));
return CPROVER_EXIT_SUCCESS;
Expand Down Expand Up @@ -275,20 +274,21 @@ bool jdiff_parse_optionst::process_goto_program(
{
{
// remove function pointers
status() << "Removing function pointers and virtual functions" << eom;
log.status() << "Removing function pointers and virtual functions"
<< messaget::eom;
remove_function_pointers(
get_message_handler(), goto_model, cmdline.isset("pointer-check"));
log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));

// Java virtual functions -> explicit dispatch tables:
remove_virtual_functions(goto_model);

// remove Java throw and catch
// This introduces instanceof, so order is important:
remove_exceptions_using_instanceof(goto_model, get_message_handler());
remove_exceptions_using_instanceof(goto_model, log.get_message_handler());

// Java instanceof -> clsid comparison:
class_hierarchyt class_hierarchy(goto_model.symbol_table);
remove_instanceof(goto_model, class_hierarchy, get_message_handler());
remove_instanceof(goto_model, class_hierarchy, log.get_message_handler());

mm_io(goto_model);

Expand All @@ -302,7 +302,7 @@ bool jdiff_parse_optionst::process_goto_program(
rewrite_union(goto_model);

// add generic checks
status() << "Generic Property Instrumentation" << eom;
log.status() << "Generic Property Instrumentation" << messaget::eom;
goto_check(options, goto_model);

// checks don't know about adjusted float expressions
Expand All @@ -322,9 +322,9 @@ bool jdiff_parse_optionst::process_goto_program(
if(cmdline.isset("cover"))
{
const auto cover_config = get_cover_config(
options, goto_model.symbol_table, get_message_handler());
options, goto_model.symbol_table, log.get_message_handler());
if(instrument_cover_goals(
cover_config, goto_model, get_message_handler()))
cover_config, goto_model, log.get_message_handler()))
return true;
}

Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/jdiff/jdiff_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ class goto_modelt;
"(compact-output)"
// clang-format on

class jdiff_parse_optionst : public parse_options_baset, public messaget
class jdiff_parse_optionst : public parse_options_baset
{
public:
virtual int doit();
Expand Down
Loading