44struct simplify_expr_cachet
48 typedef std::unordered_map<
51 typedef std::unordered_map<exprt, exprt, irep_hash> containert;
54 containert container_normal;
56 containert &container()
58 return container_normal;
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) &&
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))
840 if(typecast.op().type()==expr_type)
842 return typecast.op();
848 if(expr_type.
id()==ID_c_bool &&
849 op_type.
id()!=ID_bool)
853 auto new_expr = expr;
867 return std::move(tmp);
873 expr_type.
id() == ID_pointer && expr.
op().
id() == ID_typecast &&
874 op_type.
id() == ID_pointer)
876 auto new_expr = expr;
884 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
885 expr.
op().
id() == ID_typecast && expr.
op().
operands().size() == 1 &&
886 op_type.
id() == ID_pointer)
891 auto outer_cast = expr;
900 (expr_type.
id() == ID_signedbv || expr_type.
id() == ID_unsignedbv) &&
901 op_type.
id() == ID_pointer && expr.
op().
id() == ID_plus &&
907 (op_plus_expr.op0().id() == ID_typecast &&
909 (op_plus_expr.op0().is_constant() &&
914 if(sub_size.has_value())
916 auto new_expr = expr;
921 if(*sub_size == 0 || *sub_size == 1)
922 new_expr.op() = offset_expr;
943 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
944 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv))
954 if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
955 op_id==ID_unary_minus ||
956 op_id==ID_bitxor || 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 &&
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)
1188 if(expr_type_id==ID_rational)
1194 else if(op_type_id==ID_fixedbv)
1196 if(expr_type_id==ID_unsignedbv ||
1197 expr_type_id==ID_signedbv)
1203 else if(expr_type_id==ID_fixedbv)
1210 else if(expr_type_id == ID_bv)
1216 else if(op_type_id==ID_floatbv)
1220 if(expr_type_id==ID_unsignedbv ||
1221 expr_type_id==ID_signedbv)
1226 else if(expr_type_id==ID_floatbv)
1232 else if(expr_type_id==ID_fixedbv)
1242 else if(expr_type_id == ID_bv)
1247 else if(op_type_id==ID_bv)
1250 expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1251 expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1252 expr_type_id == ID_c_bit_field)
1256 if(expr_type_id != ID_c_enum_tag)
1262 result.type() = tag_type;
1263 return std::move(result);
1266 else if(expr_type_id == ID_floatbv)
1271 ieee_float.unpack(int_value);
1272 return ieee_float.to_expr();
1274 else if(expr_type_id == ID_fixedbv)
1279 fixedbv.set_value(int_value);
1280 return fixedbv.to_expr();
1283 else if(op_type_id==ID_c_enum_tag)
1285 const typet &base_type =
1287 if(base_type.
id()==ID_signedbv || base_type.
id()==ID_unsignedbv)
1290 auto new_expr = expr;
1291 new_expr.
op().
type() = base_type;
1295 else if(op_type_id==ID_c_enum)
1298 if(base_type.
id()==ID_signedbv || base_type.
id()==ID_unsignedbv)
1301 auto new_expr = expr;
1302 new_expr.
op().
type() = base_type;
1307 else if(operand.
id()==ID_typecast)
1312 op_type_id == expr_type_id &&
1313 (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1314 expr_type_id == ID_bv) &&
1318 auto new_expr = expr;
1324 else if(operand.
id()==ID_address_of)
1330 o.
type().
id() == ID_array &&
1351 as_const(expr).op().
id() == ID_if && expr_type.
id() != ID_floatbv &&
1352 op_type.
id() != ID_floatbv)
1362 if(r_it.has_changed())
1364 expr.
op() = r_it.expr;
1377 if(pointer.
type().
id()!=ID_pointer)
1380 if(pointer.
id()==ID_if && pointer.
operands().size()==3)
1384 auto tmp_op1 = expr;
1388 auto tmp_op2 = expr;
1392 if_exprt tmp{if_expr.
cond(), tmp_op1_result, tmp_op2_result};
1397 if(pointer.
id()==ID_address_of)
1405 pointer.
id() == ID_plus && pointer.
operands().size() == 2 &&
1413 if(address_of.
object().
id()==ID_index)
1438 bool no_change =
true;
1444 auto with_expr = expr;
1446 const typet old_type_followed =
ns.
follow(with_expr.old().type());
1450 if(old_type_followed.
id() == ID_struct)
1452 if(with_expr.old().id() == ID_struct || with_expr.old().is_constant())
1454 while(with_expr.operands().size() > 1)
1457 with_expr.where().get(ID_component_name);
1459 if(!
to_struct_type(old_type_followed).has_component(component_name))
1462 std::size_t number =
1465 if(number >= with_expr.old().operands().size())
1468 with_expr.old().operands()[number].swap(with_expr.new_value());
1470 with_expr.operands().erase(++with_expr.operands().begin());
1471 with_expr.operands().erase(++with_expr.operands().begin());
1478 with_expr.old().type().id() == ID_array ||
1479 with_expr.old().type().id() == ID_vector)
1482 with_expr.old().id() == ID_array || with_expr.old().is_constant() ||
1483 with_expr.old().id() == ID_vector)
1485 while(with_expr.operands().size() > 1)
1492 if(*i < 0 || *i >= with_expr.old().operands().size())
1496 with_expr.new_value());
1498 with_expr.operands().erase(++with_expr.operands().begin());
1499 with_expr.operands().erase(++with_expr.operands().begin());
1506 if(with_expr.operands().size() == 1)
1507 return with_expr.old();
1512 return std::move(with_expr);
1523 exprt *value_ptr=&updated_value;
1525 for(
const auto &e : designator)
1529 if(e.id()==ID_index_designator &&
1530 value_ptr->
id()==ID_array)
1537 if(*i < 0 || *i >= value_ptr->
operands().size())
1542 else if(e.id()==ID_member_designator &&
1543 value_ptr->
id()==ID_struct)
1546 e.get(ID_component_name);
1552 value_ptr = &designator_as_struct_expr.component(component_name,
ns);
1561 return updated_value;
1566 if(expr.
id()==ID_plus)
1568 if(expr.
type().
id()==ID_pointer)
1572 if(op.type().id() == ID_pointer)
1576 else if(expr.
id()==ID_typecast)
1579 const typet &op_type = typecast_expr.op().type();
1581 if(op_type.
id()==ID_pointer)
1586 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1593 const exprt &casted_expr = typecast_expr.op();
1594 if(casted_expr.
id() == ID_plus && casted_expr.
operands().size() == 2)
1598 const exprt &cand = plus_expr.
op0().
id() == ID_typecast
1602 if(cand.
id() == ID_typecast)
1606 if(typecast_op.id() == ID_address_of)
1611 typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1622 else if(expr.
id()==ID_address_of)
1626 if(
object.
id() == ID_index)
1632 else if(
object.
id() == ID_member)
1647 if(expr.
op().
id()==ID_if)
1658 if(el_size.has_value() && *el_size < 0)
1663 if(expr.
op().
id()==expr.
id())
1679 ((expr.
id() == ID_byte_extract_big_endian &&
1680 expr.
op().
id() == ID_byte_update_big_endian) ||
1681 (expr.
id() == ID_byte_extract_little_endian &&
1682 expr.
op().
id() == ID_byte_update_little_endian)) &&
1687 if(expr.
type() == op_byte_update.value().type())
1689 return op_byte_update.value();
1691 else if(el_size.has_value())
1693 const auto update_bits_opt =
1696 if(update_bits_opt.has_value() && *el_size <= *update_bits_opt)
1699 tmp.
op() = op_byte_update.value();
1709 if(!offset.has_value() || *offset < 0)
1717 if(bu && el_size.has_value() && update_offset.has_value())
1728 *update_offset * bu->get_bits_per_byte())
1732 tmp.
op() = bu->op();
1740 *update_offset * bu->get_bits_per_byte() + *update_size)
1744 tmp.
op() = bu->op();
1748 *offset >= *update_offset &&
1750 *update_offset * bu->get_bits_per_byte() + *update_size)
1754 tmp.
op() = bu->value();
1765 *offset == 0 && ((expr.
id() == ID_byte_extract_little_endian &&
1768 (expr.
id() == ID_byte_extract_big_endian &&
1778 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1785 (expr.
type().
id() == ID_union || expr.
type().
id() == ID_union_tag) &&
1791 (expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag) &&
1799 if(!el_size.has_value() || *el_size == 0)
1803 expr.
op().
id() == ID_array_of &&
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 expr.
op().
id() == ID_array_of &&
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 = to_struct_type(ns.follow(type));
1868 const auto &comps = st.components();
1869 if(comps.empty() || comps.back().type().id() != ID_array)
1872 if(comps.back().type().get_bool(ID_C_flexible_array_member))
1876 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1877 return !size.has_value() || *size <= 1;
1880 if(!struct_has_flexible_array_member)
1882 std::string bits_cut = std::string(
1888 bits_cut, expr.
type(), expr.
id() == ID_byte_extract_little_endian,
ns);
1891 return std::move(*tmp);
1898 if(expr.
op().
id() == ID_struct || expr.
op().
id() == ID_union)
1900 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
1908 for(
const auto &comp : components)
1914 !component_bits.has_value() || *component_bits == 0 ||
1921 auto member_offset_opt =
1924 if(!member_offset_opt.has_value())
1933 member_offset_opt.value(), expr.
offset().
type())});
1936 tmp.
type() = comp.type();
1937 tmp.offset() = new_offset;
1945 else if(expr.
type().
id() == ID_union || expr.
type().
id() == ID_union_tag)
1949 if(widest_member_opt.has_value())
1952 be.
type() = widest_member_opt->first.type();
1953 return union_exprt{widest_member_opt->first.get_name(),
1959 else if(expr.
op().
id() == ID_array)
1962 const auto &element_bit_width =
1964 if(element_bit_width.has_value() && *element_bit_width > 0)
1973 slice.operands().erase(
1974 slice.operands().begin(),
1975 slice.operands().begin() +
1976 std::min(elements_to_erase,
slice.operands().size()));
1977 slice.type().size() =
1984 else if(*offset == 0 && *el_size % *element_bit_width == 0)
1986 const auto elements_to_keep =
1989 if(
slice.operands().size() > elements_to_keep)
1991 slice.operands().resize(elements_to_keep);
1992 slice.type().size() =
2005 if(subexpr.has_value() && subexpr.value() != expr)
2020 expr.
id() == expr.
op().
id() &&
2026 return std::move(tmp);
2029 const exprt &root = expr.
op();
2035 const auto matching_byte_extract_id =
2036 expr.
id() == ID_byte_update_little_endian ? ID_byte_extract_little_endian
2037 : ID_byte_extract_big_endian;
2041 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
2042 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
2045 matching_byte_extract_id,
2057 root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
2058 *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
2062 expr2bits(root, expr.
id() == ID_byte_update_little_endian,
ns);
2064 if(root_bits.has_value())
2066 const auto val_bits =
2067 expr2bits(value, expr.
id() == ID_byte_update_little_endian,
ns);
2069 if(val_bits.has_value())
2079 expr.
id() == ID_byte_update_little_endian,
2083 return std::move(*tmp);
2096 if(value.
id()==ID_with)
2100 if(with.
old().
id() == matching_byte_extract_id)
2107 if(!(root==extract.
op()))
2109 if(!(offset==extract.
offset()))
2113 if(tp.
id()==ID_struct)
2120 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
2135 tmp.set_value(std::move(new_value));
2140 else if(tp.
id()==ID_array)
2146 exprt index_offset =
2160 tmp.set_value(std::move(new_value));
2168 if(!offset_int.has_value() || *offset_int < 0)
2174 if(!val_size.has_value() || *val_size == 0)
2179 if(op_type.
id()==ID_struct)
2198 if(!m_offset.has_value())
2206 !m_size_bits.has_value() || *m_size_bits == 0 ||
2216 if(*m_offset + m_size_bytes <= *offset_int)
2220 update_size.has_value() && *update_size > 0 &&
2221 *m_offset >= *offset_int + *update_size)
2229 exprt member_name(ID_member_name);
2230 member_name.
set(ID_component_name,
component.get_name());
2235 *m_offset < *offset_int ||
2236 (*m_offset == *offset_int && update_size.has_value() &&
2237 *update_size > 0 && m_size_bytes > *update_size))
2249 update_size.has_value() && *update_size > 0 &&
2250 *m_offset + m_size_bytes > *offset_int + *update_size)
2259 matching_byte_extract_id,
2275 if(root.
id()==ID_array)
2281 !el_size.has_value() || *el_size == 0 ||
2300 bytes_req-=val_offset;
2305 matching_byte_extract_id,
2324 val_offset+=bytes_req;
2327 m_offset_bits += *el_size;
2330 return std::move(result);
2339 if(expr.
id() == ID_complex_real)
2343 if(complex_real_expr.op().id() == ID_complex)
2346 else if(expr.
id() == ID_complex_imag)
2350 if(complex_imag_expr.op().id() == ID_complex)
2384 op_type_id == ID_integer || op_type_id == ID_rational ||
2385 op_type_id == ID_real)
2394 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2402 if(!op0_value.has_value() || !op1_value.has_value())
2407 no_overflow_result = *op0_value + *op1_value;
2409 no_overflow_result = *op0_value - *op1_value;
2411 no_overflow_result = *op0_value * *op1_value;
2413 no_overflow_result = *op0_value << *op1_value;
2420 no_overflow_result < bv_type.smallest() ||
2421 no_overflow_result > bv_type.largest())
2439 op_type_id == ID_integer || op_type_id == ID_rational ||
2440 op_type_id == ID_real)
2445 if(op_type_id == ID_natural)
2449 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2456 if(!op_value.has_value())
2461 no_overflow_result = -*op_value;
2468 no_overflow_result < bv_type.smallest() ||
2469 no_overflow_result > bv_type.largest())
2480 if(expr.
id() == ID_overflow_result_unary_minus)
2489 op_type_id == ID_integer || op_type_id == ID_rational ||
2490 op_type_id == ID_real)
2497 if(op_type_id == ID_natural)
2501 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2508 if(!op_value.has_value())
2516 no_overflow_result < bv_type.smallest() ||
2517 no_overflow_result > bv_type.largest())
2537 expr.
id() == ID_overflow_result_plus ||
2538 expr.
id() == ID_overflow_result_shl)
2542 else if(expr.
id() == ID_overflow_result_mult)
2551 expr.
id() == ID_overflow_result_plus ||
2552 expr.
id() == ID_overflow_result_minus ||
2553 expr.
id() == ID_overflow_result_shl)
2566 expr.
id() == ID_overflow_result_mult &&
2576 expr.
id() != ID_overflow_result_shl &&
2585 expr.
id() != ID_overflow_result_shl &&
2586 (op_type_id == ID_integer || op_type_id == ID_rational ||
2587 op_type_id == ID_real))
2590 expr.
id() == ID_overflow_result_plus
2592 : expr.
id() == ID_overflow_result_minus ? ID_minus : ID_mult;
2600 (expr.
id() == ID_overflow_result_plus ||
2601 expr.
id() == ID_overflow_result_mult) &&
2602 op_type_id == ID_natural)
2607 expr.
id() == ID_overflow_result_plus ? ID_plus : ID_mult,
2614 if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2618 if(expr.
id() == ID_overflow_result_minus)
2628 if(sum->type().id() == ID_pointer)
2633 if(offset->id() == ID_pointer_offset)
2643 offset_op.
type().
id() != ID_signedbv &&
2644 offset_op.
type().
id() != ID_unsignedbv)
2649 const std::size_t width =
2674 for(
const auto &op : expr.
operands())
2676 const typet &sizeof_type =
2677 static_cast<const typet &
>(op.find(ID_C_c_sizeof_type));
2680 c_sizeof_type = sizeof_type;
2687 if(!op0_value.has_value() || !op1_value.has_value())
2691 if(expr.
id() == ID_overflow_result_plus)
2692 no_overflow_result = *op0_value + *op1_value;
2693 else if(expr.
id() == ID_overflow_result_minus)
2694 no_overflow_result = *op0_value - *op1_value;
2695 else if(expr.
id() == ID_overflow_result_mult)
2696 no_overflow_result = *op0_value * *op1_value;
2697 else if(expr.
id() == ID_overflow_result_shl)
2698 no_overflow_result = *op0_value << *op1_value;
2702 exprt no_overflow_result_expr =
2704 if(c_sizeof_type.has_value())
2705 no_overflow_result_expr.
set(ID_C_c_sizeof_type, *c_sizeof_type);
2710 no_overflow_result < bv_type.smallest() ||
2711 no_overflow_result > bv_type.largest())
2714 {std::move(no_overflow_result_expr),
true_exprt{}}, expr.
type()};
2730 if(expr.
id()==ID_address_of)
2734 else if(expr.
id()==ID_if)
2736 else if(expr.
id() == ID_typecast)
2745 if(r_it.has_changed())
2754 if(
as_const(expr).type().
id() == ID_array)
2784 if(expr.
id()==ID_typecast)
2788 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2789 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2790 expr.
id()==ID_ge || expr.
id()==ID_le)
2794 else if(expr.
id()==ID_if)
2798 else if(expr.
id()==ID_lambda)
2802 else if(expr.
id()==ID_with)
2806 else if(expr.
id()==ID_update)
2810 else if(expr.
id()==ID_index)
2814 else if(expr.
id()==ID_member)
2818 else if(expr.
id()==ID_byte_update_little_endian ||
2819 expr.
id()==ID_byte_update_big_endian)
2823 else if(expr.
id()==ID_byte_extract_little_endian ||
2824 expr.
id()==ID_byte_extract_big_endian)
2828 else if(expr.
id()==ID_pointer_object)
2832 else if(expr.
id() == ID_is_dynamic_object)
2836 else if(expr.
id() == ID_is_invalid_pointer)
2845 else if(expr.
id()==ID_div)
2849 else if(expr.
id()==ID_mod)
2853 else if(expr.
id()==ID_bitnot)
2857 else if(expr.
id()==ID_bitand ||
2858 expr.
id()==ID_bitor ||
2859 expr.
id()==ID_bitxor)
2863 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2867 else if(expr.
id()==ID_power)
2871 else if(expr.
id()==ID_plus)
2875 else if(expr.
id()==ID_minus)
2879 else if(expr.
id()==ID_mult)
2883 else if(expr.
id()==ID_floatbv_plus ||
2884 expr.
id()==ID_floatbv_minus ||
2885 expr.
id()==ID_floatbv_mult ||
2886 expr.
id()==ID_floatbv_div)
2890 else if(expr.
id()==ID_floatbv_typecast)
2894 else if(expr.
id()==ID_unary_minus)
2898 else if(expr.
id()==ID_unary_plus)
2902 else if(expr.
id()==ID_not)
2906 else if(expr.
id()==ID_implies ||
2907 expr.
id()==ID_or || expr.
id()==ID_xor ||
2912 else if(expr.
id()==ID_dereference)
2916 else if(expr.
id()==ID_address_of)
2920 else if(expr.
id()==ID_pointer_offset)
2924 else if(expr.
id()==ID_extractbit)
2928 else if(expr.
id()==ID_concatenation)
2932 else if(expr.
id()==ID_extractbits)
2936 else if(expr.
id()==ID_ieee_float_equal ||
2937 expr.
id()==ID_ieee_float_notequal)
2941 else if(expr.
id() == ID_bswap)
2945 else if(expr.
id()==ID_isinf)
2949 else if(expr.
id()==ID_isnan)
2953 else if(expr.
id()==ID_isnormal)
2957 else if(expr.
id()==ID_abs)
2961 else if(expr.
id()==ID_sign)
2965 else if(expr.
id() == ID_popcount)
2969 else if(expr.
id() == ID_count_leading_zeros)
2973 else if(expr.
id() == ID_count_trailing_zeros)
2977 else if(expr.
id() == ID_find_first_set)
2981 else if(expr.
id() == ID_function_application)
2985 else if(expr.
id() == ID_complex_real || expr.
id() == ID_complex_imag)
2990 const auto binary_overflow =
2996 const auto unary_overflow =
3002 const auto overflow_result =
3007 else if(expr.
id() == ID_bitreverse)
3012 const auto prophecy_r_or_w_ok =
3018 const auto prophecy_pointer_in_range =
3024 if(!no_change_join_operands)
3030# ifdef DEBUG_ON_DEMAND
3035 std::cout <<
"===== " << node.
id() <<
": " <<
format(node) <<
'\n'
3036 <<
" ---> " <<
format(
r.expr) <<
'\n';
3048 std::pair<simplify_expr_cachet::containert::iterator, bool>
3049 cache_result=simplify_expr_cache.container().
3050 insert(std::pair<exprt, exprt>(expr,
exprt()));
3052 if(!cache_result.second)
3054 const exprt &new_expr=cache_result.first->second;
3070 if(simplify_node_result.has_changed())
3073 tmp = simplify_node_result.expr;
3076#ifdef USE_LOCAL_REPLACE_MAP
3078 replace_mapt::const_iterator it=local_replace_map.
find(tmp);
3079 if(it!=local_replace_map.end())
3085 if(!local_replace_map.empty() &&
3101 (
as_const(tmp).type().
id() == ID_array && expr.
type().
id() == ID_array) ||
3108 cache_result.first->second = tmp;
3111 return std::move(tmp);
3118#ifdef DEBUG_ON_DEMAND
3120 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
3123#ifdef DEBUG_ON_DEMAND
3125 std::cout <<
"FULLSIMP " <<
format(result.expr) <<
"\n";
3127 if(result.has_changed())
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
API to expression classes for bitvectors.
bool can_cast_expr< mult_overflow_exprt >(const exprt &base)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
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.
bool can_cast_expr< minus_overflow_exprt >(const exprt &base)
const find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
bool can_cast_expr< shl_overflow_exprt >(const exprt &base)
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.
bool can_cast_expr< plus_overflow_exprt >(const exprt &base)
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.
bool can_cast_expr< unary_minus_overflow_exprt >(const exprt &base)
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_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.
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.
struct configt::ansi_ct ansi_c
A constant literal expression.
const irep_idt & get_value() const
void set_value(const irep_idt &value)
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
bool zero_permitted() const
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
bool zero_permitted() const
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Union constructor to support unions without any member (a GCC/Clang feature).
Base class for all expressions.
std::vector< exprt > operandst
bool is_one() const
Return whether the expression is a constant representing 1.
bool has_operands() const
Return true if there is at least one operand.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The Boolean constant false.
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
std::size_t get_fraction_bits() const
Fixed-width bit-vector with signed fixed-point interpretation.
void from_integer(const mp_integer &i)
mp_integer to_integer() const
void set_value(const mp_integer &_v)
void round(const fixedbv_spect &dest_spec)
constant_exprt to_expr() const
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
mp_integer to_integer() const
constant_exprt to_expr() const
void set_sign(bool _sign)
void from_integer(const mp_integer &i)
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
Fixed-width bit-vector representing a signed or unsigned integer.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
A (mathematical) lambda expression.
exprt application(const operandst &arguments) const
Extract member of struct or union.
Binary multiplication Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
The plus expression Associativity is not specified.
The offset (in bytes) of a pointer relative to the object.
The popcount (counting the number of bits set to 1) expression.
const exprt & length() const
const exprt & content() const
Sign of an expression Predicate is true if _op is negative, false otherwise.
Fixed-width bit-vector with two's complement interpretation.
resultt simplify_isnan(const unary_exprt &)
resultt simplify_bitwise(const multi_ary_exprt &)
resultt simplify_power(const binary_exprt &)
resultt simplify_div(const div_exprt &)
resultt simplify_byte_extract(const byte_extract_exprt &)
resultt simplify_bitreverse(const bitreverse_exprt &)
Try to simplify bit-reversing to a constant expression.
resultt simplify_abs(const abs_exprt &)
resultt simplify_isnormal(const unary_exprt &)
resultt simplify_dereference(const dereference_exprt &)
resultt simplify_bitnot(const bitnot_exprt &)
resultt simplify_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &)
Try to simplify prophecy_{r,w,rw}_ok to a constant expression.
resultt simplify_popcount(const popcount_exprt &)
static resultt changed(resultt<> result)
bool simplify_if_preorder(if_exprt &expr)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_if(const if_exprt &)
resultt simplify_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_typecast(const typecast_exprt &)
resultt simplify_pointer_object(const pointer_object_exprt &)
resultt simplify_boolean(const exprt &)
resultt simplify_object(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
resultt simplify_with(const with_exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_not(const not_exprt &)
resultt simplify_isinf(const unary_exprt &)
resultt simplify_overflow_binary(const binary_overflow_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
resultt simplify_function_application(const function_application_exprt &)
Attempt to simplify mathematical function applications if we have enough information to do so.
resultt simplify_index(const index_exprt &)
resultt simplify_bswap(const bswap_exprt &)
resultt simplify_member(const member_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_byte_update(const byte_update_exprt &)
bool simplify_node_preorder(exprt &expr)
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
resultt simplify_update(const update_exprt &)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_mod(const mod_exprt &)
resultt simplify_complex(const unary_exprt &)
resultt simplify_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_is_dynamic_object(const unary_exprt &)
resultt simplify_node(exprt)
bool simplify_typecast_preorder(typecast_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_sign(const sign_exprt &)
resultt simplify_unary_minus(const unary_minus_exprt &)
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
const 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.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Generic base class for unary expressions.
const exprt & op1() const =delete
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
optionalt< 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.
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 is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
const 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)
nonstd::optional< T > optionalt
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.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
exprt pointer_offset_sum(const exprt &a, const exprt &b)
exprt object_size(const exprt &pointer)
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify(exprt &expr, const namespacet &ns)
static simplify_exprt::resultt simplify_string_compare_to(const function_application_exprt &expr, const namespacet &ns)
Simplify String.compareTo function when arguments are constant.
static simplify_exprt::resultt simplify_string_contains(const function_application_exprt &expr, const namespacet &ns)
Simplify String.contains function when arguments are constant.
static simplify_exprt::resultt simplify_string_endswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.endsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_char_at(const function_application_exprt &expr, const namespacet &ns)
Simplify String.charAt function when arguments are constant.
static simplify_exprt::resultt simplify_string_startswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.startsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_is_empty(const function_application_exprt &expr, const namespacet &ns)
Simplify String.isEmpty function when arguments are constant.
static bool lower_case_string_expression(array_exprt &string_data)
Take the passed-in constant string array and lower-case every character.
static simplify_exprt::resultt simplify_string_index_of(const function_application_exprt &expr, const namespacet &ns, const bool search_from_end)
Simplify String.indexOf function when arguments are constant.
static simplify_exprt::resultt simplify_string_equals_ignore_case(const function_application_exprt &expr, const namespacet &ns)
Simplify String.equalsIgnorecase function when arguments are constant.
exprt simplify_expr(exprt src, const namespacet &ns)
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
bool join_operands(exprt &expr)
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)
Get char sequence from content field of a refined string expression.
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define POSTCONDITION_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 binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
String expressions for the string solver.
refined_string_exprt & to_string_expr(exprt &expr)
bool can_cast_expr< refined_string_exprt >(const exprt &base)
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)