Skip to content

Fix crash with exceptions and --string-refine #1190

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 2 commits into from
Aug 3, 2017
Merged

Fix crash with exceptions and --string-refine #1190

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c1f4db1
Refactoring in string_refinementt::set_to()
Aug 1, 2017
6ec155b
Call supert::set_to on non-symbol lhs
Aug 1, 2017
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
89 changes: 40 additions & 49 deletions src/solvers/refinement/string_refinement.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -415,52 +415,50 @@ void string_refinementt::concretize_lengths()
/// \par parameters: an expression and the value to set it to
void string_refinementt::set_to(const exprt &expr, bool value)
{
INVARIANT(
equality_propagation,
string_refinement_invariantt("set_to should only be called when equality "
"propagation is enabled"));
PRECONDITION(expr.type().id()==ID_bool);
PRECONDITION(equality_propagation);

if(expr.id()==ID_equal)
{
equal_exprt eq_expr=to_equal_expr(expr);
const exprt &lhs=eq_expr.lhs();
const exprt &rhs=eq_expr.rhs();

// The assignment of a string equality to false is not supported.
PRECONDITION(value || !is_char_array(rhs.type()));
PRECONDITION(value ||
!refined_string_typet::is_refined_string_type(rhs.type()));

PRECONDITION(lhs.id()==ID_symbol || !is_char_array(rhs.type()));
PRECONDITION(lhs.id()==ID_symbol ||
!refined_string_typet::is_refined_string_type(rhs.type()));

if(eq_expr.lhs().type()!=eq_expr.rhs().type())
// If lhs is not a symbol, let supert::set_to() handle it.
if(lhs.id()!=ID_symbol)
{
warning() << "ignoring " << from_expr(ns, "", expr)
<< " [inconsistent types]" << eom;
debug() << "lhs has type: " << eq_expr.lhs().type().pretty(12) << eom;
debug() << "rhs has type: " << eq_expr.rhs().type().pretty(12) << eom;
non_string_axioms.push_back(std::make_pair(expr, value));
return;
}

if(expr.type().id()!=ID_bool)
if(lhs.type()!=rhs.type())
{
error() << "string_refinementt::set_to got non-boolean operand: "
<< expr.pretty() << eom;
INVARIANT(
false,
string_refinement_invariantt("set_to should only be called with exprs "
"of type bool"));
warning() << "ignoring " << from_expr(ns, "", expr)
<< " [inconsistent types]" << eom;
debug() << "lhs has type: " << lhs.type().pretty(12) << eom;
debug() << "rhs has type: " << rhs.type().pretty(12) << eom;
return;
Copy link
Contributor

Choose a reason for hiding this comment

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

Similarly, this is clearly a bit odd, but why not let the superclass handle it or complain on its own?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes, probably. I now call supert::set_to(). I left the warning though, as the superclass seems to be less verbose.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Actually the string solver is not robust enough to call the superclass, as incompatible types do happen here and then (e.g. #1105 introduces such errors) and the superclass makes cbmc crash. These issues need to be fixed one by one but I can't call the superclass yet. So I reverted to the previous version.

Copy link
Contributor

Choose a reason for hiding this comment

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

In that case there is a problem with #1105 generating inconsistent equations, can you create an issue for that?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Issue diffblue/test-gen#1202 has been created.
@smowton is that all good for you?

Copy link
Contributor

Choose a reason for hiding this comment

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

sure, sounds reasonable

Copy link
Contributor Author

Choose a reason for hiding this comment

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

@smowton could you approve then? Otherwise I can promise a very complicated badminton game! ;-)

}

// Preprocessing to remove function applications.
const exprt &lhs=eq_expr.lhs();
debug() << "(sr::set_to) " << from_expr(ns, "", lhs)
<< " = " << from_expr(ns, "", eq_expr.rhs()) << eom;

// TODO: See if this happens at all.
if(lhs.id()!=ID_symbol)
{
warning() << "ignoring " << from_expr(ns, "", expr) << eom;
return;
}
<< " = " << from_expr(ns, "", rhs) << eom;

exprt subst_rhs=substitute_function_applications(eq_expr.rhs());
if(eq_expr.lhs().type()!=subst_rhs.type())
const exprt subst_rhs=substitute_function_applications(rhs);
if(lhs.type()!=subst_rhs.type())
{
if(eq_expr.lhs().type().id() != ID_array ||
subst_rhs.type().id() != ID_array ||
eq_expr.lhs().type().subtype() != subst_rhs.type().subtype())
if(lhs.type().id()!=ID_array ||
subst_rhs.type().id()!=ID_array ||
lhs.type().subtype()!=subst_rhs.type().subtype())
{
warning() << "ignoring " << from_expr(ns, "", expr)
<< " [inconsistent types after substitution]" << eom;
Expand All @@ -473,29 +471,22 @@ void string_refinementt::set_to(const exprt &expr, bool value)
}
}

if(value)
{
if(!add_axioms_for_string_assigns(lhs, subst_rhs))
return;
}
else
{
// TODO: Something should also be done if value is false.
INVARIANT(
!is_char_array(eq_expr.rhs().type()),
string_refinement_invariantt("set_to cannot set a char_array"));
INVARIANT(
!refined_string_typet::is_refined_string_type(eq_expr.rhs().type()),
string_refinement_invariantt("set_to cannot set a refined_string"));
}
if(value && !add_axioms_for_string_assigns(lhs, subst_rhs))
return;

non_string_axioms.push_back(std::make_pair(equal_exprt(lhs, subst_rhs),
value));
// Push the substituted equality to the list of axioms to be given to
// supert::set_to.
non_string_axioms.push_back(
std::make_pair(equal_exprt(lhs, subst_rhs), value));
}
// We keep a list of the axioms to give to supert::set_to in order to
// substitute the symbols in dec_solve().
// Push the unmodified equality to the list of axioms to be given to
// supert::set_to.
else
{
// TODO: Verify that the expression contains no string.
// This will be easy once exprt iterators will have been implemented.
non_string_axioms.push_back(std::make_pair(expr, value));
}
}

/// use a refinement loop to instantiate universal axioms, call the sat solver,
Expand Down