util: expose is_zero_width via util/pointer_offset_size

src/solvers/smt2/smt2_conv.cpp

@@ -243,38 +243,6 @@ void smt2_convt::write_footer()
       << "\n";
 }
 
-/// Returns true iff \p type has effective width of zero bits.
-static bool is_zero_width(const typet &type, const namespacet &ns)
-{
-  if(type.id() == ID_empty)
-    return true;
-  else if(type.id() == ID_struct_tag)
-    return is_zero_width(ns.follow_tag(to_struct_tag_type(type)), ns);
-  else if(type.id() == ID_union_tag)
-    return is_zero_width(ns.follow_tag(to_union_tag_type(type)), ns);
-  else if(type.id() == ID_struct || type.id() == ID_union)
-  {
-    for(const auto &comp : to_struct_union_type(type).components())
-    {
-      if(!is_zero_width(comp.type(), ns))
-        return false;
-    }
-    return true;
-  }
-  else if(auto array_type = type_try_dynamic_cast<array_typet>(type))
-  {
-    // we ignore array_type->size().is_zero() for now as there may be
-    // out-of-bounds accesses that we need to model
-    return is_zero_width(array_type->element_type(), ns);
-  }
-  else if(auto bv_type = type_try_dynamic_cast<bitvector_typet>(type))
-  {
-    return bv_type->width() == 0;
-  }
-  else
-    return false;
-}
-
 void smt2_convt::define_object_size(
   const irep_idt &id,
   const object_size_exprt &expr)

src/util/pointer_offset_size.cpp

@@ -497,6 +497,41 @@ std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns)
     return {};
 }
 
+bool is_zero_width(const typet &type, const namespacet &ns)
+{
+  if(type.id() == ID_empty)
+    return true;
+  else if(type.id() == ID_struct_tag)
+    return is_zero_width(ns.follow_tag(to_struct_tag_type(type)), ns);
+  else if(type.id() == ID_union_tag)
+    return is_zero_width(ns.follow_tag(to_union_tag_type(type)), ns);
+  else if(type.id() == ID_c_enum_tag)
+    return is_zero_width(ns.follow_tag(to_c_enum_tag_type(type)), ns);
+  else if(type.id() == ID_c_enum)
+    return is_zero_width(to_c_enum_type(type).subtype(), ns);
+  else if(type.id() == ID_struct || type.id() == ID_union)
+  {
+    for(const auto &comp : to_struct_union_type(type).components())
+    {
+      if(!is_zero_width(comp.type(), ns))
+        return false;
+    }
+    return true;
+  }
+  else if(auto array_type = type_try_dynamic_cast<array_typet>(type))
+  {
+    // we ignore array_type->size().is_zero() for now as there may be
+    // out-of-bounds accesses that we need to model
+    return is_zero_width(array_type->element_type(), ns);
+  }
+  else if(auto bv_type = type_try_dynamic_cast<bitvector_typet>(type))
+  {
+    return bv_type->width() == 0;
+  }
+  else
+    return false;
+}
+
 std::optional<mp_integer>
 compute_pointer_offset(const exprt &expr, const namespacet &ns)
 {

src/util/pointer_offset_size.h

@@ -39,6 +39,16 @@ pointer_offset_size(const typet &type, const namespacet &ns);
 std::optional<mp_integer>
 pointer_offset_bits(const typet &type, const namespacet &ns);
 
+/// Returns true iff \p type has effective width of zero bits.
+/// In addition to the obvious \c ID_empty, this recognises
+/// struct/union types whose components are all zero-width and arrays
+/// of zero-width elements, mirroring the semantics that the
+/// bit-blasting back-ends use to skip such types. Tag types
+/// (\c ID_struct_tag, \c ID_union_tag, \c ID_c_enum_tag) are unwrapped
+/// via \p ns before further recursion; \c ID_c_enum types recurse
+/// into their underlying integer type.
+bool is_zero_width(const typet &type, const namespacet &ns);
+
 std::optional<mp_integer>
 compute_pointer_offset(const exprt &expr, const namespacet &ns);
 

unit/util/pointer_offset_size.cpp

@@ -124,3 +124,85 @@ TEST_CASE("Build subexpression to access element at offset into struct")
         member_exprt(s, "foo", t), from_integer(1, c_index_type()), small_t));
   }
 }
+
+TEST_CASE("is_zero_width predicate", "[core][util][pointer_offset_size]")
+{
+  cmdlinet cmdline;
+  config.set(cmdline);
+
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  // Trivial cases.
+  REQUIRE(is_zero_width(empty_typet{}, ns));
+  REQUIRE_FALSE(is_zero_width(signedbv_typet{32}, ns));
+
+  // Zero-width bitvector. bv_typet permits a zero width.
+  REQUIRE(is_zero_width(bv_typet{0}, ns));
+
+  // Struct with all-empty components is zero-width.
+  {
+    struct_typet st({{"a", empty_typet{}}, {"b", empty_typet{}}});
+    REQUIRE(is_zero_width(st, ns));
+  }
+
+  // Struct with at least one non-zero-width component is not zero-width.
+  {
+    struct_typet st({{"a", empty_typet{}}, {"b", signedbv_typet{32}}});
+    REQUIRE_FALSE(is_zero_width(st, ns));
+  }
+
+  // Array of empty type is zero-width regardless of size — the predicate
+  // deliberately ignores the array length, since we may still need to
+  // model out-of-bounds accesses.
+  {
+    array_typet at_const(empty_typet{}, from_integer(2, size_type()));
+    REQUIRE(is_zero_width(at_const, ns));
+
+    array_typet at_sym(empty_typet{}, symbol_exprt{"n", size_type()});
+    REQUIRE(is_zero_width(at_sym, ns));
+  }
+
+  // struct_tag_typet that resolves (via symbol table) to an empty struct
+  // is zero-width — exercises the tag-following recursion.
+  {
+    type_symbolt empty_struct_symbol{
+      "empty_struct_t",
+      struct_typet({{"a", empty_typet{}}, {"b", empty_typet{}}}),
+      ID_C};
+    symbol_table.insert(empty_struct_symbol);
+
+    struct_tag_typet stag{empty_struct_symbol.name};
+    REQUIRE(is_zero_width(stag, ns));
+  }
+
+  // c_enum_tag_typet recurses into the underlying c_enum_typet, which
+  // recurses into its subtype. A regular C enum (signed int subtype)
+  // is not zero-width. (Behaviour changed in this PR — the predicate
+  // previously fell through to `return false` for any tag kind other
+  // than struct/union, which happened to give the correct answer for
+  // this case but was an unprincipled coincidence.)
+  {
+    c_enum_typet enum_signed_int{signed_int_type()};
+    type_symbolt enum_symbol{"my_enum_t", enum_signed_int, ID_C};
+    symbol_table.insert(enum_symbol);
+
+    c_enum_tag_typet etag{enum_symbol.name};
+    REQUIRE_FALSE(is_zero_width(etag, ns));
+  }
+
+  // Hypothetical zero-width c_enum: subtype is zero-width, so the
+  // resolved enum is too. Without this PR's added arm the predicate
+  // would have returned false here.
+  {
+    c_enum_typet enum_empty{empty_typet{}};
+    type_symbolt zw_enum_symbol{"zero_width_enum_t", enum_empty, ID_C};
+    symbol_table.insert(zw_enum_symbol);
+
+    c_enum_tag_typet zw_etag{zw_enum_symbol.name};
+    REQUIRE(is_zero_width(zw_etag, ns));
+
+    // The unwrapped c_enum_typet itself also recurses into its subtype.
+    REQUIRE(is_zero_width(enum_empty, ns));
+  }
+}