boolbv_index: handle incomplete extern array types in symbol registration

regression/cbmc/incomplete_extern_array1/main.c

@@ -0,0 +1,26 @@
+// Regression test for the fix to:
+//   src/solvers/flattening/boolbv_index.cpp
+// where indexing into an `extern T arr[]` (incomplete array)
+// at multiple indices used to register the symbol with width
+// 0 in boolbv_mapt, then trip the size-equals-width invariant
+// in get_literals.
+//
+// The Linux kernel hits this via <linux/ctype.h>'s
+// `extern const unsigned char _ctype[]` declaration combined
+// with the `__ismask(c)` macro that expands to `_ctype[c]`.
+
+extern const unsigned char _ctype[];
+
+int nondet_int(void);
+
+int main(void)
+{
+  int c = nondet_int();
+  if(c >= 0 && c < 128)
+  {
+    unsigned char m1 = _ctype[c];
+    unsigned char m2 = _ctype[c + 1];
+    return m1 + m2;
+  }
+  return 0;
+}

regression/cbmc/incomplete_extern_array1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^Invariant check failed

src/solvers/flattening/boolbv_index.cpp

@@ -51,10 +51,22 @@ bvt boolbvt::convert_index(const index_exprt &expr)
           final_array.id() == ID_symbol || final_array.id() == ID_nondet_symbol)
         {
           const auto &array_width_opt = bv_width.get_width_opt(array_type);
-          (void)map.get_literals(
-            final_array.get(ID_identifier),
-            array_type,
-            array_width_opt.value_or(0));
+          const std::size_t array_width = array_width_opt.value_or(0);
+          // Record the array symbol's type.  Skip only when the symbol is
+          // already registered at a *different* width: an incomplete extern
+          // array (e.g. `extern T arr[]`, width 0 here) may already be
+          // registered at a non-zero width via its element-typed access path,
+          // and re-registering at width 0 would trip get_literals'
+          // size-equals-width invariant.  A first-time registration (the
+          // common case, including string refinement) is preserved.
+          const irep_idt &array_id = final_array.get(ID_identifier);
+          const auto existing = map.get_map_entry(array_id);
+          if(
+            !existing.has_value() ||
+            existing->get().literal_map.size() == array_width)
+          {
+            (void)map.get_literals(array_id, array_type, array_width);
+          }
         }
 
         // make sure we have the index in the cache
@@ -71,8 +83,16 @@ bvt boolbvt::convert_index(const index_exprt &expr)
         if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)
         {
           const auto &array_width_opt = bv_width.get_width_opt(array_type);
-          (void)map.get_literals(
-            array.get(ID_identifier), array_type, array_width_opt.value_or(0));
+          // See comment above for the same case in the byte-operator branch.
+          const std::size_t array_width = array_width_opt.value_or(0);
+          const irep_idt &array_id = array.get(ID_identifier);
+          const auto existing = map.get_map_entry(array_id);
+          if(
+            !existing.has_value() ||
+            existing->get().literal_map.size() == array_width)
+          {
+            (void)map.get_literals(array_id, array_type, array_width);
+          }
         }
 
         // make sure we have the index in the cache

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -171,6 +171,19 @@ void send_function_definition(
     &expression_identifiers,
   std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
+  // The same SSA identifier can be reached via two expressions that differ
+  // only in their (sort-equivalent) type irep -- e.g. an incomplete
+  // `extern T arr[]` whose array type is represented differently at
+  // different access sites.  Such expressions are distinct keys in
+  // expression_identifiers, so both reach this point, but they denote the
+  // same symbol and must be declared to the solver only once.  Map any
+  // later expression to the already-declared identifier.
+  const auto existing = identifier_table.find(symbol_identifier);
+  if(existing != identifier_table.end())
+  {
+    expression_identifiers.emplace(expr, existing->second);
+    return;
+  }
   const smt_declare_function_commandt function{
     smt_identifier_termt(
       symbol_identifier, convert_type_to_smt_sort(expr.type())),