41 struct simplify_expr_cachet
45 typedef std::unordered_map<
48 typedef std::unordered_map<exprt, exprt, irep_hash> containert;
51 containert container_normal;
53 containert &container()
55 return container_normal;
59 simplify_expr_cachet simplify_expr_cache;
71 if(type.
id()==ID_floatbv)
78 else if(type.
id()==ID_signedbv ||
79 type.
id()==ID_unsignedbv)
111 if(type.
id()==ID_floatbv)
117 else if(type.
id()==ID_signedbv ||
118 type.
id()==ID_unsignedbv)
121 if(value.has_value())
140 if(op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv)
144 std::size_t result = 0;
146 for(std::size_t i = 0; i < width; i++)
151 expr.
swap(result_expr);
169 if(expr.
op0().
id()==ID_infinity)
180 if(op_type.
id()==ID_pointer &&
183 (expr_type.
id()==ID_unsignedbv || expr_type.
id()==ID_signedbv) &&
194 if(expr_type.
id()==ID_pointer &&
195 expr.
op0().
id()==ID_typecast &&
197 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv) &&
217 if(expr_type.
id()==ID_bool)
221 inequality.
id(op_type.
id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal);
223 inequality.
lhs()=expr.
op0();
227 expr.
swap(inequality);
233 expr.
op0().
id()==ID_typecast)
242 if(typecast.op().type()==expr_type)
251 if(expr_type.
id()==ID_c_bool &&
252 op_type.
id()!=ID_bool)
257 expr.
op0()=inequality;
263 if(expr_type.
id()==ID_pointer &&
277 if(expr_type.
id()==ID_pointer &&
278 expr.
op0().
id()==ID_typecast &&
279 op_type.
id()==ID_pointer &&
292 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
293 expr.
op0().
id()==ID_typecast &&
295 op_type.
id()==ID_pointer)
306 (expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
307 op_type.
id()==ID_pointer &&
308 expr.
op0().
id()==ID_plus &&
310 ((expr.
op0().
op0().
id()==ID_typecast &&
317 if(sub_size.has_value())
320 if(*sub_size == 0 || *sub_size == 1)
342 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
343 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv))
353 if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
354 op_id==ID_unary_minus ||
355 op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
366 it->make_typecast(expr.
type());
375 else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
384 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
385 op_type.
id()==ID_pointer &&
386 expr.
op0().
id()==ID_plus)
390 if(step.has_value() && *step != 0)
397 if(op.type().id()==ID_pointer)
399 op.make_typecast(size_t_type);
403 op.make_typecast(size_t_type);
416 if(expr.
op0().
id()==ID_if &&
439 static_cast<const typet &
>(operand.
find(ID_C_c_sizeof_type));
441 if(op_type_id==ID_integer ||
442 op_type_id==ID_natural)
448 if(expr_type_id==ID_bool)
454 if(expr_type_id==ID_unsignedbv ||
455 expr_type_id==ID_signedbv ||
456 expr_type_id==ID_c_enum ||
457 expr_type_id==ID_c_bit_field ||
458 expr_type_id==ID_integer)
464 else if(op_type_id==ID_rational)
467 else if(op_type_id==ID_real)
470 else if(op_type_id==ID_bool)
472 if(expr_type_id==ID_unsignedbv ||
473 expr_type_id==ID_signedbv ||
474 expr_type_id==ID_integer ||
475 expr_type_id==ID_natural ||
476 expr_type_id==ID_rational ||
477 expr_type_id==ID_c_bool ||
478 expr_type_id==ID_c_enum ||
479 expr_type_id==ID_c_bit_field)
494 else if(expr_type_id==ID_c_enum_tag)
497 if(c_enum_type.
id()==ID_c_enum)
499 unsigned int_value = operand.
is_true() ? 1u : 0u;
501 tmp.
type()=expr_type;
506 else if(expr_type_id==ID_pointer &&
514 else if(op_type_id==ID_unsignedbv ||
515 op_type_id==ID_signedbv ||
516 op_type_id==ID_c_bit_field ||
517 op_type_id==ID_c_bool)
524 if(expr_type_id==ID_bool)
530 if(expr_type_id==ID_c_bool)
536 if(expr_type_id==ID_integer)
542 if(expr_type_id==ID_natural)
551 if(expr_type_id==ID_unsignedbv ||
552 expr_type_id==ID_signedbv ||
553 expr_type_id==ID_bv ||
554 expr_type_id==ID_c_bit_field)
559 expr.
set(ID_C_c_sizeof_type, c_sizeof_type);
564 if(expr_type_id==ID_c_enum_tag)
567 if(c_enum_type.
id()==ID_c_enum)
570 tmp.
type()=expr_type;
576 if(expr_type_id==ID_c_enum)
582 if(expr_type_id==ID_fixedbv)
596 if(expr_type_id==ID_floatbv)
609 if(expr_type_id==ID_rational)
616 else if(op_type_id==ID_fixedbv)
618 if(expr_type_id==ID_unsignedbv ||
619 expr_type_id==ID_signedbv)
626 else if(expr_type_id==ID_fixedbv)
635 else if(op_type_id==ID_floatbv)
639 if(expr_type_id==ID_unsignedbv ||
640 expr_type_id==ID_signedbv)
646 else if(expr_type_id==ID_floatbv)
653 else if(expr_type_id==ID_fixedbv)
665 else if(op_type_id==ID_bv)
667 if(expr_type_id==ID_unsignedbv ||
668 expr_type_id==ID_signedbv ||
669 expr_type_id==ID_floatbv)
677 else if(op_type_id==ID_c_enum_tag)
689 else if(op_type_id==ID_c_enum)
701 else if(operand.
id()==ID_typecast)
706 op_type_id==expr_type_id &&
707 (expr_type_id==ID_unsignedbv || expr_type_id==ID_signedbv) &&
719 else if(operand.
id()==ID_address_of)
724 if(o.
type().
id()==ID_array &&
741 if(pointer.
type().
id()!=ID_pointer)
744 if(pointer.
id()==ID_if && pointer.
operands().size()==3)
762 if(pointer.
id()==ID_address_of)
771 else if(pointer.
id()==ID_plus &&
773 pointer.
op0().
id()==ID_address_of)
777 if(address_of.
object().
id()==ID_index)
807 if(truth && cond.
id()==ID_lt && expr.
id()==ID_lt)
809 if(cond.
op0()==expr.
op0() &&
828 if(cond.
op1()==expr.
op1() &&
856 if(expr.
type().
id()==ID_bool)
933 if(cond.
id()==ID_and)
938 else if(cond.
id()==ID_or)
954 return tresult && fresult;
966 if(expr.
id()==ID_and)
971 for(exprt::operandst::iterator it1=operands.begin();
972 it1!=operands.end(); it1++)
974 for(exprt::operandst::iterator it2=operands.begin();
975 it2!=operands.end(); it2++)
987 result=tmp && result;
1013 if(cond.
id()==ID_not)
1018 truevalue.
swap(falsevalue);
1022 #ifdef USE_LOCAL_REPLACE_MAP 1026 if(cond.
id()==ID_and)
1030 if(it->id()==ID_not)
1031 local_replace_map.insert(
1034 local_replace_map.insert(
1039 local_replace_map.insert(std::make_pair(cond,
true_exprt()));
1043 local_replace_map=map_before;
1046 if(cond.
id()==ID_or)
1050 if(it->id()==ID_not)
1051 local_replace_map.insert(
1054 local_replace_map.insert(
1059 local_replace_map.insert(std::make_pair(cond,
false_exprt()));
1063 local_replace_map.swap(map_before);
1150 if(truevalue==falsevalue)
1153 tmp.
swap(truevalue);
1158 if(((truevalue.
id()==ID_struct && falsevalue.
id()==ID_struct) ||
1159 (truevalue.
id()==ID_array && falsevalue.
id()==ID_array)) &&
1162 exprt cond_copy=cond;
1163 exprt falsevalue_copy=falsevalue;
1164 expr.
swap(truevalue);
1166 exprt::operandst::const_iterator f_it=
1167 falsevalue_copy.
operands().begin();
1170 if_exprt if_expr(cond_copy, *it, *f_it);
1192 value_list.insert(int_value);
1196 else if(expr.
id()==ID_if)
1226 if(op0_type.
id()==ID_struct)
1228 if(expr.
op0().
id()==ID_struct ||
1229 expr.
op0().
id()==ID_constant)
1234 expr.
op1().
get(ID_component_name);
1237 has_component(component_name))
1241 component_number(component_name);
1252 else if(expr.
op0().
type().
id()==ID_array)
1254 if(expr.
op0().
id()==ID_array ||
1255 expr.
op0().
id()==ID_constant)
1267 expr.
op0().
operands()[numeric_cast_v<std::size_t>(*i)].swap(expr.
op2());
1298 exprt *value_ptr=&updated_value;
1300 for(
const auto &e : designator)
1304 if(e.id()==ID_index_designator &&
1305 value_ptr->
id()==ID_array)
1312 if(*i < 0 || *i >= value_ptr->
operands().size())
1315 value_ptr = &value_ptr->
operands()[numeric_cast_v<std::size_t>(*i)];
1317 else if(e.id()==ID_member_designator &&
1318 value_ptr->
id()==ID_struct)
1321 e.get(ID_component_name);
1327 value_ptr = &designator_as_struct_expr.component(component_name,
ns);
1336 expr.
swap(updated_value);
1343 if(expr.
id()==ID_plus)
1345 if(expr.
type().
id()==ID_pointer)
1349 if(
ns.
follow(it->type()).
id()==ID_pointer)
1358 else if(expr.
id()==ID_typecast)
1361 const typet &op_type =
ns.
follow(typecast_expr.op().type());
1363 if(op_type.
id()==ID_pointer)
1366 expr = typecast_expr.op();
1370 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1377 const exprt &casted_expr = typecast_expr.op();
1378 if(casted_expr.
id() == ID_plus && casted_expr.
operands().size() == 2)
1380 const exprt &cand = casted_expr.
op0().
id() == ID_typecast
1382 : casted_expr.
op1();
1384 if(cand.
id()==ID_typecast &&
1386 cand.
op0().
id()==ID_address_of)
1391 else if(cand.
id()==ID_typecast &&
1393 cand.
op0().
id()==ID_plus &&
1395 cand.
op0().
op0().
id()==ID_typecast &&
1405 else if(expr.
id()==ID_address_of)
1413 expr.
swap(new_expr);
1421 expr.
swap(new_expr);
1432 const std::string &bits,
1441 if(!type_bits.has_value() || *type_bits != bits.size())
1444 if(type.
id()==ID_unsignedbv ||
1445 type.
id()==ID_signedbv ||
1446 type.
id()==ID_floatbv ||
1447 type.
id()==ID_fixedbv)
1451 std::string tmp=bits;
1455 std::reverse(tmp.begin(), tmp.end());
1460 else if(type.
id()==ID_c_enum)
1466 else if(type.
id()==ID_c_enum_tag)
1472 else if(type.
id()==ID_union)
1488 else if(type.
id()==ID_struct)
1503 std::string comp_bits = std::string(
1505 numeric_cast_v<std::size_t>(m_offset_bits),
1506 numeric_cast_v<std::size_t>(*m_size));
1513 m_offset_bits += *m_size;
1516 return std::move(result);
1518 else if(type.
id()==ID_array)
1522 const std::size_t n_el = numeric_cast_v<std::size_t>(array_type.
size());
1525 CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
1527 const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
1532 for(std::size_t i=0; i<n_el; ++i)
1534 std::string el_bits=std::string(bits, i*el_size, el_size);
1541 return std::move(result);
1554 if(expr.
id()==ID_constant)
1558 if(type.
id()==ID_unsignedbv ||
1559 type.
id()==ID_signedbv ||
1560 type.
id()==ID_floatbv ||
1561 type.
id()==ID_fixedbv)
1567 std::string result(width,
' ');
1574 else if(type.
id() == ID_c_enum_tag)
1579 else if(type.
id() == ID_c_enum)
1585 else if(expr.
id()==ID_union)
1589 else if(expr.
id()==ID_struct)
1595 if(!tmp.has_value())
1597 result+=tmp.value();
1602 else if(expr.
id()==ID_array)
1608 if(!tmp.has_value())
1610 result+=tmp.value();
1622 if(expr.
op().
id()==ID_if)
1636 if(expr.
op().
id()==expr.
id())
1651 if(((expr.
id()==ID_byte_extract_big_endian &&
1652 expr.
op().
id()==ID_byte_update_big_endian) ||
1653 (expr.
id()==ID_byte_extract_little_endian &&
1654 expr.
op().
id()==ID_byte_update_little_endian)) &&
1665 el_size.has_value() &&
1679 if(!offset.has_value() || *offset < 0)
1695 expr.
type().
id() == ID_pointer && expr.
op().
type().
id() == ID_pointer)
1706 if(!el_size.has_value() || *el_size == 0)
1709 if(expr.
op().
id()==ID_array_of &&
1712 const auto const_bits_opt=
1716 if(!const_bits_opt.has_value())
1719 std::string const_bits=const_bits_opt.value();
1721 DATA_INVARIANT(!const_bits.empty(),
"bit representation must be non-empty");
1724 while(
mp_integer(const_bits.size()) < *offset * 8 + *el_size)
1725 const_bits+=const_bits;
1727 std::string el_bits = std::string(
1729 numeric_cast_v<std::size_t>(*offset * 8),
1730 numeric_cast_v<std::size_t>(*el_size));
1736 expr.
id()==ID_byte_extract_little_endian);
1747 expr.
op().
id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
1759 expr2bits(expr.
op(), expr.
id()==ID_byte_extract_little_endian);
1763 if(bits.has_value() &&
mp_integer(bits->size()) == *el_size + *offset * 8)
1765 std::string bits_cut = std::string(
1767 numeric_cast_v<std::size_t>(*offset * 8),
1768 numeric_cast_v<std::size_t>(*el_size));
1774 expr.
id()==ID_byte_extract_little_endian);
1776 if(tmp.is_not_nil())
1787 if(subexpr.
is_nil() || subexpr == expr)
1799 if(expr.
id()==expr.
op().
id() &&
1815 offset.
is_zero() && val_size.has_value() && *val_size > 0 &&
1816 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
1819 expr.
id()==ID_byte_update_little_endian ?
1820 ID_byte_extract_little_endian :
1821 ID_byte_extract_big_endian,
1822 value, offset, expr.
type());
1838 if(expr.
id()!=ID_byte_update_little_endian)
1841 if(value.
id()==ID_with)
1845 if(with.
old().
id()==ID_byte_extract_little_endian)
1852 if(!(root==extract.
op()))
1854 if(!(offset==extract.
offset()))
1858 if(tp.
id()==ID_struct)
1865 if(c_type.
id() == ID_c_bit_field || c_type.
id() == ID_bool)
1886 else if(tp.
id()==ID_array)
1900 index_offset.
swap(tmp);
1917 if(!offset_int.has_value() || *offset_int < 0)
1923 if(!val_size.has_value() || *val_size == 0)
1928 if(op_type.
id()==ID_struct)
1938 struct_type.components();
1947 if(!m_offset.has_value())
1954 if(!m_size_bits.has_value() || *m_size_bits == 0 || (*m_size_bits) % 8 != 0)
1960 mp_integer m_size_bytes = (*m_size_bits) / 8;
1963 if(*m_offset + m_size_bytes <= *offset_int)
1967 update_size.has_value() && *update_size > 0 &&
1968 *m_offset >= *offset_int + *update_size)
1974 result_expr=expr.
op();
1976 exprt member_name(ID_member_name);
1977 member_name.
set(ID_component_name,
component.get_name());
1982 *m_offset < *offset_int ||
1983 (*m_offset == *offset_int && update_size.has_value() &&
1984 *update_size > 0 && m_size_bytes > *update_size))
1987 ID_byte_update_little_endian,
1995 update_size.has_value() && *update_size > 0 &&
1996 *m_offset + m_size_bytes > *offset_int + *update_size)
2005 ID_byte_extract_little_endian,
2017 expr.
swap(result_expr);
2025 expr.
swap(result_expr);
2033 if(root.
id()==ID_array)
2037 if(!el_size.has_value() || *el_size == 0 ||
2038 (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
2048 if(*offset_int * 8 + (*val_size) <= m_offset_bits)
2051 if(*offset_int * 8 < m_offset_bits + *el_size)
2053 mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
2054 bytes_req-=val_offset;
2055 if(val_offset + bytes_req > (*val_size) / 8)
2056 bytes_req = (*val_size) / 8 - val_offset;
2069 *offset_int + val_offset - m_offset_bits / 8, offset.
type()),
2074 val_offset+=bytes_req;
2077 m_offset_bits += *el_size;
2094 if(expr.
id()==ID_address_of)
2098 else if(expr.
id()==ID_if)
2128 if(expr.
id()==ID_typecast)
2130 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2131 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2132 expr.
id()==ID_ge || expr.
id()==ID_le)
2134 else if(expr.
id()==ID_if)
2136 else if(expr.
id()==ID_lambda)
2138 else if(expr.
id()==ID_with)
2140 else if(expr.
id()==ID_update)
2142 else if(expr.
id()==ID_index)
2144 else if(expr.
id()==ID_member)
2146 else if(expr.
id()==ID_byte_update_little_endian ||
2147 expr.
id()==ID_byte_update_big_endian)
2149 else if(expr.
id()==ID_byte_extract_little_endian ||
2150 expr.
id()==ID_byte_extract_big_endian)
2152 else if(expr.
id()==ID_pointer_object)
2154 else if(expr.
id()==ID_dynamic_object)
2156 else if(expr.
id()==ID_invalid_pointer)
2158 else if(expr.
id()==ID_object_size)
2160 else if(expr.
id()==ID_good_pointer)
2162 else if(expr.
id()==ID_div)
2164 else if(expr.
id()==ID_mod)
2166 else if(expr.
id()==ID_bitnot)
2168 else if(expr.
id()==ID_bitand ||
2169 expr.
id()==ID_bitor ||
2170 expr.
id()==ID_bitxor)
2172 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2174 else if(expr.
id()==ID_power)
2176 else if(expr.
id()==ID_plus)
2178 else if(expr.
id()==ID_minus)
2180 else if(expr.
id()==ID_mult)
2182 else if(expr.
id()==ID_floatbv_plus ||
2183 expr.
id()==ID_floatbv_minus ||
2184 expr.
id()==ID_floatbv_mult ||
2185 expr.
id()==ID_floatbv_div)
2187 else if(expr.
id()==ID_floatbv_typecast)
2189 else if(expr.
id()==ID_unary_minus)
2191 else if(expr.
id()==ID_unary_plus)
2193 else if(expr.
id()==ID_not)
2195 else if(expr.
id()==ID_implies ||
2196 expr.
id()==ID_or || expr.
id()==ID_xor ||
2199 else if(expr.
id()==ID_dereference)
2201 else if(expr.
id()==ID_address_of)
2203 else if(expr.
id()==ID_pointer_offset)
2205 else if(expr.
id()==ID_extractbit)
2207 else if(expr.
id()==ID_concatenation)
2209 else if(expr.
id()==ID_extractbits)
2211 else if(expr.
id()==ID_ieee_float_equal ||
2212 expr.
id()==ID_ieee_float_notequal)
2214 else if(expr.
id() == ID_bswap)
2216 else if(expr.
id()==ID_isinf)
2218 else if(expr.
id()==ID_isnan)
2220 else if(expr.
id()==ID_isnormal)
2222 else if(expr.
id()==ID_abs)
2224 else if(expr.
id()==ID_sign)
2226 else if(expr.
id() == ID_popcount)
2231 #ifdef DEBUG_ON_DEMAND
2236 std::cout <<
"===== " <<
format(old) <<
"\n ---> " <<
format(expr)
2250 std::pair<simplify_expr_cachet::containert::iterator, bool>
2251 cache_result=simplify_expr_cache.container().
2252 insert(std::pair<exprt, exprt>(expr,
exprt()));
2254 if(!cache_result.second)
2256 const exprt &new_expr=cache_result.first->second;
2275 #ifdef USE_LOCAL_REPLACE_MAP 2277 replace_mapt::const_iterator it=local_replace_map.find(tmp);
2278 if(it!=local_replace_map.end())
2284 if(!local_replace_map.empty() &&
2299 cache_result.first->second=expr;
2308 #ifdef DEBUG_ON_DEMAND 2310 std::cout <<
"TO-SIMP " <<
format(expr) <<
"\n";
2313 #ifdef DEBUG_ON_DEMAND 2315 std::cout <<
"FULLSIMP " <<
format(expr) <<
"\n";
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality at the top level.
The type of an expression, extends irept.
bool simplify_abs(exprt &expr)
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
bool simplify_member(exprt &expr)
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Semantic type conversion.
std::size_t get_fraction_bits() const
bool simplify_sign(exprt &expr)
A base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
Maps a big-endian offset to a little-endian offset.
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
bool simplify_pointer_object(exprt &expr)
void set_value(const mp_integer &_v)
const mp_integer string2integer(const std::string &n, unsigned base)
bool simplify_popcount(popcount_exprt &expr)
bool simplify_node(exprt &expr)
bool simplify_if_cond(exprt &expr)
constant_exprt to_expr() const
exprt simplify_expr(const exprt &src, const namespacet &ns)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Fixed-width bit-vector with IEEE floating-point interpretation.
bool simplify_shifts(exprt &expr)
bool simplify_index(exprt &expr)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Deprecated expression utility functions.
bool simplify_concatenation(exprt &expr)
bool simplify_dynamic_object(exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
exprt::operandst & designator()
std::vector< componentt > componentst
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
bool is_false() const
Return whether the expression is a constant representing false.
const irep_idt & get_value() const
The null pointer constant.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
bool simplify_lambda(exprt &expr)
const componentst & components() const
void set_sign(bool _sign)
The trinary if-then-else operator.
bool is_true() const
Return whether the expression is a constant representing true.
bool simplify_mult(exprt &expr)
typet & type()
Return the type of the expression.
unsignedbv_typet size_type()
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
A constant literal expression.
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
#define CHECK_RETURN(CONDITION)
Structure type, corresponds to C style structs.
bool simplify_mod(exprt &expr)
bool simplify_with(exprt &expr)
bool simplify_if_conj(exprt &expr, const exprt &cond)
void round(const fixedbv_spect &dest_spec)
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool simplify_node_preorder(exprt &expr)
Extract member of struct or union.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
void change_spec(const ieee_float_spect &dest_spec)
bool simplify_bswap(bswap_exprt &expr)
bool simplify_if(if_exprt &expr)
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
void set_value(const irep_idt &value)
mp_integer to_integer() const
bool simplify_good_pointer(exprt &expr)
Expression classes for byte-level operators.
The Boolean constant true.
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
bool simplify_object(exprt &expr)
exprt get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
bool simplify_floatbv_op(exprt &expr)
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.
bool simplify_div(exprt &expr)
bool simplify_boolean(exprt &expr)
void from_integer(const mp_integer &i)
bool simplify_if_disj(exprt &expr, const exprt &cond)
Fixed-width bit-vector with two's complement interpretation.
nonstd::optional< T > optionalt
bool simplify_address_of(exprt &expr)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Union constructor from single element.
API to expression classes.
bool simplify_pointer_offset(exprt &expr)
bool simplify_isinf(exprt &expr)
const irep_idt & get(const irep_namet &name) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool simplify_byte_extract(byte_extract_exprt &expr)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const exprt & size() const
#define forall_operands(it, expr)
The plus expression Associativity is not specified.
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
exprt bits2expr(const std::string &bits, const typet &type, bool little_endian)
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Operator to return the address of an object.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
constant_exprt to_expr() const
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Fixed-width bit-vector with signed fixed-point interpretation.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
bool has_operands() const
Return true if there is at least one operand.
The Boolean constant false.
bool simplify_unary_plus(exprt &expr)
bool is_constant() const
Return whether the expression is a constant.
std::size_t get_width() const
bool get_values(const exprt &expr, value_listt &value_list)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
bool has_component(const irep_idt &component_name) const
std::vector< exprt > operandst
Binary multiplication Associativity is not specified.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
mp_integer to_integer() const
bool simplify_floatbv_typecast(exprt &expr)
bool simplify_if_preorder(if_exprt &expr)
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
bool simplify_typecast(exprt &expr)
bool simplify_rec(exprt &expr)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
The popcount (counting the number of bits set to 1) expression.
bool simplify_unary_minus(exprt &expr)
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
bool simplify_power(exprt &expr)
bool simplify_bitwise(exprt &expr)
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
bool simplify_ieee_float_relation(exprt &expr)
Operator to update elements in structs and arrays.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const source_locationt & source_location() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
void base_type(typet &type, const namespacet &ns)
bool simplify_update(exprt &expr)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
void from_integer(const mp_integer &i)
virtual bool simplify(exprt &expr)
#define Forall_operands(it, expr)
bool is_zero() const
Return whether the expression is a constant representing 0.
source_locationt & add_source_location()
optionalt< std::string > expr2bits(const exprt &, bool little_endian)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
bool simplify_dereference(exprt &expr)
size_t map_bit(size_t bit) const
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
bool simplify_not(exprt &expr)
bool simplify_extractbit(exprt &expr)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
bool simplify_minus(exprt &expr)
std::set< mp_integer > value_listt
const typet & subtype() const
bool simplify_invalid_pointer(exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
static bool sort_and_join(const struct saj_tablet &saj_entry, const irep_idt &type_id)
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
Struct constructor from list of elements.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bool simplify_isnormal(exprt &expr)
bool simplify_object_size(exprt &expr)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const irept & find(const irep_namet &name) const
Array constructor from list of elements.
bool simplify_plus(exprt &expr)
void set(const irep_namet &name, const irep_idt &value)
void reserve_operands(operandst::size_type n)
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==
bool simplify_byte_update(byte_update_exprt &expr)
bool simplify_bitnot(exprt &expr)
bool simplify_isnan(exprt &expr)
bool simplify(exprt &expr, const namespacet &ns)
irep_idt byte_extract_id()
bool simplify_extractbits(extractbits_exprt &expr)
Simplifies extracting of bits from a constant.