From 85d99a4e457bdaa79420579b369ee9fa2b5a40f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 Feb 2022 11:30:27 +0000 Subject: [PATCH 1/2] Move build_sizeof_expr to expr2c expr2c is the only user of a function that does entirely C-frontend-specific work. It constructs a "sizeof" expression in the way the C frontend expects such an expression to look like. --- src/ansi-c/expr2c.cpp | 49 +++++++++++++++++++++++++++++--- src/util/pointer_offset_size.cpp | 44 ---------------------------- src/util/pointer_offset_size.h | 3 -- 3 files changed, 45 insertions(+), 51 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index c5ee73d76bd..565e27b20ca 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1728,6 +1728,49 @@ std::string expr2ct::convert_object_descriptor( return result; } +static optionalt +build_sizeof_expr(const constant_exprt &expr, const namespacet &ns) +{ + const typet &type = static_cast(expr.find(ID_C_c_sizeof_type)); + + if(type.is_nil()) + return {}; + + const auto type_size = pointer_offset_size(type, ns); + auto val = numeric_cast(expr); + + if( + !type_size.has_value() || *type_size < 0 || !val.has_value() || + *val < *type_size || (*type_size == 0 && *val > 0)) + { + return {}; + } + + const typet t(size_type()); + DATA_INVARIANT( + address_bits(*val + 1) <= *pointer_offset_bits(t, ns), + "sizeof value does not fit size_type"); + + mp_integer remainder = 0; + + if(*type_size != 0) + { + remainder = *val % *type_size; + *val -= remainder; + *val /= *type_size; + } + + exprt result(ID_sizeof, t); + result.set(ID_type_arg, type); + + if(*val > 1) + result = mult_exprt(result, from_integer(*val, t)); + if(remainder > 0) + result = plus_exprt(result, from_integer(remainder, t)); + + return typecast_exprt::conditional_cast(result, expr.type()); +} + std::string expr2ct::convert_constant( const constant_exprt &src, unsigned &precedence) @@ -1852,11 +1895,9 @@ std::string expr2ct::convert_constant( else if(c_type==ID_signed_long_long_int) dest+="ll"; - if(src.find(ID_C_c_sizeof_type).is_not_nil() && - sizeof_nesting==0) + if(sizeof_nesting == 0) { - const auto sizeof_expr_opt = - build_sizeof_expr(to_constant_expr(src), ns); + const auto sizeof_expr_opt = build_sizeof_expr(src, ns); if(sizeof_expr_opt.has_value()) { diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 246fbecc3e6..23b688eea44 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -560,50 +560,6 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns) return {}; // don't know } -optionalt -build_sizeof_expr(const constant_exprt &expr, const namespacet &ns) -{ - const typet &type= - static_cast(expr.find(ID_C_c_sizeof_type)); - - if(type.is_nil()) - return {}; - - const auto type_size = pointer_offset_size(type, ns); - auto val = numeric_cast(expr); - - if( - !type_size.has_value() || *type_size < 0 || !val.has_value() || - *val < *type_size || (*type_size == 0 && *val > 0)) - { - return {}; - } - - const typet t(size_type()); - DATA_INVARIANT( - address_bits(*val + 1) <= *pointer_offset_bits(t, ns), - "sizeof value does not fit size_type"); - - mp_integer remainder=0; - - if(*type_size != 0) - { - remainder = *val % *type_size; - *val -= remainder; - *val /= *type_size; - } - - exprt result(ID_sizeof, t); - result.set(ID_type_arg, type); - - if(*val > 1) - result = mult_exprt(result, from_integer(*val, t)); - if(remainder>0) - result=plus_exprt(result, from_integer(remainder, t)); - - return typecast_exprt::conditional_cast(result, expr.type()); -} - optionalt get_subexpression_at_offset( const exprt &expr, const mp_integer &offset_bytes, diff --git a/src/util/pointer_offset_size.h b/src/util/pointer_offset_size.h index f75d0586c39..ac44ac92958 100644 --- a/src/util/pointer_offset_size.h +++ b/src/util/pointer_offset_size.h @@ -51,9 +51,6 @@ optionalt member_offset_expr( optionalt size_of_expr(const typet &type, const namespacet &ns); -optionalt -build_sizeof_expr(const constant_exprt &expr, const namespacet &ns); - optionalt get_subexpression_at_offset( const exprt &expr, const mp_integer &offset, From 673bd73e43a8f0fb8e9ae8d4d0de7332d921b5fa Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 Feb 2022 11:33:02 +0000 Subject: [PATCH 2/2] Cleanup build_sizeof_expr Make sure we use any peculiar properties of "sizeof" that size_of_expr will make sure to handle: pointer_offset_size performs size computation using the runtime size, and not C-frontend specific oddities. --- src/ansi-c/expr2c.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 565e27b20ca..b8216d9b163 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1736,7 +1736,10 @@ build_sizeof_expr(const constant_exprt &expr, const namespacet &ns) if(type.is_nil()) return {}; - const auto type_size = pointer_offset_size(type, ns); + const auto type_size_expr = size_of_expr(type, ns); + optionalt type_size; + if(type_size_expr.has_value()) + type_size = numeric_cast(*type_size_expr); auto val = numeric_cast(expr); if( @@ -1746,9 +1749,9 @@ build_sizeof_expr(const constant_exprt &expr, const namespacet &ns) return {}; } - const typet t(size_type()); + const unsignedbv_typet t(size_type()); DATA_INVARIANT( - address_bits(*val + 1) <= *pointer_offset_bits(t, ns), + address_bits(*val + 1) <= t.get_width(), "sizeof value does not fit size_type"); mp_integer remainder = 0;