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/exception_utils.h>
16 #include <util/std_expr.h>
17 #include <util/std_types.h>
18 
20 {
21  const bvt &src_bv = convert_bv(expr.src());
22 
23  // constant?
24  if(expr.index().is_constant())
25  {
26  mp_integer index_as_integer = numeric_cast_v<mp_integer>(expr.index());
27 
28  if(index_as_integer < 0 || index_as_integer >= src_bv.size())
29  return prop.new_variable(); // out of range!
30  else
31  return src_bv[numeric_cast_v<std::size_t>(index_as_integer)];
32  }
33 
34  if(
35  expr.src().type().id() == ID_verilog_signedbv ||
36  expr.src().type().id() == ID_verilog_unsignedbv)
37  {
39  "extractbit expression not implemented for verilog integers in "
40  "flattening solver");
41  }
42  else
43  {
44  std::size_t src_bv_width = boolbv_width(expr.src().type());
45  std::size_t index_bv_width = boolbv_width(expr.index().type());
46 
47  if(src_bv_width == 0 || index_bv_width == 0)
48  return SUB::convert_rest(expr);
49 
50  std::size_t index_width =
51  std::max(address_bits(src_bv_width), index_bv_width);
52  unsignedbv_typet index_type(index_width);
53 
55  equality.lhs() = expr.index();
56 
57  if(index_type!=equality.lhs().type())
58  equality.lhs().make_typecast(index_type);
59 
60  if(prop.has_set_to())
61  {
62  // free variable
64 
65  // add implications
66  for(std::size_t i = 0; i < src_bv.size(); i++)
67  {
69  literalt equal = prop.lequal(literal, src_bv[i]);
71  }
72 
73  return literal;
74  }
75  else
76  {
78 
79  for(std::size_t i = 0; i < src_bv.size(); i++)
80  {
82  literal = prop.lselect(convert(equality), src_bv[i], literal);
83  }
84 
85  return literal;
86  }
87  }
88 
89  return SUB::convert_rest(expr);
90 }
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
BigInt mp_integer
Definition: mp_arith.h:22
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:157
boolbv_widtht boolbv_width
Definition: boolbv.h:92
Thrown when we encounter an instruction, parameters to an instruction etc.
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
typet & type()
Return the type of the expression.
Definition: expr.h:68
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:49
Equality.
Definition: std_expr.h:1484
const irep_idt & id() const
Definition: irep.h:259
virtual literalt new_variable()=0
API to expression classes.
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
Definition: boolbv.cpp:32
bitvector_typet index_type()
Definition: c_types.cpp:16
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
exprt & index()
Definition: std_expr.h:3105
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
Pre-defined types.
virtual bool has_set_to() const
Definition: prop.h:78
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:330
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt convert_extractbit(const extractbit_exprt &expr)
exprt & src()
Definition: std_expr.h:3100
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:3080