The size of arrays is unsigned

Arrays have an unsigned size, and this must also be true when converting
string constants to arrays. Using signed size types resulted in
invariant failures in the simplifier, which were triggered by passing in
arrays with a negative size. Observed on several SV-COMP benchmarks in
the device drivers category, for example (with --unwind 2):
ldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--wireless--iwlwifi--iwlwifi.ko-entry_point.cil.out.i

Author: tautschnig

regression/ansi-c/arch_flags_mcpu_bad/object.intel

@@ -1,6 +1,6 @@
 CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y
+--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:5 --havoc-variables y
 ^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$
 ^\[main.assertion.2\] line \d+ assertion 0: FAILURE$
 ^EXIT=10$

regression/ansi-c/arch_flags_mcpu_good/object.arm

@@ -951,7 +951,7 @@ exprt c_typecheck_baset::do_initializer_list(
     // make complete by setting array size
     size_t size=result.operands().size();
     result.type().id(ID_array);
-    result.type().set(ID_size, from_integer(size, index_type()));
+    result.type().set(ID_size, from_integer(size, size_type()));
   }
 
   return result;

regression/ansi-c/arch_flags_mthumb_bad/object.intel

@@ -559,7 +559,6 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
   if(size.is_not_nil())
   {
     typecheck_expr(size);
-    make_index_type(size);
 
     // The size need not be a constant!
     // We simplify it, for the benefit of array initialisation.
@@ -587,10 +586,13 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
         throw 0;
       }
 
+      implicit_typecast(tmp_size, size_type());
+      simplify(tmp_size, *this);
       size=tmp_size;
     }
     else if(tmp_size.id()==ID_infinity)
     {
+      tmp_size.type() = size_type();
       size=tmp_size;
     }
     else if(tmp_size.id()==ID_symbol &&
@@ -602,6 +604,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
       // Of course we can modify a 'const' symbol, e.g.,
       // using a pointer type cast. Interestingly,
       // at least gcc 4.2.1 makes the very same mistake!
+      implicit_typecast(tmp_size, size_type());
       size=tmp_size;
     }
     else
@@ -985,7 +988,7 @@ void c_typecheck_baset::typecheck_compound_body(
 
         // make it zero-length
         c_type.id(ID_array);
-        c_type.set(ID_size, from_integer(0, index_type()));
+        c_type.set(ID_size, from_integer(0, size_type()));
       }
     }
   }

regression/ansi-c/arch_flags_mthumb_good/object.arm

@@ -132,7 +132,7 @@ exprt convert_string_literal(const std::string &src)
     result.set(ID_C_string_constant, true);
     result.type()=typet(ID_array);
     result.type().subtype()=subtype;
-    result.type().set(ID_size, from_integer(value.size(), index_type()));
+    result.type().set(ID_size, from_integer(value.size(), size_type()));
 
     result.operands().resize(value.size());
     for(std::size_t i=0; i<value.size(); i++)

regression/goto-harness/havoc-global-int-02/test.desc

@@ -774,7 +774,8 @@ void cpp_typecheckt::check_fixed_size_array(typet &type)
           array_type.size() = symbol.value;
       }
 
-      make_constant_index(array_type.size());
+      implicit_typecast(array_type.size(), size_type());
+      make_constant(array_type.size());
     }
 
     // recursive call for multi-dimensional arrays

src/ansi-c/c_typecheck_initializer.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_initializer.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 
 #include <ansi-c/c_qualifiers.h>
 
@@ -758,10 +759,8 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr)
     exprt &size=to_array_type(expr.type()).size();
     typecheck_expr(size);
 
-    bool size_is_unsigned=(size.type().id()==ID_unsignedbv);
-    bitvector_typet integer_type(
-      size_is_unsigned ? ID_unsignedbv : ID_signedbv, config.ansi_c.int_width);
-    implicit_typecast(size, integer_type);
+    implicit_typecast(size, size_type());
+    simplify(size, *this);
 
     expr.set(ID_statement, ID_cpp_new_array);