From 935f4d21b6814d8af190a62b8d8748d625e20bb0 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 4 Oct 2018 09:38:54 +0100 Subject: [PATCH] introduce integer2bv and bv2integer The representation of bitvectors is now hard-wired to binary with leading zeros and fixed width. These two new functions provide a wrapper around any future representation. --- ...a_bytecode_concurrency_instrumentation.cpp | 2 +- src/ansi-c/expr2c.cpp | 6 ++--- src/goto-cc/linker_script_merge.cpp | 6 ++--- src/goto-programs/goto_convert.cpp | 4 +-- src/goto-programs/goto_trace.cpp | 2 +- src/goto-programs/interpreter_evaluate.cpp | 14 +++++----- src/util/arith_tools.cpp | 26 +++++++++---------- src/util/bv_arithmetic.cpp | 4 +-- src/util/expr.cpp | 2 +- src/util/fixedbv.cpp | 4 +-- src/util/ieee_float.cpp | 4 +-- src/util/mp_arith.cpp | 12 +++++++++ src/util/mp_arith.h | 6 +++++ src/util/simplify_expr.cpp | 22 +++++++++------- src/util/simplify_expr_int.cpp | 2 +- src/util/simplify_expr_pointer.cpp | 2 +- 16 files changed, 70 insertions(+), 48 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp index 380282d32ff..9ac874cd3ef 100644 --- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp @@ -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 = binary2integer(expr.op0().get_string(ID_value), false); + mp_integer lbl_id = bv2integer(expr.op0().get_string(ID_value), false); return integer2string(lbl_id); } diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 6ffbc25ce7b..764cd3f6937 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1813,7 +1813,7 @@ std::string expr2ct::convert_constant( bool is_signed=c_enum_type.subtype().id()==ID_signedbv; - mp_integer int_value=binary2integer(id2string(value), is_signed); + mp_integer int_value = bv2integer(id2string(value), is_signed); mp_integer i=0; irep_idt int_value_string=integer2string(int_value); @@ -1849,8 +1849,8 @@ std::string expr2ct::convert_constant( type.id()==ID_c_bit_field || type.id()==ID_c_bool) { - mp_integer int_value= - binary2integer(id2string(value), type.id()==ID_signedbv); + mp_integer int_value = + bv2integer(id2string(value), type.id() == ID_signedbv); const irep_idt &c_type= type.id()==ID_c_bit_field?type.subtype().get(ID_C_c_type): diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 7c8b04ac316..446ddca4166 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -566,7 +566,7 @@ int linker_script_merget::ls_data2instructions( symbol_exprt lhs(d["sym"].value, pointer_type(char_type())); constant_exprt rhs( - integer2binary( + integer2bv( string2integer(id2string(symbol_value)), unsigned_int_type().get_width()), unsigned_int_type()); @@ -632,8 +632,8 @@ int linker_script_merget::ls_data2instructions( symbol_exprt lhs(d["sym"].value, pointer_type(char_type())); constant_exprt rhs; - rhs.set_value(integer2binary(string2integer(d["val"].value), - unsigned_int_type().get_width())); + rhs.set_value(integer2bv( + string2integer(d["val"].value), unsigned_int_type().get_width())); rhs.type()=unsigned_int_type(); exprt rhs_tc(rhs); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 7fce24e1d24..df09d62e2e6 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -1834,8 +1834,8 @@ bool goto_convertt::get_string_constant( forall_operands(it, index_op) if(it->is_constant()) { - unsigned long i=integer2ulong( - binary2integer(id2string(to_constant_expr(*it).get_value()), true)); + unsigned long i = integer2ulong( + bv2integer(id2string(to_constant_expr(*it).get_value()), true)); if(i!=0) // to skip terminating 0 result+=static_cast(i); diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index b8259c5d8ff..0b032fe1b93 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -137,7 +137,7 @@ numeric_representation(const exprt &expr, const trace_optionst &options) if(options.hex_representation) { mp_integer value_int = - binary2integer(id2string(to_constant_expr(expr).get_value()), false); + bv2integer(id2string(to_constant_expr(expr).get_value()), false); result = integer2string(value_int, 16); prefix = "0x"; } diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index f1a60299323..51d04a0a552 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -382,7 +382,7 @@ void interpretert::evaluate( else if(expr.type().id()==ID_c_bool) { const irep_idt &value=to_constant_expr(expr).get_value(); - dest.push_back(binary2integer(id2string(value), false)); + dest.push_back(bv2integer(id2string(value), false)); return; } else if(expr.type().id()==ID_bool) @@ -981,16 +981,16 @@ void interpretert::evaluate( } else if(expr.type().id()==ID_signedbv) { - const std::string s= - integer2binary(value, to_signedbv_type(expr.type()).get_width()); - dest.push_back(binary2integer(s, true)); + const std::string s = + integer2bv(value, to_signedbv_type(expr.type()).get_width()); + dest.push_back(bv2integer(s, true)); return; } else if(expr.type().id()==ID_unsignedbv) { - const std::string s= - integer2binary(value, to_unsignedbv_type(expr.type()).get_width()); - dest.push_back(binary2integer(s, false)); + const std::string s = + integer2bv(value, to_unsignedbv_type(expr.type()).get_width()); + dest.push_back(bv2integer(s, false)); return; } else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool)) diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index 90a958b50d0..1b66f9ab1ee 100644 --- a/src/util/arith_tools.cpp +++ b/src/util/arith_tools.cpp @@ -43,17 +43,17 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value) } else if(type_id==ID_unsignedbv) { - int_value=binary2integer(id2string(value), false); + int_value = bv2integer(id2string(value), false); return false; } else if(type_id==ID_signedbv) { - int_value=binary2integer(id2string(value), true); + int_value = bv2integer(id2string(value), true); return false; } else if(type_id==ID_c_bool) { - int_value=binary2integer(id2string(value), false); + int_value = bv2integer(id2string(value), false); return false; } else if(type_id==ID_c_enum) @@ -61,12 +61,12 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value) const typet &subtype=to_c_enum_type(type).subtype(); if(subtype.id()==ID_signedbv) { - int_value=binary2integer(id2string(value), true); + int_value = bv2integer(id2string(value), true); return false; } else if(subtype.id()==ID_unsignedbv) { - int_value=binary2integer(id2string(value), false); + int_value = bv2integer(id2string(value), false); return false; } } @@ -75,12 +75,12 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value) const typet &subtype=type.subtype(); if(subtype.id()==ID_signedbv) { - int_value=binary2integer(id2string(value), true); + int_value = bv2integer(id2string(value), true); return false; } else if(subtype.id()==ID_unsignedbv) { - int_value=binary2integer(id2string(value), false); + int_value = bv2integer(id2string(value), false); return false; } } @@ -123,28 +123,28 @@ constant_exprt from_integer( else if(type_id==ID_unsignedbv) { std::size_t width=to_unsignedbv_type(type).get_width(); - return constant_exprt(integer2binary(int_value, width), type); + return constant_exprt(integer2bv(int_value, width), type); } else if(type_id==ID_bv) { std::size_t width=to_bv_type(type).get_width(); - return constant_exprt(integer2binary(int_value, width), type); + return constant_exprt(integer2bv(int_value, width), type); } else if(type_id==ID_signedbv) { std::size_t width=to_signedbv_type(type).get_width(); - return constant_exprt(integer2binary(int_value, width), type); + return constant_exprt(integer2bv(int_value, width), type); } else if(type_id==ID_c_enum) { const std::size_t width = to_c_enum_type(type).subtype().get_size_t(ID_width); - return constant_exprt(integer2binary(int_value, width), type); + return constant_exprt(integer2bv(int_value, width), type); } else if(type_id==ID_c_bool) { std::size_t width=to_c_bool_type(type).get_width(); - return constant_exprt(integer2binary(int_value, width), type); + return constant_exprt(integer2bv(int_value, width), type); } else if(type_id==ID_bool) { @@ -162,7 +162,7 @@ constant_exprt from_integer( else if(type_id==ID_c_bit_field) { std::size_t width=to_c_bit_field_type(type).get_width(); - return constant_exprt(integer2binary(int_value, width), type); + return constant_exprt(integer2bv(int_value, width), type); } else if(type_id==ID_fixedbv) { diff --git a/src/util/bv_arithmetic.cpp b/src/util/bv_arithmetic.cpp index 107b9f1e434..38842e33ec3 100644 --- a/src/util/bv_arithmetic.cpp +++ b/src/util/bv_arithmetic.cpp @@ -84,7 +84,7 @@ mp_integer bv_arithmetict::pack() const exprt bv_arithmetict::to_expr() const { - return constant_exprt(integer2binary(value, spec.width), spec.to_type()); + return constant_exprt(integer2bv(value, spec.width), spec.to_type()); } bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other) @@ -184,5 +184,5 @@ void bv_arithmetict::from_expr(const exprt &expr) { PRECONDITION(expr.is_constant()); spec=bv_spect(expr.type()); - value=binary2integer(expr.get_string(ID_value), spec.is_signed); + value = bv2integer(expr.get_string(ID_value), spec.is_signed); } diff --git a/src/util/expr.cpp b/src/util/expr.cpp index c6024623501..a800ea15be0 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -245,7 +245,7 @@ bool exprt::is_one() const } else if(type_id==ID_unsignedbv || type_id==ID_signedbv) { - mp_integer int_value=binary2integer(value, false); + mp_integer int_value = bv2integer(value, false); if(int_value==1) return true; } diff --git a/src/util/fixedbv.cpp b/src/util/fixedbv.cpp index 2d4202b412f..5c5e48332ff 100644 --- a/src/util/fixedbv.cpp +++ b/src/util/fixedbv.cpp @@ -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=binary2integer(id2string(expr.get_value()), true); + v = bv2integer(id2string(expr.get_value()), true); } void fixedbvt::from_integer(const mp_integer &i) @@ -46,7 +46,7 @@ constant_exprt fixedbvt::to_expr() const type.set_width(spec.width); type.set_integer_bits(spec.integer_bits); PRECONDITION(spec.width != 0); - return constant_exprt(integer2binary(v, spec.width), type); + return constant_exprt(integer2bv(v, spec.width), type); } void fixedbvt::round(const fixedbv_spect &dest_spec) diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp index 1dd8c26657a..cbc363a33df 100644 --- a/src/util/ieee_float.cpp +++ b/src/util/ieee_float.cpp @@ -696,7 +696,7 @@ void ieee_floatt::divide_and_round( constant_exprt ieee_floatt::to_expr() const { - return constant_exprt(integer2binary(pack(), spec.width()), spec.to_type()); + return constant_exprt(integer2bv(pack(), spec.width()), spec.to_type()); } ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other) @@ -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(binary2integer(id2string(expr.get_value()), false)); + unpack(bv2integer(id2string(expr.get_value()), false)); } mp_integer ieee_floatt::to_integer() const diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp index 59199adb7a6..db65427d84e 100644 --- a/src/util/mp_arith.cpp +++ b/src/util/mp_arith.cpp @@ -185,6 +185,18 @@ const mp_integer binary2integer(const std::string &n, bool is_signed) #endif } +/// convert an integer to bit-vector representation with given width +const std::string integer2bv(const mp_integer &src, std::size_t width) +{ + return integer2binary(src, width); +} + +/// convert a bit-vector representation (possibly signed) to integer +const mp_integer bv2integer(const std::string &src, bool is_signed) +{ + return binary2integer(src, is_signed); +} + mp_integer::ullong_t integer2ulong(const mp_integer &n) { PRECONDITION(n.is_ulong()); diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h index d20bb33f29a..7ca97ec86b3 100644 --- a/src/util/mp_arith.h +++ b/src/util/mp_arith.h @@ -52,6 +52,12 @@ const mp_integer string2integer(const std::string &, unsigned base=10); const std::string integer2binary(const mp_integer &, std::size_t width); const mp_integer binary2integer(const std::string &, bool is_signed); +/// convert an integer to bit-vector representation with given width +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); + /// \deprecated use numeric_cast_v instead DEPRECATED("Use numeric_cast_v instead") mp_integer::ullong_t integer2ulong(const mp_integer &); diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 4a06c1d03c7..be8407ab1fc 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -677,7 +677,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr) expr_type_id==ID_signedbv || expr_type_id==ID_floatbv) { - mp_integer int_value=binary2integer(id2string(value), false); + mp_integer int_value = bv2integer(id2string(value), false); expr=from_integer(int_value, expr_type); return false; } @@ -832,8 +832,9 @@ bool simplify_exprt::simplify_if_implies( else if(type_id==ID_unsignedbv) { const mp_integer i1, i2; - if(binary2integer(cond.op1().get_string(ID_value), false)>= - binary2integer(expr.op1().get_string(ID_value), false)) + if( + bv2integer(cond.op1().get_string(ID_value), false) >= + bv2integer(expr.op1().get_string(ID_value), false)) { new_truth = true; return false; @@ -842,8 +843,9 @@ bool simplify_exprt::simplify_if_implies( else if(type_id==ID_signedbv) { const mp_integer i1, i2; - if(binary2integer(cond.op1().get_string(ID_value), true)>= - binary2integer(expr.op1().get_string(ID_value), true)) + if( + bv2integer(cond.op1().get_string(ID_value), true) >= + bv2integer(expr.op1().get_string(ID_value), true)) { new_truth = true; return false; @@ -868,8 +870,9 @@ bool simplify_exprt::simplify_if_implies( else if(type_id==ID_unsignedbv) { const mp_integer i1, i2; - if(binary2integer(cond.op1().get_string(ID_value), false)<= - binary2integer(expr.op1().get_string(ID_value), false)) + if( + bv2integer(cond.op1().get_string(ID_value), false) <= + bv2integer(expr.op1().get_string(ID_value), false)) { new_truth = true; return false; @@ -878,8 +881,9 @@ bool simplify_exprt::simplify_if_implies( else if(type_id==ID_signedbv) { const mp_integer i1, i2; - if(binary2integer(cond.op1().get_string(ID_value), true)<= - binary2integer(expr.op1().get_string(ID_value), true)) + if( + bv2integer(cond.op1().get_string(ID_value), true) <= + bv2integer(expr.op1().get_string(ID_value), true)) { new_truth = true; return false; diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 5762ad31dff..45306287761 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -821,7 +821,7 @@ bool simplify_exprt::simplify_bitwise(exprt &expr) } else if(expr.id()==ID_bitxor) { - constant_exprt new_op(integer2binary(0, width), expr.type()); + constant_exprt new_op(integer2bv(0, width), expr.type()); expr.swap(new_op); return false; } diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index f650ee0d124..0e145f310ee 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -387,7 +387,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr) else { // this is a pointer, we can't use to_integer - mp_integer number=binary2integer(id2string(c_ptr.get_value()), false); + mp_integer number = bv2integer(id2string(c_ptr.get_value()), false); // a null pointer would have been caught above, return value 0 // will indicate that conversion failed if(number==0)