cprover
boolbv_extractbits.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 <util/arith_tools.h>
12 
14 {
15  const std::size_t bv_width = boolbv_width(expr.type());
16 
17  if(bv_width == 0)
18  return conversion_failed(expr);
19 
20  auto const &src_bv = convert_bv(expr.src());
21 
22  auto const maybe_upper_as_int = numeric_cast<mp_integer>(expr.upper());
23  auto const maybe_lower_as_int = numeric_cast<mp_integer>(expr.lower());
24 
25  // We only do constants for now.
26  // Should implement a shift here.
27  if(!maybe_upper_as_int.has_value() || !maybe_lower_as_int.has_value())
28  return conversion_failed(expr);
29 
30  auto upper_as_int = maybe_upper_as_int.value();
31  auto lower_as_int = maybe_lower_as_int.value();
32 
34  upper_as_int >= 0 && upper_as_int < src_bv.size(),
35  "upper end of extracted bits must be within the bitvector",
36  expr.find_source_location(),
38 
40  lower_as_int >= 0 && lower_as_int < src_bv.size(),
41  "lower end of extracted bits must be within the bitvector",
42  expr.find_source_location(),
44 
46  lower_as_int <= upper_as_int,
47  "upper bound must be greater or equal to lower bound");
48 
49  // now lower_as_int <= upper_as_int
50 
52  (upper_as_int - lower_as_int + 1) == bv_width,
53  "the difference between upper and lower end of the range must have the "
54  "same width as the resulting bitvector type",
55  expr.find_source_location(),
57 
58  const std::size_t offset = numeric_cast_v<std::size_t>(lower_as_int);
59 
60  bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset + bv_width);
61 
62  return result_bv;
63 }
extractbits_exprt::lower
exprt & lower()
Definition: std_expr.h:2728
arith_tools.h
bvt
std::vector< literalt > bvt
Definition: literal.h:201
extractbits_exprt::upper
exprt & upper()
Definition: std_expr.h:2723
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
DATA_INVARIANT_WITH_DIAGNOSTICS
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:512
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
boolbvt::convert_extractbits
virtual bvt convert_extractbits(const extractbits_exprt &expr)
Definition: boolbv_extractbits.cpp:13
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:231
extractbits_exprt::src
exprt & src()
Definition: std_expr.h:2718
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:119
irep_pretty_diagnosticst
Definition: irep.h:524
boolbv.h
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2697