Skip to content

Commit c1d59c9

Browse files
authored
Merge pull request diffblue#6664 from tautschnig/cleanup/build_sizeof_expr
Cleanup build_sizeof_expr
2 parents e831f43 + 673bd73 commit c1d59c9

File tree

3 files changed

+48
-51
lines changed

3 files changed

+48
-51
lines changed

src/ansi-c/expr2c.cpp

Lines changed: 48 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1728,6 +1728,52 @@ std::string expr2ct::convert_object_descriptor(
17281728
return result;
17291729
}
17301730

1731+
static optionalt<exprt>
1732+
build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
1733+
{
1734+
const typet &type = static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
1735+
1736+
if(type.is_nil())
1737+
return {};
1738+
1739+
const auto type_size_expr = size_of_expr(type, ns);
1740+
optionalt<mp_integer> type_size;
1741+
if(type_size_expr.has_value())
1742+
type_size = numeric_cast<mp_integer>(*type_size_expr);
1743+
auto val = numeric_cast<mp_integer>(expr);
1744+
1745+
if(
1746+
!type_size.has_value() || *type_size < 0 || !val.has_value() ||
1747+
*val < *type_size || (*type_size == 0 && *val > 0))
1748+
{
1749+
return {};
1750+
}
1751+
1752+
const unsignedbv_typet t(size_type());
1753+
DATA_INVARIANT(
1754+
address_bits(*val + 1) <= t.get_width(),
1755+
"sizeof value does not fit size_type");
1756+
1757+
mp_integer remainder = 0;
1758+
1759+
if(*type_size != 0)
1760+
{
1761+
remainder = *val % *type_size;
1762+
*val -= remainder;
1763+
*val /= *type_size;
1764+
}
1765+
1766+
exprt result(ID_sizeof, t);
1767+
result.set(ID_type_arg, type);
1768+
1769+
if(*val > 1)
1770+
result = mult_exprt(result, from_integer(*val, t));
1771+
if(remainder > 0)
1772+
result = plus_exprt(result, from_integer(remainder, t));
1773+
1774+
return typecast_exprt::conditional_cast(result, expr.type());
1775+
}
1776+
17311777
std::string expr2ct::convert_constant(
17321778
const constant_exprt &src,
17331779
unsigned &precedence)
@@ -1852,11 +1898,9 @@ std::string expr2ct::convert_constant(
18521898
else if(c_type==ID_signed_long_long_int)
18531899
dest+="ll";
18541900

1855-
if(src.find(ID_C_c_sizeof_type).is_not_nil() &&
1856-
sizeof_nesting==0)
1901+
if(sizeof_nesting == 0)
18571902
{
1858-
const auto sizeof_expr_opt =
1859-
build_sizeof_expr(to_constant_expr(src), ns);
1903+
const auto sizeof_expr_opt = build_sizeof_expr(src, ns);
18601904

18611905
if(sizeof_expr_opt.has_value())
18621906
{

src/util/pointer_offset_size.cpp

Lines changed: 0 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -560,50 +560,6 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns)
560560
return {}; // don't know
561561
}
562562

563-
optionalt<exprt>
564-
build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
565-
{
566-
const typet &type=
567-
static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
568-
569-
if(type.is_nil())
570-
return {};
571-
572-
const auto type_size = pointer_offset_size(type, ns);
573-
auto val = numeric_cast<mp_integer>(expr);
574-
575-
if(
576-
!type_size.has_value() || *type_size < 0 || !val.has_value() ||
577-
*val < *type_size || (*type_size == 0 && *val > 0))
578-
{
579-
return {};
580-
}
581-
582-
const typet t(size_type());
583-
DATA_INVARIANT(
584-
address_bits(*val + 1) <= *pointer_offset_bits(t, ns),
585-
"sizeof value does not fit size_type");
586-
587-
mp_integer remainder=0;
588-
589-
if(*type_size != 0)
590-
{
591-
remainder = *val % *type_size;
592-
*val -= remainder;
593-
*val /= *type_size;
594-
}
595-
596-
exprt result(ID_sizeof, t);
597-
result.set(ID_type_arg, type);
598-
599-
if(*val > 1)
600-
result = mult_exprt(result, from_integer(*val, t));
601-
if(remainder>0)
602-
result=plus_exprt(result, from_integer(remainder, t));
603-
604-
return typecast_exprt::conditional_cast(result, expr.type());
605-
}
606-
607563
optionalt<exprt> get_subexpression_at_offset(
608564
const exprt &expr,
609565
const mp_integer &offset_bytes,

src/util/pointer_offset_size.h

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,6 @@ optionalt<exprt> member_offset_expr(
5151

5252
optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns);
5353

54-
optionalt<exprt>
55-
build_sizeof_expr(const constant_exprt &expr, const namespacet &ns);
56-
5754
optionalt<exprt> get_subexpression_at_offset(
5855
const exprt &expr,
5956
const mp_integer &offset,

0 commit comments

Comments
 (0)