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  std::size_t index_width = std::max(address_bits(width_op0), width_op1);
56  unsignedbv_typet index_type(index_width);
57 
59  equality.lhs()=operands[1]; // index operand
60 
61  if(index_type!=equality.lhs().type())
62  equality.lhs().make_typecast(index_type);
63 
64  if(prop.has_set_to())
65  {
66  // free variable
68 
69  // add implications
70  for(std::size_t i=0; i<bv0.size(); i++)
71  {
73  literalt equal=prop.lequal(l, bv0[i]);
75  }
76 
77  return l;
78  }
79  else
80  {
82 
83  for(std::size_t i=0; i<bv0.size(); i++)
84  {
86  l=prop.lselect(convert(equality), bv0[i], l);
87  }
88 
89  return l;
90  }
91  }
92 
93  return SUB::convert_rest(expr);
94 }
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1220
BigInt mp_integer
Definition: mp_arith.h:22
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:162
boolbv_widtht boolbv_width
Definition: boolbv.h:90
std::size_t 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:49
equality
Definition: std_expr.h:1354
virtual literalt new_variable()=0
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
API to expression classes.
bitvector_typet index_type()
Definition: c_types.cpp:16
std::vector< exprt > operandst
Definition: expr.h:45
virtual literalt lequal(literalt a, literalt b)=0
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:78
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:331
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
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:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::vector< literalt > bvt
Definition: literal.h:200
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2991