38 std::vector<mp_integer> bytes;
41 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
42 bytes.push_back((value >> bit)%
power(2, bits_per_byte));
46 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
50 "bytes is not empty because we just pushed just as many elements on "
51 "top of it as we are popping now");
52 new_value+=bytes.back()<<bit;
74 type_id == ID_integer || type_id == ID_natural ||
75 type_id == ID_unsignedbv || type_id == ID_signedbv)
84 else if(type_id==ID_rational)
93 else if(type_id==ID_fixedbv)
100 else if(type_id==ID_floatbv)
123 type_id == ID_integer || type_id == ID_natural ||
124 type_id == ID_unsignedbv || type_id == ID_signedbv)
133 else if(type_id==ID_rational)
142 else if(type_id==ID_fixedbv)
149 else if(type_id==ID_floatbv)
170 bool no_change =
true;
173 exprt::operandst::iterator constant;
176 bool constant_found =
false;
181 for(exprt::operandst::iterator it = new_operands.begin();
182 it != new_operands.end();)
191 it->type().id()!=ID_floatbv)
197 bool do_erase =
false;
200 if(it->is_constant() && it->type()==expr.
type())
203 if(!c_sizeof_type.has_value())
205 const typet &sizeof_type =
206 static_cast<const typet &
>(it->find(ID_C_c_sizeof_type));
208 c_sizeof_type = sizeof_type;
221 constant_found =
true;
228 it = new_operands.erase(it);
235 if(c_sizeof_type.has_value())
239 "c_sizeof_type is only set to a non-nil value "
240 "if a constant has been found");
241 constant->set(ID_C_c_sizeof_type, *c_sizeof_type);
244 if(new_operands.size() == 1)
246 return new_operands.front();
251 if(constant_found && constant->is_one())
254 new_operands.erase(constant);
257 if(new_operands.size() == 1)
258 return new_operands.front();
267 tmp.
operands() = std::move(new_operands);
268 return std::move(tmp);
279 if(expr_type!=expr.
op0().
type() ||
285 if(expr_type.
id()==ID_signedbv ||
286 expr_type.
id()==ID_unsignedbv ||
287 expr_type.
id()==ID_natural ||
288 expr_type.
id()==ID_integer)
290 const auto int_value0 = numeric_cast<mp_integer>(expr.
op0());
291 const auto int_value1 = numeric_cast<mp_integer>(expr.
op1());
294 if(int_value1.has_value() && *int_value1 == 0)
298 if(int_value1.has_value() && *int_value1 == 1)
304 if(int_value0.has_value() && *int_value0 == 0)
309 if(int_value0.has_value() && int_value1.has_value())
311 mp_integer result = *int_value0 / *int_value1;
315 else if(expr_type.
id()==ID_rational)
323 if(ok1 && rat_value1.
is_zero())
326 if((ok1 && rat_value1.
is_one()) ||
338 return std::move(tmp);
341 else if(expr_type.
id()==ID_fixedbv)
371 if(expr.
type().
id()==ID_signedbv ||
372 expr.
type().
id()==ID_unsignedbv ||
373 expr.
type().
id()==ID_natural ||
374 expr.
type().
id()==ID_integer)
379 const auto int_value0 = numeric_cast<mp_integer>(expr.
op0());
380 const auto int_value1 = numeric_cast<mp_integer>(expr.
op1());
382 if(int_value1.has_value() && *int_value1 == 0)
386 (int_value1.has_value() && *int_value1 == 1) ||
387 (int_value0.has_value() && *int_value0 == 0))
392 if(int_value0.has_value() && int_value1.has_value())
394 mp_integer result = *int_value0 % *int_value1;
408 bool no_change =
true;
415 if(expr.
type().
id() == ID_floatbv)
420 const exprt::operandst::iterator next = std::next(it);
422 if(next != new_operands.end())
424 if(it->type()==next->type() &&
429 new_operands.erase(next);
440 expr.
op0().
id() == ID_plus && expr.
op0().
type().
id() == ID_pointer &&
445 if(op0.
op1().
id() == ID_plus)
460 if(
is_number(it->type()) && it->is_constant())
466 exprt::operandst::iterator const_sum;
467 bool const_sum_set=
false;
469 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
471 if(
is_number(it->type()) && it->is_constant())
493 typedef std::unordered_map<exprt, exprt::operandst::iterator, irep_hash>
497 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
498 if(it->id() == ID_unary_minus)
504 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
508 else if(it->id()==ID_unary_minus)
511 expr_mapt::iterator itm=expr_map.find(*it);
513 if(itm!=expr_map.end())
525 for(exprt::operandst::iterator it = new_operands.begin();
526 it != new_operands.end();
529 if(
is_number(it->type()) && it->is_zero())
531 it = new_operands.erase(it);
539 if(new_operands.empty())
543 else if(new_operands.size() == 1)
545 return new_operands.front();
553 tmp.
operands() = std::move(new_operands);
554 return std::move(tmp);
562 if(!
is_number(minus_expr.type()) && minus_expr.type().id() != ID_pointer)
577 minus_expr.type().id() == ID_pointer &&
578 operands[0].type().id() == ID_pointer &&
is_number(operands[1].type()))
588 is_number(minus_expr.type()) && operands[0].type().id() == ID_pointer &&
589 operands[1].type().id() == ID_pointer)
593 if(operands[0]==operands[1])
607 if(expr.
type().
id()!=ID_bool)
614 it->id() == ID_typecast &&
618 else if(it->is_zero() || it->is_one())
630 if(expr.
id()==ID_bitand)
632 else if(expr.
id()==ID_bitor)
634 else if(expr.
id()==ID_bitxor)
641 if(it->id()==ID_typecast)
643 else if(it->is_zero())
645 else if(it->is_one())
657 bool no_change =
true;
658 auto new_expr = expr;
664 while(new_expr.operands().size() >= 2)
666 if(!new_expr.op0().is_constant())
669 if(!new_expr.op1().is_constant())
672 if(new_expr.op0().type() != new_expr.type())
675 if(new_expr.op1().type() != new_expr.type())
681 std::function<bool(
bool,
bool)> f;
683 if(new_expr.id() == ID_bitand)
684 f = [](
bool a,
bool b) {
return a && b; };
685 else if(new_expr.id() == ID_bitor)
686 f = [](
bool a,
bool b) {
return a || b; };
687 else if(new_expr.id() == ID_bitxor)
688 f = [](
bool a,
bool b) {
return a != b; };
693 make_bvrep(width, [&a_val, &b_val, &width, &f](std::size_t i) {
701 new_expr.operands().erase(new_expr.operands().begin());
702 new_expr.op0().swap(new_op);
709 if(new_expr.id() == ID_bitor || new_expr.id() == ID_bitxor)
711 for(exprt::operandst::iterator it = new_expr.operands().begin();
712 it != new_expr.operands().end();)
714 if(it->is_zero() && new_expr.operands().size() > 1)
716 it = new_expr.operands().erase(it);
720 it->is_constant() && it->type().id() == ID_bv &&
722 new_expr.operands().size() > 1)
724 it = new_expr.operands().erase(it);
734 if(new_expr.id() == ID_bitand)
736 const auto all_ones =
power(2, width) - 1;
737 for(exprt::operandst::iterator it = new_expr.operands().begin();
738 it != new_expr.operands().end();)
744 new_expr.operands().size() > 1)
746 it = new_expr.operands().erase(it);
756 if(new_expr.operands().size() == 2 && new_expr.op0() == new_expr.op1())
758 if(new_expr.id() == ID_bitand || new_expr.id() == ID_bitor)
760 return new_expr.op0();
762 else if(new_expr.id() == ID_bitxor)
768 if(new_expr.operands().size() == 1)
769 return new_expr.op0();
774 return std::move(new_expr);
787 const auto index_converted_to_int = numeric_cast<mp_integer>(expr.
index());
789 !index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
790 *index_converted_to_int >= src_bit_width)
801 numeric_cast_v<std::size_t>(*index_converted_to_int));
809 bool no_change =
true;
821 const bool value = op.
is_true();
830 while(i < new_expr.
operands().size() - 1)
845 const auto new_width = width_i + width_n;
848 new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
863 else if(new_expr.
type().
id() == ID_verilog_unsignedbv)
868 while(i < new_expr.
operands().size() - 1)
875 (opi.
type().
id()==ID_verilog_unsignedbv ||
877 (opn.
type().
id()==ID_verilog_unsignedbv ||
881 const std::string new_value=
883 opi.
set(ID_value, new_value);
885 opi.
type().
id(ID_verilog_unsignedbv);
899 return new_expr.
op0();
905 return std::move(new_expr);
914 const auto distance = numeric_cast<mp_integer>(expr.
distance());
916 if(!distance.has_value())
922 auto value = numeric_cast<mp_integer>(expr.
op());
925 !value.has_value() && expr.
op().
type().
id() == ID_bv &&
926 expr.
op().
id() == ID_constant)
933 if(!value.has_value())
937 expr.
op().
type().
id() == ID_unsignedbv ||
942 if(expr.
id()==ID_lshr)
945 if(*distance >= width)
949 else if(*distance >= 0)
952 *value +=
power(2, width);
953 *value /=
power(2, *distance);
957 else if(expr.
id()==ID_ashr)
966 else if(expr.
id()==ID_shl)
969 if(*distance >= width)
973 else if(*distance >= 0)
975 *value *=
power(2, *distance);
983 if(expr.
id()==ID_lshr)
987 *value /=
power(2, *distance);
991 else if(expr.
id()==ID_ashr)
997 if(*value < 0 && new_value == 0)
1003 else if(expr.
id()==ID_shl)
1007 *value *=
power(2, *distance);
1022 const auto base = numeric_cast<mp_integer>(expr.
op0());
1023 const auto exponent = numeric_cast<mp_integer>(expr.
op1());
1025 if(!base.has_value())
1028 if(!exponent.has_value())
1048 const auto start = numeric_cast<mp_integer>(expr.
upper());
1049 const auto end = numeric_cast<mp_integer>(expr.
lower());
1051 if(!start.has_value())
1054 if(!end.has_value())
1059 if(!width.has_value())
1062 if(*start < 0 || *start >= (*width) || *end < 0 || *end >= (*width))
1065 DATA_INVARIANT(*start >= *end,
"extractbits must have upper() >= lower()");
1071 if(!svalue.has_value() || svalue->size() != *width)
1074 std::string extracted_value = svalue->substr(
1075 numeric_cast_v<std::size_t>(*end),
1076 numeric_cast_v<std::size_t>(*start - *end + 1));
1079 if(!result.has_value())
1082 return std::move(*result);
1084 else if(expr.
src().
id() == ID_concatenation)
1094 if(!op_width.has_value() || *op_width <= 0)
1097 if(*start + 1 == offset && *end + *op_width == offset)
1103 return std::move(tmp);
1106 offset -= *op_width;
1126 const exprt &operand = expr.
op();
1131 if(operand.
id()==ID_unary_minus)
1139 else if(operand.
id()==ID_constant)
1144 if(type_id==ID_integer ||
1145 type_id==ID_signedbv ||
1146 type_id==ID_unsignedbv)
1148 const auto int_value = numeric_cast<mp_integer>(constant_expr);
1150 if(!int_value.has_value())
1155 else if(type_id==ID_rational)
1163 else if(type_id==ID_fixedbv)
1169 else if(type_id==ID_floatbv)
1185 const auto &type = expr.
type();
1188 type.id() == ID_bv || type.id() == ID_unsignedbv ||
1189 type.id() == ID_signedbv)
1193 if(op.
type() == type)
1195 if(op.
id()==ID_constant)
1198 const auto new_value =
1199 make_bvrep(width, [&value, &width](std::size_t i) {
1214 if(expr.
type().
id()!=ID_bool)
1225 if((expr.
id()==ID_equal || expr.
id()==ID_notequal) &&
1229 auto new_expr = expr;
1230 new_expr.
op0().
swap(new_expr.op1());
1234 if(tmp0.
id()==ID_if && tmp0.
operands().size()==3)
1252 if(tmp0.
id()==ID_pointer_object &&
1253 tmp1.
id()==ID_pointer_object &&
1254 (expr.
id()==ID_equal || expr.
id()==ID_notequal))
1259 if(tmp0.
type().
id()==ID_c_enum_tag)
1262 if(tmp1.
type().
id()==ID_c_enum_tag)
1269 if(tmp0_const && tmp1_const)
1279 if(expr.
id()==ID_ge)
1281 else if(expr.
id()==ID_le)
1283 else if(expr.
id()==ID_gt)
1285 else if(expr.
id()==ID_lt)
1313 if(tmp0.
type().
id() == ID_c_enum_tag)
1316 if(tmp1.
type().
id() == ID_c_enum_tag)
1322 if(expr.
id() == ID_equal || expr.
id() == ID_notequal)
1326 bool equal = (tmp0_const.get_value() == tmp1_const.get_value());
1328 !equal && tmp0_const.type().id() == ID_pointer &&
1329 tmp1_const.type().id() == ID_pointer)
1333 tmp1_const.get_value() == ID_NULL))
1339 equal = tmp0_const.is_zero() && tmp1_const.is_zero();
1344 if(tmp0.
type().
id() == ID_fixedbv)
1349 if(expr.
id() == ID_ge)
1351 else if(expr.
id() == ID_le)
1353 else if(expr.
id() == ID_gt)
1355 else if(expr.
id() == ID_lt)
1360 else if(tmp0.
type().
id() == ID_floatbv)
1365 if(expr.
id() == ID_ge)
1367 else if(expr.
id() == ID_le)
1369 else if(expr.
id() == ID_gt)
1371 else if(expr.
id() == ID_lt)
1376 else if(tmp0.
type().
id() == ID_rational)
1386 if(expr.
id() == ID_ge)
1388 else if(expr.
id() == ID_le)
1390 else if(expr.
id() == ID_gt)
1392 else if(expr.
id() == ID_lt)
1399 const auto v0 = numeric_cast<mp_integer>(tmp0_const);
1404 const auto v1 = numeric_cast<mp_integer>(tmp1_const);
1409 if(expr.
id() == ID_ge)
1411 else if(expr.
id() == ID_le)
1413 else if(expr.
id() == ID_gt)
1415 else if(expr.
id() == ID_lt)
1433 if(op0.
id()==ID_plus)
1435 bool no_change =
true;
1443 else if(op1.
id()==ID_plus)
1445 bool no_change =
true;
1456 op0.
type().
id()!=ID_complex)
1474 if(expr.
op0().
type().
id() == ID_floatbv)
1478 if(expr.
id()==ID_notequal)
1480 auto new_rel_expr = expr;
1481 new_rel_expr.
id(ID_equal);
1485 else if(expr.
id()==ID_gt)
1487 auto new_rel_expr = expr;
1488 new_rel_expr.
id(ID_ge);
1490 new_rel_expr.lhs().
swap(new_rel_expr.rhs());
1494 else if(expr.
id()==ID_lt)
1496 auto new_rel_expr = expr;
1497 new_rel_expr.
id(ID_ge);
1501 else if(expr.
id()==ID_le)
1503 auto new_rel_expr = expr;
1504 new_rel_expr.
id(ID_ge);
1506 new_rel_expr.lhs().
swap(new_rel_expr.rhs());
1513 expr.
id() == ID_ge || expr.
id() == ID_equal,
1514 "we previously converted all other cases to >= or ==");
1518 if(expr.
op0() == expr.
op1())
1523 if(expr.
id()==ID_equal)
1559 if(expr.
id()==ID_notequal)
1561 auto new_rel_expr = expr;
1562 new_rel_expr.
id(ID_equal);
1568 if(expr.
id()==ID_equal &&
1570 expr.
op1().
get(ID_value)==ID_NULL)
1574 if(expr.
op0().
id() == ID_address_of)
1579 object.
id() == ID_symbol ||
object.
id() == ID_dynamic_object ||
1580 object.
id() == ID_member ||
object.
id() == ID_index ||
1581 object.
id() == ID_string_constant)
1587 expr.
op0().
id() == ID_typecast &&
1591 const auto &
object =
1595 object.
id() == ID_symbol ||
object.
id() == ID_dynamic_object ||
1596 object.
id() == ID_member ||
object.
id() == ID_index ||
1597 object.
id() == ID_string_constant)
1603 expr.
op0().
id() == ID_typecast && expr.
op0().
type().
id() == ID_pointer)
1607 op.
type().
id() != ID_pointer &&
1609 op.
type().
id() == ID_complex))
1616 auto new_expr = expr;
1618 if(new_expr.op0().type().id() != ID_pointer)
1619 new_expr.op1() =
from_integer(0, new_expr.op0().type());
1621 new_expr.op1().type() = new_expr.op0().type();
1632 if(expr.
op0().
id()==ID_plus)
1636 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1639 bool op_changed =
false;
1640 auto new_expr = expr;
1644 if(it->is_constant())
1662 new_expr.op1() =
from_integer(i, new_expr.op1().type());
1675 expr.
op0().
id() == ID_typecast && expr.
op0().
type().
id() == ID_floatbv &&
1682 ieee_floatt const_val_converted_back=const_val_converted;
1685 if(const_val_converted_back==const_val)
1690 return std::move(result);
1699 if(expr.
id()==ID_ge &&
1706 auto new_expr = expr;
1709 if(expr.
id()==ID_equal)
1712 if(operand.
id()==ID_unary_minus)
1715 return std::move(new_expr);
1717 else if(operand.
id()==ID_plus)
1722 if(operand_plus_expr.operands().size() == 2)
1725 if(operand_plus_expr.op0().id() == ID_unary_minus)
1726 operand_plus_expr.op0().swap(operand_plus_expr.op1());
1728 if(operand_plus_expr.op1().id() == ID_unary_minus)
1731 operand_plus_expr.op0(),
1743 expr.
op0().
id() == ID_typecast &&
1757 return lhs_typecast_op;
1761 #define NORMALISE_CONSTANT_TESTS
1762 #ifdef NORMALISE_CONSTANT_TESTS
1764 if(expr.
op0().
type().
id()==ID_unsignedbv ||
1769 if(expr.
id()==ID_notequal)
1771 auto new_rel_expr = expr;
1772 new_rel_expr.
id(ID_equal);
1776 else if(expr.
id()==ID_gt)
1785 auto new_expr = expr;
1788 new_expr.op1() =
from_integer(i, new_expr.op1().type());
1791 else if(expr.
id()==ID_lt)
1793 auto new_rel_expr = expr;
1794 new_rel_expr.
id(ID_ge);
1798 else if(expr.
id()==ID_le)
1807 auto new_rel_expr = expr;
1808 new_rel_expr.
id(ID_ge);
1810 new_rel_expr.op1() =
from_integer(i, new_rel_expr.op1().type());