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 <algorithm>
12 
13 #include <util/arith_tools.h>
14 #include <util/bitvector_expr.h>
15 #include <util/bitvector_types.h>
16 #include <util/exception_utils.h>
17 #include <util/std_expr.h>
18 #include <util/std_types.h>
19 
21 {
22  const bvt &src_bv = convert_bv(expr.src());
23  const auto &index = expr.index();
24 
25  // constant?
26  if(index.is_constant())
27  {
28  mp_integer index_as_integer =
29  numeric_cast_v<mp_integer>(to_constant_expr(index));
30 
31  if(index_as_integer < 0 || index_as_integer >= src_bv.size())
32  return prop.new_variable(); // out of range!
33  else
34  return src_bv[numeric_cast_v<std::size_t>(index_as_integer)];
35  }
36 
37  if(
38  expr.src().type().id() == ID_verilog_signedbv ||
39  expr.src().type().id() == ID_verilog_unsignedbv)
40  {
42  "extractbit expression not implemented for verilog integers in "
43  "flattening solver");
44  }
45  else
46  {
47  std::size_t src_bv_width = boolbv_width(expr.src().type());
48  std::size_t index_bv_width = boolbv_width(index.type());
49 
50  if(src_bv_width == 0 || index_bv_width == 0)
51  return SUB::convert_rest(expr);
52 
53  std::size_t index_width =
54  std::max(address_bits(src_bv_width), index_bv_width);
55  unsignedbv_typet index_type(index_width);
56 
59 
60  if(prop.has_set_to())
61  {
62  // free variable
63  literalt literal = prop.new_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  {
77  literalt literal = prop.new_variable();
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 }
exception_utils.h
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1788
arith_tools.h
bvt
std::vector< literalt > bvt
Definition: literal.h:201
unsupported_operation_exceptiont
Thrown when we encounter an instruction, parameters to an instruction etc.
Definition: exception_utils.h:144
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
propt::new_variable
virtual literalt new_variable()=0
exprt
Base class for all expressions.
Definition: expr.h:54
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:52
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1139
boolbvt::convert_extractbit
virtual literalt convert_extractbit(const extractbit_exprt &expr)
Definition: boolbv_extractbit.cpp:20
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: bitvector_types.h:159
address_bits
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
Definition: arith_tools.cpp:177
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:96
bitvector_types.h
Pre-defined bitvector types.
std_types.h
Pre-defined types.
extractbit_exprt::index
exprt & index()
Definition: bitvector_expr.h:378
irept::id
const irep_idt & id() const
Definition: irep.h:407
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:47
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:154
prop_conv_solvert::convert_rest
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv_solver.cpp:335
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: bitvector_expr.h:363
propt::lequal
virtual literalt lequal(literalt a, literalt b)=0
extractbit_exprt::src
exprt & src()
Definition: bitvector_expr.h:373
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
literalt
Definition: literal.h:26
propt::has_set_to
virtual bool has_set_to() const
Definition: prop.h:81
boolbv.h
std_expr.h
API to expression classes.
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
bitvector_expr.h
API to expression classes for bitvectors.
equalityt::equality
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:128
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700