Factor out computation of maximum union member

Avoids duplicate code and enables future re-use.

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -21,6 +21,46 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/string_constant.h>
 
+/// Determine the member of maximum fixed bit width in a union type. If no
+/// member, or no member of fixed and non-zero width can be found, return
+/// nullopt.
+/// \param union_expr: Expression to use as compound operand in the resulting
+///   member_exprt.
+/// \param union_type: Type to determine the member of.
+/// \param ns: Namespace to resolve tag types.
+/// \return Pair of a member_exprt pointing to the maximum fixed bit-width
+///   member of \p union_type and the bit width of that member.
+static optionalt<std::pair<member_exprt, mp_integer>>
+find_maximum_union_component(
+  const exprt &union_expr,
+  const union_typet &union_type,
+  const namespacet &ns)
+{
+  const union_typet::componentst &components = union_type.components();
+
+  mp_integer max_width = 0;
+  typet max_comp_type;
+  irep_idt max_comp_name;
+
+  for(const auto &comp : components)
+  {
+    auto element_width = pointer_offset_bits(comp.type(), ns);
+
+    if(!element_width.has_value() || *element_width <= max_width)
+      continue;
+
+    max_width = *element_width;
+    max_comp_type = comp.type();
+    max_comp_name = comp.get_name();
+  }
+
+  if(max_width == 0)
+    return {};
+  else
+    return std::make_pair(
+      member_exprt{union_expr, max_comp_name, max_comp_type}, max_width);
+}
+
 static exprt bv_to_expr(
   const exprt &bitvector_expr,
   const typet &target_type,
@@ -1124,31 +1164,19 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
   else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
   {
     const union_typet &union_type = to_union_type(ns.follow(src.type()));
-    const union_typet::componentst &components = union_type.components();
-
-    mp_integer max_width = 0;
-    typet max_comp_type;
-    irep_idt max_comp_name;
-
-    for(const auto &comp : components)
-    {
-      auto element_width = pointer_offset_bits(comp.type(), ns);
 
-      if(!element_width.has_value() || *element_width <= max_width)
-        continue;
+    const auto max_member_expr =
+      find_maximum_union_component(src, union_type, ns);
 
-      max_width = *element_width;
-      max_comp_type = comp.type();
-      max_comp_name = comp.get_name();
-    }
-
-    if(max_width > 0)
+    if(max_member_expr.has_value())
     {
       byte_extract_exprt tmp(unpacked);
-      tmp.type() = max_comp_type;
+      tmp.type() = max_member_expr->first.type();
 
       return union_exprt(
-        max_comp_name, lower_byte_extract(tmp, ns), src.type());
+        max_member_expr->first.get_component_name(),
+        lower_byte_extract(tmp, ns),
+        src.type());
     }
   }
 
@@ -1945,34 +1973,19 @@ static exprt lower_byte_update_union(
   const optionalt<exprt> &non_const_update_bound,
   const namespacet &ns)
 {
-  const union_typet::componentst &components = union_type.components();
-
-  mp_integer max_width = 0;
-  typet max_comp_type;
-  irep_idt max_comp_name;
-
-  for(const auto &comp : components)
-  {
-    auto element_width = pointer_offset_bits(comp.type(), ns);
-
-    if(!element_width.has_value() || *element_width <= max_width)
-      continue;
-
-    max_width = *element_width;
-    max_comp_type = comp.type();
-    max_comp_name = comp.get_name();
-  }
+  const auto max_member_expr =
+    find_maximum_union_component(src.op(), union_type, ns);
 
   PRECONDITION_WITH_DIAGNOSTICS(
-    max_width > 0,
+    max_member_expr.has_value(),
     "lower_byte_update of union of unknown size is not supported");
 
   byte_update_exprt bu = src;
-  bu.set_op(member_exprt{src.op(), max_comp_name, max_comp_type});
-  bu.type() = max_comp_type;
+  bu.set_op(max_member_expr->first);
+  bu.type() = max_member_expr->first.type();
 
   return union_exprt{
-    max_comp_name,
+    max_member_expr->first.get_component_name(),
     lower_byte_update(bu, value_as_byte_array, non_const_update_bound, ns),
     src.type()};
 }