cprover
flatten_byte_operators.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
10 
11 #include <util/arith_tools.h>
12 #include <util/byte_operators.h>
13 #include <util/c_types.h>
14 #include <util/namespace.h>
16 #include <util/replace_symbol.h>
17 #include <util/simplify_expr.h>
18 
20 
31  const exprt &src,
32  bool little_endian,
33  const exprt &max_bytes,
34  const namespacet &ns,
35  bool unpack_byte_array=false)
36 {
37  array_exprt array(
39 
40  // endianness_mapt should be the point of reference for mapping out
41  // endianness, but we need to work on elements here instead of
42  // individual bits
43 
44  const typet &type=ns.follow(src.type());
45 
46  if(type.id()==ID_array)
47  {
48  const array_typet &array_type=to_array_type(type);
49  const typet &subtype=array_type.subtype();
50 
51  mp_integer element_width=pointer_offset_bits(subtype, ns);
52  // this probably doesn't really matter
53  #if 0
54  if(element_width<=0)
55  throw "cannot unpack array with non-constant element width:\n"+
56  type.pretty();
57  else if(element_width%8!=0)
58  throw "cannot unpack array of non-byte aligned elements:\n"+
59  type.pretty();
60  #endif
61 
62  if(!unpack_byte_array && element_width==8)
63  return src;
64 
65  mp_integer num_elements;
66  if(to_integer(max_bytes, num_elements) &&
67  to_integer(array_type.size(), num_elements))
68  {
69  throw non_const_array_sizet(array_type, max_bytes);
70  }
71 
72  // all array members will have the same structure; do this just
73  // once and then replace the dummy symbol by a suitable index
74  // expression in the loop below
75  symbol_exprt dummy(ID_C_incomplete, subtype);
76  exprt sub=unpack_rec(dummy, little_endian, max_bytes, ns, true);
77 
78  for(mp_integer i=0; i<num_elements; ++i)
79  {
80  index_exprt index(src, from_integer(i, index_type()));
81  replace_symbolt replace;
82  replace.insert(ID_C_incomplete, index);
83 
84  for(const auto &op : sub.operands())
85  {
86  exprt new_op=op;
87  replace(new_op);
88  simplify(new_op, ns);
89  array.copy_to_operands(new_op);
90  }
91  }
92  }
93  else if(type.id()==ID_struct)
94  {
95  const struct_typet &struct_type=to_struct_type(type);
96  const struct_typet::componentst &components=struct_type.components();
97 
98  for(const auto &comp : components)
99  {
100  mp_integer element_width=pointer_offset_bits(comp.type(), ns);
101 
102  // the next member would be misaligned, abort
103  if(element_width<=0 || element_width%8!=0)
104  {
105  throw non_byte_alignedt(struct_type, comp, element_width);
106  }
107 
108  member_exprt member(src, comp.get_name(), comp.type());
109  exprt sub=unpack_rec(member, little_endian, max_bytes, ns, true);
110 
111  for(const auto& op : sub.operands())
112  array.copy_to_operands(op);
113  }
114  }
115  else if(type.id()!=ID_empty)
116  {
117  // a basic type; we turn that into extractbits while considering
118  // endianness
119  mp_integer bits=pointer_offset_bits(type, ns);
120  if(bits<0)
121  {
122  if(to_integer(max_bytes, bits))
123  {
124  throw non_constant_widtht(src, max_bytes);
125  }
126  else
127  bits*=8;
128  }
129 
130  for(mp_integer i=0; i<bits; i+=8)
131  {
132  extractbits_exprt extractbits(
133  src,
134  from_integer(i+7, index_type()),
135  from_integer(i, index_type()),
136  unsignedbv_typet(8));
137 
138  if(little_endian)
139  array.copy_to_operands(extractbits);
140  else
141  array.operands().insert(array.operands().begin(), extractbits);
142  }
143  }
144 
145  to_array_type(array.type()).size()=
146  from_integer(array.operands().size(), size_type());
147 
148  return array;
149 }
150 
154  const byte_extract_exprt &src,
155  const namespacet &ns)
156 {
157  // General notes about endianness and the bit-vector conversion:
158  // A single byte with value 0b10001000 is stored (in irept) as
159  // exactly this string literal, and its bit-vector encoding will be
160  // bvt bv={0,0,0,1,0,0,0,1}, i.e., bv[0]==0 and bv[7]==1
161  //
162  // A multi-byte value like x=256 would be:
163  // - little-endian storage: ((char*)&x)[0]==0, ((char*)&x)[1]==1
164  // - big-endian storage: ((char*)&x)[0]==1, ((char*)&x)[1]==0
165  // - irept representation: 0000000100000000
166  // - bvt: {0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0}
167  // <... 8bits ...> <... 8bits ...>
168  //
169  // An array {0, 1} will be encoded as bvt bv={0,1}, i.e., bv[1]==1
170  // concatenation(0, 1) will yield a bvt bv={1,0}, i.e., bv[1]==0
171  //
172  // The semantics of byte_extract(endianness, op, offset, T) is:
173  // interpret ((char*)&op)+offset as the endianness-ordered storage
174  // of an object of type T at address ((char*)&op)+offset
175  // For some T x, byte_extract(endianness, x, 0, T) must yield x.
176  //
177  // byte_extract for a composite type T or an array will interpret
178  // the individual subtypes with suitable endianness; the overall
179  // order of components is not affected by endianness.
180  //
181  // Examples:
182  // unsigned char A[4];
183  // byte_extract_little_endian(A, 0, unsigned short) requests that
184  // A[0],A[1] be interpreted as the storage of an unsigned short with
185  // A[1] being the most-significant byte; byte_extract_big_endian for
186  // the same operands will select A[0] as the most-significant byte.
187  //
188  // int A[2] = {0x01020304,0xDEADBEEF}
189  // byte_extract_big_endian(A, 0, short) should yield 0x0102
190  // byte_extract_little_endian(A, 0, short) should yield 0x0304
191  // To obtain this we first compute byte arrays while taking into
192  // account endianness:
193  // big-endian byte representation: {01,02,03,04,DE,AB,BE,EF}
194  // little-endian byte representation: {04,03,02,01,EF,BE,AB,DE}
195  // We extract the relevant bytes starting from ((char*)A)+0:
196  // big-endian: {01,02}; little-endian: {04,03}
197  // Finally we place them in the appropriate byte order as indicated
198  // by endianness:
199  // big-endian: (short)concatenation(01,02)=0x0102
200  // little-endian: (short)concatenation(03,04)=0x0304
201 
202  assert(src.operands().size()==2);
203 
204  bool little_endian;
205 
206  if(src.id()==ID_byte_extract_little_endian)
207  little_endian=true;
208  else if(src.id()==ID_byte_extract_big_endian)
209  little_endian=false;
210  else
211  UNREACHABLE;
212 
213  // determine an upper bound of the number of bytes we might need
214  exprt upper_bound=size_of_expr(src.type(), ns);
215  if(upper_bound.is_not_nil())
216  upper_bound=
218  plus_exprt(
219  upper_bound,
220  typecast_exprt(src.offset(), upper_bound.type())),
221  ns);
222 
223  byte_extract_exprt unpacked(src);
224  unpacked.op()=
225  unpack_rec(src.op(), little_endian, upper_bound, ns);
226 
227  const typet &type=ns.follow(src.type());
228 
229  if(type.id()==ID_array)
230  {
231  const array_typet &array_type=to_array_type(type);
232  const typet &subtype=array_type.subtype();
233 
234  mp_integer element_width=pointer_offset_bits(subtype, ns);
235  mp_integer num_elements;
236  // TODO: consider ways of dealing with arrays of unknown subtype
237  // size or with a subtype size that does not fit byte boundaries
238  if(element_width>0 && element_width%8==0 &&
239  to_integer(array_type.size(), num_elements))
240  {
241  array_exprt array(array_type);
242 
243  for(mp_integer i=0; i<num_elements; ++i)
244  {
245  plus_exprt new_offset(
246  unpacked.offset(),
247  from_integer(i*element_width, unpacked.offset().type()));
248 
249  byte_extract_exprt tmp(unpacked);
250  tmp.type()=subtype;
251  tmp.offset()=new_offset;
252 
253  array.copy_to_operands(flatten_byte_extract(tmp, ns));
254  }
255 
256  return simplify_expr(array, ns);
257  }
258  }
259  else if(type.id()==ID_struct)
260  {
261  const struct_typet &struct_type=to_struct_type(type);
262  const struct_typet::componentst &components=struct_type.components();
263 
264  bool failed=false;
265  struct_exprt s(struct_type);
266 
267  for(const auto &comp : components)
268  {
269  mp_integer element_width=pointer_offset_bits(comp.type(), ns);
270 
271  // the next member would be misaligned, abort
272  if(element_width<=0 || element_width%8!=0)
273  {
274  failed=true;
275  break;
276  }
277 
278  plus_exprt new_offset(
279  unpacked.offset(),
281  member_offset_expr(struct_type, comp.get_name(), ns),
282  unpacked.offset().type()));
283 
284  byte_extract_exprt tmp(unpacked);
285  tmp.type()=comp.type();
286  tmp.offset()=new_offset;
287 
288  s.move_to_operands(tmp);
289  }
290 
291  if(!failed)
292  return simplify_expr(s, ns);
293  }
294 
295  const exprt &root=unpacked.op();
296  const exprt &offset=unpacked.offset();
297 
298  const array_typet &array_type=to_array_type(root.type());
299  const typet &subtype=array_type.subtype();
300 
301  DATA_INVARIANT(pointer_offset_bits(subtype, ns)==8,
302  "offset bits are byte aligned");
303 
304  mp_integer size_bits=pointer_offset_bits(unpacked.type(), ns);
305  if(size_bits<0)
306  {
307  mp_integer op0_bits=pointer_offset_bits(unpacked.op().type(), ns);
308  if(op0_bits<0)
309  {
310  throw non_const_byte_extraction_sizet(unpacked);
311  }
312  else
313  size_bits=op0_bits;
314  }
315 
316  mp_integer num_elements=
317  size_bits/8+((size_bits%8==0)?0:1);
318 
319  const typet &offset_type=ns.follow(offset.type());
320 
321  // get 'width'-many bytes, and concatenate
322  std::size_t width_bytes=integer2unsigned(num_elements);
323  exprt::operandst op;
324  op.reserve(width_bytes);
325 
326  for(std::size_t i=0; i<width_bytes; i++)
327  {
328  // the most significant byte comes first in the concatenation!
329  std::size_t offset_int=
330  little_endian?(width_bytes-i-1):i;
331 
332  plus_exprt offset_i(from_integer(offset_int, offset_type), offset);
333  index_exprt index_expr(root, offset_i);
334  op.push_back(index_expr);
335  }
336 
337  if(width_bytes==1)
338  return simplify_expr(typecast_exprt(op.front(), src.type()), ns);
339  else // width_bytes>=2
340  {
341  concatenation_exprt concatenation(src.type());
342  concatenation.operands().swap(op);
343  return simplify_expr(concatenation, ns);
344  }
345 }
346 
348  const byte_update_exprt &src,
349  const namespacet &ns,
350  bool negative_offset)
351 {
352  assert(src.operands().size()==3);
353 
354  mp_integer element_size=
355  pointer_offset_size(src.op2().type(), ns);
356  if(element_size<0)
357  throw "byte_update of unknown width:\n"+src.pretty();
358 
359  const typet &t=ns.follow(src.op0().type());
360 
361  if(t.id()==ID_array)
362  {
363  const array_typet &array_type=to_array_type(t);
364  const typet &subtype=array_type.subtype();
365 
366  // array of bitvectors?
367  if(subtype.id()==ID_unsignedbv ||
368  subtype.id()==ID_signedbv ||
369  subtype.id()==ID_floatbv ||
370  subtype.id()==ID_c_bool ||
371  subtype.id()==ID_pointer)
372  {
373  mp_integer sub_size=pointer_offset_size(subtype, ns);
374 
375  if(sub_size==-1)
376  throw "can't flatten byte_update for sub-type without size";
377 
378  // byte array?
379  if(sub_size==1)
380  {
381  // apply 'array-update-with' element_size times
382  exprt result=src.op0();
383 
384  for(mp_integer i=0; i<element_size; ++i)
385  {
386  exprt i_expr=from_integer(i, ns.follow(src.op1().type()));
387 
388  exprt new_value;
389 
390  if(i==0 && element_size==1) // bytes?
391  {
392  new_value=src.op2();
393  if(new_value.type()!=subtype)
394  new_value.make_typecast(subtype);
395  }
396  else
397  {
398  byte_extract_exprt byte_extract_expr(
399  src.id()==ID_byte_update_little_endian?
400  ID_byte_extract_little_endian:
401  src.id()==ID_byte_update_big_endian?
402  ID_byte_extract_big_endian:
403  throw "unexpected src.id() in flatten_byte_update",
404  subtype);
405 
406  byte_extract_expr.op()=src.op2();
407  byte_extract_expr.offset()=i_expr;
408 
409  new_value=flatten_byte_extract(byte_extract_expr, ns);
410  }
411 
412  const plus_exprt where(src.op1(), i_expr);
413 
414  with_exprt with_expr(result, where, new_value);
415  with_expr.type()=src.type();
416 
417  result.swap(with_expr);
418  }
419 
420  return simplify_expr(result, ns);
421  }
422  else // sub_size!=1
423  {
424  exprt result=src.op0();
425 
426  // Number of potentially affected array cells:
427  mp_integer num_elements=
428  element_size/sub_size+((element_size%sub_size==0)?1:2);
429 
430  const auto &offset_type=ns.follow(src.op1().type());
431  exprt zero_offset=from_integer(0, offset_type);
432 
433  exprt sub_size_expr=from_integer(sub_size, offset_type);
434  exprt element_size_expr=from_integer(element_size, offset_type);
435 
436  // First potentially affected cell:
437  div_exprt first_cell(src.op1(), sub_size_expr);
438 
439  for(mp_integer i=0; i<num_elements; ++i)
440  {
441  plus_exprt cell_index(first_cell, from_integer(i, offset_type));
442  mult_exprt cell_offset(cell_index, sub_size_expr);
443  index_exprt old_cell_value(src.op0(), cell_index, subtype);
444  bool is_first_cell=i==0;
445  bool is_last_cell=i==num_elements-1;
446 
447  exprt new_value;
448  exprt stored_value_offset;
449  if(element_size<=sub_size)
450  {
451  new_value=src.op2();
452  stored_value_offset=zero_offset;
453  }
454  else
455  {
456  // Offset to retrieve from the stored value: make sure not to
457  // ask for anything out of range; in the first- or last-cell cases
458  // we will adjust the offset in the byte_update call below.
459  if(is_first_cell)
460  stored_value_offset=zero_offset;
461  else if(is_last_cell)
462  stored_value_offset=
463  from_integer(element_size-sub_size, offset_type);
464  else
465  stored_value_offset=minus_exprt(cell_offset, src.op1());
466 
467  auto extract_opcode=
468  src.id()==ID_byte_update_little_endian ?
469  ID_byte_extract_little_endian :
470  src.id()==ID_byte_update_big_endian ?
471  ID_byte_extract_big_endian :
472  throw "unexpected src.id() in flatten_byte_update";
473  byte_extract_exprt byte_extract_expr(
474  extract_opcode,
475  element_size<sub_size ? src.op2().type() : subtype);
476 
477  byte_extract_expr.op()=src.op2();
478  byte_extract_expr.offset()=stored_value_offset;
479 
480  new_value=flatten_byte_extract(byte_extract_expr, ns);
481  }
482 
483  // Where does the value we just extracted align in this cell?
484  // This value might be negative, indicating only the most-significant
485  // bytes should be written, to the least-significant bytes of the
486  // target array cell.
487  exprt overwrite_offset;
488  if(is_first_cell)
489  overwrite_offset=mod_exprt(src.op1(), sub_size_expr);
490  else if(is_last_cell)
491  {
492  // This is intentionally negated; passing is_last_cell
493  // to flatten below leads to it being negated again later.
494  overwrite_offset=
495  minus_exprt(
496  minus_exprt(cell_offset, src.op1()),
497  stored_value_offset);
498  }
499  else
500  overwrite_offset=zero_offset;
501 
502  byte_update_exprt byte_update_expr(
503  src.id(),
504  old_cell_value,
505  overwrite_offset,
506  new_value);
507 
508  // Call recursively, the array is gone!
509  // The last parameter indicates that the
510  exprt flattened_byte_update_expr=
511  flatten_byte_update(byte_update_expr, ns, is_last_cell);
512 
513  with_exprt with_expr(
514  result, cell_index, flattened_byte_update_expr);
515 
516  result=with_expr;
517  }
518 
519  return simplify_expr(result, ns);
520  }
521  }
522  else
523  {
524  throw
525  "flatten_byte_update can only do arrays of scalars right now, "
526  "but got "+subtype.id_string();
527  }
528  }
529  else if(t.id()==ID_signedbv ||
530  t.id()==ID_unsignedbv ||
531  t.id()==ID_floatbv ||
532  t.id()==ID_c_bool ||
533  t.id()==ID_pointer)
534  {
535  // do a shift, mask and OR
536  mp_integer type_width=pointer_offset_bits(t, ns);
537  assert(type_width>0);
538  std::size_t width=integer2size_t(type_width);
539 
540  if(element_size*8>width)
541  throw "flatten_byte_update to update element that is too large";
542 
543  // build mask
544  exprt mask=
545  from_integer(power(2, element_size*8)-1, unsignedbv_typet(width));
546 
547  // zero-extend the value, but only if needed
548  exprt value_extended;
549 
550  if(width>integer2unsigned(element_size)*8)
551  value_extended=
553  from_integer(
554  0, unsignedbv_typet(width-integer2unsigned(element_size)*8)),
555  src.op2(), t);
556  else
557  value_extended=src.op2();
558 
559  const typet &offset_type=ns.follow(src.op1().type());
560  mult_exprt offset_times_eight(src.op1(), from_integer(8, offset_type));
561 
562  binary_predicate_exprt offset_ge_zero(
563  offset_times_eight,
564  ID_ge,
565  from_integer(0, offset_type));
566 
567  // Shift the mask and value.
568  // Note either shift might discard some of the new value's bits.
569  exprt mask_shifted;
570  exprt value_shifted;
571  if(negative_offset)
572  {
573  // In this case we shift right, to mask out higher addresses
574  // rather than left to mask out lower ones as usual.
575  mask_shifted=lshr_exprt(mask, offset_times_eight);
576  value_shifted=lshr_exprt(value_extended, offset_times_eight);
577  }
578  else
579  {
580  mask_shifted=shl_exprt(mask, offset_times_eight);
581  value_shifted=shl_exprt(value_extended, offset_times_eight);
582  }
583 
584  // original_bits &= ~mask
585  bitand_exprt bitand_expr(src.op0(), bitnot_exprt(mask_shifted));
586 
587  // original_bits |= newvalue
588  bitor_exprt bitor_expr(bitand_expr, value_shifted);
589 
590  return simplify_expr(bitor_expr, ns);
591  }
592  else
593  {
594  throw "flatten_byte_update can only do array and scalars "
595  "right now, but got "+t.id_string();
596  }
597 }
598 
600  const byte_update_exprt &src,
601  const namespacet &ns)
602 {
603  return flatten_byte_update(src, ns, false);
604 }
605 
606 bool has_byte_operator(const exprt &src)
607 {
608  if(src.id()==ID_byte_update_little_endian ||
609  src.id()==ID_byte_update_big_endian ||
610  src.id()==ID_byte_extract_little_endian ||
611  src.id()==ID_byte_extract_big_endian)
612  return true;
613 
614  forall_operands(it, src)
615  if(has_byte_operator(*it))
616  return true;
617 
618  return false;
619 }
620 
622  const exprt &src,
623  const namespacet &ns)
624 {
625  exprt tmp=src;
626 
627  // destroys any sharing, should use hash table
628  Forall_operands(it, tmp)
629  {
630  exprt tmp=flatten_byte_operators(*it, ns);
631  it->swap(tmp);
632  }
633 
634  if(src.id()==ID_byte_update_little_endian ||
635  src.id()==ID_byte_update_big_endian)
636  return flatten_byte_update(to_byte_update_expr(tmp), ns);
637  else if(src.id()==ID_byte_extract_little_endian ||
638  src.id()==ID_byte_extract_big_endian)
640  else
641  return tmp;
642 }
The type of an expression.
Definition: type.h:22
exprt size_of_expr(const typet &type, const namespacet &ns)
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1220
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
bool is_not_nil() const
Definition: irep.h:103
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
exprt simplify_expr(const exprt &src, const namespacet &ns)
exprt flatten_byte_update(const byte_update_exprt &src, const namespacet &ns, bool negative_offset)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
std::vector< componentt > componentst
Definition: std_types.h:243
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
const componentst & components() const
Definition: std_types.h:245
exprt flatten_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...
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
typet & type()
Definition: expr.h:56
unsignedbv_typet size_type()
Definition: c_types.cpp:58
Structure type.
Definition: std_types.h:297
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Extract member of struct or union.
Definition: std_expr.h:3871
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Concatenation of bit-vector operands.
Definition: std_expr.h:4625
const irep_idt & id() const
Definition: irep.h:189
Bit-wise OR.
Definition: std_expr.h:2583
Expression classes for byte-level operators.
division (integer and real)
Definition: std_expr.h:1075
static exprt unpack_rec(const exprt &src, bool little_endian, const exprt &max_bytes, const namespacet &ns, bool unpack_byte_array=false)
rewrite an object into its individual bytes
exprt flatten_byte_operators(const exprt &src, const namespacet &ns)
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3072
exprt & op1()
Definition: expr.h:75
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Left shift.
Definition: std_expr.h:2848
const exprt & size() const
Definition: std_types.h:1014
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:893
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
Logical right shift.
Definition: std_expr.h:2888
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
std::vector< exprt > operandst
Definition: expr.h:45
binary multiplication
Definition: std_expr.h:1017
Pointer Logic.
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:202
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
Operator to update elements in structs and arrays.
Definition: std_expr.h:3461
#define UNREACHABLE
Definition: invariant.h:250
const std::string & id_string() const
Definition: irep.h:192
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
void insert(const irep_idt &identifier, const exprt &expr)
arrays with given size
Definition: std_types.h:1004
binary minus
Definition: std_expr.h:959
TO_BE_DOCUMENTED.
Bit-wise AND.
Definition: std_expr.h:2704
Expression to hold a symbol (variable)
Definition: std_expr.h:90
exprt & op2()
Definition: expr.h:78
bool has_byte_operator(const exprt &src)
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:730
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
operandst & operands()
Definition: expr.h:66
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2529
struct constructor from list of elements
Definition: std_expr.h:1815
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
void make_typecast(const typet &_type)
Definition: expr.cpp:84
array constructor from list of elements
Definition: std_expr.h:1617
binary modulo
Definition: std_expr.h:1133
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
bool simplify(exprt &expr, const namespacet &ns)
array index operator
Definition: std_expr.h:1462