Skip to content

Use numeric_cast<mp_integer> instead of deprecated to_integer(exprt) #3252

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
Nov 3, 2018
Merged

Use numeric_cast<mp_integer> instead of deprecated to_integer(exprt) #3252

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
26 changes: 14 additions & 12 deletions src/ansi-c/padding.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,12 +35,15 @@ mp_integer alignment(const typet &type, const namespacet &ns)
const exprt &given_alignment=
static_cast<const exprt &>(type.find(ID_C_alignment));

mp_integer a_int;
mp_integer a_int = 0;

// we trust it blindly, no matter how nonsensical
if(given_alignment.is_nil() ||
to_integer(given_alignment, a_int))
a_int=0;
if(given_alignment.is_not_nil())
{
const auto a = numeric_cast<mp_integer>(given_alignment);
if(a.has_value())
a_int = *a;
}

// alignment but no packing
if(a_int>0 && !type.get_bool(ID_C_packed))
Expand Down Expand Up @@ -402,17 +405,16 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
}

// any explicit alignment for the struct?
if(type.find(ID_C_alignment).is_not_nil())
const exprt &alignment =
static_cast<const exprt &>(type.find(ID_C_alignment));
if(alignment.is_not_nil())
{
const exprt &alignment=
static_cast<const exprt &>(type.find(ID_C_alignment));
if(alignment.id()!=ID_default)
{
exprt tmp=alignment;
simplify(tmp, ns);
mp_integer tmp_i;
if(!to_integer(tmp, tmp_i) && tmp_i>max_alignment)
max_alignment=tmp_i;
const auto tmp_i = numeric_cast<mp_integer>(simplify_expr(alignment, ns));

if(tmp_i.has_value() && *tmp_i > max_alignment)
max_alignment = *tmp_i;
}
}
// Is the struct packed, without any alignment specification?
Expand Down
19 changes: 12 additions & 7 deletions src/ansi-c/type2name.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -178,14 +178,19 @@ static std::string type2name(
}
else if(type.id()==ID_array)
{
const array_typet &t=to_array_type(type);
mp_integer size;
if(t.size().id()==ID_symbol)
result += "ARR" + id2string(to_symbol_expr(t.size()).get_identifier());
else if(to_integer(t.size(), size))
result+="ARR?";
const exprt &size = to_array_type(type).size();

if(size.id() == ID_symbol)
result += "ARR" + id2string(to_symbol_expr(size).get_identifier());
else
result+="ARR"+integer2string(size);
{
const auto size_int = numeric_cast<mp_integer>(size);

if(!size_int.has_value())
result += "ARR?";
else
result += "ARR" + integer2string(*size_int);
}
}
else if(
type.id() == ID_symbol_type || type.id() == ID_c_enum_tag ||
Expand Down
10 changes: 4 additions & 6 deletions src/cpp/cpp_typecheck_constructor.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -395,13 +395,11 @@ void cpp_typecheckt::default_assignop_value(
continue;
}

mp_integer size;
bool to_int=to_integer(size_expr, size);
CHECK_RETURN(!to_int);
CHECK_RETURN(size>=0);
const auto size = numeric_cast<mp_integer>(size_expr);
CHECK_RETURN(!size.has_value());
CHECK_RETURN(*size >= 0);

exprt::operandst empty_operands;
for(mp_integer i=0; i < size; ++i)
for(mp_integer i = 0; i < *size; ++i)
copy_array(source_location, mem_name, i, arg_name, block);
}
else
Expand Down
6 changes: 5 additions & 1 deletion src/goto-symex/build_goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,11 @@ void build_goto_trace(
exprt clock_value=prop_conv.get(
symbol_exprt(partial_order_concurrencyt::rw_clock_id(it)));

to_integer(clock_value, current_time);
const auto cv = numeric_cast<mp_integer>(clock_value);
if(cv.has_value())
current_time = *cv;
else
current_time = 0;
}
else if(it->is_atomic_end() && current_time<0)
current_time*=-1;
Expand Down
8 changes: 4 additions & 4 deletions src/solvers/flattening/boolbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -323,17 +323,17 @@ bvt boolbvt::convert_lambda(const exprt &expr)
const exprt &array_size=
to_array_type(expr.type()).size();

mp_integer size;
const auto size = numeric_cast<mp_integer>(array_size);

if(to_integer(array_size, size))
if(!size.has_value())
return conversion_failed(expr);

typet counter_type=expr.op0().type();

bvt bv;
bv.resize(width);

for(mp_integer i=0; i<size; ++i)
for(mp_integer i = 0; i < *size; ++i)
{
exprt counter=from_integer(i, counter_type);

Expand All @@ -343,7 +343,7 @@ bvt boolbvt::convert_lambda(const exprt &expr)
const bvt &tmp=convert_bv(expr_op1);

INVARIANT(
size * tmp.size() == width,
*size * tmp.size() == width,
"total bitvector width shall equal the number of operands times the size "
"per operand");

Expand Down
6 changes: 3 additions & 3 deletions src/solvers/flattening/boolbv_byte_update.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,11 +38,11 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)

// see if the byte number is constant

mp_integer index;
if(!to_integer(offset_expr, index))
const auto index = numeric_cast<mp_integer>(offset_expr);
if(index.has_value())
{
// yes!
mp_integer offset=index*8;
const mp_integer offset = *index * 8;

if(offset+update_width>mp_integer(bv.size()) || offset<0)
{
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_extractbit.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
if(index_as_integer < 0 || index_as_integer >= src_bv.size())
return prop.new_variable(); // out of range!
else
return src_bv[integer2size_t(index_as_integer)];
return src_bv[numeric_cast_v<std::size_t>(index_as_integer)];
}

if(
Expand Down
24 changes: 8 additions & 16 deletions src/solvers/flattening/boolbv_width.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,16 +128,16 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
const array_typet &array_type=to_array_type(type);
std::size_t sub_width=operator()(array_type.subtype());

mp_integer array_size;
const auto array_size = numeric_cast<mp_integer>(array_type.size());

if(to_integer(array_type.size(), array_size))
if(!array_size.has_value())
{
// we can still use the theory of arrays for this
entry.total_width=0;
}
else
{
mp_integer total=array_size*sub_width;
mp_integer total = *array_size * sub_width;
if(total>(1<<30)) // realistic limit
throw analysis_exceptiont("array too large for flattening");

Expand All @@ -149,21 +149,13 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
const vector_typet &vector_type=to_vector_type(type);
std::size_t sub_width=operator()(vector_type.subtype());

mp_integer vector_size;
const auto vector_size = numeric_cast_v<mp_integer>(vector_type.size());

if(to_integer(vector_type.size(), vector_size))
{
// we can still use the theory of arrays for this
entry.total_width=0;
}
else
{
mp_integer total=vector_size*sub_width;
if(total>(1<<30)) // realistic limit
analysis_exceptiont("vector too large for flattening");
mp_integer total = vector_size * sub_width;
if(total > (1 << 30)) // realistic limit
analysis_exceptiont("vector too large for flattening");

entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
}
entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
}
else if(type_id==ID_complex)
{
Expand Down
8 changes: 4 additions & 4 deletions src/solvers/flattening/boolbv_with.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,9 +125,9 @@ void boolbvt::convert_with_array(

const exprt &array_size=type.size();

mp_integer size;
const auto size = numeric_cast<mp_integer>(array_size);

if(to_integer(array_size, size))
if(!size.has_value())
{
error().source_location=type.source_location();
error() << "convert_with_array expects constant array size" << eom;
Expand All @@ -136,7 +136,7 @@ void boolbvt::convert_with_array(

const bvt &op2_bv=convert_bv(op2);

if(size*op2_bv.size()!=prev_bv.size())
if(*size * op2_bv.size() != prev_bv.size())
{
error().source_location=type.source_location();
error() << "convert_with_array: unexpected operand 2 width" << eom;
Expand All @@ -150,7 +150,7 @@ void boolbvt::convert_with_array(
// Yes, it is!
next_bv=prev_bv;

if(op1_value>=0 && op1_value<size) // bounds check
if(op1_value >= 0 && op1_value < *size) // bounds check
{
const std::size_t offset =
numeric_cast_v<std::size_t>(op1_value * op2_bv.size());
Expand Down
14 changes: 6 additions & 8 deletions src/util/endianness_map.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,25 +92,23 @@ void endianness_mapt::build_big_endian(const typet &src)
const array_typet &array_type=to_array_type(src);

// array size constant?
mp_integer s;
if(!to_integer(array_type.size(), s))
auto s = numeric_cast<mp_integer>(array_type.size());
if(s.has_value())
{
while(s>0)
while(*s > 0)
{
build_big_endian(array_type.subtype());
--s;
--(*s);
}
}
}
else if(src.id()==ID_vector)
{
const vector_typet &vector_type=to_vector_type(src);

mp_integer s;
if(to_integer(vector_type.size(), s))
CHECK_RETURN(false);
mp_integer s = numeric_cast_v<mp_integer>(vector_type.size());

while(s>0)
while(s > 0)
{
build_big_endian(vector_type.subtype());
--s;
Expand Down
23 changes: 8 additions & 15 deletions src/util/expr_initializer.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,8 +136,6 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
if(tmpval.is_nil())
return nil_exprt();

mp_integer array_size;

if(array_type.size().id()==ID_infinity)
{
if(nondet)
Expand All @@ -147,19 +145,21 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
value.add_source_location()=source_location;
return std::move(value);
}
else if(to_integer(array_type.size(), array_size))

const auto array_size = numeric_cast<mp_integer>(array_type.size());
if(!array_size.has_value())
{
if(nondet)
return side_effect_expr_nondett(type, source_location);
else
return nil_exprt();
}

if(array_size < 0)
if(*array_size < 0)
return nil_exprt();

array_exprt value(array_type);
value.operands().resize(integer2size_t(array_size), tmpval);
value.operands().resize(numeric_cast_v<std::size_t>(*array_size), tmpval);
value.add_source_location()=source_location;
return std::move(value);
}
Expand All @@ -172,21 +172,14 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
if(tmpval.is_nil())
return nil_exprt();

mp_integer vector_size;

if(to_integer(vector_type.size(), vector_size))
{
if(nondet)
return side_effect_expr_nondett(type, source_location);
else
return nil_exprt();
}
const mp_integer vector_size =
numeric_cast_v<mp_integer>(vector_type.size());

Copy link
Member

Choose a reason for hiding this comment

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

This is a change in behavior -- intended?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yes, my apologies for not noting that in the commit message (which I have now done). In several places we had already treated vectors having constant size as an invariant. This should add consistency.

if(vector_size < 0)
return nil_exprt();

vector_exprt value(vector_type);
value.operands().resize(integer2size_t(vector_size), tmpval);
value.operands().resize(numeric_cast_v<std::size_t>(vector_size), tmpval);
value.add_source_location()=source_location;

return std::move(value);
Expand Down
Loading