Skip to content

Commit 29799b4

Browse files
authored
Merge pull request #6715 from diffblue/address_expressions
Fixes for address expressions
2 parents 633790b + 06075c0 commit 29799b4

File tree

3 files changed

+53
-53
lines changed

3 files changed

+53
-53
lines changed

src/solvers/flattening/bv_pointers.cpp

Lines changed: 45 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -539,6 +539,51 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
539539
{
540540
return SUB::convert_byte_update(to_byte_update_expr(expr));
541541
}
542+
else if(expr.id() == ID_field_address)
543+
{
544+
const auto &field_address_expr = to_field_address_expr(expr);
545+
const typet &compound_type = ns.follow(field_address_expr.compound_type());
546+
547+
// recursive call
548+
auto bv = convert_bitvector(field_address_expr.base());
549+
550+
if(compound_type.id() == ID_struct)
551+
{
552+
auto offset = member_offset(
553+
to_struct_type(compound_type), field_address_expr.component_name(), ns);
554+
CHECK_RETURN(offset.has_value());
555+
556+
// add offset
557+
bv = offset_arithmetic(field_address_expr.type(), bv, *offset);
558+
}
559+
else if(compound_type.id() == ID_union)
560+
{
561+
// nothing to do, all fields have offset 0
562+
}
563+
else
564+
{
565+
INVARIANT(false, "field address expressions operate on struct or union");
566+
}
567+
568+
return bv;
569+
}
570+
else if(expr.id() == ID_element_address)
571+
{
572+
const auto &element_address_expr = to_element_address_expr(expr);
573+
574+
// recursive call
575+
auto bv = convert_bitvector(element_address_expr.base());
576+
577+
// get element size
578+
auto size = pointer_offset_size(element_address_expr.element_type(), ns);
579+
CHECK_RETURN(size.has_value() && *size >= 0);
580+
581+
// add offset
582+
bv = offset_arithmetic(
583+
element_address_expr.type(), bv, *size, element_address_expr.index());
584+
585+
return bv;
586+
}
542587

543588
return conversion_failed(expr);
544589
}
@@ -702,51 +747,6 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
702747
const auto &object_address_expr = to_object_address_expr(expr);
703748
return add_addr(object_address_expr.object_expr());
704749
}
705-
else if(expr.id() == ID_field_address)
706-
{
707-
const auto &field_address_expr = to_field_address_expr(expr);
708-
const typet &compound_type = ns.follow(field_address_expr.compound_type());
709-
710-
// recursive call
711-
auto bv = convert_bitvector(field_address_expr.base());
712-
713-
if(compound_type.id() == ID_struct)
714-
{
715-
auto offset = member_offset(
716-
to_struct_type(compound_type), field_address_expr.component_name(), ns);
717-
CHECK_RETURN(offset.has_value());
718-
719-
// add offset
720-
bv = offset_arithmetic(field_address_expr.type(), bv, *offset);
721-
}
722-
else if(compound_type.id() == ID_union)
723-
{
724-
// nothing to do, all fields have offset 0
725-
}
726-
else
727-
{
728-
INVARIANT(false, "field address expressions operate on struct or union");
729-
}
730-
731-
return bv;
732-
}
733-
else if(expr.id() == ID_element_address)
734-
{
735-
const auto &element_address_expr = to_element_address_expr(expr);
736-
737-
// recursive call
738-
auto bv = convert_bitvector(element_address_expr.base());
739-
740-
// get element size
741-
auto size = pointer_offset_size(element_address_expr.element_type(), ns);
742-
CHECK_RETURN(size.has_value() && *size >= 0);
743-
744-
// add offset
745-
bv = offset_arithmetic(
746-
element_address_expr.type(), bv, *size, element_address_expr.index());
747-
748-
return bv;
749-
}
750750

751751
return SUB::convert_bitvector(expr);
752752
}

src/util/pointer_expr.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -138,22 +138,22 @@ field_address_exprt::field_address_exprt(
138138
pointer_typet _type)
139139
: unary_exprt(ID_field_address, std::move(compound_ptr), std::move(_type))
140140
{
141-
const auto &compound_ptr_type = compound_ptr.type();
142-
PRECONDITION(compound_ptr_type.id() == ID_pointer);
143-
const auto &compound_type = to_pointer_type(compound_ptr_type).base_type();
141+
const auto &base_type = field_address_exprt::base().type();
142+
PRECONDITION(base_type.id() == ID_pointer);
143+
const auto &compound_type = to_pointer_type(base_type).base_type();
144144
PRECONDITION(
145145
compound_type.id() == ID_struct || compound_type.id() == ID_struct_tag ||
146146
compound_type.id() == ID_union || compound_type.id() == ID_union_tag);
147147
set(ID_component_name, component_name);
148148
}
149149

150-
element_address_exprt::element_address_exprt(exprt base, exprt index)
150+
element_address_exprt::element_address_exprt(const exprt &base, exprt index)
151151
: binary_exprt(
152-
std::move(base),
152+
base,
153153
ID_element_address,
154154
std::move(index),
155155
pointer_typet(
156-
to_array_type(base.type()).element_type(),
156+
to_pointer_type(base.type()).base_type(),
157157
to_pointer_type(base.type()).get_width()))
158158
{
159159
}

src/util/pointer_expr.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -450,7 +450,7 @@ inline bool can_cast_expr<object_address_exprt>(const exprt &base)
450450

451451
inline void validate_expr(const object_address_exprt &value)
452452
{
453-
validate_operands(value, 1, "object_address must have one operand");
453+
validate_operands(value, 0, "object_address must have zero operands");
454454
}
455455

456456
/// \brief Cast an exprt to an \ref object_address_exprt
@@ -569,7 +569,7 @@ class element_address_exprt : public binary_exprt
569569
/// constructor for element addresses.
570570
/// The base address must be a pointer to an element.
571571
/// The index is expected to have an integer type.
572-
element_address_exprt(exprt base, exprt index);
572+
element_address_exprt(const exprt &base, exprt index);
573573

574574
const pointer_typet &type() const
575575
{

0 commit comments

Comments
 (0)