47 struct simplify_expr_cachet
51 typedef std::unordered_map<
54 typedef std::unordered_map<exprt, exprt, irep_hash> containert;
57 containert container_normal;
59 containert &container()
61 return container_normal;
65 simplify_expr_cachet simplify_expr_cache;
77 if(type.
id()==ID_floatbv)
84 else if(type.
id()==ID_signedbv ||
85 type.
id()==ID_unsignedbv)
117 if(type.
id()==ID_floatbv)
123 else if(type.
id()==ID_signedbv ||
124 type.
id()==ID_unsignedbv)
147 if(type.
id()==ID_signedbv ||
148 type.
id()==ID_unsignedbv)
155 for(result=0; value!=0; value=value>>1)
174 const typet &expr_type=ns.follow(expr.
type());
178 if(expr.
op0().
id()==ID_infinity)
189 if(op_type.
id()==ID_pointer &&
192 (expr_type.
id()==ID_unsignedbv || expr_type.
id()==ID_signedbv) &&
203 if(expr_type.
id()==ID_pointer &&
204 expr.
op0().
id()==ID_typecast &&
206 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv) &&
211 simplify_typecast(expr);
225 if(expr_type.
id()==ID_bool)
229 inequality.
id(op_type.
id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal);
231 inequality.
lhs()=expr.
op0();
234 simplify_node(inequality);
235 expr.
swap(inequality);
240 if(expr_type.
id()==ID_c_bool &&
241 op_type.
id()!=ID_bool)
245 inequality.
id(op_type.
id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal);
247 inequality.
lhs()=expr.
op0();
250 simplify_node(inequality);
251 expr.
op0()=inequality;
252 simplify_typecast(expr);
257 if(expr_type.
id()==ID_pointer &&
271 if(expr_type.
id()==ID_pointer &&
272 expr.
op0().
id()==ID_typecast &&
273 op_type.
id()==ID_pointer &&
286 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
287 expr.
op0().
id()==ID_typecast &&
289 op_type.
id()==ID_pointer)
292 simplify_typecast(expr.
op0());
293 simplify_typecast(expr);
300 (expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
301 expr.
op0().
id()==ID_plus &&
303 expr.
op0().
op0().
id()==ID_typecast &&
306 op_type.
id()==ID_pointer)
312 if(sub_size==0 || sub_size==1)
318 simplify_rec(expr.
op0());
319 simplify_typecast(expr);
333 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
334 (op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv))
344 if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
345 op_id==ID_unary_minus ||
346 op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
357 it->make_typecast(expr.
type());
358 simplify_typecast(*it);
361 simplify_node(result);
366 else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
375 if((expr_type.
id()==ID_signedbv || expr_type.
id()==ID_unsignedbv) &&
376 op_type.
id()==ID_pointer &&
377 expr.
op0().
id()==ID_plus)
388 if(op.type().id()==ID_pointer)
390 op.make_typecast(size_t_type);
394 op.make_typecast(size_t_type);
407 if(expr.
op0().
id()==ID_if &&
412 simplify_typecast(tmp_op1);
413 simplify_typecast(tmp_op2);
430 static_cast<const typet &
>(operand.
find(ID_C_c_sizeof_type));
432 if(op_type_id==ID_integer ||
433 op_type_id==ID_natural)
439 if(expr_type_id==ID_bool)
445 if(expr_type_id==ID_unsignedbv ||
446 expr_type_id==ID_signedbv ||
447 expr_type_id==ID_c_enum ||
448 expr_type_id==ID_c_bit_field ||
449 expr_type_id==ID_integer)
455 else if(op_type_id==ID_rational)
458 else if(op_type_id==ID_real)
461 else if(op_type_id==ID_bool)
463 if(expr_type_id==ID_unsignedbv ||
464 expr_type_id==ID_signedbv ||
465 expr_type_id==ID_integer ||
466 expr_type_id==ID_natural ||
467 expr_type_id==ID_rational ||
468 expr_type_id==ID_c_bool ||
469 expr_type_id==ID_c_enum ||
470 expr_type_id==ID_c_bit_field)
485 else if(expr_type_id==ID_c_enum_tag)
488 if(c_enum_type.
id()==ID_c_enum)
490 unsigned int_value=operand.
is_true();
492 tmp.
type()=expr_type;
497 else if(expr_type_id==ID_pointer &&
505 else if(op_type_id==ID_unsignedbv ||
506 op_type_id==ID_signedbv ||
507 op_type_id==ID_c_bit_field ||
508 op_type_id==ID_c_bool)
515 if(expr_type_id==ID_bool)
521 if(expr_type_id==ID_c_bool)
527 if(expr_type_id==ID_integer)
533 if(expr_type_id==ID_natural)
542 if(expr_type_id==ID_unsignedbv ||
543 expr_type_id==ID_signedbv ||
544 expr_type_id==ID_bv ||
545 expr_type_id==ID_c_bit_field)
550 expr.
set(ID_C_c_sizeof_type, c_sizeof_type);
555 if(expr_type_id==ID_c_enum_tag)
558 if(c_enum_type.
id()==ID_c_enum)
561 tmp.
type()=expr_type;
567 if(expr_type_id==ID_c_enum)
573 if(expr_type_id==ID_fixedbv)
587 if(expr_type_id==ID_floatbv)
600 if(expr_type_id==ID_rational)
607 else if(op_type_id==ID_fixedbv)
609 if(expr_type_id==ID_unsignedbv ||
610 expr_type_id==ID_signedbv)
617 else if(expr_type_id==ID_fixedbv)
626 else if(op_type_id==ID_floatbv)
630 if(expr_type_id==ID_unsignedbv ||
631 expr_type_id==ID_signedbv)
637 else if(expr_type_id==ID_floatbv)
645 else if(expr_type_id==ID_fixedbv)
657 else if(op_type_id==ID_bv)
659 if(expr_type_id==ID_unsignedbv ||
660 expr_type_id==ID_signedbv ||
661 expr_type_id==ID_floatbv)
668 else if(op_type_id==ID_c_enum_tag)
672 if(base_type.
id()==ID_signedbv || base_type.
id()==ID_unsignedbv)
676 simplify_typecast(expr);
680 else if(op_type_id==ID_c_enum)
683 if(base_type.
id()==ID_signedbv || base_type.
id()==ID_unsignedbv)
687 simplify_typecast(expr);
692 else if(operand.
id()==ID_typecast)
697 op_type_id==expr_type_id &&
698 (expr_type_id==ID_unsignedbv || expr_type_id==ID_signedbv) &&
706 simplify_typecast(expr);
718 if(pointer.
type().
id()!=ID_pointer)
721 if(pointer.
id()==ID_if && pointer.
operands().size()==3)
727 simplify_dereference(tmp_op1);
730 simplify_dereference(tmp_op2);
739 if(pointer.
id()==ID_address_of)
748 else if(pointer.
id()==ID_plus &&
750 pointer.
op0().
id()==ID_address_of)
754 if(address_of.
object().
id()==ID_index)
757 if(ns.follow(old.
array().
type()).
id()==ID_array)
761 ns.follow(old.
array().
type()).subtype());
784 if(truth && cond.
id()==ID_lt && expr.
id()==ID_lt)
786 if(cond.
op0()==expr.
op0() &&
792 if(type_id==ID_integer || type_id==ID_natural)
801 else if(type_id==ID_unsignedbv)
811 else if(type_id==ID_signedbv)
822 if(cond.
op1()==expr.
op1() &&
828 if(type_id==ID_integer || type_id==ID_natural)
837 else if(type_id==ID_unsignedbv)
847 else if(type_id==ID_signedbv)
868 if(expr.
type().
id()==ID_bool)
872 if(!simplify_if_implies(expr, cond, truth, new_truth))
890 result = simplify_if_recursive(*it, cond, truth) && result;
911 result=simplify_if_conj(*it, cond) && result;
932 result=simplify_if_disj(*it, cond) && result;
945 if(cond.
id()==ID_and)
947 tresult = simplify_if_conj(trueexpr, cond) && tresult;
948 fresult = simplify_if_recursive(falseexpr, cond,
false) && fresult;
950 else if(cond.
id()==ID_or)
952 tresult = simplify_if_recursive(trueexpr, cond,
true) && tresult;
953 fresult = simplify_if_disj(falseexpr, cond) && fresult;
957 tresult = simplify_if_recursive(trueexpr, cond,
true) && tresult;
958 fresult = simplify_if_recursive(falseexpr, cond,
false) && fresult;
962 simplify_rec(trueexpr);
964 simplify_rec(falseexpr);
966 return tresult && fresult;
978 if(expr.
id()==ID_and)
983 for(exprt::operandst::iterator it1=operands.begin();
984 it1!=operands.end(); it1++)
986 for(exprt::operandst::iterator it2=operands.begin();
987 it2!=operands.end(); it2++)
990 tmp=simplify_if_recursive(*it1, *it2,
true) && tmp;
999 result=tmp && result;
1012 bool result=simplify_rec(cond);
1025 if(cond.
id()==ID_not)
1030 truevalue.
swap(falsevalue);
1038 if(cond.
id()==ID_and)
1042 if(it->id()==ID_not)
1043 local_replace_map.insert(
1046 local_replace_map.insert(
1051 local_replace_map.insert(std::make_pair(cond,
true_exprt()));
1053 result=simplify_rec(truevalue) && result;
1055 local_replace_map=map_before;
1058 if(cond.
id()==ID_or)
1062 if(it->id()==ID_not)
1063 local_replace_map.insert(
1066 local_replace_map.insert(
1071 local_replace_map.insert(std::make_pair(cond,
false_exprt()));
1073 result=simplify_rec(falsevalue) && result;
1075 local_replace_map.swap(map_before);
1077 result=simplify_rec(truevalue) && result;
1078 result=simplify_rec(falsevalue) && result;
1083 result=simplify_rec(truevalue) && result;
1084 result=simplify_rec(falsevalue) && result;
1101 result = simplify_if_cond(cond) && result;
1102 result = simplify_if_branch(truevalue, falsevalue, cond) && result;
1140 simplify_node(tmp.
op0());
1158 simplify_node(tmp.
op0());
1166 if(truevalue==falsevalue)
1169 tmp.
swap(truevalue);
1174 if(((truevalue.
id()==ID_struct && falsevalue.
id()==ID_struct) ||
1175 (truevalue.
id()==ID_array && falsevalue.
id()==ID_array)) &&
1178 exprt cond_copy=cond;
1179 exprt falsevalue_copy=falsevalue;
1180 expr.
swap(truevalue);
1182 exprt::operandst::const_iterator f_it=
1183 falsevalue_copy.
operands().begin();
1186 if_exprt if_expr(cond_copy, *it, *f_it);
1208 value_list.insert(int_value);
1212 else if(expr.
id()==ID_if)
1217 return get_values(expr.
op1(), value_list) ||
1218 get_values(expr.
operands().back(), value_list);
1242 if(op0_type.
id()==ID_struct)
1244 if(expr.
op0().
id()==ID_struct ||
1245 expr.
op0().
id()==ID_constant)
1250 expr.
op1().
get(ID_component_name);
1253 has_component(component_name))
1257 component_number(component_name);
1268 else if(expr.
op0().
type().
id()==ID_array)
1270 if(expr.
op0().
id()==ID_array ||
1271 expr.
op0().
id()==ID_constant)
1314 exprt *value_ptr=&updated_value;
1316 for(
const auto &e : designator)
1318 const typet &value_ptr_type=ns.follow(value_ptr->
type());
1320 if(e.id()==ID_index_designator &&
1321 value_ptr->
id()==ID_array)
1328 if(i<0 || i>=value_ptr->
operands().size())
1333 else if(e.id()==ID_member_designator &&
1334 value_ptr->
id()==ID_struct)
1337 e.get(ID_component_name);
1340 has_component(component_name))
1344 component_number(component_name);
1346 assert(number<value_ptr->operands().size());
1348 value_ptr=&value_ptr->
operands()[number];
1356 expr.
swap(updated_value);
1363 if(expr.
id()==ID_plus)
1365 if(expr.
type().
id()==ID_pointer)
1369 if(ns.follow(it->type()).
id()==ID_pointer)
1373 simplify_object(expr);
1378 else if(expr.
id()==ID_typecast)
1384 if(op_type.
id()==ID_pointer)
1390 simplify_object(expr);
1393 else if(op_type.
id()==ID_signedbv || op_type.
id()==ID_unsignedbv)
1401 if(tmp.
id()==ID_plus && tmp.
operands().size()==2)
1405 if(cand.
id()==ID_typecast &&
1407 cand.
op0().
id()==ID_address_of)
1412 else if(cand.
id()==ID_typecast &&
1414 cand.
op0().
id()==ID_plus &&
1416 cand.
op0().
op0().
id()==ID_typecast &&
1426 else if(expr.
id()==ID_address_of)
1434 expr.
swap(new_expr);
1435 simplify_object(expr);
1442 expr.
swap(new_expr);
1443 simplify_object(expr);
1453 const std::string &bits,
1458 const typet &type=ns.follow(_type);
1463 if(type.
id()==ID_unsignedbv ||
1464 type.
id()==ID_signedbv ||
1465 type.
id()==ID_floatbv ||
1466 type.
id()==ID_fixedbv)
1470 std::string tmp=bits;
1474 std::reverse(tmp.begin(), tmp.end());
1477 else if(type.
id()==ID_c_enum)
1479 exprt val=bits2expr(bits, type.
subtype(), little_endian);
1483 else if(type.
id()==ID_c_enum_tag)
1489 else if(type.
id()==ID_union)
1496 for(
const auto &component : components)
1498 exprt val=bits2expr(bits, component.type(), little_endian);
1502 return union_exprt(component.get_name(), val, type);
1505 else if(type.
id()==ID_struct)
1515 for(
const auto &component : components)
1520 std::string comp_bits=
1525 exprt comp=bits2expr(comp_bits, component.type(), little_endian);
1530 m_offset_bits+=m_size;
1535 else if(type.
id()==ID_array)
1544 std::size_t el_size=
1551 for(std::size_t i=0; i<n_el; ++i)
1553 std::string el_bits=std::string(bits, i*el_size, el_size);
1554 exprt el=bits2expr(el_bits, type.
subtype(), little_endian);
1571 const typet &type=ns.follow(expr.
type());
1573 if(expr.
id()==ID_constant)
1575 if(type.
id()==ID_unsignedbv ||
1576 type.
id()==ID_signedbv ||
1577 type.
id()==ID_c_enum ||
1578 type.
id()==ID_c_enum_tag ||
1579 type.
id()==ID_floatbv ||
1580 type.
id()==ID_fixedbv)
1583 std::reverse(nat.begin(), nat.end());
1587 std::string result=nat;
1589 result[map.map_bit(i)]=nat[i];
1594 else if(expr.
id()==ID_union)
1598 else if(expr.
id()==ID_struct)
1603 std::string tmp=expr2bits(*it, little_endian);
1610 else if(expr.
id()==ID_array)
1615 std::string tmp=expr2bits(*it, little_endian);
1629 if(expr.
op().
id()==ID_if)
1634 simplify_if(if_expr);
1643 if(expr.
op().
id()==expr.
id())
1648 simplify_plus(expr.
offset());
1651 simplify_byte_extract(expr);
1658 if(((expr.
id()==ID_byte_extract_big_endian &&
1659 expr.
op().
id()==ID_byte_update_big_endian) ||
1660 (expr.
id()==ID_byte_extract_little_endian &&
1661 expr.
op().
id()==ID_byte_update_little_endian)) &&
1671 else if(el_size>=0 &&
1677 simplify_byte_extract(expr);
1706 if(expr.
op().
id()==ID_array_of &&
1707 expr.
op().
op0().
id()==ID_constant)
1709 std::string const_bits=
1710 expr2bits(expr.
op().
op0(),
1714 while(
mp_integer(const_bits.size())<offset*8+el_size)
1715 const_bits+=const_bits;
1717 std::string el_bits=
1727 expr.
id()==ID_byte_extract_little_endian);
1737 if(expr.
op().
id()==ID_array_of &&
1738 (offset*8)%el_size==0 &&
1750 expr2bits(expr.
op(), expr.
id()==ID_byte_extract_little_endian);
1753 if(
mp_integer(bits.size())==el_size+offset*8)
1755 std::string bits_cut=
1765 expr.
id()==ID_byte_extract_little_endian);
1776 if(expr.
id()!=ID_byte_extract_little_endian)
1782 if(op_type.
id()==ID_array)
1787 for(
const typet *op_type_ptr=&op_type;
1788 op_type_ptr->
id()==ID_array;
1789 op_type_ptr=&(ns.follow(*op_type_ptr).subtype()))
1794 assert(el_size%8==0);
1798 (expr.
type().
id()==ID_pointer &&
1799 op_type_ptr->subtype().id()==ID_pointer))
1801 if(offset%el_bytes==0)
1835 else if(op_type.
id()==ID_struct)
1843 for(
const auto &component : components)
1850 if(offset*8==m_offset_bits &&
1855 simplify_member(member);
1860 else if(offset*8>=m_offset_bits &&
1861 offset*8+el_size<=m_offset_bits+m_size &&
1866 simplify_member(expr.
op());
1869 simplify_rec(expr.
offset());
1874 m_offset_bits+=m_size;
1885 if(expr.
id()==expr.
op().
id() &&
1903 val_size>=root_size)
1906 expr.
id()==ID_byte_update_little_endian ?
1907 ID_byte_extract_little_endian :
1908 ID_byte_extract_big_endian,
1909 value, offset, expr.
type());
1911 simplify_byte_extract(be);
1925 if(expr.
id()!=ID_byte_update_little_endian)
1928 if(value.
id()==ID_with)
1932 if(with.
old().
id()==ID_byte_extract_little_endian)
1939 if(!(root==extract.
op()))
1941 if(!(offset==extract.
offset()))
1945 if(tp.
id()==ID_struct)
1964 simplify_node(new_offset);
1968 simplify_byte_update(expr);
1973 else if(tp.
id()==ID_array)
1980 simplify_node(index_offset);
1987 index_offset.
swap(tmp);
1991 simplify_node(new_offset);
1995 simplify_byte_update(expr);
2004 if(
to_integer(offset, offset_int) || offset_int<0)
2007 const typet &op_type=ns.follow(root.
type());
2015 if(op_type.
id()==ID_struct)
2026 struct_type.components();
2028 for(
const auto &component : components)
2045 else if(m_offset+m_size_bytes<=offset_int)
2048 else if(update_size>0 &&
2049 m_offset>=offset_int+update_size)
2053 result_expr=expr.
op();
2055 exprt member_name(ID_member_name);
2056 member_name.
set(ID_component_name, component.get_name());
2060 if(m_offset<offset_int ||
2061 (m_offset==offset_int &&
2063 m_size_bytes>update_size))
2066 ID_byte_update_little_endian,
2073 else if(update_size>0 &&
2074 m_offset+m_size_bytes>offset_int+update_size)
2083 ID_byte_extract_little_endian,
2094 simplify_rec(result_expr);
2095 expr.
swap(result_expr);
2103 if(root.
id()==ID_array)
2106 if(el_size<=0 || el_size%8!=0 || val_size%8!=0)
2114 if(offset_int*8+val_size<=m_offset_bits)
2117 if(offset_int*8<m_offset_bits+el_size)
2119 mp_integer bytes_req=(m_offset_bits+el_size)/8-offset_int;
2120 bytes_req-=val_offset;
2121 if(val_offset+bytes_req>val_size/8)
2122 bytes_req=val_size/8-val_offset;
2139 val_offset+=bytes_req;
2142 m_offset_bits+=el_size;
2159 if(expr.
id()==ID_address_of)
2163 else if(expr.
id()==ID_if)
2164 result=simplify_if_preorder(
to_if_expr(expr));
2170 if(!simplify_rec(*it))
2193 if(expr.
id()==ID_typecast)
2194 result=simplify_typecast(expr) && result;
2195 else if(expr.
id()==ID_equal || expr.
id()==ID_notequal ||
2196 expr.
id()==ID_gt || expr.
id()==ID_lt ||
2197 expr.
id()==ID_ge || expr.
id()==ID_le)
2198 result=simplify_inequality(expr) && result;
2199 else if(expr.
id()==ID_if)
2200 result=simplify_if(
to_if_expr(expr)) && result;
2201 else if(expr.
id()==ID_lambda)
2202 result=simplify_lambda(expr) && result;
2203 else if(expr.
id()==ID_with)
2204 result=simplify_with(expr) && result;
2205 else if(expr.
id()==ID_update)
2206 result=simplify_update(expr) && result;
2207 else if(expr.
id()==ID_index)
2208 result=simplify_index(expr) && result;
2209 else if(expr.
id()==ID_member)
2210 result=simplify_member(expr) && result;
2211 else if(expr.
id()==ID_byte_update_little_endian ||
2212 expr.
id()==ID_byte_update_big_endian)
2214 else if(expr.
id()==ID_byte_extract_little_endian ||
2215 expr.
id()==ID_byte_extract_big_endian)
2217 else if(expr.
id()==ID_pointer_object)
2218 result=simplify_pointer_object(expr) && result;
2219 else if(expr.
id()==ID_dynamic_object)
2220 result=simplify_dynamic_object(expr) && result;
2221 else if(expr.
id()==ID_invalid_pointer)
2222 result=simplify_invalid_pointer(expr) && result;
2223 else if(expr.
id()==ID_object_size)
2224 result=simplify_object_size(expr) && result;
2225 else if(expr.
id()==ID_good_pointer)
2226 result=simplify_good_pointer(expr) && result;
2227 else if(expr.
id()==ID_div)
2228 result=simplify_div(expr) && result;
2229 else if(expr.
id()==ID_mod)
2230 result=simplify_mod(expr) && result;
2231 else if(expr.
id()==ID_bitnot)
2232 result=simplify_bitnot(expr) && result;
2233 else if(expr.
id()==ID_bitand ||
2234 expr.
id()==ID_bitor ||
2235 expr.
id()==ID_bitxor)
2236 result=simplify_bitwise(expr) && result;
2237 else if(expr.
id()==ID_ashr || expr.
id()==ID_lshr || expr.
id()==ID_shl)
2238 result=simplify_shifts(expr) && result;
2239 else if(expr.
id()==ID_power)
2240 result=simplify_power(expr) && result;
2241 else if(expr.
id()==ID_plus)
2242 result=simplify_plus(expr) && result;
2243 else if(expr.
id()==ID_minus)
2244 result=simplify_minus(expr) && result;
2245 else if(expr.
id()==ID_mult)
2246 result=simplify_mult(expr) && result;
2247 else if(expr.
id()==ID_floatbv_plus ||
2248 expr.
id()==ID_floatbv_minus ||
2249 expr.
id()==ID_floatbv_mult ||
2250 expr.
id()==ID_floatbv_div)
2251 result=simplify_floatbv_op(expr) && result;
2252 else if(expr.
id()==ID_floatbv_typecast)
2253 result=simplify_floatbv_typecast(expr) && result;
2254 else if(expr.
id()==ID_unary_minus)
2255 result=simplify_unary_minus(expr) && result;
2256 else if(expr.
id()==ID_unary_plus)
2257 result=simplify_unary_plus(expr) && result;
2258 else if(expr.
id()==ID_not)
2259 result=simplify_not(expr) && result;
2260 else if(expr.
id()==ID_implies || expr.
id()==ID_iff ||
2261 expr.
id()==ID_or || expr.
id()==ID_xor ||
2263 result=simplify_boolean(expr) && result;
2264 else if(expr.
id()==ID_dereference)
2265 result=simplify_dereference(expr) && result;
2266 else if(expr.
id()==ID_address_of)
2267 result=simplify_address_of(expr) && result;
2268 else if(expr.
id()==ID_pointer_offset)
2269 result=simplify_pointer_offset(expr) && result;
2270 else if(expr.
id()==ID_extractbit)
2271 result=simplify_extractbit(expr) && result;
2272 else if(expr.
id()==ID_concatenation)
2273 result=simplify_concatenation(expr) && result;
2274 else if(expr.
id()==ID_extractbits)
2275 result=simplify_extractbits(expr) && result;
2276 else if(expr.
id()==ID_ieee_float_equal ||
2277 expr.
id()==ID_ieee_float_notequal)
2278 result=simplify_ieee_float_relation(expr) && result;
2279 else if(expr.
id()==ID_bswap)
2280 result=simplify_bswap(expr) && result;
2281 else if(expr.
id()==ID_isinf)
2282 result=simplify_isinf(expr) && result;
2283 else if(expr.
id()==ID_isnan)
2284 result=simplify_isnan(expr) && result;
2285 else if(expr.
id()==ID_isnormal)
2286 result=simplify_isnormal(expr) && result;
2287 else if(expr.
id()==ID_abs)
2288 result=simplify_abs(expr) && result;
2289 else if(expr.
id()==ID_sign)
2290 result=simplify_sign(expr) && result;
2291 else if(expr.
id()==ID_popcount)
2292 result=simplify_popcount(expr) && result;
2296 #ifdef DEBUG_ON_DEMAND
2301 std::cout <<
"===== " <<
from_expr(ns,
"", old)
2302 <<
"\n ---> " <<
from_expr(ns,
"", expr)
2316 std::pair<simplify_expr_cachet::containert::iterator, bool>
2317 cache_result=simplify_expr_cache.container().
2318 insert(std::pair<exprt, exprt>(expr,
exprt()));
2320 if(!cache_result.second)
2322 const exprt &new_expr=cache_result.first->second;
2336 result=simplify_node_preorder(tmp);
2338 if(!simplify_node(tmp))
2342 replace_mapt::const_iterator it=local_replace_map.find(tmp);
2343 if(it!=local_replace_map.end())
2349 if(!local_replace_map.empty() &&
2363 cache_result.first->second=expr;
2372 #ifdef DEBUG_ON_DEMAND 2374 std::cout <<
"TO-SIMP " <<
from_expr(ns,
"", expr) <<
"\n";
2376 bool res=simplify_rec(expr);
2377 #ifdef DEBUG_ON_DEMAND 2379 std::cout <<
"FULLSIMP " <<
from_expr(ns,
"", expr) <<
"\n";
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
The type of an expression.
bool simplify_abs(exprt &expr)
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
std::size_t get_fraction_bits() const
bool simplify_sign(exprt &expr)
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
Maps a big-endian offset to a little-endian offset.
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
void set_value(const mp_integer &_v)
const mp_integer string2integer(const std::string &n, unsigned base)
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)
Fixed-width bit-vector with IEEE floating-point interpretation.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Deprecated expression utility functions.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
exprt::operandst & designator()
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< componentt > componentst
void move_to_operands(exprt &expr)
const irep_idt & get_value() const
The null pointer constant.
std::string expr2bits(const exprt &expr, bool little_endian)
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.
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
unsignedbv_typet size_type()
A constant literal expression.
void make_bool(bool value)
bool simplify_with(exprt &expr)
bool simplify_if_conj(exprt &expr, const exprt &cond)
void round(const fixedbv_spect &dest_spec)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
bool simplify_node_preorder(exprt &expr)
Extract member of struct or union.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
void change_spec(const ieee_float_spect &dest_spec)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
bool simplify_if(if_exprt &expr)
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
void set_value(const irep_idt &value)
mp_integer to_integer() const
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
Expression classes for byte-level operators.
The boolean constant true.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
bool simplify_object(exprt &expr)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
void from_integer(const mp_integer &i)
bool simplify_if_disj(exprt &expr, const exprt &cond)
const update_exprt & to_update_expr(const exprt &expr)
Cast a generic exprt to an update_exprt.
union constructor from single element
API to expression classes.
const irep_idt & get(const irep_namet &name) const
irep_idt byte_extract_id()
bool simplify_byte_extract(byte_extract_exprt &expr)
const exprt & size() const
#define forall_operands(it, expr)
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
exprt bits2expr(const std::string &bits, const typet &type, bool little_endian)
Operator to return the address of an object.
constant_exprt to_expr() const
Various predicates over pointers in programs.
Fixed-width bit-vector with signed fixed-point interpretation.
bool has_operands() const
The boolean constant false.
std::size_t get_width() const
bool get_values(const exprt &expr, value_listt &value_list)
bool simplify_popcount(exprt &expr)
std::vector< exprt > operandst
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
mp_integer to_integer() const
bool simplify_if_preorder(if_exprt &expr)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
bool simplify_typecast(exprt &expr)
bool simplify_rec(exprt &expr)
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Base class for all expressions.
Operator to update elements in structs and arrays.
const source_locationt & source_location() const
void base_type(typet &type, const namespacet &ns)
const std::string & get_string(const irep_namet &name) const
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)
source_locationt & add_source_location()
bool simplify_dereference(exprt &expr)
size_t map_bit(size_t bit) const
std::size_t integer2size_t(const mp_integer &n)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
std::set< mp_integer > value_listt
const typet & subtype() const
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)
void make_typecast(const typet &_type)
const irept & find(const irep_namet &name) const
array constructor from list of elements
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
bool simplify_byte_update(byte_update_exprt &expr)
bool simplify(exprt &expr, const namespacet &ns)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.