Skip to content

Commit a290617

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

File tree

10 files changed

+78
-21
lines changed

10 files changed

+78
-21
lines changed

src/goto-instrument/accelerate/acceleration_utils.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1057,7 +1057,7 @@ bool acceleration_utilst::assign_array(
10571057
{
10581058
if(idx.id()==ID_pointer_offset)
10591059
{
1060-
poly.from_expr(to_unary_expr(idx).op());
1060+
poly.from_expr(to_pointer_offset_expr(idx).pointer());
10611061
}
10621062
else
10631063
{

src/goto-programs/interpreter_evaluate.cpp

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -779,13 +779,10 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
779779
}
780780
else if(expr.id()==ID_pointer_offset)
781781
{
782-
if(expr.operands().size()!=1)
783-
throw "pointer_offset expects one operand";
784-
785-
if(to_unary_expr(expr).op().type().id() != ID_pointer)
782+
if(to_pointer_offset_expr(expr).op().type().id() != ID_pointer)
786783
throw "pointer_offset expects a pointer operand";
787784

788-
mp_vectort result = evaluate(to_unary_expr(expr).op());
785+
mp_vectort result = evaluate(to_pointer_offset_expr(expr).op());
789786

790787
if(result.size()==1)
791788
{

src/pointer-analysis/value_set.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -309,7 +309,7 @@ bool value_sett::eval_pointer_offset(
309309
if(expr.id()==ID_pointer_offset)
310310
{
311311
const object_mapt reference_set =
312-
get_value_set(to_unary_expr(expr).op(), ns, true);
312+
get_value_set(to_pointer_offset_expr(expr).pointer(), ns, true);
313313

314314
exprt new_expr;
315315
mp_integer previous_offset=0;

src/solvers/flattening/bv_pointers.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -683,17 +683,18 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
683683
}
684684
else if(
685685
expr.id() == ID_pointer_offset &&
686-
to_unary_expr(expr).op().type().id() == ID_pointer)
686+
to_pointer_offset_expr(expr).pointer().type().id() == ID_pointer)
687687
{
688688
std::size_t width=boolbv_width(expr.type());
689689

690690
if(width==0)
691691
return conversion_failed(expr);
692692

693-
const exprt &op0 = to_unary_expr(expr).op();
694-
const bvt &op0_bv = convert_bv(op0);
693+
const exprt &pointer = to_pointer_offset_expr(expr).pointer();
694+
const bvt &pointer_bv = convert_bv(pointer);
695695

696-
bvt offset_bv = offset_literals(op0_bv, to_pointer_type(op0.type()));
696+
bvt offset_bv =
697+
offset_literals(pointer_bv, to_pointer_type(pointer.type()));
697698

698699
// we do a sign extension to permit negative offsets
699700
return bv_utils.sign_extension(offset_bv, width);

src/solvers/smt2/smt2_conv.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1562,7 +1562,7 @@ void smt2_convt::convert_expr(const exprt &expr)
15621562
}
15631563
else if(expr.id()==ID_pointer_offset)
15641564
{
1565-
const auto &op = to_unary_expr(expr).op();
1565+
const auto &op = to_pointer_offset_expr(expr).pointer();
15661566

15671567
DATA_INVARIANT(
15681568
op.type().id() == ID_pointer,

src/util/pointer_expr.h

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -873,4 +873,62 @@ to_annotated_pointer_constant_expr(exprt &expr)
873873
return ret;
874874
}
875875

876+
/// The offset (in bytes) of a pointer relative to the object
877+
class pointer_offset_exprt : public unary_exprt
878+
{
879+
public:
880+
explicit pointer_offset_exprt(exprt pointer, typet type)
881+
: unary_exprt(ID_pointer_offset, std::move(pointer), std::move(type))
882+
{
883+
}
884+
885+
exprt &pointer()
886+
{
887+
return op0();
888+
}
889+
890+
const exprt &pointer() const
891+
{
892+
return op0();
893+
}
894+
};
895+
896+
template <>
897+
inline bool can_cast_expr<pointer_offset_exprt>(const exprt &base)
898+
{
899+
return base.id() == ID_pointer_offset;
900+
}
901+
902+
inline void validate_expr(const pointer_offset_exprt &value)
903+
{
904+
validate_operands(value, 1, "pointer_offset must have one operand");
905+
DATA_INVARIANT(
906+
value.pointer().type().id() == ID_pointer,
907+
"pointer_offset must have pointer-typed operand");
908+
}
909+
910+
/// \brief Cast an exprt to a \ref pointer_offset_exprt
911+
///
912+
/// \a expr must be known to be \ref pointer_offset_exprt.
913+
///
914+
/// \param expr: Source expression
915+
/// \return Object of type \ref pointer_offset_exprt
916+
inline const pointer_offset_exprt &to_pointer_offset_expr(const exprt &expr)
917+
{
918+
PRECONDITION(expr.id() == ID_pointer_offset);
919+
const pointer_offset_exprt &ret =
920+
static_cast<const pointer_offset_exprt &>(expr);
921+
validate_expr(ret);
922+
return ret;
923+
}
924+
925+
/// \copydoc to_pointer_offset_expr(const exprt &)
926+
inline pointer_offset_exprt &to_pointer_offset_expr(exprt &expr)
927+
{
928+
PRECONDITION(expr.id() == ID_pointer_offset);
929+
pointer_offset_exprt &ret = static_cast<pointer_offset_exprt &>(expr);
930+
validate_expr(ret);
931+
return ret;
932+
}
933+
876934
#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
@@ -37,7 +37,7 @@ exprt object_size(const exprt &pointer)
3737

3838
exprt pointer_offset(const exprt &pointer)
3939
{
40-
return unary_exprt(ID_pointer_offset, pointer, signed_size_type());
40+
return pointer_offset_exprt(pointer, signed_size_type());
4141
}
4242

4343
exprt deallocated(const exprt &pointer, const namespacet &ns)

src/util/simplify_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2483,7 +2483,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
24832483
}
24842484
else if(expr.id()==ID_pointer_offset)
24852485
{
2486-
r = simplify_pointer_offset(to_unary_expr(expr));
2486+
r = simplify_pointer_offset(to_pointer_offset_expr(expr));
24872487
}
24882488
else if(expr.id()==ID_extractbit)
24892489
{

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_offset_exprt;
6263
class popcount_exprt;
6364
class refined_string_exprt;
6465
class shift_exprt;
@@ -180,7 +181,7 @@ class simplify_exprt
180181
NODISCARD resultt<> simplify_unary_plus(const unary_plus_exprt &);
181182
NODISCARD resultt<> simplify_dereference(const dereference_exprt &);
182183
NODISCARD resultt<> simplify_address_of(const address_of_exprt &);
183-
NODISCARD resultt<> simplify_pointer_offset(const unary_exprt &);
184+
NODISCARD resultt<> simplify_pointer_offset(const pointer_offset_exprt &);
184185
NODISCARD resultt<> simplify_bswap(const bswap_exprt &);
185186
NODISCARD resultt<> simplify_isinf(const unary_exprt &);
186187
NODISCARD resultt<> simplify_isnan(const unary_exprt &);

src/util/simplify_expr_pointer.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -245,17 +245,17 @@ simplify_exprt::simplify_address_of(const address_of_exprt &expr)
245245
}
246246

247247
simplify_exprt::resultt<>
248-
simplify_exprt::simplify_pointer_offset(const unary_exprt &expr)
248+
simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr)
249249
{
250-
const exprt &ptr = expr.op();
250+
const exprt &ptr = expr.pointer();
251251

252252
if(ptr.id()==ID_if && ptr.operands().size()==3)
253253
{
254254
if_exprt if_expr=lift_if(expr, 0);
255255
if_expr.true_case() =
256-
simplify_pointer_offset(to_unary_expr(if_expr.true_case()));
256+
simplify_pointer_offset(to_pointer_offset_expr(if_expr.true_case()));
257257
if_expr.false_case() =
258-
simplify_pointer_offset(to_unary_expr(if_expr.false_case()));
258+
simplify_pointer_offset(to_pointer_offset_expr(if_expr.false_case()));
259259
return changed(simplify_if(if_expr));
260260
}
261261

@@ -358,8 +358,8 @@ simplify_exprt::simplify_pointer_offset(const unary_exprt &expr)
358358
return unchanged(expr);
359359

360360
// this might change the type of the pointer!
361-
exprt pointer_offset_expr =
362-
simplify_pointer_offset(to_unary_expr(pointer_offset(ptr_expr.front())));
361+
exprt pointer_offset_expr = simplify_pointer_offset(
362+
to_pointer_offset_expr(pointer_offset(ptr_expr.front())));
363363

364364
exprt sum;
365365

0 commit comments

Comments
 (0)