Skip to content

Commit

Permalink
Make goto_symext a subtype of messaget
Browse files Browse the repository at this point in the history 
to enable debug(), status() etc. output from goto_symext.
  • Loading branch information
@karkhaz
karkhaz committed Nov 30, 2017
1 parent 21439f4 commit 6c6f873
Show file tree
Hide file tree
Showing 19 changed files with 231 additions and 182 deletions.
1 change: 0 additions & 1 deletion src/cbmc/bmc.cpp
View file
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
View file
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
View file
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
View file
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
View file
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
View file
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
View file
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

0 comments on commit 6c6f873

Please sign in to comment.