Skip to content

Commit

Permalink
Factor out getting & processing goto-model
Browse files Browse the repository at this point in the history 
CBMC's methods for getting a goto-model from a source file, and
processing that goto-model to be ready for bounded model checking, are
now static so that they can be called from clients that wish to set up a
goto-model the same way that CBMC does.
  • Loading branch information
@karkhaz
karkhaz committed Apr 17, 2018
1 parent 751a882 commit 014d151
Show file tree
Hide file tree
Showing 3 changed files with 108 additions and 80 deletions.
3 changes: 2 additions & 1 deletion src/cbmc/bmc.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -321,7 +321,8 @@ class path_explorert : public bmct
" (use --show-loops to get the loop IDs)\n" \
" --show-vcc show the verification conditions\n" \
" --slice-formula remove assignments unrelated to property\n" \
" --unwinding-assertions generate unwinding assertions\n" \
" --unwinding-assertions generate unwinding assertions (cannot be\n" \
" used with --cover or --partial-loops)\n" \
" --partial-loops permit paths with partial loops\n" \
" --no-pretty-names do not simplify identifiers\n" \
" --graphml-witness filename write the witness in GraphML format to " \
Expand Down
174 changes: 97 additions & 77 deletions src/cbmc/cbmc_parse_options.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,13 +97,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
options.set_option("simplify", true);
options.set_option("simplify-if", true);

// Default false
options.set_option("partial-loops", false);
options.set_option("slice-formula", false);
options.set_option("stop-on-fail", false);
options.set_option("unwinding-assertions", false);

// Other
// Other default
options.set_option("arrays-uf", "auto");
}

Expand Down Expand Up @@ -132,6 +126,28 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)

cbmc_parse_optionst::set_default_options(options);

if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
{
error() << "--cover and --unwinding-assertions must not be given together"
<< eom;
exit(CPROVER_EXIT_USAGE_ERROR);
}

if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions"))
{
error() << "--partial-loops and --unwinding-assertions must not be given "
<< "together" << eom;
exit(CPROVER_EXIT_USAGE_ERROR);
}

if(cmdline.isset("reachability-slice") &&
cmdline.isset("reachability-slice-fb"))
{
error() << "--reachability-slice and --reachability-slice-fb must not be "
<< "given together" << eom;
exit(CPROVER_EXIT_USAGE_ERROR);
}

if(cmdline.isset("paths"))
options.set_option("paths", true);

Expand Down Expand Up @@ -165,6 +181,24 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
if(cmdline.isset("cpp11"))
config.cpp.set_cpp11();

if(cmdline.isset("property"))
options.set_option("property", cmdline.get_values("property"));

if(cmdline.isset("drop-unused-functions"))
options.set_option("drop-unused-functions", true);

if(cmdline.isset("string-abstraction"))
options.set_option("string-abstraction", true);

if(cmdline.isset("reachability-slice-fb"))
options.set_option("reachability-slice-fb", true);

if(cmdline.isset("reachability-slice"))
options.set_option("reachability-slice", true);

if(cmdline.isset("nondet-static"))
options.set_option("nondet-static", true);

if(cmdline.isset("no-simplify"))
options.set_option("simplify", false);

Expand Down Expand Up @@ -227,21 +261,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
if(cmdline.isset("partial-loops"))
options.set_option("partial-loops", true);

if(options.is_set("cover") && options.get_bool_option("unwinding-assertions"))
{
error() << "--cover and --unwinding-assertions "
<< "must not be given together" << eom;
exit(CPROVER_EXIT_USAGE_ERROR);
}

if(options.get_bool_option("partial-loops") &&
options.get_bool_option("unwinding-assertions"))
{
error() << "--partial-loops and --unwinding-assertions "
<< "must not be given together" << eom;
exit(CPROVER_EXIT_USAGE_ERROR);
}

// remove unused equations
if(cmdline.isset("slice-formula"))
options.set_option("slice-formula", true);
Expand Down Expand Up @@ -532,7 +551,8 @@ int cbmc_parse_optionst::doit()
return CPROVER_EXIT_SUCCESS;
}

int get_goto_program_ret=get_goto_program(options);
int get_goto_program_ret =
get_goto_program(goto_model, options, cmdline, *this, ui_message_handler);

if(get_goto_program_ret!=-1)
return get_goto_program_ret;
Expand Down Expand Up @@ -585,25 +605,29 @@ bool cbmc_parse_optionst::set_properties()
}

int cbmc_parse_optionst::get_goto_program(
const optionst &options)
goto_modelt &goto_model,
const optionst &options,
const cmdlinet &cmdline,
messaget &log,
ui_message_handlert &ui_message_handler)
{
if(cmdline.args.empty())
{
error() << "Please provide a program to verify" << eom;
log.error() << "Please provide a program to verify" << log.eom;
return CPROVER_EXIT_INCORRECT_TASK;
}

try
{
goto_model=initialize_goto_model(cmdline, get_message_handler());
goto_model = initialize_goto_model(cmdline, ui_message_handler);

if(cmdline.isset("show-symbol-table"))
{
show_symbol_table(goto_model, ui_message_handler.get_ui());
return CPROVER_EXIT_SUCCESS;
}

if(process_goto_program(options))
if(cbmc_parse_optionst::process_goto_program(goto_model, options, log))
return CPROVER_EXIT_INTERNAL_ERROR;

// show it?
Expand All @@ -620,36 +644,36 @@ int cbmc_parse_optionst::get_goto_program(
{
show_goto_functions(
goto_model,
get_message_handler(),
ui_message_handler,
ui_message_handler.get_ui(),
cmdline.isset("list-goto-functions"));
return CPROVER_EXIT_SUCCESS;
}

status() << config.object_bits_info() << eom;
log.status() << config.object_bits_info() << log.eom;
}

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

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

catch(int e)
{
error() << "Numeric exception : " << e << eom;
log.error() << "Numeric exception : " << e << log.eom;
return CPROVER_EXIT_EXCEPTION;
}

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

Expand Down Expand Up @@ -714,7 +738,9 @@ void cbmc_parse_optionst::preprocessing()
}

bool cbmc_parse_optionst::process_goto_program(
const optionst &options)
goto_modelt &goto_model,
const optionst &options,
messaget &log)
{
try
{
Expand All @@ -723,17 +749,17 @@ bool cbmc_parse_optionst::process_goto_program(
remove_asm(goto_model);

// add the library
link_to_library(goto_model, get_message_handler());
link_to_library(goto_model, log.get_message_handler());

if(cmdline.isset("string-abstraction"))
string_instrumentation(goto_model, get_message_handler());
if(options.get_bool_option("string-abstraction"))
string_instrumentation(goto_model, log.get_message_handler());

// remove function pointers
status() << "Removal of function pointers and virtual functions" << eom;
log.status() << "Removal of function pointers and virtual functions" << eom;
remove_function_pointers(
get_message_handler(),
log.get_message_handler(),
goto_model,
cmdline.isset("pointer-check"));
options.get_bool_option("pointer-check"));
// remove catch and throw (introduces instanceof)
remove_exceptions(goto_model);

Expand All @@ -749,27 +775,26 @@ bool cbmc_parse_optionst::process_goto_program(
rewrite_union(goto_model);

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

// checks don't know about adjusted float expressions
adjust_float_expressions(goto_model);

// ignore default/user-specified initialization
// of variables with static lifetime
if(cmdline.isset("nondet-static"))
if(options.get_bool_option("nondet-static"))
{
status() << "Adding nondeterministic initialization "
"of static/global variables" << eom;
log.status() << "Adding nondeterministic initialization "
"of static/global variables"
<< eom;
nondet_static(goto_model);
}

if(cmdline.isset("string-abstraction"))
if(options.get_bool_option("string-abstraction"))
{
status() << "String Abstraction" << eom;
string_abstraction(
goto_model,
get_message_handler());
log.status() << "String Abstraction" << eom;
string_abstraction(goto_model, log.get_message_handler());
}

// add failed symbols
Expand All @@ -782,21 +807,21 @@ bool cbmc_parse_optionst::process_goto_program(
// add loop ids
goto_model.goto_functions.compute_loop_numbers();

if(cmdline.isset("drop-unused-functions"))
if(options.get_bool_option("drop-unused-functions"))
{
// Entry point will have been set before and function pointers removed
status() << "Removing unused functions" << eom;
remove_unused_functions(goto_model, get_message_handler());
log.status() << "Removing unused functions" << eom;
remove_unused_functions(goto_model, log.get_message_handler());
}

// remove skips such that trivial GOTOs are deleted and not considered
// for coverage annotation:
remove_skip(goto_model);

// instrument cover goals
if(cmdline.isset("cover"))
if(options.is_set("cover"))
{
if(instrument_cover_goals(options, goto_model, get_message_handler()))
if(instrument_cover_goals(options, goto_model, log.get_message_handler()))
return true;
}

Expand All @@ -808,37 +833,32 @@ bool cbmc_parse_optionst::process_goto_program(
label_properties(goto_model);

// reachability slice?
if(cmdline.isset("reachability-slice-fb"))
if(options.get_bool_option("reachability-slice-fb"))
{
if(cmdline.isset("reachability-slice"))
{
error() << "--reachability-slice and --reachability-slice-fb "
<< "must not be given together" << eom;
return true;
}

status() << "Performing a forwards-backwards reachability slice" << eom;
if(cmdline.isset("property"))
reachability_slicer(goto_model, cmdline.get_values("property"), true);
log.status() << "Performing a forwards-backwards reachability slice"
<< eom;
if(options.is_set("property"))
reachability_slicer(
goto_model, options.get_list_option("property"), true);
else
reachability_slicer(goto_model, true);
}

if(cmdline.isset("reachability-slice"))
if(options.get_bool_option("reachability-slice"))
{
status() << "Performing a reachability slice" << eom;
if(cmdline.isset("property"))
reachability_slicer(goto_model, cmdline.get_values("property"));
log.status() << "Performing a reachability slice" << eom;
if(options.is_set("property"))
reachability_slicer(goto_model, options.get_list_option("property"));
else
reachability_slicer(goto_model);
}

// full slice?
if(cmdline.isset("full-slice"))
if(options.get_bool_option("full-slice"))
{
status() << "Performing a full slice" << eom;
if(cmdline.isset("property"))
property_slicer(goto_model, cmdline.get_values("property"));
log.status() << "Performing a full slice" << eom;
if(options.is_set("property"))
property_slicer(goto_model, options.get_list_option("property"));
else
full_slicer(goto_model);
}
Expand All @@ -849,25 +869,25 @@ bool cbmc_parse_optionst::process_goto_program(

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

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

catch(int e)
{
error() << "Numeric exception : " << e << eom;
log.error() << "Numeric exception : " << e << eom;
return true;
}

catch(const std::bad_alloc &)
{
error() << "Out of memory" << eom;
log.error() << "Out of memory" << eom;
exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
return true;
}
Expand Down
11 changes: 9 additions & 2 deletions src/cbmc/cbmc_parse_options.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,15 @@ class cbmc_parse_optionst:
/// default behaviour, for example unit tests.
static void set_default_options(optionst &);

static bool process_goto_program(goto_modelt &, const optionst &, messaget &);

static int get_goto_program(
goto_modelt &,
const optionst &,
const cmdlinet &,
messaget &,
ui_message_handlert &);

protected:
goto_modelt goto_model;
ui_message_handlert ui_message_handler;
Expand All @@ -105,8 +114,6 @@ class cbmc_parse_optionst:
void register_languages();
void get_command_line_options(optionst &);
void preprocessing();
int get_goto_program(const optionst &);
bool process_goto_program(const optionst &);
bool set_properties();
};

Expand Down

0 comments on commit 014d151

Please sign in to comment.