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());
97 lower_res.size() + upper_res.size() == dest_width,
98 "lower result bitvector size plus upper result bitvector size shall "
99 "equal the destination bitvector size");
101 dest.insert(dest.end(), upper_res.begin(), upper_res.end());
106 if(src_type.
id()==ID_complex)
109 dest_type.
id() == ID_complex,
110 "destination type shall be of complex type when source type is of "
112 if(dest_type.
id()==ID_signedbv ||
113 dest_type.
id()==ID_unsignedbv ||
114 dest_type.
id()==ID_floatbv ||
115 dest_type.
id()==ID_fixedbv ||
116 dest_type.
id()==ID_c_enum ||
117 dest_type.
id()==ID_c_enum_tag ||
118 dest_type.
id()==ID_bool)
123 tmp_src.resize(src.size()/2);
140 dest.resize(dest_width);
141 for(std::size_t i=0; i<dest.size(); i++)
152 if(dest_from==src_from)
197 src_width == dest_width,
198 "source bitvector size shall equal the destination bitvector size");
203 if(src_type.
id()==ID_bool)
214 src_width == 1,
"bitvector of type boolean shall have width one");
230 std::size_t dest_fraction_bits=
232 std::size_t dest_int_bits=dest_width-dest_fraction_bits;
233 std::size_t op_fraction_bits=
235 std::size_t op_int_bits=src_width-op_fraction_bits;
237 dest.resize(dest_width);
242 for(std::size_t i=0; i<dest_fraction_bits; i++)
245 std::size_t p=dest_fraction_bits-i-1;
247 if(i<op_fraction_bits)
248 dest[p]=src[op_fraction_bits-i-1];
253 for(std::size_t i=0; i<dest_int_bits; i++)
256 std::size_t p=dest_fraction_bits+i;
257 INVARIANT(p < dest_width,
"bit index shall be within bounds");
260 dest[p]=src[i+op_fraction_bits];
262 dest[p]=src[src_width-1];
270 src_width == dest_width,
271 "source bitvector with shall equal the destination bitvector width");
282 std::size_t dest_fraction_bits=
285 for(std::size_t i=0; i<dest_fraction_bits; i++)
288 for(std::size_t i=0; i<dest_width-dest_fraction_bits; i++)
307 else if(src_type.
id()==ID_bool)
310 std::size_t fraction_bits=
314 src_width == 1,
"bitvector of type boolean shall have width one");
316 for(std::size_t i=0; i<dest_width; i++)
319 dest.push_back(src[0]);
340 std::size_t op_fraction_bits=
343 for(std::size_t i=0; i<dest_width; i++)
345 if(i<src_width-op_fraction_bits)
346 dest.push_back(src[i+op_fraction_bits]);
350 dest.push_back(src[src_width-1]);
359 bvt fraction_bits_bv=src;
360 fraction_bits_bv.resize(op_fraction_bits);
381 for(std::size_t i=0; i<dest_width; i++)
384 dest.push_back(src[i]);
385 else if(sign_extension)
386 dest.push_back(src[src_width-1]);
396 for(std::size_t i=0; i<dest_width; i++)
398 std::size_t src_index=i*2;
400 if(src_index<src_width)
401 dest.push_back(src[src_index]);
412 for(std::size_t i=0; i<dest_width; i++)
414 std::size_t src_index=i*2;
416 if(src_index<src_width)
417 dest.push_back(src[src_index]);
419 dest.push_back(src.back());
427 if(src_type.
id()==ID_bool)
432 src_width == 1,
"bitvector of type boolean shall have width one");
434 for(std::size_t i=0; i<dest_width; i++)
437 dest.push_back(src[0]);
450 src_type.
id()==ID_bool)
452 for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
455 dest.push_back(src[j]);
466 for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
469 dest.push_back(src[j]);
471 dest.push_back(src.back());
483 if(dest_width<src_width)
484 dest.resize(dest_width);
488 while(dest.size()<dest_width)
500 src_width == dest_width,
501 "source bitvector width shall equal the destination bitvector width");
511 dest[0]=!float_utils.
is_zero(src);
521 if(dest_type.
id()==ID_array)
523 if(src_width==dest_width)
529 else if(dest_type.
id()==ID_struct)
533 if(src_type.
id()==ID_struct)
552 typedef std::map<irep_idt, std::size_t> op_mapt;
555 for(std::size_t i=0; i<op_comp.size(); i++)
556 op_map[op_comp[i].get_name()]=i;
563 std::size_t offset=dest_offsets[i];
564 std::size_t comp_width=
boolbv_width(dest_comp[i].type());
568 op_mapt::const_iterator it=
569 op_map.find(dest_comp[i].get_name());
576 for(std::size_t j=0; j<comp_width; j++)
582 if(dest_comp[i].type()!=dest_comp[it->second].type())
585 for(std::size_t j=0; j<comp_width; j++)
590 std::size_t op_offset=op_offsets[it->second];
591 for(std::size_t j=0; j<comp_width; j++)
592 dest[offset+j]=src[op_offset+j];
608 if(expr.
op().
type().
id() == ID_range)
615 else if(from==0 && to==0)