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++)
153 const bool is_little_endian =
156 const auto const_bits_opt =
expr2bits(expr.
op(), is_little_endian,
ns);
158 if(!const_bits_opt.has_value())
161 std::size_t n_leading_zeros =
162 is_little_endian ? const_bits_opt->rfind(
'1') : const_bits_opt->find(
'1');
163 if(n_leading_zeros == std::string::npos)
168 n_leading_zeros = const_bits_opt->size();
170 else if(is_little_endian)
171 n_leading_zeros = const_bits_opt->size() - n_leading_zeros - 1;
179 const bool is_little_endian =
182 const auto const_bits_opt =
expr2bits(expr.
op(), is_little_endian,
ns);
184 if(!const_bits_opt.has_value())
187 std::size_t n_trailing_zeros =
188 is_little_endian ? const_bits_opt->find(
'1') : const_bits_opt->rfind(
'1');
189 if(n_trailing_zeros == std::string::npos)
194 n_trailing_zeros = const_bits_opt->size();
196 else if(!is_little_endian)
197 n_trailing_zeros = const_bits_opt->size() - n_trailing_zeros - 1;
205 const bool is_little_endian =
208 const auto const_bits_opt =
expr2bits(expr.
op(), is_little_endian,
ns);
210 if(!const_bits_opt.has_value())
213 std::size_t first_one_bit =
214 is_little_endian ? const_bits_opt->find(
'1') : const_bits_opt->rfind(
'1');
215 if(first_one_bit == std::string::npos)
217 else if(is_little_endian)
220 first_one_bit = const_bits_opt->size() - first_one_bit;
267 const auto first_value_opt =
277 const auto second_value_opt =
280 if(!second_value_opt)
288 const bool includes =
314 const auto numeric_length =
351 const bool first_shorter = s1_size < s2_size;
356 auto it_pair = std::mismatch(ops1.begin(), ops1.end(), ops2.begin());
358 if(it_pair.first == ops1.end())
367 first_shorter ? char1 - char2 : char2 - char1, expr.
type());
379 const bool search_from_end)
381 std::size_t starting_index = 0;
386 auto &starting_index_expr = expr.
arguments().at(2);
388 if(!starting_index_expr.is_constant())
399 starting_index = numeric_cast_v<std::size_t>(idx);
414 const auto search_string_size = s1_data.
operands().size();
415 if(starting_index >= search_string_size)
420 unsigned long starting_offset =
421 starting_index > 0 ? (search_string_size - 1) - starting_index : 0;
444 ? starting_index > 0 ? starting_index : search_string_size
450 auto end = std::prev(s1_data.
operands().end(), starting_offset);
451 auto it = std::find_end(
458 std::distance(s1_data.
operands().begin(), it), expr.
type());
462 auto it = std::search(
463 std::next(s1_data.
operands().begin(), starting_index),
470 std::distance(s1_data.
operands().begin(), it), expr.
type());
473 else if(expr.
arguments().at(1).is_constant())
478 const auto c1_val = numeric_cast_v<mp_integer>(c1);
480 auto pred = [&](
const exprt &c2) {
483 return c1_val == c2_val;
488 auto it = std::find_if(
489 std::next(s1_data.
operands().rbegin(), starting_offset),
494 std::distance(s1_data.
operands().begin(), it.base() - 1),
499 auto it = std::find_if(
500 std::next(s1_data.
operands().begin(), starting_index),
505 std::distance(s1_data.
operands().begin(), it), expr.
type());
525 if(!expr.
arguments().at(1).is_constant())
543 const auto i_opt = numeric_cast<std::size_t>(index);
545 if(!i_opt || *i_opt >= char_seq.
operands().size())
552 if(c.type() != expr.
type())
563 auto &operands = string_data.
operands();
564 for(
auto &operand : operands)
567 auto character = numeric_cast_v<unsigned int>(constant_value);
599 const auto first_value_opt =
609 const auto second_value_opt =
612 if(!second_value_opt)
625 bool is_equal = first_value == second_value;
644 const auto first_value_opt =
654 const auto second_value_opt =
657 if(!second_value_opt)
668 if(!offset.is_constant())
676 offset_int + second_value.
operands().size();
679 exprt::operandst::const_iterator second_it =
681 for(
const auto &first_op : first_value.
operands())
685 else if(second_it == second_value.
operands().end())
687 else if(first_op != *second_it)
716 if(func_id == ID_cprover_string_startswith_func)
720 else if(func_id == ID_cprover_string_endswith_func)
724 else if(func_id == ID_cprover_string_is_empty_func)
728 else if(func_id == ID_cprover_string_compare_to_func)
732 else if(func_id == ID_cprover_string_index_of_func)
736 else if(func_id == ID_cprover_string_char_at_func)
740 else if(func_id == ID_cprover_string_contains_func)
744 else if(func_id == ID_cprover_string_last_index_of_func)
748 else if(func_id == ID_cprover_string_equals_ignore_case_func)
763 if(expr.
op().
id() == ID_infinity)
768 return std::move(tmp);
775 (expr_type.
id() == ID_unsignedbv || expr_type.
id() == ID_signedbv) &&
785 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
786 (op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv ||
787 op_type.
id() == ID_bv) &&
791 auto new_expr = expr;
803 if(expr_type.
id()==ID_bool)
808 op_type.
id() == ID_floatbv ? ID_ieee_float_notequal : ID_notequal,
816 op_type.
id() == ID_bool &&
817 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv ||
818 expr_type.
id() == ID_c_bool || expr_type.
id() == ID_c_bit_field))
824 if_exprt{expr.
op(), std::move(one), std::move(zero)}));
838 const auto &typecast = expr_checked_cast<typecast_exprt>(expr.
op());
839 if(typecast.op().type()==expr_type)
841 return typecast.op();
847 if(expr_type.
id()==ID_c_bool &&
848 op_type.
id()!=ID_bool)
852 auto new_expr = expr;
866 return std::move(tmp);
872 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
873 op_type.
id() == ID_pointer)
875 auto new_expr = expr;
883 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
884 expr.
op().
id() == ID_typecast && expr.
op().
operands().size() == 1 &&
885 op_type.
id() == ID_pointer)
890 auto outer_cast = expr;
899 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
900 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus &&
906 (op_plus_expr.op0().id() == ID_typecast &&
908 (op_plus_expr.op0().is_constant() &&
913 if(sub_size.has_value())
915 auto new_expr = expr;
920 if(*sub_size == 0 || *sub_size == 1)
921 new_expr.op() = offset_expr;
942 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
943 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv))
953 if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
954 op_id==ID_unary_minus ||
955 op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
974 else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
984 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
985 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus)
990 if(step.has_value() && *step != 0)
993 auto new_expr = expr;
995 new_expr.
op().
type() = size_t_type;
997 for(
auto &op : new_expr.op().operands())
1000 if(op.type().id() != ID_pointer && *step > 1)
1005 op = std::move(new_op);
1015 const exprt &operand = expr.
op();
1023 typet c_sizeof_type=
1024 static_cast<const typet &
>(operand.
find(ID_C_c_sizeof_type));
1026 if(op_type_id==ID_integer ||
1027 op_type_id==ID_natural)
1033 if(expr_type_id==ID_bool)
1038 if(expr_type_id==ID_unsignedbv ||
1039 expr_type_id==ID_signedbv ||
1040 expr_type_id==ID_c_enum ||
1041 expr_type_id==ID_c_bit_field ||
1042 expr_type_id==ID_integer)
1046 else if(expr_type_id == ID_c_enum_tag)
1049 if(!c_enum_type.is_incomplete())
1052 tmp.
type() = expr_type;
1053 return std::move(tmp);
1057 else if(op_type_id==ID_rational)
1060 else if(op_type_id==ID_real)
1063 else if(op_type_id==ID_bool)
1065 if(expr_type_id==ID_unsignedbv ||
1066 expr_type_id==ID_signedbv ||
1067 expr_type_id==ID_integer ||
1068 expr_type_id==ID_natural ||
1069 expr_type_id==ID_rational ||
1070 expr_type_id==ID_c_bool ||
1071 expr_type_id==ID_c_enum ||
1072 expr_type_id==ID_c_bit_field)
1083 else if(expr_type_id==ID_c_enum_tag)
1086 if(!c_enum_type.is_incomplete())
1088 unsigned int_value = operand.
is_true() ? 1u : 0u;
1090 tmp.
type()=expr_type;
1091 return std::move(tmp);
1094 else if(expr_type_id==ID_pointer &&
1101 else if(op_type_id==ID_unsignedbv ||
1102 op_type_id==ID_signedbv ||
1103 op_type_id==ID_c_bit_field ||
1104 op_type_id==ID_c_bool)
1111 if(expr_type_id==ID_bool)
1116 if(expr_type_id==ID_c_bool)
1121 if(expr_type_id==ID_integer)
1126 if(expr_type_id==ID_natural)
1134 if(expr_type_id==ID_unsignedbv ||
1135 expr_type_id==ID_signedbv ||
1136 expr_type_id==ID_bv ||
1137 expr_type_id==ID_c_bit_field)
1142 result.set(ID_C_c_sizeof_type, c_sizeof_type);
1144 return std::move(result);
1147 if(expr_type_id==ID_c_enum_tag)
1150 if(!c_enum_type.is_incomplete())
1153 tmp.
type()=expr_type;
1154 return std::move(tmp);
1158 if(expr_type_id==ID_c_enum)
1163 if(expr_type_id==ID_fixedbv)
1175 if(expr_type_id==ID_floatbv)
1187 if(expr_type_id==ID_rational)
1193 else if(op_type_id==ID_fixedbv)
1195 if(expr_type_id==ID_unsignedbv ||
1196 expr_type_id==ID_signedbv)
1202 else if(expr_type_id==ID_fixedbv)
1209 else if(expr_type_id == ID_bv)
1215 else if(op_type_id==ID_floatbv)
1219 if(expr_type_id==ID_unsignedbv ||
1220 expr_type_id==ID_signedbv)
1225 else if(expr_type_id==ID_floatbv)
1231 else if(expr_type_id==ID_fixedbv)
1241 else if(expr_type_id == ID_bv)
1246 else if(op_type_id==ID_bv)
1249 expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1250 expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1251 expr_type_id == ID_c_bit_field)
1255 if(expr_type_id != ID_c_enum_tag)
1261 result.type() = tag_type;
1262 return std::move(result);
1265 else if(expr_type_id == ID_floatbv)
1270 ieee_float.unpack(int_value);
1271 return ieee_float.to_expr();
1273 else if(expr_type_id == ID_fixedbv)
1278 fixedbv.set_value(int_value);
1279 return fixedbv.to_expr();
1282 else if(op_type_id==ID_c_enum_tag)
1284 const typet &base_type =
1286 if(base_type.
id()==ID_signedbv || base_type.
id()==ID_unsignedbv)
1289 auto new_expr = expr;
1290 new_expr.
op().
type() = base_type;
1294 else if(op_type_id==ID_c_enum)
1297 if(base_type.
id()==ID_signedbv || base_type.
id()==ID_unsignedbv)
1300 auto new_expr = expr;
1301 new_expr.
op().
type() = base_type;
1306 else if(operand.
id()==ID_typecast)
1311 op_type_id == expr_type_id &&
1312 (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1313 expr_type_id == ID_bv) &&
1317 auto new_expr = expr;
1323 else if(operand.
id()==ID_address_of)
1329 o.
type().
id() == ID_array &&
1351 expr.
op().
id() == ID_if && expr_type.
id() != ID_floatbv &&
1352 op_type.
id() != ID_floatbv)
1360 if(r_it.has_changed())
1363 tmp.
op() = r_it.expr;
1376 if(pointer.
type().
id()!=ID_pointer)
1379 if(pointer.
id()==ID_address_of)
1387 pointer.
id() == ID_plus && pointer.
operands().size() == 2 &&
1395 if(address_of.
object().
id()==ID_index)
1417 if(pointer.
id() == ID_if)
1425 if(r_it.has_changed())
1444 bool no_change =
true;
1450 auto with_expr = expr;
1452 const typet old_type_followed =
ns.
follow(with_expr.old().type());
1456 if(old_type_followed.
id() == ID_struct)
1458 if(with_expr.old().id() == ID_struct || with_expr.old().is_constant())
1460 while(with_expr.operands().size() > 1)
1463 with_expr.where().get(ID_component_name);
1465 if(!
to_struct_type(old_type_followed).has_component(component_name))
1468 std::size_t number =
1471 if(number >= with_expr.old().operands().size())
1474 with_expr.old().operands()[number].swap(with_expr.new_value());
1476 with_expr.operands().erase(++with_expr.operands().begin());
1477 with_expr.operands().erase(++with_expr.operands().begin());
1484 with_expr.old().type().id() == ID_array ||
1485 with_expr.old().type().id() == ID_vector)
1488 with_expr.old().id() == ID_array || with_expr.old().is_constant() ||
1489 with_expr.old().id() == ID_vector)
1491 while(with_expr.operands().size() > 1)
1493 const auto i = numeric_cast<mp_integer>(with_expr.where());
1498 if(*i < 0 || *i >= with_expr.old().operands().size())
1501 with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
1502 with_expr.new_value());
1504 with_expr.operands().erase(++with_expr.operands().begin());
1505 with_expr.operands().erase(++with_expr.operands().begin());
1512 if(with_expr.operands().size() == 1)
1513 return with_expr.old();
1518 return std::move(with_expr);
1529 exprt *value_ptr=&updated_value;
1531 for(
const auto &e : designator)
1535 if(e.id()==ID_index_designator &&
1536 value_ptr->
id()==ID_array)
1543 if(*i < 0 || *i >= value_ptr->
operands().size())
1546 value_ptr = &value_ptr->
operands()[numeric_cast_v<std::size_t>(*i)];
1548 else if(e.id()==ID_member_designator &&
1549 value_ptr->
id()==ID_struct)
1552 e.get(ID_component_name);
1558 value_ptr = &designator_as_struct_expr.component(component_name,
ns);
1567 return updated_value;
1572 if(expr.
id()==ID_plus)
1574 if(expr.
type().
id()==ID_pointer)
1578 if(op.type().id() == ID_pointer)
1582 else if(expr.
id()==ID_typecast)
1585 const typet &op_type = typecast_expr.op().type();
1587 if(op_type.
id()==ID_pointer)
1592 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1599 const exprt &casted_expr = typecast_expr.op();
1600 if(casted_expr.
id() == ID_plus && casted_expr.
operands().size() == 2)
1604 const exprt &cand = plus_expr.
op0().
id() == ID_typecast
1608 if(cand.
id() == ID_typecast)
1612 if(typecast_op.id() == ID_address_of)
1617 typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1628 else if(expr.
id()==ID_address_of)
1632 if(
object.
id() == ID_index)
1638 else if(
object.
id() == ID_member)
1653 if(expr.
op().
id() == ID_if)
1664 if(el_size.has_value() && *el_size < 0)
1669 if(expr.
op().
id()==expr.
id())
1685 ((expr.
id() == ID_byte_extract_big_endian &&
1686 expr.
op().
id() == ID_byte_update_big_endian) ||
1687 (expr.
id() == ID_byte_extract_little_endian &&
1688 expr.
op().
id() == ID_byte_update_little_endian)) &&
1693 if(expr.
type() == op_byte_update.value().type())
1695 return op_byte_update.value();
1697 else if(el_size.has_value())
1699 const auto update_bits_opt =
1702 if(update_bits_opt.has_value() && *el_size <= *update_bits_opt)
1705 tmp.
op() = op_byte_update.value();
1714 auto offset = numeric_cast<mp_integer>(expr.
offset());
1715 if(!offset.has_value() || *offset < 0)
1719 auto const bu = expr_try_dynamic_cast<byte_update_exprt>(expr.
op());
1720 std::optional<mp_integer> update_offset;
1722 update_offset = numeric_cast<mp_integer>(bu->offset());
1723 if(bu && el_size.has_value() && update_offset.has_value())
1734 *update_offset * bu->get_bits_per_byte())
1738 tmp.
op() = bu->op();
1746 *update_offset * bu->get_bits_per_byte() + *update_size)
1750 tmp.
op() = bu->op();
1754 *offset >= *update_offset &&
1756 *update_offset * bu->get_bits_per_byte() + *update_size)
1760 tmp.
op() = bu->value();
1771 *offset == 0 && ((expr.
id() == ID_byte_extract_little_endian &&
1774 (expr.
id() == ID_byte_extract_big_endian &&
1784 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1791 (expr.
type().
id() == ID_union || expr.
type().
id() == ID_union_tag) &&
1797 (expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag) &&
1805 if(!el_size.has_value() || *el_size == 0)
1809 expr.
op().
id() == ID_array_of &&
1818 if(!const_bits_opt.has_value())
1821 std::string const_bits=const_bits_opt.value();
1823 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1829 const_bits+=const_bits;
1832 std::string el_bits = std::string(
1835 numeric_cast_v<std::size_t>(*el_size));
1838 el_bits, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1841 return std::move(*tmp);
1846 expr.
op().
id() == ID_array_of &&
1867 const bool struct_has_flexible_array_member =
has_subtype(
1869 [&](
const typet &type) {
1870 if(type.id() != ID_struct && type.id() != ID_struct_tag)
1873 const struct_typet &st = to_struct_type(ns.follow(type));
1874 const auto &comps = st.components();
1875 if(comps.empty() || comps.back().type().id() != ID_array)
1878 if(comps.back().type().get_bool(ID_C_flexible_array_member))
1882 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1883 return !size.has_value() || *size <= 1;
1886 if(!struct_has_flexible_array_member)
1888 std::string bits_cut = std::string(
1891 numeric_cast_v<std::size_t>(*el_size));
1894 bits_cut, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1897 return std::move(*tmp);
1904 if(expr.
op().
id() == ID_struct || expr.
op().
id() == ID_union)
1906 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
1914 for(
const auto &comp : components)
1920 !component_bits.has_value() || *component_bits == 0 ||
1927 auto member_offset_opt =
1930 if(!member_offset_opt.has_value())
1939 member_offset_opt.value(), expr.
offset().
type())});
1942 tmp.
type() = comp.type();
1943 tmp.offset() = new_offset;
1951 else if(expr.
type().
id() == ID_union || expr.
type().
id() == ID_union_tag)
1955 if(widest_member_opt.has_value())
1958 be.
type() = widest_member_opt->first.type();
1959 return union_exprt{widest_member_opt->first.get_name(),
1965 else if(expr.
op().
id() == ID_array)
1968 const auto &element_bit_width =
1970 if(element_bit_width.has_value() && *element_bit_width > 0)
1976 const auto elements_to_erase = numeric_cast_v<std::size_t>(
1979 slice.operands().erase(
1980 slice.operands().begin(),
1981 slice.operands().begin() +
1982 std::min(elements_to_erase,
slice.operands().size()));
1983 slice.type().size() =
1990 else if(*offset == 0 && *el_size % *element_bit_width == 0)
1992 const auto elements_to_keep =
1993 numeric_cast_v<std::size_t>(*el_size / *element_bit_width);
1995 if(
slice.operands().size() > elements_to_keep)
1997 slice.operands().resize(elements_to_keep);
1998 slice.type().size() =
2011 if(subexpr.has_value() && subexpr.value() != expr)
2024 if(expr.
op().
id() == ID_if)
2031 std::optional<exprt::operandst> new_operands;
2033 for(std::size_t i = 0; i < expr.
operands().size(); ++i)
2036 if(r_it.has_changed())
2038 if(!new_operands.has_value())
2040 (*new_operands)[i] = std::move(r_it.expr);
2044 if(new_operands.has_value())
2046 exprt result = expr;
2047 std::swap(result.
operands(), *new_operands);
2061 expr.
id() == expr.
op().
id() &&
2067 return std::move(tmp);
2070 const exprt &root = expr.
op();
2076 const auto matching_byte_extract_id =
2077 expr.
id() == ID_byte_update_little_endian ? ID_byte_extract_little_endian
2078 : ID_byte_extract_big_endian;
2082 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
2083 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
2086 matching_byte_extract_id,
2096 const auto offset_int = numeric_cast<mp_integer>(offset);
2098 root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
2099 *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
2103 expr2bits(root, expr.
id() == ID_byte_update_little_endian,
ns);
2105 if(root_bits.has_value())
2107 const auto val_bits =
2108 expr2bits(value, expr.
id() == ID_byte_update_little_endian,
ns);
2110 if(val_bits.has_value())
2114 numeric_cast_v<std::size_t>(*val_size),
2120 expr.
id() == ID_byte_update_little_endian,
2124 return std::move(*tmp);
2137 if(value.
id()==ID_with)
2141 if(with.
old().
id() == matching_byte_extract_id)
2148 if(!(root==extract.
op()))
2150 if(!(offset==extract.
offset()))
2154 if(tp.
id()==ID_struct)
2161 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
2176 tmp.set_value(std::move(new_value));
2181 else if(tp.
id()==ID_array)
2187 exprt index_offset =
2201 tmp.set_value(std::move(new_value));
2209 if(!offset_int.has_value() || *offset_int < 0)
2215 if(!val_size.has_value() || *val_size == 0)
2220 if(op_type.
id()==ID_struct)
2239 if(!m_offset.has_value())
2247 !m_size_bits.has_value() || *m_size_bits == 0 ||
2257 if(*m_offset + m_size_bytes <= *offset_int)
2261 update_size.has_value() && *update_size > 0 &&
2262 *m_offset >= *offset_int + *update_size)
2270 exprt member_name(ID_member_name);
2271 member_name.
set(ID_component_name,
component.get_name());
2276 *m_offset < *offset_int ||
2277 (*m_offset == *offset_int && update_size.has_value() &&
2278 *update_size > 0 && m_size_bytes > *update_size))
2290 update_size.has_value() && *update_size > 0 &&
2291 *m_offset + m_size_bytes > *offset_int + *update_size)
2300 matching_byte_extract_id,
2316 if(root.
id()==ID_array)
2322 !el_size.has_value() || *el_size == 0 ||
2341 bytes_req-=val_offset;
2346 matching_byte_extract_id,
2365 val_offset+=bytes_req;
2368 m_offset_bits += *el_size;
2371 return std::move(result);
2380 if(expr.
id() == ID_complex_real)
2384 if(complex_real_expr.op().id() == ID_complex)
2387 else if(expr.
id() == ID_complex_imag)
2391 if(complex_imag_expr.op().id() == ID_complex)
2425 op_type_id == ID_integer || op_type_id == ID_rational ||
2426 op_type_id == ID_real)
2435 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2441 const auto op0_value = numeric_cast<mp_integer>(expr.
op0());
2442 const auto op1_value = numeric_cast<mp_integer>(expr.
op1());
2443 if(!op0_value.has_value() || !op1_value.has_value())
2448 no_overflow_result = *op0_value + *op1_value;
2450 no_overflow_result = *op0_value - *op1_value;
2452 no_overflow_result = *op0_value * *op1_value;
2454 no_overflow_result = *op0_value << *op1_value;
2461 no_overflow_result < bv_type.smallest() ||
2462 no_overflow_result > bv_type.largest())
2480 op_type_id == ID_integer || op_type_id == ID_rational ||
2481 op_type_id == ID_real)
2486 if(op_type_id == ID_natural)
2490 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2496 const auto op_value = numeric_cast<mp_integer>(expr.
op());
2497 if(!op_value.has_value())
2502 no_overflow_result = -*op_value;
2509 no_overflow_result < bv_type.smallest() ||
2510 no_overflow_result > bv_type.largest())
2521 if(expr.
id() == ID_overflow_result_unary_minus)
2530 op_type_id == ID_integer || op_type_id == ID_rational ||
2531 op_type_id == ID_real)
2538 if(op_type_id == ID_natural)
2542 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2548 const auto op_value = numeric_cast<mp_integer>(expr.
op0());
2549 if(!op_value.has_value())
2557 no_overflow_result < bv_type.smallest() ||
2558 no_overflow_result > bv_type.largest())
2578 expr.
id() == ID_overflow_result_plus ||
2579 expr.
id() == ID_overflow_result_shl)
2583 else if(expr.
id() == ID_overflow_result_mult)
2592 expr.
id() == ID_overflow_result_plus ||
2593 expr.
id() == ID_overflow_result_minus ||
2594 expr.
id() == ID_overflow_result_shl)
2607 expr.
id() == ID_overflow_result_mult &&
2617 expr.
id() != ID_overflow_result_shl &&
2626 expr.
id() != ID_overflow_result_shl &&
2627 (op_type_id == ID_integer || op_type_id == ID_rational ||
2628 op_type_id == ID_real))
2631 expr.
id() == ID_overflow_result_plus
2633 : expr.
id() == ID_overflow_result_minus ? ID_minus : ID_mult;
2641 (expr.
id() == ID_overflow_result_plus ||
2642 expr.
id() == ID_overflow_result_mult) &&
2643 op_type_id == ID_natural)
2648 expr.
id() == ID_overflow_result_plus ? ID_plus : ID_mult,
2655 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2659 if(expr.
id() == ID_overflow_result_minus)
2664 if(
auto sum = expr_try_dynamic_cast<plus_exprt>(tc_op0))
2668 std::optional<exprt> offset;
2669 if(sum->type().id() == ID_pointer)
2674 if(offset->id() == ID_pointer_offset)
2684 offset_op.
type().
id() != ID_signedbv &&
2685 offset_op.
type().
id() != ID_unsignedbv)
2690 const std::size_t width =
2714 std::optional<typet> c_sizeof_type;
2715 for(
const auto &op : expr.
operands())
2717 const typet &sizeof_type =
2718 static_cast<const typet &
>(op.find(ID_C_c_sizeof_type));
2721 c_sizeof_type = sizeof_type;
2726 const auto op0_value = numeric_cast<mp_integer>(expr.
op0());
2727 const auto op1_value = numeric_cast<mp_integer>(expr.
op1());
2728 if(!op0_value.has_value() || !op1_value.has_value())
2732 if(expr.
id() == ID_overflow_result_plus)
2733 no_overflow_result = *op0_value + *op1_value;
2734 else if(expr.
id() == ID_overflow_result_minus)
2735 no_overflow_result = *op0_value - *op1_value;
2736 else if(expr.
id() == ID_overflow_result_mult)
2737 no_overflow_result = *op0_value * *op1_value;
2738 else if(expr.
id() == ID_overflow_result_shl)
2739 no_overflow_result = *op0_value << *op1_value;
2743 exprt no_overflow_result_expr =
2745 if(c_sizeof_type.has_value())
2746 no_overflow_result_expr.
set(ID_C_c_sizeof_type, *c_sizeof_type);
2751 no_overflow_result < bv_type.smallest() ||
2752 no_overflow_result > bv_type.largest())
2755 {std::move(no_overflow_result_expr),
true_exprt{}}, expr.
type()};
2772 if(expr.
id()==ID_address_of)
2776 else if(expr.
id()==ID_if)
2780 else if(expr.
id() == ID_typecast)
2785 expr.
id() == ID_byte_extract_little_endian ||
2786 expr.
id() == ID_byte_extract_big_endian)
2790 else if(expr.
id() == ID_dereference)
2794 else if(expr.
id() == ID_index)
2798 else if(expr.
id() == ID_member)
2803 expr.
id() == ID_is_dynamic_object || expr.
id() == ID_is_invalid_pointer ||
2804 expr.
id() == ID_object_size || expr.
id() == ID_pointer_object ||
2805 expr.
id() == ID_pointer_offset)
2811 std::optional<exprt::operandst> new_operands;
2813 for(std::size_t i = 0; i < expr.
operands().size(); ++i)
2816 if(r_it.has_changed())
2818 if(!new_operands.has_value())
2820 (*new_operands)[i] = std::move(r_it.expr);
2824 if(new_operands.has_value())
2826 std::swap(result.expr.operands(), *new_operands);
2831 if(
as_const(result.expr).type().id() == ID_array)
2861 if(expr.
id()==ID_typecast)
2865 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2866 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2867 expr.
id()==ID_ge || expr.
id()==ID_le)
2871 else if(expr.
id()==ID_if)
2875 else if(expr.
id()==ID_lambda)
2879 else if(expr.
id()==ID_with)
2883 else if(expr.
id()==ID_update)
2887 else if(expr.
id()==ID_index)
2891 else if(expr.
id()==ID_member)
2895 else if(expr.
id()==ID_byte_update_little_endian ||
2896 expr.
id()==ID_byte_update_big_endian)
2900 else if(expr.
id()==ID_byte_extract_little_endian ||
2901 expr.
id()==ID_byte_extract_big_endian)
2905 else if(expr.
id()==ID_pointer_object)
2909 else if(expr.
id() == ID_is_dynamic_object)
2913 else if(expr.
id() == ID_is_invalid_pointer)
2918 const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
2922 else if(expr.
id()==ID_div)
2926 else if(expr.
id()==ID_mod)
2930 else if(expr.
id()==ID_bitnot)
2934 else if(expr.
id()==ID_bitand ||
2935 expr.
id()==ID_bitor ||
2936 expr.
id()==ID_bitxor)
2940 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2944 else if(expr.
id()==ID_power)
2948 else if(expr.
id()==ID_plus)
2952 else if(expr.
id()==ID_minus)
2956 else if(expr.
id()==ID_mult)
2960 else if(expr.
id()==ID_floatbv_plus ||
2961 expr.
id()==ID_floatbv_minus ||
2962 expr.
id()==ID_floatbv_mult ||
2963 expr.
id()==ID_floatbv_div)
2967 else if(expr.
id()==ID_floatbv_typecast)
2971 else if(expr.
id()==ID_unary_minus)
2975 else if(expr.
id()==ID_unary_plus)
2979 else if(expr.
id()==ID_not)
2983 else if(expr.
id()==ID_implies ||
2984 expr.
id()==ID_or || expr.
id()==ID_xor ||
2989 else if(expr.
id()==ID_dereference)
2993 else if(expr.
id()==ID_address_of)
2997 else if(expr.
id()==ID_pointer_offset)
3001 else if(expr.
id()==ID_extractbit)
3005 else if(expr.
id()==ID_concatenation)
3009 else if(expr.
id()==ID_extractbits)
3013 else if(expr.
id()==ID_ieee_float_equal ||
3014 expr.
id()==ID_ieee_float_notequal)
3018 else if(expr.
id() == ID_bswap)
3022 else if(expr.
id()==ID_isinf)
3026 else if(expr.
id()==ID_isnan)
3030 else if(expr.
id()==ID_isnormal)
3034 else if(expr.
id()==ID_abs)
3038 else if(expr.
id()==ID_sign)
3042 else if(expr.
id() == ID_popcount)
3046 else if(expr.
id() == ID_count_leading_zeros)
3050 else if(expr.
id() == ID_count_trailing_zeros)
3054 else if(expr.
id() == ID_find_first_set)
3058 else if(expr.
id() == ID_function_application)
3062 else if(expr.
id() == ID_complex_real || expr.
id() == ID_complex_imag)
3067 const auto binary_overflow =
3068 expr_try_dynamic_cast<binary_overflow_exprt>(expr))
3073 const auto unary_overflow =
3074 expr_try_dynamic_cast<unary_overflow_exprt>(expr))
3079 const auto overflow_result =
3080 expr_try_dynamic_cast<overflow_result_exprt>(expr))
3084 else if(expr.
id() == ID_bitreverse)
3089 const auto prophecy_r_or_w_ok =
3090 expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(expr))
3095 const auto prophecy_pointer_in_range =
3096 expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(expr))
3101 if(!no_change_join_operands)
3107 # ifdef DEBUG_ON_DEMAND
3112 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
3113 <<
" ---> " <<
format(
r.expr) <<
'\n';
3125 std::pair<simplify_expr_cachet::containert::iterator, bool>
3126 cache_result=simplify_expr_cache.container().
3127 insert(std::pair<exprt, exprt>(expr,
exprt()));
3129 if(!cache_result.second)
3131 const exprt &new_expr=cache_result.first->second;
3144 auto simplify_node_result =
simplify_node(simplify_node_preorder_result.expr);
3147 !simplify_node_result.has_changed() &&
3148 simplify_node_preorder_result.has_changed())
3150 simplify_node_result.expr_changed =
3151 simplify_node_preorder_result.expr_changed;
3154 #ifdef USE_LOCAL_REPLACE_MAP
3155 exprt tmp = simplify_node_result.expr;
3157 replace_mapt::const_iterator it =
3158 local_replace_map.
find(simplify_node_result.expr);
3159 if(it!=local_replace_map.end())
3160 simplify_node_result =
changed(it->second);
3163 !local_replace_map.empty() &&
3164 !
replace_expr(local_replace_map, simplify_node_result.expr))
3171 if(!simplify_node_result.has_changed())
3178 (
as_const(simplify_node_result.expr).type().id() == ID_array &&
3179 expr.
type().
id() == ID_array) ||
3180 as_const(simplify_node_result.expr).type() == expr.
type(),
3181 simplify_node_result.expr.
pretty(),
3186 cache_result.first->second = simplify_node_result.expr;
3189 return simplify_node_result;
3196 #ifdef DEBUG_ON_DEMAND
3198 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
3201 #ifdef DEBUG_ON_DEMAND
3203 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
3205 if(result.has_changed())
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
API to expression classes for bitvectors.
bool can_cast_expr< mult_overflow_exprt >(const exprt &base)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool can_cast_expr< minus_overflow_exprt >(const exprt &base)
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.
bool can_cast_expr< shl_overflow_exprt >(const exprt &base)
const find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
bool can_cast_expr< plus_overflow_exprt >(const exprt &base)
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.
bool can_cast_expr< unary_minus_overflow_exprt >(const exprt &base)
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.
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Expression classes for byte-level operators.
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
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.
const typet & element_type() const
The type of the elements of the array.
const exprt & size() const
A base class for binary expressions.
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
std::size_t get_bits_per_byte() const
C enum tag type, i.e., c_enum_typet with an identifier.
const typet & underlying_type() const
Determine whether an expression is constant.
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.
Union constructor to support unions without any member (a GCC/Clang feature).
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.
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.
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
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.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
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.
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
The plus expression Associativity is not specified.
The offset (in bytes) of a pointer relative to the object.
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_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &)
Try to simplify prophecy_{r,w,rw}_ok to a constant expression.
resultt simplify_member_preorder(const member_exprt &)
resultt simplify_popcount(const popcount_exprt &)
static resultt changed(resultt<> result)
resultt simplify_dereference_preorder(const dereference_exprt &)
resultt simplify_unary_pointer_predicate_preorder(const unary_exprt &)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_if(const if_exprt &)
resultt simplify_node(const exprt &)
resultt simplify_node_preorder(const exprt &)
resultt simplify_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &)
Try to simplify prophecy_pointer_in_range to a constant expression.
resultt simplify_overflow_unary(const unary_overflow_exprt &)
Try to simplify overflow-unary-.
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_index_preorder(const index_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_pointer_object(const pointer_object_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_member(const member_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_byte_update(const byte_update_exprt &)
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_pointer_offset(const pointer_offset_exprt &)
resultt simplify_plus(const plus_exprt &)
virtual bool simplify(exprt &expr)
resultt simplify_unary_plus(const unary_plus_exprt &)
resultt simplify_overflow_result(const overflow_result_exprt &)
Try to simplify overflow_result-+, overflow_result-*, overflow_result–, overflow_result-shl,...
resultt simplify_ffs(const find_first_set_exprt &)
Try to simplify find-first-set to a constant expression.
resultt simplify_if_preorder(const if_exprt &expr)
resultt simplify_byte_extract_preorder(const byte_extract_exprt &)
resultt simplify_is_dynamic_object(const unary_exprt &)
resultt simplify_object_size(const object_size_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_typecast_preorder(const typecast_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.
Generic base class for unary expressions.
const exprt & op1() const =delete
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
std::optional< 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
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
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 pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
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 pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
exprt pointer_offset_sum(const exprt &a, const exprt &b)
exprt object_size(const exprt &pointer)
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)
std::optional< 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.
std::optional< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
std::optional< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
bool join_operands(exprt &expr)
#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_WITH_DIAGNOSTICS(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 array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_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)
const type_with_subtypet & to_type_with_subtype(const typet &type)