diff --git a/regression/ansi-c/gcc_neon_vector_type_zero/main.c b/regression/ansi-c/gcc_neon_vector_type_zero/main.c new file mode 100644 index 00000000000..18a2e7ebe37 --- /dev/null +++ b/regression/ansi-c/gcc_neon_vector_type_zero/main.c @@ -0,0 +1,10 @@ +// neon_vector_type gives a lane count, which must be positive; a lane count of +// 0 must be rejected by the existing positivity check. +typedef __attribute__((neon_vector_type(0))) int bad_vector; + +int main() +{ + bad_vector v; + (void)v; + return 0; +} diff --git a/regression/ansi-c/gcc_neon_vector_type_zero/test.desc b/regression/ansi-c/gcc_neon_vector_type_zero/test.desc new file mode 100644 index 00000000000..35cc46138d2 --- /dev/null +++ b/regression/ansi-c/gcc_neon_vector_type_zero/test.desc @@ -0,0 +1,12 @@ +CORE gcc-only +main.c + +^EXIT=1$ +^SIGNAL=0$ +error: vector size must be positive, but got 0$ +^CONVERSION ERROR$ +-- +^warning: ignoring +^VERIFICATION +-- +A neon_vector_type lane count of 0 must be rejected by the positivity check. diff --git a/regression/ansi-c/gcc_vector_size_not_multiple/main.c b/regression/ansi-c/gcc_vector_size_not_multiple/main.c new file mode 100644 index 00000000000..f5a4b3904fd --- /dev/null +++ b/regression/ansi-c/gcc_vector_size_not_multiple/main.c @@ -0,0 +1,12 @@ +// Unlike neon_vector_type (a lane count), vector_size gives the size in bytes, +// which must be a multiple of the base type size. 3 is not a multiple of +// sizeof(int), so this must be rejected -- guarding the byte-size code path +// that the neon_vector_type lane-count handling shares. +typedef __attribute__((vector_size(3))) int bad_vector; + +int main() +{ + bad_vector v; + (void)v; + return 0; +} diff --git a/regression/ansi-c/gcc_vector_size_not_multiple/test.desc b/regression/ansi-c/gcc_vector_size_not_multiple/test.desc new file mode 100644 index 00000000000..56547818ed9 --- /dev/null +++ b/regression/ansi-c/gcc_vector_size_not_multiple/test.desc @@ -0,0 +1,13 @@ +CORE gcc-only +main.c + +^EXIT=1$ +^SIGNAL=0$ +error: vector size \(3\) expected to be multiple of base type size \(4\)$ +^CONVERSION ERROR$ +-- +^warning: ignoring +^VERIFICATION +-- +vector_size in bytes must be a multiple of the base type size; this guards the +byte-size branch shared with the neon_vector_type lane-count handling. diff --git a/regression/cbmc/gcc_neon_vector_type/main.c b/regression/cbmc/gcc_neon_vector_type/main.c new file mode 100644 index 00000000000..94fd65955c9 --- /dev/null +++ b/regression/cbmc/gcc_neon_vector_type/main.c @@ -0,0 +1,24 @@ +// The neon_vector_type attribute (used by Clang's ) gives the +// vector size as a lane count rather than in bytes, unlike vector_size. +typedef __attribute__((neon_vector_type(16))) signed char int8x16_t; +typedef __attribute__((neon_vector_type(8))) short int16x8_t; +typedef __attribute__((neon_vector_type(4))) int int32x4_t; +typedef __attribute__((neon_vector_type(2))) double float64x2_t; +// A non-power-of-two lane count whose byte interpretation differs: 3 lanes of +// int is 12 bytes, whereas a byte size of 3 would be rejected as not a +// multiple of sizeof(int). +typedef __attribute__((neon_vector_type(3))) int int32x3_t; + +int main() +{ + int8x16_t a = {0}; + a[3] = 7; + __CPROVER_assert(a[3] == 7, "lane indexing works"); + __CPROVER_assert(sizeof(int8x16_t) == 16, "16 lanes of signed char"); + __CPROVER_assert(sizeof(int16x8_t) == 16, "8 lanes of short"); + __CPROVER_assert(sizeof(int32x4_t) == 16, "4 lanes of int"); + __CPROVER_assert(sizeof(float64x2_t) == 16, "2 lanes of double"); + __CPROVER_assert( + sizeof(int32x3_t) == 12, "3 lanes of int (lanes, not bytes)"); + return 0; +} diff --git a/regression/cbmc/gcc_neon_vector_type/test.desc b/regression/cbmc/gcc_neon_vector_type/test.desc new file mode 100644 index 00000000000..75cc69573e8 --- /dev/null +++ b/regression/cbmc/gcc_neon_vector_type/test.desc @@ -0,0 +1,9 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index c7ed6453c90..c7461738202 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -196,6 +196,8 @@ void ansi_c_convert_typet::read_rec(const typet &type) { // note that this is not yet a vector_typet -- this is a size only vector_size = static_cast(type.find(ID_size)); + // neon_vector_type gives the size as a lane count rather than in bytes + vector_size_is_lanes = type.get_bool(ID_C_vector_size_is_lanes); } else if(type.id()==ID_void) { @@ -659,6 +661,8 @@ void ansi_c_convert_typet::build_type_with_subtype(typet &type) const { type_with_subtypet new_type(ID_frontend_vector, type); new_type.set(ID_size, vector_size); + if(vector_size_is_lanes) + new_type.set(ID_C_vector_size_is_lanes, true); new_type.add_source_location()=vector_size.source_location(); type=new_type; } diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h index 043198d8fb5..04a3686ec2a 100644 --- a/src/ansi-c/ansi_c_convert_type.h +++ b/src/ansi-c/ansi_c_convert_type.h @@ -40,7 +40,7 @@ class ansi_c_convert_typet typet gcc_attribute_mode; - bool packed, aligned; + bool packed, aligned, vector_size_is_lanes; exprt vector_size, alignment, bv_width, fraction_width; exprt msc_based; // this is Visual Studio bool constructor, destructor; @@ -106,6 +106,7 @@ class ansi_c_convert_typet gcc_attribute_mode(static_cast(get_nil_irep())), packed(false), aligned(false), + vector_size_is_lanes(false), vector_size(nil_exprt{}), alignment(nil_exprt{}), bv_width(nil_exprt{}), diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 2362e3966f6..4627e3c2997 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -708,6 +708,10 @@ void c_typecheck_baset::typecheck_vector_type(typet &type) exprt size = static_cast(type.find(ID_size)); const source_locationt source_location = size.find_source_location(); + // neon_vector_type gives the size as a lane count, whereas vector_size (and + // hence the default below) gives it in bytes. + const bool size_is_lane_count = type.get_bool(ID_C_vector_size_is_lanes); + typecheck_expr(size); typet subtype = to_type_with_subtype(type).subtype(); @@ -770,14 +774,17 @@ void c_typecheck_baset::typecheck_vector_type(typet &type) } // adjust by width of base type - if(s % *sub_size != 0) + if(!size_is_lane_count) { - throw errort().with_location(source_location) - << "vector size (" << s << ") expected to be multiple of base type size (" - << *sub_size << ")"; - } + if(s % *sub_size != 0) + { + throw errort().with_location(source_location) + << "vector size (" << s + << ") expected to be multiple of base type size (" << *sub_size << ")"; + } - s /= *sub_size; + s /= *sub_size; + } // produce the type with ID_vector vector_typet new_type( diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 91526b2b8e6..1b084931dc6 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -168,6 +168,7 @@ int yyansi_cerror(const std::string &error); %token TOK_GCC_ATTRIBUTE_TRANSPARENT_UNION "transparent_union" %token TOK_GCC_ATTRIBUTE_PACKED "packed" %token TOK_GCC_ATTRIBUTE_VECTOR_SIZE "vector_size" +%token TOK_GCC_ATTRIBUTE_NEON_VECTOR_TYPE "neon_vector_type" %token TOK_GCC_ATTRIBUTE_MODE "mode" %token TOK_GCC_ATTRIBUTE_GNU_INLINE "__gnu_inline__" %token TOK_GCC_ATTRIBUTE_WEAK "weak" @@ -1681,6 +1682,8 @@ gcc_type_attribute: { $$=$1; set($$, ID_transparent_union); } | TOK_GCC_ATTRIBUTE_VECTOR_SIZE '(' comma_expression ')' { $$=$1; set($$, ID_frontend_vector); parser_stack($$).add(ID_size)=parser_stack($3); } + | TOK_GCC_ATTRIBUTE_NEON_VECTOR_TYPE '(' comma_expression ')' + { $$=$1; set($$, ID_frontend_vector); parser_stack($$).add(ID_size)=parser_stack($3); parser_stack($$).set(ID_C_vector_size_is_lanes, true); } | TOK_GCC_ATTRIBUTE_ALIGNED { $$=$1; set($$, ID_aligned); } | TOK_GCC_ATTRIBUTE_ALIGNED '(' comma_expression ')' diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index f9c7b8674ce..aa8d4f95e45 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1672,6 +1672,9 @@ enable_or_disable ("enable"|"disable") "vector_size" | "__vector_size__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_VECTOR_SIZE; } +"neon_vector_type" | +"__neon_vector_type__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_NEON_VECTOR_TYPE; } + "mode" | "__mode__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_MODE; } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 8f1cfe001ab..4c46b775df6 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -370,6 +370,7 @@ IREP_ID_ONE(designator) IREP_ID_ONE(member_designator) IREP_ID_ONE(index_designator) IREP_ID_TWO(C_constant, #constant) +IREP_ID_TWO(C_vector_size_is_lanes, #vector_size_is_lanes) IREP_ID_TWO(C_volatile, #volatile) IREP_ID_TWO(C_restricted, #restricted) IREP_ID_TWO(C_identifier, #identifier)