Skip to content

bv2integer is now told the width #3100

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.

Sign up for GitHub

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 3 commits into from
Oct 18, 2018
Merged

bv2integer is now told the width #3100

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a3c453c
use high-level numerical conversion
Oct 4, 2018
2f080ef
goto_trace: strengthen signature of numeric_representation
Oct 4, 2018
92f2621
bv2integer is now told the width
Oct 4, 2018
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
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ static const std::string get_thread_block_identifier(
{
PRECONDITION(f_code.arguments().size() == 1);
const exprt &expr = f_code.arguments()[0];
mp_integer lbl_id = bv2integer(expr.op0().get_string(ID_value), false);
const mp_integer lbl_id = numeric_cast_v<mp_integer>(expr.op0());
return integer2string(lbl_id);
}

Expand Down
9 changes: 6 additions & 3 deletions src/ansi-c/expr2c.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1811,9 +1811,10 @@ std::string expr2ct::convert_constant(
if(c_enum_type.id()!=ID_c_enum)
return convert_norep(src, precedence);

bool is_signed=c_enum_type.subtype().id()==ID_signedbv;
const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit pick: Unrelated change?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, but we appear to do some, and not others!

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As a reviewer, the first question I usually ask myself is "why was this line changed" and expect to be able to immediately answer that to myself from the commit message. Sometimes there are additional changes in those lines beyond what's in the commit message. If those are of the nature "added in a const" or "fixed up whitespace" then those seem like desirable improvements. Everything else raises eyebrows and usually makes me post questions in here ;-)

const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();

mp_integer int_value = bv2integer(id2string(value), is_signed);
mp_integer int_value = bv2integer(id2string(value), width, is_signed);
mp_integer i=0;

irep_idt int_value_string=integer2string(int_value);
Expand Down Expand Up @@ -1849,8 +1850,10 @@ std::string expr2ct::convert_constant(
type.id()==ID_c_bit_field ||
type.id()==ID_c_bool)
{
const auto width = to_bitvector_type(type).get_width();

mp_integer int_value =
bv2integer(id2string(value), type.id() == ID_signedbv);
bv2integer(id2string(value), width, type.id() == ID_signedbv);

const irep_idt &c_type=
type.id()==ID_c_bit_field?type.subtype().get(ID_C_c_type):
Expand Down
9 changes: 5 additions & 4 deletions src/goto-programs/goto_convert.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1830,11 +1830,12 @@ bool goto_convertt::get_string_constant(
forall_operands(it, index_op)
if(it->is_constant())
{
unsigned long i = integer2ulong(
bv2integer(id2string(to_constant_expr(*it).get_value()), true));
const auto i = numeric_cast<std::size_t>(*it);
if(!i.has_value())
return true;

if(i!=0) // to skip terminating 0
result+=static_cast<char>(i);
if(i.value() != 0) // to skip terminating 0
result += static_cast<char>(i.value());
}

return value=result, false;
Expand Down
16 changes: 10 additions & 6 deletions src/goto-programs/goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,22 +129,25 @@ void goto_trace_stept::output(
/// \param expr: expression to get numeric representation from
/// \param options: configuration options
/// \return a string with the numeric representation
static std::string
numeric_representation(const exprt &expr, const trace_optionst &options)
static std::string numeric_representation(
const constant_exprt &expr,
const trace_optionst &options)
{
std::string result;
std::string prefix;

const irep_idt &value = expr.get_value();

if(options.hex_representation)
{
mp_integer value_int =
bv2integer(id2string(to_constant_expr(expr).get_value()), false);
mp_integer value_int = bv2integer(id2string(value), value.size(), false);
result = integer2string(value_int, 16);
prefix = "0x";
}
else
{
prefix = "0b";
result = expr.get_string(ID_value);
result = id2string(value);
}

std::ostringstream oss;
Expand Down Expand Up @@ -181,7 +184,8 @@ std::string trace_numeric_value(
type.id()==ID_c_enum ||
type.id()==ID_c_enum_tag)
{
const std::string &str = numeric_representation(expr, options);
const std::string &str =
numeric_representation(to_constant_expr(expr), options);
return str;
}
else if(type.id()==ID_bool)
Expand Down
15 changes: 8 additions & 7 deletions src/goto-programs/interpreter_evaluate.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -382,7 +382,8 @@ void interpretert::evaluate(
else if(expr.type().id()==ID_c_bool)
{
const irep_idt &value=to_constant_expr(expr).get_value();
dest.push_back(bv2integer(id2string(value), false));
const auto width = to_c_bool_type(expr.type()).get_width();
dest.push_back(bv2integer(id2string(value), width, false));
return;
}
else if(expr.type().id()==ID_bool)
Expand Down Expand Up @@ -983,16 +984,16 @@ void interpretert::evaluate(
}
else if(expr.type().id()==ID_signedbv)
{
const std::string s =
integer2bv(value, to_signedbv_type(expr.type()).get_width());
dest.push_back(bv2integer(s, true));
const auto width = to_signedbv_type(expr.type()).get_width();
const std::string s = integer2bv(value, width);
dest.push_back(bv2integer(s, width, true));
return;
}
else if(expr.type().id()==ID_unsignedbv)
{
const std::string s =
integer2bv(value, to_unsignedbv_type(expr.type()).get_width());
dest.push_back(bv2integer(s, false));
const auto width = to_unsignedbv_type(expr.type()).get_width();
const std::string s = integer2bv(value, width);
dest.push_back(bv2integer(s, width, false));
return;
}
else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))
Expand Down
29 changes: 21 additions & 8 deletions src/util/arith_tools.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,44 +43,57 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
}
else if(type_id==ID_unsignedbv)
{
int_value = bv2integer(id2string(value), false);
const auto width = to_unsignedbv_type(type).get_width();
int_value = bv2integer(id2string(value), width, false);
return false;
}
else if(type_id==ID_signedbv)
{
int_value = bv2integer(id2string(value), true);
const auto width = to_signedbv_type(type).get_width();
int_value = bv2integer(id2string(value), width, true);
return false;
}
else if(type_id==ID_c_bool)
{
int_value = bv2integer(id2string(value), false);
const auto width = to_c_bool_type(type).get_width();
int_value = bv2integer(id2string(value), width, false);
return false;
}
else if(type_id==ID_c_enum)
{
const typet &subtype=to_c_enum_type(type).subtype();
if(subtype.id()==ID_signedbv)
{
int_value = bv2integer(id2string(value), true);
const auto width = to_signedbv_type(type).get_width();
int_value = bv2integer(id2string(value), width, true);
return false;
}
else if(subtype.id()==ID_unsignedbv)
{
int_value = bv2integer(id2string(value), false);
const auto width = to_unsignedbv_type(type).get_width();
int_value = bv2integer(id2string(value), width, false);
return false;
}
}
else if(type_id==ID_c_bit_field)
{
const typet &subtype = to_c_bit_field_type(type).subtype();
const auto &c_bit_field_type = to_c_bit_field_type(type);
const auto width = c_bit_field_type.get_width();
const typet &subtype = c_bit_field_type.subtype();

if(subtype.id()==ID_signedbv)
{
int_value = bv2integer(id2string(value), true);
int_value = bv2integer(id2string(value), width, true);
return false;
}
else if(subtype.id()==ID_unsignedbv)
{
int_value = bv2integer(id2string(value), false);
int_value = bv2integer(id2string(value), width, false);
return false;
}
else if(subtype.id() == ID_c_bool)
{
int_value = bv2integer(id2string(value), width, false);
return false;
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/util/bv_arithmetic.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,5 +184,5 @@ void bv_arithmetict::from_expr(const exprt &expr)
{
PRECONDITION(expr.is_constant());
spec=bv_spect(expr.type());
value = bv2integer(expr.get_string(ID_value), spec.is_signed);
value = bv2integer(expr.get_string(ID_value), spec.width, spec.is_signed);
}
3 changes: 2 additions & 1 deletion src/util/expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -246,8 +246,9 @@ bool exprt::is_one() const
}
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
{
const auto width = to_bitvector_type(type()).get_width();
mp_integer int_value =
bv2integer(id2string(constant_expr.get_value()), false);
bv2integer(id2string(constant_expr.get_value()), width, false);
if(int_value==1)
return true;
}
Expand Down
2 changes: 1 addition & 1 deletion src/util/fixedbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ fixedbvt::fixedbvt(const constant_exprt &expr)
void fixedbvt::from_expr(const constant_exprt &expr)
{
spec=fixedbv_spect(to_fixedbv_type(expr.type()));
v = bv2integer(id2string(expr.get_value()), true);
v = bv2integer(id2string(expr.get_value()), spec.width, true);
}

void fixedbvt::from_integer(const mp_integer &i)
Expand Down
2 changes: 1 addition & 1 deletion src/util/ieee_float.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1062,7 +1062,7 @@ void ieee_floatt::change_spec(const ieee_float_spect &dest_spec)
void ieee_floatt::from_expr(const constant_exprt &expr)
{
spec=ieee_float_spect(to_floatbv_type(expr.type()));
unpack(bv2integer(id2string(expr.get_value()), false));
unpack(bv2integer(id2string(expr.get_value()), spec.width(), false));
}

mp_integer ieee_floatt::to_integer() const
Expand Down
4 changes: 3 additions & 1 deletion src/util/mp_arith.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -192,8 +192,10 @@ const std::string integer2bv(const mp_integer &src, std::size_t width)
}

/// convert a bit-vector representation (possibly signed) to integer
const mp_integer bv2integer(const std::string &src, bool is_signed)
const mp_integer
bv2integer(const std::string &src, std::size_t width, bool is_signed)
{
PRECONDITION(src.size() == width);
return binary2integer(src, is_signed);
}

Expand Down
3 changes: 2 additions & 1 deletion src/util/mp_arith.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,8 @@ const mp_integer binary2integer(const std::string &, bool is_signed);
const std::string integer2bv(const mp_integer &, std::size_t width);

/// convert a bit-vector representation (possibly signed) to integer
const mp_integer bv2integer(const std::string &, bool is_signed);
const mp_integer
bv2integer(const std::string &, std::size_t width, bool is_signed);

/// \deprecated use numeric_cast_v<unsigned long long> instead
DEPRECATED("Use numeric_cast_v<unsigned long long> instead")
Expand Down
68 changes: 15 additions & 53 deletions src/util/simplify_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -669,7 +669,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
expr_type_id==ID_signedbv ||
expr_type_id==ID_floatbv)
{
mp_integer int_value = bv2integer(id2string(value), false);
const auto width = to_bv_type(op_type).get_width();
mp_integer int_value = bv2integer(id2string(value), width, false);
expr=from_integer(int_value, expr_type);
return false;
}
Expand Down Expand Up @@ -811,71 +812,32 @@ bool simplify_exprt::simplify_if_implies(
expr.op1().is_constant() &&
cond.op1().type()==expr.op1().type())
{
const irep_idt &type_id=cond.op1().type().id();
if(type_id==ID_integer || type_id==ID_natural)
{
if(string2integer(cond.op1().get_string(ID_value))>=
string2integer(expr.op1().get_string(ID_value)))
{
new_truth = true;
return false;
}
}
else if(type_id==ID_unsignedbv)
{
const mp_integer i1, i2;
if(
bv2integer(cond.op1().get_string(ID_value), false) >=
bv2integer(expr.op1().get_string(ID_value), false))
{
new_truth = true;
return false;
}
}
else if(type_id==ID_signedbv)
mp_integer i1, i2;

if(
!to_integer(to_constant_expr(cond.op1()), i1) &&
!to_integer(to_constant_expr(expr.op1()), i2))
{
const mp_integer i1, i2;
if(
bv2integer(cond.op1().get_string(ID_value), true) >=
bv2integer(expr.op1().get_string(ID_value), true))
if(i1 >= i2)
{
new_truth = true;
return false;
}
}
}

if(cond.op1()==expr.op1() &&
cond.op0().is_constant() &&
expr.op0().is_constant() &&
cond.op0().type()==expr.op0().type())
{
const irep_idt &type_id = cond.op1().type().id();
if(type_id==ID_integer || type_id==ID_natural)
{
if(string2integer(cond.op1().get_string(ID_value))<=
string2integer(expr.op1().get_string(ID_value)))
{
new_truth = true;
return false;
}
}
else if(type_id==ID_unsignedbv)
{
const mp_integer i1, i2;
if(
bv2integer(cond.op1().get_string(ID_value), false) <=
bv2integer(expr.op1().get_string(ID_value), false))
{
new_truth = true;
return false;
}
}
else if(type_id==ID_signedbv)
mp_integer i1, i2;

if(
!to_integer(to_constant_expr(cond.op0()), i1) &&
!to_integer(to_constant_expr(expr.op0()), i2))
{
const mp_integer i1, i2;
if(
bv2integer(cond.op1().get_string(ID_value), true) <=
bv2integer(expr.op1().get_string(ID_value), true))
if(i1 <= i2)
{
new_truth = true;
return false;
Expand Down
4 changes: 3 additions & 1 deletion src/util/simplify_expr_pointer.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -387,7 +387,9 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
else
{
// this is a pointer, we can't use to_integer
mp_integer number = bv2integer(id2string(c_ptr.get_value()), false);
const auto width = to_pointer_type(ptr.type()).get_width();
mp_integer number =
bv2integer(id2string(c_ptr.get_value()), width, false);
// a null pointer would have been caught above, return value 0
// will indicate that conversion failed
if(number==0)
Expand Down