cprover
Loading...
Searching...
No Matches
simplify_utils.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "simplify_utils.h"
10
11#include "arith_tools.h"
12#include "c_types.h"
13#include "config.h"
14#include "endianness_map.h"
15#include "namespace.h"
16#include "pointer_expr.h"
17#include "pointer_offset_size.h"
18#include "std_expr.h"
19#include "string_constant.h"
20#include "symbol.h"
21
22#include <algorithm>
23
28{
29 bool do_sort=false;
30
31 forall_expr(it, operands)
32 {
33 exprt::operandst::const_iterator next_it=it;
34 next_it++;
35
36 if(next_it!=operands.end() && *next_it < *it)
37 {
38 do_sort=true;
39 break;
40 }
41 }
42
43 if(!do_sort)
44 return true;
45
46 std::sort(operands.begin(), operands.end());
47
48 return false;
49}
50
52// The entries
53// { ID_plus, ID_floatbv },
54// { ID_mult, ID_floatbv },
55// { ID_plus, ID_pointer },
56// are deliberately missing, as FP-addition and multiplication
57// aren't associative. Addition to pointers isn't really
58// associative.
59
61{
62 const irep_idt id;
63 const irep_idt type_ids[10];
64} const saj_table[]=
65{
68 ID_real ,
74 irep_idt() }},
77 ID_real ,
83 irep_idt() }},
84 { ID_and, {ID_bool ,
85 irep_idt() }},
86 { ID_or, {ID_bool ,
87 irep_idt() }},
88 { ID_xor, {ID_bool ,
89 irep_idt() }},
94 irep_idt() }},
99 irep_idt() }},
102 ID_floatbv ,
103 ID_fixedbv ,
104 irep_idt() }},
105 { irep_idt(), { irep_idt() }}
107
109 const struct saj_tablet &saj_entry,
110 const irep_idt &type_id)
111{
112 for(unsigned i=0; !saj_entry.type_ids[i].empty(); i++)
113 if(type_id==saj_entry.type_ids[i])
114 return true;
115
116 return false;
117}
118
119static const struct saj_tablet &
121{
122 unsigned i=0;
123
124 for( ; !saj_table[i].id.empty(); i++)
125 {
126 if(
127 id == saj_table[i].id &&
129 return saj_table[i];
130 }
131
132 return saj_table[i];
133}
134
135static bool sort_and_join(exprt &expr, bool do_sort)
136{
137 bool no_change = true;
138
139 if(!expr.has_operands())
140 return true;
141
142 const struct saj_tablet &saj_entry =
143 get_sort_and_join_table_entry(expr.id(), as_const(expr).type().id());
144 if(saj_entry.id.empty())
145 return true;
146
147 // check operand types
148
149 forall_operands(it, expr)
151 return true;
152
153 // join expressions
154
156 new_ops.reserve(as_const(expr).operands().size());
157
158 forall_operands(it, expr)
159 {
160 if(it->id()==expr.id())
161 {
162 new_ops.reserve(new_ops.capacity()+it->operands().size()-1);
163
164 forall_operands(it2, *it)
165 new_ops.push_back(*it2);
166
167 no_change = false;
168 }
169 else
170 new_ops.push_back(*it);
171 }
172
173 // sort it
174 if(do_sort)
176
177 if(!no_change)
178 expr.operands().swap(new_ops);
179
180 return no_change;
181}
182
184{
185 return sort_and_join(expr, true);
186}
187
189{
190 return sort_and_join(expr, false);
191}
192
194 const std::string &bits,
195 const typet &type,
196 bool little_endian,
197 const namespacet &ns)
198{
199 // bits start at lowest memory address
200 auto type_bits = pointer_offset_bits(type, ns);
201
202 if(
203 !type_bits.has_value() ||
204 (type.id() != ID_union && type.id() != ID_union_tag &&
205 *type_bits != bits.size()) ||
206 ((type.id() == ID_union || type.id() == ID_union_tag) &&
207 *type_bits < bits.size()))
208 {
209 return {};
210 }
211
212 if(
213 type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
214 type.id() == ID_floatbv || type.id() == ID_fixedbv ||
215 type.id() == ID_c_bit_field || type.id() == ID_pointer ||
216 type.id() == ID_bv || type.id() == ID_c_bool)
217 {
218 if(
219 type.id() == ID_pointer && config.ansi_c.NULL_is_zero &&
220 bits.find('1') == std::string::npos)
221 {
223 }
224
225 endianness_mapt map(type, little_endian, ns);
226
227 std::string tmp = bits;
228 for(std::string::size_type i = 0; i < bits.size(); ++i)
229 tmp[i] = bits[map.map_bit(i)];
230
231 std::reverse(tmp.begin(), tmp.end());
232
233 mp_integer i = binary2integer(tmp, false);
234 return constant_exprt(integer2bvrep(i, bits.size()), type);
235 }
236 else if(type.id() == ID_c_enum)
237 {
238 auto val = bits2expr(
239 bits, to_c_enum_type(type).underlying_type(), little_endian, ns);
240 if(val.has_value())
241 {
242 val->type() = type;
243 return *val;
244 }
245 else
246 return {};
247 }
248 else if(type.id() == ID_c_enum_tag)
249 {
250 auto val = bits2expr(
251 bits, ns.follow_tag(to_c_enum_tag_type(type)), little_endian, ns);
252 if(val.has_value())
253 {
254 val->type() = type;
255 return *val;
256 }
257 else
258 return {};
259 }
260 else if(type.id() == ID_union)
261 {
262 // find a suitable member
263 const union_typet &union_type = to_union_type(type);
264 const union_typet::componentst &components = union_type.components();
265
266 for(const auto &component : components)
267 {
268 auto val = bits2expr(bits, component.type(), little_endian, ns);
269 if(!val.has_value())
270 continue;
271
272 return union_exprt(component.get_name(), *val, type);
273 }
274 }
275 else if(type.id() == ID_union_tag)
276 {
277 auto val = bits2expr(
278 bits, ns.follow_tag(to_union_tag_type(type)), little_endian, ns);
279 if(val.has_value())
280 {
281 val->type() = type;
282 return *val;
283 }
284 else
285 return {};
286 }
287 else if(type.id() == ID_struct)
288 {
290 const struct_typet::componentst &components = struct_type.components();
291
292 struct_exprt result({}, type);
293 result.reserve_operands(components.size());
294
296 for(const auto &component : components)
297 {
298 const auto m_size = pointer_offset_bits(component.type(), ns);
299 CHECK_RETURN(m_size.has_value() && *m_size >= 0);
300
301 std::string comp_bits = std::string(
302 bits,
305
306 auto comp = bits2expr(comp_bits, component.type(), little_endian, ns);
307 if(!comp.has_value())
308 return {};
309 result.add_to_operands(std::move(*comp));
310
311 m_offset_bits += *m_size;
312 }
313
314 return std::move(result);
315 }
316 else if(type.id() == ID_struct_tag)
317 {
318 auto val = bits2expr(
319 bits, ns.follow_tag(to_struct_tag_type(type)), little_endian, ns);
320 if(val.has_value())
321 {
322 val->type() = type;
323 return *val;
324 }
325 else
326 return {};
327 }
328 else if(type.id() == ID_array)
329 {
330 const array_typet &array_type = to_array_type(type);
331 const auto &size_expr = array_type.size();
332
333 PRECONDITION(size_expr.is_constant());
334
335 const std::size_t number_of_elements =
337
338 const auto el_size_opt = pointer_offset_bits(array_type.element_type(), ns);
339 CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
340
341 const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
342
343 array_exprt result({}, array_type);
345
346 for(std::size_t i = 0; i < number_of_elements; ++i)
347 {
348 std::string el_bits = std::string(bits, i * el_size, el_size);
349 auto el =
350 bits2expr(el_bits, array_type.element_type(), little_endian, ns);
351 if(!el.has_value())
352 return {};
353 result.add_to_operands(std::move(*el));
354 }
355
356 return std::move(result);
357 }
358 else if(type.id() == ID_vector)
359 {
361
362 const std::size_t n_el = numeric_cast_v<std::size_t>(vector_type.size());
363
364 const auto el_size_opt =
365 pointer_offset_bits(vector_type.element_type(), ns);
366 CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
367
368 const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
369
370 vector_exprt result({}, vector_type);
371 result.reserve_operands(n_el);
372
373 for(std::size_t i = 0; i < n_el; ++i)
374 {
375 std::string el_bits = std::string(bits, i * el_size, el_size);
376 auto el =
377 bits2expr(el_bits, vector_type.element_type(), little_endian, ns);
378 if(!el.has_value())
379 return {};
380 result.add_to_operands(std::move(*el));
381 }
382
383 return std::move(result);
384 }
385 else if(type.id() == ID_complex)
386 {
388
389 const auto sub_size_opt = pointer_offset_bits(complex_type.subtype(), ns);
390 CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > 0);
391
393
394 auto real = bits2expr(
395 bits.substr(0, sub_size), complex_type.subtype(), little_endian, ns);
396 auto imag = bits2expr(
397 bits.substr(sub_size), complex_type.subtype(), little_endian, ns);
398 if(!real.has_value() || !imag.has_value())
399 return {};
400
401 return complex_exprt(*real, *imag, complex_type);
402 }
403
404 return {};
405}
406
408expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
409{
410 // extract bits from lowest to highest memory address
411 const typet &type = expr.type();
412
413 if(expr.id() == ID_constant)
414 {
415 const auto &value = to_constant_expr(expr).get_value();
416
417 if(
418 type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
419 type.id() == ID_floatbv || type.id() == ID_fixedbv ||
420 type.id() == ID_c_bit_field || type.id() == ID_bv ||
421 type.id() == ID_c_bool)
422 {
423 const auto width = to_bitvector_type(type).get_width();
424
425 endianness_mapt map(type, little_endian, ns);
426
427 std::string result(width, ' ');
428
429 for(std::string::size_type i = 0; i < width; ++i)
430 result[map.map_bit(i)] = get_bvrep_bit(value, width, i) ? '1' : '0';
431
432 return result;
433 }
434 else if(type.id() == ID_pointer)
435 {
436 if(value == ID_NULL && config.ansi_c.NULL_is_zero)
437 return std::string(to_bitvector_type(type).get_width(), '0');
438 else
439 return {};
440 }
441 else if(type.id() == ID_c_enum_tag)
442 {
443 const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(type));
444 return expr2bits(constant_exprt(value, c_enum_type), little_endian, ns);
445 }
446 else if(type.id() == ID_c_enum)
447 {
448 return expr2bits(
449 constant_exprt(value, to_c_enum_type(type).underlying_type()),
450 little_endian,
451 ns);
452 }
453 }
454 else if(expr.id() == ID_string_constant)
455 {
456 return expr2bits(
457 to_string_constant(expr).to_array_expr(), little_endian, ns);
458 }
459 else if(expr.id() == ID_union)
460 {
461 return expr2bits(to_union_expr(expr).op(), little_endian, ns);
462 }
463 else if(
464 expr.id() == ID_struct || expr.id() == ID_array || expr.id() == ID_vector ||
465 expr.id() == ID_complex)
466 {
467 std::string result;
468 forall_operands(it, expr)
469 {
470 auto tmp = expr2bits(*it, little_endian, ns);
471 if(!tmp.has_value())
472 return {}; // failed
473 result += tmp.value();
474 }
475
476 return result;
477 }
478
479 return {};
480}
481
484{
485 if(content.id() != ID_address_of)
486 {
487 return {};
488 }
489
490 const auto &array_pointer = to_address_of_expr(content);
491
492 if(array_pointer.object().id() != ID_index)
493 {
494 return {};
495 }
496
497 const auto &array_start = to_index_expr(array_pointer.object());
498
499 if(
500 array_start.array().id() != ID_symbol ||
501 array_start.array().type().id() != ID_array)
502 {
503 return {};
504 }
505
506 const auto &array = to_symbol_expr(array_start.array());
507
508 const symbolt *symbol_ptr = nullptr;
509
510 if(
511 ns.lookup(array.get_identifier(), symbol_ptr) ||
512 symbol_ptr->value.id() != ID_array)
513 {
514 return {};
515 }
516
517 const auto &char_seq = to_array_expr(symbol_ptr->value);
518
520}
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:302
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition c_types.h:344
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
Array constructor from list of elements.
Definition std_expr.h:1476
Arrays with given size.
Definition std_types.h:763
std::size_t get_width() const
Definition std_types.h:864
Complex constructor from a pair of numbers.
Definition std_expr.h:1761
Complex numbers made of pair of given subtype.
Definition std_types.h:1057
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition std_expr.h:2807
const irep_idt & get_value() const
Definition std_expr.h:2815
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.
size_t map_bit(size_t bit) const
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:89
void reserve_operands(operandst::size_type n)
Definition expr.h:124
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
Struct constructor from list of elements.
Definition std_expr.h:1722
Structure type, corresponds to C style structs.
Definition std_types.h:231
std::vector< componentt > componentst
Definition std_types.h:140
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
Union constructor from single element.
Definition std_expr.h:1611
The union type.
Definition c_types.h:125
Vector constructor from list of elements.
Definition std_expr.h:1575
The vector type.
Definition std_types.h:996
configt config
Definition config.cpp:25
#define forall_operands(it, expr)
Definition expr.h:18
#define forall_expr(it, expr)
Definition expr.h:30
dstringt irep_idt
Definition irep.h:37
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition mp_arith.cpp:117
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
struct saj_tablet saj_table[]
bool sort_operands(exprt::operandst &operands)
sort operands of an expression according to ordering defined by operator<
static const struct saj_tablet & get_sort_and_join_table_entry(const irep_idt &id, const irep_idt &type_id)
static bool is_associative_and_commutative_for_type(const struct saj_tablet &saj_entry, const irep_idt &type_id)
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
static bool sort_and_join(exprt &expr, bool do_sort)
bool join_operands(exprt &expr)
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)
Get char sequence from content field of a refined string expression.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:48
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1506
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1657
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1040
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 complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1082
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832
const string_constantt & to_string_constant(const exprt &expr)
produce canonical ordering for associative and commutative binary operators
const irep_idt id
const irep_idt type_ids[10]
Symbol table entry.