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  INVARIANT(
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");
100  dest=lower_res;
101  dest.insert(dest.end(), upper_res.begin(), upper_res.end());
102  return false;
103  }
104  }
105 
106  if(src_type.id()==ID_complex)
107  {
108  INVARIANT(
109  dest_type.id() == ID_complex,
110  "destination type shall be of complex type when source type is of "
111  "complex type");
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)
119  {
120  // A cast from complex x to real T
121  // is (T) __real__ x.
122  bvt tmp_src(src);
123  tmp_src.resize(src.size()/2); // cut off imag part
124  return type_conversion(src_type.subtype(), tmp_src, dest_type, dest);
125  }
126  }
127 
128  switch(dest_bvtype)
129  {
130  case bvtypet::IS_RANGE:
131  if(src_bvtype==bvtypet::IS_UNSIGNED ||
132  src_bvtype==bvtypet::IS_SIGNED ||
133  src_bvtype==bvtypet::IS_C_BOOL)
134  {
135  mp_integer dest_from=to_range_type(dest_type).get_from();
136 
137  if(dest_from==0)
138  {
139  // do zero extension
140  dest.resize(dest_width);
141  for(std::size_t i=0; i<dest.size(); i++)
142  dest[i]=(i<src.size()?src[i]:const_literal(false));
143 
144  return false;
145  }
146  }
147  else if(src_bvtype==bvtypet::IS_RANGE) // range to range
148  {
149  mp_integer src_from=to_range_type(src_type).get_from();
150  mp_integer dest_from=to_range_type(dest_type).get_from();
151 
152  if(dest_from==src_from)
153  {
154  // do zero extension, if needed
155  dest=bv_utils.zero_extension(src, dest_width);
156  return false;
157  }
158  else
159  {
160  // need to do arithmetic: add src_from-dest_from
161  mp_integer offset=src_from-dest_from;
162  dest=
163  bv_utils.add(
164  bv_utils.zero_extension(src, dest_width),
165  bv_utils.build_constant(offset, dest_width));
166  }
167 
168  return false;
169  }
170  break;
171 
172  case bvtypet::IS_FLOAT: // to float
173  {
174  float_utilst float_utils(prop);
175 
176  switch(src_bvtype)
177  {
178  case bvtypet::IS_FLOAT: // float to float
179  // we don't have a rounding mode here,
180  // which is why we refuse.
181  break;
182 
183  case bvtypet::IS_SIGNED: // signed to float
184  case bvtypet::IS_C_ENUM:
185  float_utils.spec=ieee_float_spect(to_floatbv_type(dest_type));
186  dest=float_utils.from_signed_integer(src);
187  return false;
188 
189  case bvtypet::IS_UNSIGNED: // unsigned to float
190  case bvtypet::IS_C_BOOL: // _Bool to float
191  float_utils.spec=ieee_float_spect(to_floatbv_type(dest_type));
192  dest=float_utils.from_unsigned_integer(src);
193  return false;
194 
195  case bvtypet::IS_BV:
196  INVARIANT(
197  src_width == dest_width,
198  "source bitvector size shall equal the destination bitvector size");
199  dest=src;
200  return false;
201 
202  default:
203  if(src_type.id()==ID_bool)
204  {
205  // bool to float
206 
207  // build a one
208  ieee_floatt f(to_floatbv_type(dest_type));
209  f.from_integer(1);
210 
211  dest=convert_bv(f.to_expr());
212 
213  INVARIANT(
214  src_width == 1, "bitvector of type boolean shall have width one");
215 
216  Forall_literals(it, dest)
217  *it=prop.land(*it, src[0]);
218 
219  return false;
220  }
221  }
222  }
223  break;
224 
225  case bvtypet::IS_FIXED:
226  if(src_bvtype==bvtypet::IS_FIXED)
227  {
228  // fixed to fixed
229 
230  std::size_t dest_fraction_bits=
231  to_fixedbv_type(dest_type).get_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;
236 
237  dest.resize(dest_width);
238 
239  // i == position after dot
240  // i == 0: first position after dot
241 
242  for(std::size_t i=0; i<dest_fraction_bits; i++)
243  {
244  // position in bv
245  std::size_t p=dest_fraction_bits-i-1;
246 
247  if(i<op_fraction_bits)
248  dest[p]=src[op_fraction_bits-i-1];
249  else
250  dest[p]=const_literal(false); // zero padding
251  }
252 
253  for(std::size_t i=0; i<dest_int_bits; i++)
254  {
255  // position in bv
256  std::size_t p=dest_fraction_bits+i;
257  INVARIANT(p < dest_width, "bit index shall be within bounds");
258 
259  if(i<op_int_bits)
260  dest[p]=src[i+op_fraction_bits];
261  else
262  dest[p]=src[src_width-1]; // sign extension
263  }
264 
265  return false;
266  }
267  else if(src_bvtype==bvtypet::IS_BV)
268  {
269  INVARIANT(
270  src_width == dest_width,
271  "source bitvector with shall equal the destination bitvector width");
272  dest=src;
273  return false;
274  }
275  else if(src_bvtype==bvtypet::IS_UNSIGNED ||
276  src_bvtype==bvtypet::IS_SIGNED ||
277  src_bvtype==bvtypet::IS_C_BOOL ||
278  src_bvtype==bvtypet::IS_C_ENUM)
279  {
280  // integer to fixed
281 
282  std::size_t dest_fraction_bits=
283  to_fixedbv_type(dest_type).get_fraction_bits();
284 
285  for(std::size_t i=0; i<dest_fraction_bits; i++)
286  dest.push_back(const_literal(false)); // zero padding
287 
288  for(std::size_t i=0; i<dest_width-dest_fraction_bits; i++)
289  {
290  literalt l;
291 
292  if(i<src_width)
293  l=src[i];
294  else
295  {
296  if(src_bvtype==bvtypet::IS_SIGNED || 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=
311  to_fixedbv_type(dest_type).get_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 
329  case bvtypet::IS_SIGNED:
330  case bvtypet::IS_C_ENUM:
331  switch(src_bvtype)
332  {
333  case bvtypet::IS_FLOAT: // float to integer
334  // we don't have a rounding mode here,
335  // which is why we refuse.
336  break;
337 
338  case bvtypet::IS_FIXED: // fixed to integer
339  {
340  std::size_t op_fraction_bits=
342 
343  for(std::size_t i=0; i<dest_width; i++)
344  {
345  if(i<src_width-op_fraction_bits)
346  dest.push_back(src[i+op_fraction_bits]);
347  else
348  {
349  if(dest_bvtype==bvtypet::IS_SIGNED)
350  dest.push_back(src[src_width-1]); // sign extension
351  else
352  dest.push_back(const_literal(false)); // zero extension
353  }
354  }
355 
356  // we might need to round up in case of negative numbers
357  // e.g., (int)(-1.00001)==1
358 
359  bvt fraction_bits_bv=src;
360  fraction_bits_bv.resize(op_fraction_bits);
361  literalt round_up=
362  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
370  case bvtypet::IS_SIGNED:
371  case bvtypet::IS_C_ENUM:
372  case bvtypet::IS_C_BOOL:
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  default:
427  if(src_type.id()==ID_bool)
428  {
429  // bool to integer
430 
431  INVARIANT(
432  src_width == 1, "bitvector of type boolean shall have width one");
433 
434  for(std::size_t i=0; i<dest_width; i++)
435  {
436  if(i==0)
437  dest.push_back(src[0]);
438  else
439  dest.push_back(const_literal(false));
440  }
441 
442  return false;
443  }
444  }
445  break;
446 
448  if(src_bvtype==bvtypet::IS_UNSIGNED ||
449  src_bvtype==bvtypet::IS_C_BOOL ||
450  src_type.id()==ID_bool)
451  {
452  for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
453  {
454  if(j<src_width)
455  dest.push_back(src[j]);
456  else
457  dest.push_back(const_literal(false));
458 
459  dest.push_back(const_literal(false));
460  }
461 
462  return false;
463  }
464  else if(src_bvtype==bvtypet::IS_SIGNED)
465  {
466  for(std::size_t i=0, j=0; i<dest_width; i+=2, j++)
467  {
468  if(j<src_width)
469  dest.push_back(src[j]);
470  else
471  dest.push_back(src.back());
472 
473  dest.push_back(const_literal(false));
474  }
475 
476  return false;
477  }
478  else if(src_bvtype==bvtypet::IS_VERILOG_UNSIGNED)
479  {
480  // verilog_unsignedbv to verilog_unsignedbv
481  dest=src;
482 
483  if(dest_width<src_width)
484  dest.resize(dest_width);
485  else
486  {
487  dest=src;
488  while(dest.size()<dest_width)
489  {
490  dest.push_back(const_literal(false));
491  dest.push_back(const_literal(false));
492  }
493  }
494  return false;
495  }
496  break;
497 
498  case bvtypet::IS_BV:
499  INVARIANT(
500  src_width == dest_width,
501  "source bitvector width shall equal the destination bitvector width");
502  dest=src;
503  return false;
504 
505  case bvtypet::IS_C_BOOL:
506  dest.resize(dest_width, const_literal(false));
507 
508  if(src_bvtype==bvtypet::IS_FLOAT)
509  {
510  float_utilst float_utils(prop, to_floatbv_type(src_type));
511  dest[0]=!float_utils.is_zero(src);
512  }
513  else if(src_bvtype==bvtypet::IS_C_BOOL)
514  dest[0]=src[0];
515  else
516  dest[0]=!bv_utils.is_zero(src);
517 
518  return false;
519 
520  default:
521  if(dest_type.id()==ID_array)
522  {
523  if(src_width==dest_width)
524  {
525  dest=src;
526  return false;
527  }
528  }
529  else if(dest_type.id()==ID_struct)
530  {
531  const struct_typet &dest_struct=to_struct_type(dest_type);
532 
533  if(src_type.id()==ID_struct)
534  {
535  // we do subsets
536 
537  dest.resize(dest_width, const_literal(false));
538 
539  const struct_typet &op_struct=to_struct_type(src_type);
540 
541  const struct_typet::componentst &dest_comp=
542  dest_struct.components();
543 
544  const struct_typet::componentst &op_comp=
545  op_struct.components();
546 
547  // build offset maps
548  const offset_mapt op_offsets = build_offset_map(op_struct);
549  const offset_mapt dest_offsets = build_offset_map(dest_struct);
550 
551  // build name map
552  typedef std::map<irep_idt, std::size_t> op_mapt;
553  op_mapt op_map;
554 
555  for(std::size_t i=0; i<op_comp.size(); i++)
556  op_map[op_comp[i].get_name()]=i;
557 
558  // now gather required fields
559  for(std::size_t i=0;
560  i<dest_comp.size();
561  i++)
562  {
563  std::size_t offset=dest_offsets[i];
564  std::size_t comp_width=boolbv_width(dest_comp[i].type());
565  if(comp_width==0)
566  continue;
567 
568  op_mapt::const_iterator it=
569  op_map.find(dest_comp[i].get_name());
570 
571  if(it==op_map.end())
572  {
573  // not found
574 
575  // filling with free variables
576  for(std::size_t j=0; j<comp_width; j++)
577  dest[offset+j]=prop.new_variable();
578  }
579  else
580  {
581  // found
582  if(dest_comp[i].type()!=dest_comp[it->second].type())
583  {
584  // filling with free variables
585  for(std::size_t j=0; j<comp_width; j++)
586  dest[offset+j]=prop.new_variable();
587  }
588  else
589  {
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];
593  }
594  }
595  }
596 
597  return false;
598  }
599  }
600  }
601 
602  return true;
603 }
604 
607 {
608  if(expr.op().type().id() == ID_range)
609  {
610  mp_integer from = string2integer(expr.op().type().get_string(ID_from));
611  mp_integer to = string2integer(expr.op().type().get_string(ID_to));
612 
613  if(from==1 && to==1)
614  return const_literal(true);
615  else if(from==0 && to==0)
616  return const_literal(false);
617  }
618 
619  const bvt &bv = convert_bv(expr.op());
620 
621  if(!bv.empty())
622  return prop.lor(bv);
623 
624  return SUB::convert_rest(expr);
625 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
boolbvt::convert_bv_typecast
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
Definition: boolbv_typecast.cpp:20
ieee_floatt
Definition: ieee_float.h:119
bvtypet::IS_SIGNED
typet::subtype
const typet & subtype() const
Definition: type.h:38
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
boolbvt::type_conversion
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
Definition: boolbv_typecast.cpp:35
c_bit_field_replacement_type.h
float_utilst
Definition: float_utils.h:17
typet
The type of an expression, extends irept.
Definition: type.h:27
float_utils.h
bvt
std::vector< literalt > bvt
Definition: literal.h:200
bvtypet::IS_FIXED
bvtypet::IS_C_BIT_FIELD
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
boolbv_type.h
get_bvtype
bvtypet get_bvtype(const typet &type)
Definition: boolbv_type.cpp:12
propt::new_variable
virtual literalt new_variable()=0
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:203
propt::lor
virtual literalt lor(literalt a, literalt b)=0
bvtypet::IS_VERILOG_SIGNED
bvtypet::IS_RANGE
bv_utilst::incrementer
bvt incrementer(const bvt &op, literalt carry_in)
Definition: bv_utils.cpp:573
bvtypet::IS_UNSIGNED
forall_literals
#define forall_literals(it, bv)
Definition: literal.h:202
propt::land
virtual literalt land(literalt a, literalt b)=0
Forall_literals
#define Forall_literals(it, bv)
Definition: literal.h:206
bvtypet::IS_BV
float_utilst::from_signed_integer
bvt from_signed_integer(const bvt &)
Definition: float_utils.cpp:32
ieee_float_spect
Definition: ieee_float.h:25
bvtypet
bvtypet
Definition: boolbv_type.h:16
bvtypet::IS_VERILOG_UNSIGNED
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
bvtypet::IS_FLOAT
bv_utilst::add
bvt add(const bvt &op0, const bvt &op1)
Definition: bv_utils.h:64
float_utilst::is_zero
literalt is_zero(const bvt &)
Definition: float_utils.cpp:652
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:92
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1380
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:110
bvtypet::IS_C_BOOL
range_typet::get_from
mp_integer get_from() const
Definition: std_types.cpp:155
std_types.h
to_c_bit_field_type
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: std_types.h:1491
const_literal
literalt const_literal(bool value)
Definition: literal.h:187
decision_proceduret::ns
const namespacet & ns
Definition: decision_procedure.h:61
irept::id
const irep_idt & id() const
Definition: irep.h:259
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:512
prop_conv_solvert::convert_rest
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:330
to_range_type
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition: std_types.h:1734
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
bvtypet::IS_C_ENUM
bv_utilst::build_constant
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
fixedbv_typet::get_fraction_bits
std::size_t get_fraction_bits() const
Definition: std_types.h:1344
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:95
literalt
Definition: literal.h:24
c_bit_field_replacement_type
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
Definition: c_bit_field_replacement_type.cpp:12
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
boolbv.h
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
boolbvt::convert_typecast
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
Definition: boolbv_typecast.cpp:606
bv_utilst::is_zero
literalt is_zero(const bvt &op)
Definition: bv_utils.h:141
boolbvt::offset_mapt
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:252
boolbvt::build_offset_map
offset_mapt build_offset_map(const struct_typet &src)
Definition: boolbv.cpp:655
float_utilst::spec
ieee_float_spect spec
Definition: float_utils.h:87
float_utilst::from_unsigned_integer
bvt from_unsigned_integer(const bvt &)
Definition: float_utils.cpp:50
validation_modet::INVARIANT
bv_utilst::zero_extension
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition: bv_utils.h:184
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152