18 #include "../floatbv/float_utils.h" 36 const typet &src_type,
const bvt &src,
58 std::size_t src_width=src.size();
61 if(dest_width==0 || src_width==0)
65 dest.reserve(dest_width);
67 if(dest_type.
id()==ID_complex)
69 if(src_type==dest_type.
subtype())
75 for(std::size_t i=src.size(); i<dest_width; i++)
80 else if(src_type.
id()==ID_complex)
83 bvt lower, upper, lower_res, upper_res;
84 lower.assign(src.begin(), src.begin()+src.size()/2);
85 upper.assign(src.begin()+src.size()/2, src.end());
96 assert(lower_res.size()+upper_res.size()==dest_width);
98 dest.insert(dest.end(), upper_res.begin(), upper_res.end());
103 if(src_type.
id()==ID_complex)
105 assert(dest_type.
id()!=ID_complex);
106 if(dest_type.
id()==ID_signedbv ||
107 dest_type.
id()==ID_unsignedbv ||
108 dest_type.
id()==ID_floatbv ||
109 dest_type.
id()==ID_fixedbv ||
110 dest_type.
id()==ID_c_enum ||
111 dest_type.
id()==ID_c_enum_tag ||
112 dest_type.
id()==ID_bool)
117 tmp_src.resize(src.size()/2);
134 dest.resize(dest_width);
135 for(std::size_t i=0; i<dest.size(); i++)
146 if(dest_from==src_from)
190 assert(src_width==dest_width);
195 if(src_type.
id()==ID_bool)
205 assert(src_width==1);
221 std::size_t dest_fraction_bits=
223 std::size_t dest_int_bits=dest_width-dest_fraction_bits;
224 std::size_t op_fraction_bits=
226 std::size_t op_int_bits=src_width-op_fraction_bits;
228 dest.resize(dest_width);
233 for(std::size_t i=0; i<dest_fraction_bits; i++)
236 std::size_t p=dest_fraction_bits-i-1;
238 if(i<op_fraction_bits)
239 dest[p]=src[op_fraction_bits-i-1];
244 for(std::size_t i=0; i<dest_int_bits; i++)
247 std::size_t p=dest_fraction_bits+i;
248 assert(p<dest_width);
251 dest[p]=src[i+op_fraction_bits];
253 dest[p]=src[src_width-1];
260 assert(src_width==dest_width);
271 std::size_t dest_fraction_bits=
274 for(std::size_t i=0; i<dest_fraction_bits; i++)
277 for(std::size_t i=0; i<dest_width-dest_fraction_bits; i++)
296 else if(src_type.
id()==ID_bool)
299 std::size_t fraction_bits=
302 assert(src_width==1);
304 for(std::size_t i=0; i<dest_width; i++)
307 dest.push_back(src[0]);
328 std::size_t op_fraction_bits=
331 for(std::size_t i=0; i<dest_width; i++)
333 if(i<src_width-op_fraction_bits)
334 dest.push_back(src[i+op_fraction_bits]);
338 dest.push_back(src[src_width-1]);
347 bvt fraction_bits_bv=src;
348 fraction_bits_bv.resize(op_fraction_bits);
369 for(std::size_t i=0; i<dest_width; i++)
372 dest.push_back(src[i]);
373 else if(sign_extension)
374 dest.push_back(src[src_width-1]);
384 for(std::size_t i=0; i<dest_width; i++)
386 std::size_t src_index=i*2;
388 if(src_index<src_width)
389 dest.push_back(src[src_index]);
400 for(std::size_t i=0; i<dest_width; i++)
402 std::size_t src_index=i*2;
404 if(src_index<src_width)
405 dest.push_back(src[src_index]);
407 dest.push_back(src.back());
415 if(src_type.
id()==ID_bool)
419 assert(src_width==1);
421 for(std::size_t i=0; i<dest_width; i++)
424 dest.push_back(src[0]);
437 src_type.
id()==ID_bool)
439 for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
442 dest.push_back(src[j]);
453 for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
456 dest.push_back(src[j]);
458 dest.push_back(src.back());
470 if(dest_width<src_width)
471 dest.resize(dest_width);
475 while(dest.size()<dest_width)
486 assert(src_width==dest_width);
496 dest[0]=!float_utils.
is_zero(src);
506 if(dest_type.
id()==ID_array)
508 if(src_width==dest_width)
514 else if(dest_type.
id()==ID_struct)
518 if(src_type.
id()==ID_struct)
539 typedef std::map<irep_idt, std::size_t> op_mapt;
542 for(std::size_t i=0; i<op_comp.size(); i++)
543 op_map[op_comp[i].get_name()]=i;
550 std::size_t offset=dest_offsets[i];
551 std::size_t comp_width=
boolbv_width(dest_comp[i].type());
555 op_mapt::const_iterator it=
556 op_map.find(dest_comp[i].get_name());
563 for(std::size_t j=0; j<comp_width; j++)
569 if(dest_comp[i].type()!=dest_comp[it->second].type())
572 for(std::size_t j=0; j<comp_width; j++)
577 std::size_t op_offset=op_offsets[it->second];
578 for(std::size_t j=0; j<comp_width; j++)
579 dest[offset+j]=src[op_offset+j];
604 else if(from==0 && to==0)
The type of an expression.
std::vector< std::size_t > offset_mapt
const typet & follow(const typet &src) const
const mp_integer string2integer(const std::string &n, unsigned base)
constant_exprt to_expr() const
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
boolbv_widtht boolbv_width
std::vector< componentt > componentst
virtual literalt lor(literalt a, literalt b)=0
const componentst & components() const
const range_typet & to_range_type(const typet &type)
Cast a generic typet to a range_typet.
void build_offset_map(const struct_typet &src, offset_mapt &dest)
literalt is_zero(const bvt &op)
#define forall_literals(it, bv)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
virtual const bvt & convert_bv(const exprt &expr)
std::size_t get_fraction_bits() const
void conversion_failed(const exprt &expr, bvt &bv)
literalt is_zero(const bvt &)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
bvtypet get_bvtype(const typet &type)
bvt zero_extension(const bvt &bv, std::size_t new_size)
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
bvt incrementer(const bvt &op, literalt carry_in)
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
literalt const_literal(bool value)
bvt add(const bvt &op0, const bvt &op1)
bvt from_unsigned_integer(const bvt &)
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Base class for all expressions.
const std::string & get_string(const irep_namet &name) const
virtual literalt convert_rest(const exprt &expr)
void from_integer(const mp_integer &i)
bvt from_signed_integer(const bvt &)
const typet & subtype() const
std::vector< literalt > bvt
bvt build_constant(const mp_integer &i, std::size_t width)
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
mp_integer get_from() const