C front-end: ensure array type updates are consistent

We must not end up in a situation where the symbol's array type is
different from the type applied to symbol expressions in code. With the
previous approach, support-function generation would alter the type
after typechecking of code had already been completed. Instead, do as
the C standard says: if the type is incomplete _at the end of a
translation unit_, the (implicit) initializer makes it a one-element
array.

Fixes: #7608

Author: tautschnig

regression/cbmc/extern6/main.c

@@ -0,0 +1,12 @@
+extern int stuff[];
+
+extern int a[];
+int a[] = {1, 2, 3};
+
+int main()
+{
+  unsigned char idx;
+  long val = *(long *)(stuff + idx);
+  __CPROVER_assert(val == 13, "compare");
+  return 0;
+}

regression/cbmc/extern6/test.desc

@@ -0,0 +1,9 @@
+CORE broken-smt-backend no-new-smt
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^Invariant check failed

src/ansi-c/ansi_c_language.cpp

@@ -8,8 +8,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "ansi_c_language.h"
 
+#include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/get_base_name.h>
+#include <util/replace_symbol.h>
 #include <util/symbol_table.h>
 
 #include <linking/linking.h>
@@ -124,6 +127,36 @@ bool ansi_c_languaget::typecheck(
     return true;
   }
 
+  unchecked_replace_symbolt array_type_updates;
+  for(auto it = new_symbol_table.begin(); it != new_symbol_table.end(); ++it)
+  {
+    // C standard 6.9.2, paragraph 5
+    // adjust the type of an external array without size to an array of size 1
+    symbolt &symbol = it.get_writeable_symbol();
+    if(
+      symbol.is_static_lifetime && !symbol.is_extern && !symbol.is_type &&
+      !symbol.is_macro && symbol.type.id() == ID_array &&
+      to_array_type(symbol.type).size().is_nil())
+    {
+      symbol_exprt previous_expr = symbol.symbol_expr();
+      to_array_type(symbol.type).size() = from_integer(1, size_type());
+      array_type_updates.insert(previous_expr, symbol.symbol_expr());
+    }
+  }
+  if(!array_type_updates.empty())
+  {
+    // Apply type updates to initializers
+    for(auto it = new_symbol_table.begin(); it != new_symbol_table.end(); ++it)
+    {
+      if(
+        !it->second.is_type && !it->second.is_macro &&
+        it->second.value.is_not_nil())
+      {
+        array_type_updates(it.get_writeable_symbol().value);
+      }
+    }
+  }
+
   remove_internal_symbols(
     new_symbol_table, message_handler, keep_file_local, keep);
 

src/linking/static_lifetime_init.cpp

@@ -8,7 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "static_lifetime_init.h"
 
-#include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
 #include <util/namespace.h>
@@ -53,11 +52,8 @@ static std::optional<codet> static_lifetime_init(
 
   if(symbol.type.id() == ID_array && to_array_type(symbol.type).size().is_nil())
   {
-    // C standard 6.9.2, paragraph 5
-    // adjust the type to an array of size 1
-    symbolt &writable_symbol = symbol_table.get_writeable_ref(identifier);
-    writable_symbol.type = symbol.type;
-    writable_symbol.type.set(ID_size, from_integer(1, size_type()));
+    DATA_INVARIANT(symbol.is_extern, "arrays must have a size");
+    return {};
   }
 
   if(

src/util/lower_byte_operators.cpp

@@ -511,6 +511,14 @@ static exprt unpack_array_vector_no_known_bounds(
                                     ? to_vector_type(src.type()).size()
                                     : to_array_type(src.type()).size();
 
+  if(array_vector_size.is_nil())
+  {
+    return array_comprehension_exprt{
+      std::move(array_comprehension_index),
+      std::move(body),
+      array_typet{bv_typet{bits_per_byte}, from_integer(0, size_type())}};
+  }
+
   return array_comprehension_exprt{
     std::move(array_comprehension_index),
     std::move(body),