24 std::size_t old_size = bv0.size();
25 std::size_t new_size = old_size * 2;
28 const bvt &bv0_extended = bv_utils.extension(bv0, new_size, rep);
29 const bvt &bv1_extended = bv_utils.extension(bv1, new_size, rep);
31 bvt result_extended = bv_utils.multiplier(bv0_extended, bv1_extended, rep);
32 bvt bv{result_extended.begin(), result_extended.begin() + old_size};
33 bvt bv_overflow{result_extended.begin() + old_size, result_extended.end()};
37 bv.push_back(prop.
lor(bv_overflow));
42 bv_overflow.push_back(bv.back());
47 bv.push_back(!prop.
lor(all_one, all_zero));
62 std::size_t old_size = bv0.size();
63 std::size_t new_size = old_size * 2;
65 bvt result_extended = bv_utils.shift(
66 bv_utils.extension(bv0, new_size, rep0),
69 bvt bv{result_extended.begin(), result_extended.begin() + old_size};
70 bvt bv_overflow{result_extended.begin() + old_size, result_extended.end()};
75 : bv_utils.sign_bit(bv1);
78 std::size_t cmp_width = std::max(bv1.size(),
address_bits(old_size) + 1);
80 bv_utils.extension(bv1, cmp_width, rep1),
82 bv_utils.build_constant(old_size, cmp_width),
88 bv.push_back(prop.
lor(bv_overflow));
93 bv_overflow.push_back(bv.back());
97 !prop.
lequal(bv_utils.sign_bit(bv0), bv_utils.sign_bit(bv));
103 bv.push_back(prop.
lor(sign_change, !prop.
lor(all_one, all_zero)));
109 prop.
land(!neg_shift, prop.
lselect(undef, prop.
lor(bv0), bv.back()));
120 ? std::optional<std::size_t>{bv0.size()}
130 if(bv0.size() != bv1.size())
133 return bv_utils.overflow_add(bv0, bv1, rep);
137 if(bv0.size() != bv1.size())
140 return bv_utils.overflow_sub(bv0, bv1, rep);
153 mult_overflow->lhs().type() == mult_overflow->rhs().type(),
154 "operands of overflow_mult expression shall have same type");
181 const auto unary_minus_overflow =
186 return bv_utils.overflow_negate(bv);
197 if(expr.
id() == ID_overflow_result_unary_minus)
201 bv.push_back(
bv_utils.overflow_negate(op_bv));
205 else if(expr.
operands().size() != 2)
217 if(expr.
id() == ID_overflow_result_plus)
230 bv.push_back(
prop.land(sign_the_same,
prop.lxor(new_sign, old_sign)));
242 for(std::size_t i = 0; i < bv0.size(); i++)
243 bv.push_back(
bv_utils.full_adder(bv0[i], bv1[i], carry, carry));
251 else if(expr.
id() == ID_overflow_result_minus)
270 bv.push_back(
prop.lselect(
273 prop.land(sign_the_same,
prop.lxor(new_sign, old_sign))));
285 for(std::size_t i = 0; i < bv0.size(); i++)
286 bv.push_back(
bv_utils.full_adder(bv0[i], !bv1[i], carry, carry));
288 bv.push_back(!carry);
296 else if(expr.
id() == ID_overflow_result_mult)
305 else if(expr.
id() == ID_overflow_result_shl)
API to expression classes for bitvectors.
Pre-defined bitvector types.
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
static bvt shl_overflow_result(propt &prop, const bvt &bv0, const bvt &bv1, bv_utilst::representationt rep0, bv_utilst::representationt rep1)
static bvt mult_overflow_result(propt &prop, const bvt &bv0, const bvt &bv1, bv_utilst::representationt rep)
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
virtual literalt convert_binary_overflow(const binary_overflow_exprt &expr)
virtual bvt convert_overflow_result(const overflow_result_exprt &expr)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
virtual literalt convert_unary_overflow(const unary_overflow_exprt &expr)
virtual std::size_t boolbv_width(const typet &type) const
typet & type()
Return the type of the expression.
const irep_idt & id() const
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
virtual literalt convert_rest(const exprt &expr)
virtual literalt land(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)=0
The type of an expression, extends irept.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
std::vector< literalt > bvt
literalt const_literal(bool value)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...