diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 6fe8532ba6d..63da1ef5251 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -591,7 +591,8 @@ void ansi_c_convert_typet::write(typet &type) if(vector_size.is_not_nil()) { - vector_typet new_type(type, vector_size); + type_with_subtypet new_type(ID_frontend_vector, type); + new_type.set(ID_size, vector_size); new_type.add_source_location()=vector_size.source_location(); type=new_type; } diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 18e7c109d13..a8c1ff8ecd8 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -213,7 +213,7 @@ class c_typecheck_baset: virtual void typecheck_c_bit_field_type(c_bit_field_typet &type); virtual void typecheck_typeof_type(typet &type); virtual void typecheck_array_type(array_typet &type); - virtual void typecheck_vector_type(vector_typet &type); + virtual void typecheck_vector_type(typet &type); virtual void typecheck_custom_type(typet &type); virtual void adjust_function_parameter(typet &type) const; virtual bool is_complete_type(const typet &type) const; diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 69e52348450..901c592819c 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -99,7 +99,13 @@ void c_typecheck_baset::typecheck_type(typet &type) // nothing to do, these stay as is } else if(type.id()==ID_vector) - typecheck_vector_type(to_vector_type(type)); + { + // already done + } + else if(type.id() == ID_frontend_vector) + { + typecheck_vector_type(type); + } else if(type.id()==ID_custom_unsignedbv || type.id()==ID_custom_signedbv || type.id()==ID_custom_floatbv || @@ -655,14 +661,17 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) } } -void c_typecheck_baset::typecheck_vector_type(vector_typet &type) +void c_typecheck_baset::typecheck_vector_type(typet &type) { - exprt &size=type.size(); - source_locationt source_location=size.find_source_location(); + // This turns the type with ID_frontend_vector into the type + // with ID_vector; the difference is that the latter has + // a constant as size, which we establish now. + exprt size = static_cast(type.find(ID_size)); + const source_locationt source_location = size.find_source_location(); typecheck_expr(size); - typet &subtype=type.subtype(); + typet subtype = type.subtype(); typecheck_type(subtype); // we are willing to combine 'vector' with various @@ -699,25 +708,24 @@ void c_typecheck_baset::typecheck_vector_type(vector_typet &type) } // the subtype must have constant size - exprt size_expr=size_of_expr(type.subtype(), *this); + exprt sub_size_expr = size_of_expr(subtype, *this); - simplify(size_expr, *this); + simplify(sub_size_expr, *this); - const auto sub_size = numeric_cast(size_expr); + const auto sub_size = numeric_cast(sub_size_expr); if(!sub_size.has_value()) { error().source_location=source_location; error() << "failed to determine size of vector base type `" - << to_string(type.subtype()) << "'" << eom; + << to_string(subtype) << "'" << eom; throw 0; } if(*sub_size == 0) { error().source_location=source_location; - error() << "type had size 0: `" - << to_string(type.subtype()) << "'" << eom; + error() << "type had size 0: `" << to_string(subtype) << "'" << eom; throw 0; } @@ -733,7 +741,11 @@ void c_typecheck_baset::typecheck_vector_type(vector_typet &type) s /= *sub_size; - type.size()=from_integer(s, signed_size_type()); + // produce the type with ID_vector + vector_typet new_type(subtype, from_integer(s, signed_size_type())); + new_type.add_source_location() = source_location; + new_type.size().add_source_location() = source_location; + type = new_type; } void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp index b92c9108a03..61b9fb34987 100644 --- a/src/cpp/cpp_typecheck_type.cpp +++ b/src/cpp/cpp_typecheck_type.cpp @@ -142,7 +142,11 @@ void cpp_typecheckt::typecheck_type(typet &type) } else if(type.id()==ID_vector) { - typecheck_vector_type(to_vector_type(type)); + // already done + } + else if(type.id() == ID_frontend_vector) + { + typecheck_vector_type(type); } else if(type.id()==ID_code) { diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index b5c763d18e3..36157bef491 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -2206,7 +2206,8 @@ bool Parser::rAttribute(typet &t) if(lex.get_token(tk3)!=')') return false; - vector_typet attr(uninitialized_typet{}, exp); + type_with_subtypet attr(ID_frontend_vector, uninitialized_typet{}); + attr.set(ID_size, exp); attr.add_source_location()=exp.source_location(); merge_types(attr, t); break; diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 141c6dde995..22427af79ad 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -470,6 +470,7 @@ IREP_ID_ONE(transparent_union) IREP_ID_TWO(C_transparent_union, #transparent_union) IREP_ID_ONE(aligned) IREP_ID_TWO(C_alignment, #alignment) +IREP_ID_ONE(frontend_vector) IREP_ID_ONE(vector) IREP_ID_ONE(abstract) IREP_ID_ONE(function_application) diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index 77cc1f73a4a..19b2f49dc7e 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -283,3 +283,19 @@ bool is_constant_or_has_constant_components( return false; } + +vector_typet::vector_typet(const typet &_subtype, const constant_exprt &_size) + : type_with_subtypet(ID_vector, _subtype) +{ + size() = _size; +} + +const constant_exprt &vector_typet::size() const +{ + return static_cast(find(ID_size)); +} + +constant_exprt &vector_typet::size() +{ + return static_cast(add(ID_size)); +} diff --git a/src/util/std_types.h b/src/util/std_types.h index 2a5e16a14ed..5e2bdfdaf9e 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -1751,28 +1751,18 @@ inline range_typet &to_range_type(typet &type) /// Used to represent the short vectors used by CPU instruction sets such as /// MMX, SSE and AVX. They all provide registers that are something like /// 8 x int32, for example, and corresponding operations that operate -/// element-wise on their operand vectors. Compared to \ref array_typet -/// that has no element-wise operators. Note that `remove_vector.h` removes -/// this data type by compilation into arrays. +/// element-wise on their operand vectors. Compared to \ref array_typet, +/// vector_typet has a fixed size whereas array_typet has no element-wise +/// operators. +/// Note that `remove_vector.h` removes this data type by compilation into +/// arrays. class vector_typet:public type_with_subtypet { public: - vector_typet( - const typet &_subtype, - const exprt &_size):type_with_subtypet(ID_vector, _subtype) - { - size()=_size; - } + vector_typet(const typet &_subtype, const constant_exprt &_size); - const exprt &size() const - { - return static_cast(find(ID_size)); - } - - exprt &size() - { - return static_cast(add(ID_size)); - } + const constant_exprt &size() const; + constant_exprt &size(); }; /// Check whether a reference to a typet is a \ref vector_typet. diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp index dfb93ca081b..7f690b46685 100644 --- a/unit/solvers/lowering/byte_operators.cpp +++ b/unit/solvers/lowering/byte_operators.cpp @@ -68,7 +68,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") unsignedbv_typet u32(32); unsignedbv_typet u64(64); - exprt size = from_integer(8, size_type()); + constant_exprt size = from_integer(8, size_type()); std::vector types = { struct_typet({{"comp1", u32}, {"comp2", u64}}), @@ -211,7 +211,7 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]") unsignedbv_typet u32(32); unsignedbv_typet u64(64); - exprt size = from_integer(8, size_type()); + constant_exprt size = from_integer(8, size_type()); std::vector types = { // TODO: only arrays and scalars