goto-symex: nil array size must not have a type added

An expression has a type() member, which the nil irept lacks. Trying to
access (in a non-const context) the type() member would thus create it,
which in turn means that it no longer compares equal to a nil_exprt.  As
SSA renaming did access the type() member in such a way, the type of an
array without specified size would no longer compare equal to the irept
describing the type as generated by the C front-end, which in turn made
simplification fail.

The problem was surfaced by running cbmc --unwind 2 --pointer-check
--bounds-check on
c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--i915--i915.ko-entry_point.cil.out.i
from SV-COMP.

Author: tautschnig

src/goto-symex/goto_symex_state.cpp

@@ -252,6 +252,10 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
       as_const(address_of_expr).object().type();
     return renamedt<exprt, level>{std::move(expr)};
   }
+  else if(expr.is_nil())
+  {
+    return renamedt<exprt, level>{std::move(expr)};
+  }
   else
   {
     rename<level>(expr.type(), irep_idt(), ns);

src/goto-symex/renaming_level.cpp

@@ -263,6 +263,10 @@ bool check_renaming(const exprt &expr)
     if(to_ssa_expr(expr).get_original_expr().type() != type)
       return true;
   }
+  else if(expr.id() == ID_nil)
+  {
+    return expr != nil_exprt{};
+  }
   else
   {
     forall_operands(it, expr)

src/util/std_types.cpp

@@ -18,6 +18,19 @@ Author: Daniel Kroening, [email protected]
 #include "std_expr.h"
 #include "string2int.h"
 
+void array_typet::check(const typet &type, const validation_modet vm)
+{
+  PRECONDITION(type.id() == ID_array);
+  const array_typet &array_type = static_cast<const array_typet &>(type);
+  if(array_type.size().is_nil())
+  {
+    DATA_CHECK(
+      vm,
+      array_type.size() == nil_exprt{},
+      "nil array size must be exactly nil");
+  }
+}
+
 std::size_t fixedbv_typet::get_integer_bits() const
 {
   const irep_idt integer_bits=get(ID_integer_bits);

src/util/std_types.h

@@ -984,6 +984,10 @@ class array_typet:public type_with_subtypet
   {
     return size().is_nil();
   }
+
+  static void check(
+    const typet &type,
+    const validation_modet vm = validation_modet::INVARIANT);
 };
 
 /// Check whether a reference to a typet is a \ref array_typet.

src/util/validate_types.cpp

@@ -52,6 +52,10 @@ void call_on_type(const typet &type, Args &&... args)
   {
     CALL_ON_TYPE(c_bool_typet);
   }
+  else if(type.id() == ID_array)
+  {
+    CALL_ON_TYPE(array_typet);
+  }
   else
   {
 #ifdef REPORT_UNIMPLEMENTED_TYPE_CHECKS