From e6943dfe8229ec7f8a1451cd2c70285a510bedfc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 26 Feb 2021 23:50:18 +0000 Subject: [PATCH] Simplify overflow-* expressions We can simplify these over constants and for some trivial cases when mathematical types are used. --- regression/ansi-c/simplify-overflow/main.c | 14 ++ regression/ansi-c/simplify-overflow/test.desc | 7 + src/util/simplify_expr.cpp | 121 ++++++++++++++++++ src/util/simplify_expr_class.h | 10 ++ 4 files changed, 152 insertions(+) create mode 100644 regression/ansi-c/simplify-overflow/main.c create mode 100644 regression/ansi-c/simplify-overflow/test.desc diff --git a/regression/ansi-c/simplify-overflow/main.c b/regression/ansi-c/simplify-overflow/main.c new file mode 100644 index 00000000000..5d9e000e0eb --- /dev/null +++ b/regression/ansi-c/simplify-overflow/main.c @@ -0,0 +1,14 @@ +#ifdef _MSC_VER +# define _Static_assert static_assert +#endif + +int main() +{ + _Static_assert(!__CPROVER_overflow_plus(1, 2), ""); + _Static_assert(__CPROVER_overflow_minus(1U, 2U), ""); + _Static_assert(__CPROVER_overflow_minus(0U, 2U), ""); + _Static_assert(!__CPROVER_overflow_mult(1U, 2U), ""); + _Static_assert(!__CPROVER_overflow_shl(1, 2), ""); + _Static_assert(!__CPROVER_overflow_unary_minus(1), ""); + _Static_assert(__CPROVER_overflow_unary_minus(1U), ""); +} diff --git a/regression/ansi-c/simplify-overflow/test.desc b/regression/ansi-c/simplify-overflow/test.desc new file mode 100644 index 00000000000..932cbf87ce3 --- /dev/null +++ b/regression/ansi-c/simplify-overflow/test.desc @@ -0,0 +1,7 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index dbb4ec89d49..cde9744f17d 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2047,6 +2047,117 @@ simplify_exprt::simplify_complex(const unary_exprt &expr) return unchanged(expr); } +simplify_exprt::resultt<> +simplify_exprt::simplify_overflow_binary(const binary_exprt &expr) +{ + // zero is a neutral element for all operations supported here + if( + expr.op1().is_zero() || + (expr.op0().is_zero() && expr.id() != ID_overflow_minus)) + { + return false_exprt{}; + } + + // we only handle the case of same operand types + if(expr.op0().type() != expr.op1().type()) + return unchanged(expr); + + // catch some cases over mathematical types + const irep_idt &op_type_id = expr.op0().type().id(); + if( + op_type_id == ID_integer || op_type_id == ID_rational || + op_type_id == ID_real) + { + return false_exprt{}; + } + + if(op_type_id == ID_natural && expr.id() != ID_overflow_minus) + return false_exprt{}; + + // we only handle constants over signedbv/unsignedbv for the remaining cases + if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv) + return unchanged(expr); + + if(!expr.op0().is_constant() || !expr.op1().is_constant()) + return unchanged(expr); + + const auto op0_value = numeric_cast(expr.op0()); + const auto op1_value = numeric_cast(expr.op1()); + if(!op0_value.has_value() || !op1_value.has_value()) + return unchanged(expr); + + mp_integer no_overflow_result; + if(expr.id() == ID_overflow_plus) + no_overflow_result = *op0_value + *op1_value; + else if(expr.id() == ID_overflow_minus) + no_overflow_result = *op0_value - *op1_value; + else if(expr.id() == ID_overflow_mult) + no_overflow_result = *op0_value * *op1_value; + else if(expr.id() == ID_overflow_shl) + no_overflow_result = *op0_value << *op1_value; + else + UNREACHABLE; + + const std::size_t width = to_bitvector_type(expr.op0().type()).get_width(); + const integer_bitvector_typet bv_type{op_type_id, width}; + if( + no_overflow_result < bv_type.smallest() || + no_overflow_result > bv_type.largest()) + { + return true_exprt{}; + } + else + return false_exprt{}; +} + +simplify_exprt::resultt<> +simplify_exprt::simplify_overflow_unary(const unary_exprt &expr) +{ + // zero is a neutral element for all operations supported here + if(expr.op().is_zero()) + return false_exprt{}; + + // catch some cases over mathematical types + const irep_idt &op_type_id = expr.op().type().id(); + if( + op_type_id == ID_integer || op_type_id == ID_rational || + op_type_id == ID_real) + { + return false_exprt{}; + } + + if(op_type_id == ID_natural) + return true_exprt{}; + + // we only handle constants over signedbv/unsignedbv for the remaining cases + if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv) + return unchanged(expr); + + if(!expr.op().is_constant()) + return unchanged(expr); + + const auto op_value = numeric_cast(expr.op()); + if(!op_value.has_value()) + return unchanged(expr); + + mp_integer no_overflow_result; + if(expr.id() == ID_overflow_unary_minus) + no_overflow_result = -*op_value; + else + UNREACHABLE; + + const std::size_t width = to_bitvector_type(expr.op().type()).get_width(); + const integer_bitvector_typet bv_type{op_type_id, width}; + if( + no_overflow_result < bv_type.smallest() || + no_overflow_result > bv_type.largest()) + { + return true_exprt{}; + } + else + return false_exprt{}; +} + bool simplify_exprt::simplify_node_preorder(exprt &expr) { bool result=true; @@ -2290,6 +2401,16 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node) { r = simplify_complex(to_unary_expr(expr)); } + else if( + expr.id() == ID_overflow_plus || expr.id() == ID_overflow_minus || + expr.id() == ID_overflow_mult || expr.id() == ID_overflow_shl) + { + r = simplify_overflow_binary(to_binary_expr(expr)); + } + else if(expr.id() == ID_overflow_unary_minus) + { + r = simplify_overflow_unary(to_unary_expr(expr)); + } if(!no_change_join_operands) r = changed(r); diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index cccc06f70c7..fde630a11bf 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -185,6 +185,16 @@ class simplify_exprt NODISCARD resultt<> simplify_popcount(const popcount_exprt &); NODISCARD resultt<> simplify_complex(const unary_exprt &); + /// Try to simplify overflow-+, overflow-*, overflow--, overflow-shl. + /// Simplification will be possible when the operands are constants or the + /// types of the operands have infinite domains. + NODISCARD resultt<> simplify_overflow_binary(const binary_exprt &); + + /// Try to simplify overflow-unary-. + /// Simplification will be possible when the operand is constants or the + /// type of the operand has an infinite domain. + NODISCARD resultt<> simplify_overflow_unary(const unary_exprt &); + /// Attempt to simplify mathematical function applications if we have /// enough information to do so. Currently focused on constant comparisons. NODISCARD resultt<>