37 std::vector<mp_integer> bytes;
40 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
41 bytes.push_back((value >> bit)%
power(2, bits_per_byte));
45 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
49 "bytes is not empty because we just pushed just as many elements on "
50 "top of it as we are popping now");
51 new_value+=bytes.back()<<bit;
73 type_id == ID_integer || type_id == ID_natural ||
74 type_id == ID_unsignedbv || type_id == ID_signedbv)
83 else if(type_id==ID_rational)
92 else if(type_id==ID_fixedbv)
99 else if(type_id==ID_floatbv)
122 type_id == ID_integer || type_id == ID_natural ||
123 type_id == ID_unsignedbv || type_id == ID_signedbv)
132 else if(type_id==ID_rational)
141 else if(type_id==ID_fixedbv)
148 else if(type_id==ID_floatbv)
169 bool no_change =
true;
172 exprt::operandst::iterator constant;
175 bool constant_found =
false;
180 for(exprt::operandst::iterator it = new_operands.begin();
181 it != new_operands.end();)
190 it->type().id()!=ID_floatbv)
196 bool do_erase =
false;
199 if(it->is_constant() && it->type()==expr.
type())
202 if(!c_sizeof_type.has_value())
204 const typet &sizeof_type =
205 static_cast<const typet &
>(it->find(ID_C_c_sizeof_type));
207 c_sizeof_type = sizeof_type;
220 constant_found =
true;
227 it = new_operands.erase(it);
234 if(c_sizeof_type.has_value())
238 "c_sizeof_type is only set to a non-nil value "
239 "if a constant has been found");
240 constant->set(ID_C_c_sizeof_type, *c_sizeof_type);
243 if(new_operands.size() == 1)
245 return new_operands.front();
250 if(constant_found && constant->is_one())
253 new_operands.erase(constant);
256 if(new_operands.size() == 1)
257 return new_operands.front();
266 tmp.
operands() = std::move(new_operands);
267 return std::move(tmp);
278 if(expr_type!=expr.
op0().
type() ||
284 if(expr_type.
id()==ID_signedbv ||
285 expr_type.
id()==ID_unsignedbv ||
286 expr_type.
id()==ID_natural ||
287 expr_type.
id()==ID_integer)
289 const auto int_value0 = numeric_cast<mp_integer>(expr.
op0());
290 const auto int_value1 = numeric_cast<mp_integer>(expr.
op1());
293 if(int_value1.has_value() && *int_value1 == 0)
297 if(int_value1.has_value() && *int_value1 == 1)
303 if(int_value0.has_value() && *int_value0 == 0)
308 if(int_value0.has_value() && int_value1.has_value())
310 mp_integer result = *int_value0 / *int_value1;
314 else if(expr_type.
id()==ID_rational)
322 if(ok1 && rat_value1.
is_zero())
325 if((ok1 && rat_value1.
is_one()) ||
337 return std::move(tmp);
340 else if(expr_type.
id()==ID_fixedbv)
370 if(expr.
type().
id()==ID_signedbv ||
371 expr.
type().
id()==ID_unsignedbv ||
372 expr.
type().
id()==ID_natural ||
373 expr.
type().
id()==ID_integer)
378 const auto int_value0 = numeric_cast<mp_integer>(expr.
op0());
379 const auto int_value1 = numeric_cast<mp_integer>(expr.
op1());
381 if(int_value1.has_value() && *int_value1 == 0)
385 (int_value1.has_value() && *int_value1 == 1) ||
386 (int_value0.has_value() && *int_value0 == 0))
391 if(int_value0.has_value() && int_value1.has_value())
393 mp_integer result = *int_value0 % *int_value1;
407 bool no_change =
true;
414 if(expr.
type().
id() == ID_floatbv)
419 const exprt::operandst::iterator next = std::next(it);
421 if(next != new_operands.end())
423 if(it->type()==next->type() &&
428 new_operands.erase(next);
439 expr.
op0().
id() == ID_plus && expr.
op0().
type().
id() == ID_pointer &&
444 if(op0.
op1().
id() == ID_plus)
459 if(
is_number(it->type()) && it->is_constant())
465 exprt::operandst::iterator const_sum;
466 bool const_sum_set=
false;
468 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
470 if(
is_number(it->type()) && it->is_constant())
492 typedef std::unordered_map<exprt, exprt::operandst::iterator, irep_hash>
496 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
497 if(it->id() == ID_unary_minus)
503 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
507 else if(it->id()==ID_unary_minus)
510 expr_mapt::iterator itm=expr_map.find(*it);
512 if(itm!=expr_map.end())
524 for(exprt::operandst::iterator it = new_operands.begin();
525 it != new_operands.end();
528 if(
is_number(it->type()) && it->is_zero())
530 it = new_operands.erase(it);
538 if(new_operands.empty())
542 else if(new_operands.size() == 1)
544 return new_operands.front();
552 tmp.
operands() = std::move(new_operands);
553 return std::move(tmp);
561 if(!
is_number(minus_expr.type()) && minus_expr.type().id() != ID_pointer)
576 minus_expr.type().id() == ID_pointer &&
577 operands[0].type().id() == ID_pointer &&
is_number(operands[1].type()))
587 is_number(minus_expr.type()) && operands[0].type().id() == ID_pointer &&
588 operands[1].type().id() == ID_pointer)
592 if(operands[0]==operands[1])
606 if(expr.
type().
id()!=ID_bool)
613 it->id() == ID_typecast &&
617 else if(it->is_zero() || it->is_one())
629 if(expr.
id()==ID_bitand)
631 else if(expr.
id()==ID_bitor)
633 else if(expr.
id()==ID_bitxor)
640 if(it->id()==ID_typecast)
642 else if(it->is_zero())
644 else if(it->is_one())
656 bool no_change =
true;
657 auto new_expr = expr;
663 while(new_expr.operands().size() >= 2)
665 if(!new_expr.op0().is_constant())
668 if(!new_expr.op1().is_constant())
671 if(new_expr.op0().type() != new_expr.type())
674 if(new_expr.op1().type() != new_expr.type())
680 std::function<bool(
bool,
bool)> f;
682 if(new_expr.id() == ID_bitand)
683 f = [](
bool a,
bool b) {
return a && b; };
684 else if(new_expr.id() == ID_bitor)
685 f = [](
bool a,
bool b) {
return a || b; };
686 else if(new_expr.id() == ID_bitxor)
687 f = [](
bool a,
bool b) {
return a != b; };
692 make_bvrep(width, [&a_val, &b_val, &width, &f](std::size_t i) {
700 new_expr.operands().erase(new_expr.operands().begin());
701 new_expr.op0().swap(new_op);
708 if(new_expr.id() == ID_bitor || new_expr.id() == ID_bitxor)
710 for(exprt::operandst::iterator it = new_expr.operands().begin();
711 it != new_expr.operands().end();)
713 if(it->is_zero() && new_expr.operands().size() > 1)
715 it = new_expr.operands().erase(it);
725 if(new_expr.id() == ID_bitand)
727 const auto all_ones =
power(2, width) - 1;
728 for(exprt::operandst::iterator it = new_expr.operands().begin();
729 it != new_expr.operands().end();)
735 new_expr.operands().size() > 1)
737 it = new_expr.operands().erase(it);
747 if(new_expr.operands().size() == 2 && new_expr.op0() == new_expr.op1())
749 if(new_expr.id() == ID_bitand || new_expr.id() == ID_bitor)
751 return new_expr.op0();
753 else if(new_expr.id() == ID_bitxor)
759 if(new_expr.operands().size() == 1)
760 return new_expr.op0();
765 return std::move(new_expr);
778 const auto index_converted_to_int = numeric_cast<mp_integer>(expr.
index());
780 !index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
781 *index_converted_to_int >= src_bit_width)
792 numeric_cast_v<std::size_t>(*index_converted_to_int));
800 bool no_change =
true;
812 const bool value = op.
is_true();
821 while(i < new_expr.
operands().size() - 1)
836 const auto new_width = width_i + width_n;
839 new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
854 else if(new_expr.
type().
id() == ID_verilog_unsignedbv)
859 while(i < new_expr.
operands().size() - 1)
866 (opi.
type().
id()==ID_verilog_unsignedbv ||
868 (opn.
type().
id()==ID_verilog_unsignedbv ||
872 const std::string new_value=
874 opi.
set(ID_value, new_value);
876 opi.
type().
id(ID_verilog_unsignedbv);
890 return new_expr.
op0();
896 return std::move(new_expr);
905 const auto distance = numeric_cast<mp_integer>(expr.
distance());
907 if(!distance.has_value())
913 auto value = numeric_cast<mp_integer>(expr.
op());
916 !value.has_value() && expr.
op().
type().
id() == ID_bv &&
917 expr.
op().
id() == ID_constant)
924 if(!value.has_value())
928 expr.
op().
type().
id() == ID_unsignedbv ||
933 if(expr.
id()==ID_lshr)
936 if(*distance >= width)
940 else if(*distance >= 0)
943 *value +=
power(2, width);
944 *value /=
power(2, *distance);
948 else if(expr.
id()==ID_ashr)
957 else if(expr.
id()==ID_shl)
960 if(*distance >= width)
964 else if(*distance >= 0)
966 *value *=
power(2, *distance);
974 if(expr.
id()==ID_lshr)
978 *value /=
power(2, *distance);
982 else if(expr.
id()==ID_ashr)
988 if(*value < 0 && new_value == 0)
994 else if(expr.
id()==ID_shl)
998 *value *=
power(2, *distance);
1013 const auto base = numeric_cast<mp_integer>(expr.
op0());
1014 const auto exponent = numeric_cast<mp_integer>(expr.
op1());
1016 if(!base.has_value())
1019 if(!exponent.has_value())
1039 const auto start = numeric_cast<mp_integer>(expr.
upper());
1040 const auto end = numeric_cast<mp_integer>(expr.
lower());
1042 if(!start.has_value())
1045 if(!end.has_value())
1050 if(!width.has_value())
1053 if(*start < 0 || *start >= (*width) || *end < 0 || *end >= (*width))
1056 DATA_INVARIANT(*start >= *end,
"extractbits must have upper() >= lower()");
1062 if(!svalue.has_value() || svalue->size() != *width)
1065 std::string extracted_value = svalue->substr(
1066 numeric_cast_v<std::size_t>(*end),
1067 numeric_cast_v<std::size_t>(*start - *end + 1));
1070 if(!result.has_value())
1073 return std::move(*result);
1075 else if(expr.
src().
id() == ID_concatenation)
1085 if(!op_width.has_value() || *op_width <= 0)
1088 if(*start + 1 == offset && *end + *op_width == offset)
1094 return std::move(tmp);
1097 offset -= *op_width;
1117 const exprt &operand = expr.
op();
1122 if(operand.
id()==ID_unary_minus)
1130 else if(operand.
id()==ID_constant)
1135 if(type_id==ID_integer ||
1136 type_id==ID_signedbv ||
1137 type_id==ID_unsignedbv)
1139 const auto int_value = numeric_cast<mp_integer>(constant_expr);
1141 if(!int_value.has_value())
1146 else if(type_id==ID_rational)
1154 else if(type_id==ID_fixedbv)
1160 else if(type_id==ID_floatbv)
1176 const auto &type = expr.
type();
1179 type.id() == ID_bv || type.id() == ID_unsignedbv ||
1180 type.id() == ID_signedbv)
1184 if(op.
type() == type)
1186 if(op.
id()==ID_constant)
1189 const auto new_value =
1190 make_bvrep(width, [&value, &width](std::size_t i) {
1205 if(expr.
type().
id()!=ID_bool)
1216 if((expr.
id()==ID_equal || expr.
id()==ID_notequal) &&
1220 auto new_expr = expr;
1221 new_expr.
op0().
swap(new_expr.op1());
1225 if(tmp0.
id()==ID_if && tmp0.
operands().size()==3)
1237 (tmp0.
id() == ID_address_of ||
1238 (tmp0.
id() == ID_typecast &&
1240 (tmp1.
id() == ID_address_of ||
1241 (tmp1.
id() == ID_typecast &&
1243 (expr.
id() == ID_equal || expr.
id() == ID_notequal))
1248 if(tmp0.
id()==ID_pointer_object &&
1249 tmp1.
id()==ID_pointer_object &&
1250 (expr.
id()==ID_equal || expr.
id()==ID_notequal))
1255 if(tmp0.
type().
id()==ID_c_enum_tag)
1258 if(tmp1.
type().
id()==ID_c_enum_tag)
1265 if(tmp0_const && tmp1_const)
1275 if(expr.
id()==ID_ge)
1277 else if(expr.
id()==ID_le)
1279 else if(expr.
id()==ID_gt)
1281 else if(expr.
id()==ID_lt)
1309 if(tmp0.
type().
id() == ID_c_enum_tag)
1312 if(tmp1.
type().
id() == ID_c_enum_tag)
1318 if(expr.
id() == ID_equal || expr.
id() == ID_notequal)
1322 bool equal = (tmp0_const.get_value() == tmp1_const.get_value());
1324 !equal && tmp0_const.type().id() == ID_pointer &&
1325 tmp1_const.type().id() == ID_pointer)
1329 tmp1_const.get_value() == ID_NULL))
1335 equal = tmp0_const.is_zero() && tmp1_const.is_zero();
1340 if(tmp0.
type().
id() == ID_fixedbv)
1345 if(expr.
id() == ID_ge)
1347 else if(expr.
id() == ID_le)
1349 else if(expr.
id() == ID_gt)
1351 else if(expr.
id() == ID_lt)
1356 else if(tmp0.
type().
id() == ID_floatbv)
1361 if(expr.
id() == ID_ge)
1363 else if(expr.
id() == ID_le)
1365 else if(expr.
id() == ID_gt)
1367 else if(expr.
id() == ID_lt)
1372 else if(tmp0.
type().
id() == ID_rational)
1382 if(expr.
id() == ID_ge)
1384 else if(expr.
id() == ID_le)
1386 else if(expr.
id() == ID_gt)
1388 else if(expr.
id() == ID_lt)
1395 const auto v0 = numeric_cast<mp_integer>(tmp0_const);
1400 const auto v1 = numeric_cast<mp_integer>(tmp1_const);
1405 if(expr.
id() == ID_ge)
1407 else if(expr.
id() == ID_le)
1409 else if(expr.
id() == ID_gt)
1411 else if(expr.
id() == ID_lt)
1429 if(op0.
id()==ID_plus)
1431 bool no_change =
true;
1439 else if(op1.
id()==ID_plus)
1441 bool no_change =
true;
1452 op0.
type().
id()!=ID_complex)
1470 if(expr.
op0().
type().
id() == ID_floatbv)
1474 if(expr.
id()==ID_notequal)
1476 auto new_rel_expr = expr;
1477 new_rel_expr.
id(ID_equal);
1481 else if(expr.
id()==ID_gt)
1483 auto new_rel_expr = expr;
1484 new_rel_expr.
id(ID_ge);
1486 new_rel_expr.lhs().
swap(new_rel_expr.rhs());
1490 else if(expr.
id()==ID_lt)
1492 auto new_rel_expr = expr;
1493 new_rel_expr.
id(ID_ge);
1497 else if(expr.
id()==ID_le)
1499 auto new_rel_expr = expr;
1500 new_rel_expr.
id(ID_ge);
1502 new_rel_expr.lhs().
swap(new_rel_expr.rhs());
1509 expr.
id() == ID_ge || expr.
id() == ID_equal,
1510 "we previously converted all other cases to >= or ==");
1514 if(expr.
op0() == expr.
op1())
1519 if(expr.
id()==ID_equal)
1555 if(expr.
id()==ID_notequal)
1557 auto new_rel_expr = expr;
1558 new_rel_expr.
id(ID_equal);
1564 if(expr.
id()==ID_equal &&
1566 expr.
op1().
get(ID_value)==ID_NULL)
1570 if(expr.
op0().
id() == ID_address_of)
1575 object.
id() == ID_symbol ||
object.
id() == ID_dynamic_object ||
1576 object.
id() == ID_member ||
object.
id() == ID_index ||
1577 object.
id() == ID_string_constant)
1583 expr.
op0().
id() == ID_typecast &&
1587 const auto &
object =
1591 object.
id() == ID_symbol ||
object.
id() == ID_dynamic_object ||
1592 object.
id() == ID_member ||
object.
id() == ID_index ||
1593 object.
id() == ID_string_constant)
1599 expr.
op0().
id() == ID_typecast && expr.
op0().
type().
id() == ID_pointer)
1603 op.
type().
id() != ID_pointer &&
1605 op.
type().
id() == ID_complex))
1612 auto new_expr = expr;
1614 if(new_expr.op0().type().id() != ID_pointer)
1615 new_expr.op1() =
from_integer(0, new_expr.op0().type());
1617 new_expr.op1().type() = new_expr.op0().type();
1628 if(expr.
op0().
id()==ID_plus)
1632 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1635 bool op_changed =
false;
1636 auto new_expr = expr;
1640 if(it->is_constant())
1658 new_expr.op1() =
from_integer(i, new_expr.op1().type());
1671 expr.
op0().
id() == ID_typecast && expr.
op0().
type().
id() == ID_floatbv &&
1678 ieee_floatt const_val_converted_back=const_val_converted;
1681 if(const_val_converted_back==const_val)
1686 return std::move(result);
1695 if(expr.
id()==ID_ge &&
1702 auto new_expr = expr;
1705 if(expr.
id()==ID_equal)
1708 if(operand.
id()==ID_unary_minus)
1711 return std::move(new_expr);
1713 else if(operand.
id()==ID_plus)
1718 if(operand_plus_expr.operands().size() == 2)
1721 if(operand_plus_expr.op0().id() == ID_unary_minus)
1722 operand_plus_expr.op0().swap(operand_plus_expr.op1());
1724 if(operand_plus_expr.op1().id() == ID_unary_minus)
1727 operand_plus_expr.op0(),
1739 expr.
op0().
id() == ID_typecast &&
1753 return lhs_typecast_op;
1757 #define NORMALISE_CONSTANT_TESTS
1758 #ifdef NORMALISE_CONSTANT_TESTS
1760 if(expr.
op0().
type().
id()==ID_unsignedbv ||
1765 if(expr.
id()==ID_notequal)
1767 auto new_rel_expr = expr;
1768 new_rel_expr.
id(ID_equal);
1772 else if(expr.
id()==ID_gt)
1781 auto new_expr = expr;
1784 new_expr.op1() =
from_integer(i, new_expr.op1().type());
1787 else if(expr.
id()==ID_lt)
1789 auto new_rel_expr = expr;
1790 new_rel_expr.
id(ID_ge);
1794 else if(expr.
id()==ID_le)
1803 auto new_rel_expr = expr;
1804 new_rel_expr.
id(ID_ge);
1806 new_rel_expr.op1() =
from_integer(i, new_rel_expr.op1().type());