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  if(expr.operands().size()!=2)
34  throw "shifting takes two operands";
35 
36  const bvt &op=convert_bv(expr.op0());
37 
38  if(op.size()!=width)
39  throw "convert_shift: unexpected operand 0 width";
40 
41  bv_utilst::shiftt shift;
42 
43  if(expr.id()==ID_shl)
45  else if(expr.id()==ID_ashr)
47  else if(expr.id()==ID_lshr)
49  else
50  throw "unexpected shift operator";
51 
52  // we allow a constant as shift distance
53 
54  if(expr.op1().is_constant())
55  {
56  mp_integer i;
57  if(to_integer(expr.op1(), i))
58  throw "convert_shift: failed to convert constant";
59 
60  std::size_t distance;
61 
62  if(i<0 || i>std::numeric_limits<signed>::max())
63  distance=0;
64  else
65  distance=integer2size_t(i);
66 
67  if(type_id==ID_verilog_signedbv ||
68  type_id==ID_verilog_unsignedbv)
69  distance*=2;
70 
71  return bv_utils.shift(op, shift, distance);
72  }
73  else
74  {
75  const bvt &distance=convert_bv(expr.op1());
76  return bv_utils.shift(op, shift, distance);
77  }
78 }
bv_utilst bv_utils
Definition: boolbv.h:93
BigInt mp_integer
Definition: mp_arith.h:19
exprt & op0()
Definition: expr.h:84
virtual bvt convert_shift(const binary_exprt &expr)
boolbv_widtht boolbv_width
Definition: boolbv.h:90
typet & type()
Definition: expr.h:60
const irep_idt & id() const
Definition: irep.h:189
A generic base class for binary expressions.
Definition: std_expr.h:471
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
exprt & op1()
Definition: expr.h:87
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
bool is_constant() const
Definition: expr.cpp:128
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:18
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
operandst & operands()
Definition: expr.h:70
std::vector< literalt > bvt
Definition: literal.h:197