cprover
Loading...
Searching...
No Matches
boolbv_byte_extract.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/byte_operators.h>
13#include <util/pointer_expr.h>
15#include <util/std_expr.h>
16
18
19bvt map_bv(const endianness_mapt &map, const bvt &src)
20{
21 PRECONDITION(map.number_of_bits() == src.size());
22 bvt result;
23 result.reserve(src.size());
24
25 for(std::size_t i=0; i<src.size(); i++)
26 {
27 const size_t mapped_index = map.map_bit(i);
28 CHECK_RETURN(mapped_index < src.size());
29 result.push_back(src[mapped_index]);
30 }
31
32 return result;
33}
34
36{
37 // array logic does not handle byte operators, thus lower when operating on
38 // unbounded arrays
39 if(is_unbounded_array(expr.op().type()))
40 {
41 return convert_bv(lower_byte_extract(expr, ns));
42 }
43
44 const std::size_t width = boolbv_width(expr.type());
45
46 // special treatment for bit-fields and big-endian:
47 // we need byte granularity
48 #if 0
49 if(expr.id()==ID_byte_extract_big_endian &&
50 expr.type().id()==ID_c_bit_field &&
51 (width%8)!=0)
52 {
53 byte_extract_exprt tmp=expr;
54 // round up
55 to_c_bit_field_type(tmp.type()).set_width(width+8-width%8);
56 convert_byte_extract(tmp, bv);
57 bv.resize(width); // chop down
58 return;
59 }
60 #endif
61
62 if(width==0)
63 return conversion_failed(expr);
64
65 // see if the byte number is constant and within bounds, else work from the
66 // root object
67 const auto op_bytes_opt = pointer_offset_size(expr.op().type(), ns);
68 auto index = numeric_cast<mp_integer>(expr.offset());
69
70 if(
71 (!index.has_value() || !op_bytes_opt.has_value() ||
72 *index < 0 || *index >= *op_bytes_opt) &&
73 (expr.op().id() == ID_member ||
74 expr.op().id() == ID_index ||
75 expr.op().id() == ID_byte_extract_big_endian ||
76 expr.op().id() == ID_byte_extract_little_endian))
77 {
79 o.build(expr.op(), ns);
80 CHECK_RETURN(o.offset().id() != ID_unknown);
81
82 o.offset() =
84
86 expr.id(),
87 o.root_object(),
88 plus_exprt(o.offset(), expr.offset()),
89 expr.type());
90
91 return convert_bv(be);
92 }
93
94 const exprt &op=expr.op();
96 expr.id() == ID_byte_extract_little_endian ||
97 expr.id() == ID_byte_extract_big_endian);
98 const bool little_endian = expr.id() == ID_byte_extract_little_endian;
99
100 // first do op0
101 const endianness_mapt op_map = endianness_map(op.type(), little_endian);
102 const bvt op_bv=map_bv(op_map, convert_bv(op));
103
104 // do result
105 endianness_mapt result_map = endianness_map(expr.type(), little_endian);
106 bvt bv;
107 bv.resize(width);
108
109 // see if the byte number is constant
110 unsigned byte_width=8;
111
112 if(index.has_value())
113 {
114 const mp_integer offset = *index * byte_width;
115
116 for(std::size_t i=0; i<width; i++)
117 // out of bounds?
118 if(offset + i < 0 || offset + i >= op_bv.size())
119 bv[i]=prop.new_variable();
120 else
121 bv[i] = op_bv[numeric_cast_v<std::size_t>(offset + i)];
122 }
123 else
124 {
125 std::size_t bytes=op_bv.size()/byte_width;
126
127 if(prop.has_set_to())
128 {
129 // free variables
130 bv = prop.new_variables(width);
131
132 // add implications
133
134 // type of index operand
135 const typet &constant_type = expr.offset().type();
136
137 bvt equal_bv;
138 equal_bv.resize(width);
139
140 for(std::size_t i=0; i<bytes; i++)
141 {
142 std::size_t offset=i*byte_width;
143
144 for(std::size_t j=0; j<width; j++)
145 if(offset+j<op_bv.size())
146 equal_bv[j]=prop.lequal(bv[j], op_bv[offset+j]);
147 else
148 equal_bv[j]=const_literal(true);
149
151 convert(equal_exprt(expr.offset(), from_integer(i, constant_type))),
152 prop.land(equal_bv)));
153 }
154 }
155 else
156 {
157 // type of index operand
158 const typet &constant_type = expr.offset().type();
159
160 for(std::size_t i=0; i<bytes; i++)
161 {
162 literalt e =
163 convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));
164
165 std::size_t offset=i*byte_width;
166
167 for(std::size_t j=0; j<width; j++)
168 {
169 literalt l;
170
171 if(offset+j<op_bv.size())
172 l=op_bv[offset+j];
173 else
174 l=const_literal(false);
175
176 if(i==0)
177 bv[j]=l;
178 else
179 bv[j]=prop.lselect(e, l, bv[j]);
180 }
181 }
182 }
183 }
184
185 // shuffle the result
186 bv=map_bv(result_map, bv);
187
188 return bv;
189}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bvt map_bv(const endianness_mapt &map, const bvt &src)
Expression classes for byte-level operators.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:58
const namespacet & ns
Definition: arrays.h:56
void set_width(std::size_t width)
Definition: std_types.h:869
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:547
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
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 endianness_mapt endianness_map(const typet &type, bool little_endian) const
Definition: boolbv.h:105
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:99
Expression of type type extracted from some object op starting at position offset (given in number of...
Maps a big-endian offset to a little-endian offset.
size_t number_of_bits() const
size_t map_bit(size_t bit) const
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
const irep_idt & id() const
Definition: irep.h:396
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:167
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
The plus expression Associativity is not specified.
Definition: std_expr.h:914
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
void l_set_to_true(literalt a)
Definition: prop.h:51
virtual literalt land(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
virtual literalt new_variable()=0
virtual literalt lequal(literalt a, literalt b)=0
virtual bool has_set_to() const
Definition: prop.h:80
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
std::vector< literalt > bvt
Definition: literal.h:201
literalt const_literal(bool value)
Definition: literal.h:188
API to expression classes for Pointers.
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Pointer Logic.
BigInt mp_integer
Definition: smt_terms.h:12
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.