Skip to content

Commit d59e8f8

Browse files
kroeningkroening
authored
Merge pull request #6596 from diffblue/type_with_subtype
check type invariant of type_with_subtypet
2 parents cedd5ea + 87fef52 commit d59e8f8

File tree

9 files changed

+90
-25
lines changed

9 files changed

+90
-25
lines changed

‎src/ansi-c/ansi_c_convert_type.cpp‎

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -45,9 +45,13 @@ void ansi_c_convert_typet::read_rec(const typet &type)
4545
c_qualifiers.is_volatile=true;
4646
else if(type.id()==ID_asm)
4747
{
48-
if(type.has_subtype() &&
49-
type.subtype().id()==ID_string_constant)
50-
c_storage_spec.asm_label = to_string_constant(type.subtype()).get_value();
48+
// These can have up to 5 subtypes; we only use the first one.
49+
const auto &type_with_subtypes = to_type_with_subtypes(type);
50+
if(
51+
!type_with_subtypes.subtypes().empty() &&
52+
type_with_subtypes.subtypes()[0].id() == ID_string_constant)
53+
c_storage_spec.asm_label =
54+
to_string_constant(type_with_subtypes.subtypes()[0]).get_value();
5155
}
5256
else if(type.id()==ID_section &&
5357
type.has_subtype() &&
@@ -187,8 +191,11 @@ void ansi_c_convert_typet::read_rec(const typet &type)
187191
{
188192
c_qualifiers.is_transparent_union=true;
189193
}
190-
else if(type.id()==ID_vector)
191-
vector_size=to_vector_type(type).size();
194+
else if(type.id() == ID_frontend_vector)
195+
{
196+
// note that this is not yet a vector_typet -- this is a size only
197+
vector_size = static_cast<const constant_exprt &>(type.find(ID_size));
198+
}
192199
else if(type.id()==ID_void)
193200
{
194201
// we store 'void' as 'empty'

‎src/ansi-c/c_storage_spec.cpp‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -52,11 +52,12 @@ void c_storage_spect::read(const typet &type)
5252
{
5353
alias = to_string_constant(type.subtype()).get_value();
5454
}
55-
else if(type.id()==ID_asm &&
56-
type.has_subtype() &&
57-
type.subtype().id()==ID_string_constant)
55+
else if(
56+
type.id() == ID_asm && !to_type_with_subtypes(type).subtypes().empty() &&
57+
to_type_with_subtypes(type).subtypes()[0].id() == ID_string_constant)
5858
{
59-
asm_label = to_string_constant(type.subtype()).get_value();
59+
asm_label =
60+
to_string_constant(to_type_with_subtypes(type).subtypes()[0]).get_value();
6061
}
6162
else if(type.id()==ID_section &&
6263
type.has_subtype() &&

‎src/ansi-c/parser.y‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1607,7 +1607,7 @@ gcc_type_attribute:
16071607
| TOK_GCC_ATTRIBUTE_TRANSPARENT_UNION
16081608
{ $$=$1; set($$, ID_transparent_union); }
16091609
| TOK_GCC_ATTRIBUTE_VECTOR_SIZE '(' comma_expression ')'
1610-
{ $$=$1; set($$, ID_vector); parser_stack($$).add(ID_size)=parser_stack($3); }
1610+
{ $$=$1; set($$, ID_frontend_vector); parser_stack($$).add(ID_size)=parser_stack($3); }
16111611
| TOK_GCC_ATTRIBUTE_ALIGNED
16121612
{ $$=$1; set($$, ID_aligned); }
16131613
| TOK_GCC_ATTRIBUTE_ALIGNED '(' comma_expression ')'

‎src/solvers/lowering/byte_operators.cpp‎

Lines changed: 32 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,24 @@ static boundst map_bounds(
5656
return result;
5757
}
5858

59+
/// changes the width of the given bitvector type
60+
bitvector_typet adjust_width(const typet &src, std::size_t new_width)
61+
{
62+
if(src.id() == ID_unsignedbv)
63+
return unsignedbv_typet(new_width);
64+
else if(src.id() == ID_signedbv)
65+
return signedbv_typet(new_width);
66+
else if(src.id() == ID_bv)
67+
return bv_typet(new_width);
68+
else if(src.id() == ID_c_enum) // we use the underlying type
69+
return adjust_width(to_c_enum_type(src).underlying_type(), new_width);
70+
else if(src.id() == ID_c_bit_field)
71+
return c_bit_field_typet(
72+
to_c_bit_field_type(src).underlying_type(), new_width);
73+
else
74+
PRECONDITION(false);
75+
}
76+
5977
/// Convert a bitvector-typed expression \p bitvector_expr to a struct-typed
6078
/// expression. See \ref bv_to_expr for an overview.
6179
static struct_exprt bv_to_struct_expr(
@@ -89,7 +107,7 @@ static struct_exprt bv_to_struct_expr(
89107
endianness_map,
90108
member_offset_bits,
91109
member_offset_bits + component_bits - 1);
92-
bitvector_typet type{bitvector_expr.type().id(), component_bits};
110+
bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits);
93111
operands.push_back(bv_to_expr(
94112
extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
95113
comp.type(),
@@ -133,7 +151,7 @@ static union_exprt bv_to_union_expr(
133151
}
134152

135153
const auto bounds = map_bounds(endianness_map, 0, component_bits - 1);
136-
bitvector_typet type{bitvector_expr.type().id(), component_bits};
154+
bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits);
137155
const irep_idt &component_name = widest_member.has_value()
138156
? widest_member->first.get_name()
139157
: components.front().get_name();
@@ -185,7 +203,8 @@ static array_exprt bv_to_array_expr(
185203
numeric_cast_v<std::size_t>(*subtype_bits);
186204
const auto bounds = map_bounds(
187205
endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
188-
bitvector_typet type{bitvector_expr.type().id(), subtype_bits_int};
206+
bitvector_typet type =
207+
adjust_width(bitvector_expr.type(), subtype_bits_int);
189208
operands.push_back(bv_to_expr(
190209
extractbits_exprt{
191210
bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
@@ -230,7 +249,8 @@ static vector_exprt bv_to_vector_expr(
230249
numeric_cast_v<std::size_t>(*subtype_bits);
231250
const auto bounds = map_bounds(
232251
endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
233-
bitvector_typet type{bitvector_expr.type().id(), subtype_bits_int};
252+
bitvector_typet type =
253+
adjust_width(bitvector_expr.type(), subtype_bits_int);
234254
operands.push_back(bv_to_expr(
235255
extractbits_exprt{
236256
bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
@@ -274,7 +294,8 @@ static complex_exprt bv_to_complex_expr(
274294
const auto bounds_imag =
275295
map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
276296

277-
const bitvector_typet type{bitvector_expr.type().id(), subtype_bits};
297+
const bitvector_typet type =
298+
adjust_width(bitvector_expr.type(), subtype_bits);
278299

279300
return complex_exprt{
280301
bv_to_expr(
@@ -1293,7 +1314,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
12931314
else // width_bytes>=2
12941315
{
12951316
concatenation_exprt concatenation(
1296-
std::move(op), bitvector_typet(subtype->id(), width_bytes * 8));
1317+
std::move(op), adjust_width(*subtype, width_bytes * 8));
12971318

12981319
endianness_mapt map(concatenation.type(), little_endian, ns);
12991320
return bv_to_expr(concatenation, src.type(), map, ns);
@@ -2304,12 +2325,11 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
23042325
extractbits_exprt extra_bits{
23052326
src.op(), bounds.ub, bounds.lb, bv_typet{n_extra_bits}};
23062327

2307-
update_value =
2308-
concatenation_exprt{typecast_exprt::conditional_cast(
2309-
update_value, bv_typet{update_bits_int}),
2310-
extra_bits,
2311-
bitvector_typet{update_value.type().id(),
2312-
update_bits_int + n_extra_bits}};
2328+
update_value = concatenation_exprt{
2329+
typecast_exprt::conditional_cast(
2330+
update_value, bv_typet{update_bits_int}),
2331+
extra_bits,
2332+
adjust_width(update_value.type(), update_bits_int + n_extra_bits)};
23132333
}
23142334
else
23152335
{

‎src/util/c_types.h‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,13 +58,15 @@ inline bool can_cast_type<c_bit_field_typet>(const typet &type)
5858
inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
5959
{
6060
PRECONDITION(can_cast_type<c_bit_field_typet>(type));
61+
type_with_subtypet::check(type);
6162
return static_cast<const c_bit_field_typet &>(type);
6263
}
6364

6465
/// \copydoc to_c_bit_field_type(const typet &type)
6566
inline c_bit_field_typet &to_c_bit_field_type(typet &type)
6667
{
6768
PRECONDITION(can_cast_type<c_bit_field_typet>(type));
69+
type_with_subtypet::check(type);
6870
return static_cast<c_bit_field_typet &>(type);
6971
}
7072

@@ -300,13 +302,15 @@ inline bool can_cast_type<c_enum_typet>(const typet &type)
300302
inline const c_enum_typet &to_c_enum_type(const typet &type)
301303
{
302304
PRECONDITION(can_cast_type<c_enum_typet>(type));
305+
type_with_subtypet::check(type);
303306
return static_cast<const c_enum_typet &>(type);
304307
}
305308

306309
/// \copydoc to_c_enum_type(const typet &)
307310
inline c_enum_typet &to_c_enum_type(typet &type)
308311
{
309312
PRECONDITION(can_cast_type<c_enum_typet>(type));
313+
type_with_subtypet::check(type);
310314
return static_cast<c_enum_typet &>(type);
311315
}
312316

‎src/util/pointer_expr.h‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,7 @@ class pointer_typet : public bitvector_typet
5454
const typet &type,
5555
const validation_modet vm = validation_modet::INVARIANT)
5656
{
57+
type_with_subtypet::check(type);
5758
DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width");
5859
}
5960
};
@@ -116,6 +117,8 @@ class reference_typet : public pointer_typet
116117
const validation_modet vm = validation_modet::INVARIANT)
117118
{
118119
PRECONDITION(type.id() == ID_pointer);
120+
DATA_CHECK(
121+
vm, type.get_sub().size() == 1, "reference must have one type parameter");
119122
const reference_typet &reference_type =
120123
static_cast<const reference_typet &>(type);
121124
DATA_CHECK(

‎src/util/std_types.cpp‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
1919
void array_typet::check(const typet &type, const validation_modet vm)
2020
{
2121
PRECONDITION(type.id() == ID_array);
22+
type_with_subtypet::check(type);
2223
const array_typet &array_type = static_cast<const array_typet &>(type);
2324
if(array_type.size().is_nil())
2425
{

‎src/util/std_types.h‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -832,13 +832,15 @@ inline bool can_cast_type<array_typet>(const typet &type)
832832
inline const array_typet &to_array_type(const typet &type)
833833
{
834834
PRECONDITION(can_cast_type<array_typet>(type));
835+
array_typet::check(type);
835836
return static_cast<const array_typet &>(type);
836837
}
837838

838839
/// \copydoc to_array_type(const typet &)
839840
inline array_typet &to_array_type(typet &type)
840841
{
841842
PRECONDITION(can_cast_type<array_typet>(type));
843+
array_typet::check(type);
842844
return static_cast<array_typet &>(type);
843845
}
844846

@@ -1038,13 +1040,15 @@ inline bool can_cast_type<vector_typet>(const typet &type)
10381040
inline const vector_typet &to_vector_type(const typet &type)
10391041
{
10401042
PRECONDITION(can_cast_type<vector_typet>(type));
1043+
type_with_subtypet::check(type);
10411044
return static_cast<const vector_typet &>(type);
10421045
}
10431046

10441047
/// \copydoc to_vector_type(const typet &)
10451048
inline vector_typet &to_vector_type(typet &type)
10461049
{
10471050
PRECONDITION(can_cast_type<vector_typet>(type));
1051+
type_with_subtypet::check(type);
10481052
return static_cast<vector_typet &>(type);
10491053
}
10501054

@@ -1078,13 +1082,15 @@ inline bool can_cast_type<complex_typet>(const typet &type)
10781082
inline const complex_typet &to_complex_type(const typet &type)
10791083
{
10801084
PRECONDITION(can_cast_type<complex_typet>(type));
1085+
type_with_subtypet::check(type);
10811086
return static_cast<const complex_typet &>(type);
10821087
}
10831088

10841089
/// \copydoc to_complex_type(const typet &)
10851090
inline complex_typet &to_complex_type(typet &type)
10861091
{
10871092
PRECONDITION(can_cast_type<complex_typet>(type));
1093+
type_with_subtypet::check(type);
10881094
return static_cast<complex_typet &>(type);
10891095
}
10901096

‎src/util/type.h‎

Lines changed: 26 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
1616
class namespacet;
1717

1818
#include "source_location.h"
19+
#include "validate.h"
1920
#include "validate_types.h"
2021
#include "validation_mode.h"
2122

@@ -63,7 +64,9 @@ class typet:public irept
6364
{ return !get_sub().empty(); }
6465

6566
bool has_subtype() const
66-
{ return !get_sub().empty(); }
67+
{
68+
return get_sub().size() == 1;
69+
}
6770

6871
void remove_subtype()
6972
{ get_sub().clear(); }
@@ -149,17 +152,37 @@ class type_with_subtypet:public typet
149152
: typet(std::move(_id), std::move(_subtype))
150153
{
151154
}
155+
156+
const typet &subtype() const
157+
{
158+
// the existence of get_sub().front() is established by check()
159+
return static_cast<const typet &>(get_sub().front());
160+
}
161+
162+
typet &subtype()
163+
{
164+
// the existence of get_sub().front() is established by check()
165+
return static_cast<typet &>(get_sub().front());
166+
}
167+
168+
static void check(
169+
const typet &type,
170+
const validation_modet vm = validation_modet::INVARIANT)
171+
{
172+
DATA_CHECK(
173+
vm, type.get_sub().size() == 1, "type must have one type parameter");
174+
}
152175
};
153176

154177
inline const type_with_subtypet &to_type_with_subtype(const typet &type)
155178
{
156-
PRECONDITION(type.has_subtype());
179+
type_with_subtypet::check(type);
157180
return static_cast<const type_with_subtypet &>(type);
158181
}
159182

160183
inline type_with_subtypet &to_type_with_subtype(typet &type)
161184
{
162-
PRECONDITION(type.has_subtype());
185+
type_with_subtypet::check(type);
163186
return static_cast<type_with_subtypet &>(type);
164187
}
165188

0 commit comments

Comments
 (0)