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 }
exception_utils.h
arith_tools.h
bvt
std::vector< literalt > bvt
Definition: literal.h:200
unsupported_operation_exceptiont
Thrown when we encounter an instruction, parameters to an instruction etc.
Definition: exception_utils.h:143
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
propt::new_variable
virtual literalt new_variable()=0
boolbvt::literal
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
Definition: boolbv.cpp:32
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:49
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1484
boolbvt::convert_extractbit
virtual literalt convert_extractbit(const extractbit_exprt &expr)
Definition: boolbv_extractbit.cpp:19
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
address_bits
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
Definition: arith_tools.cpp:200
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:92
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
std_types.h
extractbit_exprt::index
exprt & index()
Definition: std_expr.h:3105
irept::id
const irep_idt & id() const
Definition: irep.h:259
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:157
prop_conv_solvert::convert_rest
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:330
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:3080
propt::lequal
virtual literalt lequal(literalt a, literalt b)=0
extractbit_exprt::src
exprt & src()
Definition: std_expr.h:3100
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
literalt
Definition: literal.h:24
propt::has_set_to
virtual bool has_set_to() const
Definition: prop.h:78
boolbv.h
std_expr.h
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
equalityt::equality
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152