Merge pull request #7018 from diffblue/index_array_type

index_exprt enforces array or vector type

Author: kroening

src/ansi-c/expr2c.cpp

@@ -1401,15 +1401,10 @@ std::string expr2ct::convert_unary_post(
   return dest;
 }
 
-std::string expr2ct::convert_index(
-  const exprt &src,
-  unsigned precedence)
+std::string expr2ct::convert_index(const binary_exprt &src, unsigned precedence)
 {
-  if(src.operands().size()!=2)
-    return convert_norep(src, precedence);
-
   unsigned p;
-  std::string op = convert_with_precedence(to_index_expr(src).array(), p);
+  std::string op = convert_with_precedence(src.op0(), p);
 
   std::string dest;
   if(precedence>p)
@@ -1419,7 +1414,7 @@ std::string expr2ct::convert_index(
     dest+=')';
 
   dest+='[';
-  dest += convert(to_index_expr(src).index());
+  dest += convert(src.op1());
   dest+=']';
 
   return dest;
@@ -3680,15 +3675,14 @@ std::string expr2ct::convert_with_precedence(
       to_plus_expr(pointer).op0().type().id() == ID_pointer)
     {
       // Note that index[pointer] is legal C, but we avoid it nevertheless.
-      return convert(
-        index_exprt(to_plus_expr(pointer).op0(), to_plus_expr(pointer).op1()));
+      return convert_index(to_binary_expr(pointer), precedence = 16);
     }
     else
       return convert_unary(to_unary_expr(src), "*", precedence = 15);
   }
 
   else if(src.id()==ID_index)
-    return convert_index(src, precedence=16);
+    return convert_index(to_binary_expr(src), precedence = 16);
 
   else if(src.id()==ID_member)
     return convert_member(to_member_expr(src), precedence=16);

src/ansi-c/expr2c_class.h

@@ -157,8 +157,7 @@ class expr2ct
   std::string convert_index_designator(
     const exprt &src);
 
-  std::string convert_index(
-    const exprt &src, unsigned precedence);
+  std::string convert_index(const binary_exprt &, unsigned precedence);
 
   std::string
   convert_byte_extract(const byte_extract_exprt &, unsigned precedence);

src/util/std_expr.h

@@ -1409,6 +1409,7 @@ inline notequal_exprt &to_notequal_expr(exprt &expr)
 class index_exprt:public binary_exprt
 {
 public:
+  // _array must have either index or vector type.
   // When _array has array_type, the type of _index
   // must be array_type.index_type().
   // This will eventually be enforced using a precondition.
@@ -1419,6 +1420,9 @@ class index_exprt:public binary_exprt
         std::move(_index),
         to_type_with_subtype(_array.type()).subtype())
   {
+    const auto &array_op_type = _array.type();
+    PRECONDITION(
+      array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
   }
 
   index_exprt(exprt _array, exprt _index, typet _type)
@@ -1428,6 +1432,9 @@ class index_exprt:public binary_exprt
         std::move(_index),
         std::move(_type))
   {
+    const auto &array_op_type = array().type();
+    PRECONDITION(
+      array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
   }
 
   exprt &array()

unit/solvers/smt2_incremental/object_tracking.cpp

@@ -93,7 +93,8 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]")
 TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]")
 {
   const typet base_type = pointer_typet{signedbv_typet{16}, 18};
-  const symbol_exprt foo{"foo", base_type};
+  const symbol_exprt foo{
+    "foo", array_typet(base_type, from_integer(2, size_type()))};
   const symbol_exprt bar{"bar", base_type};
   const symbol_exprt qux{"qux", struct_typet{}};
   const symbol_exprt index{"index", base_type};