28 if(expr.
type().
id()==ID_unsignedbv &&
36 std::vector<mp_integer> bytes;
39 for(std::size_t bit=0; bit<width; bit+=8)
40 bytes.push_back((value >> bit)%256);
44 for(std::size_t bit=0; bit<width; bit+=8)
46 assert(!bytes.empty());
47 new_value+=bytes.back()<<bit;
71 exprt::operandst::iterator constant;
79 for(exprt::operandst::iterator it=operands.begin();
89 it->type().id()!=ID_floatbv)
96 bool do_erase =
false;
99 if(it->is_constant() && it->type()==expr.
type())
102 if(c_sizeof_type.
is_nil())
104 static_cast<const typet &>(it->find(ID_C_c_sizeof_type));
109 if(!constant->mul(*it))
123 it=operands.erase(it);
133 constant->set(ID_C_c_sizeof_type, c_sizeof_type);
136 if(operands.size()==1)
138 exprt product(operands.front());
146 if(found && constant->is_one())
149 operands.erase(constant);
152 if(operands.size()==1)
154 exprt product(operands.front());
173 if(expr_type!=expr.
op0().
type() ||
177 if(expr_type.
id()==ID_signedbv ||
178 expr_type.
id()==ID_unsignedbv ||
179 expr_type.
id()==ID_natural ||
180 expr_type.
id()==ID_integer)
189 if(ok1 && int_value1==0)
193 if(ok1 && int_value1==1)
202 if(ok0 && int_value0==0)
222 else if(expr_type.
id()==ID_rational)
230 if(ok1 && rat_value1.
is_zero())
233 if((ok1 && rat_value1.
is_one()) ||
254 else if(expr_type.
id()==ID_fixedbv)
291 if(expr.
type().
id()==ID_signedbv ||
292 expr.
type().
id()==ID_unsignedbv ||
293 expr.
type().
id()==ID_natural ||
294 expr.
type().
id()==ID_integer)
305 if(ok1 && int_value1==0)
308 if((ok1 && int_value1==1) ||
309 (ok0 && int_value0==0))
335 expr.
type().
id()!=ID_pointer)
342 assert(expr.
id()==ID_plus);
352 exprt::operandst::iterator next=it;
355 if(next!=operands.end())
357 if(it->type()==next->type() &&
362 operands.erase(next);
370 if(expr.
type().
id()==ID_pointer &&
372 expr.
op0().
id()==ID_plus &&
393 if(
is_number(it->type()) && it->is_constant())
399 exprt::operandst::iterator const_sum;
400 bool const_sum_set=
false;
404 if(
is_number(it->type()) && it->is_constant())
413 if(!const_sum->sum(*it))
416 assert(it->is_not_nil());
426 typedef std::unordered_map<exprt, exprt::operandst::iterator, irep_hash>
431 if(it->id()==ID_unary_minus &&
432 it->operands().size()==1)
433 expr_map.insert(std::make_pair(it->op0(), it));
440 else if(it->id()==ID_unary_minus)
443 expr_mapt::iterator itm=expr_map.find(*it);
445 if(itm!=expr_map.end())
449 assert(it->is_not_nil());
458 for(exprt::operandst::iterator
463 if(
is_number(it->type()) && it->is_zero())
465 it=operands.erase(it);
479 else if(operands.size()==1)
481 exprt tmp(operands.front());
492 expr.
type().
id()!=ID_pointer)
497 assert(expr.
id()==ID_minus);
499 if(operands.size()!=2)
516 else if(expr.
type().
id()==ID_pointer &&
517 operands[0].type().id()==ID_pointer &&
531 operands[0].type().id()==ID_pointer &&
532 operands[1].type().id()==ID_pointer)
536 if(operands[0]==operands[1])
554 if(expr.
type().
id()!=ID_bool)
560 if(it->id()==ID_typecast &&
561 it->operands().size()==1 &&
562 ns.
follow(it->op0().type()).
id()==ID_bool)
565 else if(it->is_zero() || it->is_one())
577 if(expr.
id()==ID_bitand)
579 else if(expr.
id()==ID_bitor)
581 else if(expr.
id()==ID_bitxor)
588 if(it->id()==ID_typecast)
594 else if(it->is_zero())
596 else if(it->is_one())
637 std::string new_value;
638 new_value.resize(width);
640 if(expr.
id()==ID_bitand)
642 for(std::size_t i=0; i<width; i++)
643 new_value[i]=(a_str[i]==
'1' && b_str[i]==
'1')?
'1':
'0';
645 else if(expr.
id()==ID_bitor)
647 for(std::size_t i=0; i<width; i++)
648 new_value[i]=(a_str[i]==
'1' || b_str[i]==
'1')?
'1':
'0';
650 else if(expr.
id()==ID_bitxor)
652 for(std::size_t i=0; i<width; i++)
653 new_value[i]=((a_str[i]==
'1')!=(b_str[i]==
'1'))?
'1':
'0';
669 if(expr.
id()==ID_bitor || expr.
id()==ID_bitxor)
671 for(exprt::operandst::iterator
676 if(it->is_zero() && expr.
operands().size()>1)
688 if(expr.
id()==ID_bitand)
690 for(exprt::operandst::iterator
695 if(it->is_constant() &&
713 if(expr.
id()==ID_bitand || expr.
id()==ID_bitor)
720 else if(expr.
id()==ID_bitxor)
764 if(value.
size()!=width)
805 const std::string new_value=
807 opi.
set(ID_value, new_value);
808 opi.
type().
set(ID_width, new_value.size());
817 else if(expr.
type().
id()==ID_verilog_unsignedbv)
829 (opi.
type().
id()==ID_verilog_unsignedbv ||
831 (opn.
type().
id()==ID_verilog_unsignedbv ||
835 const std::string new_value=
837 opi.
set(ID_value, new_value);
838 opi.
type().
set(ID_width, new_value.size());
839 opi.
type().
id(ID_verilog_unsignedbv);
887 if(expr.
op0().
type().
id()==ID_unsignedbv ||
893 if(expr.
id()==ID_lshr)
903 value/=
power(2, distance);
908 else if(expr.
id()==ID_ashr)
918 else if(expr.
id()==ID_shl)
928 value*=
power(2, distance);
934 else if(expr.
op0().
type().
id()==ID_integer ||
937 if(expr.
id()==ID_lshr)
941 value/=
power(2, distance);
946 else if(expr.
id()==ID_ashr)
952 if(value<0 && new_value==0)
959 else if(expr.
id()==ID_shl)
963 value*=
power(2, distance);
1017 if(start<0 || start>=width ||
1018 end<0 || end>=width)
1025 if(value.
size()!=width)
1030 std::string extracted_value=
1035 tmp.
set(ID_value, extracted_value);
1067 if(operand.
id()==ID_unary_minus)
1081 else if(operand.
id()==ID_constant)
1085 if(type_id==ID_integer ||
1086 type_id==ID_signedbv ||
1087 type_id==ID_unsignedbv)
1103 else if(type_id==ID_rational)
1112 else if(type_id==ID_fixedbv)
1119 else if(type_id==ID_floatbv)
1138 if(operands.size()!=1)
1141 exprt &op=operands.front();
1143 if(expr.
type().
id()==ID_bv ||
1144 expr.
type().
id()==ID_unsignedbv ||
1145 expr.
type().
id()==ID_signedbv)
1149 if(op.
id()==ID_constant)
1153 for(
auto &ch : value)
1154 ch=(ch==
'0')?
'1':
'0';
1157 tmp.
set(ID_value, value);
1172 if(expr.
type().
id()!=ID_bool)
1175 if(operands.size()!=2)
1186 if((expr.
id()==ID_equal || expr.
id()==ID_notequal) &&
1194 if(tmp0.
id()==ID_if && tmp0.
operands().size()==3)
1206 if((tmp0.
id()==ID_address_of ||
1207 (tmp0.
id()==ID_typecast && tmp0.
op0().
id()==ID_address_of)) &&
1208 (tmp1.
id()==ID_address_of ||
1209 (tmp1.
id()==ID_typecast && tmp1.
op0().
id()==ID_address_of)) &&
1210 (expr.
id()==ID_equal || expr.
id()==ID_notequal))
1213 if(tmp0.
id()==ID_pointer_object &&
1214 tmp1.
id()==ID_pointer_object &&
1215 (expr.
id()==ID_equal || expr.
id()==ID_notequal))
1226 if(tmp0.
type().
id()==ID_c_enum_tag)
1229 if(tmp1.
type().
id()==ID_c_enum_tag)
1233 if(op0_is_const && op1_is_const)
1235 if(tmp0.
type().
id()==ID_bool)
1240 if(expr.
id()==ID_equal)
1245 else if(expr.
id()==ID_notequal)
1251 else if(tmp0.
type().
id()==ID_fixedbv)
1256 if(expr.
id()==ID_notequal)
1258 else if(expr.
id()==ID_equal)
1260 else if(expr.
id()==ID_ge)
1262 else if(expr.
id()==ID_le)
1264 else if(expr.
id()==ID_gt)
1266 else if(expr.
id()==ID_lt)
1273 else if(tmp0.
type().
id()==ID_floatbv)
1278 if(expr.
id()==ID_notequal)
1280 else if(expr.
id()==ID_equal)
1282 else if(expr.
id()==ID_ge)
1284 else if(expr.
id()==ID_le)
1286 else if(expr.
id()==ID_gt)
1288 else if(expr.
id()==ID_lt)
1295 else if(tmp0.
type().
id()==ID_rational)
1305 if(expr.
id()==ID_notequal)
1307 else if(expr.
id()==ID_equal)
1309 else if(expr.
id()==ID_ge)
1311 else if(expr.
id()==ID_le)
1313 else if(expr.
id()==ID_gt)
1315 else if(expr.
id()==ID_lt)
1332 if(expr.
id()==ID_notequal)
1334 else if(expr.
id()==ID_equal)
1336 else if(expr.
id()==ID_ge)
1338 else if(expr.
id()==ID_le)
1340 else if(expr.
id()==ID_gt)
1342 else if(expr.
id()==ID_lt)
1350 else if(op0_is_const)
1354 if(expr.
id()==ID_ge)
1356 else if(expr.
id()==ID_le)
1358 else if(expr.
id()==ID_gt)
1360 else if(expr.
id()==ID_lt)
1369 else if(op1_is_const)
1397 if(op0.
id()==ID_plus)
1407 else if(op1.
id()==ID_plus)
1420 op0.
type().
id()!=ID_complex)
1443 if(expr.
id()==ID_notequal)
1451 else if(expr.
id()==ID_gt)
1461 else if(expr.
id()==ID_lt)
1469 else if(expr.
id()==ID_le)
1480 assert(expr.
id()==ID_ge || expr.
id()==ID_equal);
1484 if(operands.front()==operands.back())
1512 if(expr.
id()==ID_ge)
1513 tmp=(int_value0>=int_value1);
1514 else if(expr.
id()==ID_equal)
1515 tmp=(int_value0==int_value1);
1527 else if(result!=tmp)
1543 if(expr.
id()==ID_equal)
1578 if(expr.
id()==ID_notequal)
1588 if(expr.
id()==ID_equal &&
1590 expr.
op1().
get(ID_value)==ID_NULL)
1594 if(expr.
op0().
id()==ID_address_of &&
1597 if(expr.
op0().
op0().
id()==ID_symbol ||
1598 expr.
op0().
op0().
id()==ID_dynamic_object ||
1599 expr.
op0().
op0().
id()==ID_member ||
1601 expr.
op0().
op0().
id()==ID_string_constant)
1607 else if(expr.
op0().
id()==ID_typecast &&
1610 expr.
op0().
op0().
id()==ID_address_of &&
1623 else if(expr.
op0().
id()==ID_typecast &&
1648 if(expr.
op0().
id()==ID_plus)
1652 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1659 if(it->is_constant())
1666 assert(it->is_not_nil());
1691 if(expr.
op0().
id()==ID_typecast &&
1700 ieee_floatt const_val_converted_back=const_val_converted;
1703 if(const_val_converted_back==const_val)
1718 if(expr.
id()==ID_ge &&
1728 if(expr.
id()==ID_equal)
1731 if(operand.
id()==ID_unary_minus)
1740 else if(operand.
id()==ID_plus)
1748 if(operand.
op0().
id()==ID_unary_minus)
1751 if(operand.
op1().
id()==ID_unary_minus &&
1756 tmp.op0().swap(operand.
op0());
1757 tmp.op1().swap(operand.
op1().
op0());
1767 if(expr.
op0().
id()==ID_typecast &&
1787 #define NORMALISE_CONSTANT_TESTS 1788 #ifdef NORMALISE_CONSTANT_TESTS 1790 if(expr.
op0().
type().
id()==ID_unsignedbv ||
1796 if(expr.
id()==ID_notequal)
1804 else if(expr.
id()==ID_gt)
1808 throw "bit-vector constant unexpectedly non-integer";
1822 else if(expr.
id()==ID_lt)
1830 else if(expr.
id()==ID_le)
1834 throw "bit-vector constant unexpectedly non-integer";
The type of an expression.
const typet & follow(const typet &src) const
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
const std::string & id2string(const irep_idt &d)
const mp_integer string2integer(const std::string &n, unsigned base)
bool simplify_node(exprt &expr)
constant_exprt to_expr() const
bool simplify_shifts(exprt &expr)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Deprecated expression utility functions.
bool simplify_concatenation(exprt &expr)
void copy_to_operands(const exprt &expr)
const irep_idt & get_value() const
bool simplify_inequality_pointer_object(exprt &expr)
The trinary if-then-else operator.
bool simplify_mult(exprt &expr)
A constant literal expression.
void make_bool(bool value)
bool simplify_mod(exprt &expr)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
void change_spec(const ieee_float_spect &dest_spec)
const typet & follow_tag(const union_tag_typet &src) const
bool simplify_if(if_exprt &expr)
bool simplify_inequality_constant(exprt &expr)
const irep_idt & id() const
void set_value(const irep_idt &value)
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.
#define Forall_expr(it, expr)
bool simplify_div(exprt &expr)
API to expression classes.
const irep_idt & get(const irep_namet &name) const
#define forall_value_list(it, value_list)
bool simplify_extractbits(exprt &expr)
Simplifies extracting of bits from a constant.
#define forall_operands(it, expr)
The unary minus expression.
constant_exprt to_expr() const
bool has_operands() const
The boolean constant false.
bool simplify_unary_plus(exprt &expr)
std::size_t get_width() const
bool get_values(const exprt &expr, value_listt &value_list)
bool simplify_bswap(exprt &expr)
std::vector< exprt > operandst
void follow_symbol(irept &irep) const
bool eliminate_common_addends(exprt &op0, exprt &op1)
bool is_number(const typet &type)
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
Base class for all expressions.
bool simplify_power(exprt &expr)
bool simplify_bitwise(exprt &expr)
const std::string integer2binary(const mp_integer &n, std::size_t width)
const std::string & get_string(const irep_namet &name) const
#define Forall_operands(it, expr)
bool simplify_inequality_not_constant(exprt &expr)
std::size_t integer2size_t(const mp_integer &n)
bool simplify_inequality_address_of(exprt &expr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
bool simplify_extractbit(exprt &expr)
bool simplify_minus(exprt &expr)
std::set< mp_integer > value_listt
void make_typecast(const typet &_type)
bool simplify_plus(exprt &expr)
void set(const irep_namet &name, const irep_idt &value)
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==
static bool is_bitvector_type(const typet &type)
bool simplify_bitnot(exprt &expr)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.