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)
The type of an expression, extends irept.
std::vector< std::size_t > offset_mapt
Semantic type conversion.
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
typet & type()
Return the type of the expression.
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
literalt is_zero(const bvt &op)
Structure type, corresponds to C style structs.
#define forall_literals(it, bv)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
std::size_t get_fraction_bits() const
offset_mapt build_offset_map(const struct_typet &src)
void conversion_failed(const exprt &expr, bvt &bv)
literalt is_zero(const bvt &)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_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)
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 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.
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 c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
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