Skip to content

Commit 1f21648

Browse files
author
Enrico Steffinlongo
committed
Restructured duplicate_per_byte unit tests
1 parent d88568c commit 1f21648

File tree

1 file changed

+135
-90
lines changed

1 file changed

+135
-90
lines changed

‎unit/util/expr_initializer.cpp‎

Lines changed: 135 additions & 90 deletions
Original file line numberDiff line numberDiff line change
@@ -143,7 +143,7 @@ std::string to_hex(unsigned int value)
143143
}
144144

145145
TEST_CASE(
146-
"duplicate_per_byte on unsigned_bv with constant",
146+
"duplicate_per_byte on bitvector types with constant",
147147
"[core][util][duplicate_per_byte]")
148148
{
149149
auto test = expr_initializer_test_environmentt::make();
@@ -162,47 +162,73 @@ TEST_CASE(
162162
rowt{0xAB, 8, 0xABAB, 16}, // smaller-type constant gets replicated
163163
rowt{0xAB, 8, 0xBABAB, 20}); // smaller-type constant gets replicated
164164
SECTION(
165-
"Testing with output size " + std::to_string(output_size) + " init value " +
166-
to_hex(init_expr_value) + " of size " + std::to_string(init_expr_size))
165+
"Testing with init value " + to_hex(init_expr_value) + " of size " +
166+
std::to_string(init_expr_size))
167167
{
168-
typet output_type = unsignedbv_typet{output_size};
169-
const auto result = duplicate_per_byte(
170-
from_integer(init_expr_value, unsignedbv_typet{init_expr_size}),
171-
output_type);
172-
const auto expected =
173-
from_integer(output_expected_value, unsignedbv_typet{output_size});
174-
REQUIRE(result == expected);
175-
176-
// Check that signed-bv values are replicated including the sign bit.
177-
const auto result_with_signed_init_type = duplicate_per_byte(
178-
from_integer(init_expr_value, signedbv_typet{init_expr_size}),
179-
output_type);
180-
REQUIRE(result_with_signed_init_type == result);
181-
182-
// Check that replicating a pointer_value is same as unsigned_bv.
183-
const pointer_typet pointer_type{bool_typet{}, output_size};
184-
const auto result_with_pointer_type = duplicate_per_byte(
185-
from_integer(init_expr_value, signedbv_typet{init_expr_size}),
186-
pointer_type);
187-
auto pointer_typed_expected =
188-
from_integer(output_expected_value, unsignedbv_typet{output_size});
189-
// Forcing the type to be pointer_typet otherwise from_integer fails when
190-
// the init value is not 0 (NULL).
191-
pointer_typed_expected.type() = pointer_type;
192-
REQUIRE(result_with_pointer_type == pointer_typed_expected);
193-
194-
// Check that replicating to a float_value is same as unsigned_bv.
195-
const auto result_with_float_type = duplicate_per_byte(
196-
from_integer(init_expr_value, unsignedbv_typet{init_expr_size}),
197-
float_type());
198-
const auto expected_unsigned_value =
199-
expr_try_dynamic_cast<constant_exprt>(duplicate_per_byte(
168+
SECTION("filling unsignedbv of size " + std::to_string(output_size))
169+
{
170+
typet output_type = unsignedbv_typet{output_size};
171+
const auto result = duplicate_per_byte(
200172
from_integer(init_expr_value, unsignedbv_typet{init_expr_size}),
201-
unsignedbv_typet{float_type().get_width()}));
202-
REQUIRE(expected_unsigned_value);
203-
const auto float_typed_expected =
204-
constant_exprt{expected_unsigned_value->get_value(), float_type()};
205-
REQUIRE(result_with_float_type == float_typed_expected);
173+
output_type);
174+
const auto expected =
175+
from_integer(output_expected_value, unsignedbv_typet{output_size});
176+
REQUIRE(result == expected);
177+
178+
// Check that signed-bv values are replicated including the sign bit.
179+
const auto result_with_signed_init_type = duplicate_per_byte(
180+
from_integer(init_expr_value, signedbv_typet{init_expr_size}),
181+
output_type);
182+
REQUIRE(result_with_signed_init_type == result);
183+
}
184+
185+
SECTION("filling signedbv of size " + std::to_string(output_size))
186+
{
187+
typet output_type = signedbv_typet{output_size};
188+
const auto result = duplicate_per_byte(
189+
from_integer(init_expr_value, unsignedbv_typet{init_expr_size}),
190+
output_type);
191+
const auto expected =
192+
from_integer(output_expected_value, signedbv_typet{output_size});
193+
REQUIRE(result == expected);
194+
195+
// Check that signed-bv values are replicated including the sign bit.
196+
const auto result_with_signed_init_type = duplicate_per_byte(
197+
from_integer(init_expr_value, signedbv_typet{init_expr_size}),
198+
output_type);
199+
REQUIRE(result_with_signed_init_type == result);
200+
}
201+
202+
SECTION("filling pointer of size " + std::to_string(output_size))
203+
{
204+
// Check that replicating a pointer_value is same as unsigned_bv.
205+
const pointer_typet output_type{bool_typet{}, output_size};
206+
const auto result = duplicate_per_byte(
207+
from_integer(init_expr_value, signedbv_typet{init_expr_size}),
208+
output_type);
209+
auto expected =
210+
from_integer(output_expected_value, unsignedbv_typet{output_size});
211+
// Forcing the type to be pointer_typet otherwise from_integer fails when
212+
// the init value is not 0 (NULL).
213+
expected.type() = output_type;
214+
REQUIRE(result == expected);
215+
}
216+
217+
SECTION("filling float")
218+
{
219+
// Check that replicating to a float_value is same as unsigned_bv.
220+
const auto result = duplicate_per_byte(
221+
from_integer(init_expr_value, unsignedbv_typet{init_expr_size}),
222+
float_type());
223+
const auto expected_unsigned_value =
224+
expr_try_dynamic_cast<constant_exprt>(duplicate_per_byte(
225+
from_integer(init_expr_value, unsignedbv_typet{init_expr_size}),
226+
unsignedbv_typet{float_type().get_width()}));
227+
REQUIRE(expected_unsigned_value);
228+
const auto expected =
229+
constant_exprt{expected_unsigned_value->get_value(), float_type()};
230+
REQUIRE(result == expected);
231+
}
206232
}
207233
}
208234

@@ -221,57 +247,78 @@ TEST_CASE(
221247
rowt{8, 2, 1}, // bigger type gets truncated
222248
rowt{8, 16, 2}, // replicated twice
223249
rowt{8, 20, 3}); // replicated three times and truncated
224-
SECTION(
225-
"Testing with output size " + std::to_string(output_size) + " init size " +
226-
std::to_string(init_expr_size))
250+
SECTION("Testing with init size " + std::to_string(init_expr_size))
227251
{
228-
typet output_type = signedbv_typet{output_size};
229-
230252
const auto init_expr = plus_exprt{
231253
from_integer(1, unsignedbv_typet{init_expr_size}),
232254
from_integer(2, unsignedbv_typet{init_expr_size})};
233-
const auto result = duplicate_per_byte(init_expr, output_type);
255+
SECTION("filling signedbv of size " + std::to_string(output_size))
256+
{
257+
typet output_type = signedbv_typet{output_size};
234258

235-
const auto casted_init_expr =
236-
typecast_exprt::conditional_cast(init_expr, output_type);
237-
const auto expected =
238-
replicate_expression(casted_init_expr, output_type, replication_count);
239-
240-
REQUIRE(result == expected);
241-
242-
// Check that replicating a pointer_value is same as unsigned_bv modulo a
243-
// typecast outside.
244-
const pointer_typet pointer_type{bool_typet{}, output_size};
245-
const auto pointer_typed_result =
246-
duplicate_per_byte(init_expr, pointer_type);
247-
const auto pointer_unsigned_corr_type = unsignedbv_typet{output_size};
248-
const auto pointer_init_expr =
249-
typecast_exprt::conditional_cast(init_expr, pointer_unsigned_corr_type);
250-
const auto pointer_expected = make_byte_extract(
251-
replicate_expression(
252-
pointer_init_expr, pointer_unsigned_corr_type, replication_count),
253-
from_integer(0, char_type()),
254-
pointer_type);
255-
256-
REQUIRE(pointer_typed_result == pointer_expected);
257-
258-
// Check that replicating a float is same as unsigned_bv modulo a typecast
259-
// outside.
260-
const std::size_t float_replication_count =
261-
(float_type().get_width() + config.ansi_c.char_width - 1) /
262-
config.ansi_c.char_width;
263-
const auto float_typed_result = duplicate_per_byte(init_expr, float_type());
264-
const auto float_unsigned_corr_type =
265-
unsignedbv_typet{float_type().get_width()};
266-
const auto float_init_expr =
267-
typecast_exprt::conditional_cast(init_expr, float_unsigned_corr_type);
268-
const auto float_expected = make_byte_extract(
269-
replicate_expression(
270-
float_init_expr, float_unsigned_corr_type, float_replication_count),
271-
from_integer(0, char_type()),
272-
float_type());
273-
274-
REQUIRE(float_typed_result == float_expected);
259+
const auto result = duplicate_per_byte(init_expr, output_type);
260+
261+
const auto casted_init_expr =
262+
typecast_exprt::conditional_cast(init_expr, output_type);
263+
const auto expected =
264+
replicate_expression(casted_init_expr, output_type, replication_count);
265+
266+
REQUIRE(result == expected);
267+
}
268+
269+
SECTION("filling unsignedbv of size " + std::to_string(output_size))
270+
{
271+
typet output_type = unsignedbv_typet{output_size};
272+
const auto result = duplicate_per_byte(init_expr, output_type);
273+
274+
const auto casted_init_expr =
275+
typecast_exprt::conditional_cast(init_expr, output_type);
276+
const auto expected =
277+
replicate_expression(casted_init_expr, output_type, replication_count);
278+
279+
REQUIRE(result == expected);
280+
}
281+
282+
SECTION("filling pointer of size " + std::to_string(output_size))
283+
{
284+
// Check that replicating a pointer_value is same as unsigned_bv modulo a
285+
// byte_extract outside.
286+
const pointer_typet output_type{bool_typet{}, output_size};
287+
const auto result = duplicate_per_byte(init_expr, output_type);
288+
const auto unsigned_corr_type = unsignedbv_typet{output_size};
289+
const auto unsigned_init_expr =
290+
typecast_exprt::conditional_cast(init_expr, unsigned_corr_type);
291+
const auto expected = make_byte_extract(
292+
replicate_expression(
293+
unsigned_init_expr, unsigned_corr_type, replication_count),
294+
from_integer(0, char_type()),
295+
output_type);
296+
297+
REQUIRE(result == expected);
298+
}
299+
300+
SECTION("filling float")
301+
{
302+
// Check that replicating a float is same as unsigned_bv modulo a
303+
// byte_extract outside.
304+
// We ignore the output size and replication_count passed above as float
305+
// size is constant
306+
const std::size_t float_replication_count =
307+
(float_type().get_width() + config.ansi_c.char_width - 1) /
308+
config.ansi_c.char_width;
309+
const auto result = duplicate_per_byte(init_expr, float_type());
310+
const auto unsigned_corr_type =
311+
unsignedbv_typet{float_type().get_width()};
312+
const auto unsigned_init_expr =
313+
typecast_exprt::conditional_cast(init_expr, unsigned_corr_type);
314+
const auto expected = make_byte_extract(
315+
replicate_expression(
316+
unsigned_init_expr, unsigned_corr_type, float_replication_count),
317+
from_integer(0, char_type()),
318+
float_type());
319+
320+
REQUIRE(result == expected);
321+
}
275322
}
276323
}
277324

@@ -439,8 +486,7 @@ TEST_CASE("expr_initializer on float type", "[core][util][expr_initializer]")
439486
{
440487
const auto result = zero_initializer(input_type, test.loc, test.ns);
441488
REQUIRE(result.has_value());
442-
auto expected =
443-
from_integer(0, float_type());
489+
auto expected = from_integer(0, float_type());
444490
REQUIRE(result.value() == expected);
445491
const auto expr_result = expr_initializer(
446492
input_type, test.loc, test.ns, constant_exprt(ID_0, char_type()));
@@ -453,8 +499,7 @@ TEST_CASE("expr_initializer on float type", "[core][util][expr_initializer]")
453499
const auto result =
454500
expr_initializer(input_type, test.loc, test.ns, init_value);
455501
REQUIRE(result.has_value());
456-
const auto expected = duplicate_per_byte(
457-
init_value, float_type());
502+
const auto expected = duplicate_per_byte(init_value, float_type());
458503
REQUIRE(result.value() == expected);
459504
}
460505
}

0 commit comments

Comments
 (0)