cprover
Loading...
Searching...
No Matches
boolbv_with.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/c_types.h>
13#include <util/namespace.h>
14#include <util/std_expr.h>
15
17{
18 bvt bv = convert_bv(expr.old());
19
20 std::size_t width=boolbv_width(expr.type());
21
22 if(width==0)
23 {
24 // A zero-length array is acceptable:
25 if(
26 expr.type().id() == ID_array &&
28 {
29 return bvt();
30 }
31 else
32 return conversion_failed(expr);
33 }
34
36 bv.size() == width,
37 "unexpected operand 0 width",
39
41 prev_bv.resize(width);
42
43 const exprt::operandst &ops=expr.operands();
44
45 for(std::size_t op_no=1; op_no<ops.size(); op_no+=2)
46 {
47 bv.swap(prev_bv);
48
49 convert_with(expr.old().type(), ops[op_no], ops[op_no + 1], prev_bv, bv);
50 }
51
52 return bv;
53}
54
56 const typet &type,
57 const exprt &op1,
58 const exprt &op2,
59 const bvt &prev_bv,
60 bvt &next_bv)
61{
62 // we only do that on arrays, bitvectors, structs, and unions
63
64 next_bv.resize(prev_bv.size());
65
66 if(type.id()==ID_array)
67 return convert_with_array(to_array_type(type), op1, op2, prev_bv, next_bv);
68 else if(type.id()==ID_bv ||
69 type.id()==ID_unsignedbv ||
70 type.id()==ID_signedbv)
71 return convert_with_bv(op1, op2, prev_bv, next_bv);
72 else if(type.id()==ID_struct)
73 return
75 else if(type.id() == ID_struct_tag)
76 return convert_with(
78 else if(type.id()==ID_union)
80 else if(type.id() == ID_union_tag)
81 return convert_with(
82 ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
83
85 false, "unexpected with type", irep_pretty_diagnosticst{type});
86}
87
89 const array_typet &type,
90 const exprt &op1,
91 const exprt &op2,
92 const bvt &prev_bv,
93 bvt &next_bv)
94{
95 // can't do this
97 !is_unbounded_array(type),
98 "convert_with_array called for unbounded array",
100
101 const exprt &array_size=type.size();
102
103 const auto size = numeric_cast<mp_integer>(array_size);
104
106 size.has_value(),
107 "convert_with_array expects constant array size",
109
110 const bvt &op2_bv=convert_bv(op2);
111
113 *size * op2_bv.size() == prev_bv.size(),
114 "convert_with_array: unexpected operand 2 width",
116
117 // Is the index a constant?
118 if(const auto op1_value = numeric_cast<mp_integer>(op1))
119 {
120 // Yes, it is!
122
123 if(*op1_value >= 0 && *op1_value < *size) // bounds check
124 {
125 const std::size_t offset =
126 numeric_cast_v<std::size_t>(*op1_value * op2_bv.size());
127
128 for(std::size_t j=0; j<op2_bv.size(); j++)
129 next_bv[offset+j]=op2_bv[j];
130 }
131
132 return;
133 }
134
135 typet counter_type=op1.type();
136
137 for(mp_integer i=0; i<size; i=i+1)
138 {
140
142
143 const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());
144
145 for(std::size_t j=0; j<op2_bv.size(); j++)
146 next_bv[offset+j]=
147 prop.lselect(eq_lit, op2_bv[j], prev_bv[offset+j]);
148 }
149}
150
152 const exprt &op1,
153 const exprt &op2,
154 const bvt &prev_bv,
155 bvt &next_bv)
156{
157 literalt l=convert(op2);
158
159 if(const auto op1_value = numeric_cast<mp_integer>(op1))
160 {
162
163 if(*op1_value < next_bv.size())
164 next_bv[numeric_cast_v<std::size_t>(*op1_value)] = l;
165
166 return;
167 }
168
169 typet counter_type=op1.type();
170
171 for(std::size_t i=0; i<prev_bv.size(); i++)
172 {
174
176
178 }
179}
180
182 const struct_typet &type,
183 const exprt &op1,
184 const exprt &op2,
185 const bvt &prev_bv,
186 bvt &next_bv)
187{
189
190 const bvt &op2_bv=convert_bv(op2);
191
192 const irep_idt &component_name=op1.get(ID_component_name);
193 const struct_typet::componentst &components=
194 type.components();
195
196 std::size_t offset=0;
197
198 for(const auto &c : components)
199 {
200 const typet &subtype = c.type();
201
202 std::size_t sub_width=boolbv_width(subtype);
203
204 if(c.get_name() == component_name)
205 {
207 subtype == op2.type(),
208 "with/struct: component '" + id2string(component_name) +
209 "' type does not match",
212
214 sub_width == op2_bv.size(),
215 "convert_with_struct: unexpected operand op2 width",
217
218 for(std::size_t i=0; i<sub_width; i++)
219 next_bv[offset+i]=op2_bv[i];
220
221 break; // done
222 }
223
224 offset+=sub_width;
225 }
226}
227
229 const union_typet &type,
230 const exprt &op2,
231 const bvt &prev_bv,
232 bvt &next_bv)
233{
235
236 const bvt &op2_bv=convert_bv(op2);
237
239 next_bv.size() >= op2_bv.size(),
240 "convert_with_union: unexpected operand op2 width",
242
245
246 for(std::size_t i = 0; i < op2_bv.size(); i++)
247 next_bv[map_u.map_bit(i)] = op2_bv[map_op2.map_bit(i)];
248}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:162
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:202
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Arrays with given size.
Definition std_types.h:763
const exprt & size() const
Definition std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:777
const namespacet & ns
Definition arrays.h:56
virtual bvt convert_with(const with_exprt &expr)
void convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
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
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
void convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
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
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Maps a big-endian offset to a little-endian offset.
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
const irep_idt & id() const
Definition irep.h:396
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
The type of an expression, extends irept.
Definition type.h:29
The union type.
Definition c_types.h:125
Operator to update elements in structs and arrays.
Definition std_expr.h:2312
exprt & old()
Definition std_expr.h:2322
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
std::vector< literalt > bvt
Definition literal.h:201
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition invariant.h:511
API to expression classes.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832