Skip to content

goto symex member cleanup #3221

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 6 commits into from
Nov 5, 2018
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
8 changes: 0 additions & 8 deletions src/cbmc/bmc.h
Original file line number Diff line number Diff line change
Expand Up @@ -86,11 +86,6 @@ class bmct:public safety_checkert
ui_message_handler(_message_handler),
driver_callback_after_symex(callback_after_symex)
{
symex.constant_propagation=options.get_bool_option("propagation");
symex.record_coverage=
!options.get_option("symex-coverage-report").empty();
symex.self_loops_to_assumptions =
options.get_bool_option("self-loops-to-assumptions");
}

virtual resultt run(const goto_functionst &goto_functions)
Expand Down Expand Up @@ -162,9 +157,6 @@ class bmct:public safety_checkert
ui_message_handler(_message_handler),
driver_callback_after_symex(callback_after_symex)
{
symex.constant_propagation = options.get_bool_option("propagation");
symex.record_coverage =
!options.get_option("symex-coverage-report").empty();
INVARIANT(
options.get_bool_option("paths"),
"Should only use saved equation & goto_state constructor "
Expand Down
2 changes: 1 addition & 1 deletion src/cbmc/symex_bmc.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ symex_bmct::symex_bmct(
const optionst &options,
path_storaget &path_storage)
: goto_symext(mh, outer_symbol_table, _target, options, path_storage),
record_coverage(false),
record_coverage(!options.get_option("symex-coverage-report").empty()),
symex_coverage(ns)
{
}
Expand Down
2 changes: 1 addition & 1 deletion src/cbmc/symex_bmc.h
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ class symex_bmct: public goto_symext
return symex_coverage.generate_report(goto_functions, path);
}

bool record_coverage;
const bool record_coverage;

unwindsett unwindset;

Expand Down
8 changes: 7 additions & 1 deletion src/goto-instrument/accelerate/scratch_program.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,6 @@ bool scratch_programt::check_sat(bool do_slice)
output(ns, "scratch", std::cout);
#endif

symex.constant_propagation=constant_propagation;
goto_symex_statet::propagationt::valuest constants;

symex.symex_with_state(symex_state, functions, symex_symbol_table);
Expand Down Expand Up @@ -203,3 +202,10 @@ void scratch_programt::append_loop(
}
}
}

optionst scratch_programt::get_default_options()
{
optionst ret;
ret.set_option("simplify", true);
return ret;
}
6 changes: 2 additions & 4 deletions src/goto-instrument/accelerate/scratch_program.h
Original file line number Diff line number Diff line change
Expand Up @@ -43,16 +43,13 @@ class scratch_programt:public goto_programt
ns(symbol_table, symex_symbol_table),
equation(),
path_storage(),
options(),
options(get_default_options()),
symex(mh, symbol_table, equation, options, path_storage),
satcheck(util_make_unique<satcheckt>()),
satchecker(ns, *satcheck),
z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
checker(&z3) // checker(&satchecker)
{
// Unconditionally set for performance reasons. This option setting applies
// only to this program.
options.set_option("simplify", true);
}

void append(goto_programt::instructionst &instructions);
Expand Down Expand Up @@ -91,6 +88,7 @@ class scratch_programt:public goto_programt
bv_pointerst satchecker;
smt2_dect z3;
prop_convt *checker;
static optionst get_default_options();
};

#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
2 changes: 1 addition & 1 deletion src/goto-symex/goto_symex.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ unsigned goto_symext::dynamic_counter=0;

void goto_symext::do_simplify(exprt &expr)
{
if(options.get_bool_option("simplify"))
if(simplify_opt)
simplify(expr, ns);
}

Expand Down
24 changes: 15 additions & 9 deletions src/goto-symex/goto_symex.h
Original file line number Diff line number Diff line change
Expand Up @@ -55,14 +55,18 @@ class goto_symext
const optionst &options,
path_storaget &path_storage)
: should_pause_symex(false),
options(options),
max_depth(options.get_unsigned_int_option("depth")),
doing_path_exploration(options.is_set("paths")),
allow_pointer_unsoundness(
options.get_bool_option("allow-pointer-unsoundness")),
constant_propagation(true),
self_loops_to_assumptions(true),
language_mode(),
constant_propagation(options.get_bool_option("propagation")),
self_loops_to_assumptions(
options.get_bool_option("self-loops-to-assumptions")),
simplify_opt(options.get_bool_option("simplify")),
unwinding_assertions(options.get_bool_option("unwinding-assertions")),
partial_loops(options.get_bool_option("partial-loops")),
debug_level(options.get_option("debug-level")),
outer_symbol_table(outer_symbol_table),
ns(outer_symbol_table),
target(_target),
Expand Down Expand Up @@ -200,8 +204,6 @@ class goto_symext
const get_goto_functiont &,
statet &);

const optionst &options;

const unsigned max_depth;
const bool doing_path_exploration;
const bool allow_pointer_unsoundness;
Expand All @@ -210,14 +212,18 @@ class goto_symext
// these bypass the target maps
virtual void symex_step_goto(statet &, bool taken);

bool constant_propagation;
bool self_loops_to_assumptions;

/// language_mode: ID_java, ID_C or another language identifier
/// if we know the source language in use, irep_idt() otherwise.
irep_idt language_mode;

protected:
const bool constant_propagation;
const bool self_loops_to_assumptions;
const bool simplify_opt;
const bool unwinding_assertions;
const bool partial_loops;
const std::string debug_level;

/// The symbol table associated with the goto-program that we're
/// executing. This symbol table will not additionally contain objects
/// that are dynamically created as part of symbolic execution; the
Expand Down Expand Up @@ -274,7 +280,7 @@ class goto_symext

// guards

irep_idt guard_identifier;
const irep_idt guard_identifier;

// symex
virtual void symex_transition(
Expand Down
2 changes: 1 addition & 1 deletion src/goto-symex/symex_assign.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -247,7 +247,7 @@ void goto_symext::symex_assign_symbol(
ssa_lhs,
ssa_rhs,
ns,
options.get_bool_option("simplify"),
simplify_opt,
constant_propagation,
allow_pointer_unsoundness);

Expand Down
2 changes: 1 addition & 1 deletion src/goto-symex/symex_builtin_functions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -458,7 +458,7 @@ void goto_symext::symex_trace(
{
PRECONDITION(code.arguments().size() >= 2);

int debug_thresh=unsafe_string2int(options.get_option("debug-level"));
int debug_thresh = unsafe_string2int(debug_level);

mp_integer debug_lvl;
optionalt<mp_integer> maybe_debug =
Expand Down
1 change: 0 additions & 1 deletion src/goto-symex/symex_dereference.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -281,7 +281,6 @@ void goto_symext::dereference_rec(
value_set_dereferencet dereference(
ns,
state.symbol_table,
options,
symex_dereference_state,
language_mode,
expr_is_not_null);
Expand Down
4 changes: 2 additions & 2 deletions src/goto-symex/symex_function_call.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -236,13 +236,13 @@ void goto_symext::symex_function_call_code(
// see if it's too much
if(stop_recursing)
{
if(options.get_bool_option("partial-loops"))
if(partial_loops)
{
// it's ok, ignore
}
else
{
if(options.get_bool_option("unwinding-assertions"))
if(unwinding_assertions)
vcc(false_exprt(), "recursion unwinding assertion", state);

// add to state guard to prevent further assignments
Expand Down
6 changes: 0 additions & 6 deletions src/goto-symex/symex_goto.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -515,12 +515,6 @@ void goto_symext::loop_bound_exceeded(
else
negated_cond=not_exprt(guard);

bool unwinding_assertions=
options.get_bool_option("unwinding-assertions");

bool partial_loops=
options.get_bool_option("partial-loops");

if(!partial_loops)
{
if(unwinding_assertions)
Expand Down
14 changes: 7 additions & 7 deletions src/pointer-analysis/goto_program_dereference.h
Original file line number Diff line number Diff line change
Expand Up @@ -30,13 +30,13 @@ class goto_program_dereferencet:protected dereference_callbackt
const namespacet &_ns,
symbol_tablet &_new_symbol_table,
const optionst &_options,
value_setst &_value_sets):
options(_options),
ns(_ns),
value_sets(_value_sets),
dereference(_ns, _new_symbol_table, _options, *this, ID_nil, false)
{
}
value_setst &_value_sets)
: options(_options),
ns(_ns),
value_sets(_value_sets),
dereference(_ns, _new_symbol_table, *this, ID_nil, false)
{
}

void dereference_program(
goto_programt &goto_program,
Expand Down
5 changes: 0 additions & 5 deletions src/pointer-analysis/value_set_dereference.h
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,6 @@ class value_set_dereferencet
/*! \brief Constructor
* \param _ns Namespace
* \param _new_symbol_table A symbol_table to store new symbols in
* \param _options Options, in particular whether pointer checks are
to be performed
* \param _dereference_callback Callback object for error reporting
* \param _language_mode Mode for any new symbols created to represent
a dereference failure
Expand All @@ -43,13 +41,11 @@ class value_set_dereferencet
value_set_dereferencet(
const namespacet &_ns,
symbol_tablet &_new_symbol_table,
const optionst &_options,
dereference_callbackt &_dereference_callback,
const irep_idt _language_mode,
bool _exclude_null_derefs):
ns(_ns),
new_symbol_table(_new_symbol_table),
options(_options),
dereference_callback(_dereference_callback),
language_mode(_language_mode),
exclude_null_derefs(_exclude_null_derefs)
Expand Down Expand Up @@ -83,7 +79,6 @@ class value_set_dereferencet
private:
const namespacet &ns;
symbol_tablet &new_symbol_table;
const optionst &options;
dereference_callbackt &dereference_callback;
/// language_mode: ID_java, ID_C or another language identifier
/// if we know the source language in use, irep_idt() otherwise.
Expand Down