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