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