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 <algorithm>
12 
13 #include <util/arith_tools.h>
14 #include <util/byte_operators.h>
15 #include <util/c_types.h>
16 #include <util/endianness_map.h>
17 #include <util/expr_util.h>
18 #include <util/namespace.h>
20 #include <util/replace_symbol.h>
21 #include <util/simplify_expr.h>
22 #include <util/string_constant.h>
23 
24 static exprt bv_to_expr(
25  const exprt &bitvector_expr,
26  const typet &target_type,
27  const endianness_mapt &endianness_map,
28  const namespacet &ns);
29 
30 struct boundst
31 {
32  std::size_t lb;
33  std::size_t ub;
34 };
35 
38  const endianness_mapt &endianness_map,
39  std::size_t lower_bound,
40  std::size_t upper_bound)
41 {
42  boundst result;
43  result.lb = lower_bound;
44  result.ub = upper_bound;
45 
46  if(result.ub < endianness_map.number_of_bits())
47  {
48  result.lb = endianness_map.map_bit(result.lb);
49  result.ub = endianness_map.map_bit(result.ub);
50 
51  // big-endian bounds need swapping
52  if(result.ub < result.lb)
53  {
54  result.lb = endianness_map.number_of_bits() - result.lb - 1;
55  result.ub = endianness_map.number_of_bits() - result.ub - 1;
56  }
57  }
58 
59  return result;
60 }
61 
65  const exprt &bitvector_expr,
66  const struct_typet &struct_type,
67  const endianness_mapt &endianness_map,
68  const namespacet &ns)
69 {
70  const struct_typet::componentst &components = struct_type.components();
71 
72  exprt::operandst operands;
73  operands.reserve(components.size());
74  std::size_t member_offset_bits = 0;
75  for(const auto &comp : components)
76  {
77  const auto component_bits_opt = pointer_offset_bits(comp.type(), ns);
78  std::size_t component_bits;
79  if(component_bits_opt.has_value())
80  component_bits = numeric_cast_v<std::size_t>(*component_bits_opt);
81  else
82  component_bits = to_bitvector_type(bitvector_expr.type()).get_width() -
84 
85  if(component_bits == 0)
86  {
87  operands.push_back(constant_exprt{irep_idt{}, comp.type()});
88  continue;
89  }
90 
91  const auto bounds = map_bounds(
92  endianness_map,
94  member_offset_bits + component_bits - 1);
95  bitvector_typet type{bitvector_expr.type().id(), component_bits};
96  operands.push_back(bv_to_expr(
97  extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
98  comp.type(),
99  endianness_map,
100  ns));
101 
102  if(component_bits_opt.has_value())
103  member_offset_bits += component_bits;
104  }
105 
106  return struct_exprt{std::move(operands), struct_type};
107 }
108 
112  const exprt &bitvector_expr,
113  const array_typet &array_type,
114  const endianness_mapt &endianness_map,
115  const namespacet &ns)
116 {
117  auto num_elements = numeric_cast<std::size_t>(array_type.size());
118  auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
119 
120  const std::size_t total_bits =
121  to_bitvector_type(bitvector_expr.type()).get_width();
122  if(!num_elements.has_value())
123  {
124  if(!subtype_bits.has_value() || *subtype_bits == 0)
125  num_elements = total_bits;
126  else
127  num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
128  }
130  !num_elements.has_value() || !subtype_bits.has_value() ||
131  *subtype_bits * *num_elements == total_bits,
132  "subtype width times array size should be total bitvector width");
133 
134  exprt::operandst operands;
135  operands.reserve(*num_elements);
136  for(std::size_t i = 0; i < *num_elements; ++i)
137  {
138  if(subtype_bits.has_value())
139  {
140  const std::size_t subtype_bits_int =
141  numeric_cast_v<std::size_t>(*subtype_bits);
142  const auto bounds = map_bounds(
143  endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
144  bitvector_typet type{bitvector_expr.type().id(), subtype_bits_int};
145  operands.push_back(bv_to_expr(
147  bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
148  array_type.subtype(),
149  endianness_map,
150  ns));
151  }
152  else
153  {
154  operands.push_back(
155  bv_to_expr(bitvector_expr, array_type.subtype(), endianness_map, ns));
156  }
157  }
158 
159  return array_exprt{std::move(operands), array_type};
160 }
161 
165  const exprt &bitvector_expr,
166  const vector_typet &vector_type,
167  const endianness_mapt &endianness_map,
168  const namespacet &ns)
169 {
170  const std::size_t num_elements =
171  numeric_cast_v<std::size_t>(vector_type.size());
172  auto subtype_bits = pointer_offset_bits(vector_type.subtype(), ns);
174  !subtype_bits.has_value() ||
175  *subtype_bits * num_elements ==
176  to_bitvector_type(bitvector_expr.type()).get_width(),
177  "subtype width times vector size should be total bitvector width");
178 
179  exprt::operandst operands;
180  operands.reserve(num_elements);
181  for(std::size_t i = 0; i < num_elements; ++i)
182  {
183  if(subtype_bits.has_value())
184  {
185  const std::size_t subtype_bits_int =
186  numeric_cast_v<std::size_t>(*subtype_bits);
187  const auto bounds = map_bounds(
188  endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
189  bitvector_typet type{bitvector_expr.type().id(), subtype_bits_int};
190  operands.push_back(bv_to_expr(
192  bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
193  vector_type.subtype(),
194  endianness_map,
195  ns));
196  }
197  else
198  {
199  operands.push_back(
200  bv_to_expr(bitvector_expr, vector_type.subtype(), endianness_map, ns));
201  }
202  }
203 
204  return vector_exprt{std::move(operands), vector_type};
205 }
206 
210  const exprt &bitvector_expr,
211  const complex_typet &complex_type,
212  const endianness_mapt &endianness_map,
213  const namespacet &ns)
214 {
215  const std::size_t total_bits =
216  to_bitvector_type(bitvector_expr.type()).get_width();
217  const auto subtype_bits_opt = pointer_offset_bits(complex_type.subtype(), ns);
218  std::size_t subtype_bits;
219  if(subtype_bits_opt.has_value())
220  {
221  subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
223  subtype_bits * 2 == total_bits,
224  "subtype width should be half of the total bitvector width");
225  }
226  else
227  subtype_bits = total_bits / 2;
228 
229  const auto bounds_real = map_bounds(endianness_map, 0, subtype_bits - 1);
230  const auto bounds_imag =
231  map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
232 
233  const bitvector_typet type{bitvector_expr.type().id(), subtype_bits};
234 
235  return complex_exprt{
236  bv_to_expr(
237  extractbits_exprt{bitvector_expr, bounds_real.ub, bounds_real.lb, type},
238  complex_type.subtype(),
239  endianness_map,
240  ns),
241  bv_to_expr(
242  extractbits_exprt{bitvector_expr, bounds_imag.ub, bounds_imag.lb, type},
243  complex_type.subtype(),
244  endianness_map,
245  ns),
246  complex_type};
247 }
248 
263  const exprt &bitvector_expr,
264  const typet &target_type,
265  const endianness_mapt &endianness_map,
266  const namespacet &ns)
267 {
269 
270  if(
271  can_cast_type<bitvector_typet>(target_type) ||
272  target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
273  target_type.id() == ID_string)
274  {
275  std::size_t width = to_bitvector_type(bitvector_expr.type()).get_width();
276  exprt bv_expr =
277  typecast_exprt::conditional_cast(bitvector_expr, bv_typet{width});
278  return simplify_expr(
279  typecast_exprt::conditional_cast(bv_expr, target_type), ns);
280  }
281 
282  if(target_type.id() == ID_struct)
283  {
284  return bv_to_struct_expr(
285  bitvector_expr, to_struct_type(target_type), endianness_map, ns);
286  }
287  else if(target_type.id() == ID_struct_tag)
288  {
290  bitvector_expr,
291  ns.follow_tag(to_struct_tag_type(target_type)),
292  endianness_map,
293  ns);
294  result.type() = target_type;
295  return std::move(result);
296  }
297  else if(target_type.id() == ID_array)
298  {
299  return bv_to_array_expr(
300  bitvector_expr, to_array_type(target_type), endianness_map, ns);
301  }
302  else if(target_type.id() == ID_vector)
303  {
304  return bv_to_vector_expr(
305  bitvector_expr, to_vector_type(target_type), endianness_map, ns);
306  }
307  else if(target_type.id() == ID_complex)
308  {
309  return bv_to_complex_expr(
310  bitvector_expr, to_complex_type(target_type), endianness_map, ns);
311  }
312  else
313  {
315  false, "bv_to_expr does not yet support ", target_type.id_string());
316  }
317 }
318 
319 static exprt unpack_rec(
320  const exprt &src,
321  bool little_endian,
322  const optionalt<mp_integer> &offset_bytes,
323  const optionalt<mp_integer> &max_bytes,
324  const namespacet &ns,
325  bool unpack_byte_array = false);
326 
334  const exprt &src,
335  std::size_t lower_bound,
336  std::size_t upper_bound,
337  const namespacet &ns)
338 {
339  PRECONDITION(lower_bound <= upper_bound);
340 
341  if(src.id() == ID_array)
342  {
343  PRECONDITION(upper_bound <= src.operands().size());
344  return exprt::operandst{
345  src.operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
346  src.operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
347  }
348 
349  exprt::operandst bytes;
350  bytes.reserve(upper_bound - lower_bound);
351  for(std::size_t i = lower_bound; i < upper_bound; ++i)
352  {
353  const index_exprt idx{src, from_integer(i, index_type())};
354  bytes.push_back(simplify_expr(idx, ns));
355  }
356  return bytes;
357 }
358 
373  const exprt &src,
374  const optionalt<mp_integer> &src_size,
375  const mp_integer &element_bits,
376  bool little_endian,
377  const optionalt<mp_integer> &offset_bytes,
378  const optionalt<mp_integer> &max_bytes,
379  const namespacet &ns)
380 {
381  const std::size_t el_bytes =
382  numeric_cast_v<std::size_t>((element_bits + 7) / 8);
383 
384  if(!src_size.has_value() && !max_bytes.has_value())
385  {
386  // TODO we either need a symbol table here or make array comprehensions
387  // introduce a scope
388  static std::size_t array_comprehension_index_counter = 0;
389  ++array_comprehension_index_counter;
390  symbol_exprt array_comprehension_index{
391  "$array_comprehension_index_a_v" +
392  std::to_string(array_comprehension_index_counter),
393  index_type()};
394 
395  CHECK_RETURN(el_bytes > 0);
396  index_exprt element{src,
397  div_exprt{array_comprehension_index,
398  from_integer(el_bytes, index_type())}};
399 
400  exprt sub = unpack_rec(element, little_endian, {}, {}, ns, false);
401  exprt::operandst sub_operands =
402  instantiate_byte_array(sub, 0, el_bytes, ns);
403 
404  exprt body = sub_operands.front();
405  const mod_exprt offset{
406  array_comprehension_index,
407  from_integer(el_bytes, array_comprehension_index.type())};
408  for(std::size_t i = 1; i < el_bytes; ++i)
409  {
410  body = if_exprt{
411  equal_exprt{offset, from_integer(i, array_comprehension_index.type())},
412  sub_operands[i],
413  body};
414  }
415 
416  optionalt<exprt> array_vector_size;
417  optionalt<typet> subtype;
418  if(src.type().id() == ID_vector)
419  {
420  array_vector_size = to_vector_type(src.type()).size();
421  subtype = to_vector_type(src.type()).subtype();
422  }
423  else
424  {
425  array_vector_size = to_array_type(src.type()).size();
426  subtype = to_array_type(src.type()).subtype();
427  }
428 
430  std::move(array_comprehension_index),
431  std::move(body),
432  array_typet{
433  *subtype,
434  mult_exprt{*array_vector_size,
435  from_integer(el_bytes, array_vector_size->type())}}};
436  }
437 
438  exprt::operandst byte_operands;
439  mp_integer first_element = 0;
440 
441  // refine the number of elements to extract in case the element width is known
442  // and a multiple of bytes; otherwise we will expand the entire array/vector
443  optionalt<mp_integer> num_elements = src_size;
444  if(element_bits > 0 && element_bits % 8 == 0)
445  {
446  if(!num_elements.has_value())
447  {
448  // turn bytes into elements, rounding up
449  num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
450  }
451 
452  if(offset_bytes.has_value())
453  {
454  // compute offset as number of elements
455  first_element = *offset_bytes / el_bytes;
456  // insert offset_bytes-many nil bytes into the output array
457  byte_operands.resize(
458  numeric_cast_v<std::size_t>(*offset_bytes - (*offset_bytes % el_bytes)),
459  from_integer(0, bv_typet{8}));
460  }
461  }
462 
463  // the maximum number of bytes is an upper bound in case the size of the
464  // array/vector is unknown; if element_bits was usable above this will
465  // have been turned into a number of elements already
466  if(!num_elements)
467  num_elements = *max_bytes;
468 
469  const exprt src_simp = simplify_expr(src, ns);
470 
471  for(mp_integer i = first_element; i < *num_elements; ++i)
472  {
473  exprt element;
474 
475  if(
476  (src_simp.id() == ID_array || src_simp.id() == ID_vector) &&
477  i < src_simp.operands().size())
478  {
479  const std::size_t index_int = numeric_cast_v<std::size_t>(i);
480  element = src_simp.operands()[index_int];
481  }
482  else
483  {
484  element = index_exprt(src_simp, from_integer(i, index_type()));
485  }
486 
487  // recursively unpack each element so that we eventually just have an array
488  // of bytes left
489  exprt sub = unpack_rec(element, little_endian, {}, max_bytes, ns, true);
490  exprt::operandst sub_operands =
491  instantiate_byte_array(sub, 0, el_bytes, ns);
492  byte_operands.insert(
493  byte_operands.end(), sub_operands.begin(), sub_operands.end());
494  }
495 
496  const std::size_t size = byte_operands.size();
497  return array_exprt(
498  std::move(byte_operands),
500 }
501 
512 static void process_bit_fields(
513  exprt::operandst &&bit_fields,
514  std::size_t total_bits,
515  exprt::operandst &dest,
516  bool little_endian,
517  const optionalt<mp_integer> &offset_bytes,
518  const optionalt<mp_integer> &max_bytes,
519  const namespacet &ns)
520 {
521  const concatenation_exprt concatenation{std::move(bit_fields),
522  bv_typet{total_bits}};
523 
524  exprt sub =
525  unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns, true);
526 
527  dest.insert(
528  dest.end(),
529  std::make_move_iterator(sub.operands().begin()),
530  std::make_move_iterator(sub.operands().end()));
531 }
532 
543  const exprt &src,
544  bool little_endian,
545  const optionalt<mp_integer> &offset_bytes,
546  const optionalt<mp_integer> &max_bytes,
547  const namespacet &ns)
548 {
549  const struct_typet &struct_type = to_struct_type(ns.follow(src.type()));
550  const struct_typet::componentst &components = struct_type.components();
551 
552  optionalt<mp_integer> offset_in_member;
553  optionalt<mp_integer> max_bytes_left;
555 
557  exprt::operandst byte_operands;
558  for(auto it = components.begin(); it != components.end(); ++it)
559  {
560  const auto &comp = *it;
561  auto component_bits = pointer_offset_bits(comp.type(), ns);
562 
563  // We can only handle a member of unknown width when it is the last member
564  // and is byte-aligned. Members of unknown width in the middle would leave
565  // us with unknown alignment of subsequent members, and queuing them up as
566  // bit fields is not possible either as the total width of the concatenation
567  // could not be determined.
569  component_bits.has_value() ||
570  (std::next(it) == components.end() && !bit_fields.has_value()),
571  "members of non-constant width should come last in a struct");
572 
573  member_exprt member(src, comp.get_name(), comp.type());
574  if(src.id() == ID_struct)
575  simplify(member, ns);
576 
577  // Is it a byte-aligned member?
578  if(member_offset_bits % 8 == 0)
579  {
580  if(bit_fields.has_value())
581  {
583  std::move(bit_fields->first),
584  bit_fields->second,
585  byte_operands,
586  little_endian,
587  offset_in_member,
588  max_bytes_left,
589  ns);
590  bit_fields.reset();
591  }
592 
593  if(offset_bytes.has_value())
594  {
595  offset_in_member = *offset_bytes - member_offset_bits / 8;
596  // if the offset is negative, offset_in_member remains unset, which has
597  // the same effect as setting it to zero
598  if(*offset_in_member < 0)
599  offset_in_member.reset();
600  }
601 
602  if(max_bytes.has_value())
603  {
604  max_bytes_left = *max_bytes - member_offset_bits / 8;
605  if(*max_bytes_left < 0)
606  break;
607  }
608  }
609 
610  if(
611  member_offset_bits % 8 != 0 ||
612  (component_bits.has_value() && *component_bits % 8 != 0))
613  {
614  if(!bit_fields.has_value())
615  bit_fields = std::make_pair(exprt::operandst{}, std::size_t{0});
616 
617  const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
618  bit_fields->first.insert(
619  little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
620  typecast_exprt::conditional_cast(member, bv_typet{bits_int}));
621  bit_fields->second += bits_int;
622 
623  member_offset_bits += *component_bits;
624 
625  continue;
626  }
627 
628  INVARIANT(
629  !bit_fields.has_value(),
630  "all preceding members should have been processed");
631 
632  exprt sub = unpack_rec(
633  member, little_endian, offset_in_member, max_bytes_left, ns, true);
634 
635  byte_operands.insert(
636  byte_operands.end(),
637  std::make_move_iterator(sub.operands().begin()),
638  std::make_move_iterator(sub.operands().end()));
639 
640  if(component_bits.has_value())
641  member_offset_bits += *component_bits;
642  }
643 
644  if(bit_fields.has_value())
646  std::move(bit_fields->first),
647  bit_fields->second,
648  byte_operands,
649  little_endian,
650  offset_in_member,
651  max_bytes_left,
652  ns);
653 
654  const std::size_t size = byte_operands.size();
655  return array_exprt{std::move(byte_operands),
657 }
658 
664 static array_exprt
665 unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
666 {
667  const complex_typet &complex_type = to_complex_type(src.type());
668  const typet &subtype = complex_type.subtype();
669 
670  auto subtype_bits = pointer_offset_bits(subtype, ns);
671  CHECK_RETURN(subtype_bits.has_value());
672  CHECK_RETURN(*subtype_bits % 8 == 0);
673 
674  exprt sub_real = unpack_rec(
675  complex_real_exprt{src},
676  little_endian,
677  mp_integer{0},
678  *subtype_bits / 8,
679  ns,
680  true);
681  exprt::operandst byte_operands = std::move(sub_real.operands());
682 
683  exprt sub_imag = unpack_rec(
684  complex_imag_exprt{src},
685  little_endian,
686  mp_integer{0},
687  *subtype_bits / 8,
688  ns,
689  true);
690  byte_operands.insert(
691  byte_operands.end(),
692  std::make_move_iterator(sub_imag.operands().begin()),
693  std::make_move_iterator(sub_imag.operands().end()));
694 
695  const std::size_t size = byte_operands.size();
696  return array_exprt{std::move(byte_operands),
698 }
699 
709 // array of bytes
712  const exprt &src,
713  bool little_endian,
714  const optionalt<mp_integer> &offset_bytes,
715  const optionalt<mp_integer> &max_bytes,
716  const namespacet &ns,
717  bool unpack_byte_array)
718 {
719  if(src.type().id()==ID_array)
720  {
721  const array_typet &array_type=to_array_type(src.type());
722  const typet &subtype=array_type.subtype();
723 
724  auto element_bits = pointer_offset_bits(subtype, ns);
725  CHECK_RETURN(element_bits.has_value());
726 
727  if(!unpack_byte_array && *element_bits == 8)
728  return src;
729 
730  const auto constant_size_opt = numeric_cast<mp_integer>(array_type.size());
731  return unpack_array_vector(
732  src,
733  constant_size_opt,
734  *element_bits,
735  little_endian,
736  offset_bytes,
737  max_bytes,
738  ns);
739  }
740  else if(src.type().id() == ID_vector)
741  {
742  const vector_typet &vector_type = to_vector_type(src.type());
743  const typet &subtype = vector_type.subtype();
744 
745  auto element_bits = pointer_offset_bits(subtype, ns);
746  CHECK_RETURN(element_bits.has_value());
747 
748  if(!unpack_byte_array && *element_bits == 8)
749  return src;
750 
751  return unpack_array_vector(
752  src,
753  numeric_cast_v<mp_integer>(vector_type.size()),
754  *element_bits,
755  little_endian,
756  offset_bytes,
757  max_bytes,
758  ns);
759  }
760  else if(src.type().id() == ID_complex)
761  {
762  return unpack_complex(src, little_endian, ns);
763  }
764  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
765  {
766  return unpack_struct(src, little_endian, offset_bytes, max_bytes, ns);
767  }
768  else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
769  {
770  const union_typet &union_type = to_union_type(ns.follow(src.type()));
771  const union_typet::componentst &components = union_type.components();
772 
773  mp_integer max_width = 0;
774  typet max_comp_type;
775  irep_idt max_comp_name;
776 
777  for(const auto &comp : components)
778  {
779  auto element_width = pointer_offset_bits(comp.type(), ns);
780 
781  if(!element_width.has_value() || *element_width <= max_width)
782  continue;
783 
784  max_width = *element_width;
785  max_comp_type = comp.type();
786  max_comp_name = comp.get_name();
787  }
788 
789  if(max_width > 0)
790  {
791  member_exprt member(src, max_comp_name, max_comp_type);
792  return unpack_rec(
793  member, little_endian, offset_bytes, max_bytes, ns, true);
794  }
795  }
796  else if(src.type().id() == ID_pointer)
797  {
798  return unpack_rec(
800  little_endian,
801  offset_bytes,
802  max_bytes,
803  ns,
804  unpack_byte_array);
805  }
806  else if(src.id() == ID_string_constant)
807  {
808  return unpack_rec(
810  little_endian,
811  offset_bytes,
812  max_bytes,
813  ns,
814  unpack_byte_array);
815  }
816  else if(src.id() == ID_constant && src.type().id() == ID_string)
817  {
818  return unpack_rec(
819  string_constantt(to_constant_expr(src).get_value()).to_array_expr(),
820  little_endian,
821  offset_bytes,
822  max_bytes,
823  ns,
824  unpack_byte_array);
825  }
826  else if(src.type().id()!=ID_empty)
827  {
828  // a basic type; we turn that into extractbits while considering
829  // endianness
830  auto bits_opt = pointer_offset_bits(src.type(), ns);
831  DATA_INVARIANT(bits_opt.has_value(), "basic type should have a fixed size");
832  mp_integer bits = *bits_opt;
833 
834  exprt::operandst byte_operands;
835  for(mp_integer i=0; i<bits; i+=8)
836  {
837  extractbits_exprt extractbits(
839  src, bv_typet{numeric_cast_v<std::size_t>(bits)}),
840  from_integer(i + 7, index_type()),
841  from_integer(i, index_type()),
842  bv_typet{8});
843 
844  // endianness_mapt should be the point of reference for mapping out
845  // endianness, but we need to work on elements here instead of
846  // individual bits
847  if(little_endian)
848  byte_operands.push_back(extractbits);
849  else
850  byte_operands.insert(byte_operands.begin(), extractbits);
851  }
852 
853  const std::size_t size = byte_operands.size();
854  return array_exprt(
855  std::move(byte_operands),
857  }
858 
859  return array_exprt(
860  {}, array_typet{bv_typet{8}, from_integer(0, size_type())});
861 }
862 
872  const byte_extract_exprt &src,
873  const byte_extract_exprt &unpacked,
874  const namespacet &ns)
875 {
876  const complex_typet &complex_type = to_complex_type(src.type());
877  const typet &subtype = complex_type.subtype();
878 
879  auto subtype_bits = pointer_offset_bits(subtype, ns);
880  if(!subtype_bits.has_value() || *subtype_bits % 8 != 0)
881  return {};
882 
883  // offset remains unchanged
884  byte_extract_exprt real{unpacked};
885  real.type() = subtype;
886 
887  const plus_exprt new_offset{
888  unpacked.offset(),
889  from_integer(*subtype_bits / 8, unpacked.offset().type())};
890  byte_extract_exprt imag{unpacked};
891  imag.type() = subtype;
892  imag.offset() = simplify_expr(new_offset, ns);
893 
894  return simplify_expr(
896  lower_byte_extract(real, ns), lower_byte_extract(imag, ns), complex_type},
897  ns);
898 }
899 
903 {
904  // General notes about endianness and the bit-vector conversion:
905  // A single byte with value 0b10001000 is stored (in irept) as
906  // exactly this string literal, and its bit-vector encoding will be
907  // bvt bv={0,0,0,1,0,0,0,1}, i.e., bv[0]==0 and bv[7]==1
908  //
909  // A multi-byte value like x=256 would be:
910  // - little-endian storage: ((char*)&x)[0]==0, ((char*)&x)[1]==1
911  // - big-endian storage: ((char*)&x)[0]==1, ((char*)&x)[1]==0
912  // - irept representation: 0000000100000000
913  // - bvt: {0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0}
914  // <... 8bits ...> <... 8bits ...>
915  //
916  // An array {0, 1} will be encoded as bvt bv={0,1}, i.e., bv[1]==1
917  // concatenation(0, 1) will yield a bvt bv={1,0}, i.e., bv[1]==0
918  //
919  // The semantics of byte_extract(endianness, op, offset, T) is:
920  // interpret ((char*)&op)+offset as the endianness-ordered storage
921  // of an object of type T at address ((char*)&op)+offset
922  // For some T x, byte_extract(endianness, x, 0, T) must yield x.
923  //
924  // byte_extract for a composite type T or an array will interpret
925  // the individual subtypes with suitable endianness; the overall
926  // order of components is not affected by endianness.
927  //
928  // Examples:
929  // unsigned char A[4];
930  // byte_extract_little_endian(A, 0, unsigned short) requests that
931  // A[0],A[1] be interpreted as the storage of an unsigned short with
932  // A[1] being the most-significant byte; byte_extract_big_endian for
933  // the same operands will select A[0] as the most-significant byte.
934  //
935  // int A[2] = {0x01020304,0xDEADBEEF}
936  // byte_extract_big_endian(A, 0, short) should yield 0x0102
937  // byte_extract_little_endian(A, 0, short) should yield 0x0304
938  // To obtain this we first compute byte arrays while taking into
939  // account endianness:
940  // big-endian byte representation: {01,02,03,04,DE,AB,BE,EF}
941  // little-endian byte representation: {04,03,02,01,EF,BE,AB,DE}
942  // We extract the relevant bytes starting from ((char*)A)+0:
943  // big-endian: {01,02}; little-endian: {04,03}
944  // Finally we place them in the appropriate byte order as indicated
945  // by endianness:
946  // big-endian: (short)concatenation(01,02)=0x0102
947  // little-endian: (short)concatenation(03,04)=0x0304
948 
949  PRECONDITION(
950  src.id() == ID_byte_extract_little_endian ||
951  src.id() == ID_byte_extract_big_endian);
952  const bool little_endian = src.id() == ID_byte_extract_little_endian;
953 
954  // determine an upper bound of the number of bytes we might need
955  auto upper_bound_opt = size_of_expr(src.type(), ns);
956  if(upper_bound_opt.has_value())
957  {
958  upper_bound_opt = simplify_expr(
959  plus_exprt(
960  upper_bound_opt.value(),
962  src.offset(), upper_bound_opt.value().type())),
963  ns);
964  }
965  else if(src.type().id() == ID_empty)
966  upper_bound_opt = from_integer(0, size_type());
967 
968  const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.offset());
969  const auto upper_bound_int_opt =
970  numeric_cast<mp_integer>(upper_bound_opt.value_or(nil_exprt()));
971 
972  byte_extract_exprt unpacked(src);
973  unpacked.op() = unpack_rec(
974  src.op(), little_endian, lower_bound_int_opt, upper_bound_int_opt, ns);
975 
976  if(src.type().id()==ID_array)
977  {
978  const array_typet &array_type=to_array_type(src.type());
979  const typet &subtype=array_type.subtype();
980 
981  // consider ways of dealing with arrays of unknown subtype size or with a
982  // subtype size that does not fit byte boundaries; currently we fall back to
983  // stitching together consecutive elements down below
984  auto element_bits = pointer_offset_bits(subtype, ns);
985  if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
986  {
987  auto num_elements = numeric_cast<std::size_t>(array_type.size());
988  if(!num_elements.has_value() && unpacked.op().id() == ID_array)
989  num_elements = unpacked.op().operands().size();
990 
991  if(num_elements.has_value())
992  {
993  exprt::operandst operands;
994  operands.reserve(*num_elements);
995  for(std::size_t i = 0; i < *num_elements; ++i)
996  {
997  plus_exprt new_offset(
998  unpacked.offset(),
999  from_integer(i * (*element_bits) / 8, unpacked.offset().type()));
1000 
1001  byte_extract_exprt tmp(unpacked);
1002  tmp.type() = subtype;
1003  tmp.offset() = new_offset;
1004 
1005  operands.push_back(lower_byte_extract(tmp, ns));
1006  }
1007 
1008  return simplify_expr(array_exprt(std::move(operands), array_type), ns);
1009  }
1010  else
1011  {
1012  // TODO we either need a symbol table here or make array comprehensions
1013  // introduce a scope
1014  static std::size_t array_comprehension_index_counter = 0;
1015  ++array_comprehension_index_counter;
1016  symbol_exprt array_comprehension_index{
1017  "$array_comprehension_index_a" +
1018  std::to_string(array_comprehension_index_counter),
1019  index_type()};
1020 
1021  plus_exprt new_offset{
1022  unpacked.offset(),
1024  mult_exprt{array_comprehension_index,
1025  from_integer(
1026  *element_bits / 8, array_comprehension_index.type())},
1027  unpacked.offset().type())};
1028 
1029  byte_extract_exprt body(unpacked);
1030  body.type() = subtype;
1031  body.offset() = std::move(new_offset);
1032 
1033  return array_comprehension_exprt{std::move(array_comprehension_index),
1034  lower_byte_extract(body, ns),
1035  array_type};
1036  }
1037  }
1038  }
1039  else if(src.type().id() == ID_vector)
1040  {
1041  const vector_typet &vector_type = to_vector_type(src.type());
1042  const typet &subtype = vector_type.subtype();
1043 
1044  // consider ways of dealing with vectors of unknown subtype size or with a
1045  // subtype size that does not fit byte boundaries; currently we fall back to
1046  // stitching together consecutive elements down below
1047  auto element_bits = pointer_offset_bits(subtype, ns);
1048  if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1049  {
1050  const std::size_t num_elements =
1051  numeric_cast_v<std::size_t>(vector_type.size());
1052 
1053  exprt::operandst operands;
1054  operands.reserve(num_elements);
1055  for(std::size_t i = 0; i < num_elements; ++i)
1056  {
1057  plus_exprt new_offset(
1058  unpacked.offset(),
1059  from_integer(i * (*element_bits) / 8, unpacked.offset().type()));
1060 
1061  byte_extract_exprt tmp(unpacked);
1062  tmp.type() = subtype;
1063  tmp.offset() = simplify_expr(new_offset, ns);
1064 
1065  operands.push_back(lower_byte_extract(tmp, ns));
1066  }
1067 
1068  return simplify_expr(vector_exprt(std::move(operands), vector_type), ns);
1069  }
1070  }
1071  else if(src.type().id() == ID_complex)
1072  {
1073  auto result = lower_byte_extract_complex(src, unpacked, ns);
1074  if(result.has_value())
1075  return std::move(*result);
1076 
1077  // else fall back to generic lowering that uses bit masks, below
1078  }
1079  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
1080  {
1081  const struct_typet &struct_type=to_struct_type(ns.follow(src.type()));
1082  const struct_typet::componentst &components=struct_type.components();
1083 
1084  bool failed=false;
1085  struct_exprt s({}, src.type());
1086 
1087  for(const auto &comp : components)
1088  {
1089  auto component_bits = pointer_offset_bits(comp.type(), ns);
1090 
1091  // the next member would be misaligned, abort
1092  if(
1093  !component_bits.has_value() || *component_bits == 0 ||
1094  *component_bits % 8 != 0)
1095  {
1096  failed=true;
1097  break;
1098  }
1099 
1100  auto member_offset_opt =
1101  member_offset_expr(struct_type, comp.get_name(), ns);
1102 
1103  if(!member_offset_opt.has_value())
1104  {
1105  failed = true;
1106  break;
1107  }
1108 
1109  plus_exprt new_offset(
1110  unpacked.offset(),
1112  member_offset_opt.value(), unpacked.offset().type()));
1113 
1114  byte_extract_exprt tmp(unpacked);
1115  tmp.type()=comp.type();
1116  tmp.offset()=new_offset;
1117 
1118  s.add_to_operands(lower_byte_extract(tmp, ns));
1119  }
1120 
1121  if(!failed)
1122  return simplify_expr(std::move(s), ns);
1123  }
1124  else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
1125  {
1126  const union_typet &union_type = to_union_type(ns.follow(src.type()));
1127  const union_typet::componentst &components = union_type.components();
1128 
1129  mp_integer max_width = 0;
1130  typet max_comp_type;
1131  irep_idt max_comp_name;
1132 
1133  for(const auto &comp : components)
1134  {
1135  auto element_width = pointer_offset_bits(comp.type(), ns);
1136 
1137  if(!element_width.has_value() || *element_width <= max_width)
1138  continue;
1139 
1140  max_width = *element_width;
1141  max_comp_type = comp.type();
1142  max_comp_name = comp.get_name();
1143  }
1144 
1145  if(max_width > 0)
1146  {
1147  byte_extract_exprt tmp(unpacked);
1148  tmp.type() = max_comp_type;
1149 
1150  return union_exprt(
1151  max_comp_name, lower_byte_extract(tmp, ns), src.type());
1152  }
1153  }
1154 
1155  const exprt &root=unpacked.op();
1156  const exprt &offset=unpacked.offset();
1157 
1158  optionalt<typet> subtype;
1159  if(root.type().id() == ID_vector)
1160  subtype = to_vector_type(root.type()).subtype();
1161  else
1162  subtype = to_array_type(root.type()).subtype();
1163 
1164  auto subtype_bits = pointer_offset_bits(*subtype, ns);
1165 
1167  subtype_bits.has_value() && *subtype_bits == 8,
1168  "offset bits are byte aligned");
1169 
1170  auto size_bits = pointer_offset_bits(unpacked.type(), ns);
1171  if(!size_bits.has_value())
1172  {
1173  auto op0_bits = pointer_offset_bits(unpacked.op().type(), ns);
1174  // all cases with non-constant width should have been handled above
1176  op0_bits.has_value(),
1177  "the extracted width or the source width must be known");
1178  size_bits = op0_bits;
1179  }
1180 
1181  mp_integer num_elements =
1182  (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
1183 
1184  // get 'width'-many bytes, and concatenate
1185  const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_elements);
1186  exprt::operandst op;
1187  op.reserve(width_bytes);
1188 
1189  for(std::size_t i=0; i<width_bytes; i++)
1190  {
1191  // the most significant byte comes first in the concatenation!
1192  std::size_t offset_int=
1193  little_endian?(width_bytes-i-1):i;
1194 
1195  plus_exprt offset_i(from_integer(offset_int, offset.type()), offset);
1196  simplify(offset_i, ns);
1197 
1198  mp_integer index = 0;
1199  if(
1200  offset_i.is_constant() &&
1201  (root.id() == ID_array || root.id() == ID_vector) &&
1202  !to_integer(to_constant_expr(offset_i), index) &&
1203  index < root.operands().size() && index >= 0)
1204  {
1205  // offset is constant and in range
1206  op.push_back(root.operands()[numeric_cast_v<std::size_t>(index)]);
1207  }
1208  else
1209  {
1210  op.push_back(index_exprt(root, offset_i));
1211  }
1212  }
1213 
1214  if(width_bytes==1)
1215  {
1216  return simplify_expr(
1217  typecast_exprt::conditional_cast(op.front(), src.type()), ns);
1218  }
1219  else // width_bytes>=2
1220  {
1221  concatenation_exprt concatenation(
1222  std::move(op), bitvector_typet(subtype->id(), width_bytes * 8));
1223 
1224  endianness_mapt map(src.type(), little_endian, ns);
1225  return bv_to_expr(concatenation, src.type(), map, ns);
1226  }
1227 }
1228 
1229 static exprt lower_byte_update(
1230  const byte_update_exprt &src,
1231  const exprt &value_as_byte_array,
1232  const optionalt<exprt> &non_const_update_bound,
1233  const namespacet &ns);
1234 
1245  const byte_update_exprt &src,
1246  const typet &subtype,
1247  const exprt &value_as_byte_array,
1248  const exprt &non_const_update_bound,
1249  const namespacet &ns)
1250 {
1251  // TODO we either need a symbol table here or make array comprehensions
1252  // introduce a scope
1253  static std::size_t array_comprehension_index_counter = 0;
1254  ++array_comprehension_index_counter;
1255  symbol_exprt array_comprehension_index{
1256  "$array_comprehension_index_u_a_v" +
1257  std::to_string(array_comprehension_index_counter),
1258  index_type()};
1259 
1260  binary_predicate_exprt lower_bound{
1262  array_comprehension_index, src.offset().type()),
1263  ID_lt,
1264  src.offset()};
1265  binary_predicate_exprt upper_bound{
1267  array_comprehension_index, non_const_update_bound.type()),
1268  ID_ge,
1270  src.offset(), non_const_update_bound.type()),
1271  non_const_update_bound}};
1272 
1273  if_exprt array_comprehension_body{
1274  or_exprt{std::move(lower_bound), std::move(upper_bound)},
1275  index_exprt{src.op(), array_comprehension_index},
1277  index_exprt{
1278  value_as_byte_array,
1279  minus_exprt{array_comprehension_index,
1281  src.offset(), array_comprehension_index.type())}},
1282  subtype)};
1283 
1284  return simplify_expr(
1285  array_comprehension_exprt{array_comprehension_index,
1286  std::move(array_comprehension_body),
1287  to_array_type(src.type())},
1288  ns);
1289 }
1290 
1301  const byte_update_exprt &src,
1302  const typet &subtype,
1303  const array_exprt &value_as_byte_array,
1304  const optionalt<exprt> &non_const_update_bound,
1305  const namespacet &ns)
1306 {
1307  // apply 'array-update-with' num_elements times
1308  exprt result = src.op();
1309 
1310  for(std::size_t i = 0; i < value_as_byte_array.operands().size(); ++i)
1311  {
1312  const exprt &element = value_as_byte_array.operands()[i];
1313 
1314  const exprt where = simplify_expr(
1315  plus_exprt{src.offset(), from_integer(i, src.offset().type())}, ns);
1316 
1317  // skip elements that wouldn't change (skip over typecasts as we might have
1318  // some signed/unsigned char conversions)
1319  const exprt &e = skip_typecast(element);
1320  if(e.id() == ID_index)
1321  {
1322  const index_exprt &index_expr = to_index_expr(e);
1323  if(index_expr.array() == src.op() && index_expr.index() == where)
1324  continue;
1325  }
1326 
1327  exprt update_value;
1328  if(non_const_update_bound.has_value())
1329  {
1330  update_value = typecast_exprt::conditional_cast(
1332  from_integer(i, non_const_update_bound->type()),
1333  ID_lt,
1334  *non_const_update_bound},
1335  element,
1336  index_exprt{src.op(), where}},
1337  subtype);
1338  }
1339  else
1340  update_value = typecast_exprt::conditional_cast(element, subtype);
1341 
1342  if(result.id() != ID_with)
1343  result = with_exprt{result, where, update_value};
1344  else
1345  result.add_to_operands(where, update_value);
1346  }
1347 
1348  return simplify_expr(std::move(result), ns);
1349 }
1350 
1367  const byte_update_exprt &src,
1368  const typet &subtype,
1369  const exprt &subtype_size,
1370  const exprt &value_as_byte_array,
1371  const exprt &non_const_update_bound,
1372  const exprt &initial_bytes,
1373  const exprt &first_index,
1374  const exprt &first_update_value,
1375  const namespacet &ns)
1376 {
1377  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1378  ? ID_byte_extract_little_endian
1379  : ID_byte_extract_big_endian;
1380 
1381  // TODO we either need a symbol table here or make array comprehensions
1382  // introduce a scope
1383  static std::size_t array_comprehension_index_counter = 0;
1384  ++array_comprehension_index_counter;
1385  symbol_exprt array_comprehension_index{
1386  "$array_comprehension_index_u_a_v_u" +
1387  std::to_string(array_comprehension_index_counter),
1388  index_type()};
1389 
1390  // all arithmetic uses offset/index types
1391  PRECONDITION(subtype_size.type() == src.offset().type());
1392  PRECONDITION(initial_bytes.type() == src.offset().type());
1393  PRECONDITION(first_index.type() == src.offset().type());
1394 
1395  // the bound from where updates start
1396  binary_predicate_exprt lower_bound{
1398  array_comprehension_index, first_index.type()),
1399  ID_lt,
1400  first_index};
1401 
1402  // The actual value of updates other than at the start or end
1403  plus_exprt offset_expr{
1404  initial_bytes,
1405  mult_exprt{subtype_size,
1407  array_comprehension_index, first_index.type()),
1408  first_index}}};
1409  exprt update_value = lower_byte_extract(
1411  extract_opcode, value_as_byte_array, std::move(offset_expr), subtype},
1412  ns);
1413 
1414  // The number of target array/vector elements being replaced, not including
1415  // a possible partial update a the end of the updated range, which is handled
1416  // below: (non_const_update_bound + (subtype_size - 1)) / subtype_size to
1417  // round up to the nearest multiple of subtype_size.
1418  div_exprt updated_elements{
1420  non_const_update_bound, subtype_size.type()),
1421  minus_exprt{subtype_size, from_integer(1, subtype_size.type())}},
1422  subtype_size};
1423 
1424  // The last element to be updated: first_index + updated_elements - 1
1425  plus_exprt last_index{first_index,
1426  minus_exprt{std::move(updated_elements),
1427  from_integer(1, first_index.type())}};
1428 
1429  // The size of a partial update at the end of the updated range, may be zero.
1430  mod_exprt tail_size{
1432  non_const_update_bound, initial_bytes.type()),
1433  initial_bytes},
1434  subtype_size};
1435 
1436  // The bound where updates end, which is conditional on the partial update
1437  // being empty.
1438  binary_predicate_exprt upper_bound{
1440  array_comprehension_index, last_index.type()),
1441  ID_ge,
1442  if_exprt{equal_exprt{tail_size, from_integer(0, tail_size.type())},
1443  last_index,
1444  plus_exprt{last_index, from_integer(1, last_index.type())}}};
1445 
1446  // The actual value of a partial update at the end.
1447  exprt last_update_value = lower_byte_operators(
1449  src.id(),
1450  index_exprt{src.op(), last_index},
1451  from_integer(0, src.offset().type()),
1452  byte_extract_exprt{extract_opcode,
1453  value_as_byte_array,
1455  last_index, subtype_size.type()),
1456  subtype_size},
1457  array_typet{bv_typet{8}, tail_size}}},
1458  ns);
1459 
1460  if_exprt array_comprehension_body{
1461  or_exprt{std::move(lower_bound), std::move(upper_bound)},
1462  index_exprt{src.op(), array_comprehension_index},
1463  if_exprt{
1465  array_comprehension_index, first_index.type()),
1466  first_index},
1467  first_update_value,
1469  array_comprehension_index, last_index.type()),
1470  last_index},
1471  std::move(last_update_value),
1472  std::move(update_value)}}};
1473 
1474  return simplify_expr(
1475  array_comprehension_exprt{array_comprehension_index,
1476  std::move(array_comprehension_body),
1477  to_array_type(src.type())},
1478  ns);
1479 }
1480 
1492  const byte_update_exprt &src,
1493  const typet &subtype,
1494  const exprt &value_as_byte_array,
1495  const optionalt<exprt> &non_const_update_bound,
1496  const namespacet &ns)
1497 {
1498  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1499  ? ID_byte_extract_little_endian
1500  : ID_byte_extract_big_endian;
1501 
1502  // do all arithmetic below using index/offset types - the array theory
1503  // back-end is really picky about indices having the same type
1504  auto subtype_size_opt = size_of_expr(subtype, ns);
1505  CHECK_RETURN(subtype_size_opt.has_value());
1506 
1507  const exprt subtype_size = simplify_expr(
1509  subtype_size_opt.value(), src.offset().type()),
1510  ns);
1511 
1512  // compute the index of the first element of the array/vector that may be
1513  // updated
1514  exprt first_index = div_exprt{src.offset(), subtype_size};
1515  simplify(first_index, ns);
1516 
1517  // compute the offset within that first element
1518  const exprt update_offset = mod_exprt{src.offset(), subtype_size};
1519 
1520  // compute the number of bytes (from the update value) that are going to be
1521  // consumed for updating the first element
1522  exprt initial_bytes = minus_exprt{subtype_size, update_offset};
1523  exprt update_bound;
1524  if(non_const_update_bound.has_value())
1525  {
1526  update_bound = typecast_exprt::conditional_cast(
1527  *non_const_update_bound, subtype_size.type());
1528  }
1529  else
1530  {
1532  value_as_byte_array.id() == ID_array,
1533  "value should be an array expression if the update bound is constant");
1534  update_bound =
1535  from_integer(value_as_byte_array.operands().size(), initial_bytes.type());
1536  }
1537  initial_bytes =
1538  if_exprt{binary_predicate_exprt{initial_bytes, ID_lt, update_bound},
1539  initial_bytes,
1540  update_bound};
1541  simplify(initial_bytes, ns);
1542 
1543  // encode the first update: update the original element at first_index with
1544  // initial_bytes-many bytes extracted from value_as_byte_array
1545  exprt first_update_value = lower_byte_operators(
1547  src.id(),
1548  index_exprt{src.op(), first_index},
1549  update_offset,
1550  byte_extract_exprt{extract_opcode,
1551  value_as_byte_array,
1552  from_integer(0, src.offset().type()),
1553  array_typet{bv_typet{8}, initial_bytes}}},
1554  ns);
1555 
1556  if(value_as_byte_array.id() != ID_array)
1557  {
1559  src,
1560  subtype,
1561  subtype_size,
1562  value_as_byte_array,
1563  *non_const_update_bound,
1564  initial_bytes,
1565  first_index,
1566  first_update_value,
1567  ns);
1568  }
1569 
1570  // We will update one array/vector element at a time - compute the number of
1571  // update values that will be consumed in each step. If we cannot determine a
1572  // constant value at this time we assume it's at least one byte. The
1573  // byte_extract_exprt within the loop uses the symbolic value (subtype_size),
1574  // we just need to make sure we make progress for the loop to terminate.
1575  std::size_t step_size = 1;
1576  if(subtype_size.is_constant())
1577  step_size = numeric_cast_v<std::size_t>(to_constant_expr(subtype_size));
1578  // Given the first update already encoded, keep track of the offset into the
1579  // update value. Again, the expressions within the loop use the symbolic
1580  // value, this is just an optimization in case we can determine a constant
1581  // offset.
1582  std::size_t offset = 0;
1583  if(initial_bytes.is_constant())
1584  offset = numeric_cast_v<std::size_t>(to_constant_expr(initial_bytes));
1585 
1586  with_exprt result{src.op(), first_index, first_update_value};
1587 
1588  std::size_t i = 1;
1589  for(; offset + step_size <= value_as_byte_array.operands().size();
1590  offset += step_size, ++i)
1591  {
1592  exprt where = simplify_expr(
1593  plus_exprt{first_index, from_integer(i, first_index.type())}, ns);
1594 
1595  exprt offset_expr = simplify_expr(
1596  plus_exprt{
1597  initial_bytes,
1598  mult_exprt{subtype_size, from_integer(i - 1, subtype_size.type())}},
1599  ns);
1600 
1601  exprt element = lower_byte_operators(
1603  src.id(),
1604  index_exprt{src.op(), where},
1605  from_integer(0, src.offset().type()),
1606  byte_extract_exprt{extract_opcode,
1607  value_as_byte_array,
1608  std::move(offset_expr),
1609  array_typet{bv_typet{8}, subtype_size}}},
1610  ns);
1611 
1612  result.add_to_operands(std::move(where), std::move(element));
1613  }
1614 
1615  // do the tail
1616  if(offset < value_as_byte_array.operands().size())
1617  {
1618  const std::size_t tail_size =
1619  value_as_byte_array.operands().size() - offset;
1620 
1621  exprt where = simplify_expr(
1622  plus_exprt{first_index, from_integer(i, first_index.type())}, ns);
1623 
1624  exprt element = lower_byte_operators(
1626  src.id(),
1627  index_exprt{src.op(), where},
1628  from_integer(0, src.offset().type()),
1630  extract_opcode,
1631  value_as_byte_array,
1632  from_integer(offset, src.offset().type()),
1633  array_typet{bv_typet{8}, from_integer(tail_size, size_type())}}},
1634  ns);
1635 
1636  result.add_to_operands(std::move(where), std::move(element));
1637  }
1638 
1639  return simplify_expr(std::move(result), ns);
1640 }
1641 
1652  const byte_update_exprt &src,
1653  const typet &subtype,
1654  const exprt &value_as_byte_array,
1655  const optionalt<exprt> &non_const_update_bound,
1656  const namespacet &ns)
1657 {
1658  const bool is_array = src.type().id() == ID_array;
1659  exprt size;
1660  if(is_array)
1661  size = to_array_type(src.type()).size();
1662  else
1663  size = to_vector_type(src.type()).size();
1664 
1665  auto subtype_bits = pointer_offset_bits(subtype, ns);
1666 
1667  // fall back to bytewise updates in all non-constant or dubious cases
1668  if(
1669  !size.is_constant() || !src.offset().is_constant() ||
1670  !subtype_bits.has_value() || *subtype_bits == 0 || *subtype_bits % 8 != 0 ||
1671  non_const_update_bound.has_value() || value_as_byte_array.id() != ID_array)
1672  {
1674  src, subtype, value_as_byte_array, non_const_update_bound, ns);
1675  }
1676 
1677  std::size_t num_elements =
1678  numeric_cast_v<std::size_t>(to_constant_expr(size));
1679  mp_integer offset_bytes =
1680  numeric_cast_v<mp_integer>(to_constant_expr(src.offset()));
1681 
1682  exprt::operandst elements;
1683  elements.reserve(num_elements);
1684 
1685  std::size_t i = 0;
1686  // copy the prefix not affected by the update
1687  for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bytes * 8; ++i)
1688  elements.push_back(index_exprt{src.op(), from_integer(i, index_type())});
1689 
1690  // the modified elements
1691  for(; i < num_elements &&
1692  i * *subtype_bits <
1693  (offset_bytes + value_as_byte_array.operands().size()) * 8;
1694  ++i)
1695  {
1696  mp_integer update_offset = offset_bytes - i * (*subtype_bits / 8);
1697  mp_integer update_elements = *subtype_bits / 8;
1698  exprt::operandst::const_iterator first =
1699  value_as_byte_array.operands().begin();
1700  exprt::operandst::const_iterator end = value_as_byte_array.operands().end();
1701  if(update_offset < 0)
1702  {
1703  INVARIANT(
1704  value_as_byte_array.operands().size() > -update_offset,
1705  "indices past the update should be handled above");
1706  first += numeric_cast_v<std::ptrdiff_t>(-update_offset);
1707  }
1708  else
1709  {
1710  update_elements -= update_offset;
1711  INVARIANT(
1712  update_elements > 0,
1713  "indices before the update should be handled above");
1714  }
1715 
1716  if(std::distance(first, end) > update_elements)
1717  end = first + numeric_cast_v<std::ptrdiff_t>(update_elements);
1718  exprt::operandst update_values{first, end};
1719  const std::size_t update_size = update_values.size();
1720 
1721  const byte_update_exprt bu{
1722  src.id(),
1723  index_exprt{src.op(), from_integer(i, index_type())},
1724  from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
1725  array_exprt{
1726  std::move(update_values),
1727  array_typet{bv_typet{8}, from_integer(update_size, size_type())}}};
1728  elements.push_back(lower_byte_operators(bu, ns));
1729  }
1730 
1731  // copy the tail not affected by the update
1732  for(; i < num_elements; ++i)
1733  elements.push_back(index_exprt{src.op(), from_integer(i, index_type())});
1734 
1735  if(is_array)
1736  return simplify_expr(
1737  array_exprt{std::move(elements), to_array_type(src.type())}, ns);
1738  else
1739  return simplify_expr(
1740  vector_exprt{std::move(elements), to_vector_type(src.type())}, ns);
1741 }
1742 
1753  const byte_update_exprt &src,
1754  const struct_typet &struct_type,
1755  const exprt &value_as_byte_array,
1756  const optionalt<exprt> &non_const_update_bound,
1757  const namespacet &ns)
1758 {
1759  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1760  ? ID_byte_extract_little_endian
1761  : ID_byte_extract_big_endian;
1762 
1763  exprt::operandst elements;
1764  elements.reserve(struct_type.components().size());
1765 
1767  for(const auto &comp : struct_type.components())
1768  {
1769  auto element_width = pointer_offset_bits(comp.type(), ns);
1770 
1771  exprt member = member_exprt{src.op(), comp.get_name(), comp.type()};
1772 
1773  // compute the update offset relative to this struct member - will be
1774  // negative if we are already in the middle of the update or beyond it
1775  exprt offset = simplify_expr(
1776  minus_exprt{src.offset(),
1777  from_integer(member_offset_bits / 8, src.offset().type())},
1778  ns);
1779  auto offset_bytes = numeric_cast<mp_integer>(offset);
1780  // we don't need to update anything when
1781  // 1) the update offset is greater than the end of this member (thus the
1782  // relative offset is greater than this element) or
1783  // 2) the update offset plus the size of the update is less than the member
1784  // offset
1785  if(
1786  offset_bytes.has_value() &&
1787  (*offset_bytes * 8 >= *element_width ||
1788  (value_as_byte_array.id() == ID_array && *offset_bytes < 0 &&
1789  -*offset_bytes >= value_as_byte_array.operands().size())))
1790  {
1791  elements.push_back(std::move(member));
1792  member_offset_bits += *element_width;
1793  continue;
1794  }
1795  else if(!offset_bytes.has_value())
1796  {
1797  // The offset to update is not constant; abort the attempt to update
1798  // indiviual struct members and instead turn the operand-to-be-updated
1799  // into a byte array, which we know how to update even if the offset is
1800  // non-constant.
1801  auto src_size_opt = size_of_expr(src.type(), ns);
1802  CHECK_RETURN(src_size_opt.has_value());
1803 
1804  const byte_extract_exprt byte_extract_expr{
1805  extract_opcode,
1806  src.op(),
1807  from_integer(0, src.offset().type()),
1808  array_typet{bv_typet{8}, src_size_opt.value()}};
1809 
1810  byte_update_exprt bu = src;
1811  bu.set_op(lower_byte_extract(byte_extract_expr, ns));
1812  bu.type() = bu.op().type();
1813 
1814  return lower_byte_extract(
1816  extract_opcode,
1818  bu, value_as_byte_array, non_const_update_bound, ns),
1819  from_integer(0, src.offset().type()),
1820  src.type()},
1821  ns);
1822  }
1823 
1824  // We now need to figure out how many bytes to consume from the update
1825  // value. If the size of the update is unknown, then we need to leave some
1826  // of this work to a back-end solver via the non_const_update_bound branch
1827  // below.
1828  mp_integer update_elements = (*element_width + 7) / 8;
1829  std::size_t first = 0;
1830  if(*offset_bytes < 0)
1831  {
1832  offset = from_integer(0, src.offset().type());
1833  INVARIANT(
1834  value_as_byte_array.id() != ID_array ||
1835  value_as_byte_array.operands().size() > -*offset_bytes,
1836  "members past the update should be handled above");
1837  first = numeric_cast_v<std::size_t>(-*offset_bytes);
1838  }
1839  else
1840  {
1841  update_elements -= *offset_bytes;
1842  INVARIANT(
1843  update_elements > 0,
1844  "members before the update should be handled above");
1845  }
1846 
1847  // Now that we have an idea on how many bytes we need from the update value,
1848  // determine the exact range [first, end) in the update value, and create
1849  // that sequence of bytes (via instantiate_byte_array).
1850  std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1851  if(value_as_byte_array.id() == ID_array)
1852  end = std::min(end, value_as_byte_array.operands().size());
1853  exprt::operandst update_values =
1854  instantiate_byte_array(value_as_byte_array, first, end, ns);
1855  const std::size_t update_size = update_values.size();
1856 
1857  // With an upper bound on the size of the update established, construct the
1858  // actual update expression. If the exact size of the update is unknown,
1859  // make the size expression conditional.
1860  exprt update_size_expr = from_integer(update_size, size_type());
1861  array_exprt update_expr{std::move(update_values),
1862  array_typet{bv_typet{8}, update_size_expr}};
1863  optionalt<exprt> member_update_bound;
1864  if(non_const_update_bound.has_value())
1865  {
1866  // The size of the update is not constant, and thus is to be symbolically
1867  // bound; first see how many bytes we have left in the update:
1868  // non_const_update_bound > first ? non_const_update_bound - first: 0
1869  const exprt remaining_update_bytes = typecast_exprt::conditional_cast(
1870  if_exprt{
1872  *non_const_update_bound,
1873  ID_gt,
1874  from_integer(first, non_const_update_bound->type())},
1875  minus_exprt{*non_const_update_bound,
1876  from_integer(first, non_const_update_bound->type())},
1877  from_integer(0, non_const_update_bound->type())},
1878  size_type());
1879  // Now take the minimum of update-bytes-left and the previously computed
1880  // size of the member to be updated:
1881  update_size_expr = if_exprt{
1882  binary_predicate_exprt{update_size_expr, ID_lt, remaining_update_bytes},
1883  update_size_expr,
1884  remaining_update_bytes};
1885  simplify(update_size_expr, ns);
1886  member_update_bound = std::move(update_size_expr);
1887  }
1888 
1889  // We have established the bytes to use for the update, but now need to
1890  // account for sub-byte members.
1891  const std::size_t shift =
1892  numeric_cast_v<std::size_t>(member_offset_bits % 8);
1893  const std::size_t element_bits_int =
1894  numeric_cast_v<std::size_t>(*element_width);
1895 
1896  const bool little_endian = src.id() == ID_byte_update_little_endian;
1897  if(shift != 0)
1898  {
1899  member = concatenation_exprt{
1900  typecast_exprt::conditional_cast(member, bv_typet{element_bits_int}),
1901  from_integer(0, bv_typet{shift}),
1902  bv_typet{shift + element_bits_int}};
1903 
1904  if(!little_endian)
1905  to_concatenation_expr(member).op0().swap(
1906  to_concatenation_expr(member).op1());
1907  }
1908 
1909  // Finally construct the updated member.
1910  byte_update_exprt bu{src.id(), std::move(member), offset, update_expr};
1911  exprt updated_element =
1912  lower_byte_update(bu, update_expr, member_update_bound, ns);
1913 
1914  if(shift == 0)
1915  elements.push_back(updated_element);
1916  else
1917  {
1918  elements.push_back(typecast_exprt::conditional_cast(
1919  extractbits_exprt{updated_element,
1920  element_bits_int - 1 + (little_endian ? shift : 0),
1921  (little_endian ? shift : 0),
1922  bv_typet{element_bits_int}},
1923  comp.type()));
1924  }
1925 
1926  member_offset_bits += *element_width;
1927  }
1928 
1929  return simplify_expr(struct_exprt{std::move(elements), struct_type}, ns);
1930 }
1931 
1942  const byte_update_exprt &src,
1943  const union_typet &union_type,
1944  const exprt &value_as_byte_array,
1945  const optionalt<exprt> &non_const_update_bound,
1946  const namespacet &ns)
1947 {
1948  const union_typet::componentst &components = union_type.components();
1949 
1950  mp_integer max_width = 0;
1951  typet max_comp_type;
1952  irep_idt max_comp_name;
1953 
1954  for(const auto &comp : components)
1955  {
1956  auto element_width = pointer_offset_bits(comp.type(), ns);
1957 
1958  if(!element_width.has_value() || *element_width <= max_width)
1959  continue;
1960 
1961  max_width = *element_width;
1962  max_comp_type = comp.type();
1963  max_comp_name = comp.get_name();
1964  }
1965 
1967  max_width > 0,
1968  "lower_byte_update of union of unknown size is not supported");
1969 
1970  byte_update_exprt bu = src;
1971  bu.set_op(member_exprt{src.op(), max_comp_name, max_comp_type});
1972  bu.type() = max_comp_type;
1973 
1974  return union_exprt{
1975  max_comp_name,
1976  lower_byte_update(bu, value_as_byte_array, non_const_update_bound, ns),
1977  src.type()};
1978 }
1979 
1989  const byte_update_exprt &src,
1990  const exprt &value_as_byte_array,
1991  const optionalt<exprt> &non_const_update_bound,
1992  const namespacet &ns)
1993 {
1994  if(src.type().id() == ID_array || src.type().id() == ID_vector)
1995  {
1996  optionalt<typet> subtype;
1997  if(src.type().id() == ID_vector)
1998  subtype = to_vector_type(src.type()).subtype();
1999  else
2000  subtype = to_array_type(src.type()).subtype();
2001 
2002  auto element_width = pointer_offset_bits(*subtype, ns);
2003  CHECK_RETURN(element_width.has_value());
2004  CHECK_RETURN(*element_width > 0);
2005  CHECK_RETURN(*element_width % 8 == 0);
2006 
2007  if(*element_width == 8)
2008  {
2009  if(value_as_byte_array.id() != ID_array)
2010  {
2012  non_const_update_bound.has_value(),
2013  "constant update bound should yield an array expression");
2015  src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2016  }
2017 
2019  src,
2020  *subtype,
2021  to_array_expr(value_as_byte_array),
2022  non_const_update_bound,
2023  ns);
2024  }
2025  else
2027  src, *subtype, value_as_byte_array, non_const_update_bound, ns);
2028  }
2029  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
2030  {
2032  src,
2033  to_struct_type(ns.follow(src.type())),
2034  value_as_byte_array,
2035  non_const_update_bound,
2036  ns);
2037  result.type() = src.type();
2038  return result;
2039  }
2040  else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
2041  {
2042  exprt result = lower_byte_update_union(
2043  src,
2044  to_union_type(ns.follow(src.type())),
2045  value_as_byte_array,
2046  non_const_update_bound,
2047  ns);
2048  result.type() = src.type();
2049  return result;
2050  }
2051  else if(
2053  src.type().id() == ID_c_enum || src.type().id() == ID_c_enum_tag)
2054  {
2055  // mask out the bits to be updated, shift the value according to the
2056  // offset and bit-or
2057  const auto type_width = pointer_offset_bits(src.type(), ns);
2058  CHECK_RETURN(type_width.has_value() && *type_width > 0);
2059  const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2060 
2061  exprt::operandst update_bytes;
2062  if(value_as_byte_array.id() == ID_array)
2063  update_bytes = value_as_byte_array.operands();
2064  else
2065  {
2066  update_bytes =
2067  instantiate_byte_array(value_as_byte_array, 0, (type_bits + 7) / 8, ns);
2068  }
2069 
2070  if(non_const_update_bound.has_value())
2071  {
2072  const exprt src_as_bytes = unpack_rec(
2073  src.op(),
2074  src.id() == ID_byte_update_little_endian,
2075  mp_integer{0},
2076  mp_integer{update_bytes.size()},
2077  ns);
2078  CHECK_RETURN(src_as_bytes.id() == ID_array);
2079  CHECK_RETURN(src_as_bytes.operands().size() == update_bytes.size());
2080  for(std::size_t i = 0; i < update_bytes.size(); ++i)
2081  {
2082  update_bytes[i] =
2084  from_integer(i, non_const_update_bound->type()),
2085  ID_lt,
2086  *non_const_update_bound},
2087  update_bytes[i],
2088  src_as_bytes.operands()[i]};
2089  }
2090  }
2091 
2092  const std::size_t update_size = update_bytes.size();
2093  const std::size_t width = std::max(type_bits, update_size * 8);
2094 
2095  const bool is_little_endian = src.id() == ID_byte_update_little_endian;
2096 
2097  // build mask
2098  exprt mask;
2099  if(is_little_endian)
2100  mask = from_integer(power(2, update_size * 8) - 1, bv_typet{width});
2101  else
2102  {
2103  mask = from_integer(
2104  power(2, width) - power(2, width - update_size * 8), bv_typet{width});
2105  }
2106 
2107  const typet &offset_type = src.offset().type();
2108  mult_exprt offset_times_eight{src.offset(), from_integer(8, offset_type)};
2109 
2110  const binary_predicate_exprt offset_ge_zero{
2111  offset_times_eight, ID_ge, from_integer(0, offset_type)};
2112 
2113  if_exprt mask_shifted{offset_ge_zero,
2114  shl_exprt{mask, offset_times_eight},
2115  lshr_exprt{mask, offset_times_eight}};
2116  if(!is_little_endian)
2117  mask_shifted.true_case().swap(mask_shifted.false_case());
2118 
2119  // original_bits &= ~mask
2120  exprt val_before =
2121  typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits});
2122  if(width > type_bits)
2123  {
2124  val_before =
2125  concatenation_exprt{from_integer(0, bv_typet{width - type_bits}),
2126  val_before,
2127  bv_typet{width}};
2128 
2129  if(!is_little_endian)
2130  to_concatenation_expr(val_before)
2131  .op0()
2132  .swap(to_concatenation_expr(val_before).op1());
2133  }
2134  bitand_exprt bitand_expr{val_before, bitnot_exprt{mask_shifted}};
2135 
2136  // concatenate and zero-extend the value
2137  concatenation_exprt value{update_bytes, bv_typet{update_size * 8}};
2138  if(is_little_endian)
2139  std::reverse(value.operands().begin(), value.operands().end());
2140 
2141  exprt zero_extended;
2142  if(width > update_size * 8)
2143  {
2144  zero_extended =
2145  concatenation_exprt{from_integer(0, bv_typet{width - update_size * 8}),
2146  value,
2147  bv_typet{width}};
2148 
2149  if(!is_little_endian)
2150  to_concatenation_expr(zero_extended)
2151  .op0()
2152  .swap(to_concatenation_expr(zero_extended).op1());
2153  }
2154  else
2155  zero_extended = value;
2156 
2157  // shift the value
2158  if_exprt value_shifted{offset_ge_zero,
2159  shl_exprt{zero_extended, offset_times_eight},
2160  lshr_exprt{zero_extended, offset_times_eight}};
2161  if(!is_little_endian)
2162  value_shifted.true_case().swap(value_shifted.false_case());
2163 
2164  // original_bits |= newvalue
2165  bitor_exprt bitor_expr{bitand_expr, value_shifted};
2166 
2167  if(!is_little_endian && width > type_bits)
2168  {
2169  return simplify_expr(
2172  bitor_expr, width - 1, width - type_bits, bv_typet{type_bits}},
2173  src.type()),
2174  ns);
2175  }
2176 
2177  return simplify_expr(
2178  typecast_exprt::conditional_cast(bitor_expr, src.type()), ns);
2179  }
2180  else
2181  {
2183  false, "lower_byte_update does not yet support ", src.type().id_string());
2184  }
2185 }
2186 
2188 {
2190  src.id() == ID_byte_update_little_endian ||
2191  src.id() == ID_byte_update_big_endian,
2192  "byte update expression should either be little or big endian");
2193 
2194  // An update of a void-typed object or update by a void-typed value is the
2195  // source operand (this is questionable, but may arise when dereferencing
2196  // invalid pointers).
2197  if(src.type().id() == ID_empty || src.value().type().id() == ID_empty)
2198  return src.op();
2199 
2200  // byte_update lowering proceeds as follows:
2201  // 1) Determine the size of the update, with the size of the object to be
2202  // updated as an upper bound. We fail if neither can be determined.
2203  // 2) Turn the update value into a byte array of the size determined above.
2204  // 3) If the offset is not constant, turn the object into a byte array, and
2205  // use a "with" expression to encode the update; else update the values in
2206  // place.
2207  // 4) Construct a new object.
2208  optionalt<exprt> non_const_update_bound;
2209  auto update_size_expr_opt = size_of_expr(src.value().type(), ns);
2210  CHECK_RETURN(update_size_expr_opt.has_value());
2211  simplify(update_size_expr_opt.value(), ns);
2212 
2213  if(!update_size_expr_opt.value().is_constant())
2214  non_const_update_bound = *update_size_expr_opt;
2215 
2216  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
2217  ? ID_byte_extract_little_endian
2218  : ID_byte_extract_big_endian;
2219 
2220  const byte_extract_exprt byte_extract_expr{
2221  extract_opcode,
2222  src.value(),
2223  from_integer(0, src.offset().type()),
2224  array_typet{bv_typet{8}, *update_size_expr_opt}};
2225 
2226  const exprt value_as_byte_array = lower_byte_extract(byte_extract_expr, ns);
2227 
2228  exprt result =
2229  lower_byte_update(src, value_as_byte_array, non_const_update_bound, ns);
2230  return result;
2231 }
2232 
2233 bool has_byte_operator(const exprt &src)
2234 {
2235  if(src.id()==ID_byte_update_little_endian ||
2236  src.id()==ID_byte_update_big_endian ||
2237  src.id()==ID_byte_extract_little_endian ||
2238  src.id()==ID_byte_extract_big_endian)
2239  return true;
2240 
2241  forall_operands(it, src)
2242  if(has_byte_operator(*it))
2243  return true;
2244 
2245  return false;
2246 }
2247 
2249 {
2250  exprt tmp=src;
2251 
2252  // destroys any sharing, should use hash table
2253  Forall_operands(it, tmp)
2254  {
2255  *it = lower_byte_operators(*it, ns);
2256  }
2257 
2258  if(src.id()==ID_byte_update_little_endian ||
2259  src.id()==ID_byte_update_big_endian)
2260  return lower_byte_update(to_byte_update_expr(tmp), ns);
2261  else if(src.id()==ID_byte_extract_little_endian ||
2262  src.id()==ID_byte_extract_big_endian)
2263  return lower_byte_extract(to_byte_extract_expr(tmp), ns);
2264  else
2265  return tmp;
2266 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3079
bv_to_vector_expr
static vector_exprt bv_to_vector_expr(const exprt &bitvector_expr, const vector_typet &vector_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a vector-typed expression.
Definition: byte_operators.cpp:164
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
unpack_complex
static array_exprt unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
Rewrite a complex_exprt into its individual bytes.
Definition: byte_operators.cpp:665
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2050
typet::subtype
const typet & subtype() const
Definition: type.h:47
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:217
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:78
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
arith_tools.h
to_array_expr
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1474
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
member_offset_bits
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:64
typet
The type of an expression, extends irept.
Definition: type.h:29
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:54
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1353
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2993
has_byte_operator
bool has_byte_operator(const exprt &src)
Definition: byte_operators.cpp:2233
replace_symbol.h
unpack_array_vector
static exprt unpack_array_vector(const exprt &src, const optionalt< mp_integer > &src_size, const mp_integer &element_bits, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
Rewrite an array or vector into its individual bytes.
Definition: byte_operators.cpp:372
lower_byte_update
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
Definition: byte_operators.cpp:1988
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1757
union_exprt
Union constructor from single element.
Definition: std_expr.h:1579
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
bv_to_expr
static exprt bv_to_expr(const exprt &bitvector_expr, const typet &target_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an expression of type target_type.
Definition: byte_operators.cpp:262
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:887
lower_byte_extract
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...
Definition: byte_operators.cpp:902
string_constant.h
lower_byte_update_array_vector
static exprt lower_byte_update_array_vector(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand using the byte array value_as_byte_array as ...
Definition: byte_operators.cpp:1651
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
byte_update_exprt::set_op
void set_op(exprt e)
Definition: byte_operators.h:96
complex_typet
Complex numbers made of pair of given subtype.
Definition: std_types.h:1790
vector_typet
The vector type.
Definition: std_types.h:1750
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
concatenation_exprt
Concatenation of bit-vector operands.
Definition: std_expr.h:4096
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1543
lshr_exprt
Logical right shift.
Definition: std_expr.h:2643
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1815
div_exprt
Division.
Definition: std_expr.h:1037
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
string_constantt
Definition: string_constant.h:16
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1196
expr_lowering.h
to_concatenation_expr
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: std_expr.h:4124
lower_byte_update_byte_array_vector
static exprt lower_byte_update_byte_array_vector(const byte_update_exprt &src, const typet &subtype, const array_exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte array value_as_byte_array as updat...
Definition: byte_operators.cpp:1300
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1645
array_typet::size
const exprt & size() const
Definition: std_types.h:973
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
bv_to_struct_expr
static struct_exprt bv_to_struct_expr(const exprt &bitvector_expr, const struct_typet &struct_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a struct-typed expression.
Definition: byte_operators.cpp:64
byte_operators.h
Expression classes for byte-level operators.
bitor_exprt
Bit-wise OR.
Definition: std_expr.h:2417
endianness_mapt::number_of_bits
size_t number_of_bits() const
Definition: endianness_map.h:56
or_exprt
Boolean OR.
Definition: std_expr.h:2274
lower_byte_update_array_vector_non_const
static exprt lower_byte_update_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
Definition: byte_operators.cpp:1491
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
lower_byte_update_struct
static exprt lower_byte_update_struct(const byte_update_exprt &src, const struct_typet &struct_type, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a struct typed operand using the byte array value_as_byte_array as update ...
Definition: byte_operators.cpp:1752
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:40
failed
static bool failed(bool error_indicator)
Definition: symtab2gb_parse_options.cpp:34
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:114
boundst
Definition: byte_operators.cpp:31
lower_byte_update_array_vector_unbounded
static exprt lower_byte_update_array_vector_unbounded(const byte_update_exprt &src, const typet &subtype, const exprt &subtype_size, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const exprt &initial_bytes, const exprt &first_index, const exprt &first_update_value, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
Definition: byte_operators.cpp:1366
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
nil_exprt
The NIL expression.
Definition: std_expr.h:4002
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
endianness_mapt::map_bit
size_t map_bit(size_t bit) const
Definition: endianness_map.h:48
lower_byte_operators
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
Definition: byte_operators.cpp:2248
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:992
bv_to_complex_expr
static complex_exprt bv_to_complex_expr(const exprt &bitvector_expr, const complex_typet &complex_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a complex-typed expression.
Definition: byte_operators.cpp:209
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
index_exprt::index
exprt & index()
Definition: std_expr.h:1325
index_exprt::array
exprt & array()
Definition: std_expr.h:1315
irept::swap
void swap(irept &irep)
Definition: irep.h:463
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
instantiate_byte_array
static exprt::operandst instantiate_byte_array(const exprt &src, std::size_t lower_bound, std::size_t upper_bound, const namespacet &ns)
Build the individual bytes to be used in an update.
Definition: byte_operators.cpp:333
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1689
union_typet
The union type.
Definition: std_types.h:393
bitand_exprt
Bit-wise AND.
Definition: std_expr.h:2489
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
lower_byte_update_union
static exprt lower_byte_update_union(const byte_update_exprt &src, const union_typet &union_type, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a union typed operand using the byte array value_as_byte_array as update v...
Definition: byte_operators.cpp:1941
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:268
minus_exprt
Binary minus.
Definition: std_expr.h:946
lower_byte_extract_complex
static optionalt< exprt > lower_byte_extract_complex(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const namespacet &ns)
Rewrite a byte extraction of a complex-typed result to byte extraction of the individual components t...
Definition: byte_operators.cpp:871
map_bounds
static boundst map_bounds(const endianness_mapt &endianness_map, std::size_t lower_bound, std::size_t upper_bound)
Map bit boundaries according to endianness.
Definition: byte_operators.cpp:37
endianness_map.h
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2373
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:41
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3434
expr_util.h
Deprecated expression utility functions.
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
array_typet
Arrays with given size.
Definition: std_types.h:965
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:1030
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
bv_to_array_expr
static array_exprt bv_to_array_expr(const exprt &bitvector_expr, const array_typet &array_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an array-typed expression.
Definition: byte_operators.cpp:111
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
byte_update_exprt::value
exprt & value()
Definition: byte_operators.h:94
PRECONDITION_WITH_DIAGNOSTICS
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:465
unpack_rec
static exprt unpack_rec(const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns, bool unpack_byte_array=false)
Rewrite an object into its individual bytes.
Definition: byte_operators.cpp:711
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:85
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1802
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:155
endianness_mapt
Maps a big-endian offset to a little-endian offset.
Definition: endianness_map.h:32
byte_update_exprt::offset
exprt & offset()
Definition: byte_operators.h:92
unpack_struct
static array_exprt unpack_struct(const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
Rewrite a struct-typed expression into its individual bytes.
Definition: byte_operators.cpp:542
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1775
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
boundst::ub
std::size_t ub
Definition: byte_operators.cpp:33
boundst::lb
std::size_t lb
Definition: byte_operators.cpp:32
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2726
exprt::operands
operandst & operands()
Definition: expr.h:95
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:422
index_exprt
Array index operator.
Definition: std_expr.h:1299
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2042
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
byte_update_exprt::op
exprt & op()
Definition: byte_operators.h:90
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:4451
constant_exprt
A constant literal expression.
Definition: std_expr.h:3935
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:817
member_offset_expr
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:226
lower_byte_update_byte_array_vector_non_const
static exprt lower_byte_update_byte_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte-array typed expression value_as_by...
Definition: byte_operators.cpp:1244
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1438
c_types.h
process_bit_fields
static void process_bit_fields(exprt::operandst &&bit_fields, std::size_t total_bits, exprt::operandst &dest, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
Extract bytes from a sequence of bitvector-typed elements.
Definition: byte_operators.cpp:512
can_cast_type< bitvector_typet >
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:1064
bv_typet
Fixed-width bit-vector without numerical interpretation.
Definition: std_types.h:1106
mod_exprt
Modulo.
Definition: std_expr.h:1106
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
shl_exprt
Left shift.
Definition: std_expr.h:2590
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3968