44 struct 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;
62 simplify_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)
961 if(step.has_value() && *step != 0)
964 auto new_expr = expr;
966 new_expr.
op().
type() = size_t_type;
968 for(
auto &op : new_expr.op().operands())
971 if(op.type().id() != ID_pointer && *step > 1)
976 op = std::move(new_op);
987 if(expr.
op().
id()==ID_if &&
994 auto new_expr=
if_exprt(expr.
op().
op0(), tmp_op1, tmp_op2, expr_type);
996 return std::move(new_expr);
1001 const exprt &operand = expr.
op();
1009 typet c_sizeof_type=
1010 static_cast<const typet &
>(operand.
find(ID_C_c_sizeof_type));
1012 if(op_type_id==ID_integer ||
1013 op_type_id==ID_natural)
1019 if(expr_type_id==ID_bool)
1024 if(expr_type_id==ID_unsignedbv ||
1025 expr_type_id==ID_signedbv ||
1026 expr_type_id==ID_c_enum ||
1027 expr_type_id==ID_c_bit_field ||
1028 expr_type_id==ID_integer)
1032 else if(expr_type_id == ID_c_enum_tag)
1035 if(!c_enum_type.is_incomplete())
1038 tmp.
type() = expr_type;
1039 return std::move(tmp);
1043 else if(op_type_id==ID_rational)
1046 else if(op_type_id==ID_real)
1049 else if(op_type_id==ID_bool)
1051 if(expr_type_id==ID_unsignedbv ||
1052 expr_type_id==ID_signedbv ||
1053 expr_type_id==ID_integer ||
1054 expr_type_id==ID_natural ||
1055 expr_type_id==ID_rational ||
1056 expr_type_id==ID_c_bool ||
1057 expr_type_id==ID_c_enum ||
1058 expr_type_id==ID_c_bit_field)
1069 else if(expr_type_id==ID_c_enum_tag)
1072 if(!c_enum_type.is_incomplete())
1074 unsigned int_value = operand.
is_true() ? 1u : 0u;
1076 tmp.
type()=expr_type;
1077 return std::move(tmp);
1080 else if(expr_type_id==ID_pointer &&
1087 else if(op_type_id==ID_unsignedbv ||
1088 op_type_id==ID_signedbv ||
1089 op_type_id==ID_c_bit_field ||
1090 op_type_id==ID_c_bool)
1097 if(expr_type_id==ID_bool)
1102 if(expr_type_id==ID_c_bool)
1107 if(expr_type_id==ID_integer)
1112 if(expr_type_id==ID_natural)
1120 if(expr_type_id==ID_unsignedbv ||
1121 expr_type_id==ID_signedbv ||
1122 expr_type_id==ID_bv ||
1123 expr_type_id==ID_c_bit_field)
1128 result.set(ID_C_c_sizeof_type, c_sizeof_type);
1130 return std::move(result);
1133 if(expr_type_id==ID_c_enum_tag)
1136 if(!c_enum_type.is_incomplete())
1139 tmp.
type()=expr_type;
1140 return std::move(tmp);
1144 if(expr_type_id==ID_c_enum)
1149 if(expr_type_id==ID_fixedbv)
1161 if(expr_type_id==ID_floatbv)
1173 if(expr_type_id==ID_rational)
1179 else if(op_type_id==ID_fixedbv)
1181 if(expr_type_id==ID_unsignedbv ||
1182 expr_type_id==ID_signedbv)
1188 else if(expr_type_id==ID_fixedbv)
1195 else if(expr_type_id == ID_bv)
1201 else if(op_type_id==ID_floatbv)
1205 if(expr_type_id==ID_unsignedbv ||
1206 expr_type_id==ID_signedbv)
1211 else if(expr_type_id==ID_floatbv)
1217 else if(expr_type_id==ID_fixedbv)
1227 else if(expr_type_id == ID_bv)
1232 else if(op_type_id==ID_bv)
1235 expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1236 expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1237 expr_type_id == ID_c_bit_field)
1241 if(expr_type_id != ID_c_enum_tag)
1247 result.type() = tag_type;
1248 return std::move(result);
1251 else if(expr_type_id == ID_floatbv)
1256 ieee_float.unpack(int_value);
1257 return ieee_float.to_expr();
1259 else if(expr_type_id == ID_fixedbv)
1264 fixedbv.set_value(int_value);
1265 return fixedbv.to_expr();
1268 else if(op_type_id==ID_c_enum_tag)
1275 auto new_expr = expr;
1280 else if(op_type_id==ID_c_enum)
1286 auto new_expr = expr;
1292 else if(operand.
id()==ID_typecast)
1297 op_type_id == expr_type_id &&
1298 (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv) &&
1302 auto new_expr = expr;
1308 else if(operand.
id()==ID_address_of)
1314 o.
type().
id() == ID_array &&
1332 if(pointer.
type().
id()!=ID_pointer)
1335 if(pointer.
id()==ID_if && pointer.
operands().size()==3)
1339 auto tmp_op1 = expr;
1343 auto tmp_op2 = expr;
1347 if_exprt tmp{if_expr.
cond(), tmp_op1_result, tmp_op2_result};
1352 if(pointer.
id()==ID_address_of)
1360 pointer.
id() == ID_plus && pointer.
operands().size() == 2 &&
1368 if(address_of.
object().
id()==ID_index)
1393 bool no_change =
true;
1399 auto with_expr = expr;
1401 const typet old_type_followed =
ns.
follow(with_expr.old().type());
1405 if(old_type_followed.
id() == ID_struct)
1407 if(with_expr.old().id() == ID_struct || with_expr.old().id() == ID_constant)
1409 while(with_expr.operands().size() > 1)
1412 with_expr.where().get(ID_component_name);
1414 if(!
to_struct_type(old_type_followed).has_component(component_name))
1417 std::size_t number =
1420 if(number >= with_expr.old().operands().size())
1423 with_expr.old().operands()[number].swap(with_expr.new_value());
1425 with_expr.operands().erase(++with_expr.operands().begin());
1426 with_expr.operands().erase(++with_expr.operands().begin());
1433 with_expr.old().type().id() == ID_array ||
1434 with_expr.old().type().id() == ID_vector)
1437 with_expr.old().id() == ID_array || with_expr.old().id() == ID_constant ||
1438 with_expr.old().id() == ID_vector)
1440 while(with_expr.operands().size() > 1)
1442 const auto i = numeric_cast<mp_integer>(with_expr.where());
1447 if(*i < 0 || *i >= with_expr.old().operands().size())
1450 with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
1451 with_expr.new_value());
1453 with_expr.operands().erase(++with_expr.operands().begin());
1454 with_expr.operands().erase(++with_expr.operands().begin());
1461 if(with_expr.operands().size() == 1)
1462 return with_expr.old();
1467 return std::move(with_expr);
1478 exprt *value_ptr=&updated_value;
1480 for(
const auto &e : designator)
1484 if(e.id()==ID_index_designator &&
1485 value_ptr->
id()==ID_array)
1492 if(*i < 0 || *i >= value_ptr->
operands().size())
1495 value_ptr = &value_ptr->
operands()[numeric_cast_v<std::size_t>(*i)];
1497 else if(e.id()==ID_member_designator &&
1498 value_ptr->
id()==ID_struct)
1501 e.get(ID_component_name);
1507 value_ptr = &designator_as_struct_expr.component(component_name,
ns);
1516 return updated_value;
1521 if(expr.
id()==ID_plus)
1523 if(expr.
type().
id()==ID_pointer)
1527 if(op.type().id() == ID_pointer)
1531 else if(expr.
id()==ID_typecast)
1534 const typet &op_type = typecast_expr.op().type();
1536 if(op_type.
id()==ID_pointer)
1541 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1548 const exprt &casted_expr = typecast_expr.op();
1549 if(casted_expr.
id() == ID_plus && casted_expr.
operands().size() == 2)
1553 const exprt &cand = plus_expr.
op0().
id() == ID_typecast
1557 if(cand.
id() == ID_typecast)
1561 if(typecast_op.id() == ID_address_of)
1566 typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1577 else if(expr.
id()==ID_address_of)
1581 if(
object.
id() == ID_index)
1587 else if(
object.
id() == ID_member)
1602 if(expr.
op().
id()==ID_if)
1613 if(el_size.has_value() && *el_size < 0)
1618 if(expr.
op().
id()==expr.
id())
1632 ((expr.
id() == ID_byte_extract_big_endian &&
1633 expr.
op().
id() == ID_byte_update_big_endian) ||
1634 (expr.
id() == ID_byte_extract_little_endian &&
1635 expr.
op().
id() == ID_byte_update_little_endian)) &&
1640 if(expr.
type() == op_byte_update.value().type())
1642 return op_byte_update.value();
1645 el_size.has_value() &&
1649 tmp.
op() = op_byte_update.value();
1657 auto offset = numeric_cast<mp_integer>(expr.
offset());
1658 if(!offset.has_value() || *offset < 0)
1664 *offset == 0 && ((expr.
id() == ID_byte_extract_little_endian &&
1667 (expr.
id() == ID_byte_extract_big_endian &&
1677 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1685 if(!el_size.has_value() || *el_size == 0)
1688 if(expr.
op().
id()==ID_array_of &&
1697 if(!const_bits_opt.has_value())
1700 std::string const_bits=const_bits_opt.value();
1702 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1705 while(
mp_integer(const_bits.size()) < *offset * 8 + *el_size)
1706 const_bits+=const_bits;
1708 std::string el_bits = std::string(
1710 numeric_cast_v<std::size_t>(*offset * 8),
1711 numeric_cast_v<std::size_t>(*el_size));
1714 el_bits, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1717 return std::move(*tmp);
1722 expr.
op().
id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
1737 const bool struct_has_flexible_array_member =
has_subtype(
1739 [&](
const typet &type) {
1740 if(type.id() != ID_struct && type.id() != ID_struct_tag)
1743 const struct_typet &st = to_struct_type(ns.follow(type));
1744 const auto &comps = st.components();
1745 if(comps.empty() || comps.back().type().id() != ID_array)
1749 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1750 return !size.has_value() || *size <= 1;
1754 bits.has_value() &&
mp_integer(bits->size()) >= *el_size + *offset * 8 &&
1755 !struct_has_flexible_array_member)
1757 std::string bits_cut = std::string(
1759 numeric_cast_v<std::size_t>(*offset * 8),
1760 numeric_cast_v<std::size_t>(*el_size));
1763 bits_cut, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1766 return std::move(*tmp);
1772 if(expr.
op().
id() == ID_struct || expr.
op().
id() == ID_union)
1774 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
1782 for(
const auto &comp : components)
1788 !component_bits.has_value() || *component_bits == 0 ||
1789 *component_bits % 8 != 0)
1795 auto member_offset_opt =
1798 if(!member_offset_opt.has_value())
1807 member_offset_opt.value(), expr.
offset().
type())});
1810 tmp.
type() = comp.type();
1811 tmp.offset() = new_offset;
1819 else if(expr.
type().
id() == ID_union || expr.
type().
id() == ID_union_tag)
1823 if(widest_member_opt.has_value())
1826 be.
type() = widest_member_opt->first.type();
1827 return union_exprt{widest_member_opt->first.get_name(),
1837 if(!subexpr.has_value() || subexpr.value() == expr)
1849 expr.
id() == expr.
op().
id() &&
1855 return std::move(tmp);
1858 const exprt &root = expr.
op();
1866 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
1867 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
1870 expr.
id()==ID_byte_update_little_endian ?
1871 ID_byte_extract_little_endian :
1872 ID_byte_extract_big_endian,
1873 value, offset, expr.
type());
1879 const auto offset_int = numeric_cast<mp_integer>(offset);
1881 root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
1882 *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
1883 *offset_int + *val_size <= *root_size)
1886 expr2bits(root, expr.
id() == ID_byte_update_little_endian,
ns);
1888 if(root_bits.has_value())
1890 const auto val_bits =
1891 expr2bits(value, expr.
id() == ID_byte_update_little_endian,
ns);
1893 if(val_bits.has_value())
1896 numeric_cast_v<std::size_t>(*offset_int * 8),
1897 numeric_cast_v<std::size_t>(*val_size),
1903 expr.
id() == ID_byte_update_little_endian,
1907 return std::move(*tmp);
1920 if(expr.
id()!=ID_byte_update_little_endian)
1923 if(value.
id()==ID_with)
1927 if(with.
old().
id()==ID_byte_extract_little_endian)
1934 if(!(root==extract.
op()))
1936 if(!(offset==extract.
offset()))
1940 if(tp.
id()==ID_struct)
1947 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
1962 tmp.set_value(std::move(new_value));
1967 else if(tp.
id()==ID_array)
1973 exprt index_offset =
1987 tmp.set_value(std::move(new_value));
1995 if(!offset_int.has_value() || *offset_int < 0)
2001 if(!val_size.has_value() || *val_size == 0)
2006 if(op_type.
id()==ID_struct)
2025 if(!m_offset.has_value())
2032 if(!m_size_bits.has_value() || *m_size_bits == 0 || (*m_size_bits) % 8 != 0)
2038 mp_integer m_size_bytes = (*m_size_bits) / 8;
2041 if(*m_offset + m_size_bytes <= *offset_int)
2045 update_size.has_value() && *update_size > 0 &&
2046 *m_offset >= *offset_int + *update_size)
2054 exprt member_name(ID_member_name);
2055 member_name.
set(ID_component_name,
component.get_name());
2060 *m_offset < *offset_int ||
2061 (*m_offset == *offset_int && update_size.has_value() &&
2062 *update_size > 0 && m_size_bytes > *update_size))
2065 ID_byte_update_little_endian,
2073 update_size.has_value() && *update_size > 0 &&
2074 *m_offset + m_size_bytes > *offset_int + *update_size)
2083 ID_byte_extract_little_endian,
2098 if(root.
id()==ID_array)
2102 if(!el_size.has_value() || *el_size == 0 ||
2103 (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
2113 if(*offset_int * 8 + (*val_size) <= m_offset_bits)
2116 if(*offset_int * 8 < m_offset_bits + *el_size)
2118 mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
2119 bytes_req-=val_offset;
2120 if(val_offset + bytes_req > (*val_size) / 8)
2121 bytes_req = (*val_size) / 8 - val_offset;
2124 ID_byte_extract_little_endian,
2134 *offset_int + val_offset - m_offset_bits / 8, offset.
type()),
2139 val_offset+=bytes_req;
2142 m_offset_bits += *el_size;
2145 return std::move(result);
2154 if(expr.
id() == ID_complex_real)
2158 if(complex_real_expr.op().id() == ID_complex)
2161 else if(expr.
id() == ID_complex_imag)
2165 if(complex_imag_expr.op().id() == ID_complex)
2178 (expr.
op0().
is_zero() && expr.
id() != ID_overflow_minus))
2190 op_type_id == ID_integer || op_type_id == ID_rational ||
2191 op_type_id == ID_real)
2196 if(op_type_id == ID_natural && expr.
id() != ID_overflow_minus)
2200 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2206 const auto op0_value = numeric_cast<mp_integer>(expr.
op0());
2207 const auto op1_value = numeric_cast<mp_integer>(expr.
op1());
2208 if(!op0_value.has_value() || !op1_value.has_value())
2212 if(expr.
id() == ID_overflow_plus)
2213 no_overflow_result = *op0_value + *op1_value;
2214 else if(expr.
id() == ID_overflow_minus)
2215 no_overflow_result = *op0_value - *op1_value;
2216 else if(expr.
id() == ID_overflow_mult)
2217 no_overflow_result = *op0_value * *op1_value;
2218 else if(expr.
id() == ID_overflow_shl)
2219 no_overflow_result = *op0_value << *op1_value;
2226 no_overflow_result < bv_type.smallest() ||
2227 no_overflow_result > bv_type.largest())
2245 op_type_id == ID_integer || op_type_id == ID_rational ||
2246 op_type_id == ID_real)
2251 if(op_type_id == ID_natural)
2255 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2261 const auto op_value = numeric_cast<mp_integer>(expr.
op());
2262 if(!op_value.has_value())
2266 if(expr.
id() == ID_overflow_unary_minus)
2267 no_overflow_result = -*op_value;
2274 no_overflow_result < bv_type.smallest() ||
2275 no_overflow_result > bv_type.largest())
2289 if(expr.
id()==ID_address_of)
2293 else if(expr.
id()==ID_if)
2302 if(r_it.has_changed())
2330 if(expr.
id()==ID_typecast)
2334 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2335 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2336 expr.
id()==ID_ge || expr.
id()==ID_le)
2340 else if(expr.
id()==ID_if)
2344 else if(expr.
id()==ID_lambda)
2348 else if(expr.
id()==ID_with)
2352 else if(expr.
id()==ID_update)
2356 else if(expr.
id()==ID_index)
2360 else if(expr.
id()==ID_member)
2364 else if(expr.
id()==ID_byte_update_little_endian ||
2365 expr.
id()==ID_byte_update_big_endian)
2369 else if(expr.
id()==ID_byte_extract_little_endian ||
2370 expr.
id()==ID_byte_extract_big_endian)
2374 else if(expr.
id()==ID_pointer_object)
2378 else if(expr.
id() == ID_is_dynamic_object)
2382 else if(expr.
id() == ID_is_invalid_pointer)
2386 else if(expr.
id()==ID_object_size)
2390 else if(expr.
id()==ID_good_pointer)
2394 else if(expr.
id()==ID_div)
2398 else if(expr.
id()==ID_mod)
2402 else if(expr.
id()==ID_bitnot)
2406 else if(expr.
id()==ID_bitand ||
2407 expr.
id()==ID_bitor ||
2408 expr.
id()==ID_bitxor)
2412 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2416 else if(expr.
id()==ID_power)
2420 else if(expr.
id()==ID_plus)
2424 else if(expr.
id()==ID_minus)
2428 else if(expr.
id()==ID_mult)
2432 else if(expr.
id()==ID_floatbv_plus ||
2433 expr.
id()==ID_floatbv_minus ||
2434 expr.
id()==ID_floatbv_mult ||
2435 expr.
id()==ID_floatbv_div)
2439 else if(expr.
id()==ID_floatbv_typecast)
2443 else if(expr.
id()==ID_unary_minus)
2447 else if(expr.
id()==ID_unary_plus)
2451 else if(expr.
id()==ID_not)
2455 else if(expr.
id()==ID_implies ||
2456 expr.
id()==ID_or || expr.
id()==ID_xor ||
2461 else if(expr.
id()==ID_dereference)
2465 else if(expr.
id()==ID_address_of)
2469 else if(expr.
id()==ID_pointer_offset)
2473 else if(expr.
id()==ID_extractbit)
2477 else if(expr.
id()==ID_concatenation)
2481 else if(expr.
id()==ID_extractbits)
2485 else if(expr.
id()==ID_ieee_float_equal ||
2486 expr.
id()==ID_ieee_float_notequal)
2490 else if(expr.
id() == ID_bswap)
2494 else if(expr.
id()==ID_isinf)
2498 else if(expr.
id()==ID_isnan)
2502 else if(expr.
id()==ID_isnormal)
2506 else if(expr.
id()==ID_abs)
2510 else if(expr.
id()==ID_sign)
2514 else if(expr.
id() == ID_popcount)
2518 else if(expr.
id() == ID_count_leading_zeros)
2522 else if(expr.
id() == ID_count_trailing_zeros)
2526 else if(expr.
id() == ID_function_application)
2530 else if(expr.
id() == ID_complex_real || expr.
id() == ID_complex_imag)
2535 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_minus ||
2536 expr.
id() == ID_overflow_mult || expr.
id() == ID_overflow_shl)
2540 else if(expr.
id() == ID_overflow_unary_minus)
2545 if(!no_change_join_operands)
2551 # ifdef DEBUG_ON_DEMAND
2556 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
2557 <<
" ---> " <<
format(
r.expr) <<
'\n';
2569 std::pair<simplify_expr_cachet::containert::iterator, bool>
2570 cache_result=simplify_expr_cache.container().
2571 insert(std::pair<exprt, exprt>(expr,
exprt()));
2573 if(!cache_result.second)
2575 const exprt &new_expr=cache_result.first->second;
2591 if(simplify_node_result.has_changed())
2594 tmp = simplify_node_result.expr;
2597 #ifdef USE_LOCAL_REPLACE_MAP
2599 replace_mapt::const_iterator it=local_replace_map.
find(tmp);
2600 if(it!=local_replace_map.end())
2606 if(!local_replace_map.empty() &&
2625 cache_result.first->second = tmp;
2628 return std::move(tmp);
2635 #ifdef DEBUG_ON_DEMAND
2637 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
2640 #ifdef DEBUG_ON_DEMAND
2642 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
2644 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 binary_overflow_exprt & to_binary_overflow_expr(const exprt &expr)
Cast an exprt to a binary_overflow_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const unary_overflow_exprt & to_unary_overflow_expr(const exprt &expr)
Cast an exprt to a unary_overflow_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_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 popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_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 union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Operator to return the address of an object.
Array constructor from list of elements.
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 & value() const
const exprt & offset() const
C enum tag type, i.e., c_enum_typet with an identifier.
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 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.
source_locationt & add_source_location()
const source_locationt & source_location() const
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.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
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.
void set(const irep_namet &name, const irep_idt &value)
const irept & find(const irep_namet &name) const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) 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_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 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
const componentst & components() 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.
const typet & subtype() const
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 lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, 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< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, 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 index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_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)