cprover
boolbv_extractbits.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 <util/arith_tools.h>
12 
14 {
15  std::size_t width=boolbv_width(expr.type());
16 
17  if(width==0)
18  return conversion_failed(expr);
19 
20  if(expr.operands().size()!=3)
21  {
23  error() << "extractbits takes three operands" << eom;
24  throw 0;
25  }
26 
27  mp_integer o1, o2;
28  const bvt &bv0=convert_bv(expr.op0());
29 
30  // We only do constants for now.
31  // Should implement a shift here.
32  if(to_integer(expr.op1(), o1) ||
33  to_integer(expr.op2(), o2))
34  return conversion_failed(expr);
35 
36  if(o1<0 || o1>=bv0.size())
37  {
39  error() << "extractbits: second operand out of range: "
40  << expr.pretty() << eom;
41  }
42 
43  if(o2<0 || o2>=bv0.size())
44  {
46  error() << "extractbits: third operand out of range: "
47  << expr.pretty() << eom;
48  throw 0;
49  }
50 
51  if(o2>o1)
52  std::swap(o1, o2);
53 
54  // now o2<=o1
55 
56  if((o1-o2+1)!=width)
57  {
59  error() << "extractbits: wrong width (expected " << (o1-o2+1)
60  << " but got " << width << "): " << expr.pretty() << eom;
61  throw 0;
62  }
63 
64  std::size_t offset=integer2unsigned(o2);
65 
66  bvt bv;
67  bv.resize(width);
68 
69  for(std::size_t i=0; i<width; i++)
70  bv[i]=bv0[offset+i];
71 
72  return bv;
73 }
BigInt mp_integer
Definition: mp_arith.h:22
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
boolbv_widtht boolbv_width
Definition: boolbv.h:90
typet & type()
Definition: expr.h:56
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
const source_locationt & find_source_location() const
Definition: expr.cpp:246
source_locationt source_location
Definition: message.h:214
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3072
exprt & op1()
Definition: expr.h:75
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
mstreamt & error() const
Definition: message.h:302
virtual bvt convert_extractbits(const extractbits_exprt &expr)
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:202
exprt & op2()
Definition: expr.h:78
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
operandst & operands()
Definition: expr.h:66
std::vector< literalt > bvt
Definition: literal.h:200