Skip to content

boolbvt::convert_constant is now independent of bitvector representation #3106

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

Merged
merged 2 commits into from
Oct 7, 2018
Merged
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
7 changes: 4 additions & 3 deletions src/solvers/flattening/boolbv_constant.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Author: Daniel Kroening, [email protected]

\*******************************************************************/

#include <util/arith_tools.h>

#include "boolbv.h"

Expand Down Expand Up @@ -78,9 +79,9 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
expr_type.id()==ID_c_bit_field ||
expr_type.id()==ID_incomplete_c_enum)
{
const std::string &binary=id2string(expr.get_value());
const auto &value = expr.get_value();

if(binary.size()!=width)
if(value.size() != width)
{
error().source_location=expr.find_source_location();
error() << "wrong value length in constant: "
Expand All @@ -90,7 +91,7 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)

for(std::size_t i=0; i<width; i++)
{
bool bit=(binary[binary.size()-i-1]=='1');
const bool bit = get_bitvector_bit(value, i);
bv[i]=const_literal(bit);
}

Expand Down
11 changes: 11 additions & 0 deletions src/util/arith_tools.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -262,3 +262,14 @@ void mp_max(mp_integer &a, const mp_integer &b)
if(b>a)
a=b;
}

/// Get a bit with given index from bit-vector representation.
/// \param src: the bitvector representation
/// \param bit_index: index (0 is the least significant)
bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index)
{
// The representation is binary, using '0'/'1',
// most significant bit first.
PRECONDITION(bit_index < src.size());
return src[src.size() - 1 - bit_index] == '1';
}
2 changes: 2 additions & 0 deletions src/util/arith_tools.h
Original file line number Diff line number Diff line change
Expand Up @@ -164,4 +164,6 @@ mp_integer power(const mp_integer &base, const mp_integer &exponent);
void mp_min(mp_integer &a, const mp_integer &b);
void mp_max(mp_integer &a, const mp_integer &b);

bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index);

#endif // CPROVER_UTIL_ARITH_TOOLS_H
25 changes: 11 additions & 14 deletions src/util/simplify_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -135,25 +135,22 @@ bool simplify_exprt::simplify_popcount(popcount_exprt &expr)

if(op.is_constant())
{
const typet &type=ns.follow(op.type());
const typet &op_type = op.type();

if(type.id()==ID_signedbv ||
type.id()==ID_unsignedbv)
if(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv)
{
mp_integer value;
if(!to_integer(op, value))
{
std::size_t result;
const auto width = to_bitvector_type(op_type).get_width();
const auto &value = to_constant_expr(op).get_value();
std::size_t result = 0;

for(result=0; value!=0; value=value>>1)
if(value.is_odd())
result++;
for(std::size_t i = 0; i < width; i++)
if(get_bitvector_bit(value, i))
result++;

exprt simp_result = from_integer(result, expr.type());
expr.swap(simp_result);
auto result_expr = from_integer(result, expr.type());
expr.swap(result_expr);

return false;
}
return false;
}
}

Expand Down