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