Decompose byte_extract from union through widest member

When byte_extract is applied to a union-typed expression with a
non-constant computed offset, the byte_extract lowering creates a
massive expression because it must consider all possible byte layouts.
For unions where the widest member covers the entire union, we can
instead decompose the access through that member, avoiding the
expensive lowering.

Add union handling to the non-constant-offset overload of
get_subexpression_at_offset: for symbol and member expressions of
union type, recurse into the widest member. Guard this on the widest
member's size equalling the union's size (no trailing padding).

The constant-offset overload is left unchanged to preserve existing
simplification behavior (e.g., byte_extract(byte_update(...))
patterns used during constant propagation).

On the reproducer from #8813, the union version now takes 1.0s
(previously 94s), matching the struct version at 1.0s.

Fixes: #8813

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

regression/cbmc/union_performance1/main.c

@@ -0,0 +1,22 @@
+// Test that byte_extract from a union does not cause performance explosion.
+// See GitHub issue diffblue/cbmc#8813.
+#include <assert.h>
+#include <stdint.h>
+
+typedef struct
+{
+  int32_t data[8];
+} arr;
+
+int main()
+{
+  union
+  {
+    arr a;
+    arr b;
+  } u;
+  unsigned i;
+  __CPROVER_assume(i < 8);
+  u.a.data[i] = 42;
+  assert(u.b.data[i] == 42);
+}

regression/cbmc/union_performance1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Union of same-typed members should not cause performance explosion.
+See GitHub issue diffblue/cbmc#8813.

src/util/pointer_offset_size.cpp

@@ -859,6 +859,32 @@ std::optional<exprt> get_subexpression_at_offset(
 
       return {};
     }
+    else if(expr.type().id() == ID_union || expr.type().id() == ID_union_tag)
+    {
+      // For union-typed expressions with non-constant offset, access
+      // through the widest member to avoid expensive byte_extract lowering.
+      // This is safe when the widest member covers the full union (no
+      // trailing padding beyond it), since all members start at offset 0.
+      if(expr.id() == ID_symbol || expr.id() == ID_member)
+      {
+        const union_typet &union_type =
+          expr.type().id() == ID_union_tag
+            ? ns.follow_tag(to_union_tag_type(expr.type()))
+            : to_union_type(expr.type());
+
+        const auto union_size = pointer_offset_bits(union_type, ns);
+        const auto widest_member = union_type.find_widest_union_component(ns);
+        if(
+          widest_member.has_value() && union_size.has_value() &&
+          widest_member->second == *union_size)
+        {
+          const member_exprt member(
+            expr, widest_member->first.get_name(), widest_member->first.type());
+          return get_subexpression_at_offset(member, offset, target_type, ns);
+        }
+      }
+      return {};
+    }
     else
       return {};
   }