44struct simplify_expr_cachet
48 typedef std::unordered_map<
51 typedef std::unordered_map<exprt, exprt, irep_hash> containert;
54 containert container_normal;
56 containert &container()
58 return container_normal;
62simplify_expr_cachet simplify_expr_cache;
71 if(type.
id()==ID_floatbv)
77 else if(type.
id()==ID_signedbv ||
78 type.
id()==ID_unsignedbv)
80 auto value = numeric_cast<mp_integer>(
to_unary_expr(expr).op());
105 if(type.
id()==ID_floatbv)
110 else if(type.
id()==ID_signedbv ||
111 type.
id()==ID_unsignedbv)
113 const auto value = numeric_cast<mp_integer>(expr.
op());
114 if(value.has_value())
133 if(op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv)
137 std::size_t result = 0;
139 for(std::size_t i = 0; i < width; i++)
158 if(!const_bits_opt.has_value())
162 std::size_t n_leading_zeros = const_bits_opt->rfind(
'1');
163 if(n_leading_zeros == std::string::npos)
168 n_leading_zeros = const_bits_opt->size();
171 n_leading_zeros = const_bits_opt->size() - n_leading_zeros - 1;
184 if(!const_bits_opt.has_value())
188 std::size_t n_trailing_zeros = const_bits_opt->find(
'1');
189 if(n_trailing_zeros == std::string::npos)
194 n_trailing_zeros = const_bits_opt->size();
242 const auto first_value_opt =
252 const auto second_value_opt =
255 if(!second_value_opt)
263 const bool includes =
289 const auto numeric_length =
326 const bool first_shorter = s1_size < s2_size;
331 auto it_pair = std::mismatch(ops1.begin(), ops1.end(), ops2.begin());
333 if(it_pair.first == ops1.end())
342 first_shorter ? char1 - char2 : char2 - char1, expr.
type());
354 const bool search_from_end)
356 std::size_t starting_index = 0;
361 auto &starting_index_expr = expr.
arguments().at(2);
363 if(starting_index_expr.id() != ID_constant)
374 starting_index = numeric_cast_v<std::size_t>(idx);
389 const auto search_string_size = s1_data.
operands().size();
390 if(starting_index >= search_string_size)
395 unsigned long starting_offset =
396 starting_index > 0 ? (search_string_size - 1) - starting_index : 0;
419 ? starting_index > 0 ? starting_index : search_string_size
425 auto end = std::prev(s1_data.
operands().end(), starting_offset);
426 auto it = std::find_end(
433 std::distance(s1_data.
operands().begin(), it), expr.
type());
437 auto it = std::search(
438 std::next(s1_data.
operands().begin(), starting_index),
445 std::distance(s1_data.
operands().begin(), it), expr.
type());
448 else if(expr.
arguments().at(1).id() == ID_constant)
453 const auto c1_val = numeric_cast_v<mp_integer>(c1);
455 auto pred = [&](
const exprt &c2) {
458 return c1_val == c2_val;
463 auto it = std::find_if(
464 std::next(s1_data.
operands().rbegin(), starting_offset),
469 std::distance(s1_data.
operands().begin(), it.base() - 1),
474 auto it = std::find_if(
475 std::next(s1_data.
operands().begin(), starting_index),
480 std::distance(s1_data.
operands().begin(), it), expr.
type());
500 if(expr.
arguments().at(1).id() != ID_constant)
518 const auto i_opt = numeric_cast<std::size_t>(index);
520 if(!i_opt || *i_opt >= char_seq.
operands().size())
527 if(c.type() != expr.
type())
538 auto &operands = string_data.
operands();
539 for(
auto &operand : operands)
542 auto character = numeric_cast_v<unsigned int>(constant_value);
548 if(isalpha(character))
550 if(isupper(character))
552 from_integer(tolower(character), constant_value.type());
574 const auto first_value_opt =
584 const auto second_value_opt =
587 if(!second_value_opt)
600 bool is_equal = first_value == second_value;
619 const auto first_value_opt =
629 const auto second_value_opt =
632 if(!second_value_opt)
643 if(offset.id() != ID_constant)
651 offset_int + second_value.
operands().size();
654 exprt::operandst::const_iterator second_it =
656 for(
const auto &first_op : first_value.
operands())
660 else if(second_it == second_value.
operands().end())
662 else if(first_op != *second_it)
691 if(func_id == ID_cprover_string_startswith_func)
695 else if(func_id == ID_cprover_string_endswith_func)
699 else if(func_id == ID_cprover_string_is_empty_func)
703 else if(func_id == ID_cprover_string_compare_to_func)
707 else if(func_id == ID_cprover_string_index_of_func)
711 else if(func_id == ID_cprover_string_char_at_func)
715 else if(func_id == ID_cprover_string_contains_func)
719 else if(func_id == ID_cprover_string_last_index_of_func)
723 else if(func_id == ID_cprover_string_equals_ignore_case_func)
738 if(expr.
op().
id() == ID_infinity)
743 return std::move(tmp);
750 (expr_type.
id() == ID_unsignedbv || expr_type.
id() == ID_signedbv) &&
760 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
761 (op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv) &&
765 auto new_expr = expr;
777 if(expr_type.
id()==ID_bool)
782 op_type.
id() == ID_floatbv ? ID_ieee_float_notequal : ID_notequal,
790 op_type.
id() == ID_bool &&
791 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv ||
792 expr_type.
id() == ID_c_bool || expr_type.
id() == ID_c_bit_field))
811 const auto &typecast = expr_checked_cast<typecast_exprt>(expr.
op());
812 if(typecast.op().type()==expr_type)
814 return typecast.op();
820 if(expr_type.
id()==ID_c_bool &&
821 op_type.
id()!=ID_bool)
825 auto new_expr = expr;
839 return std::move(tmp);
845 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
846 op_type.
id() == ID_pointer)
848 auto new_expr = expr;
856 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
857 expr.
op().
id() == ID_typecast && expr.
op().
operands().size() == 1 &&
858 op_type.
id() == ID_pointer)
863 auto outer_cast = expr;
872 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
873 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus &&
878 if(((op_plus_expr.op0().id() == ID_typecast &&
880 (op_plus_expr.op0().is_constant() &&
885 if(sub_size.has_value())
887 auto new_expr = expr;
892 if(*sub_size == 0 || *sub_size == 1)
893 new_expr.op() = offset_expr;
914 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
915 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv))
925 if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
926 op_id==ID_unary_minus ||
927 op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
946 else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
956 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
957 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus)
962 if(step.has_value() && *step != 0)
965 auto new_expr = expr;
967 new_expr.
op().
type() = size_t_type;
969 for(
auto &op : new_expr.op().operands())
972 if(op.type().id() != ID_pointer && *step > 1)
977 op = std::move(new_op);
988 if(expr.
op().
id()==ID_if &&
995 auto new_expr=
if_exprt(expr.
op().
op0(), tmp_op1, tmp_op2, expr_type);
997 return std::move(new_expr);
1002 const exprt &operand = expr.
op();
1010 typet c_sizeof_type=
1011 static_cast<const typet &
>(operand.
find(ID_C_c_sizeof_type));
1013 if(op_type_id==ID_integer ||
1014 op_type_id==ID_natural)
1020 if(expr_type_id==ID_bool)
1025 if(expr_type_id==ID_unsignedbv ||
1026 expr_type_id==ID_signedbv ||
1027 expr_type_id==ID_c_enum ||
1028 expr_type_id==ID_c_bit_field ||
1029 expr_type_id==ID_integer)
1033 else if(expr_type_id == ID_c_enum_tag)
1036 if(!c_enum_type.is_incomplete())
1039 tmp.
type() = expr_type;
1040 return std::move(tmp);
1044 else if(op_type_id==ID_rational)
1047 else if(op_type_id==ID_real)
1050 else if(op_type_id==ID_bool)
1052 if(expr_type_id==ID_unsignedbv ||
1053 expr_type_id==ID_signedbv ||
1054 expr_type_id==ID_integer ||
1055 expr_type_id==ID_natural ||
1056 expr_type_id==ID_rational ||
1057 expr_type_id==ID_c_bool ||
1058 expr_type_id==ID_c_enum ||
1059 expr_type_id==ID_c_bit_field)
1070 else if(expr_type_id==ID_c_enum_tag)
1073 if(!c_enum_type.is_incomplete())
1075 unsigned int_value = operand.
is_true() ? 1u : 0u;
1077 tmp.
type()=expr_type;
1078 return std::move(tmp);
1081 else if(expr_type_id==ID_pointer &&
1088 else if(op_type_id==ID_unsignedbv ||
1089 op_type_id==ID_signedbv ||
1090 op_type_id==ID_c_bit_field ||
1091 op_type_id==ID_c_bool)
1098 if(expr_type_id==ID_bool)
1103 if(expr_type_id==ID_c_bool)
1108 if(expr_type_id==ID_integer)
1113 if(expr_type_id==ID_natural)
1121 if(expr_type_id==ID_unsignedbv ||
1122 expr_type_id==ID_signedbv ||
1123 expr_type_id==ID_bv ||
1124 expr_type_id==ID_c_bit_field)
1129 result.set(ID_C_c_sizeof_type, c_sizeof_type);
1131 return std::move(result);
1134 if(expr_type_id==ID_c_enum_tag)
1137 if(!c_enum_type.is_incomplete())
1140 tmp.
type()=expr_type;
1141 return std::move(tmp);
1145 if(expr_type_id==ID_c_enum)
1150 if(expr_type_id==ID_fixedbv)
1162 if(expr_type_id==ID_floatbv)
1174 if(expr_type_id==ID_rational)
1180 else if(op_type_id==ID_fixedbv)
1182 if(expr_type_id==ID_unsignedbv ||
1183 expr_type_id==ID_signedbv)
1189 else if(expr_type_id==ID_fixedbv)
1196 else if(expr_type_id == ID_bv)
1202 else if(op_type_id==ID_floatbv)
1206 if(expr_type_id==ID_unsignedbv ||
1207 expr_type_id==ID_signedbv)
1212 else if(expr_type_id==ID_floatbv)
1218 else if(expr_type_id==ID_fixedbv)
1228 else if(expr_type_id == ID_bv)
1233 else if(op_type_id==ID_bv)
1236 expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1237 expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1238 expr_type_id == ID_c_bit_field)
1242 if(expr_type_id != ID_c_enum_tag)
1248 result.type() = tag_type;
1249 return std::move(result);
1252 else if(expr_type_id == ID_floatbv)
1257 ieee_float.unpack(int_value);
1258 return ieee_float.to_expr();
1260 else if(expr_type_id == ID_fixedbv)
1265 fixedbv.set_value(int_value);
1266 return fixedbv.to_expr();
1269 else if(op_type_id==ID_c_enum_tag)
1276 auto new_expr = expr;
1281 else if(op_type_id==ID_c_enum)
1287 auto new_expr = expr;
1293 else if(operand.
id()==ID_typecast)
1298 op_type_id == expr_type_id &&
1299 (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv) &&
1303 auto new_expr = expr;
1309 else if(operand.
id()==ID_address_of)
1315 o.
type().
id() == ID_array &&
1333 if(pointer.
type().
id()!=ID_pointer)
1336 if(pointer.
id()==ID_if && pointer.
operands().size()==3)
1340 auto tmp_op1 = expr;
1344 auto tmp_op2 = expr;
1348 if_exprt tmp{if_expr.
cond(), tmp_op1_result, tmp_op2_result};
1353 if(pointer.
id()==ID_address_of)
1361 pointer.
id() == ID_plus && pointer.
operands().size() == 2 &&
1369 if(address_of.
object().
id()==ID_index)
1394 bool no_change =
true;
1400 auto with_expr = expr;
1402 const typet old_type_followed =
ns.
follow(with_expr.old().type());
1406 if(old_type_followed.
id() == ID_struct)
1408 if(with_expr.old().id() == ID_struct || with_expr.old().id() == ID_constant)
1410 while(with_expr.operands().size() > 1)
1413 with_expr.where().get(ID_component_name);
1415 if(!
to_struct_type(old_type_followed).has_component(component_name))
1418 std::size_t number =
1421 if(number >= with_expr.old().operands().size())
1424 with_expr.old().operands()[number].swap(with_expr.new_value());
1426 with_expr.operands().erase(++with_expr.operands().begin());
1427 with_expr.operands().erase(++with_expr.operands().begin());
1434 with_expr.old().type().id() == ID_array ||
1435 with_expr.old().type().id() == ID_vector)
1438 with_expr.old().id() == ID_array || with_expr.old().id() == ID_constant ||
1439 with_expr.old().id() == ID_vector)
1441 while(with_expr.operands().size() > 1)
1443 const auto i = numeric_cast<mp_integer>(with_expr.where());
1448 if(*i < 0 || *i >= with_expr.old().operands().size())
1451 with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
1452 with_expr.new_value());
1454 with_expr.operands().erase(++with_expr.operands().begin());
1455 with_expr.operands().erase(++with_expr.operands().begin());
1462 if(with_expr.operands().size() == 1)
1463 return with_expr.old();
1468 return std::move(with_expr);
1479 exprt *value_ptr=&updated_value;
1481 for(
const auto &e : designator)
1485 if(e.id()==ID_index_designator &&
1486 value_ptr->
id()==ID_array)
1493 if(*i < 0 || *i >= value_ptr->
operands().size())
1496 value_ptr = &value_ptr->
operands()[numeric_cast_v<std::size_t>(*i)];
1498 else if(e.id()==ID_member_designator &&
1499 value_ptr->
id()==ID_struct)
1502 e.get(ID_component_name);
1508 value_ptr = &designator_as_struct_expr.component(component_name,
ns);
1517 return updated_value;
1522 if(expr.
id()==ID_plus)
1524 if(expr.
type().
id()==ID_pointer)
1528 if(op.type().id() == ID_pointer)
1532 else if(expr.
id()==ID_typecast)
1535 const typet &op_type = typecast_expr.op().type();
1537 if(op_type.
id()==ID_pointer)
1542 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1549 const exprt &casted_expr = typecast_expr.op();
1550 if(casted_expr.
id() == ID_plus && casted_expr.
operands().size() == 2)
1554 const exprt &cand = plus_expr.
op0().
id() == ID_typecast
1558 if(cand.
id() == ID_typecast)
1562 if(typecast_op.id() == ID_address_of)
1567 typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1578 else if(expr.
id()==ID_address_of)
1582 if(
object.
id() == ID_index)
1588 else if(
object.
id() == ID_member)
1603 if(expr.
op().
id()==ID_if)
1614 if(el_size.has_value() && *el_size < 0)
1619 if(expr.
op().
id()==expr.
id())
1633 ((expr.
id() == ID_byte_extract_big_endian &&
1634 expr.
op().
id() == ID_byte_update_big_endian) ||
1635 (expr.
id() == ID_byte_extract_little_endian &&
1636 expr.
op().
id() == ID_byte_update_little_endian)) &&
1641 if(expr.
type() == op_byte_update.value().type())
1643 return op_byte_update.value();
1646 el_size.has_value() &&
1650 tmp.
op() = op_byte_update.value();
1658 auto offset = numeric_cast<mp_integer>(expr.
offset());
1659 if(!offset.has_value() || *offset < 0)
1665 *offset == 0 && ((expr.
id() == ID_byte_extract_little_endian &&
1668 (expr.
id() == ID_byte_extract_big_endian &&
1678 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1686 if(!el_size.has_value() || *el_size == 0)
1689 if(expr.
op().
id()==ID_array_of &&
1698 if(!const_bits_opt.has_value())
1701 std::string const_bits=const_bits_opt.value();
1703 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1706 while(
mp_integer(const_bits.size()) < *offset * 8 + *el_size)
1707 const_bits+=const_bits;
1709 std::string el_bits = std::string(
1711 numeric_cast_v<std::size_t>(*offset * 8),
1712 numeric_cast_v<std::size_t>(*el_size));
1715 el_bits, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1718 return std::move(*tmp);
1723 expr.
op().
id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
1738 const bool struct_has_flexible_array_member =
has_subtype(
1740 [&](
const typet &type) {
1741 if(type.id() != ID_struct && type.id() != ID_struct_tag)
1744 const struct_typet &st = to_struct_type(ns.follow(type));
1745 const auto &comps = st.components();
1746 if(comps.empty() || comps.back().type().id() != ID_array)
1750 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1751 return !size.has_value() || *size <= 1;
1755 bits.has_value() &&
mp_integer(bits->size()) >= *el_size + *offset * 8 &&
1756 !struct_has_flexible_array_member)
1758 std::string bits_cut = std::string(
1760 numeric_cast_v<std::size_t>(*offset * 8),
1761 numeric_cast_v<std::size_t>(*el_size));
1764 bits_cut, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1767 return std::move(*tmp);
1773 if(expr.
op().
id() == ID_struct || expr.
op().
id() == ID_union)
1775 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
1783 for(
const auto &comp : components)
1789 !component_bits.has_value() || *component_bits == 0 ||
1790 *component_bits % 8 != 0)
1796 auto member_offset_opt =
1799 if(!member_offset_opt.has_value())
1808 member_offset_opt.value(), expr.
offset().
type())});
1811 tmp.
type() = comp.type();
1812 tmp.offset() = new_offset;
1820 else if(expr.
type().
id() == ID_union || expr.
type().
id() == ID_union_tag)
1824 if(widest_member_opt.has_value())
1827 be.
type() = widest_member_opt->first.type();
1828 return union_exprt{widest_member_opt->first.get_name(),
1838 if(!subexpr.has_value() || subexpr.value() == expr)
1850 expr.
id() == expr.
op().
id() &&
1856 return std::move(tmp);
1859 const exprt &root = expr.
op();
1867 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
1868 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
1871 expr.
id()==ID_byte_update_little_endian ?
1872 ID_byte_extract_little_endian :
1873 ID_byte_extract_big_endian,
1874 value, offset, expr.
type());
1880 const auto offset_int = numeric_cast<mp_integer>(offset);
1882 root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
1883 *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
1884 *offset_int * 8 + *val_size <= *root_size)
1887 expr2bits(root, expr.
id() == ID_byte_update_little_endian,
ns);
1889 if(root_bits.has_value())
1891 const auto val_bits =
1892 expr2bits(value, expr.
id() == ID_byte_update_little_endian,
ns);
1894 if(val_bits.has_value())
1897 numeric_cast_v<std::size_t>(*offset_int * 8),
1898 numeric_cast_v<std::size_t>(*val_size),
1904 expr.
id() == ID_byte_update_little_endian,
1908 return std::move(*tmp);
1921 if(expr.
id()!=ID_byte_update_little_endian)
1924 if(value.
id()==ID_with)
1928 if(with.
old().
id()==ID_byte_extract_little_endian)
1935 if(!(root==extract.
op()))
1937 if(!(offset==extract.
offset()))
1941 if(tp.
id()==ID_struct)
1948 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
1963 tmp.set_value(std::move(new_value));
1968 else if(tp.
id()==ID_array)
1974 exprt index_offset =
1988 tmp.set_value(std::move(new_value));
1996 if(!offset_int.has_value() || *offset_int < 0)
2002 if(!val_size.has_value() || *val_size == 0)
2007 if(op_type.
id()==ID_struct)
2026 if(!m_offset.has_value())
2033 if(!m_size_bits.has_value() || *m_size_bits == 0 || (*m_size_bits) % 8 != 0)
2039 mp_integer m_size_bytes = (*m_size_bits) / 8;
2042 if(*m_offset + m_size_bytes <= *offset_int)
2046 update_size.has_value() && *update_size > 0 &&
2047 *m_offset >= *offset_int + *update_size)
2055 exprt member_name(ID_member_name);
2056 member_name.
set(ID_component_name,
component.get_name());
2061 *m_offset < *offset_int ||
2062 (*m_offset == *offset_int && update_size.has_value() &&
2063 *update_size > 0 && m_size_bytes > *update_size))
2066 ID_byte_update_little_endian,
2074 update_size.has_value() && *update_size > 0 &&
2075 *m_offset + m_size_bytes > *offset_int + *update_size)
2084 ID_byte_extract_little_endian,
2099 if(root.
id()==ID_array)
2104 if(!el_size.has_value() || *el_size == 0 ||
2105 (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
2115 if(*offset_int * 8 + (*val_size) <= m_offset_bits)
2118 if(*offset_int * 8 < m_offset_bits + *el_size)
2120 mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
2121 bytes_req-=val_offset;
2122 if(val_offset + bytes_req > (*val_size) / 8)
2123 bytes_req = (*val_size) / 8 - val_offset;
2126 ID_byte_extract_little_endian,
2136 *offset_int + val_offset - m_offset_bits / 8, offset.
type()),
2141 val_offset+=bytes_req;
2144 m_offset_bits += *el_size;
2147 return std::move(result);
2156 if(expr.
id() == ID_complex_real)
2160 if(complex_real_expr.op().id() == ID_complex)
2163 else if(expr.
id() == ID_complex_imag)
2167 if(complex_imag_expr.op().id() == ID_complex)
2181 (expr.
op0().
is_zero() && expr.
id() != ID_overflow_minus))
2188 expr.
id() == ID_overflow_mult &&
2201 op_type_id == ID_integer || op_type_id == ID_rational ||
2202 op_type_id == ID_real)
2207 if(op_type_id == ID_natural && expr.
id() != ID_overflow_minus)
2211 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2217 const auto op0_value = numeric_cast<mp_integer>(expr.
op0());
2218 const auto op1_value = numeric_cast<mp_integer>(expr.
op1());
2219 if(!op0_value.has_value() || !op1_value.has_value())
2223 if(expr.
id() == ID_overflow_plus)
2224 no_overflow_result = *op0_value + *op1_value;
2225 else if(expr.
id() == ID_overflow_minus)
2226 no_overflow_result = *op0_value - *op1_value;
2227 else if(expr.
id() == ID_overflow_mult)
2228 no_overflow_result = *op0_value * *op1_value;
2229 else if(expr.
id() == ID_overflow_shl)
2230 no_overflow_result = *op0_value << *op1_value;
2237 no_overflow_result < bv_type.smallest() ||
2238 no_overflow_result > bv_type.largest())
2256 op_type_id == ID_integer || op_type_id == ID_rational ||
2257 op_type_id == ID_real)
2262 if(op_type_id == ID_natural)
2266 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2272 const auto op_value = numeric_cast<mp_integer>(expr.
op());
2273 if(!op_value.has_value())
2277 if(expr.
id() == ID_overflow_unary_minus)
2278 no_overflow_result = -*op_value;
2285 no_overflow_result < bv_type.smallest() ||
2286 no_overflow_result > bv_type.largest())
2300 if(expr.
id()==ID_address_of)
2304 else if(expr.
id()==ID_if)
2313 if(r_it.has_changed())
2341 if(expr.
id()==ID_typecast)
2345 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2346 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2347 expr.
id()==ID_ge || expr.
id()==ID_le)
2351 else if(expr.
id()==ID_if)
2355 else if(expr.
id()==ID_lambda)
2359 else if(expr.
id()==ID_with)
2363 else if(expr.
id()==ID_update)
2367 else if(expr.
id()==ID_index)
2371 else if(expr.
id()==ID_member)
2375 else if(expr.
id()==ID_byte_update_little_endian ||
2376 expr.
id()==ID_byte_update_big_endian)
2380 else if(expr.
id()==ID_byte_extract_little_endian ||
2381 expr.
id()==ID_byte_extract_big_endian)
2385 else if(expr.
id()==ID_pointer_object)
2389 else if(expr.
id() == ID_is_dynamic_object)
2393 else if(expr.
id() == ID_is_invalid_pointer)
2397 else if(expr.
id()==ID_object_size)
2401 else if(expr.
id()==ID_good_pointer)
2405 else if(expr.
id()==ID_div)
2409 else if(expr.
id()==ID_mod)
2413 else if(expr.
id()==ID_bitnot)
2417 else if(expr.
id()==ID_bitand ||
2418 expr.
id()==ID_bitor ||
2419 expr.
id()==ID_bitxor)
2423 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2427 else if(expr.
id()==ID_power)
2431 else if(expr.
id()==ID_plus)
2435 else if(expr.
id()==ID_minus)
2439 else if(expr.
id()==ID_mult)
2443 else if(expr.
id()==ID_floatbv_plus ||
2444 expr.
id()==ID_floatbv_minus ||
2445 expr.
id()==ID_floatbv_mult ||
2446 expr.
id()==ID_floatbv_div)
2450 else if(expr.
id()==ID_floatbv_typecast)
2454 else if(expr.
id()==ID_unary_minus)
2458 else if(expr.
id()==ID_unary_plus)
2462 else if(expr.
id()==ID_not)
2466 else if(expr.
id()==ID_implies ||
2467 expr.
id()==ID_or || expr.
id()==ID_xor ||
2472 else if(expr.
id()==ID_dereference)
2476 else if(expr.
id()==ID_address_of)
2480 else if(expr.
id()==ID_pointer_offset)
2484 else if(expr.
id()==ID_extractbit)
2488 else if(expr.
id()==ID_concatenation)
2492 else if(expr.
id()==ID_extractbits)
2496 else if(expr.
id()==ID_ieee_float_equal ||
2497 expr.
id()==ID_ieee_float_notequal)
2501 else if(expr.
id() == ID_bswap)
2505 else if(expr.
id()==ID_isinf)
2509 else if(expr.
id()==ID_isnan)
2513 else if(expr.
id()==ID_isnormal)
2517 else if(expr.
id()==ID_abs)
2521 else if(expr.
id()==ID_sign)
2525 else if(expr.
id() == ID_popcount)
2529 else if(expr.
id() == ID_count_leading_zeros)
2533 else if(expr.
id() == ID_count_trailing_zeros)
2537 else if(expr.
id() == ID_function_application)
2541 else if(expr.
id() == ID_complex_real || expr.
id() == ID_complex_imag)
2546 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_minus ||
2547 expr.
id() == ID_overflow_mult || expr.
id() == ID_overflow_shl)
2551 else if(expr.
id() == ID_overflow_unary_minus)
2555 else if(expr.
id() == ID_bitreverse)
2560 if(!no_change_join_operands)
2566# ifdef DEBUG_ON_DEMAND
2571 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
2572 <<
" ---> " <<
format(
r.expr) <<
'\n';
2584 std::pair<simplify_expr_cachet::containert::iterator, bool>
2585 cache_result=simplify_expr_cache.container().
2586 insert(std::pair<exprt, exprt>(expr,
exprt()));
2588 if(!cache_result.second)
2590 const exprt &new_expr=cache_result.first->second;
2606 if(simplify_node_result.has_changed())
2609 tmp = simplify_node_result.expr;
2612#ifdef USE_LOCAL_REPLACE_MAP
2614 replace_mapt::const_iterator it=local_replace_map.
find(tmp);
2615 if(it!=local_replace_map.end())
2621 if(!local_replace_map.empty() &&
2640 cache_result.first->second = tmp;
2643 return std::move(tmp);
2650#ifdef DEBUG_ON_DEMAND
2652 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
2655#ifdef DEBUG_ON_DEMAND
2657 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
2659 if(result.has_changed())
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
void base_type(typet &type, const namespacet &ns)
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const binary_overflow_exprt & to_binary_overflow_expr(const exprt &expr)
Cast an exprt to a binary_overflow_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const unary_overflow_exprt & to_unary_overflow_expr(const exprt &expr)
Cast an exprt to a unary_overflow_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Operator to return the address of an object.
Array constructor from list of elements.
const typet & element_type() const
The type of the elements of the array.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for relations, i.e., binary predicates whose two operands have the same type.
std::size_t get_width() const
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & offset() const
const exprt & value() const
C enum tag type, i.e., c_enum_typet with an identifier.
const typet & underlying_type() const
struct configt::ansi_ct ansi_c
A constant literal expression.
const irep_idt & get_value() const
void set_value(const irep_idt &value)
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
bool zero_permitted() const
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
bool zero_permitted() const
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool is_one() const
Return whether the expression is a constant representing 1.
bool has_operands() const
Return true if there is at least one operand.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The Boolean constant false.
std::size_t get_fraction_bits() const
Fixed-width bit-vector with signed fixed-point interpretation.
void from_integer(const mp_integer &i)
mp_integer to_integer() const
void set_value(const mp_integer &_v)
void round(const fixedbv_spect &dest_spec)
constant_exprt to_expr() const
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
mp_integer to_integer() const
constant_exprt to_expr() const
void set_sign(bool _sign)
void from_integer(const mp_integer &i)
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
Fixed-width bit-vector representing a signed or unsigned integer.
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
A (mathematical) lambda expression.
exprt application(const operandst &arguments) const
Extract member of struct or union.
Binary multiplication Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
The plus expression Associativity is not specified.
The popcount (counting the number of bits set to 1) expression.
const exprt & length() const
const exprt & content() const
Sign of an expression Predicate is true if _op is negative, false otherwise.
Fixed-width bit-vector with two's complement interpretation.
resultt simplify_isnan(const unary_exprt &)
resultt simplify_bitwise(const multi_ary_exprt &)
resultt simplify_power(const binary_exprt &)
resultt simplify_div(const div_exprt &)
resultt simplify_byte_extract(const byte_extract_exprt &)
resultt simplify_bitreverse(const bitreverse_exprt &)
Try to simplify bit-reversing to a constant expression.
resultt simplify_abs(const abs_exprt &)
resultt simplify_isnormal(const unary_exprt &)
resultt simplify_dereference(const dereference_exprt &)
resultt simplify_bitnot(const bitnot_exprt &)
resultt simplify_good_pointer(const unary_exprt &)
resultt simplify_popcount(const popcount_exprt &)
static resultt changed(resultt<> result)
bool simplify_if_preorder(if_exprt &expr)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_if(const if_exprt &)
resultt simplify_overflow_unary(const unary_overflow_exprt &)
Try to simplify overflow-unary-.
resultt simplify_pointer_offset(const unary_exprt &)
resultt simplify_minus(const minus_exprt &)
resultt simplify_extractbit(const extractbit_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_shifts(const shift_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_boolean(const exprt &)
resultt simplify_object(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
resultt simplify_with(const with_exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_not(const not_exprt &)
resultt simplify_isinf(const unary_exprt &)
resultt simplify_overflow_binary(const binary_overflow_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
resultt simplify_function_application(const function_application_exprt &)
Attempt to simplify mathematical function applications if we have enough information to do so.
resultt simplify_index(const index_exprt &)
resultt simplify_bswap(const bswap_exprt &)
resultt simplify_object_size(const unary_exprt &)
resultt simplify_member(const member_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_byte_update(const byte_update_exprt &)
bool simplify_node_preorder(exprt &expr)
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
resultt simplify_update(const update_exprt &)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_mod(const mod_exprt &)
resultt simplify_complex(const unary_exprt &)
resultt simplify_plus(const plus_exprt &)
virtual bool simplify(exprt &expr)
resultt simplify_unary_plus(const unary_plus_exprt &)
resultt simplify_is_dynamic_object(const unary_exprt &)
resultt simplify_node(exprt)
resultt simplify_lambda(const lambda_exprt &)
resultt simplify_concatenation(const concatenation_exprt &)
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
resultt simplify_ctz(const count_trailing_zeros_exprt &)
Try to simplify count-trailing-zeros to a constant expression.
resultt simplify_clz(const count_leading_zeros_exprt &)
Try to simplify count-leading-zeros to a constant expression.
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
resultt simplify_pointer_object(const unary_exprt &)
resultt simplify_sign(const sign_exprt &)
resultt simplify_unary_minus(const unary_minus_exprt &)
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
const componentst & components() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool has_component(const irep_idt &component_name) const
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
std::vector< componentt > componentst
const irep_idt & get_identifier() const
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Generic base class for unary expressions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
optionalt< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
Fixed-width bit-vector with unsigned binary interpretation.
Operator to update elements in structs and arrays.
exprt::operandst & designator()
Operator to update elements in structs and arrays.
#define Forall_operands(it, expr)
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
exprt pointer_offset_sum(const exprt &a, const exprt &b)
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify(exprt &expr, const namespacet &ns)
static simplify_exprt::resultt simplify_string_compare_to(const function_application_exprt &expr, const namespacet &ns)
Simplify String.compareTo function when arguments are constant.
static simplify_exprt::resultt simplify_string_contains(const function_application_exprt &expr, const namespacet &ns)
Simplify String.contains function when arguments are constant.
static simplify_exprt::resultt simplify_string_endswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.endsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_char_at(const function_application_exprt &expr, const namespacet &ns)
Simplify String.charAt function when arguments are constant.
static simplify_exprt::resultt simplify_string_startswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.startsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_is_empty(const function_application_exprt &expr, const namespacet &ns)
Simplify String.isEmpty function when arguments are constant.
static bool lower_case_string_expression(array_exprt &string_data)
Take the passed-in constant string array and lower-case every character.
static simplify_exprt::resultt simplify_string_index_of(const function_application_exprt &expr, const namespacet &ns, const bool search_from_end)
Simplify String.indexOf function when arguments are constant.
static simplify_exprt::resultt simplify_string_equals_ignore_case(const function_application_exprt &expr, const namespacet &ns)
Simplify String.equalsIgnorecase function when arguments are constant.
exprt simplify_expr(exprt src, const namespacet &ns)
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
bool join_operands(exprt &expr)
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)
Get char sequence from content field of a refined string expression.
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define POSTCONDITION(CONDITION)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
String expressions for the string solver.
refined_string_exprt & to_string_expr(exprt &expr)
bool can_cast_expr< refined_string_exprt >(const exprt &base)
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)