cprover
boolbv_extractbits.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
11#include <util/arith_tools.h>
12#include <util/bitvector_expr.h>
13
15{
16 const std::size_t bv_width = boolbv_width(expr.type());
17
18 if(bv_width == 0)
19 return conversion_failed(expr);
20
21 auto const &src_bv = convert_bv(expr.src());
22
23 auto const maybe_upper_as_int = numeric_cast<mp_integer>(expr.upper());
24 auto const maybe_lower_as_int = numeric_cast<mp_integer>(expr.lower());
25
26 // We only do constants for now.
27 // Should implement a shift here.
28 if(!maybe_upper_as_int.has_value() || !maybe_lower_as_int.has_value())
29 return conversion_failed(expr);
30
31 auto upper_as_int = maybe_upper_as_int.value();
32 auto lower_as_int = maybe_lower_as_int.value();
33
35 upper_as_int >= 0 && upper_as_int < src_bv.size(),
36 "upper end of extracted bits must be within the bitvector",
39
41 lower_as_int >= 0 && lower_as_int < src_bv.size(),
42 "lower end of extracted bits must be within the bitvector",
45
47 lower_as_int <= upper_as_int,
48 "upper bound must be greater or equal to lower bound");
49
50 // now lower_as_int <= upper_as_int
51
53 (upper_as_int - lower_as_int + 1) == bv_width,
54 "the difference between upper and lower end of the range must have the "
55 "same width as the resulting bitvector type",
58
59 const std::size_t offset = numeric_cast_v<std::size_t>(lower_as_int);
60
61 bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset + bv_width);
62
63 return result_bv;
64}
API to expression classes for bitvectors.
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:40
boolbv_widtht bv_width
Definition: boolbv.h:113
virtual bvt convert_extractbits(const extractbits_exprt &expr)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition: boolbv.cpp:84
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:99
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
typet & type()
Return the type of the expression.
Definition: expr.h:82
Extracts a sub-range of a bit-vector operand.
std::vector< literalt > bvt
Definition: literal.h:201
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:511