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);
120 case bvtypet::IS_RANGE:
121 if(src_bvtype==bvtypet::IS_UNSIGNED ||
122 src_bvtype==bvtypet::IS_SIGNED ||
123 src_bvtype==bvtypet::IS_C_BOOL)
130 dest.resize(dest_width);
131 for(std::size_t i=0; i<dest.size(); i++)
137 else if(src_bvtype==bvtypet::IS_RANGE)
142 if(dest_from==src_from)
162 case bvtypet::IS_FLOAT:
168 case bvtypet::IS_FLOAT:
173 case bvtypet::IS_SIGNED:
174 case bvtypet::IS_C_ENUM:
179 case bvtypet::IS_UNSIGNED:
180 case bvtypet::IS_C_BOOL:
187 src_width == dest_width,
188 "source bitvector size shall equal the destination bitvector size");
193 case bvtypet::IS_UNKNOWN:
194 case bvtypet::IS_RANGE:
195 case bvtypet::IS_VERILOG_UNSIGNED:
196 case bvtypet::IS_VERILOG_SIGNED:
197 case bvtypet::IS_FIXED:
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]);
220 case bvtypet::IS_FIXED:
221 if(src_bvtype==bvtypet::IS_FIXED)
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];
262 else if(src_bvtype==bvtypet::IS_BV)
265 src_width == dest_width,
266 "source bitvector width shall equal the destination bitvector width");
270 else if(src_bvtype==bvtypet::IS_UNSIGNED ||
271 src_bvtype==bvtypet::IS_SIGNED ||
272 src_bvtype==bvtypet::IS_C_BOOL ||
273 src_bvtype==bvtypet::IS_C_ENUM)
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++)
291 if(src_bvtype==bvtypet::IS_SIGNED || src_bvtype==bvtypet::IS_C_ENUM)
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]);
323 case bvtypet::IS_UNSIGNED:
324 case bvtypet::IS_SIGNED:
325 case bvtypet::IS_C_ENUM:
328 case bvtypet::IS_FLOAT:
333 case bvtypet::IS_FIXED:
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]);
344 if(dest_bvtype==bvtypet::IS_SIGNED)
345 dest.push_back(src[src_width-1]);
354 bvt fraction_bits_bv=src;
355 fraction_bits_bv.resize(op_fraction_bits);
364 case bvtypet::IS_UNSIGNED:
365 case bvtypet::IS_SIGNED:
366 case bvtypet::IS_C_ENUM:
367 case bvtypet::IS_C_BOOL:
374 src_bvtype==bvtypet::IS_SIGNED || src_bvtype==bvtypet::IS_C_ENUM;
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]);
389 case bvtypet::IS_VERILOG_UNSIGNED:
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]);
405 case bvtypet::IS_VERILOG_SIGNED:
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");
428 case bvtypet::IS_RANGE:
430 case bvtypet::IS_UNKNOWN:
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]);
451 case bvtypet::IS_VERILOG_UNSIGNED:
452 if(src_bvtype==bvtypet::IS_UNSIGNED ||
453 src_bvtype==bvtypet::IS_C_BOOL ||
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]);
468 else if(src_bvtype==bvtypet::IS_SIGNED)
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());
482 else if(src_bvtype==bvtypet::IS_VERILOG_UNSIGNED)
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");
509 case bvtypet::IS_C_BOOL:
512 if(src_bvtype==bvtypet::IS_FLOAT)
515 dest[0]=!float_utils.
is_zero(src);
517 else if(src_bvtype==bvtypet::IS_C_BOOL)
525 case bvtypet::IS_UNKNOWN:
526 case bvtypet::IS_VERILOG_SIGNED:
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)