From b091560e84767d6927b46788a660eca94179d4f3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 15 Apr 2018 19:50:34 +0100 Subject: [PATCH 1/2] Typing and refactoring of simplify_extractbits --- src/util/simplify_expr.cpp | 2 +- src/util/simplify_expr_class.h | 3 ++- src/util/simplify_expr_int.cpp | 46 ++++++++++++++++++---------------- 3 files changed, 28 insertions(+), 23 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index b27daf59570..4a0e2855d29 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2317,7 +2317,7 @@ bool simplify_exprt::simplify_node(exprt &expr) else if(expr.id()==ID_concatenation) result=simplify_concatenation(expr) && result; else if(expr.id()==ID_extractbits) - result=simplify_extractbits(expr) && result; + result = simplify_extractbits(to_extractbits_expr(expr)) && result; else if(expr.id()==ID_ieee_float_equal || expr.id()==ID_ieee_float_notequal) result=simplify_ieee_float_relation(expr) && result; diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index a89134433b2..a1760e72a9b 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -28,6 +28,7 @@ class bswap_exprt; class byte_extract_exprt; class byte_update_exprt; class exprt; +class extractbits_exprt; class if_exprt; class index_exprt; class member_exprt; @@ -66,7 +67,7 @@ class simplify_exprt bool simplify_typecast(exprt &expr); bool simplify_extractbit(exprt &expr); - bool simplify_extractbits(exprt &expr); + bool simplify_extractbits(extractbits_exprt &expr); bool simplify_concatenation(exprt &expr); bool simplify_mult(exprt &expr); bool simplify_div(exprt &expr); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 9e941f58083..6dfb50d0679 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -18,7 +18,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr_util.h" #include "fixedbv.h" #include "ieee_float.h" +#include "invariant.h" #include "namespace.h" +#include "pointer_offset_size.h" #include "rational.h" #include "rational_tools.h" #include "std_expr.h" @@ -1101,45 +1103,47 @@ bool simplify_exprt::simplify_power(exprt &expr) } /// Simplifies extracting of bits from a constant. -bool simplify_exprt::simplify_extractbits(exprt &expr) +bool simplify_exprt::simplify_extractbits(extractbits_exprt &expr) { - assert(expr.operands().size()==3); - - const typet &op0_type=expr.op0().type(); + const typet &op0_type = expr.src().type(); if(!is_bitvector_type(op0_type) && !is_bitvector_type(expr.type())) return true; - if(expr.op0().is_constant()) - { - std::size_t width=to_bitvector_type(op0_type).get_width(); - mp_integer start, end; + mp_integer start, end; - if(to_integer(expr.op1(), start)) - return true; + if(to_integer(expr.upper(), start)) + return true; - if(to_integer(expr.op2(), end)) - return true; + if(to_integer(expr.lower(), end)) + return true; - if(start<0 || start>=width || - end<0 || end>=width) - return true; + const mp_integer width = pointer_offset_bits(op0_type, ns); - assert(start>=end); // is this always the case?? + if(start < 0 || start >= width || end < 0 || end >= width) + return true; - const irep_idt &value=expr.op0().get(ID_value); + DATA_INVARIANT( + start >= end, + "extractbits must have upper() >= lower()"); + + if(expr.src().is_constant()) + { + const irep_idt &value = to_constant_expr(expr.src()).get_value(); if(value.size()!=width) return true; std::string svalue=id2string(value); - std::string extracted_value= - svalue.substr(width-integer2size_t(start)-1, - integer2size_t(start-end+1)); + std::string extracted_value = + svalue.substr( + integer2size_t(width - start - 1), + integer2size_t(start - end + 1)); - expr = constant_exprt(extracted_value, expr.type()); + constant_exprt result(extracted_value, expr.type()); + expr.swap(result); return false; } From b6637343d3d1dcdc7b483c36f8416e191362a3ed Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 15 Apr 2018 19:50:58 +0100 Subject: [PATCH 2/2] Simplify extractbits(concatenation(...)) --- src/util/simplify_expr_int.cpp | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 6dfb50d0679..c225997d2c8 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1147,6 +1147,32 @@ bool simplify_exprt::simplify_extractbits(extractbits_exprt &expr) return false; } + else if(expr.src().id() == ID_concatenation) + { + // the most-significant bit comes first in an concatenation_exprt, hence we + // count down + mp_integer offset = width; + + forall_operands(it, expr.src()) + { + mp_integer op_width = pointer_offset_bits(it->type(), ns); + + if(op_width <= 0) + return true; + + if(start + 1 == offset && end + op_width == offset) + { + exprt tmp = *it; + if(tmp.type() != expr.type()) + return true; + + expr.swap(tmp); + return false; + } + + offset -= op_width; + } + } return true; }