Skip to content

Make goto_symext a subtype of messaget #1625

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
merged 1 commit into from
Dec 1, 2017
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
1 change: 0 additions & 1 deletion src/cbmc/bmc.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -340,7 +340,6 @@ void bmct::get_memory_model()
void bmct::setup()
{
get_memory_model();
symex.set_message_handler(get_message_handler());
symex.options=options;

{
Expand Down
16 changes: 8 additions & 8 deletions src/cbmc/bmc.h
Original file line number Diff line number Diff line change
Expand Up @@ -38,14 +38,14 @@ class bmct:public safety_checkert
const optionst &_options,
const symbol_tablet &_symbol_table,
message_handlert &_message_handler,
prop_convt &_prop_conv):
safety_checkert(ns, _message_handler),
options(_options),
ns(_symbol_table, new_symbol_table),
equation(ns),
symex(ns, new_symbol_table, equation),
prop_conv(_prop_conv),
ui(ui_message_handlert::uit::PLAIN)
prop_convt &_prop_conv)
: safety_checkert(ns, _message_handler),
options(_options),
ns(_symbol_table, new_symbol_table),
equation(ns),
symex(_message_handler, ns, new_symbol_table, equation),
prop_conv(_prop_conv),
ui(ui_message_handlert::uit::PLAIN)
{
symex.constant_propagation=options.get_bool_option("propagation");
symex.record_coverage=
Expand Down
57 changes: 27 additions & 30 deletions src/cbmc/symex_bmc.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,14 +17,15 @@ Author: Daniel Kroening, [email protected]
#include <util/simplify_expr.h>

symex_bmct::symex_bmct(
message_handlert &mh,
const namespacet &_ns,
symbol_tablet &_new_symbol_table,
symex_targett &_target):
goto_symext(_ns, _new_symbol_table, _target),
record_coverage(false),
max_unwind(0),
max_unwind_is_set(false),
symex_coverage(_ns)
symex_targett &_target)
: goto_symext(mh, _ns, _new_symbol_table, _target),
record_coverage(false),
max_unwind(0),
max_unwind_is_set(false),
symex_coverage(_ns)
{
}

Expand All @@ -37,10 +38,9 @@ void symex_bmct::symex_step(

if(!source_location.is_nil() && last_source_location!=source_location)
{
debug() << "BMC at file " << source_location.get_file()
<< " line " << source_location.get_line()
<< " function " << source_location.get_function()
<< eom;
log.debug() << "BMC at file " << source_location.get_file() << " line "
<< source_location.get_line() << " function "
<< source_location.get_function() << log.eom;

last_source_location=source_location;
}
Expand All @@ -52,15 +52,15 @@ void symex_bmct::symex_step(
state.source.pc->is_assume() &&
simplify_expr(state.source.pc->guard, ns).is_false())
{
statistics() << "aborting path on assume(false) at "
<< state.source.pc->source_location
<< " thread " << state.source.thread_nr;
log.statistics() << "aborting path on assume(false) at "
<< state.source.pc->source_location << " thread "
<< state.source.thread_nr;

const irep_idt &c=state.source.pc->source_location.get_comment();
if(!c.empty())
statistics() << ": " << c;
log.statistics() << ": " << c;

statistics() << eom;
log.statistics() << log.eom;
}

goto_symext::symex_step(goto_functions, state);
Expand Down Expand Up @@ -94,7 +94,7 @@ void symex_bmct::merge_goto(

goto_symext::merge_goto(goto_state, state);

assert(prev_pc->is_goto());
PRECONDITION(prev_pc->is_goto());
if(record_coverage &&
// could the branch possibly be taken?
!prev_guard.is_false() &&
Expand Down Expand Up @@ -132,15 +132,14 @@ bool symex_bmct::get_unwind(

bool abort=unwind>=this_loop_limit;

statistics() << (abort?"Not unwinding":"Unwinding")
<< " loop " << id << " iteration "
<< unwind;
log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
<< " iteration " << unwind;

if(this_loop_limit!=std::numeric_limits<unsigned>::max())
statistics() << " (" << this_loop_limit << " max)";
log.statistics() << " (" << this_loop_limit << " max)";

statistics() << " " << source.pc->source_location
<< " thread " << source.thread_nr << eom;
log.statistics() << " " << source.pc->source_location << " thread "
<< source.thread_nr << log.eom;

return abort;
}
Expand Down Expand Up @@ -176,15 +175,13 @@ bool symex_bmct::get_unwind_recursion(
{
const symbolt &symbol=ns.lookup(id);

statistics() << (abort?"Not unwinding":"Unwinding")
<< " recursion "
<< symbol.display_name()
<< " iteration " << unwind;
log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " recursion "
<< symbol.display_name() << " iteration " << unwind;

if(this_loop_limit!=std::numeric_limits<unsigned>::max())
statistics() << " (" << this_loop_limit << " max)";
log.statistics() << " (" << this_loop_limit << " max)";

statistics() << eom;
log.statistics() << log.eom;
}

return abort;
Expand All @@ -194,7 +191,7 @@ void symex_bmct::no_body(const irep_idt &identifier)
{
if(body_warnings.insert(identifier).second)
{
warning() <<
"**** WARNING: no body for function " << identifier << eom;
log.warning() << "**** WARNING: no body for function " << identifier
<< log.eom;
}
}
5 changes: 2 additions & 3 deletions src/cbmc/symex_bmc.h
Original file line number Diff line number Diff line change
Expand Up @@ -18,12 +18,11 @@ Author: Daniel Kroening, [email protected]

#include "symex_coverage.h"

class symex_bmct:
public goto_symext,
public messaget
class symex_bmct: public goto_symext
{
public:
symex_bmct(
message_handlert &mh,
const namespacet &_ns,
symbol_tablet &_new_symbol_table,
symex_targett &_target);
Expand Down
25 changes: 13 additions & 12 deletions src/goto-instrument/accelerate/accelerate.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -109,14 +109,14 @@ int acceleratet::accelerate_loop(goto_programt::targett &loop_header)
program.update();

#if 1
enumerating_loop_accelerationt
acceleration(
symbol_table,
goto_functions,
program,
loop,
loop_header,
accelerate_limit);
enumerating_loop_accelerationt acceleration(
message_handler,
symbol_table,
goto_functions,
program,
loop,
loop_header,
accelerate_limit);
#else
disjunctive_polynomial_accelerationt
acceleration(symbol_table, goto_functions, program, loop, loop_header);
Expand Down Expand Up @@ -333,7 +333,7 @@ void acceleratet::set_dirty_vars(path_acceleratort &accelerator)

if(jt==dirty_vars_map.end())
{
scratch_programt scratch(symbol_table);
scratch_programt scratch(symbol_table, message_handler);
symbolt new_sym=utils.fresh_symbol("accelerate::dirty", bool_typet());
dirty_var=new_sym.symbol_expr();
dirty_vars_map[*it]=dirty_var;
Expand Down Expand Up @@ -512,7 +512,7 @@ void acceleratet::insert_automaton(trace_automatont &automaton)
// machine.
for(const auto &sym : automaton.alphabet)
{
scratch_programt state_machine(symbol_table);
scratch_programt state_machine(symbol_table, message_handler);
trace_automatont::sym_range_pairt p=transitions.equal_range(sym);

build_state_machine(p.first, p.second, accept_states, state, next_state,
Expand Down Expand Up @@ -648,15 +648,16 @@ int acceleratet::accelerate_loops()
return num_accelerated;
}


void accelerate_functions(
goto_modelt &goto_model,
message_handlert &message_handler,
bool use_z3)
{
Forall_goto_functions(it, goto_model.goto_functions)
{
std::cout << "Accelerating function " << it->first << '\n';
acceleratet accelerate(it->second.body, goto_model, use_z3);
acceleratet accelerate(
it->second.body, goto_model, message_handler, use_z3);

int num_accelerated=accelerate.accelerate_loops();

Expand Down
81 changes: 47 additions & 34 deletions src/goto-instrument/accelerate/accelerate.h
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ Author: Matt Lewis

#include <util/namespace.h>
#include <util/expr.h>
#include <util/message.h>

#include <analyses/natural_loops.h>

Expand All @@ -28,15 +29,18 @@ Author: Matt Lewis

class acceleratet
{
public:
acceleratet(goto_programt &_program,
goto_modelt &_goto_model,
bool _use_z3):
public:
acceleratet(
goto_programt &_program,
goto_modelt &_goto_model,
message_handlert &message_handler,
bool _use_z3)
: message_handler(message_handler),
program(_program),
goto_functions(_goto_model.goto_functions),
symbol_table(_goto_model.symbol_table),
ns(_goto_model.symbol_table),
utils(symbol_table, goto_functions),
utils(symbol_table, message_handler, goto_functions),
use_z3(_use_z3)
{
natural_loops(program);
Expand All @@ -51,46 +55,54 @@ class acceleratet

static const int accelerate_limit = -1;

protected:
void find_paths(goto_programt::targett &loop_header,
pathst &loop_paths,
pathst &exit_paths,
goto_programt::targett &back_jump);
protected:
message_handlert &message_handler;

void extend_path(goto_programt::targett &t,
goto_programt::targett &loop_header,
natural_loops_mutablet::natural_loopt &loop,
patht &prefix,
pathst &loop_paths,
pathst &exit_paths,
goto_programt::targett &back_jump);
void find_paths(
goto_programt::targett &loop_header,
pathst &loop_paths,
pathst &exit_paths,
goto_programt::targett &back_jump);

void extend_path(
goto_programt::targett &t,
goto_programt::targett &loop_header,
natural_loops_mutablet::natural_loopt &loop,
patht &prefix,
pathst &loop_paths,
pathst &exit_paths,
goto_programt::targett &back_jump);

goto_programt::targett find_back_jump(goto_programt::targett loop_header);

void insert_looping_path(goto_programt::targett &loop_header,
goto_programt::targett &back_jump,
goto_programt &looping_path,
patht &inserted_path);
void insert_accelerator(goto_programt::targett &loop_header,
goto_programt::targett &back_jump,
path_acceleratort &accelerator,
subsumed_patht &subsumed);
void insert_looping_path(
goto_programt::targett &loop_header,
goto_programt::targett &back_jump,
goto_programt &looping_path,
patht &inserted_path);
void insert_accelerator(
goto_programt::targett &loop_header,
goto_programt::targett &back_jump,
path_acceleratort &accelerator,
subsumed_patht &subsumed);

void set_dirty_vars(path_acceleratort &accelerator);
void add_dirty_checks();
bool is_underapproximate(path_acceleratort &accelerator);

void make_overflow_loc(goto_programt::targett loop_header,
goto_programt::targett &loop_end,
goto_programt::targett &overflow_loc);
void make_overflow_loc(
goto_programt::targett loop_header,
goto_programt::targett &loop_end,
goto_programt::targett &overflow_loc);

void insert_automaton(trace_automatont &automaton);
void build_state_machine(trace_automatont::sym_mapt::iterator p,
trace_automatont::sym_mapt::iterator end,
state_sett &accept_states,
symbol_exprt state,
symbol_exprt next_state,
scratch_programt &state_machine);
void build_state_machine(
trace_automatont::sym_mapt::iterator p,
trace_automatont::sym_mapt::iterator end,
state_sett &accept_states,
symbol_exprt state,
symbol_exprt next_state,
scratch_programt &state_machine);

symbolt make_symbol(std::string name, typet type);
void decl(symbol_exprt &sym, goto_programt::targett t);
Expand All @@ -117,6 +129,7 @@ class acceleratet

void accelerate_functions(
goto_modelt &,
message_handlert &message_handler,
bool use_z3);

#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H
4 changes: 2 additions & 2 deletions src/goto-instrument/accelerate/acceleration_utils.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ bool acceleration_utilst::check_inductive(
// assert (target1==polynomial1);
// assert (target2==polynomial2);
// ...
scratch_programt program(symbol_table);
scratch_programt program(symbol_table, message_handler);
std::vector<exprt> polynomials_hold;
substitutiont substitution;

Expand Down Expand Up @@ -386,7 +386,7 @@ bool acceleration_utilst::do_assumptions(
// assert(!precondition);

exprt condition=precondition(path);
scratch_programt program(symbol_table);
scratch_programt program(symbol_table, message_handler);

substitutiont substitution;
stash_polynomials(program, polynomials, substitution, path);
Expand Down
Loading