Skip to content

Cegis cbmc #1614

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 3 commits into from
Nov 27, 2017
Merged

Cegis cbmc #1614

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1a33c87
refactoring bmc.cpp
polgreen Nov 22, 2017
8b1f65e
Added range-based symex operations
pkesseli Sep 17, 2017
8a389f9
Hook for cegis to freeze program variables
polgreen Nov 22, 2017
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
172 changes: 97 additions & 75 deletions src/cbmc/bmc.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,17 @@ void bmct::do_unwind_module()
// this is a hook for hw-cbmc
}

/// Hook used by CEGIS to selectively freeze variables
/// in the SAT solver after the SSA formula is added to the solver.
/// Freezing variables is necessary to make use of incremental
/// solving with MiniSat SimpSolver.
/// Potentially a useful hook for other applications using
/// incremental solving.
void bmct::freeze_program_variables()
{
// this is a hook for cegis
}

void bmct::error_trace()
{
status() << "Building error trace" << eom;
Expand Down Expand Up @@ -131,6 +142,8 @@ void bmct::do_conversion()
forall_expr_list(it, bmc_constraints)
prop_conv.set_to_true(*it);
}
// hook for cegis to freeze synthesis program vars
freeze_program_variables();
}

decision_proceduret::resultt
Expand Down Expand Up @@ -305,11 +318,10 @@ void bmct::show_program()
}
}

safety_checkert::resultt bmct::run(
const goto_functionst &goto_functions)

void bmct::get_memory_model()
{
const std::string mm=options.get_option("mm");
std::unique_ptr<memory_model_baset> memory_model;

if(mm.empty() || mm=="sc")
memory_model=util_make_unique<memory_model_sct>(ns);
Expand All @@ -321,9 +333,13 @@ safety_checkert::resultt bmct::run(
{
error() << "Invalid memory model " << mm
<< " -- use one of sc, tso, pso" << eom;
return safety_checkert::resultt::ERROR;
throw "invalid memory model";
}
}

void bmct::setup()
{
get_memory_model();
symex.set_message_handler(get_message_handler());
symex.options=options;

Expand All @@ -337,11 +353,13 @@ safety_checkert::resultt bmct::run(

symex.last_source_location.make_nil();

try
{
// get unwinding info
setup_unwind();
}

safety_checkert::resultt bmct::execute(const goto_functionst &goto_functions)
{
try
{
// perform symbolic execution
symex(goto_functions);

Expand All @@ -351,77 +369,12 @@ safety_checkert::resultt bmct::run(
memory_model->set_message_handler(get_message_handler());
(*memory_model)(equation);
}
}

catch(const std::string &error_str)
{
messaget message(get_message_handler());
message.error().source_location=symex.last_source_location;
Copy link
Contributor

@smowton smowton Nov 23, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Has this error-source-location behaviour gone away? Why? If for no particular reason can we restore it?

Copy link
Contributor Author

@polgreen polgreen Nov 23, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I combined two catch statements into one, and used the format of the second, which doesn't have the error source location behaviour (this is the catch statement that I presevered: https://github.com/diffblue/cbmc/blob/develop/src/cbmc/bmc.cpp#L474-L484). I'll add it back in.

message.error() << error_str << messaget::eom;

return safety_checkert::resultt::ERROR;
}

catch(const char *error_str)
{
messaget message(get_message_handler());
message.error().source_location=symex.last_source_location;
message.error() << error_str << messaget::eom;

return safety_checkert::resultt::ERROR;
}

catch(const std::bad_alloc &)
Copy link
Contributor

@smowton smowton Nov 23, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Has some existing catch subsumed this, or has the bad-alloc-catch behaviour gone away altogether?

Copy link
Contributor Author

@polgreen polgreen Nov 23, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've combined two "try catch" statements into one, and everything is now caught at the end of bmct::execute (the bad-alloc-catch is at line 433).

{
error() << "Out of memory" << eom;
return safety_checkert::resultt::ERROR;
}

statistics() << "size of program expression: "
<< equation.SSA_steps.size()
<< " steps" << eom;

try
{
if(options.get_option("slice-by-trace")!="")
{
symex_slice_by_tracet symex_slice_by_trace(ns);

symex_slice_by_trace.slice_by_trace
(options.get_option("slice-by-trace"), equation);
}

if(equation.has_threads())
{
// we should build a thread-aware SSA slicer
statistics() << "no slicing due to threads" << eom;
}
else
{
if(options.get_bool_option("slice-formula"))
{
slice(equation);
statistics() << "slicing removed "
<< equation.count_ignored_SSA_steps()
<< " assignments" << eom;
}
else
{
if(options.get_list_option("cover").empty())
{
simple_slice(equation);
statistics() << "simple slicing removed "
<< equation.count_ignored_SSA_steps()
<< " assignments" << eom;
}
}
}

{
statistics() << "Generated " << symex.total_vccs
<< " VCC(s), " << symex.remaining_vccs
<< " remaining after simplification" << eom;
}
slice();

// coverage report
std::string cov_out=options.get_option("symex-coverage-report");
Expand Down Expand Up @@ -473,13 +426,19 @@ safety_checkert::resultt bmct::run(

catch(const std::string &error_str)
{
error() << error_str << eom;
messaget message(get_message_handler());
message.error().source_location=symex.last_source_location;
message.error() << error_str << messaget::eom;

return safety_checkert::resultt::ERROR;
}

catch(const char *error_str)
{
error() << error_str << eom;
messaget message(get_message_handler());
message.error().source_location=symex.last_source_location;
message.error() << error_str << messaget::eom;

return safety_checkert::resultt::ERROR;
}

Expand All @@ -490,6 +449,56 @@ safety_checkert::resultt bmct::run(
}
}

void bmct::slice()
{
if(options.get_option("slice-by-trace")!="")
{
symex_slice_by_tracet symex_slice_by_trace(ns);

symex_slice_by_trace.slice_by_trace
(options.get_option("slice-by-trace"),
equation);
}
// any properties to check at all?
if(equation.has_threads())
{
// we should build a thread-aware SSA slicer
statistics() << "no slicing due to threads" << eom;
}
else
{
if(options.get_bool_option("slice-formula"))
{
::slice(equation);
statistics() << "slicing removed "
<< equation.count_ignored_SSA_steps()
<< " assignments"<<eom;
}
else
{
if(options.get_list_option("cover").empty())
{
simple_slice(equation);
statistics() << "simple slicing removed "
<< equation.count_ignored_SSA_steps()
<< " assignments"<<eom;
}
}
}
statistics() << "Generated "
<< symex.total_vccs<<" VCC(s), "
<< symex.remaining_vccs
<< " remaining after simplification" << eom;
}

safety_checkert::resultt bmct::run(
const goto_functionst &goto_functions)
{
setup();

return execute(goto_functions);
}

safety_checkert::resultt bmct::decide(
const goto_functionst &goto_functions,
prop_convt &prop_conv)
Expand All @@ -502,6 +511,19 @@ safety_checkert::resultt bmct::decide(
return all_properties(goto_functions, prop_conv);
}

void bmct::show(const goto_functionst &goto_functions)
{
if(options.get_bool_option("show-vcc"))
{
show_vcc();
}

if(options.get_bool_option("program-only"))
{
show_program();
}
}

safety_checkert::resultt bmct::stop_on_fail(
const goto_functionst &goto_functions,
prop_convt &prop_conv)
Expand Down
11 changes: 10 additions & 1 deletion src/cbmc/bmc.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com

#include <goto-symex/symex_target_equation.h>
#include <goto-programs/safety_checker.h>
#include <goto-symex/memory_model.h>

#include "symex_bmc.h"

Expand All @@ -52,6 +53,8 @@ class bmct:public safety_checkert
}

virtual resultt run(const goto_functionst &goto_functions);
void setup();
safety_checkert::resultt execute(const goto_functionst &);
virtual ~bmct() { }

// additional stuff
Expand All @@ -73,7 +76,7 @@ class bmct:public safety_checkert
symex_target_equationt equation;
symex_bmct symex;
prop_convt &prop_conv;

std::unique_ptr<memory_model_baset> memory_model;
// use gui format
ui_message_handlert::uit ui;

Expand All @@ -89,6 +92,8 @@ class bmct:public safety_checkert
virtual void do_unwind_module();
void do_conversion();

virtual void freeze_program_variables();

virtual void show_vcc();
virtual void show_vcc_plain(std::ostream &out);
virtual void show_vcc_json(std::ostream &out);
Expand All @@ -108,6 +113,10 @@ class bmct:public safety_checkert
resultt result,
const goto_functionst &goto_functions);

void get_memory_model();
void slice();
void show(const goto_functionst &);

bool cover(
const goto_functionst &goto_functions,
const optionst::value_listt &criteria);
Expand Down
34 changes: 34 additions & 0 deletions src/goto-symex/goto_symex.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,40 @@ class goto_symext
const goto_functionst &goto_functions,
const goto_programt &goto_program);

/// Symexes from the first instruction and the given state, terminating as
/// soon as the last instruction is reached. This is useful to explicitly
/// symex certain ranges of a program, e.g. in an incremental decision
/// procedure.
/// \param state Symex state to start with.
/// \param goto_functions GOTO model to symex.
/// \param first Entry point in form of a first instruction.
/// \param limit Final instruction, which itself will not be symexed.
virtual void operator()(
statet &state,
const goto_functionst &goto_functions,
goto_programt::const_targett first,
goto_programt::const_targett limit);

/// Initialise the symbolic execution and the given state with <code>pc</code>
/// as entry point.
/// \param state Symex state to initialise.
/// \param goto_functions GOTO model to symex.
/// \param pc first instruction to symex
/// \param limit final instruction, which itself will not
/// be symexed.
void symex_entry_point(
statet &state,
const goto_functionst &goto_functions,
goto_programt::const_targett pc,
goto_programt::const_targett limit);

/// Invokes symex_step and verifies whether additional threads can be
/// executed.
/// \param state Current GOTO symex step.
/// \param goto_functions GOTO model to symex.
void symex_threaded_step(
statet &state, const goto_functionst &goto_functions);

/** execute just one step */
virtual void symex_step(
const goto_functionst &goto_functions,
Expand Down
Loading