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(), width);
34 
35  bv_utilst::shiftt shift;
36 
37  if(expr.id()==ID_shl)
39  else if(expr.id()==ID_ashr)
41  else if(expr.id()==ID_lshr)
43  else if(expr.id()==ID_rol)
45  else if(expr.id()==ID_ror)
47  else
49 
50  // we optimise for the special case where the shift distance
51  // is a constant
52 
53  if(expr.op1().is_constant())
54  {
55  mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
56 
57  std::size_t distance;
58 
59  if(i<0 || i>std::numeric_limits<signed>::max())
60  distance=0;
61  else
62  distance = numeric_cast_v<std::size_t>(i);
63 
64  if(type_id==ID_verilog_signedbv ||
65  type_id==ID_verilog_unsignedbv)
66  distance*=2;
67 
68  return bv_utils.shift(op, shift, distance);
69  }
70  else
71  {
72  const bvt &distance=convert_bv(expr.op1());
73  return bv_utils.shift(op, shift, distance);
74  }
75 }
bv_utilst::shiftt::SHIFT_LEFT
@ SHIFT_LEFT
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
arith_tools.h
bvt
std::vector< literalt > bvt
Definition: literal.h:201
bv_utilst::shiftt::SHIFT_ARIGHT
@ SHIFT_ARIGHT
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
bv_utilst::shift
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:481
boolbvt::convert_shift
virtual bvt convert_shift(const binary_exprt &expr)
Definition: boolbv_shift.cpp:15
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:119
bv_utilst::shiftt
shiftt
Definition: bv_utils.h:72
bv_utilst::shiftt::ROTATE_RIGHT
@ ROTATE_RIGHT
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:85
bv_utilst::shiftt::SHIFT_LRIGHT
@ SHIFT_LRIGHT
boolbv.h
bv_utilst::shiftt::ROTATE_LEFT
@ ROTATE_LEFT
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939