36 std::vector<mp_integer> bytes;
39 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
40 bytes.push_back((value >> bit)%
power(2, bits_per_byte));
44 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
48 "bytes is not empty because we just pushed just as many elements on "
49 "top of it as we are popping now");
50 new_value+=bytes.back()<<bit;
72 type_id == ID_integer || type_id == ID_natural ||
73 type_id == ID_unsignedbv || type_id == ID_signedbv)
82 else if(type_id==ID_rational)
91 else if(type_id==ID_fixedbv)
98 else if(type_id==ID_floatbv)
121 type_id == ID_integer || type_id == ID_natural ||
122 type_id == ID_unsignedbv || type_id == ID_signedbv)
131 else if(type_id==ID_rational)
140 else if(type_id==ID_fixedbv)
147 else if(type_id==ID_floatbv)
168 bool no_change =
true;
171 exprt::operandst::iterator constant;
174 bool constant_found =
false;
179 for(exprt::operandst::iterator it = new_operands.begin();
180 it != new_operands.end();)
189 it->type().id()!=ID_floatbv)
195 bool do_erase =
false;
198 if(it->is_constant() && it->type()==expr.
type())
201 if(!c_sizeof_type.has_value())
203 const typet &sizeof_type =
204 static_cast<const typet &
>(it->find(ID_C_c_sizeof_type));
206 c_sizeof_type = sizeof_type;
219 constant_found =
true;
226 it = new_operands.erase(it);
233 if(c_sizeof_type.has_value())
237 "c_sizeof_type is only set to a non-nil value "
238 "if a constant has been found");
239 constant->set(ID_C_c_sizeof_type, *c_sizeof_type);
242 if(new_operands.size() == 1)
244 return new_operands.front();
249 if(constant_found && constant->is_one())
252 new_operands.erase(constant);
255 if(new_operands.size() == 1)
256 return new_operands.front();
265 tmp.
operands() = std::move(new_operands);
266 return std::move(tmp);
277 if(expr_type!=expr.
op0().
type() ||
283 if(expr_type.
id()==ID_signedbv ||
284 expr_type.
id()==ID_unsignedbv ||
285 expr_type.
id()==ID_natural ||
286 expr_type.
id()==ID_integer)
288 const auto int_value0 = numeric_cast<mp_integer>(expr.
op0());
289 const auto int_value1 = numeric_cast<mp_integer>(expr.
op1());
292 if(int_value1.has_value() && *int_value1 == 0)
296 if(int_value1.has_value() && *int_value1 == 1)
302 if(int_value0.has_value() && *int_value0 == 0)
307 if(int_value0.has_value() && int_value1.has_value())
309 mp_integer result = *int_value0 / *int_value1;
313 else if(expr_type.
id()==ID_rational)
321 if(ok1 && rat_value1.
is_zero())
324 if((ok1 && rat_value1.
is_one()) ||
336 return std::move(tmp);
339 else if(expr_type.
id()==ID_fixedbv)
369 if(expr.
type().
id()==ID_signedbv ||
370 expr.
type().
id()==ID_unsignedbv ||
371 expr.
type().
id()==ID_natural ||
372 expr.
type().
id()==ID_integer)
377 const auto int_value0 = numeric_cast<mp_integer>(expr.
op0());
378 const auto int_value1 = numeric_cast<mp_integer>(expr.
op1());
380 if(int_value1.has_value() && *int_value1 == 0)
384 (int_value1.has_value() && *int_value1 == 1) ||
385 (int_value0.has_value() && *int_value0 == 0))
390 if(int_value0.has_value() && int_value1.has_value())
392 mp_integer result = *int_value0 % *int_value1;
406 bool no_change =
true;
413 if(expr.
type().
id() == ID_floatbv)
418 const exprt::operandst::iterator next = std::next(it);
420 if(next != new_operands.end())
422 if(it->type()==next->type() &&
427 new_operands.erase(next);
438 expr.
op0().
id() == ID_plus && expr.
op0().
type().
id() == ID_pointer &&
443 if(op0.
op1().
id() == ID_plus)
458 if(
is_number(it->type()) && it->is_constant())
464 exprt::operandst::iterator const_sum;
465 bool const_sum_set=
false;
467 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
469 if(
is_number(it->type()) && it->is_constant())
491 typedef std::unordered_map<exprt, exprt::operandst::iterator, irep_hash>
495 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
496 if(it->id() == ID_unary_minus)
502 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
506 else if(it->id()==ID_unary_minus)
509 expr_mapt::iterator itm=expr_map.find(*it);
511 if(itm!=expr_map.end())
523 for(exprt::operandst::iterator it = new_operands.begin();
524 it != new_operands.end();
527 if(
is_number(it->type()) && it->is_zero())
529 it = new_operands.erase(it);
537 if(new_operands.empty())
541 else if(new_operands.size() == 1)
543 return new_operands.front();
551 tmp.
operands() = std::move(new_operands);
552 return std::move(tmp);
560 if(!
is_number(minus_expr.type()) && minus_expr.type().id() != ID_pointer)
575 minus_expr.type().id() == ID_pointer &&
576 operands[0].type().id() == ID_pointer &&
is_number(operands[1].type()))
586 is_number(minus_expr.type()) && operands[0].type().id() == ID_pointer &&
587 operands[1].type().id() == ID_pointer)
591 if(operands[0]==operands[1])
605 if(expr.
type().
id()!=ID_bool)
612 it->id() == ID_typecast &&
616 else if(it->is_zero() || it->is_one())
628 if(expr.
id()==ID_bitand)
630 else if(expr.
id()==ID_bitor)
632 else if(expr.
id()==ID_bitxor)
639 if(it->id()==ID_typecast)
641 else if(it->is_zero())
643 else if(it->is_one())
655 bool no_change =
true;
656 auto new_expr = expr;
662 while(new_expr.operands().size() >= 2)
664 if(!new_expr.op0().is_constant())
667 if(!new_expr.op1().is_constant())
670 if(new_expr.op0().type() != new_expr.type())
673 if(new_expr.op1().type() != new_expr.type())
679 std::function<bool(
bool,
bool)> f;
681 if(new_expr.id() == ID_bitand)
682 f = [](
bool a,
bool b) {
return a && b; };
683 else if(new_expr.id() == ID_bitor)
684 f = [](
bool a,
bool b) {
return a || b; };
685 else if(new_expr.id() == ID_bitxor)
686 f = [](
bool a,
bool b) {
return a != b; };
691 make_bvrep(width, [&a_val, &b_val, &width, &f](std::size_t i) {
699 new_expr.operands().erase(new_expr.operands().begin());
700 new_expr.op0().swap(new_op);
707 if(new_expr.id() == ID_bitor || new_expr.id() == ID_bitxor)
709 for(exprt::operandst::iterator it = new_expr.operands().begin();
710 it != new_expr.operands().end();)
712 if(it->is_zero() && new_expr.operands().size() > 1)
714 it = new_expr.operands().erase(it);
724 if(new_expr.id() == ID_bitand)
726 const auto all_ones =
power(2, width) - 1;
727 for(exprt::operandst::iterator it = new_expr.operands().begin();
728 it != new_expr.operands().end();)
734 new_expr.operands().size() > 1)
736 it = new_expr.operands().erase(it);
746 if(new_expr.operands().size() == 2 && new_expr.op0() == new_expr.op1())
748 if(new_expr.id() == ID_bitand || new_expr.id() == ID_bitor)
750 return new_expr.op0();
752 else if(new_expr.id() == ID_bitxor)
758 if(new_expr.operands().size() == 1)
759 return new_expr.op0();
764 return std::move(new_expr);
777 const auto index_converted_to_int = numeric_cast<mp_integer>(expr.
index());
779 !index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
780 *index_converted_to_int >= src_bit_width)
791 numeric_cast_v<std::size_t>(*index_converted_to_int));
799 bool no_change =
true;
811 const bool value = op.
is_true();
820 while(i < new_expr.
operands().size() - 1)
835 const auto new_width = width_i + width_n;
838 new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
853 else if(new_expr.
type().
id() == ID_verilog_unsignedbv)
858 while(i < new_expr.
operands().size() - 1)
865 (opi.
type().
id()==ID_verilog_unsignedbv ||
867 (opn.
type().
id()==ID_verilog_unsignedbv ||
871 const std::string new_value=
873 opi.
set(ID_value, new_value);
875 opi.
type().
id(ID_verilog_unsignedbv);
889 return new_expr.
op0();
895 return std::move(new_expr);
904 const auto distance = numeric_cast<mp_integer>(expr.
distance());
906 if(!distance.has_value())
912 auto value = numeric_cast<mp_integer>(expr.
op());
915 !value.has_value() && expr.
op().
type().
id() == ID_bv &&
916 expr.
op().
id() == ID_constant)
923 if(!value.has_value())
927 expr.
op().
type().
id() == ID_unsignedbv ||
932 if(expr.
id()==ID_lshr)
935 if(*distance >= width)
939 else if(*distance >= 0)
942 *value +=
power(2, width);
943 *value /=
power(2, *distance);
947 else if(expr.
id()==ID_ashr)
956 else if(expr.
id()==ID_shl)
959 if(*distance >= width)
963 else if(*distance >= 0)
965 *value *=
power(2, *distance);
973 if(expr.
id()==ID_lshr)
977 *value /=
power(2, *distance);
981 else if(expr.
id()==ID_ashr)
987 if(*value < 0 && new_value == 0)
993 else if(expr.
id()==ID_shl)
997 *value *=
power(2, *distance);
1012 const auto base = numeric_cast<mp_integer>(expr.
op0());
1013 const auto exponent = numeric_cast<mp_integer>(expr.
op1());
1015 if(!base.has_value())
1018 if(!exponent.has_value())
1038 const auto start = numeric_cast<mp_integer>(expr.
upper());
1039 const auto end = numeric_cast<mp_integer>(expr.
lower());
1041 if(!start.has_value())
1044 if(!end.has_value())
1049 if(!width.has_value())
1052 if(*start < 0 || *start >= (*width) || *end < 0 || *end >= (*width))
1055 DATA_INVARIANT(*start >= *end,
"extractbits must have upper() >= lower()");
1061 if(!svalue.has_value() || svalue->size() != *width)
1064 std::string extracted_value = svalue->substr(
1065 numeric_cast_v<std::size_t>(*end),
1066 numeric_cast_v<std::size_t>(*start - *end + 1));
1068 auto result =
bits2expr(extracted_value, expr.
type(),
true);
1069 if(!result.has_value())
1072 return std::move(*result);
1074 else if(expr.
src().
id() == ID_concatenation)
1084 if(!op_width.has_value() || *op_width <= 0)
1087 if(*start + 1 == offset && *end + *op_width == offset)
1093 return std::move(tmp);
1096 offset -= *op_width;
1116 const exprt &operand = expr.
op();
1121 if(operand.
id()==ID_unary_minus)
1129 else if(operand.
id()==ID_constant)
1134 if(type_id==ID_integer ||
1135 type_id==ID_signedbv ||
1136 type_id==ID_unsignedbv)
1138 const auto int_value = numeric_cast<mp_integer>(constant_expr);
1140 if(!int_value.has_value())
1145 else if(type_id==ID_rational)
1153 else if(type_id==ID_fixedbv)
1159 else if(type_id==ID_floatbv)
1175 const auto &type = expr.
type();
1178 type.id() == ID_bv || type.id() == ID_unsignedbv ||
1179 type.id() == ID_signedbv)
1183 if(op.
type() == type)
1185 if(op.
id()==ID_constant)
1188 const auto new_value =
1189 make_bvrep(width, [&value, &width](std::size_t i) {
1204 if(expr.
type().
id()!=ID_bool)
1215 if((expr.
id()==ID_equal || expr.
id()==ID_notequal) &&
1219 auto new_expr = expr;
1220 new_expr.
op0().
swap(new_expr.op1());
1224 if(tmp0.
id()==ID_if && tmp0.
operands().size()==3)
1236 (tmp0.
id() == ID_address_of ||
1237 (tmp0.
id() == ID_typecast &&
1239 (tmp1.
id() == ID_address_of ||
1240 (tmp1.
id() == ID_typecast &&
1242 (expr.
id() == ID_equal || expr.
id() == ID_notequal))
1247 if(tmp0.
id()==ID_pointer_object &&
1248 tmp1.
id()==ID_pointer_object &&
1249 (expr.
id()==ID_equal || expr.
id()==ID_notequal))
1254 if(tmp0.
type().
id()==ID_c_enum_tag)
1257 if(tmp1.
type().
id()==ID_c_enum_tag)
1264 if(tmp0_const && tmp1_const)
1274 if(expr.
id()==ID_ge)
1276 else if(expr.
id()==ID_le)
1278 else if(expr.
id()==ID_gt)
1280 else if(expr.
id()==ID_lt)
1308 if(tmp0.
type().
id() == ID_c_enum_tag)
1311 if(tmp1.
type().
id() == ID_c_enum_tag)
1317 if(expr.
id() == ID_equal || expr.
id() == ID_notequal)
1321 bool equal = (tmp0_const.get_value() == tmp1_const.get_value());
1323 !equal && tmp0_const.type().id() == ID_pointer &&
1324 tmp1_const.type().id() == ID_pointer)
1328 tmp1_const.get_value() == ID_NULL))
1334 equal = tmp0_const.is_zero() && tmp1_const.is_zero();
1339 if(tmp0.
type().
id() == ID_fixedbv)
1344 if(expr.
id() == ID_ge)
1346 else if(expr.
id() == ID_le)
1348 else if(expr.
id() == ID_gt)
1350 else if(expr.
id() == ID_lt)
1355 else if(tmp0.
type().
id() == ID_floatbv)
1360 if(expr.
id() == ID_ge)
1362 else if(expr.
id() == ID_le)
1364 else if(expr.
id() == ID_gt)
1366 else if(expr.
id() == ID_lt)
1371 else if(tmp0.
type().
id() == ID_rational)
1381 if(expr.
id() == ID_ge)
1383 else if(expr.
id() == ID_le)
1385 else if(expr.
id() == ID_gt)
1387 else if(expr.
id() == ID_lt)
1394 const auto v0 = numeric_cast<mp_integer>(tmp0_const);
1399 const auto v1 = numeric_cast<mp_integer>(tmp1_const);
1404 if(expr.
id() == ID_ge)
1406 else if(expr.
id() == ID_le)
1408 else if(expr.
id() == ID_gt)
1410 else if(expr.
id() == ID_lt)
1430 if(op0.
id()==ID_plus)
1432 bool no_change =
true;
1440 else if(op1.
id()==ID_plus)
1442 bool no_change =
true;
1453 op0.
type().
id()!=ID_complex)
1471 if(expr.
op0().
type().
id() == ID_floatbv)
1475 if(expr.
id()==ID_notequal)
1477 auto new_rel_expr = expr;
1478 new_rel_expr.
id(ID_equal);
1482 else if(expr.
id()==ID_gt)
1484 auto new_rel_expr = expr;
1485 new_rel_expr.
id(ID_ge);
1487 new_rel_expr.lhs().
swap(new_rel_expr.rhs());
1491 else if(expr.
id()==ID_lt)
1493 auto new_rel_expr = expr;
1494 new_rel_expr.
id(ID_ge);
1498 else if(expr.
id()==ID_le)
1500 auto new_rel_expr = expr;
1501 new_rel_expr.
id(ID_ge);
1503 new_rel_expr.lhs().
swap(new_rel_expr.rhs());
1510 expr.
id() == ID_ge || expr.
id() == ID_equal,
1511 "we previously converted all other cases to >= or ==");
1515 if(expr.
op0() == expr.
op1())
1540 if(expr.
id()==ID_ge)
1541 tmp=(int_value0>=int_value1);
1542 else if(expr.
id()==ID_equal)
1543 tmp=(int_value0==int_value1);
1555 else if(result!=tmp)
1570 if(expr.
id()==ID_equal)
1606 if(expr.
id()==ID_notequal)
1608 auto new_rel_expr = expr;
1609 new_rel_expr.
id(ID_equal);
1615 if(expr.
id()==ID_equal &&
1617 expr.
op1().
get(ID_value)==ID_NULL)
1621 if(expr.
op0().
id() == ID_address_of)
1626 object.
id() == ID_symbol ||
object.
id() == ID_dynamic_object ||
1627 object.
id() == ID_member ||
object.
id() == ID_index ||
1628 object.
id() == ID_string_constant)
1634 expr.
op0().
id() == ID_typecast &&
1638 const auto &
object =
1642 object.
id() == ID_symbol ||
object.
id() == ID_dynamic_object ||
1643 object.
id() == ID_member ||
object.
id() == ID_index ||
1644 object.
id() == ID_string_constant)
1650 expr.
op0().
id() == ID_typecast &&
1658 auto new_expr = expr;
1660 if(new_expr.op0().type().id() != ID_pointer)
1661 new_expr.op1() =
from_integer(0, new_expr.op0().type());
1663 new_expr.op1().type() = new_expr.op0().type();
1674 if(expr.
op0().
id()==ID_plus)
1678 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1681 bool op_changed =
false;
1682 auto new_expr = expr;
1686 if(it->is_constant())
1704 new_expr.op1() =
from_integer(i, new_expr.op1().type());
1717 expr.
op0().
id() == ID_typecast && expr.
op0().
type().
id() == ID_floatbv &&
1724 ieee_floatt const_val_converted_back=const_val_converted;
1727 if(const_val_converted_back==const_val)
1732 return std::move(result);
1741 if(expr.
id()==ID_ge &&
1748 auto new_expr = expr;
1751 if(expr.
id()==ID_equal)
1754 if(operand.
id()==ID_unary_minus)
1757 return std::move(new_expr);
1759 else if(operand.
id()==ID_plus)
1764 if(operand_plus_expr.operands().size() == 2)
1767 if(operand_plus_expr.op0().id() == ID_unary_minus)
1768 operand_plus_expr.op0().swap(operand_plus_expr.op1());
1770 if(operand_plus_expr.op1().id() == ID_unary_minus)
1773 operand_plus_expr.op0(),
1785 expr.
op0().
id() == ID_typecast &&
1799 return lhs_typecast_op;
1803 #define NORMALISE_CONSTANT_TESTS
1804 #ifdef NORMALISE_CONSTANT_TESTS
1806 if(expr.
op0().
type().
id()==ID_unsignedbv ||
1811 if(expr.
id()==ID_notequal)
1813 auto new_rel_expr = expr;
1814 new_rel_expr.
id(ID_equal);
1818 else if(expr.
id()==ID_gt)
1827 auto new_expr = expr;
1830 new_expr.op1() =
from_integer(i, new_expr.op1().type());
1833 else if(expr.
id()==ID_lt)
1835 auto new_rel_expr = expr;
1836 new_rel_expr.
id(ID_ge);
1840 else if(expr.
id()==ID_le)
1849 auto new_rel_expr = expr;
1850 new_rel_expr.
id(ID_ge);
1852 new_rel_expr.op1() =
from_integer(i, new_rel_expr.op1().type());