From 1f1df4271645323c184c8e278cc5227f62bb656f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 4 Oct 2018 13:59:42 +0100 Subject: [PATCH 1/3] added fixedbvt::operator+= and fixedbvt::operator-= --- src/util/fixedbv.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/util/fixedbv.cpp b/src/util/fixedbv.cpp index 02b441badb4..2d4202b412f 100644 --- a/src/util/fixedbv.cpp +++ b/src/util/fixedbv.cpp @@ -106,6 +106,18 @@ fixedbvt &fixedbvt::operator*=(const fixedbvt &o) return *this; } +fixedbvt &fixedbvt::operator+=(const fixedbvt &o) +{ + v += o.v; + return *this; +} + +fixedbvt &fixedbvt::operator-=(const fixedbvt &o) +{ + v -= o.v; + return *this; +} + fixedbvt &fixedbvt::operator/=(const fixedbvt &o) { v*=power(2, o.spec.get_fraction_bits()); From 4b5c41b8cb357e53794a969c38238937527e75d1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 4 Oct 2018 14:00:29 +0100 Subject: [PATCH 2/3] cleanup sum_expr to use higher level functions --- src/util/simplify_expr_int.cpp | 33 ++++++++++++++------------------- 1 file changed, 14 insertions(+), 19 deletions(-) diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index de7c9a539fd..d40d354045f 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -70,12 +70,16 @@ static bool sum_expr( const irep_idt &type_id=dest.type().id(); - if(type_id==ID_integer || type_id==ID_natural) + if( + type_id == ID_integer || type_id == ID_natural || + type_id == ID_unsignedbv || type_id == ID_signedbv) { - dest.set_value(integer2string( - string2integer(id2string(dest.get_value()))+ - string2integer(id2string(expr.get_value())))); - return false; + mp_integer a, b; + if(!to_integer(dest, a) && !to_integer(expr, b)) + { + dest = from_integer(a + b, dest.type()); + return false; + } } else if(type_id==ID_rational) { @@ -86,26 +90,17 @@ static bool sum_expr( return false; } } - else if(type_id==ID_unsignedbv || type_id==ID_signedbv) - { - dest.set_value(integer2binary( - binary2integer(id2string(dest.get_value()), false)+ - binary2integer(id2string(expr.get_value()), false), - to_bitvector_type(dest.type()).get_width())); - return false; - } else if(type_id==ID_fixedbv) { - dest.set_value(integer2binary( - binary2integer(id2string(dest.get_value()), false)+ - binary2integer(id2string(expr.get_value()), false), - to_bitvector_type(dest.type()).get_width())); + fixedbvt f(dest); + f += fixedbvt(expr); + dest = f.to_expr(); return false; } else if(type_id==ID_floatbv) { - ieee_floatt f(to_constant_expr(dest)); - f+=ieee_floatt(to_constant_expr(expr)); + ieee_floatt f(dest); + f += ieee_floatt(expr); dest=f.to_expr(); return false; } From b7caa0a256d6b1ec13337629a93477ddc34835bb Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 4 Oct 2018 14:01:26 +0100 Subject: [PATCH 3/3] cleanup mul_expr to use higher level functions --- src/util/simplify_expr_int.cpp | 23 +++++++++-------------- 1 file changed, 9 insertions(+), 14 deletions(-) diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index d40d354045f..5762ad31dff 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -119,12 +119,16 @@ static bool mul_expr( const irep_idt &type_id=dest.type().id(); - if(type_id==ID_integer || type_id==ID_natural) + if( + type_id == ID_integer || type_id == ID_natural || + type_id == ID_unsignedbv || type_id == ID_signedbv) { - dest.set_value(integer2string( - string2integer(id2string(dest.get_value()))* - string2integer(id2string(expr.get_value())))); - return false; + mp_integer a, b; + if(!to_integer(dest, a) && !to_integer(expr, b)) + { + dest = from_integer(a * b, dest.type()); + return false; + } } else if(type_id==ID_rational) { @@ -135,15 +139,6 @@ static bool mul_expr( return false; } } - else if(type_id==ID_unsignedbv || type_id==ID_signedbv) - { - // the following works for signed and unsigned integers - dest.set_value(integer2binary( - binary2integer(id2string(dest.get_value()), false)* - binary2integer(id2string(expr.get_value()), false), - to_bitvector_type(dest.type()).get_width())); - return false; - } else if(type_id==ID_fixedbv) { fixedbvt f(to_constant_expr(dest));