Skip to content

Introduce bitst and bytest to avoid bit/byte mix-up #7413

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: develop
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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))});
}
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()})
: 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 @@ -1124,7 +1124,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 @@ -3534,7 +3534,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 @@ -3770,8 +3770,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()));

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