9#ifndef CPROVER_UTIL_BITVECTOR_EXPR_H
10#define CPROVER_UTIL_BITVECTOR_EXPR_H
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;
185 return base.
id() == ID_bitnor;
225 return base.
id() == ID_bitxor;
269 return base.
id() == ID_bitxnor;
311 return base.
id() == ID_bitand;
355 return base.
id() == ID_bitnand;
412 return base.
id() == ID_shl || base.
id() == ID_ashr || base.
id() == ID_lshr ||
413 base.
id() == ID_ror || base.
id() == ID_rol;
460 return base.
id() == ID_shl;
504 return base.
id() == ID_ashr;
525 return base.
id() == ID_lshr;
564 return base.
id() == ID_extractbit;
608 {std::move(_src), std::move(_index)})
638 return base.
id() == ID_extractbits;
681 {_src, std::move(_index), std::move(_new_value)})
732 return base.
id() == ID_update_bit;
768 {_src, std::move(_index), std::move(_new_value)})
818 return base.
id() == ID_update_bits;
879 return base.
id() == ID_replication;
926 {std::move(_op0), std::move(_op1)},
935 return base.
id() == ID_concatenation;
979 return base.
id() == ID_popcount;
1020 "The kind used to construct binary_overflow_exprt should be in the set "
1021 "of expected valid kinds.");
1030 if(expr.
id() != ID_overflow_shl)
1036 "operand types must match");
1051 return id == ID_overflow_plus ||
id == ID_overflow_mult ||
1052 id == ID_overflow_minus ||
id == ID_overflow_shl;
1074 value, 2,
"binary overflow expression must have two operands");
1086 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_mult ||
1087 expr.
id() == ID_overflow_minus || expr.
id() == ID_overflow_shl);
1098 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_mult ||
1099 expr.
id() == ID_overflow_minus || expr.
id() == ID_overflow_shl);
1121 return base.
id() == ID_overflow_plus;
1140 return base.
id() == ID_overflow_minus;
1159 return base.
id() == ID_overflow_mult;
1174 return base.
id() == ID_overflow_shl;
1206 return base.
id() == ID_overflow_unary_minus;
1212 value, 1,
"unary overflow expression must have one operand");
1244 return base.
id() == ID_overflow_unary_minus;
1250 value, 1,
"unary minus overflow expression must have one operand");
1298 return !
get_bool(ID_C_bounds_check);
1303 set(ID_C_bounds_check, !value);
1313 "unary expression must have a single operand");
1317 "operand must be of bitvector type");
1336 return base.
id() == ID_count_leading_zeros;
1391 return !
get_bool(ID_C_bounds_check);
1396 set(ID_C_bounds_check, !value);
1406 "unary expression must have a single operand");
1410 "operand must be of bitvector type");
1429 return base.
id() == ID_count_trailing_zeros;
1480 return base.
id() == ID_bitreverse;
1533 return base.
id() == ID_saturating_plus;
1578 return base.
id() == ID_saturating_minus;
1619 {{ID_value, _lhs.
type()},
1621 {_lhs, std::move(_rhs)})
1625 "The kind used to construct overflow_result_exprt should be in the set "
1626 "of expected valid kinds.");
1633 {{ID_value, _op.
type()},
1639 "The kind used to construct overflow_result_exprt should be in the set "
1640 "of expected valid kinds.");
1656 if(expr.
id() != ID_overflow_result_unary_minus)
1660 expr.
id() != ID_overflow_result_unary_minus &&
1661 expr.
id() != ID_overflow_result_shl)
1667 "operand types must match");
1682 return id == ID_overflow_result_plus ||
id == ID_overflow_result_mult ||
1683 id == ID_overflow_result_minus ||
id == ID_overflow_result_shl ||
1684 id == ID_overflow_result_unary_minus;
1690 return "overflow_result-" +
id2string(kind);
1702 if(value.
id() == ID_overflow_result_unary_minus)
1705 value, 1,
"unary overflow expression must have two operands");
1710 value, 2,
"binary overflow expression must have two operands");
1760 "unary expression must have a single operand");
1764 "operand must be of bitvector type");
1783 return base.
id() == ID_find_first_set;
1835 return base.
id() == ID_zero_extend;
bool can_cast_expr< count_trailing_zeros_exprt >(const exprt &base)
const bitxnor_exprt & to_bitxnor_expr(const exprt &expr)
Cast an exprt to a bitxnor_exprt.
const onehot0_exprt & to_onehot0_expr(const exprt &expr)
Cast an exprt to a onehot0_exprt.
const saturating_minus_exprt & to_saturating_minus_expr(const exprt &expr)
Cast an exprt to a saturating_minus_exprt.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const saturating_plus_exprt & to_saturating_plus_expr(const exprt &expr)
Cast an exprt to a saturating_plus_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)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const bitnand_exprt & to_bitnand_expr(const exprt &expr)
Cast an exprt to a bitnand_exprt.
bool can_cast_expr< find_first_set_exprt >(const exprt &base)
bool can_cast_expr< saturating_plus_exprt >(const exprt &base)
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
bool can_cast_expr< bitreverse_exprt >(const exprt &base)
bool can_cast_expr< count_leading_zeros_exprt >(const exprt &base)
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.
bool can_cast_expr< bitnand_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 extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
bool can_cast_expr< popcount_exprt >(const exprt &base)
const onehot_exprt & to_onehot_expr(const exprt &expr)
Cast an exprt to a onehot_exprt.
bool can_cast_expr< extractbits_exprt >(const exprt &base)
bool can_cast_expr< bitxor_exprt >(const exprt &base)
const binary_overflow_exprt & to_binary_overflow_expr(const exprt &expr)
Cast an exprt to a binary_overflow_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 find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
bool can_cast_expr< ashr_exprt >(const exprt &base)
bool can_cast_expr< zero_extend_exprt >(const exprt &base)
bool can_cast_expr< shl_overflow_exprt >(const exprt &base)
bool can_cast_expr< bitxnor_exprt >(const exprt &base)
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_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)
const update_bit_exprt & to_update_bit_expr(const exprt &expr)
Cast an exprt to an update_bit_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const unary_overflow_exprt & to_unary_overflow_expr(const exprt &expr)
Cast an exprt to a unary_overflow_exprt.
const bitnor_exprt & to_bitnor_expr(const exprt &expr)
Cast an exprt to a bitnor_exprt.
bool can_cast_expr< concatenation_exprt >(const exprt &base)
bool can_cast_expr< unary_overflow_exprt >(const exprt &base)
const overflow_result_exprt & to_overflow_result_expr(const exprt &expr)
Cast an exprt to a overflow_result_exprt.
bool can_cast_expr< lshr_exprt >(const exprt &base)
bool can_cast_expr< shl_exprt >(const exprt &base)
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
bool can_cast_expr< plus_overflow_exprt >(const exprt &base)
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
bool can_cast_expr< bitnot_exprt >(const exprt &base)
bool can_cast_expr< binary_overflow_exprt >(const exprt &base)
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
bool can_cast_expr< unary_minus_overflow_exprt >(const exprt &base)
bool can_cast_expr< extractbit_exprt >(const exprt &base)
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
bool can_cast_expr< bitnor_exprt >(const exprt &base)
const zero_extend_exprt & to_zero_extend_expr(const exprt &expr)
Cast an exprt to a zero_extend_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
ashr_exprt(exprt _src, exprt _distance)
ashr_exprt(exprt _src, const std::size_t _distance)
A base class for binary expressions.
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
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)
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
bitand_exprt(exprt::operandst _operands, typet _type)
bitand_exprt(const exprt &_op0, exprt _op1)
bitnand_exprt(exprt _op0, exprt _op1)
bitnand_exprt(exprt::operandst _operands, typet _type)
bitnor_exprt(exprt::operandst _operands, typet _type)
bitnor_exprt(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::operandst _operands, typet _type)
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.
expr_protectedt(irep_idt _id, typet _type)
Base class for all expressions.
std::vector< exprt > operandst
static void check(const exprt &, const validation_modet)
Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are ...
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.
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
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...
overflow_result_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
overflow_result_exprt(exprt _op, const irep_idt &kind)
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.
const exprt & op2() const =delete
static irep_idt make_id(const irep_idt &kind)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const exprt & op3() const =delete
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.
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
const exprt & distance() const
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.
unary_exprt(const irep_idt &_id, const exprt &_op)
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)
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Replaces a sub-range of a bit-vector operand.
const exprt & src() const
const exprt & index() 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.
exprt lower() const
A lowering to masking, shifting, or.
const exprt & new_value() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Replaces a sub-range of a bit-vector operand.
const exprt & index() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
update_bits_exprt(exprt _src, exprt _index, exprt _new_value)
Replace the bits [_index .
const exprt & new_value() const
exprt lower() const
A lowering to masking, shifting, or.
const exprt & src() const
update_bits_exprt(exprt _src, const std::size_t _index, exprt _new_value)
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)
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
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.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...