Skip to content

Commit 3ed1438

Browse files
committed
introduce pointer_object_exprt
This introduces a class for an expression that is already in use, i.e., merely documenting it.
1 parent a290617 commit 3ed1438

File tree

9 files changed

+74
-13
lines changed

9 files changed

+74
-13
lines changed

src/goto-instrument/contracts/instrument_spec_assigns.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -468,7 +468,7 @@ car_exprt instrument_spec_assignst::create_car_expr(
468468

469469
if(target.id() == ID_pointer_object)
470470
{
471-
const auto &arg = to_unary_expr(target).op();
471+
const auto &arg = to_pointer_object_expr(target).pointer();
472472
return {
473473
condition,
474474
target,

src/goto-instrument/contracts/utils.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,8 @@ void havoc_assigns_targetst::append_havoc_code_for_expr(
6969
{
7070
if(expr.id() == ID_pointer_object)
7171
{
72-
append_object_havoc_code_for_expr(location, expr.operands().front(), dest);
72+
append_object_havoc_code_for_expr(
73+
location, to_pointer_object_expr(expr).pointer(), dest);
7374
return;
7475
}
7576

src/solvers/flattening/bv_pointers.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -713,17 +713,18 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
713713
}
714714
else if(
715715
expr.id() == ID_pointer_object &&
716-
to_unary_expr(expr).op().type().id() == ID_pointer)
716+
to_pointer_object_expr(expr).pointer().type().id() == ID_pointer)
717717
{
718718
std::size_t width=boolbv_width(expr.type());
719719

720720
if(width==0)
721721
return conversion_failed(expr);
722722

723-
const exprt &op0 = to_unary_expr(expr).op();
724-
const bvt &op0_bv = convert_bv(op0);
723+
const exprt &pointer = to_pointer_object_expr(expr).pointer();
724+
const bvt &pointer_bv = convert_bv(pointer);
725725

726-
bvt object_bv = object_literals(op0_bv, to_pointer_type(op0.type()));
726+
bvt object_bv =
727+
object_literals(pointer_bv, to_pointer_type(pointer.type()));
727728

728729
return bv_utils.zero_extension(object_bv, width);
729730
}

src/solvers/smt2/smt2_conv.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1589,7 +1589,7 @@ void smt2_convt::convert_expr(const exprt &expr)
15891589
}
15901590
else if(expr.id()==ID_pointer_object)
15911591
{
1592-
const auto &op = to_unary_expr(expr).op();
1592+
const auto &op = to_pointer_object_expr(expr).pointer();
15931593

15941594
DATA_INVARIANT(
15951595
op.type().id() == ID_pointer,

src/util/pointer_expr.h

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -931,4 +931,62 @@ inline pointer_offset_exprt &to_pointer_offset_expr(exprt &expr)
931931
return ret;
932932
}
933933

934+
/// A numerical identifier for the object a pointer points to
935+
class pointer_object_exprt : public unary_exprt
936+
{
937+
public:
938+
explicit pointer_object_exprt(exprt pointer, typet type)
939+
: unary_exprt(ID_pointer_object, std::move(pointer), std::move(type))
940+
{
941+
}
942+
943+
exprt &pointer()
944+
{
945+
return op0();
946+
}
947+
948+
const exprt &pointer() const
949+
{
950+
return op0();
951+
}
952+
};
953+
954+
template <>
955+
inline bool can_cast_expr<pointer_object_exprt>(const exprt &base)
956+
{
957+
return base.id() == ID_pointer_object;
958+
}
959+
960+
inline void validate_expr(const pointer_object_exprt &value)
961+
{
962+
validate_operands(value, 1, "pointer_object must have one operand");
963+
DATA_INVARIANT(
964+
value.pointer().type().id() == ID_pointer,
965+
"pointer_object must have pointer-typed operand");
966+
}
967+
968+
/// \brief Cast an exprt to a \ref pointer_object_exprt
969+
///
970+
/// \a expr must be known to be \ref pointer_object_exprt.
971+
///
972+
/// \param expr: Source expression
973+
/// \return Object of type \ref pointer_object_exprt
974+
inline const pointer_object_exprt &to_pointer_object_expr(const exprt &expr)
975+
{
976+
PRECONDITION(expr.id() == ID_pointer_object);
977+
const pointer_object_exprt &ret =
978+
static_cast<const pointer_object_exprt &>(expr);
979+
validate_expr(ret);
980+
return ret;
981+
}
982+
983+
/// \copydoc to_pointer_object_expr(const exprt &)
984+
inline pointer_object_exprt &to_pointer_object_expr(exprt &expr)
985+
{
986+
PRECONDITION(expr.id() == ID_pointer_object);
987+
pointer_object_exprt &ret = static_cast<pointer_object_exprt &>(expr);
988+
validate_expr(ret);
989+
return ret;
990+
}
991+
934992
#endif // CPROVER_UTIL_POINTER_EXPR_H

src/util/pointer_predicates.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ Author: Daniel Kroening, [email protected]
2222

2323
exprt pointer_object(const exprt &p)
2424
{
25-
return unary_exprt(ID_pointer_object, p, size_type());
25+
return pointer_object_exprt(p, size_type());
2626
}
2727

2828
exprt same_object(const exprt &p1, const exprt &p2)

src/util/simplify_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2388,7 +2388,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
23882388
}
23892389
else if(expr.id()==ID_pointer_object)
23902390
{
2391-
r = simplify_pointer_object(to_unary_expr(expr));
2391+
r = simplify_pointer_object(to_pointer_object_expr(expr));
23922392
}
23932393
else if(expr.id() == ID_is_dynamic_object)
23942394
{

src/util/simplify_expr_class.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,7 @@ class mult_exprt;
5959
class namespacet;
6060
class not_exprt;
6161
class plus_exprt;
62+
class pointer_object_exprt;
6263
class pointer_offset_exprt;
6364
class popcount_exprt;
6465
class refined_string_exprt;
@@ -171,7 +172,7 @@ class simplify_exprt
171172
NODISCARD resultt<> simplify_member(const member_exprt &);
172173
NODISCARD resultt<> simplify_byte_update(const byte_update_exprt &);
173174
NODISCARD resultt<> simplify_byte_extract(const byte_extract_exprt &);
174-
NODISCARD resultt<> simplify_pointer_object(const unary_exprt &);
175+
NODISCARD resultt<> simplify_pointer_object(const pointer_object_exprt &);
175176
NODISCARD resultt<> simplify_object_size(const unary_exprt &);
176177
NODISCARD resultt<> simplify_is_dynamic_object(const unary_exprt &);
177178
NODISCARD resultt<> simplify_is_invalid_pointer(const unary_exprt &);

src/util/simplify_expr_pointer.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -481,7 +481,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_pointer_object(
481481
forall_operands(it, expr)
482482
{
483483
PRECONDITION(it->id() == ID_pointer_object);
484-
const exprt &op = to_unary_expr(*it).op();
484+
const exprt &op = to_pointer_object_expr(*it).pointer();
485485

486486
if(op.id()==ID_address_of)
487487
{
@@ -516,9 +516,9 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_pointer_object(
516516
}
517517

518518
simplify_exprt::resultt<>
519-
simplify_exprt::simplify_pointer_object(const unary_exprt &expr)
519+
simplify_exprt::simplify_pointer_object(const pointer_object_exprt &expr)
520520
{
521-
const exprt &op = expr.op();
521+
const exprt &op = expr.pointer();
522522

523523
auto op_result = simplify_object(op);
524524

0 commit comments

Comments
 (0)