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