Skip to content

Commit

Permalink
Introduce bitst and bytest to avoid bit/byte mix-up
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
tautschnig committed Jun 20, 2024
1 parent a073e70 commit b533d00
Show file tree
Hide file tree
Showing 52 changed files with 834 additions and 556 deletions.
18 changes: 9 additions & 9 deletions src/analyses/goto_rw.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ void rw_range_sett::get_objects_byte_extract(
auto object_size_bits_opt = pointer_offset_bits(be.op().type(), ns);
const exprt simp_offset=simplify_expr(be.offset(), ns);

auto index = numeric_cast<mp_integer>(simp_offset);
auto index = numeric_cast<bytest>(simp_offset);
if(
range_start.is_unknown() || !index.has_value() ||
!object_size_bits_opt.has_value())
Expand All @@ -159,25 +159,25 @@ void rw_range_sett::get_objects_byte_extract(
}
else
{
*index *= be.get_bits_per_byte();
if(*index >= *object_size_bits_opt)
bitst index_bits = bytes_to_bits(*index, be.get_bits_per_byte());
if(index_bits >= *object_size_bits_opt)
return;

endianness_mapt map(
be.op().type(),
be.id()==ID_byte_extract_little_endian,
ns);
range_spect offset = range_start;
if(*index > 0)
if(index_bits > bitst{0})
{
offset += range_spect::to_range_spect(
map.map_bit(numeric_cast_v<std::size_t>(*index)));
bitst{map.map_bit(numeric_cast_v<std::size_t>(index_bits))});

Check warning on line 174 in src/analyses/goto_rw.cpp

View check run for this annotation

Codecov / codecov/patch

src/analyses/goto_rw.cpp#L174

Added line #L174 was not covered by tests
}
else
{
// outside the bounds of immediate byte-extract operand, might still be in
// bounds of a parent object
offset += range_spect::to_range_spect(*index);
offset += range_spect::to_range_spect(index_bits);
}
get_objects_rec(mode, be.op(), offset, size);
}
Expand All @@ -197,7 +197,7 @@ void rw_range_sett::get_objects_shift(
? range_spect::to_range_spect(*op_bits)
: range_spect::unknown();

const auto dist = numeric_cast<mp_integer>(simp_distance);
const auto dist = numeric_cast<bitst>(simp_distance);
if(
range_start.is_unknown() || size.is_unknown() || src_size.is_unknown() ||
!dist.has_value())
Expand Down Expand Up @@ -314,7 +314,7 @@ void rw_range_sett::get_objects_index(
get_objects_rec(
mode,
expr.array(),
range_start + range_spect::to_range_spect(*index) * sub_size,
range_start + range_spect::to_range_spect(bitst{*index}) * sub_size,
size);
}
}
Expand Down Expand Up @@ -344,7 +344,7 @@ void rw_range_sett::get_objects_array(
range_start.is_unknown() ? range_spect{0} : range_start;
range_spect full_r_e =
size.is_unknown()
? sub_size * range_spect::to_range_spect(expr.operands().size())
? sub_size * range_spect::to_range_spect(bitst{expr.operands().size()})

Check warning on line 347 in src/analyses/goto_rw.cpp

View check run for this annotation

Codecov / codecov/patch

src/analyses/goto_rw.cpp#L347

Added line #L347 was not covered by tests
: full_r_s + size;

for(const auto &op : expr.operands())
Expand Down
13 changes: 7 additions & 6 deletions src/analyses/goto_rw.h
Original file line number Diff line number Diff line change
Expand Up @@ -76,15 +76,15 @@ class range_spect
return *this == unknown();
}

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

mp_integer::llong_t ll = size.to_long();
mp_integer::llong_t ll = size.get().to_long();
if(
ll > std::numeric_limits<range_spect::value_type>::max() ||
ll < std::numeric_limits<range_spect::value_type>::min())
Expand Down Expand Up @@ -128,7 +128,7 @@ class range_spect
{
if(is_unknown() || other.is_unknown())
return range_spect::unknown();
return range_spect::to_range_spect(mp_integer{v} + mp_integer{other.v});
return range_spect::to_range_spect(bitst{v} + bitst{other.v});
}

range_spect &operator+=(const range_spect &other)
Expand All @@ -142,7 +142,7 @@ class range_spect
{
if(is_unknown() || other.is_unknown())
return range_spect::unknown();
return range_spect::to_range_spect(mp_integer{v} - mp_integer{other.v});
return range_spect::to_range_spect(bitst{v} - bitst{other.v});
}

range_spect &operator-=(const range_spect &other)
Expand All @@ -156,7 +156,8 @@ class range_spect
{
if(is_unknown() || other.is_unknown())
return range_spect::unknown();
return range_spect::to_range_spect(mp_integer{v} * mp_integer{other.v});
return range_spect::to_range_spect(
bitst{mp_integer{v} * mp_integer{other.v}});
}

private:
Expand Down
7 changes: 4 additions & 3 deletions src/ansi-c/ansi_c_internal_additions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -128,9 +128,10 @@ static std::string architecture_string(const std::string &value, const char *s)
template <typename T>
static std::string architecture_string(T value, const char *s)
{
return std::string("const " CPROVER_PREFIX "integer " CPROVER_PREFIX
"architecture_") +
std::string(s) + "=" + std::to_string(value) + ";\n";
std::ostringstream os;
os << "const " << CPROVER_PREFIX "integer " << CPROVER_PREFIX "architecture_"
<< s << '=' << value << ";\n";
return os.str();
}

void ansi_c_internal_additions(std::string &code, bool support_float16_type)
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1102,7 +1102,7 @@ void c_typecheck_baset::typecheck_expr_alignof(exprt &expr)
}

// we only care about the type
mp_integer a=alignment(argument_type, *this);
bytest a = alignment(argument_type, *this);

exprt tmp=from_integer(a, size_type());
tmp.add_source_location()=expr.source_location();
Expand Down
7 changes: 4 additions & 3 deletions src/ansi-c/expr2c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3502,7 +3502,7 @@ expr2ct::convert_extractbits(const extractbits_exprt &src, unsigned precedence)
{
auto upper = plus_exprt{
src.index(),
from_integer(expr_width_opt.value() - 1, src.index().type())};
from_integer(expr_width_opt.value() - bitst{1}, src.index().type())};
dest += convert_with_precedence(upper, precedence);
}
else
Expand Down Expand Up @@ -3738,8 +3738,9 @@ std::string expr2ct::convert_with_precedence(
else if(src.id()==ID_bswap)
return convert_function(
src,
"__builtin_bswap" + integer2string(*pointer_offset_bits(
to_unary_expr(src).op().type(), ns)));
"__builtin_bswap" +
integer2string(
pointer_offset_bits(to_unary_expr(src).op().type(), ns)->get()));

Check warning on line 3743 in src/ansi-c/expr2c.cpp

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/expr2c.cpp#L3741-L3743

Added lines #L3741 - L3743 were not covered by tests

else if(src.id().starts_with("byte_extract"))
return convert_byte_extract(to_byte_extract_expr(src), precedence = 16);
Expand Down
Loading

0 comments on commit b533d00

Please sign in to comment.