Merge pull request #5746 from tautschnig/find_widest_union_component

Make computation of widest union member widely available

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -21,41 +21,6 @@ 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_type: Type to determine the member of.
-/// \param ns: Namespace to resolve tag types.
-/// \return Pair of a componentt pointing to the maximum fixed bit-width
-///   member of \p union_type and the bit width of that member.
-static optionalt<std::pair<struct_union_typet::componentt, mp_integer>>
-find_widest_union_component(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(
-      struct_union_typet::componentt{max_comp_name, max_comp_type}, max_width);
-}
-
 static exprt bv_to_expr(
   const exprt &bitvector_expr,
   const typet &target_type,
@@ -155,7 +120,7 @@ static union_exprt bv_to_union_expr(
   if(components.empty())
     return union_exprt{irep_idt{}, nil_exprt{}, union_type};
 
-  const auto widest_member = find_widest_union_component(union_type, ns);
+  const auto widest_member = union_type.find_widest_union_component(ns);
 
   std::size_t component_bits;
   if(widest_member.has_value())
@@ -1222,7 +1187,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
   {
     const union_typet &union_type = to_union_type(ns.follow(src.type()));
 
-    const auto widest_member = find_widest_union_component(union_type, ns);
+    const auto widest_member = union_type.find_widest_union_component(ns);
 
     if(widest_member.has_value())
     {
@@ -2029,7 +1994,7 @@ static exprt lower_byte_update_union(
   const optionalt<exprt> &non_const_update_bound,
   const namespacet &ns)
 {
-  const auto widest_member = find_widest_union_component(union_type, ns);
+  const auto widest_member = union_type.find_widest_union_component(ns);
 
   PRECONDITION_WITH_DIAGNOSTICS(
     widest_member.has_value(),

src/util/pointer_offset_size.cpp

@@ -154,23 +154,16 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
   else if(type.id()==ID_union)
   {
     const union_typet &union_type=to_union_type(type);
-    mp_integer result=0;
-
-    // compute max
-
-    for(const auto &c : union_type.components())
-    {
-      const typet &subtype = c.type();
-      auto sub_size = pointer_offset_bits(subtype, ns);
 
-      if(!sub_size.has_value())
-        return {};
+    if(union_type.components().empty())
+      return mp_integer{0};
 
-      if(*sub_size > result)
-        result = *sub_size;
-    }
+    const auto widest_member = union_type.find_widest_union_component(ns);
 
-    return result;
+    if(widest_member.has_value())
+      return widest_member->second;
+    else
+      return {};
   }
   else if(type.id()==ID_signedbv ||
           type.id()==ID_unsignedbv ||

src/util/std_types.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include "arith_tools.h"
 #include "bv_arithmetic.h"
 #include "namespace.h"
+#include "pointer_offset_size.h"
 #include "std_expr.h"
 #include "string2int.h"
 
@@ -287,3 +288,34 @@ constant_exprt &vector_typet::size()
 {
   return static_cast<constant_exprt &>(add(ID_size));
 }
+
+optionalt<std::pair<struct_union_typet::componentt, mp_integer>>
+union_typet::find_widest_union_component(const namespacet &ns) const
+{
+  const union_typet::componentst &comps = components();
+
+  optionalt<mp_integer> max_width;
+  typet max_comp_type;
+  irep_idt max_comp_name;
+
+  for(const auto &comp : comps)
+  {
+    auto element_width = pointer_offset_bits(comp.type(), ns);
+
+    if(!element_width.has_value())
+      return {};
+
+    if(max_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.has_value())
+    return {};
+  else
+    return std::make_pair(
+      struct_union_typet::componentt{max_comp_name, max_comp_type}, *max_width);
+}

src/util/std_types.h

@@ -400,6 +400,14 @@ class union_typet:public struct_union_typet
     : struct_union_typet(ID_union, std::move(_components))
   {
   }
+
+  /// Determine the member of maximum bit width in a union type. If no member,
+  /// or a member of non-fixed width can be found, return nullopt.
+  /// \param ns: Namespace to resolve tag types.
+  /// \return Pair of a componentt pointing to the maximum fixed bit-width
+  ///   member of the union type and the bit width of that member.
+  optionalt<std::pair<struct_union_typet::componentt, mp_integer>>
+  find_widest_union_component(const namespacet &ns) const;
 };
 
 /// Check whether a reference to a typet is a \ref union_typet.