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