35 std::vector<mp_integer> bytes;
38 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
39 bytes.push_back((value >> bit)%
power(2, bits_per_byte));
43 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
45 assert(!bytes.empty());
46 new_value+=bytes.back()<<bit;
69 if(type_id==ID_integer || type_id==ID_natural)
76 else if(type_id==ID_rational)
85 else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
93 else if(type_id==ID_fixedbv)
101 else if(type_id==ID_floatbv)
123 if(type_id==ID_integer || type_id==ID_natural)
130 else if(type_id==ID_rational)
139 else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
148 else if(type_id==ID_fixedbv)
155 else if(type_id==ID_floatbv)
179 exprt::operandst::iterator constant;
187 for(exprt::operandst::iterator it=operands.begin();
197 it->type().id()!=ID_floatbv)
204 bool do_erase =
false;
207 if(it->is_constant() && it->type()==expr.
type())
210 if(c_sizeof_type.
is_nil())
212 static_cast<const typet &>(it->find(ID_C_c_sizeof_type));
231 it=operands.erase(it);
241 constant->set(ID_C_c_sizeof_type, c_sizeof_type);
244 if(operands.size()==1)
246 exprt product(operands.front());
254 if(found && constant->is_one())
257 operands.erase(constant);
260 if(operands.size()==1)
262 exprt product(operands.front());
281 if(expr_type!=expr.
op0().
type() ||
285 if(expr_type.
id()==ID_signedbv ||
286 expr_type.
id()==ID_unsignedbv ||
287 expr_type.
id()==ID_natural ||
288 expr_type.
id()==ID_integer)
297 if(ok1 && int_value1==0)
301 if(ok1 && int_value1==1)
310 if(ok0 && int_value0==0)
330 else if(expr_type.
id()==ID_rational)
338 if(ok1 && rat_value1.
is_zero())
341 if((ok1 && rat_value1.
is_one()) ||
362 else if(expr_type.
id()==ID_fixedbv)
399 if(expr.
type().
id()==ID_signedbv ||
400 expr.
type().
id()==ID_unsignedbv ||
401 expr.
type().
id()==ID_natural ||
402 expr.
type().
id()==ID_integer)
413 if(ok1 && int_value1==0)
416 if((ok1 && int_value1==1) ||
417 (ok0 && int_value0==0))
443 expr.
type().
id()!=ID_pointer)
450 assert(expr.
id()==ID_plus);
460 exprt::operandst::iterator next=it;
463 if(next!=operands.end())
465 if(it->type()==next->type() &&
470 operands.erase(next);
478 if(expr.
type().
id()==ID_pointer &&
480 expr.
op0().
id()==ID_plus &&
501 if(
is_number(it->type()) && it->is_constant())
507 exprt::operandst::iterator const_sum;
508 bool const_sum_set=
false;
512 if(
is_number(it->type()) && it->is_constant())
525 assert(it->is_not_nil());
535 typedef std::unordered_map<exprt, exprt::operandst::iterator, irep_hash>
540 if(it->id()==ID_unary_minus &&
541 it->operands().size()==1)
542 expr_map.insert(std::make_pair(it->op0(), it));
549 else if(it->id()==ID_unary_minus)
552 expr_mapt::iterator itm=expr_map.find(*it);
554 if(itm!=expr_map.end())
558 assert(it->is_not_nil());
567 for(exprt::operandst::iterator
572 if(
is_number(it->type()) && it->is_zero())
574 it=operands.erase(it);
588 else if(operands.size()==1)
590 exprt tmp(operands.front());
601 expr.
type().
id()!=ID_pointer)
606 assert(expr.
id()==ID_minus);
608 if(operands.size()!=2)
625 else if(expr.
type().
id()==ID_pointer &&
626 operands[0].type().id()==ID_pointer &&
640 operands[0].type().id()==ID_pointer &&
641 operands[1].type().id()==ID_pointer)
645 if(operands[0]==operands[1])
663 if(expr.
type().
id()!=ID_bool)
669 if(it->id()==ID_typecast &&
670 it->operands().size()==1 &&
671 ns.
follow(it->op0().type()).
id()==ID_bool)
674 else if(it->is_zero() || it->is_one())
686 if(expr.
id()==ID_bitand)
688 else if(expr.
id()==ID_bitor)
690 else if(expr.
id()==ID_bitxor)
697 if(it->id()==ID_typecast)
703 else if(it->is_zero())
705 else if(it->is_one())
746 std::string new_value;
747 new_value.resize(width);
749 if(expr.
id()==ID_bitand)
751 for(std::size_t i=0; i<width; i++)
752 new_value[i]=(a_str[i]==
'1' && b_str[i]==
'1')?
'1':
'0';
754 else if(expr.
id()==ID_bitor)
756 for(std::size_t i=0; i<width; i++)
757 new_value[i]=(a_str[i]==
'1' || b_str[i]==
'1')?
'1':
'0';
759 else if(expr.
id()==ID_bitxor)
761 for(std::size_t i=0; i<width; i++)
762 new_value[i]=((a_str[i]==
'1')!=(b_str[i]==
'1'))?
'1':
'0';
778 if(expr.
id()==ID_bitor || expr.
id()==ID_bitxor)
780 for(exprt::operandst::iterator
785 if(it->is_zero() && expr.
operands().size()>1)
797 if(expr.
id()==ID_bitand)
799 for(exprt::operandst::iterator
804 if(it->is_constant() &&
822 if(expr.
id()==ID_bitand || expr.
id()==ID_bitor)
829 else if(expr.
id()==ID_bitxor)
873 if(value.
size()!=width)
914 const std::string new_value=
916 opi.
set(ID_value, new_value);
917 opi.
type().
set(ID_width, new_value.size());
926 else if(expr.
type().
id()==ID_verilog_unsignedbv)
938 (opi.
type().
id()==ID_verilog_unsignedbv ||
940 (opn.
type().
id()==ID_verilog_unsignedbv ||
944 const std::string new_value=
946 opi.
set(ID_value, new_value);
947 opi.
type().
set(ID_width, new_value.size());
948 opi.
type().
id(ID_verilog_unsignedbv);
996 if(expr.
op0().
type().
id()==ID_unsignedbv ||
1002 if(expr.
id()==ID_lshr)
1010 else if(distance>=0)
1012 value/=
power(2, distance);
1017 else if(expr.
id()==ID_ashr)
1027 else if(expr.
id()==ID_shl)
1035 else if(distance>=0)
1037 value*=
power(2, distance);
1043 else if(expr.
op0().
type().
id()==ID_integer ||
1046 if(expr.
id()==ID_lshr)
1050 value/=
power(2, distance);
1055 else if(expr.
id()==ID_ashr)
1061 if(value<0 && new_value==0)
1068 else if(expr.
id()==ID_shl)
1072 value*=
power(2, distance);
1123 if(start < 0 || start >= width || end < 0 || end >= width)
1128 "extractbits must have upper() >= lower()");
1134 if(value.
size()!=width)
1139 std::string extracted_value =
1149 else if(expr.
src().
id() == ID_concatenation)
1162 if(start + 1 == offset && end + op_width == offset)
1202 if(operand.
id()==ID_unary_minus)
1216 else if(operand.
id()==ID_constant)
1220 if(type_id==ID_integer ||
1221 type_id==ID_signedbv ||
1222 type_id==ID_unsignedbv)
1238 else if(type_id==ID_rational)
1247 else if(type_id==ID_fixedbv)
1254 else if(type_id==ID_floatbv)
1273 if(operands.size()!=1)
1276 exprt &op=operands.front();
1278 if(expr.
type().
id()==ID_bv ||
1279 expr.
type().
id()==ID_unsignedbv ||
1280 expr.
type().
id()==ID_signedbv)
1284 if(op.
id()==ID_constant)
1288 for(
auto &ch : value)
1289 ch=(ch==
'0')?
'1':
'0';
1305 if(expr.
type().
id()!=ID_bool)
1308 if(operands.size()!=2)
1319 if((expr.
id()==ID_equal || expr.
id()==ID_notequal) &&
1327 if(tmp0.
id()==ID_if && tmp0.
operands().size()==3)
1339 if((tmp0.
id()==ID_address_of ||
1340 (tmp0.
id()==ID_typecast && tmp0.
op0().
id()==ID_address_of)) &&
1341 (tmp1.
id()==ID_address_of ||
1342 (tmp1.
id()==ID_typecast && tmp1.
op0().
id()==ID_address_of)) &&
1343 (expr.
id()==ID_equal || expr.
id()==ID_notequal))
1346 if(tmp0.
id()==ID_pointer_object &&
1347 tmp1.
id()==ID_pointer_object &&
1348 (expr.
id()==ID_equal || expr.
id()==ID_notequal))
1354 if(tmp0.
type().
id()==ID_c_enum_tag)
1357 if(tmp1.
type().
id()==ID_c_enum_tag)
1364 if(tmp0_const && tmp1_const)
1366 if(expr.
id() == ID_equal || expr.
id() == ID_notequal)
1369 bool equal = (tmp0_const->get_value() == tmp1_const->get_value());
1370 expr.
make_bool(expr.
id() == ID_equal ? equal : !equal);
1374 if(tmp0.
type().
id() == ID_fixedbv)
1379 if(expr.
id() == ID_ge)
1381 else if(expr.
id()==ID_le)
1383 else if(expr.
id()==ID_gt)
1385 else if(expr.
id()==ID_lt)
1392 else if(tmp0.
type().
id()==ID_floatbv)
1397 if(expr.
id() == ID_ge)
1399 else if(expr.
id()==ID_le)
1401 else if(expr.
id()==ID_gt)
1403 else if(expr.
id()==ID_lt)
1410 else if(tmp0.
type().
id()==ID_rational)
1420 if(expr.
id() == ID_ge)
1422 else if(expr.
id()==ID_le)
1424 else if(expr.
id()==ID_gt)
1426 else if(expr.
id()==ID_lt)
1443 if(expr.
id() == ID_ge)
1445 else if(expr.
id()==ID_le)
1447 else if(expr.
id()==ID_gt)
1449 else if(expr.
id()==ID_lt)
1461 if(expr.
id()==ID_ge)
1463 else if(expr.
id()==ID_le)
1465 else if(expr.
id()==ID_gt)
1467 else if(expr.
id()==ID_lt)
1501 if(op0.
id()==ID_plus)
1511 else if(op1.
id()==ID_plus)
1524 op0.
type().
id()!=ID_complex)
1547 if(expr.
id()==ID_notequal)
1555 else if(expr.
id()==ID_gt)
1565 else if(expr.
id()==ID_lt)
1573 else if(expr.
id()==ID_le)
1584 assert(expr.
id()==ID_ge || expr.
id()==ID_equal);
1588 if(operands.front()==operands.back())
1616 if(expr.
id()==ID_ge)
1617 tmp=(int_value0>=int_value1);
1618 else if(expr.
id()==ID_equal)
1619 tmp=(int_value0==int_value1);
1631 else if(result!=tmp)
1647 if(expr.
id()==ID_equal)
1682 if(expr.
id()==ID_notequal)
1692 if(expr.
id()==ID_equal &&
1694 expr.
op1().
get(ID_value)==ID_NULL)
1698 if(expr.
op0().
id()==ID_address_of &&
1701 if(expr.
op0().
op0().
id()==ID_symbol ||
1702 expr.
op0().
op0().
id()==ID_dynamic_object ||
1703 expr.
op0().
op0().
id()==ID_member ||
1705 expr.
op0().
op0().
id()==ID_string_constant)
1711 else if(expr.
op0().
id()==ID_typecast &&
1714 expr.
op0().
op0().
id()==ID_address_of &&
1727 else if(expr.
op0().
id()==ID_typecast &&
1752 if(expr.
op0().
id()==ID_plus)
1756 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1763 if(it->is_constant())
1770 assert(it->is_not_nil());
1795 if(expr.
op0().
id()==ID_typecast &&
1804 ieee_floatt const_val_converted_back=const_val_converted;
1807 if(const_val_converted_back==const_val)
1822 if(expr.
id()==ID_ge &&
1832 if(expr.
id()==ID_equal)
1835 if(operand.
id()==ID_unary_minus)
1844 else if(operand.
id()==ID_plus)
1852 if(operand.
op0().
id()==ID_unary_minus)
1855 if(operand.
op1().
id()==ID_unary_minus &&
1860 tmp.op0().swap(operand.
op0());
1861 tmp.op1().swap(operand.
op1().
op0());
1871 if(expr.
op0().
id()==ID_typecast &&
1891 #define NORMALISE_CONSTANT_TESTS 1892 #ifdef NORMALISE_CONSTANT_TESTS 1894 if(expr.
op0().
type().
id()==ID_unsignedbv ||
1900 if(expr.
id()==ID_notequal)
1908 else if(expr.
id()==ID_gt)
1912 throw "bit-vector constant unexpectedly non-integer";
1926 else if(expr.
id()==ID_lt)
1934 else if(expr.
id()==ID_le)
1938 throw "bit-vector constant unexpectedly non-integer";
The type of an expression.
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)
const std::string integer2string(const mp_integer &n, unsigned base)
bool simplify_node(exprt &expr)
constant_exprt to_expr() const
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
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
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
bool simplify_inequality_pointer_object(exprt &expr)
The trinary if-then-else operator.
bool simplify_mult(exprt &expr)
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
A constant literal expression.
void make_bool(bool value)
bool simplify_mod(exprt &expr)
const typet & follow_tag(const union_tag_typet &) const
void change_spec(const ieee_float_spect &dest_spec)
bool simplify_bswap(bswap_exprt &expr)
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.
#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)
#define forall_operands(it, expr)
const typet & follow(const typet &) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
The unary minus expression.
static bool mul_expr(constant_exprt &dest, const constant_exprt &expr)
produce a product of two expressions of the same type
constant_exprt to_expr() const
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
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)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
std::vector< exprt > operandst
bool eliminate_common_addends(exprt &op0, exprt &op1)
bool is_number(const typet &type)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
bool simplify_unary_minus(exprt &expr)
std::size_t get_bits_per_byte() const
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)
bool simplify_extractbit(exprt &expr)
bool simplify_minus(exprt &expr)
std::set< mp_integer > value_listt
#define DATA_INVARIANT(CONDITION, REASON)
static bool sum_expr(constant_exprt &dest, const constant_exprt &expr)
produce a sum of two constant expressions of the same type
void make_typecast(const typet &_type)
The byte swap expression.
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)
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.
bool simplify_extractbits(extractbits_exprt &expr)
Simplifies extracting of bits from a constant.