cprover
boolbv_typecast.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <cassert>
12 
13 #include <util/std_types.h>
14 
16 
17 #include "boolbv_type.h"
19 
21 {
22  const typet &expr_type=ns.follow(expr.type());
23  const exprt &op=expr.op();
24  const typet &op_type=ns.follow(op.type());
25  const bvt &op_bv=convert_bv(op);
26 
27  bvt bv;
28 
29  if(type_conversion(op_type, op_bv, expr_type, bv))
30  return conversion_failed(expr);
31 
32  return bv;
33 }
34 
36  const typet &src_type, const bvt &src,
37  const typet &dest_type, bvt &dest)
38 {
39  bvtypet dest_bvtype=get_bvtype(dest_type);
40  bvtypet src_bvtype=get_bvtype(src_type);
41 
42  if(src_bvtype==bvtypet::IS_C_BIT_FIELD)
43  return
46  src,
47  dest_type,
48  dest);
49 
50  if(dest_bvtype==bvtypet::IS_C_BIT_FIELD)
51  return
53  src_type,
54  src,
56  dest);
57 
58  std::size_t src_width=src.size();
59  std::size_t dest_width=boolbv_width(dest_type);
60 
61  if(dest_width==0 || src_width==0)
62  return true;
63 
64  dest.clear();
65  dest.reserve(dest_width);
66 
67  if(dest_type.id()==ID_complex)
68  {
69  if(src_type==dest_type.subtype())
70  {
71  forall_literals(it, src)
72  dest.push_back(*it);
73 
74  // pad with zeros
75  for(std::size_t i=src.size(); i<dest_width; i++)
76  dest.push_back(const_literal(false));
77 
78  return false;
79  }
80  else if(src_type.id()==ID_complex)
81  {
82  // recursively do both halfs
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());
87  ns.follow(src_type.subtype()),
88  lower,
89  ns.follow(dest_type.subtype()),
90  lower_res);
92  ns.follow(src_type.subtype()),
93  upper,
94  ns.follow(dest_type.subtype()),
95  upper_res);
96  assert(lower_res.size()+upper_res.size()==dest_width);
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  assert(dest_type.id()!=ID_complex);
106  if(dest_type.id()==ID_signedbv ||
107  dest_type.id()==ID_unsignedbv ||
108  dest_type.id()==ID_floatbv ||
109  dest_type.id()==ID_fixedbv ||
110  dest_type.id()==ID_c_enum ||
111  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(src_type.subtype(), tmp_src, dest_type, dest);
119  }
120  }
121 
122  switch(dest_bvtype)
123  {
124  case bvtypet::IS_RANGE:
125  if(src_bvtype==bvtypet::IS_UNSIGNED ||
126  src_bvtype==bvtypet::IS_SIGNED ||
127  src_bvtype==bvtypet::IS_C_BOOL)
128  {
129  mp_integer dest_from=to_range_type(dest_type).get_from();
130 
131  if(dest_from==0)
132  {
133  // do zero extension
134  dest.resize(dest_width);
135  for(std::size_t i=0; i<dest.size(); i++)
136  dest[i]=(i<src.size()?src[i]:const_literal(false));
137 
138  return false;
139  }
140  }
141  else if(src_bvtype==bvtypet::IS_RANGE) // range to range
142  {
143  mp_integer src_from=to_range_type(src_type).get_from();
144  mp_integer dest_from=to_range_type(dest_type).get_from();
145 
146  if(dest_from==src_from)
147  {
148  // do zero extension, if needed
149  dest=bv_utils.zero_extension(src, dest_width);
150  return false;
151  }
152  else
153  {
154  // need to do arithmetic: add src_from-dest_from
155  mp_integer offset=src_from-dest_from;
156  dest=
157  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
178  case bvtypet::IS_C_ENUM:
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  assert(src_width==dest_width);
191  dest=src;
192  return false;
193 
194  default:
195  if(src_type.id()==ID_bool)
196  {
197  // bool to float
198 
199  // build a one
200  ieee_floatt f(to_floatbv_type(dest_type));
201  f.from_integer(1);
202 
203  dest=convert_bv(f.to_expr());
204 
205  assert(src_width==1);
206 
207  Forall_literals(it, dest)
208  *it=prop.land(*it, src[0]);
209 
210  return false;
211  }
212  }
213  }
214  break;
215 
216  case bvtypet::IS_FIXED:
217  if(src_bvtype==bvtypet::IS_FIXED)
218  {
219  // fixed to fixed
220 
221  std::size_t dest_fraction_bits=
222  to_fixedbv_type(dest_type).get_fraction_bits();
223  std::size_t dest_int_bits=dest_width-dest_fraction_bits;
224  std::size_t op_fraction_bits=
226  std::size_t op_int_bits=src_width-op_fraction_bits;
227 
228  dest.resize(dest_width);
229 
230  // i == position after dot
231  // i == 0: first position after dot
232 
233  for(std::size_t i=0; i<dest_fraction_bits; i++)
234  {
235  // position in bv
236  std::size_t p=dest_fraction_bits-i-1;
237 
238  if(i<op_fraction_bits)
239  dest[p]=src[op_fraction_bits-i-1];
240  else
241  dest[p]=const_literal(false); // zero padding
242  }
243 
244  for(std::size_t i=0; i<dest_int_bits; i++)
245  {
246  // position in bv
247  std::size_t p=dest_fraction_bits+i;
248  assert(p<dest_width);
249 
250  if(i<op_int_bits)
251  dest[p]=src[i+op_fraction_bits];
252  else
253  dest[p]=src[src_width-1]; // sign extension
254  }
255 
256  return false;
257  }
258  else if(src_bvtype==bvtypet::IS_BV)
259  {
260  assert(src_width==dest_width);
261  dest=src;
262  return false;
263  }
264  else if(src_bvtype==bvtypet::IS_UNSIGNED ||
265  src_bvtype==bvtypet::IS_SIGNED ||
266  src_bvtype==bvtypet::IS_C_BOOL ||
267  src_bvtype==bvtypet::IS_C_ENUM)
268  {
269  // integer to fixed
270 
271  std::size_t dest_fraction_bits=
272  to_fixedbv_type(dest_type).get_fraction_bits();
273 
274  for(std::size_t i=0; i<dest_fraction_bits; i++)
275  dest.push_back(const_literal(false)); // zero padding
276 
277  for(std::size_t i=0; i<dest_width-dest_fraction_bits; i++)
278  {
279  literalt l;
280 
281  if(i<src_width)
282  l=src[i];
283  else
284  {
285  if(src_bvtype==bvtypet::IS_SIGNED || src_bvtype==bvtypet::IS_C_ENUM)
286  l=src[src_width-1]; // sign extension
287  else
288  l=const_literal(false); // zero extension
289  }
290 
291  dest.push_back(l);
292  }
293 
294  return false;
295  }
296  else if(src_type.id()==ID_bool)
297  {
298  // bool to fixed
299  std::size_t fraction_bits=
300  to_fixedbv_type(dest_type).get_fraction_bits();
301 
302  assert(src_width==1);
303 
304  for(std::size_t i=0; i<dest_width; i++)
305  {
306  if(i==fraction_bits)
307  dest.push_back(src[0]);
308  else
309  dest.push_back(const_literal(false));
310  }
311 
312  return false;
313  }
314  break;
315 
317  case bvtypet::IS_SIGNED:
318  case bvtypet::IS_C_ENUM:
319  switch(src_bvtype)
320  {
321  case bvtypet::IS_FLOAT: // float to integer
322  // we don't have a rounding mode here,
323  // which is why we refuse.
324  break;
325 
326  case bvtypet::IS_FIXED: // fixed to integer
327  {
328  std::size_t op_fraction_bits=
330 
331  for(std::size_t i=0; i<dest_width; i++)
332  {
333  if(i<src_width-op_fraction_bits)
334  dest.push_back(src[i+op_fraction_bits]);
335  else
336  {
337  if(dest_bvtype==bvtypet::IS_SIGNED)
338  dest.push_back(src[src_width-1]); // sign extension
339  else
340  dest.push_back(const_literal(false)); // zero extension
341  }
342  }
343 
344  // we might need to round up in case of negative numbers
345  // e.g., (int)(-1.00001)==1
346 
347  bvt fraction_bits_bv=src;
348  fraction_bits_bv.resize(op_fraction_bits);
349  literalt round_up=
350  prop.land(prop.lor(fraction_bits_bv), src.back());
351 
352  dest=bv_utils.incrementer(dest, round_up);
353 
354  return false;
355  }
356 
357  case bvtypet::IS_UNSIGNED: // integer to integer
358  case bvtypet::IS_SIGNED:
359  case bvtypet::IS_C_ENUM:
360  case bvtypet::IS_C_BOOL:
361  {
362  // We do sign extension for any source type
363  // that is signed, independently of the
364  // destination type.
365  // E.g., ((short)(ulong)(short)-1)==-1
366  bool sign_extension=
367  src_bvtype==bvtypet::IS_SIGNED || src_bvtype==bvtypet::IS_C_ENUM;
368 
369  for(std::size_t i=0; i<dest_width; i++)
370  {
371  if(i<src_width)
372  dest.push_back(src[i]);
373  else if(sign_extension)
374  dest.push_back(src[src_width-1]); // sign extension
375  else
376  dest.push_back(const_literal(false));
377  }
378 
379  return false;
380  }
381  // verilog_unsignedbv to signed/unsigned/enum
383  {
384  for(std::size_t i=0; i<dest_width; i++)
385  {
386  std::size_t src_index=i*2; // we take every second bit
387 
388  if(src_index<src_width)
389  dest.push_back(src[src_index]);
390  else // always zero-extend
391  dest.push_back(const_literal(false));
392  }
393 
394  return false;
395  }
396  break;
397 
398  case bvtypet::IS_VERILOG_SIGNED: // verilog_signedbv to signed/unsigned/enum
399  {
400  for(std::size_t i=0; i<dest_width; i++)
401  {
402  std::size_t src_index=i*2; // we take every second bit
403 
404  if(src_index<src_width)
405  dest.push_back(src[src_index]);
406  else // always sign-extend
407  dest.push_back(src.back());
408  }
409 
410  return false;
411  }
412  break;
413 
414  default:
415  if(src_type.id()==ID_bool)
416  {
417  // bool to integer
418 
419  assert(src_width==1);
420 
421  for(std::size_t i=0; i<dest_width; i++)
422  {
423  if(i==0)
424  dest.push_back(src[0]);
425  else
426  dest.push_back(const_literal(false));
427  }
428 
429  return false;
430  }
431  }
432  break;
433 
435  if(src_bvtype==bvtypet::IS_UNSIGNED ||
436  src_bvtype==bvtypet::IS_C_BOOL ||
437  src_type.id()==ID_bool)
438  {
439  for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
440  {
441  if(j<src_width)
442  dest.push_back(src[j]);
443  else
444  dest.push_back(const_literal(false));
445 
446  dest.push_back(const_literal(false));
447  }
448 
449  return false;
450  }
451  else if(src_bvtype==bvtypet::IS_SIGNED)
452  {
453  for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
454  {
455  if(j<src_width)
456  dest.push_back(src[j]);
457  else
458  dest.push_back(src.back());
459 
460  dest.push_back(const_literal(false));
461  }
462 
463  return false;
464  }
465  else if(src_bvtype==bvtypet::IS_VERILOG_UNSIGNED)
466  {
467  // verilog_unsignedbv to verilog_unsignedbv
468  dest=src;
469 
470  if(dest_width<src_width)
471  dest.resize(dest_width);
472  else
473  {
474  dest=src;
475  while(dest.size()<dest_width)
476  {
477  dest.push_back(const_literal(false));
478  dest.push_back(const_literal(false));
479  }
480  }
481  return false;
482  }
483  break;
484 
485  case bvtypet::IS_BV:
486  assert(src_width==dest_width);
487  dest=src;
488  return false;
489 
490  case bvtypet::IS_C_BOOL:
491  dest.resize(dest_width, const_literal(false));
492 
493  if(src_bvtype==bvtypet::IS_FLOAT)
494  {
495  float_utilst float_utils(prop, to_floatbv_type(src_type));
496  dest[0]=!float_utils.is_zero(src);
497  }
498  else if(src_bvtype==bvtypet::IS_C_BOOL)
499  dest[0]=src[0];
500  else
501  dest[0]=!bv_utils.is_zero(src);
502 
503  return false;
504 
505  default:
506  if(dest_type.id()==ID_array)
507  {
508  if(src_width==dest_width)
509  {
510  dest=src;
511  return false;
512  }
513  }
514  else if(dest_type.id()==ID_struct)
515  {
516  const struct_typet &dest_struct=to_struct_type(dest_type);
517 
518  if(src_type.id()==ID_struct)
519  {
520  // we do subsets
521 
522  dest.resize(dest_width, const_literal(false));
523 
524  const struct_typet &op_struct=to_struct_type(src_type);
525 
526  const struct_typet::componentst &dest_comp=
527  dest_struct.components();
528 
529  const struct_typet::componentst &op_comp=
530  op_struct.components();
531 
532  // build offset maps
533  const offset_mapt op_offsets = build_offset_map(op_struct);
534  const offset_mapt dest_offsets = build_offset_map(dest_struct);
535 
536  // build name map
537  typedef std::map<irep_idt, std::size_t> op_mapt;
538  op_mapt op_map;
539 
540  for(std::size_t i=0; i<op_comp.size(); i++)
541  op_map[op_comp[i].get_name()]=i;
542 
543  // now gather required fields
544  for(std::size_t i=0;
545  i<dest_comp.size();
546  i++)
547  {
548  std::size_t offset=dest_offsets[i];
549  std::size_t comp_width=boolbv_width(dest_comp[i].type());
550  if(comp_width==0)
551  continue;
552 
553  op_mapt::const_iterator it=
554  op_map.find(dest_comp[i].get_name());
555 
556  if(it==op_map.end())
557  {
558  // not found
559 
560  // filling with free variables
561  for(std::size_t j=0; j<comp_width; j++)
562  dest[offset+j]=prop.new_variable();
563  }
564  else
565  {
566  // found
567  if(dest_comp[i].type()!=dest_comp[it->second].type())
568  {
569  // filling with free variables
570  for(std::size_t j=0; j<comp_width; j++)
571  dest[offset+j]=prop.new_variable();
572  }
573  else
574  {
575  std::size_t op_offset=op_offsets[it->second];
576  for(std::size_t j=0; j<comp_width; j++)
577  dest[offset+j]=src[op_offset+j];
578  }
579  }
580  }
581 
582  return false;
583  }
584  }
585  }
586 
587  return true;
588 }
589 
592 {
593  assert(expr.operands().size()==1);
594 
595  if(expr.op0().type().id()==ID_range)
596  {
597  mp_integer from=string2integer(expr.op0().type().get_string(ID_from));
598  mp_integer to=string2integer(expr.op0().type().get_string(ID_to));
599 
600  if(from==1 && to==1)
601  return const_literal(true);
602  else if(from==0 && to==0)
603  return const_literal(false);
604  }
605 
606  const bvt &bv=convert_bv(expr.op0());
607 
608  if(!bv.empty())
609  return prop.lor(bv);
610 
611  return SUB::convert_rest(expr);
612 }
The type of an expression.
Definition: type.h:22
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:250
semantic type conversion
Definition: std_expr.h:2111
bv_utilst bv_utils
Definition: boolbv.h:93
BigInt mp_integer
Definition: mp_arith.h:22
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
exprt & op0()
Definition: expr.h:72
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
const exprt & op() const
Definition: std_expr.h:340
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
boolbv_widtht boolbv_width
Definition: boolbv.h:90
std::vector< componentt > componentst
Definition: std_types.h:243
virtual literalt lor(literalt a, literalt b)=0
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
literalt is_zero(const bvt &op)
Definition: bv_utils.h:141
Structure type.
Definition: std_types.h:297
#define forall_literals(it, bv)
Definition: literal.h:202
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:259
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
Definition: literal.h:206
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
std::size_t get_fraction_bits() const
Definition: std_types.h:1320
offset_mapt build_offset_map(const struct_typet &src)
Definition: boolbv.cpp:663
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
literalt is_zero(const bvt &)
const namespacet & ns
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
bvtypet get_bvtype(const typet &type)
Definition: boolbv_type.cpp:12
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:184
bvtypet
Definition: boolbv_type.h:16
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
bvt incrementer(const bvt &op, literalt carry_in)
Definition: bv_utils.cpp:572
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
literalt const_literal(bool value)
Definition: literal.h:187
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:64
ieee_float_spect spec
Definition: float_utils.h:86
bvt from_unsigned_integer(const bvt &)
Definition: float_utils.cpp:51
API to type classes.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1382
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1343
Base class for all expressions.
Definition: expr.h:42
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:331
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:508
bvt from_signed_integer(const bvt &)
Definition: float_utils.cpp:33
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Definition: std_types.h:1411
const range_typet & to_range_type(const typet &type)
Cast a generic typet to a range_typet.
Definition: std_types.h:1630
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
std::vector< literalt > bvt
Definition: literal.h:200
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
mp_integer get_from() const
Definition: std_types.cpp:127