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);
1277 else if(expr_type_id == ID_fixedbv)
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 &&
1351 result.
type() = expr_type;
1368 expr.
op().
id() == ID_if && expr_type.
id() != ID_floatbv &&
1369 op_type.
id() != ID_floatbv)
1377 if(r_it.has_changed())
1380 tmp.
op() = r_it.expr;
1393 if(pointer.
type().
id()!=ID_pointer)
1396 if(pointer.
id()==ID_address_of)
1404 pointer.
id() == ID_plus && pointer.
operands().size() == 2 &&
1412 if(address_of.
object().
id()==ID_index)
1434 if(pointer.
id() == ID_if)
1442 if(r_it.has_changed())
1465 expr.
old().
type().
id() == ID_struct_tag)
1493 expr.
old().
id() == ID_vector)
1497 if(i.has_value() && *i >= 0 && *i < expr.
old().
operands().size())
1517 exprt *value_ptr=&updated_value;
1519 for(
const auto &e : designator)
1521 if(e.id()==ID_index_designator &&
1522 value_ptr->
id()==ID_array)
1529 if(*i < 0 || *i >= value_ptr->
operands().size())
1534 else if(e.id()==ID_member_designator &&
1535 value_ptr->
id()==ID_struct)
1538 e.get(ID_component_name);
1540 value_ptr->
type().
id() == ID_struct_tag
1546 value_ptr = &designator_as_struct_expr.component(component_name,
ns);
1555 return updated_value;
1560 if(expr.
id()==ID_plus)
1562 if(expr.
type().
id()==ID_pointer)
1566 if(op.type().id() == ID_pointer)
1570 else if(expr.
id()==ID_typecast)
1573 const typet &op_type = typecast_expr.op().type();
1575 if(op_type.
id()==ID_pointer)
1580 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1587 const exprt &casted_expr = typecast_expr.op();
1588 if(casted_expr.
id() == ID_plus && casted_expr.
operands().size() == 2)
1592 const exprt &cand = plus_expr.
op0().
id() == ID_typecast
1596 if(cand.
id() == ID_typecast)
1600 if(typecast_op.id() == ID_address_of)
1605 typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1616 else if(expr.
id()==ID_address_of)
1620 if(
object.
id() == ID_index)
1626 else if(
object.
id() == ID_member)
1641 if(expr.
op().
id() == ID_if)
1652 if(el_size.has_value() && *el_size < 0)
1657 if(expr.
op().
id()==expr.
id())
1673 ((expr.
id() == ID_byte_extract_big_endian &&
1674 expr.
op().
id() == ID_byte_update_big_endian) ||
1675 (expr.
id() == ID_byte_extract_little_endian &&
1676 expr.
op().
id() == ID_byte_update_little_endian)) &&
1681 if(expr.
type() == op_byte_update.value().type())
1683 return op_byte_update.value();
1685 else if(el_size.has_value())
1687 const auto update_bits_opt =
1690 if(update_bits_opt.has_value() && *el_size <= *update_bits_opt)
1693 tmp.
op() = op_byte_update.value();
1702 if(offset.has_value() && *offset < 0)
1707 std::optional<mp_integer> update_offset;
1711 offset.has_value() && bu && el_size.has_value() &&
1712 update_offset.has_value())
1723 *update_offset * bu->get_bits_per_byte())
1727 tmp.
op() = bu->op();
1735 *update_offset * bu->get_bits_per_byte() + *update_size)
1739 tmp.
op() = bu->op();
1743 *offset >= *update_offset &&
1745 *update_offset * bu->get_bits_per_byte() + *update_size)
1749 tmp.
op() = bu->value();
1760 offset.has_value() && *offset == 0 &&
1761 ((expr.
id() == ID_byte_extract_little_endian &&
1762 config.ansi_c.endianness ==
1764 (expr.
id() == ID_byte_extract_big_endian &&
1765 config.ansi_c.endianness ==
1774 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1781 (expr.
type().
id() == ID_union &&
1783 (expr.
type().
id() == ID_union_tag &&
1789 (expr.
type().
id() == ID_struct &&
1791 (expr.
type().
id() == ID_struct_tag &&
1799 if(!el_size.has_value() || *el_size == 0)
1803 offset.has_value() && expr.
op().
id() == ID_array_of &&
1808 config.ansi_c.endianness ==
1812 if(!const_bits_opt.has_value())
1815 std::string const_bits=const_bits_opt.value();
1817 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1823 const_bits+=const_bits;
1826 std::string el_bits = std::string(
1832 el_bits, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1835 return std::move(*tmp);
1840 offset.has_value() && expr.
op().
id() == ID_array_of &&
1856 offset.has_value() &&
bits.has_value() &&
1861 const bool struct_has_flexible_array_member =
has_subtype(
1863 [&](
const typet &type) {
1864 if(type.id() != ID_struct && type.id() != ID_struct_tag)
1867 const struct_typet &st = type.id() == ID_struct_tag
1868 ? ns.follow_tag(to_struct_tag_type(type))
1869 : to_struct_type(type);
1870 const auto &comps = st.components();
1871 if(comps.empty() || comps.back().type().id() != ID_array)
1874 if(comps.back().type().get_bool(ID_C_flexible_array_member))
1878 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1879 return !size.has_value() || *size <= 1;
1882 if(!struct_has_flexible_array_member)
1884 std::string bits_cut = std::string(
1890 bits_cut, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1893 return std::move(*tmp);
1900 if(expr.
op().
id() == ID_struct || expr.
op().
id() == ID_union)
1902 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
1905 expr.
type().
id() == ID_struct_tag
1913 for(
const auto &comp : components)
1919 !component_bits.has_value() || *component_bits == 0 ||
1926 auto member_offset_opt =
1929 if(!member_offset_opt.has_value())
1938 member_offset_opt.value(), expr.
offset().
type())});
1941 tmp.
type() = comp.type();
1942 tmp.offset() = new_offset;
1950 else if(expr.
type().
id() == ID_union || expr.
type().
id() == ID_union_tag)
1953 expr.
type().
id() == ID_union_tag
1957 if(widest_member_opt.has_value())
1960 be.
type() = widest_member_opt->first.type();
1961 return union_exprt{widest_member_opt->first.get_name(),
1967 else if(expr.
op().
id() == ID_array)
1970 const auto &element_bit_width =
1973 offset.has_value() && element_bit_width.has_value() &&
1974 *element_bit_width > 0)
1983 slice.operands().erase(
1984 slice.operands().begin(),
1985 slice.operands().begin() +
1986 std::min(elements_to_erase,
slice.operands().size()));
1987 slice.type().size() =
1994 else if(*offset == 0 && *el_size % *element_bit_width == 0)
1996 const auto elements_to_keep =
1999 if(
slice.operands().size() > elements_to_keep)
2001 slice.operands().resize(elements_to_keep);
2002 slice.type().size() =
2015 if(subexpr.has_value() && subexpr.value() != expr)
2028 if(expr.
op().
id() == ID_if)
2035 std::optional<exprt::operandst> new_operands;
2037 for(std::size_t i = 0; i < expr.
operands().size(); ++i)
2040 if(r_it.has_changed())
2042 if(!new_operands.has_value())
2044 (*new_operands)[i] = std::move(r_it.expr);
2048 if(new_operands.has_value())
2050 exprt result = expr;
2051 std::swap(result.
operands(), *new_operands);
2065 expr.
id() == expr.
op().
id() &&
2071 return std::move(tmp);
2074 const exprt &root = expr.
op();
2080 const auto matching_byte_extract_id =
2081 expr.
id() == ID_byte_update_little_endian ? ID_byte_extract_little_endian
2082 : ID_byte_extract_big_endian;
2086 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
2087 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
2090 matching_byte_extract_id,
2102 root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
2103 *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
2107 expr2bits(root, expr.
id() == ID_byte_update_little_endian,
ns);
2109 if(root_bits.has_value())
2111 const auto val_bits =
2112 expr2bits(value, expr.
id() == ID_byte_update_little_endian,
ns);
2114 if(val_bits.has_value())
2124 expr.
id() == ID_byte_update_little_endian,
2128 return std::move(*tmp);
2141 if(value.
id()==ID_with)
2145 if(with.
old().
id() == matching_byte_extract_id)
2152 if(!(root==extract.
op()))
2154 if(!(offset==extract.
offset()))
2157 if(with.
type().
id() == ID_struct || with.
type().
id() == ID_struct_tag)
2160 with.
type().
id() == ID_struct_tag
2167 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
2182 tmp.set_value(std::move(new_value));
2187 else if(with.
type().
id() == ID_array)
2194 exprt index_offset =
2208 tmp.set_value(std::move(new_value));
2216 if(!val_size.has_value() || *val_size == 0)
2226 if(el_size.has_value() && *el_size > 0 && *val_size % *el_size == 0)
2229 offset_int.has_value() &&
2238 matching_byte_extract_id,
2242 array_type->element_type()}};
2243 mp_integer n_elements = *val_size / *el_size;
2249 from_integer(base_offset + i, array_type->index_type()),
2251 matching_byte_extract_id,
2256 array_type->element_type()}};
2264 offset.
id() == ID_plus && offset.
operands().size() == 2 &&
2271 : offset_plus.
op1();
2274 : offset_plus.
op0();
2281 expr_at_offset_C.
id() == ID_with &&
2285 tmp.set_offset(other_factor);
2290 offset.
id() == ID_mult && offset.
operands().size() == 2 &&
2297 : offset_mult.
op1()));
2300 : offset_mult.
op0();
2308 other_factor.
type())};
2312 base_offset, array_type->index_type()),
2314 matching_byte_extract_id,
2318 array_type->element_type()}};
2319 mp_integer n_elements = *val_size / *el_size;
2326 array_type->index_type()),
2328 matching_byte_extract_id,
2333 array_type->element_type()}};
2342 if(!offset_int.has_value() || *offset_int < 0)
2347 if(root.
type().
id() == ID_struct || root.
type().
id() == ID_struct_tag)
2355 root.
type().
id() == ID_struct_tag
2368 if(!m_offset.has_value())
2376 !m_size_bits.has_value() || *m_size_bits == 0 ||
2386 if(*m_offset + m_size_bytes <= *offset_int)
2390 update_size.has_value() && *update_size > 0 &&
2391 *m_offset >= *offset_int + *update_size)
2399 exprt member_name(ID_member_name);
2400 member_name.
set(ID_component_name,
component.get_name());
2405 *m_offset < *offset_int ||
2406 (*m_offset == *offset_int && update_size.has_value() &&
2407 *update_size > 0 && m_size_bytes > *update_size))
2419 update_size.has_value() && *update_size > 0 &&
2420 *m_offset + m_size_bytes > *offset_int + *update_size)
2429 matching_byte_extract_id,
2445 if(root.
id()==ID_array)
2451 !el_size.has_value() || *el_size == 0 ||
2470 bytes_req-=val_offset;
2475 matching_byte_extract_id,
2494 val_offset+=bytes_req;
2497 m_offset_bits += *el_size;
2500 return std::move(result);
2509 if(expr.
id() == ID_complex_real)
2513 if(complex_real_expr.op().id() == ID_complex)
2516 else if(expr.
id() == ID_complex_imag)
2520 if(complex_imag_expr.op().id() == ID_complex)
2554 op_type_id == ID_integer || op_type_id == ID_rational ||
2555 op_type_id == ID_real)
2564 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2572 if(!op0_value.has_value() || !op1_value.has_value())
2577 no_overflow_result = *op0_value + *op1_value;
2579 no_overflow_result = *op0_value - *op1_value;
2581 no_overflow_result = *op0_value * *op1_value;
2583 no_overflow_result = *op0_value << *op1_value;
2590 no_overflow_result < bv_type.
smallest() ||
2591 no_overflow_result > bv_type.
largest())
2609 op_type_id == ID_integer || op_type_id == ID_rational ||
2610 op_type_id == ID_real)
2615 if(op_type_id == ID_natural)
2619 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2626 if(!op_value.has_value())
2631 no_overflow_result = -*op_value;
2638 no_overflow_result < bv_type.
smallest() ||
2639 no_overflow_result > bv_type.
largest())
2650 if(expr.
id() == ID_overflow_result_unary_minus)
2659 op_type_id == ID_integer || op_type_id == ID_rational ||
2660 op_type_id == ID_real)
2667 if(op_type_id == ID_natural)
2671 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2678 if(!op_value.has_value())
2686 no_overflow_result < bv_type.
smallest() ||
2687 no_overflow_result > bv_type.
largest())
2707 expr.
id() == ID_overflow_result_plus ||
2708 expr.
id() == ID_overflow_result_shl)
2712 else if(expr.
id() == ID_overflow_result_mult)
2721 expr.
id() == ID_overflow_result_plus ||
2722 expr.
id() == ID_overflow_result_minus ||
2723 expr.
id() == ID_overflow_result_shl)
2736 expr.
id() == ID_overflow_result_mult &&
2746 expr.
id() != ID_overflow_result_shl &&
2755 expr.
id() != ID_overflow_result_shl &&
2756 (op_type_id == ID_integer || op_type_id == ID_rational ||
2757 op_type_id == ID_real))
2760 expr.
id() == ID_overflow_result_plus
2762 : expr.
id() == ID_overflow_result_minus ? ID_minus : ID_mult;
2770 (expr.
id() == ID_overflow_result_plus ||
2771 expr.
id() == ID_overflow_result_mult) &&
2772 op_type_id == ID_natural)
2777 expr.
id() == ID_overflow_result_plus ? ID_plus : ID_mult,
2784 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2788 if(expr.
id() == ID_overflow_result_minus)
2797 std::optional<exprt> offset;
2798 if(sum->type().id() == ID_pointer)
2803 if(offset->id() == ID_pointer_offset)
2813 offset_op.type().id() != ID_signedbv &&
2814 offset_op.type().id() != ID_unsignedbv)
2819 const std::size_t width =
2843 std::optional<typet> c_sizeof_type;
2844 for(
const auto &op : expr.
operands())
2846 const typet &sizeof_type =
2847 static_cast<const typet &
>(op.find(ID_C_c_sizeof_type));
2850 c_sizeof_type = sizeof_type;
2857 if(!op0_value.has_value() || !op1_value.has_value())
2861 if(expr.
id() == ID_overflow_result_plus)
2862 no_overflow_result = *op0_value + *op1_value;
2863 else if(expr.
id() == ID_overflow_result_minus)
2864 no_overflow_result = *op0_value - *op1_value;
2865 else if(expr.
id() == ID_overflow_result_mult)
2866 no_overflow_result = *op0_value * *op1_value;
2867 else if(expr.
id() == ID_overflow_result_shl)
2868 no_overflow_result = *op0_value << *op1_value;
2872 exprt no_overflow_result_expr =
2874 if(c_sizeof_type.has_value())
2875 no_overflow_result_expr.
set(ID_C_c_sizeof_type, *c_sizeof_type);
2880 no_overflow_result < bv_type.
smallest() ||
2881 no_overflow_result > bv_type.
largest())
2884 {std::move(no_overflow_result_expr),
true_exprt{}}, expr.
type()};
2901 if(expr.
id()==ID_address_of)
2905 else if(expr.
id()==ID_if)
2909 else if(expr.
id() == ID_typecast)
2914 expr.
id() == ID_byte_extract_little_endian ||
2915 expr.
id() == ID_byte_extract_big_endian)
2919 else if(expr.
id() == ID_dereference)
2923 else if(expr.
id() == ID_index)
2927 else if(expr.
id() == ID_member)
2932 expr.
id() == ID_is_dynamic_object || expr.
id() == ID_is_invalid_pointer ||
2933 expr.
id() == ID_object_size || expr.
id() == ID_pointer_object ||
2934 expr.
id() == ID_pointer_offset)
2940 std::optional<exprt::operandst> new_operands;
2942 for(std::size_t i = 0; i < expr.
operands().size(); ++i)
2945 if(r_it.has_changed())
2947 if(!new_operands.has_value())
2949 (*new_operands)[i] = std::move(r_it.expr);
2953 if(new_operands.has_value())
2955 std::swap(result.expr.operands(), *new_operands);
2960 if(
as_const(result.expr).type().id() == ID_array)
2990 if(expr.
id()==ID_typecast)
2994 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2995 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2996 expr.
id()==ID_ge || expr.
id()==ID_le)
3000 else if(expr.
id()==ID_if)
3004 else if(expr.
id()==ID_lambda)
3008 else if(expr.
id()==ID_with)
3012 else if(expr.
id()==ID_update)
3016 else if(expr.
id()==ID_index)
3020 else if(expr.
id()==ID_member)
3024 else if(expr.
id()==ID_byte_update_little_endian ||
3025 expr.
id()==ID_byte_update_big_endian)
3029 else if(expr.
id()==ID_byte_extract_little_endian ||
3030 expr.
id()==ID_byte_extract_big_endian)
3034 else if(expr.
id()==ID_pointer_object)
3038 else if(expr.
id() == ID_is_dynamic_object)
3042 else if(expr.
id() == ID_is_invalid_pointer)
3051 else if(expr.
id()==ID_div)
3055 else if(expr.
id()==ID_mod)
3059 else if(expr.
id()==ID_bitnot)
3064 expr.
id() == ID_bitand || expr.
id() == ID_bitor || expr.
id() == ID_bitxor ||
3065 expr.
id() == ID_bitxnor)
3069 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
3073 else if(expr.
id()==ID_power)
3077 else if(expr.
id()==ID_plus)
3081 else if(expr.
id()==ID_minus)
3085 else if(expr.
id()==ID_mult)
3089 else if(expr.
id()==ID_floatbv_plus ||
3090 expr.
id()==ID_floatbv_minus ||
3091 expr.
id()==ID_floatbv_mult ||
3092 expr.
id()==ID_floatbv_div)
3096 else if(expr.
id() == ID_floatbv_round_to_integral)
3101 else if(expr.
id()==ID_floatbv_typecast)
3105 else if(expr.
id()==ID_unary_minus)
3109 else if(expr.
id()==ID_unary_plus)
3113 else if(expr.
id()==ID_not)
3117 else if(expr.
id()==ID_implies ||
3118 expr.
id()==ID_or || expr.
id()==ID_xor ||
3123 else if(expr.
id()==ID_dereference)
3127 else if(expr.
id()==ID_address_of)
3131 else if(expr.
id()==ID_pointer_offset)
3135 else if(expr.
id()==ID_extractbit)
3139 else if(expr.
id()==ID_concatenation)
3143 else if(expr.
id()==ID_extractbits)
3147 else if(expr.
id() == ID_zero_extend)
3151 else if(expr.
id()==ID_ieee_float_equal ||
3152 expr.
id()==ID_ieee_float_notequal)
3156 else if(expr.
id() == ID_bswap)
3160 else if(expr.
id()==ID_isinf)
3164 else if(expr.
id()==ID_isnan)
3168 else if(expr.
id()==ID_isnormal)
3172 else if(expr.
id()==ID_abs)
3176 else if(expr.
id()==ID_sign)
3180 else if(expr.
id() == ID_popcount)
3184 else if(expr.
id() == ID_count_leading_zeros)
3188 else if(expr.
id() == ID_count_trailing_zeros)
3192 else if(expr.
id() == ID_find_first_set)
3196 else if(expr.
id() == ID_function_application)
3200 else if(expr.
id() == ID_complex_real || expr.
id() == ID_complex_imag)
3205 const auto binary_overflow =
3211 const auto unary_overflow =
3217 const auto overflow_result =
3222 else if(expr.
id() == ID_bitreverse)
3227 const auto prophecy_r_or_w_ok =
3233 const auto prophecy_pointer_in_range =
3238 else if(expr.
id() == ID_exists || expr.
id() == ID_forall)
3243 if(!no_change_join_operands)
3249# ifdef DEBUG_ON_DEMAND
3254 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
3255 <<
" ---> " <<
format(
r.expr) <<
'\n';
3267 std::pair<simplify_expr_cachet::containert::iterator, bool>
3268 cache_result=simplify_expr_cache.container().
3269 insert(std::pair<exprt, exprt>(expr,
exprt()));
3271 if(!cache_result.second)
3273 const exprt &new_expr=cache_result.first->second;
3286 auto simplify_node_result =
simplify_node(simplify_node_preorder_result.expr);
3289 !simplify_node_result.has_changed() &&
3290 simplify_node_preorder_result.has_changed())
3292 simplify_node_result.expr_changed =
3293 simplify_node_preorder_result.expr_changed;
3296#ifdef USE_LOCAL_REPLACE_MAP
3297 exprt tmp = simplify_node_result.expr;
3299 replace_mapt::const_iterator it =
3300 local_replace_map.
find(simplify_node_result.expr);
3301 if(it!=local_replace_map.end())
3302 simplify_node_result =
changed(it->second);
3305 !local_replace_map.empty() &&
3306 !
replace_expr(local_replace_map, simplify_node_result.expr))
3313 if(!simplify_node_result.has_changed())
3320 (
as_const(simplify_node_result.expr).type().id() == ID_array &&
3321 expr.
type().
id() == ID_array) ||
3322 as_const(simplify_node_result.expr).type() == expr.
type(),
3323 simplify_node_result.expr.
pretty(),
3328 cache_result.first->second = simplify_node_result.expr;
3331 return simplify_node_result;
3338#ifdef DEBUG_ON_DEMAND
3340 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
3343#ifdef DEBUG_ON_DEMAND
3345 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
3347 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)
const mp_integer & get_value() const
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.
mp_integer largest() const
Return the largest value that can be represented using this type.
mp_integer smallest() const
Return the smallest value that can be represented using this type.
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_quantifier_expr(const quantifier_exprt &)
Try to simplify exists/forall to a constant expression.
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 &)
virtual 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 &)
virtual 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 type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet 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 quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
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.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
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)