cprover
boolbv_typecast.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
11#include "boolbv_type.h"
13
15#include <util/c_types.h>
16#include <util/namespace.h>
17
19
21{
22 const exprt &op=expr.op();
23 const bvt &op_bv=convert_bv(op);
24
25 bvt bv;
26
27 if(type_conversion(op.type(), op_bv, expr.type(), bv))
28 return conversion_failed(expr);
29
30 return bv;
31}
32
34 const typet &src_type, const bvt &src,
35 const typet &dest_type, bvt &dest)
36{
37 bvtypet dest_bvtype=get_bvtype(dest_type);
38 bvtypet src_bvtype=get_bvtype(src_type);
39
40 if(src_bvtype==bvtypet::IS_C_BIT_FIELD)
41 return
44 src,
45 dest_type,
46 dest);
47
48 if(dest_bvtype==bvtypet::IS_C_BIT_FIELD)
49 return
51 src_type,
52 src,
54 dest);
55
56 std::size_t src_width=src.size();
57 std::size_t dest_width=boolbv_width(dest_type);
58
59 if(dest_width==0 || src_width==0)
60 return true;
61
62 dest.clear();
63 dest.reserve(dest_width);
64
65 if(dest_type.id()==ID_complex)
66 {
67 if(src_type == to_complex_type(dest_type).subtype())
68 {
69 dest.insert(dest.end(), src.begin(), src.end());
70
71 // pad with zeros
72 for(std::size_t i=src.size(); i<dest_width; i++)
73 dest.push_back(const_literal(false));
74
75 return false;
76 }
77 else if(src_type.id()==ID_complex)
78 {
79 // recursively do both halfs
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());
84 to_complex_type(src_type).subtype(),
85 lower,
86 to_complex_type(dest_type).subtype(),
87 lower_res);
89 to_complex_type(src_type).subtype(),
90 upper,
91 to_complex_type(dest_type).subtype(),
92 upper_res);
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");
97 dest=lower_res;
98 dest.insert(dest.end(), upper_res.begin(), upper_res.end());
99 return false;
100 }
101 }
102
103 if(src_type.id()==ID_complex)
104 {
105 INVARIANT(
106 dest_type.id() == ID_complex,
107 "destination type shall be of complex type when source type is of "
108 "complex type");
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)
116 {
117 // A cast from complex x to real T
118 // is (T) __real__ x.
119 bvt tmp_src(src);
120 tmp_src.resize(src.size()/2); // cut off imag part
121 return type_conversion(
122 to_complex_type(src_type).subtype(), tmp_src, dest_type, dest);
123 }
124 }
125
126 switch(dest_bvtype)
127 {
129 if(src_bvtype==bvtypet::IS_UNSIGNED ||
130 src_bvtype==bvtypet::IS_SIGNED ||
131 src_bvtype==bvtypet::IS_C_BOOL)
132 {
133 mp_integer dest_from=to_range_type(dest_type).get_from();
134
135 if(dest_from==0)
136 {
137 // do zero extension
138 dest.resize(dest_width);
139 for(std::size_t i=0; i<dest.size(); i++)
140 dest[i]=(i<src.size()?src[i]:const_literal(false));
141
142 return false;
143 }
144 }
145 else if(src_bvtype==bvtypet::IS_RANGE) // range to range
146 {
147 mp_integer src_from=to_range_type(src_type).get_from();
148 mp_integer dest_from=to_range_type(dest_type).get_from();
149
150 if(dest_from==src_from)
151 {
152 // do zero extension, if needed
153 dest=bv_utils.zero_extension(src, dest_width);
154 return false;
155 }
156 else
157 {
158 // need to do arithmetic: add src_from-dest_from
159 mp_integer offset=src_from-dest_from;
160 dest=
162 bv_utils.zero_extension(src, dest_width),
163 bv_utils.build_constant(offset, dest_width));
164 }
165
166 return false;
167 }
168 break;
169
170 case bvtypet::IS_FLOAT: // to float
171 {
172 float_utilst float_utils(prop);
173
174 switch(src_bvtype)
175 {
176 case bvtypet::IS_FLOAT: // float to float
177 // we don't have a rounding mode here,
178 // which is why we refuse.
179 break;
180
181 case bvtypet::IS_SIGNED: // signed to float
183 float_utils.spec=ieee_float_spect(to_floatbv_type(dest_type));
184 dest=float_utils.from_signed_integer(src);
185 return false;
186
187 case bvtypet::IS_UNSIGNED: // unsigned to float
188 case bvtypet::IS_C_BOOL: // _Bool to float
189 float_utils.spec=ieee_float_spect(to_floatbv_type(dest_type));
190 dest=float_utils.from_unsigned_integer(src);
191 return false;
192
193 case bvtypet::IS_BV:
194 INVARIANT(
195 src_width == dest_width,
196 "source bitvector size shall equal the destination bitvector size");
197 dest=src;
198 return false;
199
206 if(src_type.id()==ID_bool)
207 {
208 // bool to float
209
210 // build a one
211 ieee_floatt f(to_floatbv_type(dest_type));
212 f.from_integer(1);
213
214 dest=convert_bv(f.to_expr());
215
216 INVARIANT(
217 src_width == 1, "bitvector of type boolean shall have width one");
218
219 for(auto &literal : dest)
220 literal = prop.land(literal, src[0]);
221
222 return false;
223 }
224 }
225 }
226 break;
227
229 if(src_bvtype==bvtypet::IS_FIXED)
230 {
231 // fixed to fixed
232
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;
239
240 dest.resize(dest_width);
241
242 // i == position after dot
243 // i == 0: first position after dot
244
245 for(std::size_t i=0; i<dest_fraction_bits; i++)
246 {
247 // position in bv
248 std::size_t p=dest_fraction_bits-i-1;
249
250 if(i<op_fraction_bits)
251 dest[p]=src[op_fraction_bits-i-1];
252 else
253 dest[p]=const_literal(false); // zero padding
254 }
255
256 for(std::size_t i=0; i<dest_int_bits; i++)
257 {
258 // position in bv
259 std::size_t p=dest_fraction_bits+i;
260 INVARIANT(p < dest_width, "bit index shall be within bounds");
261
262 if(i<op_int_bits)
263 dest[p]=src[i+op_fraction_bits];
264 else
265 dest[p]=src[src_width-1]; // sign extension
266 }
267
268 return false;
269 }
270 else if(src_bvtype==bvtypet::IS_BV)
271 {
272 INVARIANT(
273 src_width == dest_width,
274 "source bitvector width shall equal the destination bitvector width");
275 dest=src;
276 return false;
277 }
278 else if(src_bvtype==bvtypet::IS_UNSIGNED ||
279 src_bvtype==bvtypet::IS_SIGNED ||
280 src_bvtype==bvtypet::IS_C_BOOL ||
281 src_bvtype==bvtypet::IS_C_ENUM)
282 {
283 // integer to fixed
284
285 std::size_t dest_fraction_bits=
287
288 for(std::size_t i=0; i<dest_fraction_bits; i++)
289 dest.push_back(const_literal(false)); // zero padding
290
291 for(std::size_t i=0; i<dest_width-dest_fraction_bits; i++)
292 {
293 literalt l;
294
295 if(i<src_width)
296 l=src[i];
297 else
298 {
299 if(src_bvtype==bvtypet::IS_SIGNED || src_bvtype==bvtypet::IS_C_ENUM)
300 l=src[src_width-1]; // sign extension
301 else
302 l=const_literal(false); // zero extension
303 }
304
305 dest.push_back(l);
306 }
307
308 return false;
309 }
310 else if(src_type.id()==ID_bool)
311 {
312 // bool to fixed
313 std::size_t fraction_bits=
315
316 INVARIANT(
317 src_width == 1, "bitvector of type boolean shall have width one");
318
319 for(std::size_t i=0; i<dest_width; i++)
320 {
321 if(i==fraction_bits)
322 dest.push_back(src[0]);
323 else
324 dest.push_back(const_literal(false));
325 }
326
327 return false;
328 }
329 break;
330
334 switch(src_bvtype)
335 {
336 case bvtypet::IS_FLOAT: // float to integer
337 // we don't have a rounding mode here,
338 // which is why we refuse.
339 break;
340
341 case bvtypet::IS_FIXED: // fixed to integer
342 {
343 std::size_t op_fraction_bits=
345
346 for(std::size_t i=0; i<dest_width; i++)
347 {
348 if(i<src_width-op_fraction_bits)
349 dest.push_back(src[i+op_fraction_bits]);
350 else
351 {
352 if(dest_bvtype==bvtypet::IS_SIGNED)
353 dest.push_back(src[src_width-1]); // sign extension
354 else
355 dest.push_back(const_literal(false)); // zero extension
356 }
357 }
358
359 // we might need to round up in case of negative numbers
360 // e.g., (int)(-1.00001)==1
361
362 bvt fraction_bits_bv=src;
363 fraction_bits_bv.resize(op_fraction_bits);
364 literalt round_up=
365 prop.land(prop.lor(fraction_bits_bv), src.back());
366
367 dest=bv_utils.incrementer(dest, round_up);
368
369 return false;
370 }
371
372 case bvtypet::IS_UNSIGNED: // integer to integer
376 {
377 // We do sign extension for any source type
378 // that is signed, independently of the
379 // destination type.
380 // E.g., ((short)(ulong)(short)-1)==-1
381 bool sign_extension=
382 src_bvtype==bvtypet::IS_SIGNED || src_bvtype==bvtypet::IS_C_ENUM;
383
384 for(std::size_t i=0; i<dest_width; i++)
385 {
386 if(i<src_width)
387 dest.push_back(src[i]);
388 else if(sign_extension)
389 dest.push_back(src[src_width-1]); // sign extension
390 else
391 dest.push_back(const_literal(false));
392 }
393
394 return false;
395 }
396 // verilog_unsignedbv to signed/unsigned/enum
398 {
399 for(std::size_t i=0; i<dest_width; i++)
400 {
401 std::size_t src_index=i*2; // we take every second bit
402
403 if(src_index<src_width)
404 dest.push_back(src[src_index]);
405 else // always zero-extend
406 dest.push_back(const_literal(false));
407 }
408
409 return false;
410 }
411 break;
412
413 case bvtypet::IS_VERILOG_SIGNED: // verilog_signedbv to signed/unsigned/enum
414 {
415 for(std::size_t i=0; i<dest_width; i++)
416 {
417 std::size_t src_index=i*2; // we take every second bit
418
419 if(src_index<src_width)
420 dest.push_back(src[src_index]);
421 else // always sign-extend
422 dest.push_back(src.back());
423 }
424
425 return false;
426 }
427 break;
428
429 case bvtypet::IS_BV:
430 INVARIANT(
431 src_width == dest_width,
432 "source bitvector width shall equal the destination bitvector width");
433 dest = src;
434 return false;
435
439 if(src_type.id() == ID_bool)
440 {
441 // bool to integer
442
443 INVARIANT(
444 src_width == 1, "bitvector of type boolean shall have width one");
445
446 for(std::size_t i = 0; i < dest_width; i++)
447 {
448 if(i == 0)
449 dest.push_back(src[0]);
450 else
451 dest.push_back(const_literal(false));
452 }
453
454 return false;
455 }
456 }
457 break;
458
460 if(src_bvtype==bvtypet::IS_UNSIGNED ||
461 src_bvtype==bvtypet::IS_C_BOOL ||
462 src_type.id()==ID_bool)
463 {
464 for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
465 {
466 if(j<src_width)
467 dest.push_back(src[j]);
468 else
469 dest.push_back(const_literal(false));
470
471 dest.push_back(const_literal(false));
472 }
473
474 return false;
475 }
476 else if(src_bvtype==bvtypet::IS_SIGNED)
477 {
478 for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
479 {
480 if(j<src_width)
481 dest.push_back(src[j]);
482 else
483 dest.push_back(src.back());
484
485 dest.push_back(const_literal(false));
486 }
487
488 return false;
489 }
490 else if(src_bvtype==bvtypet::IS_VERILOG_UNSIGNED)
491 {
492 // verilog_unsignedbv to verilog_unsignedbv
493 dest=src;
494
495 if(dest_width<src_width)
496 dest.resize(dest_width);
497 else
498 {
499 dest=src;
500 while(dest.size()<dest_width)
501 {
502 dest.push_back(const_literal(false));
503 dest.push_back(const_literal(false));
504 }
505 }
506 return false;
507 }
508 break;
509
510 case bvtypet::IS_BV:
511 INVARIANT(
512 src_width == dest_width,
513 "source bitvector width shall equal the destination bitvector width");
514 dest=src;
515 return false;
516
518 dest.resize(dest_width, const_literal(false));
519
520 if(src_bvtype==bvtypet::IS_FLOAT)
521 {
522 float_utilst float_utils(prop, to_floatbv_type(src_type));
523 dest[0]=!float_utils.is_zero(src);
524 }
525 else if(src_bvtype==bvtypet::IS_C_BOOL)
526 dest[0]=src[0];
527 else
528 dest[0]=!bv_utils.is_zero(src);
529
530 return false;
531
535 if(dest_type.id()==ID_array)
536 {
537 if(src_width==dest_width)
538 {
539 dest=src;
540 return false;
541 }
542 }
543 else if(ns.follow(dest_type).id() == ID_struct)
544 {
545 const struct_typet &dest_struct = to_struct_type(ns.follow(dest_type));
546
547 if(ns.follow(src_type).id() == ID_struct)
548 {
549 // we do subsets
550
551 dest.resize(dest_width, const_literal(false));
552
553 const struct_typet &op_struct = to_struct_type(ns.follow(src_type));
554
555 const struct_typet::componentst &dest_comp=
556 dest_struct.components();
557
558 const struct_typet::componentst &op_comp=
559 op_struct.components();
560
561 // build offset maps
562 const offset_mapt op_offsets = build_offset_map(op_struct);
563 const offset_mapt dest_offsets = build_offset_map(dest_struct);
564
565 // build name map
566 typedef std::map<irep_idt, std::size_t> op_mapt;
567 op_mapt op_map;
568
569 for(std::size_t i=0; i<op_comp.size(); i++)
570 op_map[op_comp[i].get_name()]=i;
571
572 // now gather required fields
573 for(std::size_t i=0;
574 i<dest_comp.size();
575 i++)
576 {
577 std::size_t offset=dest_offsets[i];
578 std::size_t comp_width=boolbv_width(dest_comp[i].type());
579 if(comp_width==0)
580 continue;
581
582 op_mapt::const_iterator it=
583 op_map.find(dest_comp[i].get_name());
584
585 if(it==op_map.end())
586 {
587 // not found
588
589 // filling with free variables
590 for(std::size_t j=0; j<comp_width; j++)
591 dest[offset+j]=prop.new_variable();
592 }
593 else
594 {
595 // found
596 if(dest_comp[i].type()!=dest_comp[it->second].type())
597 {
598 // filling with free variables
599 for(std::size_t j=0; j<comp_width; j++)
600 dest[offset+j]=prop.new_variable();
601 }
602 else
603 {
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];
607 }
608 }
609 }
610
611 return false;
612 }
613 }
614 }
615
616 return true;
617}
618
621{
622 if(expr.op().type().id() == ID_range)
623 {
624 mp_integer from = string2integer(expr.op().type().get_string(ID_from));
625 mp_integer to = string2integer(expr.op().type().get_string(ID_to));
626
627 if(from==1 && to==1)
628 return const_literal(true);
629 else if(from==0 && to==0)
630 return const_literal(false);
631 }
632
633 const bvt &bv = convert_bv(expr.op());
634
635 if(!bv.empty())
636 return prop.lor(bv);
637
638 return SUB::convert_rest(expr);
639}
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)
Definition: boolbv_type.cpp:13
bvtypet
Definition: boolbv_type.h:17
@ IS_VERILOG_UNSIGNED
@ IS_VERILOG_SIGNED
@ IS_C_BIT_FIELD
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.
Definition: c_types.h:58
const namespacet & ns
Definition: arrays.h:56
offset_mapt build_offset_map(const struct_typet &src)
Definition: boolbv.cpp:595
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...
Definition: boolbv.cpp:40
bv_utilst bv_utils
Definition: boolbv.h:114
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition: boolbv.cpp:84
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:99
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
Definition: boolbv.h:274
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:61
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:182
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:11
literalt is_zero(const bvt &op)
Definition: bv_utils.h:138
bvt incrementer(const bvt &op, literalt carry_in)
Definition: bv_utils.cpp:569
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
std::size_t get_fraction_bits() const
bvt from_unsigned_integer(const bvt &)
Definition: float_utils.cpp:50
bvt from_signed_integer(const bvt &)
Definition: float_utils.cpp:32
literalt is_zero(const bvt &)
ieee_float_spect spec
Definition: float_utils.h:88
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:515
const irep_idt & id() const
Definition: irep.h:396
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:409
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
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
Definition: std_types.cpp:160
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
std::vector< literalt > bvt
Definition: literal.h:201
literalt const_literal(bool value)
Definition: literal.h:188
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
BigInt mp_integer
Definition: smt_terms.h:12
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition: std_types.h:972
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1082