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 &&
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();
1721 if(offset.has_value() && *offset < 0)
1726 std::optional<mp_integer> update_offset;
1730 offset.has_value() && bu && el_size.has_value() &&
1731 update_offset.has_value())
1742 *update_offset * bu->get_bits_per_byte())
1746 tmp.
op() = bu->op();
1754 *update_offset * bu->get_bits_per_byte() + *update_size)
1758 tmp.
op() = bu->op();
1762 *offset >= *update_offset &&
1764 *update_offset * bu->get_bits_per_byte() + *update_size)
1768 tmp.
op() = bu->value();
1779 offset.has_value() && *offset == 0 &&
1780 ((expr.
id() == ID_byte_extract_little_endian &&
1781 config.ansi_c.endianness ==
1783 (expr.
id() == ID_byte_extract_big_endian &&
1784 config.ansi_c.endianness ==
1793 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1800 (expr.
type().
id() == ID_union &&
1802 (expr.
type().
id() == ID_union_tag &&
1808 (expr.
type().
id() == ID_struct &&
1810 (expr.
type().
id() == ID_struct_tag &&
1818 if(!el_size.has_value() || *el_size == 0)
1822 offset.has_value() && expr.
op().
id() == ID_array_of &&
1827 config.ansi_c.endianness ==
1831 if(!const_bits_opt.has_value())
1834 std::string const_bits=const_bits_opt.value();
1836 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1842 const_bits+=const_bits;
1845 std::string el_bits = std::string(
1851 el_bits, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1854 return std::move(*tmp);
1859 offset.has_value() && expr.
op().
id() == ID_array_of &&
1875 offset.has_value() &&
bits.has_value() &&
1880 const bool struct_has_flexible_array_member =
has_subtype(
1882 [&](
const typet &type) {
1883 if(type.id() != ID_struct && type.id() != ID_struct_tag)
1886 const struct_typet &st = type.id() == ID_struct_tag
1887 ? ns.follow_tag(to_struct_tag_type(type))
1888 : to_struct_type(type);
1889 const auto &comps = st.components();
1890 if(comps.empty() || comps.back().type().id() != ID_array)
1893 if(comps.back().type().get_bool(ID_C_flexible_array_member))
1897 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1898 return !size.has_value() || *size <= 1;
1901 if(!struct_has_flexible_array_member)
1903 std::string bits_cut = std::string(
1909 bits_cut, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1912 return std::move(*tmp);
1919 if(expr.
op().
id() == ID_struct || expr.
op().
id() == ID_union)
1921 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
1924 expr.
type().
id() == ID_struct_tag
1932 for(
const auto &comp : components)
1938 !component_bits.has_value() || *component_bits == 0 ||
1945 auto member_offset_opt =
1948 if(!member_offset_opt.has_value())
1957 member_offset_opt.value(), expr.
offset().
type())});
1960 tmp.
type() = comp.type();
1961 tmp.offset() = new_offset;
1969 else if(expr.
type().
id() == ID_union || expr.
type().
id() == ID_union_tag)
1972 expr.
type().
id() == ID_union_tag
1976 if(widest_member_opt.has_value())
1979 be.
type() = widest_member_opt->first.type();
1980 return union_exprt{widest_member_opt->first.get_name(),
1986 else if(expr.
op().
id() == ID_array)
1989 const auto &element_bit_width =
1992 offset.has_value() && element_bit_width.has_value() &&
1993 *element_bit_width > 0)
2002 slice.operands().erase(
2003 slice.operands().begin(),
2004 slice.operands().begin() +
2005 std::min(elements_to_erase,
slice.operands().size()));
2006 slice.type().size() =
2013 else if(*offset == 0 && *el_size % *element_bit_width == 0)
2015 const auto elements_to_keep =
2018 if(
slice.operands().size() > elements_to_keep)
2020 slice.operands().resize(elements_to_keep);
2021 slice.type().size() =
2034 if(subexpr.has_value() && subexpr.value() != expr)
2047 if(expr.
op().
id() == ID_if)
2054 std::optional<exprt::operandst> new_operands;
2056 for(std::size_t i = 0; i < expr.
operands().size(); ++i)
2059 if(r_it.has_changed())
2061 if(!new_operands.has_value())
2063 (*new_operands)[i] = std::move(r_it.expr);
2067 if(new_operands.has_value())
2069 exprt result = expr;
2070 std::swap(result.
operands(), *new_operands);
2084 expr.
id() == expr.
op().
id() &&
2090 return std::move(tmp);
2093 const exprt &root = expr.
op();
2099 const auto matching_byte_extract_id =
2100 expr.
id() == ID_byte_update_little_endian ? ID_byte_extract_little_endian
2101 : ID_byte_extract_big_endian;
2105 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
2106 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
2109 matching_byte_extract_id,
2121 root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
2122 *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
2126 expr2bits(root, expr.
id() == ID_byte_update_little_endian,
ns);
2128 if(root_bits.has_value())
2130 const auto val_bits =
2131 expr2bits(value, expr.
id() == ID_byte_update_little_endian,
ns);
2133 if(val_bits.has_value())
2143 expr.
id() == ID_byte_update_little_endian,
2147 return std::move(*tmp);
2160 if(value.
id()==ID_with)
2164 if(with.
old().
id() == matching_byte_extract_id)
2171 if(!(root==extract.
op()))
2173 if(!(offset==extract.
offset()))
2176 if(with.
type().
id() == ID_struct || with.
type().
id() == ID_struct_tag)
2179 with.
type().
id() == ID_struct_tag
2186 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
2201 tmp.set_value(std::move(new_value));
2206 else if(with.
type().
id() == ID_array)
2213 exprt index_offset =
2227 tmp.set_value(std::move(new_value));
2235 if(!val_size.has_value() || *val_size == 0)
2245 if(el_size.has_value() && *el_size > 0 && *val_size % *el_size == 0)
2248 offset_int.has_value() &&
2257 matching_byte_extract_id,
2261 array_type->element_type()}};
2262 mp_integer n_elements = *val_size / *el_size;
2267 from_integer(base_offset + i, array_type->index_type()),
2269 matching_byte_extract_id,
2272 i * (*el_size / expr.get_bits_per_byte()), offset.type()),
2273 expr.get_bits_per_byte(),
2274 array_type->element_type()});
2282 offset.
id() == ID_plus && offset.
operands().size() == 2 &&
2289 : offset_plus.
op1();
2292 : offset_plus.
op0();
2299 expr_at_offset_C.
id() == ID_with &&
2303 tmp.set_offset(other_factor);
2308 offset.
id() == ID_mult && offset.
operands().size() == 2 &&
2315 : offset_mult.
op1()));
2318 : offset_mult.
op0();
2326 other_factor.
type())};
2330 base_offset, array_type->index_type()),
2332 matching_byte_extract_id,
2336 array_type->element_type()}};
2337 mp_integer n_elements = *val_size / *el_size;
2343 array_type->index_type()),
2345 matching_byte_extract_id,
2350 array_type->element_type()});
2359 if(!offset_int.has_value() || *offset_int < 0)
2364 if(root.
type().
id() == ID_struct || root.
type().
id() == ID_struct_tag)
2372 root.
type().
id() == ID_struct_tag
2385 if(!m_offset.has_value())
2393 !m_size_bits.has_value() || *m_size_bits == 0 ||
2403 if(*m_offset + m_size_bytes <= *offset_int)
2407 update_size.has_value() && *update_size > 0 &&
2408 *m_offset >= *offset_int + *update_size)
2416 exprt member_name(ID_member_name);
2417 member_name.
set(ID_component_name,
component.get_name());
2422 *m_offset < *offset_int ||
2423 (*m_offset == *offset_int && update_size.has_value() &&
2424 *update_size > 0 && m_size_bytes > *update_size))
2436 update_size.has_value() && *update_size > 0 &&
2437 *m_offset + m_size_bytes > *offset_int + *update_size)
2446 matching_byte_extract_id,
2462 if(root.
id()==ID_array)
2468 !el_size.has_value() || *el_size == 0 ||
2487 bytes_req-=val_offset;
2492 matching_byte_extract_id,
2511 val_offset+=bytes_req;
2514 m_offset_bits += *el_size;
2517 return std::move(result);
2526 if(expr.
id() == ID_complex_real)
2530 if(complex_real_expr.op().id() == ID_complex)
2533 else if(expr.
id() == ID_complex_imag)
2537 if(complex_imag_expr.op().id() == ID_complex)
2571 op_type_id == ID_integer || op_type_id == ID_rational ||
2572 op_type_id == ID_real)
2581 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2589 if(!op0_value.has_value() || !op1_value.has_value())
2594 no_overflow_result = *op0_value + *op1_value;
2596 no_overflow_result = *op0_value - *op1_value;
2598 no_overflow_result = *op0_value * *op1_value;
2600 no_overflow_result = *op0_value << *op1_value;
2607 no_overflow_result < bv_type.
smallest() ||
2608 no_overflow_result > bv_type.
largest())
2626 op_type_id == ID_integer || op_type_id == ID_rational ||
2627 op_type_id == ID_real)
2632 if(op_type_id == ID_natural)
2636 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2643 if(!op_value.has_value())
2648 no_overflow_result = -*op_value;
2655 no_overflow_result < bv_type.
smallest() ||
2656 no_overflow_result > bv_type.
largest())
2667 if(expr.
id() == ID_overflow_result_unary_minus)
2676 op_type_id == ID_integer || op_type_id == ID_rational ||
2677 op_type_id == ID_real)
2684 if(op_type_id == ID_natural)
2688 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2695 if(!op_value.has_value())
2703 no_overflow_result < bv_type.
smallest() ||
2704 no_overflow_result > bv_type.
largest())
2724 expr.
id() == ID_overflow_result_plus ||
2725 expr.
id() == ID_overflow_result_shl)
2729 else if(expr.
id() == ID_overflow_result_mult)
2738 expr.
id() == ID_overflow_result_plus ||
2739 expr.
id() == ID_overflow_result_minus ||
2740 expr.
id() == ID_overflow_result_shl)
2753 expr.
id() == ID_overflow_result_mult &&
2763 expr.
id() != ID_overflow_result_shl &&
2772 expr.
id() != ID_overflow_result_shl &&
2773 (op_type_id == ID_integer || op_type_id == ID_rational ||
2774 op_type_id == ID_real))
2777 expr.
id() == ID_overflow_result_plus
2779 : expr.
id() == ID_overflow_result_minus ? ID_minus : ID_mult;
2787 (expr.
id() == ID_overflow_result_plus ||
2788 expr.
id() == ID_overflow_result_mult) &&
2789 op_type_id == ID_natural)
2794 expr.
id() == ID_overflow_result_plus ? ID_plus : ID_mult,
2801 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2805 if(expr.
id() == ID_overflow_result_minus)
2814 std::optional<exprt> offset;
2815 if(sum->type().id() == ID_pointer)
2820 if(offset->id() == ID_pointer_offset)
2830 offset_op.type().id() != ID_signedbv &&
2831 offset_op.type().id() != ID_unsignedbv)
2836 const std::size_t width =
2860 std::optional<typet> c_sizeof_type;
2861 for(
const auto &op : expr.
operands())
2863 const typet &sizeof_type =
2864 static_cast<const typet &
>(op.find(ID_C_c_sizeof_type));
2867 c_sizeof_type = sizeof_type;
2874 if(!op0_value.has_value() || !op1_value.has_value())
2878 if(expr.
id() == ID_overflow_result_plus)
2879 no_overflow_result = *op0_value + *op1_value;
2880 else if(expr.
id() == ID_overflow_result_minus)
2881 no_overflow_result = *op0_value - *op1_value;
2882 else if(expr.
id() == ID_overflow_result_mult)
2883 no_overflow_result = *op0_value * *op1_value;
2884 else if(expr.
id() == ID_overflow_result_shl)
2885 no_overflow_result = *op0_value << *op1_value;
2889 exprt no_overflow_result_expr =
2891 if(c_sizeof_type.has_value())
2892 no_overflow_result_expr.
set(ID_C_c_sizeof_type, *c_sizeof_type);
2897 no_overflow_result < bv_type.
smallest() ||
2898 no_overflow_result > bv_type.
largest())
2901 {std::move(no_overflow_result_expr),
true_exprt{}}, expr.
type()};
2918 if(expr.
id()==ID_address_of)
2922 else if(expr.
id()==ID_if)
2926 else if(expr.
id() == ID_typecast)
2931 expr.
id() == ID_byte_extract_little_endian ||
2932 expr.
id() == ID_byte_extract_big_endian)
2936 else if(expr.
id() == ID_dereference)
2940 else if(expr.
id() == ID_index)
2944 else if(expr.
id() == ID_member)
2949 expr.
id() == ID_is_dynamic_object || expr.
id() == ID_is_invalid_pointer ||
2950 expr.
id() == ID_object_size || expr.
id() == ID_pointer_object ||
2951 expr.
id() == ID_pointer_offset)
2957 std::optional<exprt::operandst> new_operands;
2959 for(std::size_t i = 0; i < expr.
operands().size(); ++i)
2962 if(r_it.has_changed())
2964 if(!new_operands.has_value())
2966 (*new_operands)[i] = std::move(r_it.expr);
2970 if(new_operands.has_value())
2972 std::swap(result.expr.operands(), *new_operands);
2977 if(
as_const(result.expr).type().id() == ID_array)
3007 if(expr.
id()==ID_typecast)
3011 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
3012 expr.
id()==ID_gt || expr.
id()==ID_lt ||
3013 expr.
id()==ID_ge || expr.
id()==ID_le)
3017 else if(expr.
id()==ID_if)
3021 else if(expr.
id()==ID_lambda)
3025 else if(expr.
id()==ID_with)
3029 else if(expr.
id()==ID_update)
3033 else if(expr.
id()==ID_index)
3037 else if(expr.
id()==ID_member)
3041 else if(expr.
id()==ID_byte_update_little_endian ||
3042 expr.
id()==ID_byte_update_big_endian)
3046 else if(expr.
id()==ID_byte_extract_little_endian ||
3047 expr.
id()==ID_byte_extract_big_endian)
3051 else if(expr.
id()==ID_pointer_object)
3055 else if(expr.
id() == ID_is_dynamic_object)
3059 else if(expr.
id() == ID_is_invalid_pointer)
3068 else if(expr.
id()==ID_div)
3072 else if(expr.
id()==ID_mod)
3076 else if(expr.
id()==ID_bitnot)
3081 expr.
id() == ID_bitand || expr.
id() == ID_bitor || expr.
id() == ID_bitxor ||
3082 expr.
id() == ID_bitxnor)
3086 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
3090 else if(expr.
id()==ID_power)
3094 else if(expr.
id()==ID_plus)
3098 else if(expr.
id()==ID_minus)
3102 else if(expr.
id()==ID_mult)
3106 else if(expr.
id()==ID_floatbv_plus ||
3107 expr.
id()==ID_floatbv_minus ||
3108 expr.
id()==ID_floatbv_mult ||
3109 expr.
id()==ID_floatbv_div)
3113 else if(expr.
id() == ID_floatbv_round_to_integral)
3118 else if(expr.
id()==ID_floatbv_typecast)
3122 else if(expr.
id()==ID_unary_minus)
3126 else if(expr.
id()==ID_unary_plus)
3130 else if(expr.
id()==ID_not)
3134 else if(expr.
id()==ID_implies ||
3135 expr.
id()==ID_or || expr.
id()==ID_xor ||
3140 else if(expr.
id()==ID_dereference)
3144 else if(expr.
id()==ID_address_of)
3148 else if(expr.
id()==ID_pointer_offset)
3152 else if(expr.
id()==ID_extractbit)
3156 else if(expr.
id()==ID_concatenation)
3160 else if(expr.
id()==ID_extractbits)
3164 else if(expr.
id() == ID_zero_extend)
3168 else if(expr.
id()==ID_ieee_float_equal ||
3169 expr.
id()==ID_ieee_float_notequal)
3173 else if(expr.
id() == ID_bswap)
3177 else if(expr.
id()==ID_isinf)
3181 else if(expr.
id()==ID_isnan)
3185 else if(expr.
id()==ID_isnormal)
3189 else if(expr.
id()==ID_abs)
3193 else if(expr.
id()==ID_sign)
3197 else if(expr.
id() == ID_popcount)
3201 else if(expr.
id() == ID_count_leading_zeros)
3205 else if(expr.
id() == ID_count_trailing_zeros)
3209 else if(expr.
id() == ID_find_first_set)
3213 else if(expr.
id() == ID_function_application)
3217 else if(expr.
id() == ID_complex_real || expr.
id() == ID_complex_imag)
3222 const auto binary_overflow =
3228 const auto unary_overflow =
3234 const auto overflow_result =
3239 else if(expr.
id() == ID_bitreverse)
3244 const auto prophecy_r_or_w_ok =
3250 const auto prophecy_pointer_in_range =
3255 else if(expr.
id() == ID_exists || expr.
id() == ID_forall)
3260 if(!no_change_join_operands)
3266# ifdef DEBUG_ON_DEMAND
3271 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
3272 <<
" ---> " <<
format(
r.expr) <<
'\n';
3284 std::pair<simplify_expr_cachet::containert::iterator, bool>
3285 cache_result=simplify_expr_cache.container().
3286 insert(std::pair<exprt, exprt>(expr,
exprt()));
3288 if(!cache_result.second)
3290 const exprt &new_expr=cache_result.first->second;
3303 auto simplify_node_result =
simplify_node(simplify_node_preorder_result.expr);
3306 !simplify_node_result.has_changed() &&
3307 simplify_node_preorder_result.has_changed())
3309 simplify_node_result.expr_changed =
3310 simplify_node_preorder_result.expr_changed;
3313#ifdef USE_LOCAL_REPLACE_MAP
3314 exprt tmp = simplify_node_result.expr;
3316 replace_mapt::const_iterator it =
3317 local_replace_map.
find(simplify_node_result.expr);
3318 if(it!=local_replace_map.end())
3319 simplify_node_result =
changed(it->second);
3322 !local_replace_map.empty() &&
3323 !
replace_expr(local_replace_map, simplify_node_result.expr))
3330 if(!simplify_node_result.has_changed())
3337 (
as_const(simplify_node_result.expr).type().id() == ID_array &&
3338 expr.
type().
id() == ID_array) ||
3339 as_const(simplify_node_result.expr).type() == expr.
type(),
3340 simplify_node_result.expr.
pretty(),
3345 cache_result.first->second = simplify_node_result.expr;
3348 return simplify_node_result;
3355#ifdef DEBUG_ON_DEMAND
3357 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
3360#ifdef DEBUG_ON_DEMAND
3362 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
3364 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.
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)