45 struct simplify_expr_cachet
49 typedef std::unordered_map<
52 typedef std::unordered_map<exprt, exprt, irep_hash> containert;
55 containert container_normal;
57 containert &container()
59 return container_normal;
63 simplify_expr_cachet simplify_expr_cache;
72 if(type.
id()==ID_floatbv)
78 else if(type.
id()==ID_signedbv ||
79 type.
id()==ID_unsignedbv)
81 auto value = numeric_cast<mp_integer>(
to_unary_expr(expr).op());
106 if(type.
id()==ID_floatbv)
111 else if(type.
id()==ID_signedbv ||
112 type.
id()==ID_unsignedbv)
114 const auto value = numeric_cast<mp_integer>(expr.
op());
115 if(value.has_value())
134 if(op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv)
138 std::size_t result = 0;
140 for(std::size_t i = 0; i < width; i++)
193 const auto first_value_opt =
203 const auto second_value_opt =
206 if(!second_value_opt)
214 const bool includes =
240 const auto numeric_length =
277 const bool first_shorter = s1_size < s2_size;
282 auto it_pair = std::mismatch(ops1.begin(), ops1.end(), ops2.begin());
284 if(it_pair.first == ops1.end())
293 first_shorter ? char1 - char2 : char2 - char1, expr.
type());
305 const bool search_from_end)
307 std::size_t starting_index = 0;
312 auto &starting_index_expr = expr.
arguments().at(2);
314 if(starting_index_expr.id() != ID_constant)
325 starting_index = numeric_cast_v<std::size_t>(idx);
340 const auto search_string_size = s1_data.
operands().size();
341 if(starting_index >= search_string_size)
346 unsigned long starting_offset =
347 starting_index > 0 ? (search_string_size - 1) - starting_index : 0;
370 ? starting_index > 0 ? starting_index : search_string_size
376 auto end = std::prev(s1_data.
operands().end(), starting_offset);
377 auto it = std::find_end(
384 std::distance(s1_data.
operands().begin(), it), expr.
type());
388 auto it = std::search(
389 std::next(s1_data.
operands().begin(), starting_index),
396 std::distance(s1_data.
operands().begin(), it), expr.
type());
399 else if(expr.
arguments().at(1).id() == ID_constant)
404 const auto c1_val = numeric_cast_v<mp_integer>(c1);
406 auto pred = [&](
const exprt &c2) {
409 return c1_val == c2_val;
414 auto it = std::find_if(
415 std::next(s1_data.
operands().rbegin(), starting_offset),
420 std::distance(s1_data.
operands().begin(), it.base() - 1),
425 auto it = std::find_if(
426 std::next(s1_data.
operands().begin(), starting_index),
431 std::distance(s1_data.
operands().begin(), it), expr.
type());
451 if(expr.
arguments().at(1).id() != ID_constant)
469 const auto i_opt = numeric_cast<std::size_t>(index);
471 if(!i_opt || *i_opt >= char_seq.
operands().size())
478 if(c.type() != expr.
type())
489 auto &operands = string_data.
operands();
490 for(
auto &operand : operands)
493 auto character = numeric_cast_v<unsigned int>(constant_value);
499 if(isalpha(character))
501 if(isupper(character))
503 from_integer(tolower(character), constant_value.type());
525 const auto first_value_opt =
535 const auto second_value_opt =
538 if(!second_value_opt)
551 bool is_equal = first_value == second_value;
570 const auto first_value_opt =
580 const auto second_value_opt =
583 if(!second_value_opt)
594 if(offset.id() != ID_constant)
602 offset_int + second_value.
operands().size();
605 exprt::operandst::const_iterator second_it =
607 for(
const auto &first_op : first_value.
operands())
611 else if(second_it == second_value.
operands().end())
613 else if(first_op != *second_it)
642 if(func_id == ID_cprover_string_startswith_func)
646 else if(func_id == ID_cprover_string_endswith_func)
650 else if(func_id == ID_cprover_string_is_empty_func)
654 else if(func_id == ID_cprover_string_compare_to_func)
658 else if(func_id == ID_cprover_string_index_of_func)
662 else if(func_id == ID_cprover_string_char_at_func)
666 else if(func_id == ID_cprover_string_contains_func)
670 else if(func_id == ID_cprover_string_last_index_of_func)
674 else if(func_id == ID_cprover_string_equals_ignore_case_func)
689 if(expr.
op().
id() == ID_infinity)
694 return std::move(tmp);
701 (expr_type.
id() == ID_unsignedbv || expr_type.
id() == ID_signedbv) &&
711 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
712 (op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv) &&
716 auto new_expr = expr;
728 if(expr_type.
id()==ID_bool)
733 op_type.
id() == ID_floatbv ? ID_ieee_float_notequal : ID_notequal,
741 op_type.
id() == ID_bool &&
742 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv ||
743 expr_type.
id() == ID_c_bool || expr_type.
id() == ID_c_bit_field))
761 const auto &typecast = expr_checked_cast<typecast_exprt>(expr.
op());
762 if(typecast.op().type()==expr_type)
764 return typecast.op();
770 if(expr_type.
id()==ID_c_bool &&
771 op_type.
id()!=ID_bool)
775 auto new_expr = expr;
789 return std::move(tmp);
795 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
796 op_type.
id() == ID_pointer)
798 auto new_expr = expr;
806 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
807 expr.
op().
id() == ID_typecast && expr.
op().
operands().size() == 1 &&
808 op_type.
id() == ID_pointer)
813 auto outer_cast = expr;
822 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
823 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus &&
828 if(((op_plus_expr.op0().id() == ID_typecast &&
830 (op_plus_expr.op0().is_constant() &&
835 if(sub_size.has_value())
837 auto new_expr = expr;
840 if(*sub_size == 0 || *sub_size == 1)
863 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
864 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv))
874 if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
875 op_id==ID_unary_minus ||
876 op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
895 else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
905 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
906 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus)
910 if(step.has_value() && *step != 0)
913 auto new_expr = expr;
915 new_expr.
op().
type() = size_t_type;
917 for(
auto &op : new_expr.op().operands())
919 if(op.type().id()==ID_pointer)
937 if(expr.
op().
id()==ID_if &&
944 auto new_expr=
if_exprt(expr.
op().
op0(), tmp_op1, tmp_op2, expr_type);
946 return std::move(new_expr);
951 const exprt &operand = expr.
op();
960 static_cast<const typet &
>(operand.
find(ID_C_c_sizeof_type));
962 if(op_type_id==ID_integer ||
963 op_type_id==ID_natural)
969 if(expr_type_id==ID_bool)
974 if(expr_type_id==ID_unsignedbv ||
975 expr_type_id==ID_signedbv ||
976 expr_type_id==ID_c_enum ||
977 expr_type_id==ID_c_bit_field ||
978 expr_type_id==ID_integer)
982 else if(expr_type_id == ID_c_enum_tag)
985 if(!c_enum_type.is_incomplete())
988 tmp.
type() = expr_type;
989 return std::move(tmp);
993 else if(op_type_id==ID_rational)
996 else if(op_type_id==ID_real)
999 else if(op_type_id==ID_bool)
1001 if(expr_type_id==ID_unsignedbv ||
1002 expr_type_id==ID_signedbv ||
1003 expr_type_id==ID_integer ||
1004 expr_type_id==ID_natural ||
1005 expr_type_id==ID_rational ||
1006 expr_type_id==ID_c_bool ||
1007 expr_type_id==ID_c_enum ||
1008 expr_type_id==ID_c_bit_field)
1019 else if(expr_type_id==ID_c_enum_tag)
1022 if(!c_enum_type.is_incomplete())
1024 unsigned int_value = operand.
is_true() ? 1u : 0u;
1026 tmp.
type()=expr_type;
1027 return std::move(tmp);
1030 else if(expr_type_id==ID_pointer &&
1037 else if(op_type_id==ID_unsignedbv ||
1038 op_type_id==ID_signedbv ||
1039 op_type_id==ID_c_bit_field ||
1040 op_type_id==ID_c_bool)
1047 if(expr_type_id==ID_bool)
1052 if(expr_type_id==ID_c_bool)
1057 if(expr_type_id==ID_integer)
1062 if(expr_type_id==ID_natural)
1070 if(expr_type_id==ID_unsignedbv ||
1071 expr_type_id==ID_signedbv ||
1072 expr_type_id==ID_bv ||
1073 expr_type_id==ID_c_bit_field)
1078 result.set(ID_C_c_sizeof_type, c_sizeof_type);
1080 return std::move(result);
1083 if(expr_type_id==ID_c_enum_tag)
1086 if(!c_enum_type.is_incomplete())
1089 tmp.
type()=expr_type;
1090 return std::move(tmp);
1094 if(expr_type_id==ID_c_enum)
1099 if(expr_type_id==ID_fixedbv)
1111 if(expr_type_id==ID_floatbv)
1123 if(expr_type_id==ID_rational)
1129 else if(op_type_id==ID_fixedbv)
1131 if(expr_type_id==ID_unsignedbv ||
1132 expr_type_id==ID_signedbv)
1138 else if(expr_type_id==ID_fixedbv)
1145 else if(expr_type_id == ID_bv)
1151 else if(op_type_id==ID_floatbv)
1155 if(expr_type_id==ID_unsignedbv ||
1156 expr_type_id==ID_signedbv)
1161 else if(expr_type_id==ID_floatbv)
1167 else if(expr_type_id==ID_fixedbv)
1177 else if(expr_type_id == ID_bv)
1182 else if(op_type_id==ID_bv)
1185 expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1186 expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1187 expr_type_id == ID_c_bit_field)
1191 if(expr_type_id != ID_c_enum_tag)
1197 result.type() = tag_type;
1198 return std::move(result);
1201 else if(expr_type_id == ID_floatbv)
1206 ieee_float.unpack(int_value);
1207 return ieee_float.to_expr();
1209 else if(expr_type_id == ID_fixedbv)
1214 fixedbv.set_value(int_value);
1215 return fixedbv.to_expr();
1218 else if(op_type_id==ID_c_enum_tag)
1225 auto new_expr = expr;
1230 else if(op_type_id==ID_c_enum)
1236 auto new_expr = expr;
1242 else if(operand.
id()==ID_typecast)
1247 op_type_id == expr_type_id &&
1248 (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv) &&
1252 auto new_expr = expr;
1258 else if(operand.
id()==ID_address_of)
1264 o.
type().
id() == ID_array &&
1282 if(pointer.
type().
id()!=ID_pointer)
1285 if(pointer.
id()==ID_if && pointer.
operands().size()==3)
1289 auto tmp_op1 = expr;
1293 auto tmp_op2 = expr;
1297 if_exprt tmp{if_expr.
cond(), tmp_op1_result, tmp_op2_result};
1302 if(pointer.
id()==ID_address_of)
1310 pointer.
id() == ID_plus && pointer.
operands().size() == 2 &&
1318 if(address_of.
object().
id()==ID_index)
1343 bool no_change =
true;
1349 auto with_expr = expr;
1351 const typet old_type_followed =
ns.
follow(with_expr.old().type());
1355 if(old_type_followed.
id() == ID_struct)
1357 if(with_expr.old().id() == ID_struct || with_expr.old().id() == ID_constant)
1359 while(with_expr.operands().size() > 1)
1362 with_expr.where().get(ID_component_name);
1364 if(!
to_struct_type(old_type_followed).has_component(component_name))
1367 std::size_t number =
1370 if(number >= with_expr.old().operands().size())
1373 with_expr.old().operands()[number].swap(with_expr.new_value());
1375 with_expr.operands().erase(++with_expr.operands().begin());
1376 with_expr.operands().erase(++with_expr.operands().begin());
1383 with_expr.old().type().id() == ID_array ||
1384 with_expr.old().type().id() == ID_vector)
1387 with_expr.old().id() == ID_array || with_expr.old().id() == ID_constant ||
1388 with_expr.old().id() == ID_vector)
1390 while(with_expr.operands().size() > 1)
1392 const auto i = numeric_cast<mp_integer>(with_expr.where());
1397 if(*i < 0 || *i >= with_expr.old().operands().size())
1400 with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
1401 with_expr.new_value());
1403 with_expr.operands().erase(++with_expr.operands().begin());
1404 with_expr.operands().erase(++with_expr.operands().begin());
1411 if(with_expr.operands().size() == 1)
1412 return with_expr.old();
1417 return std::move(with_expr);
1428 exprt *value_ptr=&updated_value;
1430 for(
const auto &e : designator)
1434 if(e.id()==ID_index_designator &&
1435 value_ptr->
id()==ID_array)
1442 if(*i < 0 || *i >= value_ptr->
operands().size())
1445 value_ptr = &value_ptr->
operands()[numeric_cast_v<std::size_t>(*i)];
1447 else if(e.id()==ID_member_designator &&
1448 value_ptr->
id()==ID_struct)
1451 e.get(ID_component_name);
1457 value_ptr = &designator_as_struct_expr.component(component_name,
ns);
1466 return updated_value;
1471 if(expr.
id()==ID_plus)
1473 if(expr.
type().
id()==ID_pointer)
1477 if(op.type().id() == ID_pointer)
1481 else if(expr.
id()==ID_typecast)
1484 const typet &op_type = typecast_expr.op().type();
1486 if(op_type.
id()==ID_pointer)
1491 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1498 const exprt &casted_expr = typecast_expr.op();
1499 if(casted_expr.
id() == ID_plus && casted_expr.
operands().size() == 2)
1503 const exprt &cand = plus_expr.
op0().
id() == ID_typecast
1507 if(cand.
id() == ID_typecast)
1511 if(typecast_op.id() == ID_address_of)
1516 typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1527 else if(expr.
id()==ID_address_of)
1531 if(
object.
id() == ID_index)
1537 else if(
object.
id() == ID_member)
1552 if(expr.
op().
id()==ID_if)
1563 if(el_size.has_value() && *el_size < 0)
1568 if(expr.
op().
id()==expr.
id())
1582 ((expr.
id() == ID_byte_extract_big_endian &&
1583 expr.
op().
id() == ID_byte_update_big_endian) ||
1584 (expr.
id() == ID_byte_extract_little_endian &&
1585 expr.
op().
id() == ID_byte_update_little_endian)) &&
1590 if(expr.
type() == op_byte_update.value().type())
1592 return op_byte_update.value();
1595 el_size.has_value() &&
1599 tmp.
op() = op_byte_update.value();
1607 auto offset = numeric_cast<mp_integer>(expr.
offset());
1608 if(!offset.has_value() || *offset < 0)
1621 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1629 if(!el_size.has_value() || *el_size == 0)
1632 if(expr.
op().
id()==ID_array_of &&
1640 if(!const_bits_opt.has_value())
1643 std::string const_bits=const_bits_opt.value();
1645 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1648 while(
mp_integer(const_bits.size()) < *offset * 8 + *el_size)
1649 const_bits+=const_bits;
1651 std::string el_bits = std::string(
1653 numeric_cast_v<std::size_t>(*offset * 8),
1654 numeric_cast_v<std::size_t>(*el_size));
1657 el_bits, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1660 return std::move(*tmp);
1665 expr.
op().
id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
1680 const bool struct_has_flexible_array_member =
has_subtype(
1682 [&](
const typet &type) {
1683 if(type.id() != ID_struct && type.id() != ID_struct_tag)
1686 const struct_typet &st = to_struct_type(ns.follow(type));
1687 const auto &comps = st.components();
1688 if(comps.empty() || comps.back().type().id() != ID_array)
1692 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1693 return !size.has_value() || *size <= 1;
1697 bits.has_value() &&
mp_integer(bits->size()) >= *el_size + *offset * 8 &&
1698 !struct_has_flexible_array_member)
1700 std::string bits_cut = std::string(
1702 numeric_cast_v<std::size_t>(*offset * 8),
1703 numeric_cast_v<std::size_t>(*el_size));
1706 bits_cut, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1709 return std::move(*tmp);
1715 if(!subexpr.has_value() || subexpr.value() == expr)
1727 expr.
id() == expr.
op().
id() &&
1733 return std::move(tmp);
1736 const exprt &root = expr.
op();
1744 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
1745 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
1748 expr.
id()==ID_byte_update_little_endian ?
1749 ID_byte_extract_little_endian :
1750 ID_byte_extract_big_endian,
1751 value, offset, expr.
type());
1757 const auto offset_int = numeric_cast<mp_integer>(offset);
1759 root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
1760 *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
1761 *offset_int + *val_size <= *root_size)
1764 expr2bits(root, expr.
id() == ID_byte_update_little_endian,
ns);
1766 if(root_bits.has_value())
1768 const auto val_bits =
1769 expr2bits(value, expr.
id() == ID_byte_update_little_endian,
ns);
1771 if(val_bits.has_value())
1774 numeric_cast_v<std::size_t>(*offset_int * 8),
1775 numeric_cast_v<std::size_t>(*val_size),
1781 expr.
id() == ID_byte_update_little_endian,
1785 return std::move(*tmp);
1798 if(expr.
id()!=ID_byte_update_little_endian)
1801 if(value.
id()==ID_with)
1805 if(with.
old().
id()==ID_byte_extract_little_endian)
1812 if(!(root==extract.
op()))
1814 if(!(offset==extract.
offset()))
1818 if(tp.
id()==ID_struct)
1825 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
1840 tmp.set_value(std::move(new_value));
1845 else if(tp.
id()==ID_array)
1851 exprt index_offset =
1865 tmp.set_value(std::move(new_value));
1873 if(!offset_int.has_value() || *offset_int < 0)
1879 if(!val_size.has_value() || *val_size == 0)
1884 if(op_type.
id()==ID_struct)
1903 if(!m_offset.has_value())
1910 if(!m_size_bits.has_value() || *m_size_bits == 0 || (*m_size_bits) % 8 != 0)
1916 mp_integer m_size_bytes = (*m_size_bits) / 8;
1919 if(*m_offset + m_size_bytes <= *offset_int)
1923 update_size.has_value() && *update_size > 0 &&
1924 *m_offset >= *offset_int + *update_size)
1932 exprt member_name(ID_member_name);
1933 member_name.
set(ID_component_name,
component.get_name());
1938 *m_offset < *offset_int ||
1939 (*m_offset == *offset_int && update_size.has_value() &&
1940 *update_size > 0 && m_size_bytes > *update_size))
1943 ID_byte_update_little_endian,
1951 update_size.has_value() && *update_size > 0 &&
1952 *m_offset + m_size_bytes > *offset_int + *update_size)
1961 ID_byte_extract_little_endian,
1976 if(root.
id()==ID_array)
1980 if(!el_size.has_value() || *el_size == 0 ||
1981 (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
1991 if(*offset_int * 8 + (*val_size) <= m_offset_bits)
1994 if(*offset_int * 8 < m_offset_bits + *el_size)
1996 mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
1997 bytes_req-=val_offset;
1998 if(val_offset + bytes_req > (*val_size) / 8)
1999 bytes_req = (*val_size) / 8 - val_offset;
2012 *offset_int + val_offset - m_offset_bits / 8, offset.
type()),
2017 val_offset+=bytes_req;
2020 m_offset_bits += *el_size;
2023 return std::move(result);
2032 if(expr.
id() == ID_complex_real)
2036 if(complex_real_expr.op().id() == ID_complex)
2039 else if(expr.
id() == ID_complex_imag)
2043 if(complex_imag_expr.op().id() == ID_complex)
2056 (expr.
op0().
is_zero() && expr.
id() != ID_overflow_minus))
2068 op_type_id == ID_integer || op_type_id == ID_rational ||
2069 op_type_id == ID_real)
2074 if(op_type_id == ID_natural && expr.
id() != ID_overflow_minus)
2078 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2084 const auto op0_value = numeric_cast<mp_integer>(expr.
op0());
2085 const auto op1_value = numeric_cast<mp_integer>(expr.
op1());
2086 if(!op0_value.has_value() || !op1_value.has_value())
2090 if(expr.
id() == ID_overflow_plus)
2091 no_overflow_result = *op0_value + *op1_value;
2092 else if(expr.
id() == ID_overflow_minus)
2093 no_overflow_result = *op0_value - *op1_value;
2094 else if(expr.
id() == ID_overflow_mult)
2095 no_overflow_result = *op0_value * *op1_value;
2096 else if(expr.
id() == ID_overflow_shl)
2097 no_overflow_result = *op0_value << *op1_value;
2104 no_overflow_result < bv_type.smallest() ||
2105 no_overflow_result > bv_type.largest())
2123 op_type_id == ID_integer || op_type_id == ID_rational ||
2124 op_type_id == ID_real)
2129 if(op_type_id == ID_natural)
2133 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2139 const auto op_value = numeric_cast<mp_integer>(expr.
op());
2140 if(!op_value.has_value())
2144 if(expr.
id() == ID_overflow_unary_minus)
2145 no_overflow_result = -*op_value;
2152 no_overflow_result < bv_type.smallest() ||
2153 no_overflow_result > bv_type.largest())
2167 if(expr.
id()==ID_address_of)
2171 else if(expr.
id()==ID_if)
2180 if(r_it.has_changed())
2208 if(expr.
id()==ID_typecast)
2212 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2213 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2214 expr.
id()==ID_ge || expr.
id()==ID_le)
2218 else if(expr.
id()==ID_if)
2222 else if(expr.
id()==ID_lambda)
2226 else if(expr.
id()==ID_with)
2230 else if(expr.
id()==ID_update)
2234 else if(expr.
id()==ID_index)
2238 else if(expr.
id()==ID_member)
2242 else if(expr.
id()==ID_byte_update_little_endian ||
2243 expr.
id()==ID_byte_update_big_endian)
2247 else if(expr.
id()==ID_byte_extract_little_endian ||
2248 expr.
id()==ID_byte_extract_big_endian)
2252 else if(expr.
id()==ID_pointer_object)
2256 else if(expr.
id() == ID_is_dynamic_object)
2260 else if(expr.
id() == ID_is_invalid_pointer)
2264 else if(expr.
id()==ID_object_size)
2268 else if(expr.
id()==ID_good_pointer)
2272 else if(expr.
id()==ID_div)
2276 else if(expr.
id()==ID_mod)
2280 else if(expr.
id()==ID_bitnot)
2284 else if(expr.
id()==ID_bitand ||
2285 expr.
id()==ID_bitor ||
2286 expr.
id()==ID_bitxor)
2290 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2294 else if(expr.
id()==ID_power)
2298 else if(expr.
id()==ID_plus)
2302 else if(expr.
id()==ID_minus)
2306 else if(expr.
id()==ID_mult)
2310 else if(expr.
id()==ID_floatbv_plus ||
2311 expr.
id()==ID_floatbv_minus ||
2312 expr.
id()==ID_floatbv_mult ||
2313 expr.
id()==ID_floatbv_div)
2317 else if(expr.
id()==ID_floatbv_typecast)
2321 else if(expr.
id()==ID_unary_minus)
2325 else if(expr.
id()==ID_unary_plus)
2329 else if(expr.
id()==ID_not)
2333 else if(expr.
id()==ID_implies ||
2334 expr.
id()==ID_or || expr.
id()==ID_xor ||
2339 else if(expr.
id()==ID_dereference)
2343 else if(expr.
id()==ID_address_of)
2347 else if(expr.
id()==ID_pointer_offset)
2351 else if(expr.
id()==ID_extractbit)
2355 else if(expr.
id()==ID_concatenation)
2359 else if(expr.
id()==ID_extractbits)
2363 else if(expr.
id()==ID_ieee_float_equal ||
2364 expr.
id()==ID_ieee_float_notequal)
2368 else if(expr.
id() == ID_bswap)
2372 else if(expr.
id()==ID_isinf)
2376 else if(expr.
id()==ID_isnan)
2380 else if(expr.
id()==ID_isnormal)
2384 else if(expr.
id()==ID_abs)
2388 else if(expr.
id()==ID_sign)
2392 else if(expr.
id() == ID_popcount)
2396 else if(expr.
id() == ID_function_application)
2400 else if(expr.
id() == ID_complex_real || expr.
id() == ID_complex_imag)
2405 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_minus ||
2406 expr.
id() == ID_overflow_mult || expr.
id() == ID_overflow_shl)
2410 else if(expr.
id() == ID_overflow_unary_minus)
2415 if(!no_change_join_operands)
2421 # ifdef DEBUG_ON_DEMAND
2426 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
2427 <<
" ---> " <<
format(
r.expr) <<
'\n';
2439 std::pair<simplify_expr_cachet::containert::iterator, bool>
2440 cache_result=simplify_expr_cache.container().
2441 insert(std::pair<exprt, exprt>(expr,
exprt()));
2443 if(!cache_result.second)
2445 const exprt &new_expr=cache_result.first->second;
2461 if(simplify_node_result.has_changed())
2464 tmp = simplify_node_result.expr;
2467 #ifdef USE_LOCAL_REPLACE_MAP
2469 replace_mapt::const_iterator it=local_replace_map.
find(tmp);
2470 if(it!=local_replace_map.end())
2476 if(!local_replace_map.empty() &&
2495 cache_result.first->second = tmp;
2498 return std::move(tmp);
2505 #ifdef DEBUG_ON_DEMAND
2507 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
2510 #ifdef DEBUG_ON_DEMAND
2512 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
2514 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 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 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 popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
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)
Operator to return the address of an object.
Array constructor from list of elements.
A base class for binary expressions.
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)
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.
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 &) 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_overflow_unary(const unary_exprt &)
Try to simplify overflow-unary-.
resultt simplify_byte_extract(const byte_extract_exprt &)
resultt simplify_abs(const abs_exprt &)
resultt simplify_overflow_binary(const binary_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
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_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_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_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 &)
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.
The type of an expression, extends irept.
const typet & subtype() const
Generic base class for unary expressions.
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 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)
exprt pointer_offset_sum(const exprt &a, const exprt &b)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
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 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 struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_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)
irep_idt byte_extract_id()