Skip to content

Commit 06b377d

Browse files
kroeningkroening
authored
Merge pull request #7143 from diffblue/vector_index_type
add index type to the C vector type
2 parents bc1012b + 3034749 commit 06b377d

File tree

6 files changed

+72
-39
lines changed

6 files changed

+72
-39
lines changed

‎src/ansi-c/c_expr.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,10 @@ shuffle_vector_exprt::shuffle_vector_exprt(
2323
op1() = std::move(*vector2);
2424

2525
const vector_typet &vt = to_vector_type(op0().type());
26-
type() = vector_typet{vt.element_type(),
27-
from_integer(indices.size(), vt.size().type())};
26+
type() = vector_typet{
27+
vt.index_type(),
28+
vt.element_type(),
29+
from_integer(indices.size(), vt.size().type())};
2830

2931
op2().operands().swap(indices);
3032
}

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1442,8 +1442,10 @@ void c_typecheck_baset::typecheck_expr_rel_vector(binary_exprt &expr)
14421442
// with the same dimension.
14431443
auto subtype_width =
14441444
to_bitvector_type(to_vector_type(o_type0).element_type()).get_width();
1445-
expr.type() =
1446-
vector_typet{signedbv_typet{subtype_width}, to_vector_type(o_type0).size()};
1445+
expr.type() = vector_typet{
1446+
to_vector_type(o_type0).index_type(),
1447+
signedbv_typet{subtype_width},
1448+
to_vector_type(o_type0).size()};
14471449

14481450
// Replace the id as the semantics of these are point-wise application (and
14491451
// the result is not of bool type).

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 26 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -219,24 +219,28 @@ void c_typecheck_baset::typecheck_type(typet &type)
219219
else if(gcc_attr_mode == "__V2SI__") // vector of 2 ints, deprecated
220220
{
221221
if(is_signed)
222-
result=vector_typet(
223-
signed_int_type(),
224-
from_integer(2, size_type()));
222+
{
223+
result = vector_typet(
224+
c_index_type(), signed_int_type(), from_integer(2, size_type()));
225+
}
225226
else
226-
result=vector_typet(
227-
unsigned_int_type(),
228-
from_integer(2, size_type()));
227+
{
228+
result = vector_typet(
229+
c_index_type(), unsigned_int_type(), from_integer(2, size_type()));
230+
}
229231
}
230232
else if(gcc_attr_mode == "__V4SI__") // vector of 4 ints, deprecated
231233
{
232234
if(is_signed)
233-
result=vector_typet(
234-
signed_int_type(),
235-
from_integer(4, size_type()));
235+
{
236+
result = vector_typet(
237+
c_index_type(), signed_int_type(), from_integer(4, size_type()));
238+
}
236239
else
237-
result=vector_typet(
238-
unsigned_int_type(),
239-
from_integer(4, size_type()));
240+
{
241+
result = vector_typet(
242+
c_index_type(), unsigned_int_type(), from_integer(4, size_type()));
243+
}
240244
}
241245
else // give up, just use subtype
242246
result = to_type_with_subtype(type).subtype();
@@ -266,13 +270,17 @@ void c_typecheck_baset::typecheck_type(typet &type)
266270
else if(gcc_attr_mode == "__TF__") // 128 bits
267271
result=gcc_float128_type();
268272
else if(gcc_attr_mode == "__V2SF__") // deprecated vector of 2 floats
269-
result=vector_typet(float_type(), from_integer(2, size_type()));
273+
result = vector_typet(
274+
c_index_type(), float_type(), from_integer(2, size_type()));
270275
else if(gcc_attr_mode == "__V2DF__") // deprecated vector of 2 doubles
271-
result=vector_typet(double_type(), from_integer(2, size_type()));
276+
result = vector_typet(
277+
c_index_type(), double_type(), from_integer(2, size_type()));
272278
else if(gcc_attr_mode == "__V4SF__") // deprecated vector of 4 floats
273-
result=vector_typet(float_type(), from_integer(4, size_type()));
279+
result = vector_typet(
280+
c_index_type(), float_type(), from_integer(4, size_type()));
274281
else if(gcc_attr_mode == "__V4DF__") // deprecated vector of 4 doubles
275-
result=vector_typet(double_type(), from_integer(4, size_type()));
282+
result = vector_typet(
283+
c_index_type(), double_type(), from_integer(4, size_type()));
276284
else // give up, just use subtype
277285
result = to_type_with_subtype(type).subtype();
278286

@@ -745,7 +753,8 @@ void c_typecheck_baset::typecheck_vector_type(typet &type)
745753
s /= *sub_size;
746754

747755
// produce the type with ID_vector
748-
vector_typet new_type(subtype, from_integer(s, signed_size_type()));
756+
vector_typet new_type(
757+
c_index_type(), subtype, from_integer(s, signed_size_type()));
749758
new_type.add_source_location() = source_location;
750759
new_type.size().add_source_location() = source_location;
751760
type = new_type;

‎src/util/std_types.cpp

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -244,16 +244,26 @@ bool is_constant_or_has_constant_components(
244244
return false;
245245
}
246246

247-
vector_typet::vector_typet(const typet &_subtype, const constant_exprt &_size)
248-
: type_with_subtypet(ID_vector, _subtype)
247+
vector_typet::vector_typet(
248+
typet _index_type,
249+
typet _element_type,
250+
constant_exprt _size)
251+
: type_with_subtypet(ID_vector, std::move(_element_type))
249252
{
250-
size() = _size;
253+
index_type_nonconst() = std::move(_index_type);
254+
size() = std::move(_size);
251255
}
252256

253257
typet vector_typet::index_type() const
254258
{
255-
// we may wish to make the index type part of the vector type
256-
return c_index_type();
259+
// For backwards compatibility, allow the case that the array type is
260+
// not annotated with an index type.
261+
const auto &annotated_type =
262+
static_cast<const typet &>(find(ID_C_index_type));
263+
if(annotated_type.is_nil())
264+
return c_index_type();
265+
else
266+
return annotated_type;
257267
}
258268

259269
const constant_exprt &vector_typet::size() const

‎src/util/std_types.h

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1007,11 +1007,19 @@ inline range_typet &to_range_type(typet &type)
10071007
class vector_typet:public type_with_subtypet
10081008
{
10091009
public:
1010-
vector_typet(const typet &_subtype, const constant_exprt &_size);
1010+
vector_typet(typet index_type, typet element_type, constant_exprt size);
10111011

10121012
/// The type of any index expression into an instance of this type.
10131013
typet index_type() const;
10141014

1015+
/// The type of any index expression into an instance of this type.
1016+
/// This is added as a comment now for backwards compatibility, but will
1017+
/// eventually be the first subtype.
1018+
typet &index_type_nonconst()
1019+
{
1020+
return static_cast<typet &>(add(ID_C_index_type));
1021+
}
1022+
10151023
/// The type of the elements of the vector.
10161024
/// This method is preferred over .subtype(),
10171025
/// which will eventually be deprecated.

‎unit/solvers/lowering/byte_operators.cpp

Lines changed: 14 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -255,10 +255,11 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
255255
std::vector<typet> types = {
256256
struct_typet({{"comp1", u16}, {"comp2", u16}}),
257257
struct_typet({{"comp1", u32}, {"comp2", u64}}),
258-
struct_typet({{"comp1", u32},
259-
{"compX", c_bit_field_typet(u8, 4)},
260-
{"pad", c_bit_field_typet(u8, 4)},
261-
{"comp2", u8}}),
258+
struct_typet(
259+
{{"comp1", u32},
260+
{"compX", c_bit_field_typet(u8, 4)},
261+
{"pad", c_bit_field_typet(u8, 4)},
262+
{"comp2", u8}}),
262263
union_typet({{"compA", u32}, {"compB", u64}}),
263264
c_enum_typet(u16),
264265
c_enum_typet(unsignedbv_typet(128)),
@@ -272,8 +273,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
272273
ieee_float_spect::single_precision().to_type(),
273274
// generates the correct value, but remains wrapped in a typecast
274275
// pointer_typet(u64, 64),
275-
vector_typet(u8, size),
276-
vector_typet(u64, size),
276+
vector_typet(size_type(), u8, size),
277+
vector_typet(size_type(), u64, size),
277278
complex_typet(s16),
278279
complex_typet(u64)};
279280

@@ -405,10 +406,11 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
405406
std::vector<typet> types = {
406407
struct_typet({{"comp1", u16}, {"comp2", u16}}),
407408
struct_typet({{"comp1", u32}, {"comp2", u64}}),
408-
struct_typet({{"comp1", u32},
409-
{"compX", c_bit_field_typet(u8, 4)},
410-
{"pad", c_bit_field_typet(u8, 4)},
411-
{"comp2", u8}}),
409+
struct_typet(
410+
{{"comp1", u32},
411+
{"compX", c_bit_field_typet(u8, 4)},
412+
{"pad", c_bit_field_typet(u8, 4)},
413+
{"comp2", u8}}),
412414
union_typet({{"compA", u32}, {"compB", u64}}),
413415
c_enum_typet(u16),
414416
c_enum_typet(unsignedbv_typet(128)),
@@ -422,8 +424,8 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
422424
ieee_float_spect::single_precision().to_type(),
423425
// generates the correct value, but remains wrapped in a typecast
424426
// pointer_typet(u64, 64),
425-
vector_typet(u8, size),
426-
vector_typet(u64, size),
427+
vector_typet(size_type(), u8, size),
428+
vector_typet(size_type(), u64, size),
427429
// complex_typet(s16),
428430
// complex_typet(u64)
429431
};

0 commit comments

Comments
 (0)