Skip to content

flattening/arrays.cpp: replace assert and throw with invariants #1046

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
Jul 13, 2017
Merged

flattening/arrays.cpp: replace assert and throw with invariants #1046

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
119 changes: 78 additions & 41 deletions src/solvers/flattening/arrays.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ Author: Daniel Kroening, [email protected]
\*******************************************************************/


#include <cassert>
#include <iostream>

#include <langapi/language_util.h>
Expand Down Expand Up @@ -50,10 +49,12 @@ literalt arrayst::record_array_equality(
if(!base_type_eq(op0.type(), op1.type(), ns))
{
prop.error() << equality.pretty() << messaget::eom;
throw "record_array_equality got equality without matching types";
DATA_INVARIANT(false, "record_array_equality got equality without matching types");
}

assert(ns.follow(op0.type()).id()==ID_array);
DATA_INVARIANT(
ns.follow(op0.type()).id()==ID_array,
"record_array_equality parameter should be array-typed");
Copy link
Collaborator

Choose a reason for hiding this comment

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

This is a lovely example of how to convert asserts and how to add meaningful information during the conversion.


array_equalities.push_back(array_equalityt());

Expand Down Expand Up @@ -109,14 +110,15 @@ void arrayst::collect_arrays(const exprt &a)

if(a.id()==ID_with)
{
if(a.operands().size()!=3)
throw "with expected to have three operands";
DATA_INVARIANT(
a.operands().size()==3,
"with expected to have three operands");

// check types
if(!base_type_eq(array_type, a.op0().type(), ns))
{
prop.error() << a.pretty() << messaget::eom;
throw "collect_arrays got 'with' without matching types";
DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
}

arrays.make_union(a, a.op0());
Expand All @@ -131,14 +133,15 @@ void arrayst::collect_arrays(const exprt &a)
}
else if(a.id()==ID_update) // TODO: is this obsolete?
{
if(a.operands().size()!=3)
throw "update expected to have three operands";
DATA_INVARIANT(
a.operands().size()==3,
"update expected to have three operands");

// check types
if(!base_type_eq(array_type, a.op0().type(), ns))
{
prop.error() << a.pretty() << messaget::eom;
throw "collect_arrays got 'update' without matching types";
DATA_INVARIANT(false, "collect_arrays got 'update' without matching types");
}

arrays.make_union(a, a.op0());
Expand All @@ -155,21 +158,22 @@ void arrayst::collect_arrays(const exprt &a)
}
else if(a.id()==ID_if)
{
if(a.operands().size()!=3)
throw "if expected to have three operands";
DATA_INVARIANT(
a.operands().size()==3,
"if expected to have three operands");

// check types
if(!base_type_eq(array_type, a.op1().type(), ns))
{
prop.error() << a.pretty() << messaget::eom;
throw "collect_arrays got if without matching types";
DATA_INVARIANT(false, "collect_arrays got if without matching types");
}

// check types
if(!base_type_eq(array_type, a.op2().type(), ns))
{
prop.error() << a.pretty() << messaget::eom;
throw "collect_arrays got if without matching types";
DATA_INVARIANT(false, "collect_arrays got if without matching types");
}

arrays.make_union(a, a.op1());
Expand All @@ -185,9 +189,10 @@ void arrayst::collect_arrays(const exprt &a)
}
else if(a.id()==ID_member)
{
if(to_member_expr(a).struct_op().id()!=ID_symbol)
throw
"unexpected array expression: member with `"+a.op0().id_string()+"'";
DATA_INVARIANT(
to_member_expr(a).struct_op().id()==ID_symbol,
("unexpected array expression: member with `"+
a.op0().id_string()+"'").c_str());
Copy link
Collaborator

Choose a reason for hiding this comment

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

[Not an issue for this PR, my problem not yours] This looks a little clunky. Do you think we could improve invariant.h to de-clunky this?

Copy link
Contributor Author

@smowton smowton Jun 21, 2017 •
edited
Loading

Choose a reason for hiding this comment

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

It would also be good to make this lazy for cases like this which build an error string. How about something like:

#define INVARIANT(CONDITION, REASON) \
  do { \
    if(!(CONDITION)) \
    { \
      std::string reason = (REASON); \
      invariant_failed(__FILE__, __FUNCTION__, __LINE__, reason.c_str()); \
    } \
  } while(0);

Copy link
Contributor Author

Choose a reason for hiding this comment

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

(If invariant_failed (currently check_invariant) throws then it should take a std::string not a const char* otherwise the c_str() will outlive the string it's taken from)

Copy link
Contributor

Choose a reason for hiding this comment

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

I think that looks good. It also gives the option to use an immediately-evaluated lambda as the REASON parameter, in the case that ostringstream is required to build the message string.

As you said, depending on the implementation of invariant_failed it might be better to do

std::string reason = (REASON); \
invariant_failed(__FILE__, __FUNCTION__, __LINE__, std::move(reason)); \

}
else if(a.id()==ID_constant ||
a.id()==ID_array ||
Expand All @@ -200,20 +205,24 @@ void arrayst::collect_arrays(const exprt &a)
else if(a.id()==ID_byte_update_little_endian ||
a.id()==ID_byte_update_big_endian)
{
assert(0);
DATA_INVARIANT(
false,
"byte_update should be removed before collect_arrays");
Copy link
Collaborator

Choose a reason for hiding this comment

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

Perfect -- this is exactly why these should be converted manually.

}
else if(a.id()==ID_typecast)
{
// cast between array types?
assert(a.operands().size()==1);
DATA_INVARIANT(
a.operands().size()==1,
"typecast must have one operand");

if(a.op0().type().id()==ID_array)
{
arrays.make_union(a, a.op0());
collect_arrays(a.op0());
}
else
throw "unexpected array type cast from "+a.op0().type().id_string();
DATA_INVARIANT(
a.op0().type().id()==ID_array,
("unexpected array type cast from "+
a.op0().type().id_string()).c_str());

arrays.make_union(a, a.op0());
collect_arrays(a.op0());
}
else if(a.id()==ID_index)
{
Expand All @@ -222,7 +231,12 @@ void arrayst::collect_arrays(const exprt &a)
collect_arrays(a.op0());
}
else
throw "unexpected array expression (collect_arrays): `"+a.id_string()+"'";
{
DATA_INVARIANT(
false,
("unexpected array expression (collect_arrays): `"+
a.id_string()+"'").c_str());
}
}

/// adds array constraints (refine=true...lazily for the refinement loop)
Expand Down Expand Up @@ -364,7 +378,7 @@ void arrayst::update_index_map(std::size_t i)
return;

std::size_t root_number=arrays.find_number(i);
assert(root_number!=i);
INVARIANT(root_number!=i, "is_root_number incorrect?");

index_sett &root_index_set=index_map[root_number];
index_sett &index_set=index_map[i];
Expand Down Expand Up @@ -435,7 +449,9 @@ void arrayst::add_array_constraints(
index_expr2.array()=array_equality.f2;
index_expr2.index()=*it;

assert(index_expr1.type()==index_expr2.type());
DATA_INVARIANT(
index_expr1.type()==index_expr2.type(),
"array elements should all have same type");

array_equalityt equal;
equal.f1 = index_expr1;
Expand Down Expand Up @@ -477,12 +493,14 @@ void arrayst::add_array_constraints(
else if(expr.id()==ID_byte_update_little_endian ||
expr.id()==ID_byte_update_big_endian)
{
assert(0);
INVARIANT(false, "byte_update should be removed before arrayst");
}
else if(expr.id()==ID_typecast)
{
// we got a=(type[])b
assert(expr.operands().size()==1);
DATA_INVARIANT(
expr.operands().size()==1,
"typecast should have one operand");

// add a[i]=b[i]
for(index_sett::const_iterator
Expand All @@ -500,7 +518,9 @@ void arrayst::add_array_constraints(
index_expr2.array()=expr.op0();
index_expr2.index()=*it;

assert(index_expr1.type()==index_expr2.type());
DATA_INVARIANT(
index_expr1.type()==index_expr2.type(),
"array elements should all have same type");

// add constraint
lazy_constraintt lazy(lazy_typet::ARRAY_TYPECAST,
Expand All @@ -512,9 +532,12 @@ void arrayst::add_array_constraints(
{
}
else
throw
"unexpected array expression (add_array_constraints): `"+
expr.id_string()+"'";
{
DATA_INVARIANT(
false,
("unexpected array expression (add_array_constraints): `"+
expr.id_string()+"'").c_str());
}
}

void arrayst::add_array_constraints_with(
Expand All @@ -536,7 +559,9 @@ void arrayst::add_array_constraints_with(
if(index_expr.type()!=value.type())
{
prop.error() << expr.pretty() << messaget::eom;
throw "index_expr and value types should match";
DATA_INVARIANT(
false,
"with-expression operand should match array element type");
}

lazy_constraintt lazy(
Expand Down Expand Up @@ -575,7 +600,9 @@ void arrayst::add_array_constraints_with(
index_expr2.array()=expr.op0();
index_expr2.index()=other_index;

assert(index_expr1.type()==index_expr2.type());
DATA_INVARIANT(
index_expr1.type()==index_expr2.type(),
"array elements should all have same type");

equal_exprt equality_expr(index_expr1, index_expr2);

Expand Down Expand Up @@ -620,7 +647,9 @@ void arrayst::add_array_constraints_update(
if(index_expr.type()!=value.type())
{
prop.error() << expr.pretty() << messaget::eom;
throw "index_expr and value types should match";
DATA_INVARIANT(
false,
"update operand should match array element type");
}

set_to_true(equal_exprt(index_expr, value));
Expand Down Expand Up @@ -657,7 +686,9 @@ void arrayst::add_array_constraints_update(
index_expr2.array()=expr.op0();
index_expr2.index()=other_index;

assert(index_expr1.type()==index_expr2.type());
DATA_INVARIANT(
index_expr1.type()==index_expr2.type(),
"array elements should all have same type");

equal_exprt equality_expr(index_expr1, index_expr2);

Expand Down Expand Up @@ -693,7 +724,9 @@ void arrayst::add_array_constraints_array_of(
index_expr.array()=expr;
index_expr.index()=*it;

assert(base_type_eq(index_expr.type(), expr.op0().type(), ns));
DATA_INVARIANT(
base_type_eq(index_expr.type(), expr.op0().type(), ns),
"array_of operand type should match array element type");

// add constraint
lazy_constraintt lazy(
Expand Down Expand Up @@ -730,7 +763,9 @@ void arrayst::add_array_constraints_if(
index_expr2.array()=expr.true_case();
index_expr2.index()=*it;

assert(index_expr1.type()==index_expr2.type());
DATA_INVARIANT(
index_expr1.type()==index_expr2.type(),
"array elements should all have same type");

// add implication
lazy_constraintt lazy(lazy_typet::ARRAY_IF,
Expand Down Expand Up @@ -759,7 +794,9 @@ void arrayst::add_array_constraints_if(
index_expr2.array()=expr.false_case();
index_expr2.index()=*it;

assert(index_expr1.type()==index_expr2.type());
DATA_INVARIANT(
index_expr1.type()==index_expr2.type(),
"array elements should all have same type");

// add implication
lazy_constraintt lazy(
Expand Down