cprover
Loading...
Searching...
No Matches
boolbv_extractbit.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 <algorithm>
12
13#include <util/arith_tools.h>
14#include <util/bitvector_expr.h>
17#include <util/std_expr.h>
18
20{
21 const bvt &src_bv = convert_bv(expr.src());
22 const auto &index = expr.index();
23
24 // constant?
25 if(index.is_constant())
26 {
27 mp_integer index_as_integer =
29
30 if(index_as_integer < 0 || index_as_integer >= src_bv.size())
31 return prop.new_variable(); // out of range!
32 else
33 return src_bv[numeric_cast_v<std::size_t>(index_as_integer)];
34 }
35
36 if(
37 expr.src().type().id() == ID_verilog_signedbv ||
38 expr.src().type().id() == ID_verilog_unsignedbv)
39 {
41 "extractbit expression not implemented for verilog integers in "
42 "flattening solver");
43 }
44 else
45 {
46 std::size_t src_bv_width = boolbv_width(expr.src().type());
47 std::size_t index_bv_width = boolbv_width(index.type());
48
49 if(src_bv_width == 0 || index_bv_width == 0)
50 return SUB::convert_rest(expr);
51
52 std::size_t index_width =
53 std::max(address_bits(src_bv_width), index_bv_width);
54 unsignedbv_typet index_type(index_width);
55
56 const auto index_casted =
57 typecast_exprt::conditional_cast(index, index_type);
58
59 if(prop.has_set_to())
60 {
61 // free variable
62 literalt literal = prop.new_variable();
63
64 // add implications
65 for(std::size_t i = 0; i < src_bv.size(); i++)
66 {
67 equal_exprt equality(index_casted, from_integer(i, index_type));
68 literalt equal = prop.lequal(literal, src_bv[i]);
69 prop.l_set_to_true(prop.limplies(convert(equality), equal));
70 }
71
72 return literal;
73 }
74 else
75 {
76 literalt literal = prop.new_variable();
77
78 for(std::size_t i = 0; i < src_bv.size(); i++)
79 {
80 equal_exprt equality(index_casted, from_integer(i, index_type));
81 literal = prop.lselect(convert(equality), src_bv[i], literal);
82 }
83
84 return literal;
85 }
86 }
87}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
API to expression classes for bitvectors.
Pre-defined bitvector types.
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:39
virtual literalt convert_extractbit(const extractbit_exprt &expr)
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:103
Equality.
Definition std_expr.h:1366
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition equality.cpp:17
typet & type()
Return the type of the expression.
Definition expr.h:84
Extracts a single bit of a bit-vector operand.
const irep_idt & id() const
Definition irep.h:388
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
virtual literalt convert_rest(const exprt &expr)
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
Fixed-width bit-vector with unsigned binary interpretation.
Thrown when we encounter an instruction, parameters to an instruction etc.
std::vector< literalt > bvt
Definition literal.h:201
BigInt mp_integer
Definition smt_terms.h:17
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3173