Skip to content

goto_symex now uses decision_proceduret API #4533

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 3 commits into from
Apr 18, 2019
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
17 changes: 2 additions & 15 deletions src/goto-checker/bmc_util.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -56,9 +56,9 @@ ssa_step_matches_failing_property(const irep_idt &property_id)
{
return [property_id](
symex_target_equationt::SSA_stepst::const_iterator step,
const prop_convt &prop_conv) {
const decision_proceduret &decision_procedure) {
return step->is_assert() && step->get_property_id() == property_id &&
prop_conv.l_get(step->cond_literal).is_false();
decision_procedure.get(step->cond_handle).is_false();
};
}

Expand Down Expand Up @@ -103,19 +103,6 @@ void output_error_trace(
}
}

void freeze_guards(
const symex_target_equationt &equation,
prop_convt &prop_conv)
{
for(const auto &step : equation.SSA_steps)
{
if(!step.guard_literal.is_constant())
prop_conv.set_frozen(step.guard_literal);
if(step.is_assert() && !step.cond_literal.is_constant())
prop_conv.set_frozen(step.cond_literal);
}
}

/// outputs an error witness in graphml format
void output_graphml(
const goto_tracet &goto_trace,
Expand Down
2 changes: 0 additions & 2 deletions src/goto-checker/bmc_util.h
Original file line number Diff line number Diff line change
Expand Up @@ -60,8 +60,6 @@ void output_error_trace(
const trace_optionst &,
ui_message_handlert &);

void freeze_guards(const symex_target_equationt &, prop_convt &);

void output_graphml(const goto_tracet &, const namespacet &, const optionst &);
void output_graphml(
const symex_target_equationt &,
Expand Down
18 changes: 11 additions & 7 deletions src/goto-checker/counterexample_beautification.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
#include <util/symbol.h>
#include <util/threeval.h>

#include <solvers/prop/literal_expr.h>
#include <solvers/prop/prop_minimize.h>

counterexample_beautificationt::counterexample_beautificationt(
Expand All @@ -41,7 +40,7 @@ void counterexample_beautificationt::get_minimization_list(
it->is_assignment() &&
it->assignment_type == symex_targett::assignment_typet::STATE)
{
if(!prop_conv.l_get(it->guard_literal).is_false())
if(!prop_conv.get(it->guard_handle).is_false())
{
const typet &type = it->ssa_lhs.type();

Expand Down Expand Up @@ -78,10 +77,14 @@ counterexample_beautificationt::get_failed_property(
equation.SSA_steps.begin();
it != equation.SSA_steps.end();
it++)
{
if(
it->is_assert() && prop_conv.l_get(it->guard_literal).is_true() &&
prop_conv.l_get(it->cond_literal).is_false())
it->is_assert() && prop_conv.get(it->guard_handle).is_true() &&
prop_conv.get(it->cond_handle).is_false())
{
return it;
}
}

UNREACHABLE;
return equation.SSA_steps.end();
Expand All @@ -95,7 +98,7 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation)
failed = get_failed_property(boolbv, equation);

// lock the failed assertion
boolbv.set_to(literal_exprt(failed->cond_literal), false);
boolbv.set_to(failed->cond_handle, false);

{
log.status() << "Beautifying counterexample (guards)" << messaget::eom;
Expand All @@ -113,8 +116,9 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation)
it->is_assignment() &&
it->assignment_type != symex_targett::assignment_typet::HIDDEN)
{
if(!it->guard_literal.is_constant())
guard_count[it->guard_literal]++;
literalt l = boolbv.convert(it->guard_handle);
if(!l.is_constant())
guard_count[l]++;
}

// reached failed assertion?
Expand Down
7 changes: 4 additions & 3 deletions src/goto-checker/goto_symex_fault_localizer.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -58,10 +58,11 @@ const SSA_stept &goto_symex_fault_localizert::collect_guards(
step.assignment_type == symex_targett::assignment_typet::STATE &&
!step.ignore)
{
if(!step.guard_literal.is_constant())
literalt l = solver.convert(step.guard_handle);
if(!l.is_constant())
{
auto emplace_result = fault_location.scores.emplace(step.source.pc, 0);
localization_points.emplace(step.guard_literal, emplace_result.first);
localization_points.emplace(l, emplace_result.first);
}
}

Expand Down Expand Up @@ -90,7 +91,7 @@ bool goto_symex_fault_localizert::check(
}

// lock the failed assertion
assumptions.push_back(!failed_step.cond_literal);
assumptions.push_back(!solver.convert(failed_step.cond_handle));

solver.set_assumptions(assumptions);

Expand Down
2 changes: 2 additions & 0 deletions src/goto-checker/goto_symex_fault_localizer.h
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ Author: Peter Schrammel

#include <goto-symex/symex_target_equation.h>

#include <solvers/prop/prop_conv.h>

#include "fault_localization_provider.h"

class goto_symex_fault_localizert
Expand Down
2 changes: 1 addition & 1 deletion src/goto-checker/goto_symex_property_decider.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ exprt goto_symex_property_decidert::goalt::as_expr() const
exprt::operandst conjuncts;
conjuncts.reserve(instances.size());
for(const auto &inst : instances)
conjuncts.push_back(literal_exprt(inst->cond_literal));
conjuncts.push_back(inst->cond_handle);
return conjunction(conjuncts);
}

Expand Down
3 changes: 0 additions & 3 deletions src/goto-checker/multi_path_symex_checker.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -72,9 +72,6 @@ multi_path_symex_checkert::prepare_property_decider(propertiest &properties)
std::chrono::duration<double> solver_runtime = ::prepare_property_decider(
properties, equation, property_decider, ui_message_handler);

if(options.get_bool_option("localize-faults"))
freeze_guards(equation, property_decider.get_solver());

return solver_runtime;
}

Expand Down
101 changes: 60 additions & 41 deletions src/goto-symex/build_goto_trace.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,12 @@ Author: Daniel Kroening

#include <goto-programs/goto_functions.h>

#include <solvers/prop/prop_conv.h>
#include <solvers/prop/prop.h>
#include <solvers/decision_procedure.h>

#include "partial_order_concurrency.h"

static exprt build_full_lhs_rec(
const prop_convt &prop_conv,
const decision_proceduret &decision_procedure,
const namespacet &ns,
const exprt &src_original, // original identifiers
const exprt &src_ssa) // renamed identifiers
Expand All @@ -39,17 +38,18 @@ static exprt build_full_lhs_rec(
if(id==ID_index)
{
// get index value from src_ssa
exprt index_value=prop_conv.get(to_index_expr(src_ssa).index());
exprt index_value = decision_procedure.get(to_index_expr(src_ssa).index());

if(index_value.is_not_nil())
{
simplify(index_value, ns);
index_exprt tmp=to_index_expr(src_original);
tmp.index()=index_value;
tmp.array()=
build_full_lhs_rec(prop_conv, ns,
to_index_expr(src_original).array(),
to_index_expr(src_ssa).array());
tmp.array() = build_full_lhs_rec(
decision_procedure,
ns,
to_index_expr(src_original).array(),
to_index_expr(src_ssa).array());
return std::move(tmp);
}

Expand All @@ -58,22 +58,29 @@ static exprt build_full_lhs_rec(
else if(id==ID_member)
{
member_exprt tmp=to_member_expr(src_original);
tmp.struct_op()=build_full_lhs_rec(
prop_conv, ns,
tmp.struct_op() = build_full_lhs_rec(
decision_procedure,
ns,
to_member_expr(src_original).struct_op(),
to_member_expr(src_ssa).struct_op());
}
else if(id==ID_if)
{
if_exprt tmp2=to_if_expr(src_original);

tmp2.false_case()=build_full_lhs_rec(prop_conv, ns,
tmp2.false_case(), to_if_expr(src_ssa).false_case());
tmp2.false_case() = build_full_lhs_rec(
decision_procedure,
ns,
tmp2.false_case(),
to_if_expr(src_ssa).false_case());

tmp2.true_case()=build_full_lhs_rec(prop_conv, ns,
tmp2.true_case(), to_if_expr(src_ssa).true_case());
tmp2.true_case() = build_full_lhs_rec(
decision_procedure,
ns,
tmp2.true_case(),
to_if_expr(src_ssa).true_case());

exprt tmp=prop_conv.get(to_if_expr(src_ssa).cond());
exprt tmp = decision_procedure.get(to_if_expr(src_ssa).cond());

if(tmp.is_true())
return tmp2.true_case();
Expand All @@ -85,16 +92,19 @@ static exprt build_full_lhs_rec(
else if(id==ID_typecast)
{
typecast_exprt tmp=to_typecast_expr(src_original);
tmp.op()=build_full_lhs_rec(prop_conv, ns,
to_typecast_expr(src_original).op(), to_typecast_expr(src_ssa).op());
tmp.op() = build_full_lhs_rec(
decision_procedure,
ns,
to_typecast_expr(src_original).op(),
to_typecast_expr(src_ssa).op());
return std::move(tmp);
}
else if(id==ID_byte_extract_little_endian ||
id==ID_byte_extract_big_endian)
{
byte_extract_exprt tmp = to_byte_extract_expr(src_original);
tmp.op() = build_full_lhs_rec(
prop_conv, ns, tmp.op(), to_byte_extract_expr(src_ssa).op());
decision_procedure, ns, tmp.op(), to_byte_extract_expr(src_ssa).op());

// re-write into big case-split
}
Expand Down Expand Up @@ -169,7 +179,8 @@ static void update_internal_field(

/// Replace nondet values that appear in \p type by their values as found by
/// \p solver.
static void replace_nondet_in_type(typet &type, const prop_convt &solver)
static void
replace_nondet_in_type(typet &type, const decision_proceduret &solver)
{
if(type.id() == ID_array)
{
Expand All @@ -182,7 +193,8 @@ static void replace_nondet_in_type(typet &type, const prop_convt &solver)

/// Replace nondet values that appear in the type of \p expr and its
/// subexpressions type by their values as found by \p solver.
static void replace_nondet_in_type(exprt &expr, const prop_convt &solver)
static void
replace_nondet_in_type(exprt &expr, const decision_proceduret &solver)
{
replace_nondet_in_type(expr.type(), solver);
for(auto &sub : expr.operands())
Expand All @@ -192,7 +204,7 @@ static void replace_nondet_in_type(exprt &expr, const prop_convt &solver)
void build_goto_trace(
const symex_target_equationt &target,
ssa_step_predicatet is_last_step_to_keep,
const prop_convt &prop_conv,
const decision_proceduret &decision_procedure,
const namespacet &ns,
goto_tracet &goto_trace)
{
Expand All @@ -218,14 +230,14 @@ void build_goto_trace(
{
if(
last_step_to_keep == target.SSA_steps.end() &&
is_last_step_to_keep(it, prop_conv))
is_last_step_to_keep(it, decision_procedure))
{
last_step_to_keep = it;
}

const SSA_stept &SSA_step = *it;

if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
if(!decision_procedure.get(SSA_step.guard_handle).is_true())
continue;

if(it->is_constraint() ||
Expand All @@ -250,7 +262,7 @@ void build_goto_trace(
// these are just used to get the time stamp -- the clock type is
// computed to be of the minimal necessary size, but we don't need to
// know it to get the value so just use typeless
exprt clock_value = prop_conv.get(
exprt clock_value = decision_procedure.get(
symbol_exprt::typeless(partial_order_concurrencyt::rw_clock_id(it)));

const auto cv = numeric_cast<mp_integer>(clock_value);
Expand Down Expand Up @@ -342,7 +354,7 @@ void build_goto_trace(
goto_trace_step.function_arguments = SSA_step.converted_function_arguments;

for(auto &arg : goto_trace_step.function_arguments)
arg = prop_conv.get(arg);
arg = decision_procedure.get(arg);

// update internal field for specific variables in the counterexample
update_internal_field(SSA_step, goto_trace_step, ns);
Expand All @@ -359,15 +371,20 @@ void build_goto_trace(
if(SSA_step.original_full_lhs.is_not_nil())
{
goto_trace_step.full_lhs = build_full_lhs_rec(
prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
replace_nondet_in_type(goto_trace_step.full_lhs, prop_conv);
decision_procedure,
ns,
SSA_step.original_full_lhs,
SSA_step.ssa_full_lhs);
replace_nondet_in_type(goto_trace_step.full_lhs, decision_procedure);
}

if(SSA_step.ssa_full_lhs.is_not_nil())
{
goto_trace_step.full_lhs_value = prop_conv.get(SSA_step.ssa_full_lhs);
goto_trace_step.full_lhs_value =
decision_procedure.get(SSA_step.ssa_full_lhs);
simplify(goto_trace_step.full_lhs_value, ns);
replace_nondet_in_type(goto_trace_step.full_lhs_value, prop_conv);
replace_nondet_in_type(
goto_trace_step.full_lhs_value, decision_procedure);
}

for(const auto &j : SSA_step.converted_io_args)
Expand All @@ -378,7 +395,7 @@ void build_goto_trace(
}
else
{
exprt tmp = prop_conv.get(j);
exprt tmp = decision_procedure.get(j);
goto_trace_step.io_args.push_back(tmp);
}
}
Expand All @@ -388,7 +405,7 @@ void build_goto_trace(
goto_trace_step.cond_expr = SSA_step.cond_expr;

goto_trace_step.cond_value =
prop_conv.l_get(SSA_step.cond_literal).is_true();
decision_procedure.get(SSA_step.cond_handle).is_true();
}

if(ssa_step_it == last_step_to_keep)
Expand All @@ -400,31 +417,33 @@ void build_goto_trace(
void build_goto_trace(
const symex_target_equationt &target,
symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
const prop_convt &prop_conv,
const decision_proceduret &decision_procedure,
const namespacet &ns,
goto_tracet &goto_trace)
{
const auto is_last_step_to_keep = [last_step_to_keep](
symex_target_equationt::SSA_stepst::const_iterator it, const prop_convt &) {
return last_step_to_keep == it;
};
const auto is_last_step_to_keep =
[last_step_to_keep](
symex_target_equationt::SSA_stepst::const_iterator it,
const decision_proceduret &) { return last_step_to_keep == it; };

return build_goto_trace(
target, is_last_step_to_keep, prop_conv, ns, goto_trace);
target, is_last_step_to_keep, decision_procedure, ns, goto_trace);
}

static bool is_failed_assertion_step(
symex_target_equationt::SSA_stepst::const_iterator step,
const prop_convt &prop_conv)
const decision_proceduret &decision_procedure)
{
return step->is_assert() && prop_conv.l_get(step->cond_literal).is_false();
return step->is_assert() &&
decision_procedure.get(step->cond_handle).is_false();
}

void build_goto_trace(
const symex_target_equationt &target,
const prop_convt &prop_conv,
const decision_proceduret &decision_procedure,
const namespacet &ns,
goto_tracet &goto_trace)
{
build_goto_trace(target, is_failed_assertion_step, prop_conv, ns, goto_trace);
build_goto_trace(
target, is_failed_assertion_step, decision_procedure, ns, goto_trace);
}
Loading