cprover
boolbv_shift.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 <limits>
12 
13 #include <util/arith_tools.h>
14 
16 {
17  const irep_idt &type_id=expr.type().id();
18 
19  if(type_id!=ID_unsignedbv &&
20  type_id!=ID_signedbv &&
21  type_id!=ID_floatbv &&
22  type_id!=ID_pointer &&
23  type_id!=ID_bv &&
24  type_id!=ID_verilog_signedbv &&
25  type_id!=ID_verilog_unsignedbv)
26  return conversion_failed(expr);
27 
28  std::size_t width=boolbv_width(expr.type());
29 
30  if(width==0)
31  return conversion_failed(expr);
32 
33  const bvt &op=convert_bv(expr.op0());
34 
35  if(op.size()!=width)
36  throw "convert_shift: unexpected operand 0 width";
37 
38  bv_utilst::shiftt shift;
39 
40  if(expr.id()==ID_shl)
42  else if(expr.id()==ID_ashr)
44  else if(expr.id()==ID_lshr)
46  else if(expr.id()==ID_rol)
48  else if(expr.id()==ID_ror)
50  else
51  throw "unexpected shift operator";
52 
53  // we allow a constant as shift distance
54 
55  if(expr.op1().is_constant())
56  {
57  mp_integer i;
58  if(to_integer(expr.op1(), i))
59  throw "convert_shift: failed to convert constant";
60 
61  std::size_t distance;
62 
63  if(i<0 || i>std::numeric_limits<signed>::max())
64  distance=0;
65  else
66  distance=integer2size_t(i);
67 
68  if(type_id==ID_verilog_signedbv ||
69  type_id==ID_verilog_unsignedbv)
70  distance*=2;
71 
72  return bv_utils.shift(op, shift, distance);
73  }
74  else
75  {
76  const bvt &distance=convert_bv(expr.op1());
77  return bv_utils.shift(op, shift, distance);
78  }
79 }
bv_utilst bv_utils
Definition: boolbv.h:93
BigInt mp_integer
Definition: mp_arith.h:22
exprt & op0()
Definition: expr.h:72
virtual bvt convert_shift(const binary_exprt &expr)
boolbv_widtht boolbv_width
Definition: boolbv.h:90
typet & type()
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:259
A generic base class for binary expressions.
Definition: std_expr.h:649
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
exprt & op1()
Definition: expr.h:75
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
bool is_constant() const
Definition: expr.cpp:119
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:480
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
std::vector< literalt > bvt
Definition: literal.h:200