Skip to content

Commit e7d8209

Browse files
tautschnigtautschnig
committed
make_byte_{extract,update} to build byte_{extract,update} expressions
Remove byte_{extract,update}_id from the API (marking them static) and instead add factory functions make_byte_{extract,update} to construct the full expression. These functions will ensure that both endianness and byte width are consistently configured.
1 parent 4a7b064 commit e7d8209

15 files changed

+80
-79
lines changed

‎src/ansi-c/c_typecheck_initializer.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -542,8 +542,8 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
542542

543543
if(current_symbol.is_static_lifetime)
544544
{
545-
byte_update_exprt byte_update{
546-
byte_update_id(), *dest, from_integer(0, index_type()), *zero};
545+
byte_update_exprt byte_update =
546+
make_byte_update(*dest, from_integer(0, index_type()), *zero);
547547
byte_update.add_source_location() = value.source_location();
548548
*dest = std::move(byte_update);
549549
dest = &(to_byte_update_expr(*dest).op2());

‎src/goto-programs/rewrite_union.cpp

+2-5
Original file line numberDiff line numberDiff line change
@@ -84,18 +84,15 @@ void rewrite_union(exprt &expr)
8484
if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
8585
{
8686
exprt offset=from_integer(0, index_type());
87-
byte_extract_exprt tmp(byte_extract_id(), op, offset, expr.type());
88-
expr=tmp;
87+
expr = make_byte_extract(op, offset, expr.type());
8988
}
9089
}
9190
else if(expr.id()==ID_union)
9291
{
9392
const union_exprt &union_expr=to_union_expr(expr);
9493
exprt offset=from_integer(0, index_type());
9594
side_effect_expr_nondett nondet(expr.type(), expr.source_location());
96-
byte_update_exprt tmp(
97-
byte_update_id(), nondet, offset, union_expr.op());
98-
expr=tmp;
95+
expr = make_byte_update(nondet, offset, union_expr.op());
9996
}
10097
}
10198

‎src/goto-symex/symex_clean_expr.cpp

+3-10
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
4242

4343
if(if_expr.true_case() != if_expr.false_case())
4444
{
45-
byte_extract_exprt be(
46-
byte_extract_id(),
45+
byte_extract_exprt be = make_byte_extract(
4746
if_expr.false_case(),
4847
from_integer(0, index_type()),
4948
if_expr.true_case().type());
@@ -91,8 +90,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
9190
CHECK_RETURN(array_size.has_value());
9291
if(do_simplify)
9392
simplify(array_size.value(), ns);
94-
expr = byte_extract_exprt(
95-
byte_extract_id(),
93+
expr = make_byte_extract(
9694
expr,
9795
from_integer(0, index_type()),
9896
array_typet(char_type(), array_size.value()));
@@ -123,12 +121,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
123121

124122
array_typet new_array_type(subtype, new_size);
125123

126-
expr =
127-
byte_extract_exprt(
128-
byte_extract_id(),
129-
expr,
130-
ode.offset(),
131-
new_array_type);
124+
expr = make_byte_extract(expr, ode.offset(), new_array_type);
132125
}
133126
}
134127
}

‎src/goto-symex/symex_dereference.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -95,8 +95,8 @@ exprt goto_symext::address_arithmetic(
9595
object_descriptor_exprt ode;
9696
ode.build(expr, ns);
9797

98-
const byte_extract_exprt be(
99-
byte_extract_id(), ode.root_object(), ode.offset(), expr.type());
98+
const byte_extract_exprt be =
99+
make_byte_extract(ode.root_object(), ode.offset(), expr.type());
100100

101101
// recursive call
102102
result = address_arithmetic(be, state, keep_array);
@@ -151,8 +151,7 @@ exprt goto_symext::address_arithmetic(
151151

152152
if(offset>0)
153153
{
154-
const byte_extract_exprt be(
155-
byte_extract_id(),
154+
const byte_extract_exprt be = make_byte_extract(
156155
to_ssa_expr(expr).get_l1_object(),
157156
from_integer(offset, index_type()),
158157
expr.type());

‎src/goto-symex/symex_function_call.cpp

+3-7
Original file line numberDiff line numberDiff line change
@@ -107,15 +107,11 @@ void goto_symext::parameter_assignments(
107107
rhs_type.id() == ID_pointer ||
108108
rhs_type.id() == ID_union ||
109109
rhs_type.id() == ID_union_tag))
110+
// clang-format on
110111
{
111-
rhs=
112-
byte_extract_exprt(
113-
byte_extract_id(),
114-
rhs,
115-
from_integer(0, index_type()),
116-
parameter_type);
112+
rhs = make_byte_extract(
113+
rhs, from_integer(0, index_type()), parameter_type);
117114
}
118-
// clang-format on
119115
else
120116
{
121117
std::ostringstream error;

‎src/goto-symex/symex_other.cpp

+5-14
Original file line numberDiff line numberDiff line change
@@ -144,23 +144,15 @@ void goto_symext::symex_other(
144144
{
145145
if(statement==ID_array_copy)
146146
{
147-
byte_extract_exprt be(
148-
byte_extract_id(),
149-
src_array,
150-
from_integer(0, index_type()),
151-
dest_array.type());
152-
src_array.swap(be);
147+
src_array = make_byte_extract(
148+
src_array, from_integer(0, index_type()), dest_array.type());
153149
do_simplify(src_array);
154150
}
155151
else
156152
{
157153
// ID_array_replace
158-
byte_extract_exprt be(
159-
byte_extract_id(),
160-
dest_array,
161-
from_integer(0, index_type()),
162-
src_array.type());
163-
dest_array.swap(be);
154+
dest_array = make_byte_extract(
155+
dest_array, from_integer(0, index_type()), src_array.type());
164156
do_simplify(dest_array);
165157
}
166158
}
@@ -196,8 +188,7 @@ void goto_symext::symex_other(
196188
auto array_size = size_of_expr(array_expr.type(), ns);
197189
CHECK_RETURN(array_size.has_value());
198190
do_simplify(array_size.value());
199-
array_expr = byte_extract_exprt(
200-
byte_extract_id(),
191+
array_expr = make_byte_extract(
201192
array_expr,
202193
from_integer(0, index_type()),
203194
array_typet(char_type(), array_size.value()));

‎src/pointer-analysis/value_set_dereference.cpp

+7-7
Original file line numberDiff line numberDiff line change
@@ -530,11 +530,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
530530
}
531531
else
532532
{
533-
result.value = byte_extract_exprt(
534-
byte_extract_id(),
535-
symbol_expr,
536-
pointer_offset(pointer_expr),
537-
dereference_type);
533+
result.value = make_byte_extract(
534+
symbol_expr, pointer_offset(pointer_expr), dereference_type);
538535
result.pointer = address_of_exprt{result.value};
539536
}
540537
}
@@ -627,7 +624,10 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
627624
root_object_subexpression, o.offset(), dereference_type, ns);
628625
if(subexpr.has_value())
629626
simplify(subexpr.value(), ns);
630-
if(subexpr.has_value() && subexpr.value().id() != byte_extract_id())
627+
if(
628+
subexpr.has_value() &&
629+
subexpr.value().id() != ID_byte_extract_little_endian &&
630+
subexpr.value().id() != ID_byte_extract_big_endian)
631631
{
632632
// Successfully found a member, array index, or combination thereof
633633
// that matches the desired type and offset:
@@ -768,7 +768,7 @@ bool value_set_dereferencet::memory_model_bytes(
768768
else
769769
{
770770
// no, use 'byte_extract'
771-
result = byte_extract_exprt(byte_extract_id(), value, offset, to_type);
771+
result = make_byte_extract(value, offset, to_type);
772772
}
773773

774774
value=result;

‎src/solvers/flattening/boolbv_index.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -338,8 +338,8 @@ bvt boolbvt::convert_index(
338338
o.offset(), from_integer(index * (*subtype_bytes_opt), o.offset().type())),
339339
ns);
340340

341-
byte_extract_exprt be(
342-
byte_extract_id(), o.root_object(), new_offset, array_type.subtype());
341+
byte_extract_exprt be =
342+
make_byte_extract(o.root_object(), new_offset, array_type.subtype());
343343

344344
return convert_bv(be);
345345
}

‎src/solvers/flattening/pointer_logic.cpp

+5-1
Original file line numberDiff line numberDiff line change
@@ -118,9 +118,13 @@ exprt pointer_logict::pointer_expr(
118118
CHECK_RETURN(deep_object_opt.has_value());
119119
exprt deep_object = deep_object_opt.value();
120120
simplify(deep_object, ns);
121-
if(deep_object.id() != byte_extract_id())
121+
if(
122+
deep_object.id() != ID_byte_extract_little_endian &&
123+
deep_object.id() != ID_byte_extract_big_endian)
124+
{
122125
return typecast_exprt::conditional_cast(
123126
address_of_exprt(deep_object), type);
127+
}
124128

125129
const byte_extract_exprt &be = to_byte_extract_expr(deep_object);
126130
const address_of_exprt base(be.op());

‎src/util/byte_operators.cpp

+14-2
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include "config.h"
1212

13-
irep_idt byte_extract_id()
13+
static irep_idt byte_extract_id()
1414
{
1515
switch(config.ansi_c.endianness)
1616
{
@@ -27,7 +27,7 @@ irep_idt byte_extract_id()
2727
UNREACHABLE;
2828
}
2929

30-
irep_idt byte_update_id()
30+
static irep_idt byte_update_id()
3131
{
3232
switch(config.ansi_c.endianness)
3333
{
@@ -43,3 +43,15 @@ irep_idt byte_update_id()
4343

4444
UNREACHABLE;
4545
}
46+
47+
byte_extract_exprt
48+
make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
49+
{
50+
return byte_extract_exprt{byte_extract_id(), _op, _offset, _type};
51+
}
52+
53+
byte_update_exprt
54+
make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
55+
{
56+
return byte_update_exprt{byte_update_id(), _op, _offset, _value};
57+
}

‎src/util/byte_operators.h

+10-3
Original file line numberDiff line numberDiff line change
@@ -71,9 +71,6 @@ inline void validate_expr(const byte_extract_exprt &value)
7171
validate_operands(value, 2, "Byte extract must have two operands");
7272
}
7373

74-
irep_idt byte_extract_id();
75-
irep_idt byte_update_id();
76-
7774
/// Expression corresponding to \c op() where the bytes starting at
7875
/// position \c offset (given in number of bytes) have been updated with
7976
/// \c value.
@@ -129,4 +126,14 @@ inline byte_update_exprt &to_byte_update_expr(exprt &expr)
129126
return static_cast<byte_update_exprt &>(expr);
130127
}
131128

129+
/// Construct a byte_extract_exprt with endianness and byte width matching the
130+
/// current configuration.
131+
byte_extract_exprt
132+
make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type);
133+
134+
/// Construct a byte_update_exprt with endianness and byte width matching the
135+
/// current configuration.
136+
byte_update_exprt
137+
make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value);
138+
132139
#endif // CPROVER_UTIL_BYTE_OPERATORS_H

‎src/util/pointer_offset_size.cpp

+2-5
Original file line numberDiff line numberDiff line change
@@ -682,11 +682,8 @@ optionalt<exprt> get_subexpression_at_offset(
682682
}
683683
}
684684

685-
return byte_extract_exprt(
686-
byte_extract_id(),
687-
expr,
688-
from_integer(offset_bytes, index_type()),
689-
target_type_raw);
685+
return make_byte_extract(
686+
expr, from_integer(offset_bytes, index_type()), target_type_raw);
690687
}
691688

692689
optionalt<exprt> get_subexpression_at_offset(

‎src/util/simplify_expr.cpp

+15-6
Original file line numberDiff line numberDiff line change
@@ -152,7 +152,9 @@ simplify_exprt::resultt<>
152152
simplify_exprt::simplify_clz(const count_leading_zeros_exprt &expr)
153153
{
154154
const auto const_bits_opt = expr2bits(
155-
expr.op(), byte_extract_id() == ID_byte_extract_little_endian, ns);
155+
expr.op(),
156+
config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN,
157+
ns);
156158

157159
if(!const_bits_opt.has_value())
158160
return unchanged(expr);
@@ -1634,7 +1636,13 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
16341636

16351637
// don't do any of the following if endianness doesn't match, as
16361638
// bytes need to be swapped
1637-
if(*offset == 0 && byte_extract_id() == expr.id())
1639+
if(
1640+
*offset == 0 && ((expr.id() == ID_byte_extract_little_endian &&
1641+
config.ansi_c.endianness ==
1642+
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN) ||
1643+
(expr.id() == ID_byte_extract_big_endian &&
1644+
config.ansi_c.endianness ==
1645+
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN)))
16381646
{
16391647
// byte extract of full object is object
16401648
if(expr.type() == expr.op().type())
@@ -1658,7 +1666,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
16581666
{
16591667
const auto const_bits_opt = expr2bits(
16601668
to_array_of_expr(expr.op()).op(),
1661-
byte_extract_id() == ID_byte_extract_little_endian,
1669+
config.ansi_c.endianness ==
1670+
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN,
16621671
ns);
16631672

16641673
if(!const_bits_opt.has_value())
@@ -2023,11 +2032,11 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
20232032
bytes_req = (*val_size) / 8 - val_offset;
20242033

20252034
byte_extract_exprt new_val(
2026-
byte_extract_id(),
2035+
ID_byte_extract_little_endian,
20272036
value,
20282037
from_integer(val_offset, offset.type()),
2029-
array_typet(unsignedbv_typet(8),
2030-
from_integer(bytes_req, offset.type())));
2038+
array_typet(
2039+
unsignedbv_typet(8), from_integer(bytes_req, offset.type())));
20312040

20322041
*it = byte_update_exprt(
20332042
expr.id(),

‎unit/util/pointer_offset_size.cpp

+5-9
Original file line numberDiff line numberDiff line change
@@ -59,8 +59,7 @@ TEST_CASE("Build subexpression to access element at offset into array")
5959
const signedbv_typet small_t(8);
6060
const auto result = get_subexpression_at_offset(a, 1, small_t, ns);
6161
REQUIRE(
62-
result.value() == byte_extract_exprt(
63-
byte_extract_id(),
62+
result.value() == make_byte_extract(
6463
index_exprt(a, from_integer(0, index_type())),
6564
from_integer(1, index_type()),
6665
small_t));
@@ -74,8 +73,7 @@ TEST_CASE("Build subexpression to access element at offset into array")
7473
// index_exprt.
7574
REQUIRE(
7675
result.value() ==
77-
byte_extract_exprt(
78-
byte_extract_id(), a, from_integer(3, index_type()), int16_t));
76+
make_byte_extract(a, from_integer(3, index_type()), int16_t));
7977
}
8078
}
8179

@@ -121,10 +119,8 @@ TEST_CASE("Build subexpression to access element at offset into struct")
121119
const signedbv_typet small_t(8);
122120
const auto result = get_subexpression_at_offset(s, 1, small_t, ns);
123121
REQUIRE(
124-
result.value() == byte_extract_exprt(
125-
byte_extract_id(),
126-
member_exprt(s, "foo", t),
127-
from_integer(1, index_type()),
128-
small_t));
122+
result.value() ==
123+
make_byte_extract(
124+
member_exprt(s, "foo", t), from_integer(1, index_type()), small_t));
129125
}
130126
}

‎unit/util/simplify_expr.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -78,8 +78,8 @@ TEST_CASE("Simplify byte extract", "[core][util]")
7878
// byte-extracting type T at offset 0 from an object of type T yields the
7979
// object
8080
symbol_exprt s("foo", size_type());
81-
byte_extract_exprt be(
82-
byte_extract_id(), s, from_integer(0, index_type()), size_type());
81+
byte_extract_exprt be =
82+
make_byte_extract(s, from_integer(0, index_type()), size_type());
8383

8484
exprt simp = simplify_expr(be, ns);
8585

0 commit comments

Comments
 (0)