Skip to content

Commit c09c50d

Browse files
tautschnigtautschnig
authored
Merge pull request #3882 from tautschnig/deprecation-to_integer2
Use numeric_cast<mp_integer> instead of deprecated to_integer variants [blocks: #3800]
2 parents 3a8b34d + cf1f65a commit c09c50d

22 files changed

+247
-237
lines changed

‎regression/cbmc-library/memmove-01/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,5 +47,11 @@ int main(int argc, char *argv[])
4747
printf("%d %d %d %d %d %d %d\n", a[0], a[1], a[2], a[3], a[4], a[5], a[6]);
4848

4949
assert(a[0] == -2147483600);
50+
assert(a[1] == -2147221455);
51+
assert(a[2] == -2147221455);
52+
assert(a[3] == -2147221455);
53+
assert(a[4] == 16);
54+
assert(a[5] == 256);
55+
assert(a[6] == 16384);
5056
return 0;
5157
}

‎regression/cbmc-library/memmove-01/test.desc

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,13 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--unwind 17
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
77
--
88
^warning: ignoring
9+
--
10+
Since we cannot constant-propagate lsize, we generate byte_extract operations
11+
over an int-array of unknown size when invoking memmove. This could be fixed by
12+
not using array_copy/array_replace in memmove, extensions to the byte-operator
13+
lowering, or field-sensitive SSA (this regression test is fully deterministic).

‎src/analyses/goto_rw.cpp

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -150,22 +150,21 @@ void rw_range_sett::get_objects_byte_extract(
150150
{
151151
const exprt simp_offset=simplify_expr(be.offset(), ns);
152152

153-
mp_integer index;
154-
if(range_start==-1 || to_integer(simp_offset, index))
153+
auto index = numeric_cast<mp_integer>(simp_offset);
154+
if(range_start == -1 || !index.has_value())
155155
get_objects_rec(mode, be.op(), -1, size);
156156
else
157157
{
158-
index*=8;
159-
if(index>=pointer_offset_bits(be.op().type(), ns))
158+
*index *= 8;
159+
if(*index >= *pointer_offset_bits(be.op().type(), ns))
160160
return;
161161

162162
endianness_mapt map(
163163
be.op().type(),
164164
be.id()==ID_byte_extract_little_endian,
165165
ns);
166-
assert(index<std::numeric_limits<size_t>::max());
167166
range_spect offset =
168-
range_start + map.map_bit(numeric_cast_v<std::size_t>(index));
167+
range_start + map.map_bit(numeric_cast_v<std::size_t>(*index));
169168
get_objects_rec(mode, be.op(), offset, size);
170169
}
171170
}

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2899,12 +2899,13 @@ bool c_typecheck_baset::gcc_vector_types_compatible(
28992899
// This is relatively restrictive!
29002900

29012901
// compare dimension
2902-
mp_integer s0, s1;
2903-
if(to_integer(type0.size(), s0))
2902+
const auto s0 = numeric_cast<mp_integer>(type0.size());
2903+
const auto s1 = numeric_cast<mp_integer>(type1.size());
2904+
if(!s0.has_value())
29042905
return false;
2905-
if(to_integer(type1.size(), s1))
2906+
if(!s1.has_value())
29062907
return false;
2907-
if(s0!=s1)
2908+
if(*s0 != *s1)
29082909
return false;
29092910

29102911
// compare subtype

‎src/ansi-c/c_typecheck_initializer.cpp

Lines changed: 27 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -91,29 +91,30 @@ exprt c_typecheck_baset::do_initializer_rec(
9191
to_array_type(full_type).is_complete())
9292
{
9393
// check size
94-
mp_integer array_size;
95-
if(to_integer(to_array_type(full_type).size(), array_size))
94+
const auto array_size =
95+
numeric_cast<mp_integer>(to_array_type(full_type).size());
96+
if(!array_size.has_value())
9697
{
9798
error().source_location = value.source_location();
9899
error() << "array size needs to be constant, got "
99100
<< to_string(to_array_type(full_type).size()) << eom;
100101
throw 0;
101102
}
102103

103-
if(array_size<0)
104+
if(*array_size < 0)
104105
{
105106
error().source_location = value.source_location();
106107
error() << "array size must not be negative" << eom;
107108
throw 0;
108109
}
109110

110-
if(mp_integer(tmp.operands().size())>array_size)
111+
if(mp_integer(tmp.operands().size()) > *array_size)
111112
{
112113
// cut off long strings. gcc does a warning for this
113-
tmp.operands().resize(numeric_cast_v<std::size_t>(array_size));
114+
tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size));
114115
tmp.type()=type;
115116
}
116-
else if(mp_integer(tmp.operands().size())<array_size)
117+
else if(mp_integer(tmp.operands().size()) < *array_size)
117118
{
118119
// fill up
119120
tmp.type()=type;
@@ -126,7 +127,7 @@ exprt c_typecheck_baset::do_initializer_rec(
126127
<< to_string(full_type.subtype()) << "'" << eom;
127128
throw 0;
128129
}
129-
tmp.operands().resize(numeric_cast_v<std::size_t>(array_size), *zero);
130+
tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
130131
}
131132
}
132133

@@ -152,29 +153,30 @@ exprt c_typecheck_baset::do_initializer_rec(
152153
to_array_type(full_type).is_complete())
153154
{
154155
// check size
155-
mp_integer array_size;
156-
if(to_integer(to_array_type(full_type).size(), array_size))
156+
const auto array_size =
157+
numeric_cast<mp_integer>(to_array_type(full_type).size());
158+
if(!array_size.has_value())
157159
{
158160
error().source_location = value.source_location();
159161
error() << "array size needs to be constant, got "
160162
<< to_string(to_array_type(full_type).size()) << eom;
161163
throw 0;
162164
}
163165

164-
if(array_size<0)
166+
if(*array_size < 0)
165167
{
166168
error().source_location = value.source_location();
167169
error() << "array size must not be negative" << eom;
168170
throw 0;
169171
}
170172

171-
if(mp_integer(tmp2.operands().size())>array_size)
173+
if(mp_integer(tmp2.operands().size()) > *array_size)
172174
{
173175
// cut off long strings. gcc does a warning for this
174-
tmp2.operands().resize(numeric_cast_v<std::size_t>(array_size));
176+
tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size));
175177
tmp2.type()=type;
176178
}
177-
else if(mp_integer(tmp2.operands().size())<array_size)
179+
else if(mp_integer(tmp2.operands().size()) < *array_size)
178180
{
179181
// fill up
180182
tmp2.type()=type;
@@ -187,7 +189,7 @@ exprt c_typecheck_baset::do_initializer_rec(
187189
<< to_string(full_type.subtype()) << "'" << eom;
188190
throw 0;
189191
}
190-
tmp2.operands().resize(numeric_cast_v<std::size_t>(array_size), *zero);
192+
tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
191193
}
192194
}
193195

@@ -319,35 +321,34 @@ void c_typecheck_baset::designator_enter(
319321
}
320322
else
321323
{
322-
mp_integer array_size;
323-
324-
if(to_integer(array_type.size(), array_size))
324+
const auto array_size = numeric_cast<mp_integer>(array_type.size());
325+
if(!array_size.has_value())
325326
{
326327
error().source_location = array_type.size().source_location();
327328
error() << "array has non-constant size `"
328329
<< to_string(array_type.size()) << "'" << eom;
329330
throw 0;
330331
}
331332

332-
entry.size = numeric_cast_v<std::size_t>(array_size);
333+
entry.size = numeric_cast_v<std::size_t>(*array_size);
333334
entry.subtype=array_type.subtype();
334335
}
335336
}
336337
else if(full_type.id()==ID_vector)
337338
{
338339
const vector_typet &vector_type=to_vector_type(full_type);
339340

340-
mp_integer vector_size;
341+
const auto vector_size = numeric_cast<mp_integer>(vector_type.size());
341342

342-
if(to_integer(vector_type.size(), vector_size))
343+
if(!vector_size.has_value())
343344
{
344345
error().source_location = vector_type.size().source_location();
345346
error() << "vector has non-constant size `"
346347
<< to_string(vector_type.size()) << "'" << eom;
347348
throw 0;
348349
}
349350

350-
entry.size = numeric_cast_v<std::size_t>(vector_size);
351+
entry.size = numeric_cast_v<std::size_t>(*vector_size);
351352
entry.subtype=vector_type.subtype();
352353
}
353354
else
@@ -735,7 +736,11 @@ designatort c_typecheck_baset::make_designator(
735736

736737
if(to_array_type(full_type).size().is_nil())
737738
size=0;
738-
else if(to_integer(to_array_type(full_type).size(), size))
739+
else if(
740+
const auto size_opt =
741+
numeric_cast<mp_integer>(to_array_type(full_type).size()))
742+
size = *size_opt;
743+
else
739744
{
740745
error().source_location = d_op.op0().source_location();
741746
error() << "expected constant array size" << eom;

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -703,17 +703,17 @@ void c_typecheck_baset::typecheck_vector_type(vector_typet &type)
703703

704704
simplify(size_expr, *this);
705705

706-
mp_integer sub_size;
706+
const auto sub_size = numeric_cast<mp_integer>(size_expr);
707707

708-
if(to_integer(size_expr, sub_size))
708+
if(!sub_size.has_value())
709709
{
710710
error().source_location=source_location;
711711
error() << "failed to determine size of vector base type `"
712712
<< to_string(type.subtype()) << "'" << eom;
713713
throw 0;
714714
}
715715

716-
if(sub_size==0)
716+
if(*sub_size == 0)
717717
{
718718
error().source_location=source_location;
719719
error() << "type had size 0: `"
@@ -722,16 +722,16 @@ void c_typecheck_baset::typecheck_vector_type(vector_typet &type)
722722
}
723723

724724
// adjust by width of base type
725-
if(s%sub_size!=0)
725+
if(s % *sub_size != 0)
726726
{
727727
error().source_location=source_location;
728728
error() << "vector size (" << s
729-
<< ") expected to be multiple of base type size (" << sub_size
729+
<< ") expected to be multiple of base type size (" << *sub_size
730730
<< ")" << eom;
731731
throw 0;
732732
}
733733

734-
s/=sub_size;
734+
s /= *sub_size;
735735

736736
type.size()=from_integer(s, signed_size_type());
737737
}

‎src/cpp/cpp_typecheck_initializer.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -270,12 +270,12 @@ void cpp_typecheckt::zero_initializer(
270270

271271
exprt component_size=size_of_expr(component.type(), *this);
272272

273-
mp_integer size_int;
274-
if(!to_integer(component_size, size_int))
273+
const auto size_int = numeric_cast<mp_integer>(component_size);
274+
if(size_int.has_value())
275275
{
276-
if(size_int>max_comp_size)
276+
if(*size_int > max_comp_size)
277277
{
278-
max_comp_size=size_int;
278+
max_comp_size = *size_int;
279279
comp=component;
280280
}
281281
}

‎src/cpp/cpp_typecheck_resolve.cpp

Lines changed: 14 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -696,16 +696,16 @@ exprt cpp_typecheck_resolvet::do_builtin(
696696

697697
resolve_argument(argument, fargs);
698698

699-
mp_integer i;
700-
if(to_integer(argument, i))
699+
const auto i = numeric_cast<mp_integer>(argument);
700+
if(!i.has_value())
701701
{
702702
cpp_typecheck.error().source_location=source_location;
703703
cpp_typecheck.error() << "template argument must be constant"
704704
<< messaget::eom;
705705
throw 0;
706706
}
707707

708-
if(i<1)
708+
if(*i < 1)
709709
{
710710
cpp_typecheck.error().source_location=source_location;
711711
cpp_typecheck.error()
@@ -715,7 +715,7 @@ exprt cpp_typecheck_resolvet::do_builtin(
715715
}
716716

717717
dest=type_exprt(typet(base_name));
718-
dest.type().set(ID_width, integer2string(i));
718+
dest.type().set(ID_width, integer2string(*i));
719719
}
720720
else if(base_name==ID_fixedbv)
721721
{
@@ -751,25 +751,27 @@ exprt cpp_typecheck_resolvet::do_builtin(
751751
throw 0;
752752
}
753753

754-
mp_integer width, integer_bits;
754+
const auto width = numeric_cast<mp_integer>(argument0);
755755

756-
if(to_integer(argument0, width))
756+
if(!width.has_value())
757757
{
758758
cpp_typecheck.error().source_location=argument0.find_source_location();
759759
cpp_typecheck.error() << "template argument must be constant"
760760
<< messaget::eom;
761761
throw 0;
762762
}
763763

764-
if(to_integer(argument1, integer_bits))
764+
const auto integer_bits = numeric_cast<mp_integer>(argument1);
765+
766+
if(!integer_bits.has_value())
765767
{
766768
cpp_typecheck.error().source_location=argument1.find_source_location();
767769
cpp_typecheck.error() << "template argument must be constant"
768770
<< messaget::eom;
769771
throw 0;
770772
}
771773

772-
if(width<1)
774+
if(*width < 1)
773775
{
774776
cpp_typecheck.error().source_location=argument0.find_source_location();
775777
cpp_typecheck.error()
@@ -778,7 +780,7 @@ exprt cpp_typecheck_resolvet::do_builtin(
778780
throw 0;
779781
}
780782

781-
if(integer_bits<0)
783+
if(*integer_bits < 0)
782784
{
783785
cpp_typecheck.error().source_location=argument1.find_source_location();
784786
cpp_typecheck.error()
@@ -787,7 +789,7 @@ exprt cpp_typecheck_resolvet::do_builtin(
787789
throw 0;
788790
}
789791

790-
if(integer_bits>width)
792+
if(*integer_bits > *width)
791793
{
792794
cpp_typecheck.error().source_location=argument1.find_source_location();
793795
cpp_typecheck.error()
@@ -797,8 +799,8 @@ exprt cpp_typecheck_resolvet::do_builtin(
797799
}
798800

799801
dest=type_exprt(typet(base_name));
800-
dest.type().set(ID_width, integer2string(width));
801-
dest.type().set(ID_integer_bits, integer2string(integer_bits));
802+
dest.type().set(ID_width, integer2string(*width));
803+
dest.type().set(ID_integer_bits, integer2string(*integer_bits));
802804
}
803805
else if(base_name==ID_integer)
804806
{

0 commit comments

Comments
 (0)