Skip to content

Commit 2eea327

Browse files
committed
introduce field_address_exprt and element_address_exprt
This commit introduces three new expressions, which fix the largest asymmetry in the expression system: expressions that denote pointers to objects. The first expression is the base constructor: it returns the address of an object with a given identifier. It is semantically equivalent to the existing address_of expression with a symbol subexpression. The next two expressions both take a base address, and then add to it the offset (in char units) of either a named struct field or an array element (given by its index). They are semantically equivalent to but much more concise and readable than the equivalent combination of typecasts and pointer arithmetic. They key benefit is that algorithms that iterate over expressions no longer need to special case the sub-expressions of address_of expressions.
1 parent c41ce2b commit 2eea327

File tree

3 files changed

+271
-0
lines changed

3 files changed

+271
-0
lines changed

src/util/irep_ids.def

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -188,6 +188,9 @@ IREP_ID_TWO(C_rvalue_reference, #rvalue_reference)
188188
IREP_ID_ONE(true)
189189
IREP_ID_ONE(false)
190190
IREP_ID_ONE(address_of)
191+
IREP_ID_ONE(object_address)
192+
IREP_ID_ONE(field_address)
193+
IREP_ID_ONE(element_address)
191194
IREP_ID_ONE(dereference)
192195
IREP_ID_TWO(C_lvalue, #lvalue)
193196
IREP_ID_TWO(C_base, #base)

src/util/pointer_expr.cpp

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -122,6 +122,43 @@ address_of_exprt::address_of_exprt(const exprt &_op)
122122
{
123123
}
124124

125+
object_address_exprt::object_address_exprt(const symbol_exprt &object)
126+
: nullary_exprt(ID_object_address, pointer_type(object.type()))
127+
{
128+
set(ID_identifier, object.get_identifier());
129+
}
130+
131+
symbol_exprt object_address_exprt::object_expr() const
132+
{
133+
return symbol_exprt(object_identifier(), to_pointer_type(type()).subtype());
134+
}
135+
136+
field_address_exprt::field_address_exprt(
137+
exprt base,
138+
const irep_idt &component_name,
139+
pointer_typet _type)
140+
: unary_exprt(ID_field_address, std::move(base), std::move(_type))
141+
{
142+
const auto &base_type = base.type();
143+
PRECONDITION(base_type.id() == ID_pointer);
144+
const auto &base_sub_type = base_type.subtype();
145+
PRECONDITION(
146+
base_sub_type.id() == ID_struct || base_sub_type.id() == ID_struct_tag ||
147+
base_sub_type.id() == ID_union || base_sub_type.id() == ID_union_tag);
148+
set(ID_component_name, component_name);
149+
}
150+
151+
element_address_exprt::element_address_exprt(exprt base, exprt index)
152+
: binary_exprt(
153+
std::move(base),
154+
ID_element_address,
155+
std::move(index),
156+
pointer_typet(
157+
to_array_type(base.type()).subtype(),
158+
to_pointer_type(base.type()).get_width()))
159+
{
160+
}
161+
125162
const exprt &object_descriptor_exprt::root_object(const exprt &expr)
126163
{
127164
const exprt *p = &expr;

src/util/pointer_expr.h

Lines changed: 231 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -381,6 +381,237 @@ inline address_of_exprt &to_address_of_expr(exprt &expr)
381381
return ret;
382382
}
383383

384+
/// \brief Operator to return the address of an object
385+
class object_address_exprt : public nullary_exprt
386+
{
387+
public:
388+
explicit object_address_exprt(const symbol_exprt &);
389+
390+
irep_idt object_identifier() const
391+
{
392+
return get(ID_identifier);
393+
}
394+
395+
const pointer_typet &type() const
396+
{
397+
return static_cast<const pointer_typet &>(exprt::type());
398+
}
399+
400+
pointer_typet &type()
401+
{
402+
return static_cast<pointer_typet &>(exprt::type());
403+
}
404+
405+
/// returns the type of the object whose address is represented
406+
const typet &object_type() const
407+
{
408+
return type().subtype();
409+
}
410+
411+
symbol_exprt object_expr() const;
412+
};
413+
414+
template <>
415+
inline bool can_cast_expr<object_address_exprt>(const exprt &base)
416+
{
417+
return base.id() == ID_object_address;
418+
}
419+
420+
inline void validate_expr(const object_address_exprt &value)
421+
{
422+
validate_operands(value, 1, "object_address must have one operand");
423+
}
424+
425+
/// \brief Cast an exprt to an \ref object_address_exprt
426+
///
427+
/// \a expr must be known to be \ref object_address_exprt.
428+
///
429+
/// \param expr: Source expression
430+
/// \return Object of type \ref object_address_exprt
431+
inline const object_address_exprt &to_object_address_expr(const exprt &expr)
432+
{
433+
PRECONDITION(expr.id() == ID_object_address);
434+
const object_address_exprt &ret =
435+
static_cast<const object_address_exprt &>(expr);
436+
validate_expr(ret);
437+
return ret;
438+
}
439+
440+
/// \copydoc to_object_address_expr(const exprt &)
441+
inline object_address_exprt &to_object_address_expr(exprt &expr)
442+
{
443+
PRECONDITION(expr.id() == ID_object_address);
444+
object_address_exprt &ret = static_cast<object_address_exprt &>(expr);
445+
validate_expr(ret);
446+
return ret;
447+
}
448+
449+
/// \brief Operator to return the address of a field relative
450+
/// to a base address
451+
class field_address_exprt : public unary_exprt
452+
{
453+
public:
454+
/// constructor for field addresses.
455+
/// The base address must be a pointer to a compound type.
456+
field_address_exprt(
457+
exprt base,
458+
const irep_idt &component_name,
459+
pointer_typet type);
460+
461+
exprt &base()
462+
{
463+
return op0();
464+
}
465+
466+
const exprt &base() const
467+
{
468+
return op0();
469+
}
470+
471+
const pointer_typet &type() const
472+
{
473+
return static_cast<const pointer_typet &>(exprt::type());
474+
}
475+
476+
pointer_typet &type()
477+
{
478+
return static_cast<pointer_typet &>(exprt::type());
479+
}
480+
481+
/// returns the type of the field whose address is represented
482+
const typet &field_type() const
483+
{
484+
return type().subtype();
485+
}
486+
487+
const typet &compound_type() const
488+
{
489+
return to_pointer_type(base().type()).subtype();
490+
}
491+
492+
const irep_idt &component_name() const
493+
{
494+
return get(ID_component_name);
495+
}
496+
};
497+
498+
template <>
499+
inline bool can_cast_expr<field_address_exprt>(const exprt &expr)
500+
{
501+
return expr.id() == ID_field_address;
502+
}
503+
504+
inline void validate_expr(const field_address_exprt &value)
505+
{
506+
validate_operands(value, 1, "field_address must have one operand");
507+
}
508+
509+
/// \brief Cast an exprt to an \ref field_address_exprt
510+
///
511+
/// \a expr must be known to be \ref field_address_exprt.
512+
///
513+
/// \param expr: Source expression
514+
/// \return Object of type \ref field_address_exprt
515+
inline const field_address_exprt &to_field_address_expr(const exprt &expr)
516+
{
517+
PRECONDITION(expr.id() == ID_field_address);
518+
const field_address_exprt &ret =
519+
static_cast<const field_address_exprt &>(expr);
520+
validate_expr(ret);
521+
return ret;
522+
}
523+
524+
/// \copydoc to_field_address_expr(const exprt &)
525+
inline field_address_exprt &to_field_address_expr(exprt &expr)
526+
{
527+
PRECONDITION(expr.id() == ID_field_address);
528+
field_address_exprt &ret = static_cast<field_address_exprt &>(expr);
529+
validate_expr(ret);
530+
return ret;
531+
}
532+
533+
/// \brief Operator to return the address of an array element
534+
/// relative to a base address
535+
class element_address_exprt : public binary_exprt
536+
{
537+
public:
538+
/// constructor for element addresses.
539+
/// The base address must be a pointer to an element.
540+
/// The index is expected to have an integer type.
541+
element_address_exprt(exprt base, exprt index);
542+
543+
const pointer_typet &type() const
544+
{
545+
return static_cast<const pointer_typet &>(exprt::type());
546+
}
547+
548+
pointer_typet &type()
549+
{
550+
return static_cast<pointer_typet &>(exprt::type());
551+
}
552+
553+
/// returns the type of the array element whose address is represented
554+
const typet &element_type() const
555+
{
556+
return type().subtype();
557+
}
558+
559+
exprt &base()
560+
{
561+
return op0();
562+
}
563+
564+
const exprt &base() const
565+
{
566+
return op0();
567+
}
568+
569+
exprt &index()
570+
{
571+
return op1();
572+
}
573+
574+
const exprt &index() const
575+
{
576+
return op1();
577+
}
578+
};
579+
580+
template <>
581+
inline bool can_cast_expr<element_address_exprt>(const exprt &expr)
582+
{
583+
return expr.id() == ID_element_address;
584+
}
585+
586+
inline void validate_expr(const element_address_exprt &value)
587+
{
588+
validate_operands(value, 2, "element_address must have two operands");
589+
}
590+
591+
/// \brief Cast an exprt to an \ref element_address_exprt
592+
///
593+
/// \a expr must be known to be \ref element_address_exprt.
594+
///
595+
/// \param expr: Source expression
596+
/// \return Object of type \ref element_address_exprt
597+
inline const element_address_exprt &to_element_address_expr(const exprt &expr)
598+
{
599+
PRECONDITION(expr.id() == ID_element_address);
600+
const element_address_exprt &ret =
601+
static_cast<const element_address_exprt &>(expr);
602+
validate_expr(ret);
603+
return ret;
604+
}
605+
606+
/// \copydoc to_element_address_expr(const exprt &)
607+
inline element_address_exprt &to_element_address_expr(exprt &expr)
608+
{
609+
PRECONDITION(expr.id() == ID_element_address);
610+
element_address_exprt &ret = static_cast<element_address_exprt &>(expr);
611+
validate_expr(ret);
612+
return ret;
613+
}
614+
384615
/// \brief Operator to dereference a pointer
385616
class dereference_exprt : public unary_exprt
386617
{

0 commit comments

Comments
 (0)