From e884c434ba407c3fc7773f33e2c2b7a559cdc1b3 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 23 Mar 2022 12:12:44 +0000 Subject: [PATCH 1/5] Split `convert_overflow` into binary and unary variations Because the code used for one operand vs two operands is slightly different and because this facilitates a more type-specific implementation. --- src/solvers/flattening/boolbv.cpp | 12 +++++++++--- src/solvers/flattening/boolbv.h | 5 ++++- src/solvers/flattening/boolbv_overflow.cpp | 10 ++++++++-- 3 files changed, 21 insertions(+), 6 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index a22d0b89ea0..5b1621c7543 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -417,10 +417,16 @@ literalt boolbvt::convert_rest(const exprt &expr) else if(expr.id()==ID_onehot || expr.id()==ID_onehot0) return convert_onehot(to_unary_expr(expr)); else if( - can_cast_expr(expr) || - can_cast_expr(expr)) + const auto binary_overflow = + expr_try_dynamic_cast(expr)) { - return convert_overflow(expr); + return convert_binary_overflow(*binary_overflow); + } + else if( + const auto unary_overflow = + expr_try_dynamic_cast(expr)) + { + return convert_unary_overflow(*unary_overflow); } else if(expr.id()==ID_isnan) { diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 3670171fe8b..7b1e83f37b1 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "arrays.h" class array_comprehension_exprt; +class binary_overflow_exprt; class bitreverse_exprt; class bswap_exprt; class byte_extract_exprt; @@ -38,6 +39,7 @@ class floatbv_typecast_exprt; class ieee_float_op_exprt; class member_exprt; class replication_exprt; +class unary_overflow_exprt; class union_typet; class boolbvt:public arrayst @@ -140,7 +142,8 @@ class boolbvt:public arrayst virtual literalt convert_reduction(const unary_exprt &expr); virtual literalt convert_onehot(const unary_exprt &expr); virtual literalt convert_extractbit(const extractbit_exprt &expr); - virtual literalt convert_overflow(const exprt &expr); + virtual literalt convert_binary_overflow(const binary_overflow_exprt &expr); + virtual literalt convert_unary_overflow(const unary_overflow_exprt &expr); virtual literalt convert_equality(const equal_exprt &expr); virtual literalt convert_verilog_case_equality( const binary_relation_exprt &expr); diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp index a8794987de0..b4cabaa04fe 100644 --- a/src/solvers/flattening/boolbv_overflow.cpp +++ b/src/solvers/flattening/boolbv_overflow.cpp @@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -literalt boolbvt::convert_overflow(const exprt &expr) +literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) { const auto plus_or_minus_conversion = [&]( @@ -161,7 +161,13 @@ literalt boolbvt::convert_overflow(const exprt &expr) return prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), overflow)); } - else if( + + return SUB::convert_rest(expr); +} + +literalt boolbvt::convert_unary_overflow(const unary_overflow_exprt &expr) +{ + if( const auto unary_minus_overflow = expr_try_dynamic_cast(expr)) { From c0797f971db1cceaa5ccefa44b0f03a806384736 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 23 Mar 2022 15:07:11 +0000 Subject: [PATCH 2/5] Factor out conversion of operands for `binary_overflow_exprt` --- src/solvers/flattening/boolbv_overflow.cpp | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp index b4cabaa04fe..0b8ecaa2819 100644 --- a/src/solvers/flattening/boolbv_overflow.cpp +++ b/src/solvers/flattening/boolbv_overflow.cpp @@ -13,14 +13,19 @@ Author: Daniel Kroening, kroening@kroening.com literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) { + const bvt &bv0 = convert_bv(expr.lhs()); + const bvt &bv1 = convert_bv( + expr.rhs(), + can_cast_expr(expr) + ? optionalt{bv0.size()} + : nullopt); + const auto plus_or_minus_conversion = [&]( const binary_overflow_exprt &overflow_expr, const std::function &bv_util_overflow) { - const bvt &bv0 = convert_bv(overflow_expr.lhs()); - const bvt &bv1 = convert_bv(overflow_expr.rhs()); if(bv0.size() != bv1.size()) return SUB::convert_rest(expr); @@ -49,9 +54,6 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) mult_overflow->lhs().type().id() != ID_signedbv) return SUB::convert_rest(expr); - bvt bv0 = convert_bv(mult_overflow->lhs()); - bvt bv1 = convert_bv(mult_overflow->rhs(), bv0.size()); - bv_utilst::representationt rep = mult_overflow->lhs().type().id() == ID_signedbv ? bv_utilst::representationt::SIGNED @@ -65,10 +67,10 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) std::size_t new_size=old_size*2; // sign/zero extension - bv0=bv_utils.extension(bv0, new_size, rep); - bv1=bv_utils.extension(bv1, new_size, rep); + const bvt &bv0_extended = bv_utils.extension(bv0, new_size, rep); + const bvt &bv1_extended = bv_utils.extension(bv1, new_size, rep); - bvt result=bv_utils.multiplier(bv0, bv1, rep); + bvt result = bv_utils.multiplier(bv0_extended, bv1_extended, rep); if(rep==bv_utilst::representationt::UNSIGNED) { @@ -100,9 +102,6 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) else if( const auto shl_overflow = expr_try_dynamic_cast(expr)) { - const bvt &bv0 = convert_bv(shl_overflow->lhs()); - const bvt &bv1 = convert_bv(shl_overflow->rhs()); - std::size_t old_size = bv0.size(); std::size_t new_size = old_size * 2; From 9b1a3885c1235db0867f077596f708a497e34c9b Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 23 Mar 2022 15:18:34 +0000 Subject: [PATCH 3/5] Factor out working out signedness in `convert_binary_overflow` --- src/solvers/flattening/boolbv_overflow.cpp | 20 +++++--------------- 1 file changed, 5 insertions(+), 15 deletions(-) diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp index 0b8ecaa2819..379fe2b6552 100644 --- a/src/solvers/flattening/boolbv_overflow.cpp +++ b/src/solvers/flattening/boolbv_overflow.cpp @@ -20,6 +20,11 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) ? optionalt{bv0.size()} : nullopt); + const bv_utilst::representationt rep = + expr.lhs().type().id() == ID_signedbv + ? bv_utilst::representationt::SIGNED + : bv_utilst::representationt::UNSIGNED; + const auto plus_or_minus_conversion = [&]( const binary_overflow_exprt &overflow_expr, @@ -30,11 +35,6 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) if(bv0.size() != bv1.size()) return SUB::convert_rest(expr); - bv_utilst::representationt rep = - overflow_expr.lhs().type().id() == ID_signedbv - ? bv_utilst::representationt::SIGNED - : bv_utilst::representationt::UNSIGNED; - return bv_util_overflow(&bv_utils, bv0, bv1, rep); }; if( @@ -54,11 +54,6 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) mult_overflow->lhs().type().id() != ID_signedbv) return SUB::convert_rest(expr); - bv_utilst::representationt rep = - mult_overflow->lhs().type().id() == ID_signedbv - ? bv_utilst::representationt::SIGNED - : bv_utilst::representationt::UNSIGNED; - DATA_INVARIANT( mult_overflow->lhs().type() == mult_overflow->rhs().type(), "operands of overflow_mult expression shall have same type"); @@ -105,11 +100,6 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) std::size_t old_size = bv0.size(); std::size_t new_size = old_size * 2; - bv_utilst::representationt rep = - shl_overflow->lhs().type().id() == ID_signedbv - ? bv_utilst::representationt::SIGNED - : bv_utilst::representationt::UNSIGNED; - bvt bv_ext=bv_utils.extension(bv0, new_size, rep); bvt result=bv_utils.shift(bv_ext, bv_utilst::shiftt::SHIFT_LEFT, bv1); From c5c5e91af36aabebcf83d588cf48ec6b3b862cca Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 23 Mar 2022 15:26:09 +0000 Subject: [PATCH 4/5] Use can_cast_type inplace of type id in `convert_binary_overflow` --- src/solvers/flattening/boolbv_overflow.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp index 379fe2b6552..3050c45d176 100644 --- a/src/solvers/flattening/boolbv_overflow.cpp +++ b/src/solvers/flattening/boolbv_overflow.cpp @@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include +#include #include #include "boolbv.h" @@ -21,7 +22,7 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) : nullopt); const bv_utilst::representationt rep = - expr.lhs().type().id() == ID_signedbv + can_cast_type(expr.lhs().type()) ? bv_utilst::representationt::SIGNED : bv_utilst::representationt::UNSIGNED; @@ -50,9 +51,11 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) const auto mult_overflow = expr_try_dynamic_cast(expr)) { if( - mult_overflow->lhs().type().id() != ID_unsignedbv && - mult_overflow->lhs().type().id() != ID_signedbv) + !can_cast_type(expr.lhs().type()) && + !can_cast_type(expr.lhs().type())) + { return SUB::convert_rest(expr); + } DATA_INVARIANT( mult_overflow->lhs().type() == mult_overflow->rhs().type(), @@ -105,7 +108,7 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) bvt result=bv_utils.shift(bv_ext, bv_utilst::shiftt::SHIFT_LEFT, bv1); // a negative shift is undefined; yet this isn't an overflow - literalt neg_shift = shl_overflow->lhs().type().id() == ID_unsignedbv + literalt neg_shift = rep == bv_utilst::representationt::UNSIGNED ? const_literal(false) : bv1.back(); // sign bit From fad0e203e078d842931cf63d70232b72b77d3eee Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 23 Mar 2022 15:42:45 +0000 Subject: [PATCH 5/5] Remove lambda in `convert_binary_overflow` --- src/solvers/flattening/boolbv_overflow.cpp | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp index 3050c45d176..44fd3f7d1f9 100644 --- a/src/solvers/flattening/boolbv_overflow.cpp +++ b/src/solvers/flattening/boolbv_overflow.cpp @@ -26,26 +26,20 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) ? bv_utilst::representationt::SIGNED : bv_utilst::representationt::UNSIGNED; - const auto plus_or_minus_conversion = - [&]( - const binary_overflow_exprt &overflow_expr, - const std::function - &bv_util_overflow) { - - if(bv0.size() != bv1.size()) - return SUB::convert_rest(expr); - - return bv_util_overflow(&bv_utils, bv0, bv1, rep); - }; if( const auto plus_overflow = expr_try_dynamic_cast(expr)) { - return plus_or_minus_conversion(*plus_overflow, &bv_utilst::overflow_add); + if(bv0.size() != bv1.size()) + return SUB::convert_rest(expr); + + return bv_utils.overflow_add(bv0, bv1, rep); } if(const auto minus = expr_try_dynamic_cast(expr)) { - return plus_or_minus_conversion(*minus, &bv_utilst::overflow_sub); + if(bv0.size() != bv1.size()) + return SUB::convert_rest(expr); + + return bv_utils.overflow_sub(bv0, bv1, rep); } else if( const auto mult_overflow = expr_try_dynamic_cast(expr))