33 const typet &src_type,
const bvt &src,
55 std::size_t src_width=src.size();
58 if(dest_width==0 || src_width==0)
62 dest.reserve(dest_width);
64 if(dest_type.
id()==ID_complex)
66 if(src_type==dest_type.
subtype())
68 dest.insert(dest.end(), src.begin(), src.end());
71 for(std::size_t i=src.size(); i<dest_width; i++)
76 else if(src_type.
id()==ID_complex)
79 bvt lower, upper, lower_res, upper_res;
80 lower.assign(src.begin(), src.begin()+src.size()/2);
81 upper.assign(src.begin()+src.size()/2, src.end());
87 lower_res.size() + upper_res.size() == dest_width,
88 "lower result bitvector size plus upper result bitvector size shall "
89 "equal the destination bitvector size");
91 dest.insert(dest.end(), upper_res.begin(), upper_res.end());
96 if(src_type.
id()==ID_complex)
99 dest_type.
id() == ID_complex,
100 "destination type shall be of complex type when source type is of "
102 if(dest_type.
id()==ID_signedbv ||
103 dest_type.
id()==ID_unsignedbv ||
104 dest_type.
id()==ID_floatbv ||
105 dest_type.
id()==ID_fixedbv ||
106 dest_type.
id()==ID_c_enum ||
107 dest_type.
id()==ID_c_enum_tag ||
108 dest_type.
id()==ID_bool)
113 tmp_src.resize(src.size()/2);
130 dest.resize(dest_width);
131 for(std::size_t i=0; i<dest.size(); i++)
142 if(dest_from==src_from)
187 src_width == dest_width,
188 "source bitvector size shall equal the destination bitvector size");
198 if(src_type.
id()==ID_bool)
209 src_width == 1,
"bitvector of type boolean shall have width one");
211 for(
auto &literal : dest)
212 literal =
prop.
land(literal, src[0]);
225 std::size_t dest_fraction_bits=
227 std::size_t dest_int_bits=dest_width-dest_fraction_bits;
228 std::size_t op_fraction_bits=
230 std::size_t op_int_bits=src_width-op_fraction_bits;
232 dest.resize(dest_width);
237 for(std::size_t i=0; i<dest_fraction_bits; i++)
240 std::size_t p=dest_fraction_bits-i-1;
242 if(i<op_fraction_bits)
243 dest[p]=src[op_fraction_bits-i-1];
248 for(std::size_t i=0; i<dest_int_bits; i++)
251 std::size_t p=dest_fraction_bits+i;
252 INVARIANT(p < dest_width,
"bit index shall be within bounds");
255 dest[p]=src[i+op_fraction_bits];
257 dest[p]=src[src_width-1];
265 src_width == dest_width,
266 "source bitvector width shall equal the destination bitvector width");
277 std::size_t dest_fraction_bits=
280 for(std::size_t i=0; i<dest_fraction_bits; i++)
283 for(std::size_t i=0; i<dest_width-dest_fraction_bits; i++)
302 else if(src_type.
id()==ID_bool)
305 std::size_t fraction_bits=
309 src_width == 1,
"bitvector of type boolean shall have width one");
311 for(std::size_t i=0; i<dest_width; i++)
314 dest.push_back(src[0]);
335 std::size_t op_fraction_bits=
338 for(std::size_t i=0; i<dest_width; i++)
340 if(i<src_width-op_fraction_bits)
341 dest.push_back(src[i+op_fraction_bits]);
345 dest.push_back(src[src_width-1]);
354 bvt fraction_bits_bv=src;
355 fraction_bits_bv.resize(op_fraction_bits);
376 for(std::size_t i=0; i<dest_width; i++)
379 dest.push_back(src[i]);
380 else if(sign_extension)
381 dest.push_back(src[src_width-1]);
391 for(std::size_t i=0; i<dest_width; i++)
393 std::size_t src_index=i*2;
395 if(src_index<src_width)
396 dest.push_back(src[src_index]);
407 for(std::size_t i=0; i<dest_width; i++)
409 std::size_t src_index=i*2;
411 if(src_index<src_width)
412 dest.push_back(src[src_index]);
414 dest.push_back(src.back());
423 src_width == dest_width,
424 "source bitvector width shall equal the destination bitvector width");
431 if(src_type.
id() == ID_bool)
436 src_width == 1,
"bitvector of type boolean shall have width one");
438 for(std::size_t i = 0; i < dest_width; i++)
441 dest.push_back(src[0]);
454 src_type.
id()==ID_bool)
456 for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
459 dest.push_back(src[j]);
470 for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
473 dest.push_back(src[j]);
475 dest.push_back(src.back());
487 if(dest_width<src_width)
488 dest.resize(dest_width);
492 while(dest.size()<dest_width)
504 src_width == dest_width,
505 "source bitvector width shall equal the destination bitvector width");
515 dest[0]=!float_utils.
is_zero(src);
527 if(dest_type.
id()==ID_array)
529 if(src_width==dest_width)
535 else if(
ns.
follow(dest_type).
id() == ID_struct)
558 typedef std::map<irep_idt, std::size_t> op_mapt;
561 for(std::size_t i=0; i<op_comp.size(); i++)
562 op_map[op_comp[i].get_name()]=i;
569 std::size_t offset=dest_offsets[i];
570 std::size_t comp_width=
boolbv_width(dest_comp[i].type());
574 op_mapt::const_iterator it=
575 op_map.find(dest_comp[i].get_name());
582 for(std::size_t j=0; j<comp_width; j++)
588 if(dest_comp[i].type()!=dest_comp[it->second].type())
591 for(std::size_t j=0; j<comp_width; j++)
596 std::size_t op_offset=op_offsets[it->second];
597 for(std::size_t j=0; j<comp_width; j++)
598 dest[offset+j]=src[op_offset+j];
614 if(expr.
op().
type().
id() == ID_range)
621 else if(from==0 && to==0)
Pre-defined bitvector types.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
bvtypet get_bvtype(const typet &type)
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
offset_mapt build_offset_map(const struct_typet &src)
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
virtual std::size_t boolbv_width(const typet &type) const
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
std::vector< std::size_t > offset_mapt
bvt add(const bvt &op0, const bvt &op1)
bvt zero_extension(const bvt &bv, std::size_t new_size)
static bvt build_constant(const mp_integer &i, std::size_t width)
literalt is_zero(const bvt &op)
bvt incrementer(const bvt &op, literalt carry_in)
Base class for all expressions.
typet & type()
Return the type of the expression.
std::size_t get_fraction_bits() const
bvt from_unsigned_integer(const bvt &)
bvt from_signed_integer(const bvt &)
literalt is_zero(const bvt &)
constant_exprt to_expr() const
void from_integer(const mp_integer &i)
const std::string & get_string(const irep_namet &name) const
const irep_idt & id() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
virtual literalt convert_rest(const exprt &expr)
virtual literalt land(literalt a, literalt b)=0
virtual literalt new_variable()=0
virtual literalt lor(literalt a, literalt b)=0
mp_integer get_from() const
Structure type, corresponds to C style structs.
const componentst & components() const
std::vector< componentt > componentst
Semantic type conversion.
The type of an expression, extends irept.
const typet & subtype() const
std::vector< literalt > bvt
literalt const_literal(bool value)
const mp_integer string2integer(const std::string &n, unsigned base)
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.