9 #ifndef CPROVER_UTIL_BITVECTOR_EXPR_H
10 #define CPROVER_UTIL_BITVECTOR_EXPR_H
22 :
unary_exprt(ID_bswap, std::move(_op), std::move(_type))
47 return base.
id() == ID_bswap;
54 value.
op().
type() == value.
type(),
"bswap type must match operand type");
92 return base.
id() == ID_bitnot;
141 return base.
id() == ID_bitor;
181 return base.
id() == ID_bitxor;
216 return base.
id() == ID_bitxnor;
256 return base.
id() == ID_bitand;
283 :
binary_exprt(std::move(_src), _id, std::move(_distance))
313 return base.
id() == ID_shl || base.
id() == ID_ashr || base.
id() == ID_lshr ||
314 base.
id() == ID_ror || base.
id() == ID_rol;
348 :
shift_exprt(std::move(_src), ID_shl, std::move(_distance))
361 return base.
id() == ID_shl;
392 :
shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
405 return base.
id() == ID_ashr;
413 :
shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
418 :
shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
426 return base.
id() == ID_lshr;
465 return base.
id() == ID_extractbit;
509 {std::move(_src), std::move(_index)})
539 return base.
id() == ID_extractbits;
582 {_src, std::move(_index), std::move(_new_value)})
633 return base.
id() == ID_update_bit;
669 {_src, std::move(_index), std::move(_new_value)})
719 return base.
id() == ID_update_bits;
780 return base.
id() == ID_replication;
820 :
multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
827 {std::move(_op0), std::move(_op1)},
836 return base.
id() == ID_concatenation;
863 :
unary_exprt(ID_popcount, std::move(_op), std::move(_type))
880 return base.
id() == ID_popcount;
921 "The kind used to construct binary_overflow_exprt should be in the set "
922 "of expected valid kinds.");
931 if(expr.
id() != ID_overflow_shl)
937 "operand types must match");
952 return id == ID_overflow_plus ||
id == ID_overflow_mult ||
953 id == ID_overflow_minus ||
id == ID_overflow_shl;
975 value, 2,
"binary overflow expression must have two operands");
987 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_mult ||
988 expr.
id() == ID_overflow_minus || expr.
id() == ID_overflow_shl);
999 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_mult ||
1000 expr.
id() == ID_overflow_minus || expr.
id() == ID_overflow_shl);
1022 return base.
id() == ID_overflow_plus;
1041 return base.
id() == ID_overflow_minus;
1060 return base.
id() == ID_overflow_mult;
1075 return base.
id() == ID_overflow_shl;
1107 return base.
id() == ID_overflow_unary_minus;
1113 value, 1,
"unary overflow expression must have one operand");
1145 return base.
id() == ID_overflow_unary_minus;
1151 value, 1,
"unary minus overflow expression must have one operand");
1187 :
unary_exprt(ID_count_leading_zeros, std::move(_op), std::move(_type))
1199 return !
get_bool(ID_C_bounds_check);
1204 set(ID_C_bounds_check, !value);
1214 "unary expression must have a single operand");
1218 "operand must be of bitvector type");
1237 return base.
id() == ID_count_leading_zeros;
1280 :
unary_exprt(ID_count_trailing_zeros, std::move(_op), std::move(_type))
1292 return !
get_bool(ID_C_bounds_check);
1297 set(ID_C_bounds_check, !value);
1307 "unary expression must have a single operand");
1311 "operand must be of bitvector type");
1330 return base.
id() == ID_count_trailing_zeros;
1381 return base.
id() == ID_bitreverse;
1417 :
binary_exprt(std::move(_lhs), ID_saturating_plus, std::move(_rhs))
1434 return base.
id() == ID_saturating_plus;
1471 :
binary_exprt(std::move(_lhs), ID_saturating_minus, std::move(_rhs))
1479 return base.
id() == ID_saturating_minus;
1520 {{ID_value, _lhs.
type()},
1522 {_lhs, std::move(_rhs)})
1526 "The kind used to construct overflow_result_exprt should be in the set "
1527 "of expected valid kinds.");
1534 {{ID_value, _op.
type()},
1540 "The kind used to construct overflow_result_exprt should be in the set "
1541 "of expected valid kinds.");
1557 if(expr.
id() != ID_overflow_result_unary_minus)
1561 expr.
id() != ID_overflow_result_unary_minus &&
1562 expr.
id() != ID_overflow_result_shl)
1568 "operand types must match");
1583 return id == ID_overflow_result_plus ||
id == ID_overflow_result_mult ||
1584 id == ID_overflow_result_minus ||
id == ID_overflow_result_shl ||
1585 id == ID_overflow_result_unary_minus;
1591 return "overflow_result-" +
id2string(kind);
1603 if(value.
id() == ID_overflow_result_unary_minus)
1606 value, 1,
"unary overflow expression must have two operands");
1611 value, 2,
"binary overflow expression must have two operands");
1645 :
unary_exprt(ID_find_first_set, std::move(_op), std::move(_type))
1661 "unary expression must have a single operand");
1665 "operand must be of bitvector type");
1684 return base.
id() == ID_find_first_set;
1725 :
unary_exprt(ID_zero_extend, std::move(_op), std::move(_type))
1736 return base.
id() == ID_zero_extend;
const update_bit_exprt & to_update_bit_expr(const exprt &expr)
Cast an exprt to an update_bit_exprt.
bool can_cast_expr< count_trailing_zeros_exprt >(const exprt &base)
const onehot_exprt & to_onehot_expr(const exprt &expr)
Cast an exprt to a onehot_exprt.
bool can_cast_expr< mult_overflow_exprt >(const exprt &base)
bool can_cast_expr< replication_exprt >(const exprt &base)
bool can_cast_expr< bswap_exprt >(const exprt &base)
bool can_cast_expr< find_first_set_exprt >(const exprt &base)
bool can_cast_expr< saturating_plus_exprt >(const exprt &base)
bool can_cast_expr< bitreverse_exprt >(const exprt &base)
bool can_cast_expr< count_leading_zeros_exprt >(const exprt &base)
bool can_cast_expr< shift_exprt >(const exprt &base)
bool can_cast_expr< bitand_exprt >(const exprt &base)
bool can_cast_expr< update_bits_exprt >(const exprt &base)
bool can_cast_expr< saturating_minus_exprt >(const exprt &base)
const overflow_result_exprt & to_overflow_result_expr(const exprt &expr)
Cast an exprt to a overflow_result_exprt.
const binary_overflow_exprt & to_binary_overflow_expr(const exprt &expr)
Cast an exprt to a binary_overflow_exprt.
bool can_cast_expr< popcount_exprt >(const exprt &base)
bool can_cast_expr< extractbits_exprt >(const exprt &base)
const onehot0_exprt & to_onehot0_expr(const exprt &expr)
Cast an exprt to a onehot0_exprt.
bool can_cast_expr< bitxor_exprt >(const exprt &base)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool can_cast_expr< bitor_exprt >(const exprt &base)
bool can_cast_expr< update_bit_exprt >(const exprt &base)
bool can_cast_expr< minus_overflow_exprt >(const exprt &base)
void validate_expr(const bswap_exprt &value)
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
bool can_cast_expr< ashr_exprt >(const exprt &base)
bool can_cast_expr< zero_extend_exprt >(const exprt &base)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const unary_overflow_exprt & to_unary_overflow_expr(const exprt &expr)
Cast an exprt to a unary_overflow_exprt.
bool can_cast_expr< shl_overflow_exprt >(const exprt &base)
bool can_cast_expr< bitxnor_exprt >(const exprt &base)
const saturating_plus_exprt & to_saturating_plus_expr(const exprt &expr)
Cast an exprt to a saturating_plus_exprt.
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
bool can_cast_expr< overflow_result_exprt >(const exprt &base)
bool can_cast_expr< concatenation_exprt >(const exprt &base)
const find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const zero_extend_exprt & to_zero_extend_expr(const exprt &expr)
Cast an exprt to a zero_extend_exprt.
bool can_cast_expr< unary_overflow_exprt >(const exprt &base)
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
bool can_cast_expr< lshr_exprt >(const exprt &base)
bool can_cast_expr< shl_exprt >(const exprt &base)
bool can_cast_expr< plus_overflow_exprt >(const exprt &base)
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
bool can_cast_expr< bitnot_exprt >(const exprt &base)
const saturating_minus_exprt & to_saturating_minus_expr(const exprt &expr)
Cast an exprt to a saturating_minus_exprt.
bool can_cast_expr< binary_overflow_exprt >(const exprt &base)
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
bool can_cast_expr< unary_minus_overflow_exprt >(const exprt &base)
bool can_cast_expr< extractbit_exprt >(const exprt &base)
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const update_bits_exprt & to_update_bits_expr(const exprt &expr)
Cast an exprt to an update_bits_exprt.
const bitxnor_exprt & to_bitxnor_expr(const exprt &expr)
Cast an exprt to a bitxnor_exprt.
ashr_exprt(exprt _src, exprt _distance)
ashr_exprt(exprt _src, const std::size_t _distance)
A base class for binary expressions.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
static bool valid_id(const irep_idt &id)
Returns true iff id is a valid identifier of a binary_overflow_exprt.
static irep_idt make_id(const irep_idt &kind)
binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
bitand_exprt(exprt::operandst _operands, typet _type)
bitand_exprt(const exprt &_op0, exprt _op1)
Bit-wise negation of bit-vectors.
bitor_exprt(exprt::operandst _operands, typet _type)
bitor_exprt(const exprt &_op0, exprt _op1)
Reverse the order of bits in a bit-vector.
bitreverse_exprt(exprt op)
exprt lower() const
Lower a bitreverse_exprt to arithmetic and logic expressions.
bitxnor_exprt(exprt _op0, exprt _op1)
bitxor_exprt(exprt::operandst _operands, typet _type)
bitxor_exprt(exprt _op0, exprt _op1)
The byte swap expression.
bswap_exprt(exprt _op, std::size_t bits_per_byte)
std::size_t get_bits_per_byte() const
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
void set_bits_per_byte(std::size_t bits_per_byte)
Concatenation of bit-vector operands.
concatenation_exprt(operandst _operands, typet _type)
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
A constant literal expression.
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
bool zero_permitted() const
void zero_permitted(bool value)
exprt lower() const
Lower a count_leading_zeros_exprt to arithmetic and logic expressions.
count_leading_zeros_exprt(const exprt &_op)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
count_leading_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
count_trailing_zeros_exprt(const exprt &_op)
bool zero_permitted() const
count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
void zero_permitted(bool value)
exprt lower() const
Lower a count_trailing_zeros_exprt to arithmetic and logic expressions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
find_first_set_exprt(exprt _op, typet _type)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
exprt lower() const
Lower a find_first_set_exprt to arithmetic and logic expressions.
find_first_set_exprt(const exprt &_op)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
bool get_bool(const irep_idt &name) const
std::size_t get_size_t(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
void set_size_t(const irep_idt &name, const std::size_t value)
const irep_idt & id() const
lshr_exprt(exprt _src, const std::size_t _distance)
lshr_exprt(exprt _src, exprt _distance)
minus_overflow_exprt(exprt _lhs, exprt _rhs)
exprt lower() const
Lower a minus_overflow_exprt to arithmetic and logic expressions.
mult_overflow_exprt(exprt _lhs, exprt _rhs)
exprt lower() const
Lower a mult_overflow_exprt to arithmetic and logic expressions.
A base class for multi-ary expressions Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
A Boolean expression returning true iff the given operand consists of exactly one '0' and '1' otherwi...
exprt lower() const
lowering to extractbit
A Boolean expression returning true iff the given operand consists of exactly one '1' and '0' otherwi...
exprt lower() const
lowering to extractbit
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
const exprt & op3() const =delete
overflow_result_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
overflow_result_exprt(exprt _op, const irep_idt &kind)
const exprt & op2() const =delete
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
static bool valid_id(const irep_idt &id)
Returns true iff id is a valid identifier of an overflow_exprt.
static irep_idt make_id(const irep_idt &kind)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
plus_overflow_exprt(exprt _lhs, exprt _rhs)
exprt lower() const
Lower a plus_overflow_exprt to arithmetic and logic expressions.
The popcount (counting the number of bits set to 1) expression.
exprt lower() const
Lower a popcount_exprt to arithmetic and logic expressions.
popcount_exprt(exprt _op, typet _type)
popcount_exprt(const exprt &_op)
const constant_exprt & times() const
replication_exprt(constant_exprt _times, exprt _src, typet _type)
Saturating subtraction expression.
saturating_minus_exprt(exprt _lhs, exprt _rhs)
The saturating plus expression.
saturating_plus_exprt(exprt _lhs, exprt _rhs, typet _type)
saturating_plus_exprt(exprt _lhs, exprt _rhs)
A base class for shift and rotate operators.
const exprt & distance() const
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
shl_exprt(exprt _src, const std::size_t _distance)
shl_exprt(exprt _src, exprt _distance)
shl_overflow_exprt(exprt _lhs, exprt _rhs)
Structure type, corresponds to C style structs.
The type of an expression, extends irept.
Generic base class for unary expressions.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
A Boolean expression returning true, iff negation would result in an overflow when applied to the (si...
unary_minus_overflow_exprt(exprt _op)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
unary_overflow_exprt(const irep_idt &kind, exprt _op)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Replaces a sub-range of a bit-vector operand.
const exprt & new_value() const
update_bit_exprt(exprt _src, exprt _index, exprt _new_value)
Replaces the bit [_index] from _src to produce a result of the same type as _src.
const exprt & src() const
exprt lower() const
A lowering to masking, shifting, or.
const exprt & index() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Replaces a sub-range of a bit-vector operand.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const exprt & src() const
const exprt & index() const
update_bits_exprt(exprt _src, exprt _index, exprt _new_value)
Replace the bits [_index .
exprt lower() const
A lowering to masking, shifting, or.
update_bits_exprt(exprt _src, const std::size_t _index, exprt _new_value)
const exprt & new_value() const
zero extension The operand is converted to the given type by either a) truncating if the new type is ...
zero_extend_exprt(exprt _op, typet _type)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
const std::string & id2string(const irep_idt &d)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...