Skip to content

Only convert not-yet-converted SSA steps #4065

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 1 commit into from
Feb 7, 2019
Merged

Only convert not-yet-converted SSA steps #4065

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
68 changes: 38 additions & 30 deletions src/goto-symex/symex_target_equation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -351,11 +351,11 @@ void symex_target_equationt::convert(
}

void symex_target_equationt::convert_assignments(
decision_proceduret &decision_procedure) const
decision_proceduret &decision_procedure)
{
for(const auto &step : SSA_steps)
for(auto &step : SSA_steps)
{
if(step.is_assignment() && !step.ignore)
if(step.is_assignment() && !step.ignore && !step.converted)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Instead of adding this info to every step, would it be more efficient to store a conversion frontier as a single iterator member? The current implementation increases the storage size of each SSA_stept and requires repeated traversal of steps have have been seen before. With an optionalt<SSA_stepst::const_iterator> we would just store a pointer to the last converted step.

Copy link
Member Author

Choose a reason for hiding this comment

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

There is no conversion frontier due to slicing.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Ah, of course.

{
decision_procedure.conditional_output(
decision_procedure.debug(),
Expand All @@ -365,22 +365,23 @@ void symex_target_equationt::convert_assignments(
});

decision_procedure.set_to_true(step.cond_expr);
step.converted = true;
}
}
}

void symex_target_equationt::convert_decls(
prop_convt &prop_conv) const
void symex_target_equationt::convert_decls(prop_convt &prop_conv)
{
for(const auto &step : SSA_steps)
for(auto &step : SSA_steps)
{
if(step.is_decl() && !step.ignore)
if(step.is_decl() && !step.ignore && !step.converted)
{
// The result is not used, these have no impact on
// the satisfiability of the formula.
try
{
prop_conv.convert(step.cond_expr);
step.converted = true;
}
catch(const bitvector_conversion_exceptiont &)
{
Expand Down Expand Up @@ -489,31 +490,27 @@ void symex_target_equationt::convert_goto_instructions(
}

void symex_target_equationt::convert_constraints(
decision_proceduret &decision_procedure) const
decision_proceduret &decision_procedure)
{
for(const auto &step : SSA_steps)
for(auto &step : SSA_steps)
{
if(step.is_constraint())
if(step.is_constraint() && !step.ignore && !step.converted)
{
if(!step.ignore)
{
decision_procedure.conditional_output(
decision_procedure.debug(),
[&step](messaget::mstreamt &mstream) {
step.output(mstream);
mstream << messaget::eom;
});
decision_procedure.conditional_output(
decision_procedure.debug(), [&step](messaget::mstreamt &mstream) {
step.output(mstream);
mstream << messaget::eom;
});

try
{
decision_procedure.set_to_true(step.cond_expr);
}
catch(const bitvector_conversion_exceptiont &)
{
util_throw_with_nested(
equation_conversion_exceptiont(
"Error converting constraints for step", step));
}
try
{
decision_procedure.set_to_true(step.cond_expr);
step.converted = true;
}
catch(const bitvector_conversion_exceptiont &)
{
util_throw_with_nested(equation_conversion_exceptiont(
"Error converting constraints for step", step));
}
}
}
Expand All @@ -534,8 +531,13 @@ void symex_target_equationt::convert_assertions(
{
for(auto &step : SSA_steps)
{
if(step.is_assert())
// ignore already converted assertions in the error trace
if(step.is_assert() && step.converted)
step.ignore = true;

if(step.is_assert() && !step.ignore && !step.converted)
{
step.converted = true;
prop_conv.set_to_false(step.cond_expr);
step.cond_literal=const_literal(false);
return; // prevent further assumptions!
Expand All @@ -556,8 +558,14 @@ void symex_target_equationt::convert_assertions(

for(auto &step : SSA_steps)
{
if(step.is_assert())
// ignore already converted assertions in the error trace
if(step.is_assert() && step.converted)
step.ignore = true;

if(step.is_assert() && !step.ignore && !step.converted)
{
step.converted = true;

prop_conv.conditional_output(
prop_conv.debug(),
[&step](messaget::mstreamt &mstream) {
Expand Down
11 changes: 7 additions & 4 deletions src/goto-symex/symex_target_equation.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,12 +171,12 @@ class symex_target_equationt:public symex_targett
/// Converts assignments: set the equality _lhs==rhs_ to _True_.
/// \param decision_procedure: A handle to a particular decision procedure
/// interface
void convert_assignments(decision_proceduret &decision_procedure) const;
void convert_assignments(decision_proceduret &decision_procedure);

/// Converts declarations: these are effectively ignored by the decision
/// procedure.
/// \param prop_conv: A handle to a particular decision procedure interface
void convert_decls(prop_convt &prop_conv) const;
void convert_decls(prop_convt &prop_conv);

/// Converts assumptions: convert the expression the assumption represents.
/// \param prop_conv: A handle to a particular decision procedure interface
Expand All @@ -189,7 +189,7 @@ class symex_target_equationt:public symex_targett
/// Converts constraints: set the represented condition to _True_.
/// \param decision_procedure: A handle to a particular decision procedure
/// interface
void convert_constraints(decision_proceduret &decision_procedure) const;
void convert_constraints(decision_proceduret &decision_procedure);

/// Converts goto instructions: convert the expression representing the
/// condition of this goto.
Expand Down Expand Up @@ -321,6 +321,9 @@ class symex_target_equationt:public symex_targett
// for slicing
bool ignore=false;

// for incremental conversion
bool converted = false;

SSA_stept(const sourcet &_source, goto_trace_stept::typet _type)
: source(_source),
type(_type),
Expand Down Expand Up @@ -354,7 +357,7 @@ class symex_target_equationt:public symex_targett
{
return narrow_cast<std::size_t>(std::count_if(
SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
return step.is_assert();
return step.is_assert() && !step.ignore && !step.converted;
}));
}

Expand Down