cprover
boolbv_extractbit.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 <cassert>
12 #include <algorithm>
13 
14 #include <util/arith_tools.h>
15 #include <util/std_expr.h>
16 #include <util/std_types.h>
17 
19 {
20  const exprt::operandst &operands=expr.operands();
21 
22  if(operands.size()!=2)
23  throw "extractbit takes two operands";
24 
25  const bvt &bv0=convert_bv(operands[0]);
26 
27  // constant?
28  if(operands[1].is_constant())
29  {
30  mp_integer o;
31 
32  if(to_integer(operands[1], o))
33  throw "extractbit failed to convert constant index";
34 
35  if(o<0 || o>=bv0.size())
36  return prop.new_variable(); // out of range!
37  else
38  return bv0[integer2size_t(o)];
39  }
40 
41  if(operands[0].type().id()==ID_verilog_signedbv ||
42  operands[0].type().id()==ID_verilog_unsignedbv)
43  {
44  // TODO
45  assert(false);
46  }
47  else
48  {
49  std::size_t width_op0=boolbv_width(operands[0].type());
50  std::size_t width_op1=boolbv_width(operands[1].type());
51 
52  if(width_op0==0 || width_op1==0)
53  return SUB::convert_rest(expr);
54 
55  mp_integer index_width=
56  std::max(address_bits(width_op0), mp_integer(width_op1));
57 
60 
62  equality.lhs()=operands[1]; // index operand
63 
64  if(index_type!=equality.lhs().type())
65  equality.lhs().make_typecast(index_type);
66 
67  if(prop.has_set_to())
68  {
69  // free variable
71 
72  // add implications
73  for(std::size_t i=0; i<bv0.size(); i++)
74  {
76  literalt equal=prop.lequal(l, bv0[i]);
78  }
79 
80  return l;
81  }
82  else
83  {
85 
86  for(std::size_t i=0; i<bv0.size(); i++)
87  {
89  l=prop.lselect(convert(equality), bv0[i], l);
90  }
91 
92  return l;
93  }
94  }
95 
96  return SUB::convert_rest(expr);
97 }
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1125
BigInt mp_integer
Definition: mp_arith.h:19
virtual literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:175
boolbv_widtht boolbv_width
Definition: boolbv.h:90
mp_integer address_bits(const mp_integer &size)
ceil(log2(size))
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:47
equality
Definition: std_expr.h:1082
virtual literalt new_variable()=0
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
API to expression classes.
bitvector_typet index_type()
Definition: c_types.cpp:15
std::vector< exprt > operandst
Definition: expr.h:49
virtual literalt lequal(literalt a, literalt b)=0
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
API to type classes.
virtual bool has_set_to() const
Definition: prop.h:76
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:337
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
virtual literalt convert_extractbit(const extractbit_exprt &expr)
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::vector< literalt > bvt
Definition: literal.h:197
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2434
void set_width(std::size_t width)
Definition: std_types.h:1035