Skip to content

Use numeric_cast<mp_integer> instead of deprecated to_integer(exprt), part 2 #3260

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

Use numeric_cast<mp_integer> instead of deprecated to_integer(exprt), part 2 #3260

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c2380e8
Change utf16_native_endian_to_java to consume char16_t
tautschnig Nov 5, 2018
b541bf9
Use numeric_cast<mp_integer> instead of deprecated to_integer(exprt),…
tautschnig Nov 3, 2018
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
18 changes: 5 additions & 13 deletions jbmc/src/java_bytecode/expr2java.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -191,41 +191,33 @@ std::string expr2javat::convert_constant(
std::string dest;
dest.reserve(char_representation_length);

mp_integer int_value;
if(to_integer(src, int_value))
UNREACHABLE;
const char16_t int_value = numeric_cast_v<char16_t>(src);

Copy link
Collaborator

@kroening kroening Nov 3, 2018

Choose a reason for hiding this comment

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

This is difficult. Java chars are fixed to be 16 bits, by the standard.
wchar_t may be 16 bits, or may be 32 bits, but there isn't an obvious connection to Java's concept of a 'char'.

Copy link
Collaborator

@kroening kroening Nov 3, 2018

Choose a reason for hiding this comment

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

Also, signedness may differ. Java's char is unsigned.

Copy link
Collaborator Author

@tautschnig tautschnig Nov 3, 2018

Choose a reason for hiding this comment

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

Hmm, thanks, I had inferred the type from what utf16_native_endian_to_java takes as parameter. What would be the right type to use here, and where should a possible cast happen?

Copy link
Collaborator

@kroening kroening Nov 3, 2018

Choose a reason for hiding this comment

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

Anything that is guaranteed to hold an unsigned 16-bit values should work -- so how about "char16_t". I would then do an explicit cast to wchar_t when doing the call to utf16_native_endian_to_java. Really utf16_native_endian_to_java should take a char16_t.

Copy link
Contributor

@romainbrenguier romainbrenguier Nov 5, 2018

Choose a reason for hiding this comment

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

Yes char16_t should be used here and in utf16_native_endian_to_java.

// Character literals in Java have type 'char', thus no cast is needed.
// This is different from C, where charater literals have type 'int'.
dest += '\'' + utf16_native_endian_to_java(int_value.to_long()) + '\'';
dest += '\'' + utf16_native_endian_to_java(int_value) + '\'';
return dest;
}
else if(src.type()==java_byte_type())
{
// No byte-literals in Java, so just cast:
mp_integer int_value;
if(to_integer(src, int_value))
UNREACHABLE;
const mp_integer int_value = numeric_cast_v<mp_integer>(src);
std::string dest="(byte)";
dest+=integer2string(int_value);
return dest;
}
else if(src.type()==java_short_type())
{
// No short-literals in Java, so just cast:
mp_integer int_value;
if(to_integer(src, int_value))
UNREACHABLE;
const mp_integer int_value = numeric_cast_v<mp_integer>(src);
std::string dest="(short)";
dest+=integer2string(int_value);
return dest;
}
else if(src.type()==java_long_type())
{
// long integer literals must have 'L' at the end
mp_integer int_value;
if(to_integer(src, int_value))
UNREACHABLE;
const mp_integer int_value = numeric_cast_v<mp_integer>(src);
std::string dest=integer2string(int_value);
dest+='L';
return dest;
Expand Down
47 changes: 11 additions & 36 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -210,12 +210,8 @@ const exprt java_bytecode_convert_methodt::variable(
size_t address,
java_bytecode_convert_methodt::variable_cast_argumentt do_cast)
{
mp_integer number;
bool ret=to_integer(to_constant_expr(arg), number);
CHECK_RETURN(!ret);

std::size_t number_int=integer2size_t(number);
typet t=java_type_from_char(type_char);
const std::size_t number_int = numeric_cast_v<std::size_t>(arg);
variablest &var_list=variables[number_int];

// search variable in list for correct frame / address if necessary
Expand Down Expand Up @@ -1332,19 +1328,15 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
else if(statement=="goto" || statement=="goto_w")
{
PRECONDITION(op.empty() && results.empty());
mp_integer number;
bool ret=to_integer(to_constant_expr(arg0), number);
INVARIANT(!ret, "goto argument should be an integer");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
code_gotot code_goto(label(integer2string(number)));
c=code_goto;
}
else if(statement=="jsr" || statement=="jsr_w")
{
// As 'goto', except we must also push the subroutine return address:
PRECONDITION(op.empty() && results.size() == 1);
mp_integer number;
bool ret=to_integer(to_constant_expr(arg0), number);
INVARIANT(!ret, "jsr argument should be an integer");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
code_gotot code_goto(label(integer2string(number)));
c=code_goto;
results[0]=
Expand Down Expand Up @@ -1386,9 +1378,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
else if(statement==patternt("if_?cmp??"))
{
PRECONDITION(op.size() == 2 && results.empty());
mp_integer number;
bool ret=to_integer(to_constant_expr(arg0), number);
INVARIANT(!ret, "if_?cmp?? argument should be an integer");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
c = convert_if_cmp(
address_map, statement, op, number, i_it->source_location);
}
Expand All @@ -1405,25 +1395,19 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(

INVARIANT(!id.empty(), "unexpected bytecode-if");
PRECONDITION(op.size() == 1 && results.empty());
mp_integer number;
bool ret=to_integer(to_constant_expr(arg0), number);
INVARIANT(!ret, "if?? argument should be an integer");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
c = convert_if(address_map, op, id, number, i_it->source_location);
}
else if(statement==patternt("ifnonnull"))
{
PRECONDITION(op.size() == 1 && results.empty());
mp_integer number;
bool ret=to_integer(to_constant_expr(arg0), number);
INVARIANT(!ret, "ifnonnull argument should be an integer");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
c = convert_ifnonull(address_map, op, number, i_it->source_location);
}
else if(statement==patternt("ifnull"))
{
PRECONDITION(op.size() == 1 && results.empty());
mp_integer number;
bool ret=to_integer(to_constant_expr(arg0), number);
INVARIANT(!ret, "ifnull argument should be an integer");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
c = convert_ifnull(address_map, op, number, i_it->source_location);
}
else if(statement=="iinc")
Expand Down Expand Up @@ -1620,10 +1604,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
{
// The first argument is the type, the second argument is the number of
// dimensions. The size of each dimension is on the stack.
mp_integer number;
bool ret=to_integer(to_constant_expr(arg1), number);
INVARIANT(!ret, "multianewarray argument should be an integer");
std::size_t dimension=integer2size_t(number);
const std::size_t dimension = numeric_cast_v<std::size_t>(arg1);

op=pop(dimension);
assert(results.size()==1);
Expand Down Expand Up @@ -1954,9 +1935,7 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
code_switch_caset code_case;
code_case.add_source_location() = location;

mp_integer number;
bool ret = to_integer(to_constant_expr(*a_it), number);
DATA_INVARIANT(!ret, "case label expected to be integer");
const mp_integer number = numeric_cast_v<mp_integer>(*a_it);
// The switch case does not contain any code, it just branches via a GOTO
// to the jump target of the tableswitch/lookupswitch case at
// hand. Therefore we consider this code to belong to the source bytecode
Expand Down Expand Up @@ -2074,9 +2053,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
ieee_floatt value(spec);
if(arg0.type().id() != ID_floatbv)
{
mp_integer number;
bool ret = to_integer(to_constant_expr(arg0), number);
DATA_INVARIANT(!ret, "failed to convert constant");
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
value.from_integer(number);
}
else
Expand All @@ -2086,9 +2063,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
}
else
{
mp_integer value;
bool ret = to_integer(to_constant_expr(arg0), value);
DATA_INVARIANT(!ret, "failed to convert constant");
const mp_integer value = numeric_cast_v<mp_integer>(arg0);
const typet type = java_type_from_char(statement[0]);
results[0] = from_integer(value, type);
}
Expand Down
4 changes: 1 addition & 3 deletions jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,9 +90,7 @@ refined_string_exprt make_refined_string_exprt(const array_string_exprt &arr)
/// \return the corresponding index set
std::set<exprt> full_index_set(const array_string_exprt &s)
{
PRECONDITION(s.length().is_constant());
mp_integer n;
to_integer(s.length(), n);
const mp_integer n = numeric_cast_v<mp_integer>(s.length());
std::set<exprt> ret;
for(mp_integer i=0; i<n; ++i)
ret.insert(from_integer(i));
Expand Down
8 changes: 2 additions & 6 deletions src/analyses/goto_check.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1110,13 +1110,9 @@ void goto_checkt::bounds_check(
}
else
{
mp_integer i;
const auto i = numeric_cast<mp_integer>(index);

if(!to_integer(index, i) && i>=0)
{
// ok
}
else
if(!i.has_value() || *i < 0)
{
exprt effective_offset=ode.offset();

Expand Down
22 changes: 7 additions & 15 deletions src/analyses/goto_rw.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -181,18 +181,15 @@ void rw_range_sett::get_objects_shift(

range_spect src_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;

mp_integer dist;
if(range_start==-1 ||
size==-1 ||
src_size==-1 ||
to_integer(simp_distance, dist))
const auto dist = numeric_cast<mp_integer>(simp_distance);
if(range_start == -1 || size == -1 || src_size == -1 || !dist.has_value())
{
get_objects_rec(mode, shift.op(), -1, -1);
get_objects_rec(mode, shift.distance(), -1, -1);
}
else
{
range_spect dist_r=to_range_spect(dist);
const range_spect dist_r = to_range_spect(*dist);

// not sure whether to worry about
// config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN
Expand Down Expand Up @@ -284,22 +281,17 @@ void rw_range_sett::get_objects_index(

const exprt simp_index=simplify_expr(expr.index(), ns);

mp_integer index;
if(to_integer(simp_index, index))
{
const auto index = numeric_cast<mp_integer>(simp_index);
if(!index.has_value())
get_objects_rec(get_modet::READ, expr.index());
index=-1;
}

if(range_start==-1 ||
sub_size==-1 ||
index==-1)
if(range_start == -1 || sub_size == -1 || !index.has_value())
get_objects_rec(mode, expr.array(), -1, size);
else
get_objects_rec(
mode,
expr.array(),
range_start+to_range_spect(index*sub_size),
range_start + to_range_spect(*index * sub_size),
size);
}

Expand Down
6 changes: 2 additions & 4 deletions src/analyses/interval_domain.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -254,8 +254,7 @@ void interval_domaint::assume_rec(

if(is_int(lhs.type()) && is_int(rhs.type()))
{
mp_integer tmp;
to_integer(rhs, tmp);
mp_integer tmp = numeric_cast_v<mp_integer>(rhs);
if(id==ID_lt)
--tmp;
integer_intervalt &ii=int_map[lhs_identifier];
Expand All @@ -280,8 +279,7 @@ void interval_domaint::assume_rec(

if(is_int(lhs.type()) && is_int(rhs.type()))
{
mp_integer tmp;
to_integer(lhs, tmp);
mp_integer tmp = numeric_cast_v<mp_integer>(lhs);
if(id==ID_lt)
++tmp;
integer_intervalt &ii=int_map[rhs_identifier];
Expand Down
49 changes: 23 additions & 26 deletions src/analyses/invariant_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -123,10 +123,9 @@ std::string inv_object_storet::build_string(const exprt &expr) const
if(expr.get(ID_value)==ID_NULL)
return "0";

mp_integer i;

if(!to_integer(expr, i))
return integer2string(i);
const auto i = numeric_cast<mp_integer>(expr);
if(i.has_value())
return integer2string(*i);
}

// we also like "address_of" and "reference_to"
Expand Down Expand Up @@ -455,25 +454,24 @@ void invariant_sett::strengthen_rec(const exprt &expr)
get_object(expr.op1(), p.second))
return;

mp_integer i0, i1;
bool have_i0=!to_integer(expr.op0(), i0);
bool have_i1=!to_integer(expr.op1(), i1);
const auto i0 = numeric_cast<mp_integer>(expr.op0());
const auto i1 = numeric_cast<mp_integer>(expr.op1());

if(expr.id()==ID_le)
{
if(have_i0)
add_bounds(p.second, lower_interval(i0));
else if(have_i1)
add_bounds(p.first, upper_interval(i1));
if(i0.has_value())
add_bounds(p.second, lower_interval(*i0));
else if(i1.has_value())
add_bounds(p.first, upper_interval(*i1));
else
add_le(p);
}
else if(expr.id()==ID_lt)
{
if(have_i0)
add_bounds(p.second, lower_interval(i0+1));
else if(have_i1)
add_bounds(p.first, upper_interval(i1-1));
if(i0.has_value())
add_bounds(p.second, lower_interval(*i0 + 1));
else if(i1.has_value())
add_bounds(p.first, upper_interval(*i1 - 1));
else
{
add_le(p);
Expand Down Expand Up @@ -553,12 +551,12 @@ void invariant_sett::strengthen_rec(const exprt &expr)
get_object(expr.op1(), p.second))
return;

mp_integer i;

if(!to_integer(expr.op0(), i))
add_bounds(p.second, boundst(i));
else if(!to_integer(expr.op1(), i))
add_bounds(p.first, boundst(i));
const auto i0 = numeric_cast<mp_integer>(expr.op0());
const auto i1 = numeric_cast<mp_integer>(expr.op1());
if(i0.has_value())
add_bounds(p.second, boundst(*i0));
else if(i1.has_value())
add_bounds(p.first, boundst(*i1));

s=p;
std::swap(s.first, s.second);
Expand Down Expand Up @@ -685,10 +683,10 @@ void invariant_sett::get_bounds(unsigned a, boundst &bounds) const

{
const exprt &e_a=object_store->get_expr(a);
mp_integer tmp;
if(!to_integer(e_a, tmp))
const auto tmp = numeric_cast<mp_integer>(e_a);
if(tmp.has_value())
{
bounds=boundst(tmp);
bounds = boundst(*tmp);
return;
}

Expand Down Expand Up @@ -858,8 +856,7 @@ exprt invariant_sett::get_constant(const exprt &expr) const

if(e.is_constant())
{
mp_integer value;
assert(!to_integer(e, value));
const mp_integer value = numeric_cast_v<mp_integer>(e);

if(expr.type().id()==ID_pointer)
{
Expand Down
4 changes: 1 addition & 3 deletions src/ansi-c/expr2c.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -618,9 +618,7 @@ std::string expr2ct::convert_rec(
{
const vector_typet &vector_type=to_vector_type(src);

mp_integer size_int;
to_integer(vector_type.size(), size_int);

const mp_integer size_int = numeric_cast_v<mp_integer>(vector_type.size());
std::string dest="__gcc_v"+integer2string(size_int);

std::string tmp=convert(vector_type.subtype());
Expand Down
5 changes: 1 addition & 4 deletions src/cpp/cpp_typecheck_initializer.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -225,10 +225,7 @@ void cpp_typecheckt::zero_initializer(
if(size_expr.id()==ID_infinity)
return; // don't initialize

mp_integer size;

bool to_int=to_integer(size_expr, size);
CHECK_RETURN(!to_int);
const mp_integer size = numeric_cast_v<mp_integer>(size_expr);
CHECK_RETURN(size>=0);

exprt::operandst empty_operands;
Expand Down
8 changes: 4 additions & 4 deletions src/goto-programs/goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -203,13 +203,13 @@ std::string trace_numeric_value(
}
else if(type.id()==ID_integer)
{
mp_integer i;
if(!to_integer(expr, i) && i>=0)
const auto i = numeric_cast<mp_integer>(expr);
if(i.has_value() && *i >= 0)
{
if(options.hex_representation)
return "0x" + integer2string(i, 16);
return "0x" + integer2string(*i, 16);
else
return "0b" + integer2string(i, 2);
return "0b" + integer2string(*i, 2);
}
}
Copy link
Collaborator

@kroening kroening Nov 3, 2018

Choose a reason for hiding this comment

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

Triggered #3262, will rebase once this is merged.

}
Expand Down
Loading