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