From d65222f8e95700bf9b43728a67b444c0ddfac60d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 13 Aug 2020 14:15:30 +0000 Subject: [PATCH 1/2] Make computation of widest union member widely available This functionality is of use beyond byte-operator lowering. Actual additional uses will be introduced in subsequent commits. --- src/solvers/lowering/byte_operators.cpp | 41 ++----------------------- src/util/std_types.cpp | 29 +++++++++++++++++ src/util/std_types.h | 9 ++++++ 3 files changed, 41 insertions(+), 38 deletions(-) diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index 13570a65654..f49951a5b3a 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -21,41 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -/// 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> -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 &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(), diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index 3184b5ebbed..ddd6a97d3b2 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #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,31 @@ constant_exprt &vector_typet::size() { return static_cast(add(ID_size)); } + +optionalt> +union_typet::find_widest_union_component(const namespacet &ns) const +{ + const union_typet::componentst &comps = components(); + + mp_integer max_width = 0; + 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() || *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); +} diff --git a/src/util/std_types.h b/src/util/std_types.h index 02ada334a6f..d83634dea6a 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -400,6 +400,15 @@ class union_typet:public struct_union_typet : struct_union_typet(ID_union, std::move(_components)) { } + + /// 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 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> + find_widest_union_component(const namespacet &ns) const; }; /// Check whether a reference to a typet is a \ref union_typet. From 4acaa86c9fe78bc9d452acab84e409790a88f26a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 13 Aug 2020 14:30:21 +0000 Subject: [PATCH 2/2] Make find_widest_union_component safe for non-constant sizes This should make it safer to use and enables re-use as part of pointer_offset_bits. --- src/util/pointer_offset_size.cpp | 21 +++++++-------------- src/util/std_types.cpp | 11 +++++++---- src/util/std_types.h | 5 ++--- 3 files changed, 16 insertions(+), 21 deletions(-) diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index b40d0d39fd6..ab5877de5bf 100644 --- a/src/util/pointer_offset_size.cpp +++ b/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 || diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index ddd6a97d3b2..62c7c72a3f5 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -294,7 +294,7 @@ union_typet::find_widest_union_component(const namespacet &ns) const { const union_typet::componentst &comps = components(); - mp_integer max_width = 0; + optionalt max_width; typet max_comp_type; irep_idt max_comp_name; @@ -302,7 +302,10 @@ union_typet::find_widest_union_component(const namespacet &ns) const { auto element_width = pointer_offset_bits(comp.type(), ns); - if(!element_width.has_value() || *element_width <= max_width) + if(!element_width.has_value()) + return {}; + + if(max_width.has_value() && *element_width <= *max_width) continue; max_width = *element_width; @@ -310,9 +313,9 @@ union_typet::find_widest_union_component(const namespacet &ns) const max_comp_name = comp.get_name(); } - if(max_width == 0) + if(!max_width.has_value()) return {}; else return std::make_pair( - struct_union_typet::componentt{max_comp_name, max_comp_type}, max_width); + struct_union_typet::componentt{max_comp_name, max_comp_type}, *max_width); } diff --git a/src/util/std_types.h b/src/util/std_types.h index d83634dea6a..8641c0aee72 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -401,9 +401,8 @@ class union_typet:public struct_union_typet { } - /// 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. + /// 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.