34 const typet &src_type,
const bvt &src,
56 std::size_t src_width=src.size();
59 if(dest_width==0 || src_width==0)
63 dest.reserve(dest_width);
65 if(dest_type.
id()==ID_complex)
69 dest.insert(dest.end(), src.begin(), src.end());
72 for(std::size_t i=src.size(); i<dest_width; i++)
77 else if(src_type.
id()==ID_complex)
80 bvt lower, upper, lower_res, upper_res;
81 lower.assign(src.begin(), src.begin()+src.size()/2);
82 upper.assign(src.begin()+src.size()/2, src.end());
94 lower_res.size() + upper_res.size() == dest_width,
95 "lower result bitvector size plus upper result bitvector size shall "
96 "equal the destination bitvector size");
98 dest.insert(dest.end(), upper_res.begin(), upper_res.end());
103 if(src_type.
id()==ID_complex)
106 dest_type.
id() == ID_complex,
107 "destination type shall be of complex type when source type is of "
109 if(dest_type.
id()==ID_signedbv ||
110 dest_type.
id()==ID_unsignedbv ||
111 dest_type.
id()==ID_floatbv ||
112 dest_type.
id()==ID_fixedbv ||
113 dest_type.
id()==ID_c_enum ||
114 dest_type.
id()==ID_c_enum_tag ||
115 dest_type.
id()==ID_bool)
120 tmp_src.resize(src.size()/2);
138 dest.resize(dest_width);
139 for(std::size_t i=0; i<dest.size(); i++)
150 if(dest_from==src_from)
195 src_width == dest_width,
196 "source bitvector size shall equal the destination bitvector size");
206 if(src_type.
id()==ID_bool)
217 src_width == 1,
"bitvector of type boolean shall have width one");
219 for(
auto &literal : dest)
220 literal =
prop.
land(literal, src[0]);
233 std::size_t dest_fraction_bits=
235 std::size_t dest_int_bits=dest_width-dest_fraction_bits;
236 std::size_t op_fraction_bits=
238 std::size_t op_int_bits=src_width-op_fraction_bits;
240 dest.resize(dest_width);
245 for(std::size_t i=0; i<dest_fraction_bits; i++)
248 std::size_t p=dest_fraction_bits-i-1;
250 if(i<op_fraction_bits)
251 dest[p]=src[op_fraction_bits-i-1];
256 for(std::size_t i=0; i<dest_int_bits; i++)
259 std::size_t p=dest_fraction_bits+i;
260 INVARIANT(p < dest_width,
"bit index shall be within bounds");
263 dest[p]=src[i+op_fraction_bits];
265 dest[p]=src[src_width-1];
273 src_width == dest_width,
274 "source bitvector width shall equal the destination bitvector width");
285 std::size_t dest_fraction_bits=
288 for(std::size_t i=0; i<dest_fraction_bits; i++)
291 for(std::size_t i=0; i<dest_width-dest_fraction_bits; i++)
310 else if(src_type.
id()==ID_bool)
313 std::size_t fraction_bits=
317 src_width == 1,
"bitvector of type boolean shall have width one");
319 for(std::size_t i=0; i<dest_width; i++)
322 dest.push_back(src[0]);
343 std::size_t op_fraction_bits=
346 for(std::size_t i=0; i<dest_width; i++)
348 if(i<src_width-op_fraction_bits)
349 dest.push_back(src[i+op_fraction_bits]);
353 dest.push_back(src[src_width-1]);
362 bvt fraction_bits_bv=src;
363 fraction_bits_bv.resize(op_fraction_bits);
384 for(std::size_t i=0; i<dest_width; i++)
387 dest.push_back(src[i]);
388 else if(sign_extension)
389 dest.push_back(src[src_width-1]);
399 for(std::size_t i=0; i<dest_width; i++)
401 std::size_t src_index=i*2;
403 if(src_index<src_width)
404 dest.push_back(src[src_index]);
415 for(std::size_t i=0; i<dest_width; i++)
417 std::size_t src_index=i*2;
419 if(src_index<src_width)
420 dest.push_back(src[src_index]);
422 dest.push_back(src.back());
431 src_width == dest_width,
432 "source bitvector width shall equal the destination bitvector width");
439 if(src_type.
id() == ID_bool)
444 src_width == 1,
"bitvector of type boolean shall have width one");
446 for(std::size_t i = 0; i < dest_width; i++)
449 dest.push_back(src[0]);
462 src_type.
id()==ID_bool)
464 for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
467 dest.push_back(src[j]);
478 for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
481 dest.push_back(src[j]);
483 dest.push_back(src.back());
495 if(dest_width<src_width)
496 dest.resize(dest_width);
500 while(dest.size()<dest_width)
512 src_width == dest_width,
513 "source bitvector width shall equal the destination bitvector width");
523 dest[0]=!float_utils.
is_zero(src);
535 if(dest_type.
id()==ID_array)
537 if(src_width==dest_width)
543 else if(
ns.
follow(dest_type).
id() == ID_struct)
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;
577 std::size_t offset=dest_offsets[i];
578 std::size_t comp_width=
boolbv_width(dest_comp[i].type());
582 op_mapt::const_iterator it=
583 op_map.find(dest_comp[i].get_name());
590 for(std::size_t j=0; j<comp_width; j++)
596 if(dest_comp[i].type()!=dest_comp[it->second].type())
599 for(std::size_t j=0; j<comp_width; j++)
604 std::size_t op_offset=op_offsets[it->second];
605 for(std::size_t j=0; j<comp_width; j++)
606 dest[offset+j]=src[op_offset+j];
622 if(expr.
op().
type().
id() == ID_range)
629 else if(from==0 && to==0)
Pre-defined bitvector types.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
bvtypet get_bvtype(const typet &type)
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
offset_mapt build_offset_map(const struct_typet &src)
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
virtual std::size_t boolbv_width(const typet &type) const
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
std::vector< std::size_t > offset_mapt
bvt add(const bvt &op0, const bvt &op1)
bvt zero_extension(const bvt &bv, std::size_t new_size)
static bvt build_constant(const mp_integer &i, std::size_t width)
literalt is_zero(const bvt &op)
bvt incrementer(const bvt &op, literalt carry_in)
Base class for all expressions.
typet & type()
Return the type of the expression.
std::size_t get_fraction_bits() const
bvt from_unsigned_integer(const bvt &)
bvt from_signed_integer(const bvt &)
literalt is_zero(const bvt &)
constant_exprt to_expr() const
void from_integer(const mp_integer &i)
const irep_idt & id() const
const std::string & get_string(const irep_idt &name) const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
virtual literalt convert_rest(const exprt &expr)
virtual literalt land(literalt a, literalt b)=0
virtual literalt new_variable()=0
virtual literalt lor(literalt a, literalt b)=0
mp_integer get_from() const
Structure type, corresponds to C style structs.
const componentst & components() const
std::vector< componentt > componentst
Semantic type conversion.
The type of an expression, extends irept.
std::vector< literalt > bvt
literalt const_literal(bool value)
const mp_integer string2integer(const std::string &n, unsigned base)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.