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;
136 return base.
id() == ID_bitor;
171 return base.
id() == ID_bitxor;
206 return base.
id() == ID_bitand;
233 :
binary_exprt(std::move(_src), _id, std::move(_distance))
263 return base.
id() == ID_shl || base.
id() == ID_ashr || base.
id() == ID_lshr ||
264 base.
id() == ID_ror || base.
id() == ID_rol;
298 :
shift_exprt(std::move(_src), ID_shl, std::move(_distance))
311 return base.
id() == ID_shl;
342 :
shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
355 return base.
id() == ID_ashr;
363 :
shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
368 :
shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
376 return base.
id() == ID_lshr;
415 return base.
id() == ID_extractbit;
459 {std::move(_src), std::move(_index)})
489 return base.
id() == ID_extractbits;
532 {_src, std::move(_index), std::move(_new_value)})
583 return base.
id() == ID_update_bit;
619 {_src, std::move(_index), std::move(_new_value)})
669 return base.
id() == ID_update_bits;
730 return base.
id() == ID_replication;
770 :
multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
777 {std::move(_op0), std::move(_op1)},
786 return base.
id() == ID_concatenation;
813 :
unary_exprt(ID_popcount, std::move(_op), std::move(_type))
830 return base.
id() == ID_popcount;
871 "The kind used to construct binary_overflow_exprt should be in the set "
872 "of expected valid kinds.");
881 if(expr.
id() != ID_overflow_shl)
887 "operand types must match");
902 return id == ID_overflow_plus ||
id == ID_overflow_mult ||
903 id == ID_overflow_minus ||
id == ID_overflow_shl;
925 value, 2,
"binary overflow expression must have two operands");
937 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_mult ||
938 expr.
id() == ID_overflow_minus || expr.
id() == ID_overflow_shl);
949 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_mult ||
950 expr.
id() == ID_overflow_minus || expr.
id() == ID_overflow_shl);
972 return base.
id() == ID_overflow_plus;
991 return base.
id() == ID_overflow_minus;
1010 return base.
id() == ID_overflow_mult;
1025 return base.
id() == ID_overflow_shl;
1057 return base.
id() == ID_overflow_unary_minus;
1063 value, 1,
"unary overflow expression must have one operand");
1095 return base.
id() == ID_overflow_unary_minus;
1101 value, 1,
"unary minus overflow expression must have one operand");
1137 :
unary_exprt(ID_count_leading_zeros, std::move(_op), std::move(_type))
1149 return !
get_bool(ID_C_bounds_check);
1154 set(ID_C_bounds_check, !value);
1164 "unary expression must have a single operand");
1168 "operand must be of bitvector type");
1187 return base.
id() == ID_count_leading_zeros;
1230 :
unary_exprt(ID_count_trailing_zeros, std::move(_op), std::move(_type))
1242 return !
get_bool(ID_C_bounds_check);
1247 set(ID_C_bounds_check, !value);
1257 "unary expression must have a single operand");
1261 "operand must be of bitvector type");
1280 return base.
id() == ID_count_trailing_zeros;
1331 return base.
id() == ID_bitreverse;
1367 :
binary_exprt(std::move(_lhs), ID_saturating_plus, std::move(_rhs))
1384 return base.
id() == ID_saturating_plus;
1421 :
binary_exprt(std::move(_lhs), ID_saturating_minus, std::move(_rhs))
1429 return base.
id() == ID_saturating_minus;
1470 {{ID_value, _lhs.
type()},
1472 {_lhs, std::move(_rhs)})
1476 "The kind used to construct overflow_result_exprt should be in the set "
1477 "of expected valid kinds.");
1484 {{ID_value, _op.
type()},
1490 "The kind used to construct overflow_result_exprt should be in the set "
1491 "of expected valid kinds.");
1507 if(expr.
id() != ID_overflow_result_unary_minus)
1511 expr.
id() != ID_overflow_result_unary_minus &&
1512 expr.
id() != ID_overflow_result_shl)
1518 "operand types must match");
1533 return id == ID_overflow_result_plus ||
id == ID_overflow_result_mult ||
1534 id == ID_overflow_result_minus ||
id == ID_overflow_result_shl ||
1535 id == ID_overflow_result_unary_minus;
1541 return "overflow_result-" +
id2string(kind);
1553 if(value.
id() == ID_overflow_result_unary_minus)
1556 value, 1,
"unary overflow expression must have two operands");
1561 value, 2,
"binary overflow expression must have two operands");
1595 :
unary_exprt(ID_find_first_set, std::move(_op), std::move(_type))
1611 "unary expression must have a single operand");
1615 "operand must be of bitvector type");
1634 return base.
id() == ID_find_first_set;
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)
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)
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)
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)
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.
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.
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(const exprt &_op0, exprt _op1)
Bit-wise negation of bit-vectors.
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.
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...
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)
update_bit_exprt(exprt _src, const std::size_t _index, exprt _new_value)
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
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,...