cprover
Loading...
Searching...
No Matches
boolbv_shift.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
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}
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
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
virtual bvt convert_shift(const binary_exprt &expr)
bv_utilst bv_utils
Definition: boolbv.h:114
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
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:99
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:477
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
const irep_idt & id() const
Definition: irep.h:396
std::vector< literalt > bvt
Definition: literal.h:201
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840