35 const mp_integer value = numeric_cast_v<mp_integer>(expr.
op());
36 std::vector<mp_integer> bytes;
39 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
40 bytes.push_back((value >> bit)%
power(2, bits_per_byte));
44 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
48 "bytes is not empty because we just pushed just as many elements on " 49 "top of it as we are popping now");
50 new_value+=bytes.back()<<bit;
74 type_id == ID_integer || type_id == ID_natural ||
75 type_id == ID_unsignedbv || type_id == ID_signedbv)
84 else if(type_id==ID_rational)
93 else if(type_id==ID_fixedbv)
100 else if(type_id==ID_floatbv)
123 type_id == ID_integer || type_id == ID_natural ||
124 type_id == ID_unsignedbv || type_id == ID_signedbv)
133 else if(type_id==ID_rational)
142 else if(type_id==ID_fixedbv)
149 else if(type_id==ID_floatbv)
173 exprt::operandst::iterator constant;
176 bool constant_found =
false;
181 for(exprt::operandst::iterator it=operands.begin();
191 it->type().id()!=ID_floatbv)
198 bool do_erase =
false;
201 if(it->is_constant() && it->type()==expr.
type())
204 if(c_sizeof_type.
is_nil())
206 static_cast<const typet &>(it->find(ID_C_c_sizeof_type));
218 constant_found =
true;
225 it=operands.erase(it);
236 "c_sizeof_type is only set to a non-nil value " 237 "if a constant has been found");
238 constant->set(ID_C_c_sizeof_type, c_sizeof_type);
241 if(operands.size()==1)
243 exprt product(operands.front());
251 if(constant_found && constant->is_one())
254 operands.erase(constant);
257 if(operands.size()==1)
259 exprt product(operands.front());
278 if(expr_type!=expr.
op0().
type() ||
282 if(expr_type.
id()==ID_signedbv ||
283 expr_type.
id()==ID_unsignedbv ||
284 expr_type.
id()==ID_natural ||
285 expr_type.
id()==ID_integer)
294 if(ok1 && int_value1==0)
298 if(ok1 && int_value1==1)
307 if(ok0 && int_value0==0)
327 else if(expr_type.
id()==ID_rational)
335 if(ok1 && rat_value1.
is_zero())
338 if((ok1 && rat_value1.
is_one()) ||
359 else if(expr_type.
id()==ID_fixedbv)
396 if(expr.
type().
id()==ID_signedbv ||
397 expr.
type().
id()==ID_unsignedbv ||
398 expr.
type().
id()==ID_natural ||
399 expr.
type().
id()==ID_integer)
410 if(ok1 && int_value1==0)
413 if((ok1 && int_value1==1) ||
414 (ok0 && int_value0==0))
440 if(!
is_number(plus_expr.type()) && plus_expr.type().id() != ID_pointer)
450 if(
ns.
follow(plus_expr.type()).
id() == ID_floatbv)
455 exprt::operandst::iterator next=it;
458 if(next!=operands.end())
460 if(it->type()==next->type() &&
465 operands.erase(next);
474 plus_expr.type().id() == ID_pointer && plus_expr.operands().size() == 2 &&
475 plus_expr.op0().id() == ID_plus && plus_expr.op0().operands().size() == 2)
479 if(plus_expr.op0().op1().id() == ID_plus)
495 if(
is_number(it->type()) && it->is_constant())
501 exprt::operandst::iterator const_sum;
502 bool const_sum_set=
false;
506 if(
is_number(it->type()) && it->is_constant())
529 typedef std::unordered_map<exprt, exprt::operandst::iterator, irep_hash>
534 if(it->id()==ID_unary_minus &&
535 it->operands().size()==1)
536 expr_map.insert(std::make_pair(it->op0(), it));
543 else if(it->id()==ID_unary_minus)
546 expr_mapt::iterator itm=expr_map.find(*it);
548 if(itm!=expr_map.end())
561 for(exprt::operandst::iterator
566 if(
is_number(it->type()) && it->is_zero())
568 it=operands.erase(it);
582 else if(operands.size()==1)
584 exprt tmp(operands.front());
595 if(!
is_number(minus_expr.type()) && minus_expr.type().id() != ID_pointer)
600 if(operands.size()!=2)
611 plus_exprt plus_expr(operands[0], rhs_negated);
614 expr.
swap(plus_expr);
618 minus_expr.type().id() == ID_pointer &&
619 operands[0].type().id() == ID_pointer &&
is_number(operands[1].type()))
625 plus_exprt pointer_offset_expr(operands[0], negated_pointer_offset);
628 expr.
swap(pointer_offset_expr);
632 is_number(minus_expr.type()) && operands[0].type().id() == ID_pointer &&
633 operands[1].type().id() == ID_pointer)
637 if(operands[0]==operands[1])
655 if(expr.
type().
id()!=ID_bool)
661 if(it->id()==ID_typecast &&
662 it->operands().size()==1 &&
663 ns.
follow(it->op0().type()).
id()==ID_bool)
666 else if(it->is_zero() || it->is_one())
678 if(expr.
id()==ID_bitand)
680 else if(expr.
id()==ID_bitor)
682 else if(expr.
id()==ID_bitxor)
689 if(it->id()==ID_typecast)
695 else if(it->is_zero())
697 else if(it->is_one())
735 std::function<bool(
bool,
bool)> f;
737 if(expr.
id()==ID_bitand)
738 f = [](
bool a,
bool b) {
return a && b; };
739 else if(expr.
id()==ID_bitor)
740 f = [](
bool a,
bool b) {
return a || b; };
741 else if(expr.
id()==ID_bitxor)
742 f = [](
bool a,
bool b) {
return a != b; };
747 make_bvrep(width, [&a_val, &b_val, &width, &f](std::size_t i) {
763 if(expr.
id()==ID_bitor || expr.
id()==ID_bitxor)
765 for(exprt::operandst::iterator
770 if(it->is_zero() && expr.
operands().size()>1)
782 if(expr.
id()==ID_bitand)
784 const auto all_ones =
power(2, width) - 1;
785 for(exprt::operandst::iterator
809 if(expr.
id()==ID_bitand || expr.
id()==ID_bitor)
816 else if(expr.
id()==ID_bitxor)
840 const typet &src_type = extractbit_expr.src().type();
847 const auto index_converted_to_int =
848 numeric_cast<mp_integer>(extractbit_expr.index());
850 !index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
851 *index_converted_to_int >= src_bit_width)
856 if(!extractbit_expr.src().is_constant())
862 numeric_cast_v<std::size_t>(*index_converted_to_int));
881 const bool value = op.
is_true();
905 const auto new_width = width_i + width_n;
908 new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
914 opi.
type().
set(ID_width, new_width);
923 else if(expr.
type().
id()==ID_verilog_unsignedbv)
935 (opi.
type().
id()==ID_verilog_unsignedbv ||
937 (opn.
type().
id()==ID_verilog_unsignedbv ||
941 const std::string new_value=
943 opi.
set(ID_value, new_value);
944 opi.
type().
set(ID_width, new_value.size());
945 opi.
type().
id(ID_verilog_unsignedbv);
993 if(expr.
op0().
type().
id()==ID_unsignedbv ||
999 if(expr.
id()==ID_lshr)
1007 else if(distance>=0)
1009 value/=
power(2, distance);
1014 else if(expr.
id()==ID_ashr)
1024 else if(expr.
id()==ID_shl)
1032 else if(distance>=0)
1034 value*=
power(2, distance);
1040 else if(expr.
op0().
type().
id()==ID_integer ||
1043 if(expr.
id()==ID_lshr)
1047 value/=
power(2, distance);
1052 else if(expr.
id()==ID_ashr)
1058 if(value<0 && new_value==0)
1065 else if(expr.
id()==ID_shl)
1069 value*=
power(2, distance);
1120 if(!width.has_value())
1123 if(start < 0 || start >= (*width) || end < 0 || end >= (*width))
1128 "extractbits must have upper() >= lower()");
1134 if(!svalue.has_value() || svalue->size() != *width)
1137 std::string extracted_value = svalue->substr(
1138 numeric_cast_v<std::size_t>(end),
1139 numeric_cast_v<std::size_t>(start - end + 1));
1149 else if(expr.
src().
id() == ID_concatenation)
1159 if(!op_width.has_value() || *op_width <= 0)
1162 if(start + 1 == offset && end + *op_width == offset)
1172 offset -= *op_width;
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 const auto &type = expr.
type();
1281 type.id() == ID_bv || type.id() == ID_unsignedbv ||
1282 type.id() == ID_signedbv)
1286 if(op.
type() == type)
1288 if(op.
id()==ID_constant)
1291 const auto new_value =
1292 make_bvrep(width, [&value, &width](std::size_t i) {
1309 if(expr.
type().
id()!=ID_bool)
1312 if(operands.size()!=2)
1323 if((expr.
id()==ID_equal || expr.
id()==ID_notequal) &&
1331 if(tmp0.
id()==ID_if && tmp0.
operands().size()==3)
1343 if((tmp0.
id()==ID_address_of ||
1344 (tmp0.
id()==ID_typecast && tmp0.
op0().
id()==ID_address_of)) &&
1345 (tmp1.
id()==ID_address_of ||
1346 (tmp1.
id()==ID_typecast && tmp1.
op0().
id()==ID_address_of)) &&
1347 (expr.
id()==ID_equal || expr.
id()==ID_notequal))
1350 if(tmp0.
id()==ID_pointer_object &&
1351 tmp1.
id()==ID_pointer_object &&
1352 (expr.
id()==ID_equal || expr.
id()==ID_notequal))
1358 if(tmp0.
type().
id()==ID_c_enum_tag)
1361 if(tmp1.
type().
id()==ID_c_enum_tag)
1364 const auto tmp0_const = expr_try_dynamic_cast<constant_exprt>(tmp0);
1365 const auto tmp1_const = expr_try_dynamic_cast<constant_exprt>(tmp1);
1368 if(tmp0_const && tmp1_const)
1370 if(expr.
id() == ID_equal || expr.
id() == ID_notequal)
1373 bool equal = (tmp0_const->get_value() == tmp1_const->get_value());
1374 expr.
make_bool(expr.
id() == ID_equal ? equal : !equal);
1378 if(tmp0.
type().
id() == ID_fixedbv)
1383 if(expr.
id() == ID_ge)
1385 else if(expr.
id()==ID_le)
1387 else if(expr.
id()==ID_gt)
1389 else if(expr.
id()==ID_lt)
1396 else if(tmp0.
type().
id()==ID_floatbv)
1401 if(expr.
id() == ID_ge)
1403 else if(expr.
id()==ID_le)
1405 else if(expr.
id()==ID_gt)
1407 else if(expr.
id()==ID_lt)
1414 else if(tmp0.
type().
id()==ID_rational)
1424 if(expr.
id() == ID_ge)
1426 else if(expr.
id()==ID_le)
1428 else if(expr.
id()==ID_gt)
1430 else if(expr.
id()==ID_lt)
1447 if(expr.
id() == ID_ge)
1449 else if(expr.
id()==ID_le)
1451 else if(expr.
id()==ID_gt)
1453 else if(expr.
id()==ID_lt)
1465 if(expr.
id()==ID_ge)
1467 else if(expr.
id()==ID_le)
1469 else if(expr.
id()==ID_gt)
1471 else if(expr.
id()==ID_lt)
1505 if(op0.
id()==ID_plus)
1515 else if(op1.
id()==ID_plus)
1528 op0.
type().
id()!=ID_complex)
1551 if(expr.
id()==ID_notequal)
1559 else if(expr.
id()==ID_gt)
1569 else if(expr.
id()==ID_lt)
1577 else if(expr.
id()==ID_le)
1589 expr.
id() == ID_ge || expr.
id() == ID_equal,
1590 "we previously converted all other cases to >= or ==");
1594 if(operands.front()==operands.back())
1622 if(expr.
id()==ID_ge)
1623 tmp=(int_value0>=int_value1);
1624 else if(expr.
id()==ID_equal)
1625 tmp=(int_value0==int_value1);
1637 else if(result!=tmp)
1653 if(expr.
id()==ID_equal)
1688 if(expr.
id()==ID_notequal)
1698 if(expr.
id()==ID_equal &&
1700 expr.
op1().
get(ID_value)==ID_NULL)
1704 if(expr.
op0().
id()==ID_address_of &&
1707 if(expr.
op0().
op0().
id()==ID_symbol ||
1708 expr.
op0().
op0().
id()==ID_dynamic_object ||
1709 expr.
op0().
op0().
id()==ID_member ||
1711 expr.
op0().
op0().
id()==ID_string_constant)
1717 else if(expr.
op0().
id()==ID_typecast &&
1720 expr.
op0().
op0().
id()==ID_address_of &&
1733 else if(expr.
op0().
id()==ID_typecast &&
1758 if(expr.
op0().
id()==ID_plus)
1762 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1769 if(it->is_constant())
1800 if(expr.
op0().
id()==ID_typecast &&
1809 ieee_floatt const_val_converted_back=const_val_converted;
1812 if(const_val_converted_back==const_val)
1827 if(expr.
id()==ID_ge &&
1837 if(expr.
id()==ID_equal)
1840 if(operand.
id()==ID_unary_minus)
1849 else if(operand.
id()==ID_plus)
1857 if(operand.
op0().
id()==ID_unary_minus)
1860 if(operand.
op1().
id()==ID_unary_minus &&
1865 tmp.op0().swap(operand.
op0());
1866 tmp.op1().swap(operand.
op1().
op0());
1876 if(expr.
op0().
id()==ID_typecast &&
1895 #define NORMALISE_CONSTANT_TESTS 1896 #ifdef NORMALISE_CONSTANT_TESTS 1898 if(expr.
op0().
type().
id()==ID_unsignedbv ||
1904 if(expr.
id()==ID_notequal)
1912 else if(expr.
id()==ID_gt)
1928 else if(expr.
id()==ID_lt)
1936 else if(expr.
id()==ID_le)
The type of an expression, extends irept.
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
const std::string & id2string(const irep_idt &d)
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
bool simplify_node(exprt &expr)
constant_exprt to_expr() const
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
bool simplify_shifts(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 is_false() const
Return whether the expression is a constant representing false.
const irep_idt & get_value() const
bool simplify_inequality_pointer_object(exprt &expr)
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.
A constant literal expression.
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
#define CHECK_RETURN(CONDITION)
bool simplify_mod(exprt &expr)
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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)
Expression classes for byte-level operators.
The Boolean constant true.
#define Forall_expr(it, expr)
bool simplify_div(exprt &expr)
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
API to expression classes.
const irep_idt & get(const irep_namet &name) const
#define forall_value_list(it, value_list)
#define PRECONDITION(CONDITION)
#define forall_operands(it, expr)
The plus expression Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
exprt bits2expr(const std::string &bits, const typet &type, bool little_endian)
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 an exprt to a constant_exprt.
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.
std::vector< exprt > operandst
bool eliminate_common_addends(exprt &op0, exprt &op1)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a 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)
#define UNREACHABLE
This should be used to mark dead code.
The NIL type, i.e., an invalid type, no value.
const std::string & get_string(const irep_namet &name) const
#define Forall_operands(it, expr)
bool is_zero() const
Return whether the expression is a constant representing 0.
optionalt< std::string > expr2bits(const exprt &, bool little_endian)
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
bool simplify_inequality_not_constant(exprt &expr)
bool simplify_inequality_address_of(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
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
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)
Create a typecast_exprt to the given type.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
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)
bool is_one() const
Return whether the expression is a constant representing 1.
bool simplify_extractbits(extractbits_exprt &expr)
Simplifies extracting of bits from a constant.