add index type to the array type

This commit addresses a gap between the arrays of the C programming language
and standard array theories.  In C, array indices are subject to arithmetic
promotion, and thus, may have a variety of types, depending on the operand
type.  Standard array theories expect one specific index type per array
type.

The C front-end now annotates the array type with that index type.  We will
eventually enforce that all index expressions use this type.

Author: kroening

src/ansi-c/c_typecheck_type.cpp

@@ -524,21 +524,18 @@ void c_typecheck_baset::typecheck_code_type(code_typet &type)
 
 void c_typecheck_baset::typecheck_array_type(array_typet &type)
 {
-  exprt &size=type.size();
-  const source_locationt size_source_location = size.find_source_location();
-
-  // check subtype
+  // Typecheck the element type.
   typecheck_type(type.element_type());
 
-  // we don't allow void as subtype
+  // We don't allow void as the element type.
   if(type.element_type().id() == ID_empty)
   {
     error().source_location=type.source_location();
     error() << "array of voids" << eom;
     throw 0;
   }
 
-  // we don't allow incomplete structs or unions as subtype
+  // We don't allow incomplete structs or unions as element type.
   const typet &followed_subtype = follow(type.element_type());
 
   if(
@@ -551,7 +548,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
     throw 0;
   }
 
-  // we don't allow functions as subtype
+  // We don't allow functions as element type.
   if(type.element_type().id() == ID_code)
   {
     // ISO/IEC 9899 6.7.5.2
@@ -560,10 +557,14 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
     throw 0;
   }
 
-  // check size, if any
+  // We add the index type.
+  type.index_type_nonconst() = c_index_type();
 
-  if(size.is_not_nil())
+  // Check the array size, if given.
+  if(type.is_complete())
   {
+    exprt &size = type.size();
+    const source_locationt size_source_location = size.find_source_location();
     typecheck_expr(size);
     make_index_type(size);
 

src/solvers/smt2/smt2_conv.cpp

@@ -3097,7 +3097,7 @@ void smt2_convt::flatten_array(const exprt &expr)
     if(i!=1)
       out << "(concat ";
     out << "(select ?far ";
-    convert_expr(from_integer(i-1, array_type.size().type()));
+    convert_expr(from_integer(i - 1, array_type.index_type()));
     out << ")";
     if(i!=1)
       out << " ";
@@ -4041,7 +4041,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
       out << "(store ";
       convert_expr(expr.old());
       out << " ";
-      convert_expr(typecast_exprt(expr.where(), array_type.size().type()));
+      convert_expr(typecast_exprt(expr.where(), array_type.index_type()));
       out << " ";
       convert_expr(expr.new_value());
       out << ")";
@@ -4267,7 +4267,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
         out << "(select ";
         convert_expr(expr.array());
         out << " ";
-        convert_expr(typecast_exprt(expr.index(), array_type.size().type()));
+        convert_expr(typecast_exprt(expr.index(), array_type.index_type()));
         out << ")";
         out << " #b1)";
       }
@@ -4276,7 +4276,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
         out << "(select ";
         convert_expr(expr.array());
         out << " ";
-        convert_expr(typecast_exprt(expr.index(), array_type.size().type()));
+        convert_expr(typecast_exprt(expr.index(), array_type.index_type()));
         out << ")";
       }
     }
@@ -4891,7 +4891,7 @@ void smt2_convt::find_symbols(const exprt &expr)
 
         // use a quantifier-based initialization instead of lambda
         out << "(assert (forall ((i ";
-        convert_type(array_type.size().type());
+        convert_type(array_type.index_type());
         out << ")) (= (select " << id << " i) ";
         if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
         {
@@ -4972,7 +4972,7 @@ void smt2_convt::find_symbols(const exprt &expr)
       for(std::size_t i=0; i<expr.operands().size(); i++)
       {
         out << "(assert (= (select " << id << " ";
-        convert_expr(from_integer(i, array_type.size().type()));
+        convert_expr(from_integer(i, array_type.index_type()));
         out << ") "; // select
         if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
         {
@@ -5008,7 +5008,7 @@ void smt2_convt::find_symbols(const exprt &expr)
       for(std::size_t i=0; i<tmp.operands().size(); i++)
       {
         out << "(assert (= (select " << id << ' ';
-        convert_expr(from_integer(i, array_type.size().type()));
+        convert_expr(from_integer(i, array_type.index_type()));
         out << ") "; // select
         convert_expr(tmp.operands()[i]);
         out << "))" << "\n";
@@ -5127,8 +5127,9 @@ void smt2_convt::convert_type(const typet &type)
     // we always use array theory for top-level arrays
     const typet &subtype = array_type.element_type();
 
+    // Arrays map the index type to the element type.
     out << "(Array ";
-    convert_type(array_type.size().type());
+    convert_type(array_type.index_type());
     out << " ";
 
     if(subtype.id()==ID_bool && !use_array_of_bool)

src/util/irep_ids.def

@@ -101,6 +101,7 @@ IREP_ID_ONE(return)
 IREP_ID_ONE(skip)
 IREP_ID_ONE(arguments)
 IREP_ID_ONE(array)
+IREP_ID_TWO(C_index_type, #index_type)
 IREP_ID_ONE(size)
 IREP_ID_ONE(frontend_pointer)
 IREP_ID_ONE(pointer)

src/util/std_types.cpp

@@ -32,8 +32,14 @@ void array_typet::check(const typet &type, const validation_modet vm)
 
 typet array_typet::index_type() const
 {
-  // we may wish to make the index type part of the array type
-  return c_index_type();
+  // For backwards compatibility, allow the case that the array type is
+  // not annotated with an index type.
+  const auto &annotated_type =
+    static_cast<const typet &>(find(ID_C_index_type));
+  if(annotated_type.is_nil())
+    return c_index_type();
+  else
+    return annotated_type;
 }
 
 /// Return the sequence number of the component with given name.

src/util/std_types.h

@@ -771,6 +771,14 @@ class array_typet:public type_with_subtypet
   /// The type of the index expressions into any instance of this type.
   typet index_type() const;
 
+  /// The type of the index expressions into any instance of this type.
+  /// This is added as a comment now for backwards compatibility, but will
+  /// eventually be the first subtype.
+  typet &index_type_nonconst()
+  {
+    return static_cast<typet &>(add(ID_C_index_type));
+  }
+
   /// The type of the elements of the array.
   /// This method is preferred over .subtype(),
   /// which will eventually be deprecated.
@@ -787,11 +795,15 @@ class array_typet:public type_with_subtypet
     return subtype();
   }
 
+  // We will eventually enforce that the type of the size
+  // is the same as the index type.
   const exprt &size() const
   {
     return static_cast<const exprt &>(find(ID_size));
   }
 
+  // We will eventually enforce that the type of the size
+  // is the same as the index type.
   exprt &size()
   {
     return static_cast<exprt &>(add(ID_size));