Go to the documentation of this file.
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))
336 :
shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
351 :
shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
356 :
shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
397 return base.
id() == ID_extractbit;
441 {std::move(_src), std::move(_upper), std::move(_lower)})
447 const std::size_t _upper,
448 const std::size_t _lower,
485 return base.
id() == ID_extractbits;
553 return base.
id() == ID_replication;
593 :
multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
600 {std::move(_op0), std::move(_op1)},
609 return base.
id() == ID_concatenation;
636 :
unary_exprt(ID_popcount, std::move(_op), std::move(_type))
653 return base.
id() == ID_popcount;
703 if(expr.
id() != ID_overflow_shl)
709 "operand types must match");
725 return base.
id() == ID_overflow_plus || base.
id() == ID_overflow_mult ||
726 base.
id() == ID_overflow_minus || base.
id() == ID_overflow_shl;
732 value, 2,
"binary overflow expression must have two operands");
744 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_mult ||
745 expr.
id() == ID_overflow_minus || expr.
id() == ID_overflow_shl);
756 expr.
id() == ID_overflow_plus || expr.
id() == ID_overflow_mult ||
757 expr.
id() == ID_overflow_minus || expr.
id() == ID_overflow_shl);
792 return base.
id() == ID_overflow_unary_minus;
798 value, 1,
"unary overflow expression must have one operand");
834 :
unary_exprt(ID_count_leading_zeros, std::move(_op), std::move(_type))
846 return !
get_bool(ID_C_bounds_check);
851 set(ID_C_bounds_check, !value);
861 "unary expression must have a single operand");
865 "operand must be of bitvector type");
884 return base.
id() == ID_count_leading_zeros;
927 :
unary_exprt(ID_count_trailing_zeros, std::move(_op), std::move(_type))
939 return !
get_bool(ID_C_bounds_check);
944 set(ID_C_bounds_check, !value);
954 "unary expression must have a single operand");
958 "operand must be of bitvector type");
977 return base.
id() == ID_count_trailing_zeros;
1011 #endif // CPROVER_UTIL_BITVECTOR_EXPR_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
shl_exprt(exprt _src, const std::size_t _distance)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
A base class for multi-ary expressions Associativity is not specified.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
bool can_cast_expr< bitor_exprt >(const exprt &base)
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
exprt lower() const
Lower a count_leading_zeros_exprt to arithmetic and logic expressions.
bool can_cast_expr< count_trailing_zeros_exprt >(const exprt &base)
lshr_exprt(exprt _src, exprt _distance)
bool can_cast_expr< replication_exprt >(const exprt &base)
unary_overflow_exprt(const irep_idt &kind, exprt _op)
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
bool can_cast_expr< count_leading_zeros_exprt >(const exprt &base)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
The type of an expression, extends irept.
bool can_cast_expr< shift_exprt >(const exprt &base)
bool can_cast_expr< concatenation_exprt >(const exprt &base)
exprt lower() const
Lower a count_trailing_zeros_exprt to arithmetic and logic expressions.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
exprt lower() const
Lower a popcount_exprt to arithmetic and logic expressions.
bool can_cast_expr< bitand_exprt >(const exprt &base)
bitxor_exprt(exprt _op0, exprt _op1)
bool zero_permitted() const
Base class for all expressions.
Generic base class for unary expressions.
ashr_exprt(exprt _src, exprt _distance)
A base class for binary expressions.
bswap_exprt(exprt _op, std::size_t bits_per_byte)
std::size_t get_bits_per_byte() const
Concatenation of bit-vector operands.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
replication_exprt(constant_exprt _times, exprt _src, typet _type)
bool can_cast_expr< bitnot_exprt >(const exprt &base)
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
count_trailing_zeros_exprt(const exprt &_op)
count_leading_zeros_exprt(const exprt &_op)
bool can_cast_expr< extractbit_exprt >(const exprt &base)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
void validate_expr(const bswap_exprt &value)
void zero_permitted(bool value)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool zero_permitted() const
bool get_bool(const irep_namet &name) const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const std::string & id2string(const irep_idt &d)
bitor_exprt(const exprt &_op0, exprt _op1)
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
count_leading_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define PRECONDITION(CONDITION)
void zero_permitted(bool value)
shl_exprt(exprt _src, exprt _distance)
const unary_overflow_exprt & to_unary_overflow_expr(const exprt &expr)
Cast an exprt to a unary_overflow_exprt.
concatenation_exprt(operandst _operands, typet _type)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
const irep_idt & id() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
popcount_exprt(const exprt &_op)
std::vector< exprt > operandst
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const binary_overflow_exprt & to_binary_overflow_expr(const exprt &expr)
Cast an exprt to a binary_overflow_exprt.
Bit-wise negation of bit-vectors.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
A base class for shift and rotate operators.
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 ...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
bool can_cast_expr< bitxor_exprt >(const exprt &base)
std::size_t get_size_t(const irep_namet &name) const
bitand_exprt(const exprt &_op0, exprt _op1)
bool can_cast_expr< bswap_exprt >(const exprt &base)
bool can_cast_expr< binary_overflow_exprt >(const exprt &base)
void set(const irep_namet &name, const irep_idt &value)
lshr_exprt(exprt _src, const std::size_t _distance)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
bool can_cast_expr< unary_overflow_exprt >(const exprt &base)
void set_size_t(const irep_namet &name, const std::size_t value)
bool can_cast_expr< extractbits_exprt >(const exprt &base)
void set_bits_per_byte(std::size_t bits_per_byte)
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)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
The byte swap expression.
const exprt & distance() const
count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
ashr_exprt(exprt _src, const std::size_t _distance)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
The popcount (counting the number of bits set to 1) expression.
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)
const constant_exprt & times() const
A constant literal expression.
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
API to expression classes.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
popcount_exprt(exprt _op, typet _type)
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Base class for all expressions.
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.