33 const typet &src_type,
35 const typet &dest_type,
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)
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());
93 lower_res.size() + upper_res.size() == dest_width,
94 "lower result bitvector size plus upper result bitvector size shall "
95 "equal the destination bitvector size");
97 dest.insert(dest.end(), upper_res.begin(), upper_res.end());
102 if(src_type.
id() == ID_complex)
105 dest_type.
id() == ID_complex,
106 "destination type shall be of complex type when source type is of "
109 dest_type.
id() == ID_signedbv || dest_type.
id() == ID_unsignedbv ||
110 dest_type.
id() == ID_floatbv || dest_type.
id() == ID_fixedbv ||
111 dest_type.
id() == ID_c_enum || dest_type.
id() == ID_c_enum_tag ||
112 dest_type.
id() == ID_bool)
117 tmp_src.resize(src.size() / 2);
135 dest.resize(dest_width);
136 for(std::size_t i = 0; i < dest.size(); i++)
147 if(dest_from == src_from)
150 dest =
bv_utils.zero_extension(src, dest_width);
158 bv_utils.zero_extension(src, dest_width),
159 bv_utils.build_constant(offset, dest_width));
190 INVARIANT(src_width >= dest_width,
"cannot extend bv-typed bitvector");
192 if(dest_width < src_width)
193 dest.resize(dest_width);
202 if(src_type.
id() == ID_bool)
211 src_width == 1,
"bitvector of type boolean shall have width one");
213 for(
auto &literal : dest)
214 literal =
prop.land(literal, src[0]);
227 std::size_t dest_fraction_bits =
229 std::size_t dest_int_bits = dest_width - dest_fraction_bits;
230 std::size_t op_fraction_bits =
232 std::size_t op_int_bits = src_width - op_fraction_bits;
234 dest.resize(dest_width);
239 for(std::size_t i = 0; i < dest_fraction_bits; i++)
242 std::size_t p = dest_fraction_bits - i - 1;
244 if(i < op_fraction_bits)
245 dest[p] = src[op_fraction_bits - i - 1];
250 for(std::size_t i = 0; i < dest_int_bits; i++)
253 std::size_t p = dest_fraction_bits + i;
254 INVARIANT(p < dest_width,
"bit index shall be within bounds");
257 dest[p] = src[i + op_fraction_bits];
259 dest[p] = src[src_width - 1];
266 INVARIANT(src_width >= dest_width,
"cannot extend bv-typed bitvector");
268 if(dest_width < src_width)
269 dest.resize(dest_width);
278 std::size_t dest_fraction_bits =
281 for(std::size_t i = 0; i < dest_fraction_bits; i++)
284 for(std::size_t i = 0; i < dest_width - dest_fraction_bits; i++)
295 l = src[src_width - 1];
305 else if(src_type.
id() == ID_bool)
308 std::size_t fraction_bits =
312 src_width == 1,
"bitvector of type boolean shall have width one");
314 for(std::size_t i = 0; i < dest_width; i++)
316 if(i == fraction_bits)
317 dest.push_back(src[0]);
339 std::size_t op_fraction_bits =
342 for(std::size_t i = 0; i < dest_width; i++)
344 if(i < src_width - op_fraction_bits)
345 dest.push_back(src[i + op_fraction_bits]);
349 dest.push_back(src[src_width - 1]);
358 bvt fraction_bits_bv = src;
359 fraction_bits_bv.resize(op_fraction_bits);
362 dest =
bv_utils.incrementer(dest, round_up);
376 bool sign_extension =
379 for(std::size_t i = 0; i < dest_width; i++)
382 dest.push_back(src[i]);
383 else if(sign_extension)
384 dest.push_back(src[src_width - 1]);
394 for(std::size_t i = 0; i < dest_width; i++)
396 std::size_t src_index = i * 2;
398 if(src_index < src_width)
399 dest.push_back(src[src_index]);
410 for(std::size_t i = 0; i < dest_width; i++)
412 std::size_t src_index = i * 2;
414 if(src_index < src_width)
415 dest.push_back(src[src_index]);
417 dest.push_back(src.back());
425 INVARIANT(src_width >= dest_width,
"cannot extend bv-typed bitvector");
427 if(dest_width < src_width)
428 dest.resize(dest_width);
434 if(src_type.
id() == ID_bool)
439 src_width == 1,
"bitvector of type boolean shall have width one");
441 for(std::size_t i = 0; i < dest_width; i++)
444 dest.push_back(src[0]);
458 src_type.
id() == ID_bool)
460 for(std::size_t i = 0, j = 0; i < dest_width; i += 2, j++)
463 dest.push_back(src[j]);
474 for(std::size_t i = 0, j = 0; i < dest_width; i += 2, j++)
477 dest.push_back(src[j]);
479 dest.push_back(src.back());
491 if(dest_width < src_width)
492 dest.resize(dest_width);
496 while(dest.size() < dest_width)
507 INVARIANT(src_width >= dest_width,
"cannot extend bv-typed bitvector");
509 if(dest_width < src_width)
510 dest.resize(dest_width);
519 dest[0] = !float_utils.
is_zero(src);
531 if(dest_type.
id() == ID_array)
533 if(src_width == dest_width)
539 else if(dest_type.
id() == ID_struct || dest_type.
id() == ID_struct_tag)
542 dest_type.
id() == ID_struct_tag
546 if(src_type.
id() == ID_struct || src_type.
id() == ID_struct_tag)
553 src_type.
id() == ID_struct_tag
566 typedef std::map<irep_idt, std::size_t> op_mapt;
569 for(std::size_t i = 0; i < op_comp.size(); i++)
570 op_map[op_comp[i].get_name()] = i;
573 for(std::size_t i = 0; i < dest_comp.size(); i++)
575 std::size_t offset = dest_offsets[i];
576 std::size_t comp_width =
boolbv_width(dest_comp[i].type());
580 op_mapt::const_iterator it = op_map.find(dest_comp[i].get_name());
582 if(it == op_map.end())
587 for(std::size_t j = 0; j < comp_width; j++)
588 dest[offset + j] =
prop.new_variable();
593 if(dest_comp[i].type() != dest_comp[it->second].type())
596 for(std::size_t j = 0; j < comp_width; j++)
597 dest[offset + j] =
prop.new_variable();
601 std::size_t op_offset = op_offsets[it->second];
602 for(std::size_t j = 0; j < comp_width; j++)
603 dest[offset + j] = src[op_offset + j];