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  PRECONDITION(
205  src.id() == ID_byte_extract_little_endian ||
206  src.id() == ID_byte_extract_big_endian);
207  const bool little_endian = src.id() == ID_byte_extract_little_endian;
208 
209  // determine an upper bound of the number of bytes we might need
210  exprt upper_bound=size_of_expr(src.type(), ns);
211  if(upper_bound.is_not_nil())
212  upper_bound=
214  plus_exprt(
215  upper_bound,
216  typecast_exprt(src.offset(), upper_bound.type())),
217  ns);
218 
219  byte_extract_exprt unpacked(src);
220  unpacked.op()=
221  unpack_rec(src.op(), little_endian, upper_bound, ns);
222 
223  const typet &type=ns.follow(src.type());
224 
225  if(type.id()==ID_array)
226  {
227  const array_typet &array_type=to_array_type(type);
228  const typet &subtype=array_type.subtype();
229 
230  mp_integer element_width=pointer_offset_bits(subtype, ns);
231  mp_integer num_elements;
232  // TODO: consider ways of dealing with arrays of unknown subtype
233  // size or with a subtype size that does not fit byte boundaries
234  if(element_width>0 && element_width%8==0 &&
235  to_integer(array_type.size(), num_elements))
236  {
237  array_exprt array(array_type);
238 
239  for(mp_integer i=0; i<num_elements; ++i)
240  {
241  plus_exprt new_offset(
242  unpacked.offset(),
243  from_integer(i*element_width, unpacked.offset().type()));
244 
245  byte_extract_exprt tmp(unpacked);
246  tmp.type()=subtype;
247  tmp.offset()=new_offset;
248 
249  array.copy_to_operands(flatten_byte_extract(tmp, ns));
250  }
251 
252  return simplify_expr(array, ns);
253  }
254  }
255  else if(type.id()==ID_struct)
256  {
257  const struct_typet &struct_type=to_struct_type(type);
258  const struct_typet::componentst &components=struct_type.components();
259 
260  bool failed=false;
261  struct_exprt s(struct_type);
262 
263  for(const auto &comp : components)
264  {
265  mp_integer element_width=pointer_offset_bits(comp.type(), ns);
266 
267  // the next member would be misaligned, abort
268  if(element_width<=0 || element_width%8!=0)
269  {
270  failed=true;
271  break;
272  }
273 
274  plus_exprt new_offset(
275  unpacked.offset(),
277  member_offset_expr(struct_type, comp.get_name(), ns),
278  unpacked.offset().type()));
279 
280  byte_extract_exprt tmp(unpacked);
281  tmp.type()=comp.type();
282  tmp.offset()=new_offset;
283 
284  s.move_to_operands(tmp);
285  }
286 
287  if(!failed)
288  return simplify_expr(s, ns);
289  }
290 
291  const exprt &root=unpacked.op();
292  const exprt &offset=unpacked.offset();
293 
294  const array_typet &array_type=to_array_type(root.type());
295  const typet &subtype=array_type.subtype();
296 
297  DATA_INVARIANT(pointer_offset_bits(subtype, ns)==8,
298  "offset bits are byte aligned");
299 
300  mp_integer size_bits=pointer_offset_bits(unpacked.type(), ns);
301  if(size_bits<0)
302  {
303  mp_integer op0_bits=pointer_offset_bits(unpacked.op().type(), ns);
304  if(op0_bits<0)
305  {
306  throw non_const_byte_extraction_sizet(unpacked);
307  }
308  else
309  size_bits=op0_bits;
310  }
311 
312  mp_integer num_elements=
313  size_bits/8+((size_bits%8==0)?0:1);
314 
315  const typet &offset_type=ns.follow(offset.type());
316 
317  // get 'width'-many bytes, and concatenate
318  std::size_t width_bytes=integer2unsigned(num_elements);
319  exprt::operandst op;
320  op.reserve(width_bytes);
321 
322  for(std::size_t i=0; i<width_bytes; i++)
323  {
324  // the most significant byte comes first in the concatenation!
325  std::size_t offset_int=
326  little_endian?(width_bytes-i-1):i;
327 
328  plus_exprt offset_i(from_integer(offset_int, offset_type), offset);
329  index_exprt index_expr(root, offset_i);
330  op.push_back(index_expr);
331  }
332 
333  if(width_bytes==1)
334  return simplify_expr(typecast_exprt(op.front(), src.type()), ns);
335  else // width_bytes>=2
336  {
337  concatenation_exprt concatenation(src.type());
338  concatenation.operands().swap(op);
339  return simplify_expr(concatenation, ns);
340  }
341 }
342 
344  const byte_update_exprt &src,
345  const namespacet &ns,
346  bool negative_offset)
347 {
348  assert(src.operands().size()==3);
349 
350  mp_integer element_size=
351  pointer_offset_size(src.op2().type(), ns);
352  if(element_size<0)
353  throw "byte_update of unknown width:\n"+src.pretty();
354 
355  const typet &t=ns.follow(src.op0().type());
356 
357  if(t.id()==ID_array)
358  {
359  const array_typet &array_type=to_array_type(t);
360  const typet &subtype=array_type.subtype();
361 
362  // array of bitvectors?
363  if(subtype.id()==ID_unsignedbv ||
364  subtype.id()==ID_signedbv ||
365  subtype.id()==ID_floatbv ||
366  subtype.id()==ID_c_bool ||
367  subtype.id()==ID_pointer)
368  {
369  mp_integer sub_size=pointer_offset_size(subtype, ns);
370 
371  if(sub_size==-1)
372  throw "can't flatten byte_update for sub-type without size";
373 
374  // byte array?
375  if(sub_size==1)
376  {
377  // apply 'array-update-with' element_size times
378  exprt result=src.op0();
379 
380  for(mp_integer i=0; i<element_size; ++i)
381  {
382  exprt i_expr=from_integer(i, ns.follow(src.op1().type()));
383 
384  exprt new_value;
385 
386  if(i==0 && element_size==1) // bytes?
387  {
388  new_value=src.op2();
389  if(new_value.type()!=subtype)
390  new_value.make_typecast(subtype);
391  }
392  else
393  {
394  byte_extract_exprt byte_extract_expr(
395  src.id()==ID_byte_update_little_endian?
396  ID_byte_extract_little_endian:
397  src.id()==ID_byte_update_big_endian?
398  ID_byte_extract_big_endian:
399  throw "unexpected src.id() in flatten_byte_update",
400  subtype);
401 
402  byte_extract_expr.op()=src.op2();
403  byte_extract_expr.offset()=i_expr;
404 
405  new_value=flatten_byte_extract(byte_extract_expr, ns);
406  }
407 
408  const plus_exprt where(src.op1(), i_expr);
409 
410  with_exprt with_expr(result, where, new_value);
411  with_expr.type()=src.type();
412 
413  result.swap(with_expr);
414  }
415 
416  return simplify_expr(result, ns);
417  }
418  else // sub_size!=1
419  {
420  exprt result=src.op0();
421 
422  // Number of potentially affected array cells:
423  mp_integer num_elements=
424  element_size/sub_size+((element_size%sub_size==0)?1:2);
425 
426  const auto &offset_type=ns.follow(src.op1().type());
427  exprt zero_offset=from_integer(0, offset_type);
428 
429  exprt sub_size_expr=from_integer(sub_size, offset_type);
430  exprt element_size_expr=from_integer(element_size, offset_type);
431 
432  // First potentially affected cell:
433  div_exprt first_cell(src.op1(), sub_size_expr);
434 
435  for(mp_integer i=0; i<num_elements; ++i)
436  {
437  plus_exprt cell_index(first_cell, from_integer(i, offset_type));
438  mult_exprt cell_offset(cell_index, sub_size_expr);
439  index_exprt old_cell_value(src.op0(), cell_index, subtype);
440  bool is_first_cell=i==0;
441  bool is_last_cell=i==num_elements-1;
442 
443  exprt new_value;
444  exprt stored_value_offset;
445  if(element_size<=sub_size)
446  {
447  new_value=src.op2();
448  stored_value_offset=zero_offset;
449  }
450  else
451  {
452  // Offset to retrieve from the stored value: make sure not to
453  // ask for anything out of range; in the first- or last-cell cases
454  // we will adjust the offset in the byte_update call below.
455  if(is_first_cell)
456  stored_value_offset=zero_offset;
457  else if(is_last_cell)
458  stored_value_offset=
459  from_integer(element_size-sub_size, offset_type);
460  else
461  stored_value_offset=minus_exprt(cell_offset, src.op1());
462 
463  auto extract_opcode=
464  src.id()==ID_byte_update_little_endian ?
465  ID_byte_extract_little_endian :
466  src.id()==ID_byte_update_big_endian ?
467  ID_byte_extract_big_endian :
468  throw "unexpected src.id() in flatten_byte_update";
469  byte_extract_exprt byte_extract_expr(
470  extract_opcode,
471  element_size<sub_size ? src.op2().type() : subtype);
472 
473  byte_extract_expr.op()=src.op2();
474  byte_extract_expr.offset()=stored_value_offset;
475 
476  new_value=flatten_byte_extract(byte_extract_expr, ns);
477  }
478 
479  // Where does the value we just extracted align in this cell?
480  // This value might be negative, indicating only the most-significant
481  // bytes should be written, to the least-significant bytes of the
482  // target array cell.
483  exprt overwrite_offset;
484  if(is_first_cell)
485  overwrite_offset=mod_exprt(src.op1(), sub_size_expr);
486  else if(is_last_cell)
487  {
488  // This is intentionally negated; passing is_last_cell
489  // to flatten below leads to it being negated again later.
490  overwrite_offset=
491  minus_exprt(
492  minus_exprt(cell_offset, src.op1()),
493  stored_value_offset);
494  }
495  else
496  overwrite_offset=zero_offset;
497 
498  byte_update_exprt byte_update_expr(
499  src.id(),
500  old_cell_value,
501  overwrite_offset,
502  new_value);
503 
504  // Call recursively, the array is gone!
505  // The last parameter indicates that the
506  exprt flattened_byte_update_expr=
507  flatten_byte_update(byte_update_expr, ns, is_last_cell);
508 
509  with_exprt with_expr(
510  result, cell_index, flattened_byte_update_expr);
511 
512  result=with_expr;
513  }
514 
515  return simplify_expr(result, ns);
516  }
517  }
518  else
519  {
520  throw
521  "flatten_byte_update can only do arrays of scalars right now, "
522  "but got "+subtype.id_string();
523  }
524  }
525  else if(t.id()==ID_signedbv ||
526  t.id()==ID_unsignedbv ||
527  t.id()==ID_floatbv ||
528  t.id()==ID_c_bool ||
529  t.id()==ID_pointer)
530  {
531  // do a shift, mask and OR
532  mp_integer type_width=pointer_offset_bits(t, ns);
533  assert(type_width>0);
534  std::size_t width=integer2size_t(type_width);
535 
536  if(element_size*8>width)
537  throw "flatten_byte_update to update element that is too large";
538 
539  // build mask
540  exprt mask=
541  from_integer(power(2, element_size*8)-1, unsignedbv_typet(width));
542 
543  // zero-extend the value, but only if needed
544  exprt value_extended;
545 
546  if(width>integer2unsigned(element_size)*8)
547  value_extended=
549  from_integer(
550  0, unsignedbv_typet(width-integer2unsigned(element_size)*8)),
551  src.op2(), t);
552  else
553  value_extended=src.op2();
554 
555  const typet &offset_type=ns.follow(src.op1().type());
556  mult_exprt offset_times_eight(src.op1(), from_integer(8, offset_type));
557 
558  binary_predicate_exprt offset_ge_zero(
559  offset_times_eight,
560  ID_ge,
561  from_integer(0, offset_type));
562 
563  // Shift the mask and value.
564  // Note either shift might discard some of the new value's bits.
565  exprt mask_shifted;
566  exprt value_shifted;
567  if(negative_offset)
568  {
569  // In this case we shift right, to mask out higher addresses
570  // rather than left to mask out lower ones as usual.
571  mask_shifted=lshr_exprt(mask, offset_times_eight);
572  value_shifted=lshr_exprt(value_extended, offset_times_eight);
573  }
574  else
575  {
576  mask_shifted=shl_exprt(mask, offset_times_eight);
577  value_shifted=shl_exprt(value_extended, offset_times_eight);
578  }
579 
580  // original_bits &= ~mask
581  bitand_exprt bitand_expr(src.op0(), bitnot_exprt(mask_shifted));
582 
583  // original_bits |= newvalue
584  bitor_exprt bitor_expr(bitand_expr, value_shifted);
585 
586  return simplify_expr(bitor_expr, ns);
587  }
588  else
589  {
590  throw "flatten_byte_update can only do array and scalars "
591  "right now, but got "+t.id_string();
592  }
593 }
594 
596  const byte_update_exprt &src,
597  const namespacet &ns)
598 {
599  return flatten_byte_update(src, ns, false);
600 }
601 
602 bool has_byte_operator(const exprt &src)
603 {
604  if(src.id()==ID_byte_update_little_endian ||
605  src.id()==ID_byte_update_big_endian ||
606  src.id()==ID_byte_extract_little_endian ||
607  src.id()==ID_byte_extract_big_endian)
608  return true;
609 
610  forall_operands(it, src)
611  if(has_byte_operator(*it))
612  return true;
613 
614  return false;
615 }
616 
618  const exprt &src,
619  const namespacet &ns)
620 {
621  exprt tmp=src;
622 
623  // destroys any sharing, should use hash table
624  Forall_operands(it, tmp)
625  {
626  exprt tmp=flatten_byte_operators(*it, ns);
627  it->swap(tmp);
628  }
629 
630  if(src.id()==ID_byte_update_little_endian ||
631  src.id()==ID_byte_update_big_endian)
632  return flatten_byte_update(to_byte_update_expr(tmp), ns);
633  else if(src.id()==ID_byte_extract_little_endian ||
634  src.id()==ID_byte_extract_big_endian)
636  else
637  return tmp;
638 }
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:1229
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:173
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:3869
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Concatenation of bit-vector operands.
Definition: std_expr.h:4623
const irep_idt & id() const
Definition: irep.h:259
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:3070
exprt & op1()
Definition: expr.h:75
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Left shift.
Definition: std_expr.h:2848
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
const exprt & size() const
Definition: std_types.h:1023
#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:203
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
Operator to update elements in structs and arrays.
Definition: std_expr.h:3459
const std::string & id_string() const
Definition: irep.h:262
void swap(irept &irep)
Definition: irep.h:303
#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:1013
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:278
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