44struct simplify_expr_cachet
48 typedef std::unordered_map<
49 exprt, exprt, irep_full_hash, irep_full_eq> containert;
51 typedef std::unordered_map<exprt, exprt, irep_hash> containert;
54 containert container_normal;
56 containert &container()
58 return container_normal;
62simplify_expr_cachet simplify_expr_cache;
71 if(type.
id()==ID_floatbv)
77 else if(type.
id()==ID_signedbv ||
78 type.
id()==ID_unsignedbv)
105 if(type.
id()==ID_floatbv)
110 else if(type.
id()==ID_signedbv ||
111 type.
id()==ID_unsignedbv)
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())
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())
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())
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)
573 if(isalpha(character))
575 if(isupper(character))
577 from_integer(tolower(character), constant_value.type());
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) &&
776 config.ansi_c.NULL_is_zero)
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)}));
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;
898 config.ansi_c.NULL_is_zero &&
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))
954 op_id == ID_plus || op_id == ID_minus || op_id == ID_mult ||
955 op_id == ID_unary_minus || op_id == ID_bitxor || op_id == ID_bitxnor ||
956 op_id == ID_bitor || op_id == ID_bitand)
975 else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
985 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
986 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus)
991 if(step.has_value() && *step != 0)
994 auto new_expr = expr;
996 new_expr.
op().
type() = size_t_type;
998 for(
auto &op : new_expr.op().operands())
1001 if(op.type().id() != ID_pointer && *step > 1)
1006 op = std::move(new_op);
1016 const exprt &operand = expr.
op();
1024 typet c_sizeof_type=
1025 static_cast<const typet &
>(operand.
find(ID_C_c_sizeof_type));
1027 if(op_type_id==ID_integer ||
1028 op_type_id==ID_natural)
1034 if(expr_type_id==ID_bool)
1039 if(expr_type_id==ID_unsignedbv ||
1040 expr_type_id==ID_signedbv ||
1041 expr_type_id==ID_c_enum ||
1042 expr_type_id==ID_c_bit_field ||
1043 expr_type_id==ID_integer)
1047 else if(expr_type_id == ID_c_enum_tag)
1050 if(!c_enum_type.is_incomplete())
1053 tmp.
type() = expr_type;
1054 return std::move(tmp);
1058 else if(op_type_id==ID_rational)
1061 else if(op_type_id==ID_real)
1064 else if(op_type_id==ID_bool)
1066 if(expr_type_id==ID_unsignedbv ||
1067 expr_type_id==ID_signedbv ||
1068 expr_type_id==ID_integer ||
1069 expr_type_id==ID_natural ||
1070 expr_type_id==ID_rational ||
1071 expr_type_id==ID_c_bool ||
1072 expr_type_id==ID_c_enum ||
1073 expr_type_id==ID_c_bit_field)
1084 else if(expr_type_id==ID_c_enum_tag)
1087 if(!c_enum_type.is_incomplete())
1089 unsigned int_value = operand.
is_true() ? 1u : 0u;
1091 tmp.
type()=expr_type;
1092 return std::move(tmp);
1095 else if(expr_type_id==ID_pointer &&
1097 config.ansi_c.NULL_is_zero)
1102 else if(op_type_id==ID_unsignedbv ||
1103 op_type_id==ID_signedbv ||
1104 op_type_id==ID_c_bit_field ||
1105 op_type_id==ID_c_bool)
1112 if(expr_type_id==ID_bool)
1117 if(expr_type_id==ID_c_bool)
1122 if(expr_type_id==ID_integer)
1127 if(expr_type_id==ID_natural)
1135 if(expr_type_id==ID_unsignedbv ||
1136 expr_type_id==ID_signedbv ||
1137 expr_type_id==ID_bv ||
1138 expr_type_id==ID_c_bit_field)
1143 result.set(ID_C_c_sizeof_type, c_sizeof_type);
1145 return std::move(result);
1148 if(expr_type_id==ID_c_enum_tag)
1151 if(!c_enum_type.is_incomplete())
1154 tmp.
type()=expr_type;
1155 return std::move(tmp);
1159 if(expr_type_id==ID_c_enum)
1164 if(expr_type_id==ID_fixedbv)
1176 if(expr_type_id==ID_floatbv)
1189 if(expr_type_id==ID_rational)
1195 else if(op_type_id==ID_fixedbv)
1197 if(expr_type_id==ID_unsignedbv ||
1198 expr_type_id==ID_signedbv)
1204 else if(expr_type_id==ID_fixedbv)
1211 else if(expr_type_id == ID_bv)
1217 else if(op_type_id==ID_floatbv)
1223 if(expr_type_id==ID_unsignedbv ||
1224 expr_type_id==ID_signedbv)
1229 else if(expr_type_id==ID_floatbv)
1235 else if(expr_type_id==ID_fixedbv)
1245 else if(expr_type_id == ID_bv)
1250 else if(op_type_id==ID_bv)
1253 expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1254 expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1255 expr_type_id == ID_c_bit_field)
1259 if(expr_type_id != ID_c_enum_tag)
1265 result.type() = tag_type;
1266 return std::move(result);
1269 else if(expr_type_id == ID_floatbv)
1274 ieee_float.
unpack(int_value);
1275 return ieee_float.to_expr();
1277 else if(expr_type_id == ID_fixedbv)
1283 return fixedbv.to_expr();
1286 else if(op_type_id==ID_c_enum_tag)
1288 const typet &base_type =
1290 if(base_type.
id()==ID_signedbv || base_type.
id()==ID_unsignedbv)
1293 auto new_expr = expr;
1294 new_expr.
op().
type() = base_type;
1298 else if(op_type_id==ID_c_enum)
1301 if(base_type.
id()==ID_signedbv || base_type.
id()==ID_unsignedbv)
1304 auto new_expr = expr;
1305 new_expr.
op().
type() = base_type;
1310 else if(operand.
id()==ID_typecast)
1315 op_type_id == expr_type_id &&
1316 (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1317 expr_type_id == ID_bv) &&
1321 auto new_expr = expr;
1327 else if(operand.
id()==ID_address_of)
1333 o.
type().
id() == ID_array &&
1355 expr.
op().
id() == ID_if && expr_type.
id() != ID_floatbv &&
1356 op_type.
id() != ID_floatbv)
1364 if(r_it.has_changed())
1367 tmp.
op() = r_it.expr;
1380 if(pointer.
type().
id()!=ID_pointer)
1383 if(pointer.
id()==ID_address_of)
1391 pointer.
id() == ID_plus && pointer.
operands().size() == 2 &&
1399 if(address_of.
object().
id()==ID_index)
1421 if(pointer.
id() == ID_if)
1429 if(r_it.has_changed())
1448 bool no_change =
true;
1454 auto with_expr = expr;
1459 with_expr.old().type().id() == ID_struct ||
1460 with_expr.old().type().id() == ID_struct_tag)
1462 if(with_expr.old().id() == ID_struct || with_expr.old().is_constant())
1464 while(with_expr.operands().size() > 1)
1467 with_expr.where().get(ID_component_name);
1470 with_expr.old().type().
id() == ID_struct_tag
1478 if(number >= with_expr.old().operands().size())
1481 with_expr.old().operands()[number].swap(with_expr.new_value());
1483 with_expr.operands().erase(++with_expr.operands().begin());
1484 with_expr.operands().erase(++with_expr.operands().begin());
1491 with_expr.old().type().id() == ID_array ||
1492 with_expr.old().type().id() == ID_vector)
1495 with_expr.old().id() == ID_array || with_expr.old().is_constant() ||
1496 with_expr.old().id() == ID_vector)
1498 while(with_expr.operands().size() > 1)
1505 if(*i < 0 || *i >= with_expr.old().operands().size())
1509 with_expr.new_value());
1511 with_expr.operands().erase(++with_expr.operands().begin());
1512 with_expr.operands().erase(++with_expr.operands().begin());
1519 if(with_expr.operands().size() == 1)
1520 return with_expr.
old();
1525 return std::move(with_expr);
1536 exprt *value_ptr=&updated_value;
1538 for(
const auto &e : designator)
1540 if(e.id()==ID_index_designator &&
1541 value_ptr->
id()==ID_array)
1548 if(*i < 0 || *i >= value_ptr->
operands().size())
1553 else if(e.id()==ID_member_designator &&
1554 value_ptr->
id()==ID_struct)
1557 e.get(ID_component_name);
1559 value_ptr->
type().
id() == ID_struct_tag
1565 value_ptr = &designator_as_struct_expr.component(component_name,
ns);
1574 return updated_value;
1579 if(expr.
id()==ID_plus)
1581 if(expr.
type().
id()==ID_pointer)
1585 if(op.type().id() == ID_pointer)
1589 else if(expr.
id()==ID_typecast)
1592 const typet &op_type = typecast_expr.op().type();
1594 if(op_type.
id()==ID_pointer)
1599 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1606 const exprt &casted_expr = typecast_expr.op();
1607 if(casted_expr.
id() == ID_plus && casted_expr.
operands().size() == 2)
1611 const exprt &cand = plus_expr.
op0().
id() == ID_typecast
1615 if(cand.
id() == ID_typecast)
1619 if(typecast_op.id() == ID_address_of)
1624 typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1635 else if(expr.
id()==ID_address_of)
1639 if(
object.
id() == ID_index)
1645 else if(
object.
id() == ID_member)
1660 if(expr.
op().
id() == ID_if)
1671 if(el_size.has_value() && *el_size < 0)
1676 if(expr.
op().
id()==expr.
id())
1692 ((expr.
id() == ID_byte_extract_big_endian &&
1693 expr.
op().
id() == ID_byte_update_big_endian) ||
1694 (expr.
id() == ID_byte_extract_little_endian &&
1695 expr.
op().
id() == ID_byte_update_little_endian)) &&
1700 if(expr.
type() == op_byte_update.value().type())
1702 return op_byte_update.value();
1704 else if(el_size.has_value())
1706 const auto update_bits_opt =
1709 if(update_bits_opt.has_value() && *el_size <= *update_bits_opt)
1712 tmp.
op() = op_byte_update.value();
1722 if(!offset.has_value() || *offset < 0)
1727 std::optional<mp_integer> update_offset;
1730 if(bu && el_size.has_value() && update_offset.has_value())
1741 *update_offset * bu->get_bits_per_byte())
1745 tmp.
op() = bu->op();
1753 *update_offset * bu->get_bits_per_byte() + *update_size)
1757 tmp.
op() = bu->op();
1761 *offset >= *update_offset &&
1763 *update_offset * bu->get_bits_per_byte() + *update_size)
1767 tmp.
op() = bu->value();
1778 *offset == 0 && ((expr.
id() == ID_byte_extract_little_endian &&
1779 config.ansi_c.endianness ==
1781 (expr.
id() == ID_byte_extract_big_endian &&
1782 config.ansi_c.endianness ==
1791 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1798 (expr.
type().
id() == ID_union &&
1800 (expr.
type().
id() == ID_union_tag &&
1806 (expr.
type().
id() == ID_struct &&
1808 (expr.
type().
id() == ID_struct_tag &&
1816 if(!el_size.has_value() || *el_size == 0)
1820 expr.
op().
id() == ID_array_of &&
1825 config.ansi_c.endianness ==
1829 if(!const_bits_opt.has_value())
1832 std::string const_bits=const_bits_opt.value();
1834 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1840 const_bits+=const_bits;
1843 std::string el_bits = std::string(
1849 el_bits, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1852 return std::move(*tmp);
1857 expr.
op().
id() == ID_array_of &&
1878 const bool struct_has_flexible_array_member =
has_subtype(
1880 [&](
const typet &type) {
1881 if(type.id() != ID_struct && type.id() != ID_struct_tag)
1884 const struct_typet &st = type.id() == ID_struct_tag
1885 ? ns.follow_tag(to_struct_tag_type(type))
1886 : to_struct_type(type);
1887 const auto &comps = st.components();
1888 if(comps.empty() || comps.back().type().id() != ID_array)
1891 if(comps.back().type().get_bool(ID_C_flexible_array_member))
1895 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1896 return !size.has_value() || *size <= 1;
1899 if(!struct_has_flexible_array_member)
1901 std::string bits_cut = std::string(
1907 bits_cut, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1910 return std::move(*tmp);
1917 if(expr.
op().
id() == ID_struct || expr.
op().
id() == ID_union)
1919 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
1922 expr.
type().
id() == ID_struct_tag
1930 for(
const auto &comp : components)
1936 !component_bits.has_value() || *component_bits == 0 ||
1943 auto member_offset_opt =
1946 if(!member_offset_opt.has_value())
1955 member_offset_opt.value(), expr.
offset().
type())});
1958 tmp.
type() = comp.type();
1959 tmp.offset() = new_offset;
1967 else if(expr.
type().
id() == ID_union || expr.
type().
id() == ID_union_tag)
1970 expr.
type().
id() == ID_union_tag
1974 if(widest_member_opt.has_value())
1977 be.
type() = widest_member_opt->first.type();
1978 return union_exprt{widest_member_opt->first.get_name(),
1984 else if(expr.
op().
id() == ID_array)
1987 const auto &element_bit_width =
1989 if(element_bit_width.has_value() && *element_bit_width > 0)
1998 slice.operands().erase(
1999 slice.operands().begin(),
2000 slice.operands().begin() +
2001 std::min(elements_to_erase,
slice.operands().size()));
2002 slice.type().size() =
2009 else if(*offset == 0 && *el_size % *element_bit_width == 0)
2011 const auto elements_to_keep =
2014 if(
slice.operands().size() > elements_to_keep)
2016 slice.operands().resize(elements_to_keep);
2017 slice.type().size() =
2030 if(subexpr.has_value() && subexpr.value() != expr)
2043 if(expr.
op().
id() == ID_if)
2050 std::optional<exprt::operandst> new_operands;
2052 for(std::size_t i = 0; i < expr.
operands().size(); ++i)
2055 if(r_it.has_changed())
2057 if(!new_operands.has_value())
2059 (*new_operands)[i] = std::move(r_it.expr);
2063 if(new_operands.has_value())
2065 exprt result = expr;
2066 std::swap(result.
operands(), *new_operands);
2080 expr.
id() == expr.
op().
id() &&
2086 return std::move(tmp);
2089 const exprt &root = expr.
op();
2095 const auto matching_byte_extract_id =
2096 expr.
id() == ID_byte_update_little_endian ? ID_byte_extract_little_endian
2097 : ID_byte_extract_big_endian;
2101 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
2102 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
2105 matching_byte_extract_id,
2117 root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
2118 *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
2122 expr2bits(root, expr.
id() == ID_byte_update_little_endian,
ns);
2124 if(root_bits.has_value())
2126 const auto val_bits =
2127 expr2bits(value, expr.
id() == ID_byte_update_little_endian,
ns);
2129 if(val_bits.has_value())
2139 expr.
id() == ID_byte_update_little_endian,
2143 return std::move(*tmp);
2156 if(value.
id()==ID_with)
2160 if(with.
old().
id() == matching_byte_extract_id)
2167 if(!(root==extract.
op()))
2169 if(!(offset==extract.
offset()))
2172 if(with.
type().
id() == ID_struct || with.
type().
id() == ID_struct_tag)
2175 with.
type().
id() == ID_struct_tag
2182 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
2197 tmp.set_value(std::move(new_value));
2202 else if(with.
type().
id() == ID_array)
2209 exprt index_offset =
2223 tmp.set_value(std::move(new_value));
2231 if(!offset_int.has_value() || *offset_int < 0)
2235 if(!val_size.has_value() || *val_size == 0)
2240 if(root.
type().
id() == ID_struct || root.
type().
id() == ID_struct_tag)
2248 root.
type().
id() == ID_struct_tag
2261 if(!m_offset.has_value())
2269 !m_size_bits.has_value() || *m_size_bits == 0 ||
2279 if(*m_offset + m_size_bytes <= *offset_int)
2283 update_size.has_value() && *update_size > 0 &&
2284 *m_offset >= *offset_int + *update_size)
2292 exprt member_name(ID_member_name);
2293 member_name.
set(ID_component_name,
component.get_name());
2298 *m_offset < *offset_int ||
2299 (*m_offset == *offset_int && update_size.has_value() &&
2300 *update_size > 0 && m_size_bytes > *update_size))
2312 update_size.has_value() && *update_size > 0 &&
2313 *m_offset + m_size_bytes > *offset_int + *update_size)
2322 matching_byte_extract_id,
2338 if(root.
id()==ID_array)
2344 !el_size.has_value() || *el_size == 0 ||
2363 bytes_req-=val_offset;
2368 matching_byte_extract_id,
2387 val_offset+=bytes_req;
2390 m_offset_bits += *el_size;
2393 return std::move(result);
2402 if(expr.
id() == ID_complex_real)
2406 if(complex_real_expr.op().id() == ID_complex)
2409 else if(expr.
id() == ID_complex_imag)
2413 if(complex_imag_expr.op().id() == ID_complex)
2447 op_type_id == ID_integer || op_type_id == ID_rational ||
2448 op_type_id == ID_real)
2457 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2465 if(!op0_value.has_value() || !op1_value.has_value())
2470 no_overflow_result = *op0_value + *op1_value;
2472 no_overflow_result = *op0_value - *op1_value;
2474 no_overflow_result = *op0_value * *op1_value;
2476 no_overflow_result = *op0_value << *op1_value;
2483 no_overflow_result < bv_type.smallest() ||
2484 no_overflow_result > bv_type.largest())
2502 op_type_id == ID_integer || op_type_id == ID_rational ||
2503 op_type_id == ID_real)
2508 if(op_type_id == ID_natural)
2512 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2519 if(!op_value.has_value())
2524 no_overflow_result = -*op_value;
2531 no_overflow_result < bv_type.smallest() ||
2532 no_overflow_result > bv_type.largest())
2543 if(expr.
id() == ID_overflow_result_unary_minus)
2552 op_type_id == ID_integer || op_type_id == ID_rational ||
2553 op_type_id == ID_real)
2560 if(op_type_id == ID_natural)
2564 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2571 if(!op_value.has_value())
2579 no_overflow_result < bv_type.smallest() ||
2580 no_overflow_result > bv_type.largest())
2600 expr.
id() == ID_overflow_result_plus ||
2601 expr.
id() == ID_overflow_result_shl)
2605 else if(expr.
id() == ID_overflow_result_mult)
2614 expr.
id() == ID_overflow_result_plus ||
2615 expr.
id() == ID_overflow_result_minus ||
2616 expr.
id() == ID_overflow_result_shl)
2629 expr.
id() == ID_overflow_result_mult &&
2639 expr.
id() != ID_overflow_result_shl &&
2648 expr.
id() != ID_overflow_result_shl &&
2649 (op_type_id == ID_integer || op_type_id == ID_rational ||
2650 op_type_id == ID_real))
2653 expr.
id() == ID_overflow_result_plus
2655 : expr.
id() == ID_overflow_result_minus ? ID_minus : ID_mult;
2663 (expr.
id() == ID_overflow_result_plus ||
2664 expr.
id() == ID_overflow_result_mult) &&
2665 op_type_id == ID_natural)
2670 expr.
id() == ID_overflow_result_plus ? ID_plus : ID_mult,
2677 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2681 if(expr.
id() == ID_overflow_result_minus)
2690 std::optional<exprt> offset;
2691 if(sum->type().id() == ID_pointer)
2696 if(offset->id() == ID_pointer_offset)
2706 offset_op.type().id() != ID_signedbv &&
2707 offset_op.type().id() != ID_unsignedbv)
2712 const std::size_t width =
2736 std::optional<typet> c_sizeof_type;
2737 for(
const auto &op : expr.
operands())
2739 const typet &sizeof_type =
2740 static_cast<const typet &
>(op.find(ID_C_c_sizeof_type));
2743 c_sizeof_type = sizeof_type;
2750 if(!op0_value.has_value() || !op1_value.has_value())
2754 if(expr.
id() == ID_overflow_result_plus)
2755 no_overflow_result = *op0_value + *op1_value;
2756 else if(expr.
id() == ID_overflow_result_minus)
2757 no_overflow_result = *op0_value - *op1_value;
2758 else if(expr.
id() == ID_overflow_result_mult)
2759 no_overflow_result = *op0_value * *op1_value;
2760 else if(expr.
id() == ID_overflow_result_shl)
2761 no_overflow_result = *op0_value << *op1_value;
2765 exprt no_overflow_result_expr =
2767 if(c_sizeof_type.has_value())
2768 no_overflow_result_expr.
set(ID_C_c_sizeof_type, *c_sizeof_type);
2773 no_overflow_result < bv_type.smallest() ||
2774 no_overflow_result > bv_type.largest())
2777 {std::move(no_overflow_result_expr),
true_exprt{}}, expr.
type()};
2794 if(expr.
id()==ID_address_of)
2798 else if(expr.
id()==ID_if)
2802 else if(expr.
id() == ID_typecast)
2807 expr.
id() == ID_byte_extract_little_endian ||
2808 expr.
id() == ID_byte_extract_big_endian)
2812 else if(expr.
id() == ID_dereference)
2816 else if(expr.
id() == ID_index)
2820 else if(expr.
id() == ID_member)
2825 expr.
id() == ID_is_dynamic_object || expr.
id() == ID_is_invalid_pointer ||
2826 expr.
id() == ID_object_size || expr.
id() == ID_pointer_object ||
2827 expr.
id() == ID_pointer_offset)
2833 std::optional<exprt::operandst> new_operands;
2835 for(std::size_t i = 0; i < expr.
operands().size(); ++i)
2838 if(r_it.has_changed())
2840 if(!new_operands.has_value())
2842 (*new_operands)[i] = std::move(r_it.expr);
2846 if(new_operands.has_value())
2848 std::swap(result.expr.operands(), *new_operands);
2853 if(
as_const(result.expr).type().id() == ID_array)
2883 if(expr.
id()==ID_typecast)
2887 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2888 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2889 expr.
id()==ID_ge || expr.
id()==ID_le)
2893 else if(expr.
id()==ID_if)
2897 else if(expr.
id()==ID_lambda)
2901 else if(expr.
id()==ID_with)
2905 else if(expr.
id()==ID_update)
2909 else if(expr.
id()==ID_index)
2913 else if(expr.
id()==ID_member)
2917 else if(expr.
id()==ID_byte_update_little_endian ||
2918 expr.
id()==ID_byte_update_big_endian)
2922 else if(expr.
id()==ID_byte_extract_little_endian ||
2923 expr.
id()==ID_byte_extract_big_endian)
2927 else if(expr.
id()==ID_pointer_object)
2931 else if(expr.
id() == ID_is_dynamic_object)
2935 else if(expr.
id() == ID_is_invalid_pointer)
2944 else if(expr.
id()==ID_div)
2948 else if(expr.
id()==ID_mod)
2952 else if(expr.
id()==ID_bitnot)
2957 expr.
id() == ID_bitand || expr.
id() == ID_bitor || expr.
id() == ID_bitxor ||
2958 expr.
id() == ID_bitxnor)
2962 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2966 else if(expr.
id()==ID_power)
2970 else if(expr.
id()==ID_plus)
2974 else if(expr.
id()==ID_minus)
2978 else if(expr.
id()==ID_mult)
2982 else if(expr.
id()==ID_floatbv_plus ||
2983 expr.
id()==ID_floatbv_minus ||
2984 expr.
id()==ID_floatbv_mult ||
2985 expr.
id()==ID_floatbv_div)
2989 else if(expr.
id() == ID_floatbv_round_to_integral)
2994 else if(expr.
id()==ID_floatbv_typecast)
2998 else if(expr.
id()==ID_unary_minus)
3002 else if(expr.
id()==ID_unary_plus)
3006 else if(expr.
id()==ID_not)
3010 else if(expr.
id()==ID_implies ||
3011 expr.
id()==ID_or || expr.
id()==ID_xor ||
3016 else if(expr.
id()==ID_dereference)
3020 else if(expr.
id()==ID_address_of)
3024 else if(expr.
id()==ID_pointer_offset)
3028 else if(expr.
id()==ID_extractbit)
3032 else if(expr.
id()==ID_concatenation)
3036 else if(expr.
id()==ID_extractbits)
3040 else if(expr.
id() == ID_zero_extend)
3044 else if(expr.
id()==ID_ieee_float_equal ||
3045 expr.
id()==ID_ieee_float_notequal)
3049 else if(expr.
id() == ID_bswap)
3053 else if(expr.
id()==ID_isinf)
3057 else if(expr.
id()==ID_isnan)
3061 else if(expr.
id()==ID_isnormal)
3065 else if(expr.
id()==ID_abs)
3069 else if(expr.
id()==ID_sign)
3073 else if(expr.
id() == ID_popcount)
3077 else if(expr.
id() == ID_count_leading_zeros)
3081 else if(expr.
id() == ID_count_trailing_zeros)
3085 else if(expr.
id() == ID_find_first_set)
3089 else if(expr.
id() == ID_function_application)
3093 else if(expr.
id() == ID_complex_real || expr.
id() == ID_complex_imag)
3098 const auto binary_overflow =
3104 const auto unary_overflow =
3110 const auto overflow_result =
3115 else if(expr.
id() == ID_bitreverse)
3120 const auto prophecy_r_or_w_ok =
3126 const auto prophecy_pointer_in_range =
3132 if(!no_change_join_operands)
3138# ifdef DEBUG_ON_DEMAND
3143 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
3144 <<
" ---> " <<
format(
r.expr) <<
'\n';
3156 std::pair<simplify_expr_cachet::containert::iterator, bool>
3157 cache_result=simplify_expr_cache.container().
3158 insert(std::pair<exprt, exprt>(expr,
exprt()));
3160 if(!cache_result.second)
3162 const exprt &new_expr=cache_result.first->second;
3175 auto simplify_node_result =
simplify_node(simplify_node_preorder_result.expr);
3178 !simplify_node_result.has_changed() &&
3179 simplify_node_preorder_result.has_changed())
3181 simplify_node_result.expr_changed =
3182 simplify_node_preorder_result.expr_changed;
3185#ifdef USE_LOCAL_REPLACE_MAP
3186 exprt tmp = simplify_node_result.expr;
3188 replace_mapt::const_iterator it =
3189 local_replace_map.
find(simplify_node_result.expr);
3190 if(it!=local_replace_map.end())
3191 simplify_node_result =
changed(it->second);
3194 !local_replace_map.empty() &&
3195 !
replace_expr(local_replace_map, simplify_node_result.expr))
3202 if(!simplify_node_result.has_changed())
3209 (
as_const(simplify_node_result.expr).type().id() == ID_array &&
3210 expr.
type().
id() == ID_array) ||
3211 as_const(simplify_node_result.expr).type() == expr.
type(),
3212 simplify_node_result.expr.
pretty(),
3217 cache_result.first->second = simplify_node_result.expr;
3220 return simplify_node_result;
3227#ifdef DEBUG_ON_DEMAND
3229 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
3232#ifdef DEBUG_ON_DEMAND
3234 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
3236 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.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const zero_extend_exprt & to_zero_extend_expr(const exprt &expr)
Cast an exprt to a zero_extend_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
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.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Operator to return the address of an object.
Array constructor from list of elements.
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
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 & offset() const
std::size_t get_bits_per_byte() const
const exprt & value() const
C enum tag type, i.e., c_enum_typet with an identifier.
const typet & underlying_type() const
Determine whether an expression is constant.
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.
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.
bool is_false() const
Return whether the expression is a constant representing false.
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The Boolean constant false.
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.
An IEEE 754 floating-point value, including specificiation.
void set_sign(bool _sign)
constant_exprt to_expr() const
void unpack(const mp_integer &)
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
mp_integer to_integer() const
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.
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_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_zero_extend(const zero_extend_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_power(const power_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 &)
resultt simplify_floatbv_round_to_integral(const floatbv_round_to_integral_exprt &)
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
const componentst & components() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool has_component(const irep_idt &component_name) const
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
std::vector< componentt > componentst
const irep_idt & get_identifier() const
The Boolean constant true.
const typet & subtype() const
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Generic base class for unary expressions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
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)
auto expr_checked_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
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 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_round_to_integral_exprt & to_floatbv_round_to_integral_expr(const exprt &expr)
Cast an exprt to a floatbv_round_to_integral_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 power_exprt & to_power_expr(const exprt &expr)
Cast an exprt to a power_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
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.
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< 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 > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
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)
const std::size_t sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::bits
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< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
std::optional< std::string > expr2bits(const exprt &expr, bool little_endian, 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.
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 struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const 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 div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_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)
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)