Skip to content

Commit a6df679

Browse files
committed
Introduce bitst and bytest to avoid bit/byte mix-up
Use mp_integers with a unit to clarify when an mp_integer holds a number of bits or a number of bytes. This makes sure that type-inconsistent comparisons as fixed in #7411 result in compile-time errors.
1 parent b7b8db2 commit a6df679

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

52 files changed

+835
-556
lines changed

src/analyses/goto_rw.cpp

+9-9
Original file line numberDiff line numberDiff line change
@@ -150,7 +150,7 @@ void rw_range_sett::get_objects_byte_extract(
150150
auto object_size_bits_opt = pointer_offset_bits(be.op().type(), ns);
151151
const exprt simp_offset=simplify_expr(be.offset(), ns);
152152

153-
auto index = numeric_cast<mp_integer>(simp_offset);
153+
auto index = numeric_cast<bytest>(simp_offset);
154154
if(
155155
range_start.is_unknown() || !index.has_value() ||
156156
!object_size_bits_opt.has_value())
@@ -159,25 +159,25 @@ void rw_range_sett::get_objects_byte_extract(
159159
}
160160
else
161161
{
162-
*index *= be.get_bits_per_byte();
163-
if(*index >= *object_size_bits_opt)
162+
bitst index_bits = bytes_to_bits(*index, be.get_bits_per_byte());
163+
if(index_bits >= *object_size_bits_opt)
164164
return;
165165

166166
endianness_mapt map(
167167
be.op().type(),
168168
be.id()==ID_byte_extract_little_endian,
169169
ns);
170170
range_spect offset = range_start;
171-
if(*index > 0)
171+
if(index_bits > bitst{0})
172172
{
173173
offset += range_spect::to_range_spect(
174-
map.map_bit(numeric_cast_v<std::size_t>(*index)));
174+
bitst{map.map_bit(numeric_cast_v<std::size_t>(index_bits))});
175175
}
176176
else
177177
{
178178
// outside the bounds of immediate byte-extract operand, might still be in
179179
// bounds of a parent object
180-
offset += range_spect::to_range_spect(*index);
180+
offset += range_spect::to_range_spect(index_bits);
181181
}
182182
get_objects_rec(mode, be.op(), offset, size);
183183
}
@@ -197,7 +197,7 @@ void rw_range_sett::get_objects_shift(
197197
? range_spect::to_range_spect(*op_bits)
198198
: range_spect::unknown();
199199

200-
const auto dist = numeric_cast<mp_integer>(simp_distance);
200+
const auto dist = numeric_cast<bitst>(simp_distance);
201201
if(
202202
range_start.is_unknown() || size.is_unknown() || src_size.is_unknown() ||
203203
!dist.has_value())
@@ -314,7 +314,7 @@ void rw_range_sett::get_objects_index(
314314
get_objects_rec(
315315
mode,
316316
expr.array(),
317-
range_start + range_spect::to_range_spect(*index) * sub_size,
317+
range_start + range_spect::to_range_spect(bitst{*index}) * sub_size,
318318
size);
319319
}
320320
}
@@ -344,7 +344,7 @@ void rw_range_sett::get_objects_array(
344344
range_start.is_unknown() ? range_spect{0} : range_start;
345345
range_spect full_r_e =
346346
size.is_unknown()
347-
? sub_size * range_spect::to_range_spect(expr.operands().size())
347+
? sub_size * range_spect::to_range_spect(bitst{expr.operands().size()})
348348
: full_r_s + size;
349349

350350
for(const auto &op : expr.operands())

src/analyses/goto_rw.h

+7-6
Original file line numberDiff line numberDiff line change
@@ -76,15 +76,15 @@ class range_spect
7676
return *this == unknown();
7777
}
7878

79-
static range_spect to_range_spect(const mp_integer &size)
79+
static range_spect to_range_spect(const bitst &size)
8080
{
8181
// The size need not fit into the analysis platform's width of a signed long
8282
// (as an example, it could be an unsigned size_t max, or perhaps the source
8383
// platform has much wider types than the analysis platform.
84-
if(!size.is_long())
84+
if(!size.get().is_long())
8585
return range_spect::unknown();
8686

87-
mp_integer::llong_t ll = size.to_long();
87+
mp_integer::llong_t ll = size.get().to_long();
8888
if(
8989
ll > std::numeric_limits<range_spect::value_type>::max() ||
9090
ll < std::numeric_limits<range_spect::value_type>::min())
@@ -128,7 +128,7 @@ class range_spect
128128
{
129129
if(is_unknown() || other.is_unknown())
130130
return range_spect::unknown();
131-
return range_spect::to_range_spect(mp_integer{v} + mp_integer{other.v});
131+
return range_spect::to_range_spect(bitst{v} + bitst{other.v});
132132
}
133133

134134
range_spect &operator+=(const range_spect &other)
@@ -142,7 +142,7 @@ class range_spect
142142
{
143143
if(is_unknown() || other.is_unknown())
144144
return range_spect::unknown();
145-
return range_spect::to_range_spect(mp_integer{v} - mp_integer{other.v});
145+
return range_spect::to_range_spect(bitst{v} - bitst{other.v});
146146
}
147147

148148
range_spect &operator-=(const range_spect &other)
@@ -156,7 +156,8 @@ class range_spect
156156
{
157157
if(is_unknown() || other.is_unknown())
158158
return range_spect::unknown();
159-
return range_spect::to_range_spect(mp_integer{v} * mp_integer{other.v});
159+
return range_spect::to_range_spect(
160+
bitst{mp_integer{v} * mp_integer{other.v}});
160161
}
161162

162163
private:

src/ansi-c/ansi_c_internal_additions.cpp

+4-3
Original file line numberDiff line numberDiff line change
@@ -119,9 +119,10 @@ static std::string architecture_string(const std::string &value, const char *s)
119119
template <typename T>
120120
static std::string architecture_string(T value, const char *s)
121121
{
122-
return std::string("const " CPROVER_PREFIX "integer " CPROVER_PREFIX
123-
"architecture_") +
124-
std::string(s) + "=" + std::to_string(value) + ";\n";
122+
std::ostringstream os;
123+
os << "const " << CPROVER_PREFIX "integer " << CPROVER_PREFIX "architecture_"
124+
<< s << '=' << value << ";\n";
125+
return os.str();
125126
}
126127

127128
void ansi_c_internal_additions(std::string &code, bool support_float16_type)

src/ansi-c/c_typecheck_expr.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -1084,7 +1084,7 @@ void c_typecheck_baset::typecheck_expr_alignof(exprt &expr)
10841084
}
10851085

10861086
// we only care about the type
1087-
mp_integer a=alignment(argument_type, *this);
1087+
bytest a = alignment(argument_type, *this);
10881088

10891089
exprt tmp=from_integer(a, size_type());
10901090
tmp.add_source_location()=expr.source_location();

src/ansi-c/expr2c.cpp

+3-2
Original file line numberDiff line numberDiff line change
@@ -3738,8 +3738,9 @@ std::string expr2ct::convert_with_precedence(
37383738
else if(src.id()==ID_bswap)
37393739
return convert_function(
37403740
src,
3741-
"__builtin_bswap" + integer2string(*pointer_offset_bits(
3742-
to_unary_expr(src).op().type(), ns)));
3741+
"__builtin_bswap" +
3742+
integer2string(
3743+
pointer_offset_bits(to_unary_expr(src).op().type(), ns)->get()));
37433744

37443745
else if(src.id().starts_with("byte_extract"))
37453746
return convert_byte_extract(to_byte_extract_expr(src), precedence = 16);

0 commit comments

Comments
 (0)