cprover
simplify_utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
60 struct saj_tablet
61 {
62  const irep_idt id;
63  const irep_idt type_ids[10];
64 } const saj_table[]=
65 {
66  { ID_plus, {ID_integer ,
67  ID_natural ,
68  ID_real ,
69  ID_complex ,
70  ID_rational ,
71  ID_unsignedbv ,
72  ID_signedbv ,
73  ID_fixedbv ,
74  irep_idt() }},
75  { ID_mult, {ID_integer ,
76  ID_natural ,
77  ID_real ,
78  ID_complex ,
79  ID_rational ,
80  ID_unsignedbv ,
81  ID_signedbv ,
82  ID_fixedbv ,
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() }},
90  { ID_bitand, {ID_unsignedbv ,
91  ID_signedbv ,
92  ID_floatbv ,
93  ID_fixedbv ,
94  irep_idt() }},
95  { ID_bitor, {ID_unsignedbv ,
96  ID_signedbv ,
97  ID_floatbv ,
98  ID_fixedbv ,
99  irep_idt() }},
100  { ID_bitxor, {ID_unsignedbv ,
101  ID_signedbv ,
102  ID_floatbv ,
103  ID_fixedbv ,
104  irep_idt() }},
105  { irep_idt(), { irep_idt() }}
106 };
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 
119 static 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 
135 static 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)
150  if(!is_associative_and_commutative_for_type(saj_entry, it->type().id()))
151  return true;
152 
153  // join expressions
154 
155  exprt::operandst new_ops;
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)
175  no_change = sort_operands(new_ops) && no_change;
176 
177  if(!no_change)
178  expr.operands().swap(new_ops);
179 
180  return no_change;
181 }
182 
183 bool sort_and_join(exprt &expr)
184 {
185  return sort_and_join(expr, true);
186 }
187 
188 bool join_operands(exprt &expr)
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  {
222  return null_pointer_exprt(to_pointer_type(type));
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 =
239  bits2expr(bits, to_c_enum_type(type).subtype(), 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  {
289  const struct_typet &struct_type = to_struct_type(type);
290  const struct_typet::componentst &components = struct_type.components();
291 
292  struct_exprt result({}, type);
293  result.reserve_operands(components.size());
294 
295  mp_integer m_offset_bits = 0;
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,
303  numeric_cast_v<std::size_t>(m_offset_bits),
304  numeric_cast_v<std::size_t>(*m_size));
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 =
336  numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
337 
338  const auto el_size_opt = pointer_offset_bits(array_type.subtype(), 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);
344  result.reserve_operands(number_of_elements);
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 = bits2expr(el_bits, array_type.subtype(), little_endian, ns);
350  if(!el.has_value())
351  return {};
352  result.add_to_operands(std::move(*el));
353  }
354 
355  return std::move(result);
356  }
357  else if(type.id() == ID_vector)
358  {
359  const vector_typet &vector_type = to_vector_type(type);
360 
361  const std::size_t n_el = numeric_cast_v<std::size_t>(vector_type.size());
362 
363  const auto el_size_opt = pointer_offset_bits(vector_type.subtype(), ns);
364  CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
365 
366  const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
367 
368  vector_exprt result({}, vector_type);
369  result.reserve_operands(n_el);
370 
371  for(std::size_t i = 0; i < n_el; ++i)
372  {
373  std::string el_bits = std::string(bits, i * el_size, el_size);
374  auto el = bits2expr(el_bits, vector_type.subtype(), little_endian, ns);
375  if(!el.has_value())
376  return {};
377  result.add_to_operands(std::move(*el));
378  }
379 
380  return std::move(result);
381  }
382  else if(type.id() == ID_complex)
383  {
384  const complex_typet &complex_type = to_complex_type(type);
385 
386  const auto sub_size_opt = pointer_offset_bits(complex_type.subtype(), ns);
387  CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > 0);
388 
389  const std::size_t sub_size = numeric_cast_v<std::size_t>(*sub_size_opt);
390 
391  auto real = bits2expr(
392  bits.substr(0, sub_size), complex_type.subtype(), little_endian, ns);
393  auto imag = bits2expr(
394  bits.substr(sub_size), complex_type.subtype(), little_endian, ns);
395  if(!real.has_value() || !imag.has_value())
396  return {};
397 
398  return complex_exprt(*real, *imag, complex_type);
399  }
400 
401  return {};
402 }
403 
405 expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
406 {
407  // extract bits from lowest to highest memory address
408  const typet &type = expr.type();
409 
410  if(expr.id() == ID_constant)
411  {
412  const auto &value = to_constant_expr(expr).get_value();
413 
414  if(
415  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
416  type.id() == ID_floatbv || type.id() == ID_fixedbv ||
417  type.id() == ID_c_bit_field || type.id() == ID_bv ||
418  type.id() == ID_c_bool)
419  {
420  const auto width = to_bitvector_type(type).get_width();
421 
422  endianness_mapt map(type, little_endian, ns);
423 
424  std::string result(width, ' ');
425 
426  for(std::string::size_type i = 0; i < width; ++i)
427  result[map.map_bit(i)] = get_bvrep_bit(value, width, i) ? '1' : '0';
428 
429  return result;
430  }
431  else if(type.id() == ID_pointer)
432  {
433  if(value == ID_NULL && config.ansi_c.NULL_is_zero)
434  return std::string(to_bitvector_type(type).get_width(), '0');
435  else
436  return {};
437  }
438  else if(type.id() == ID_c_enum_tag)
439  {
440  const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(type));
441  return expr2bits(constant_exprt(value, c_enum_type), little_endian, ns);
442  }
443  else if(type.id() == ID_c_enum)
444  {
445  return expr2bits(
446  constant_exprt(value, to_c_enum_type(type).subtype()),
447  little_endian,
448  ns);
449  }
450  }
451  else if(expr.id() == ID_string_constant)
452  {
453  return expr2bits(
454  to_string_constant(expr).to_array_expr(), little_endian, ns);
455  }
456  else if(expr.id() == ID_union)
457  {
458  return expr2bits(to_union_expr(expr).op(), little_endian, ns);
459  }
460  else if(
461  expr.id() == ID_struct || expr.id() == ID_array || expr.id() == ID_vector ||
462  expr.id() == ID_complex)
463  {
464  std::string result;
465  forall_operands(it, expr)
466  {
467  auto tmp = expr2bits(*it, little_endian, ns);
468  if(!tmp.has_value())
469  return {}; // failed
470  result += tmp.value();
471  }
472 
473  return result;
474  }
475 
476  return {};
477 }
478 
480 try_get_string_data_array(const exprt &content, const namespacet &ns)
481 {
482  if(content.id() != ID_address_of)
483  {
484  return {};
485  }
486 
487  const auto &array_pointer = to_address_of_expr(content);
488 
489  if(array_pointer.object().id() != ID_index)
490  {
491  return {};
492  }
493 
494  const auto &array_start = to_index_expr(array_pointer.object());
495 
496  if(
497  array_start.array().id() != ID_symbol ||
498  array_start.array().type().id() != ID_array)
499  {
500  return {};
501  }
502 
503  const auto &array = to_symbol_expr(array_start.array());
504 
505  const symbolt *symbol_ptr = nullptr;
506 
507  if(
508  ns.lookup(array.get_identifier(), symbol_ptr) ||
509  symbol_ptr->value.id() != ID_array)
510  {
511  return {};
512  }
513 
514  const auto &char_seq = to_array_expr(symbol_ptr->value);
515 
517 }
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.
unsignedbv_typet size_type()
Definition: c_types.cpp:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:277
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
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:317
Array constructor from list of elements.
Definition: std_expr.h:1467
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:771
std::size_t get_width() const
Definition: std_types.h:843
Complex constructor from a pair of numbers.
Definition: std_expr.h:1707
Complex numbers made of pair of given subtype.
Definition: std_types.h:1015
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition: std_expr.h:2753
const irep_idt & get_value() const
Definition: std_expr.h:2761
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
size_t size() const
Definition: dstring.h:104
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:407
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().
Definition: namespace.cpp:138
The null pointer constant.
Definition: pointer_expr.h:703
Struct constructor from list of elements.
Definition: std_expr.h:1668
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
Symbol table entry.
Definition: symbol.h:28
exprt value
Initial value of symbol.
Definition: symbol.h:34
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
Union constructor from single element.
Definition: std_expr.h:1602
The union type.
Definition: c_types.h:112
Vector constructor from list of elements.
Definition: std_expr.h:1566
The vector type.
Definition: std_types.h:975
const constant_exprt & size() const
Definition: std_types.cpp:239
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
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
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< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
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.
BigInt mp_integer
Definition: smt_terms.h:12
#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 constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1497
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1648
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1000
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1040
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 string_constantt & to_string_constant(const exprt &expr)
bool NULL_is_zero
Definition: config.h:167
produce canonical ordering for associative and commutative binary operators
const irep_idt id
const irep_idt type_ids[10]
Symbol table entry.