From b032d1a3ad5ad600b29d5f3181bca64d97a1c47d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 13 Dec 2020 22:29:27 +0000
Subject: [PATCH] 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.
---
 src/goto-symex/goto_symex_state.cpp |  4 ++++
 src/goto-symex/renaming_level.cpp   |  4 ++++
 src/util/std_types.cpp              | 13 +++++++++++++
 src/util/std_types.h                |  4 ++++
 src/util/validate_types.cpp         |  4 ++++
 5 files changed, 29 insertions(+)

diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 22afa8ebcbc..66fe05bed1d 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/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);
diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp
index ebb489a7cad..23af91030d7 100644
--- a/src/goto-symex/renaming_level.cpp
+++ b/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)
diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp
index 128e51a5f9c..3184b5ebbed 100644
--- a/src/util/std_types.cpp
+++ b/src/util/std_types.cpp
@@ -18,6 +18,19 @@ Author: Daniel Kroening, kroening@kroening.com
 #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);
diff --git a/src/util/std_types.h b/src/util/std_types.h
index d193f98e3ae..45acdbc5456 100644
--- a/src/util/std_types.h
+++ b/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.
diff --git a/src/util/validate_types.cpp b/src/util/validate_types.cpp
index 565285610bc..f6977ca440a 100644
--- a/src/util/validate_types.cpp
+++ b/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