ansi-c: support the neon_vector_type attribute

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;
+}

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.

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;
+}

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.

regression/cbmc/gcc_neon_vector_type/main.c

@@ -0,0 +1,23 @@
+// The neon_vector_type attribute (used by Clang's <arm_neon.h>) 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;
+}

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$

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<const constant_exprt &>(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;
   }

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<const typet &>(get_nil_irep())),
       packed(false),
       aligned(false),
+      vector_size_is_lanes(false),
       vector_size(nil_exprt{}),
       alignment(nil_exprt{}),
       bv_width(nil_exprt{}),

src/ansi-c/c_typecheck_type.cpp

@@ -708,6 +708,10 @@ void c_typecheck_baset::typecheck_vector_type(typet &type)
   exprt size = static_cast<const exprt &>(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(

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 ')'

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; }
 

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)