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/bitvector_expr.h>
15 #include <util/byte_operators.h>
16 #include <util/c_types.h>
17 #include <util/endianness_map.h>
18 #include <util/expr_util.h>
19 #include <util/namespace.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  std::swap(result.lb, result.ub);
54  }
55 
56  return result;
57 }
58 
60 bitvector_typet adjust_width(const typet &src, std::size_t new_width)
61 {
62  if(src.id() == ID_unsignedbv)
63  return unsignedbv_typet(new_width);
64  else if(src.id() == ID_signedbv)
65  return signedbv_typet(new_width);
66  else if(src.id() == ID_bv)
67  return bv_typet(new_width);
68  else if(src.id() == ID_c_enum) // we use the underlying type
69  return adjust_width(to_c_enum_type(src).underlying_type(), new_width);
70  else if(src.id() == ID_c_bit_field)
71  return c_bit_field_typet(
72  to_c_bit_field_type(src).underlying_type(), new_width);
73  else
74  PRECONDITION(false);
75 }
76 
80  const exprt &bitvector_expr,
81  const struct_typet &struct_type,
82  const endianness_mapt &endianness_map,
83  const namespacet &ns)
84 {
85  const struct_typet::componentst &components = struct_type.components();
86 
87  exprt::operandst operands;
88  operands.reserve(components.size());
89  std::size_t member_offset_bits = 0;
90  for(const auto &comp : components)
91  {
92  const auto component_bits_opt = pointer_offset_bits(comp.type(), ns);
93  std::size_t component_bits;
94  if(component_bits_opt.has_value())
95  component_bits = numeric_cast_v<std::size_t>(*component_bits_opt);
96  else
97  component_bits = to_bitvector_type(bitvector_expr.type()).get_width() -
99 
100  if(component_bits == 0)
101  {
102  operands.push_back(constant_exprt{irep_idt{}, comp.type()});
103  continue;
104  }
105 
106  const auto bounds = map_bounds(
107  endianness_map,
109  member_offset_bits + component_bits - 1);
110  bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits);
111  operands.push_back(bv_to_expr(
112  extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
113  comp.type(),
114  endianness_map,
115  ns));
116 
117  if(component_bits_opt.has_value())
118  member_offset_bits += component_bits;
119  }
120 
121  return struct_exprt{std::move(operands), struct_type};
122 }
123 
127  const exprt &bitvector_expr,
128  const union_typet &union_type,
129  const endianness_mapt &endianness_map,
130  const namespacet &ns)
131 {
132  const union_typet::componentst &components = union_type.components();
133 
134  // empty union, handled the same way as done in expr_initializert
135  if(components.empty())
136  return union_exprt{irep_idt{}, nil_exprt{}, union_type};
137 
138  const auto widest_member = union_type.find_widest_union_component(ns);
139 
140  std::size_t component_bits;
141  if(widest_member.has_value())
142  component_bits = numeric_cast_v<std::size_t>(widest_member->second);
143  else
144  component_bits = to_bitvector_type(bitvector_expr.type()).get_width();
145 
146  if(component_bits == 0)
147  {
148  return union_exprt{components.front().get_name(),
149  constant_exprt{irep_idt{}, components.front().type()},
150  union_type};
151  }
152 
153  const auto bounds = map_bounds(endianness_map, 0, component_bits - 1);
154  bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits);
155  const irep_idt &component_name = widest_member.has_value()
156  ? widest_member->first.get_name()
157  : components.front().get_name();
158  const typet &component_type = widest_member.has_value()
159  ? widest_member->first.type()
160  : components.front().type();
161  return union_exprt{
162  component_name,
163  bv_to_expr(
164  extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
165  component_type,
166  endianness_map,
167  ns),
168  union_type};
169 }
170 
174  const exprt &bitvector_expr,
175  const array_typet &array_type,
176  const endianness_mapt &endianness_map,
177  const namespacet &ns)
178 {
179  auto num_elements = numeric_cast<std::size_t>(array_type.size());
180  auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
181 
182  const std::size_t total_bits =
183  to_bitvector_type(bitvector_expr.type()).get_width();
184  if(!num_elements.has_value())
185  {
186  if(!subtype_bits.has_value() || *subtype_bits == 0)
187  num_elements = total_bits;
188  else
189  num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
190  }
192  !num_elements.has_value() || !subtype_bits.has_value() ||
193  *subtype_bits * *num_elements == total_bits,
194  "subtype width times array size should be total bitvector width");
195 
196  exprt::operandst operands;
197  operands.reserve(*num_elements);
198  for(std::size_t i = 0; i < *num_elements; ++i)
199  {
200  if(subtype_bits.has_value())
201  {
202  const std::size_t subtype_bits_int =
203  numeric_cast_v<std::size_t>(*subtype_bits);
204  const auto bounds = map_bounds(
205  endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
206  bitvector_typet type =
207  adjust_width(bitvector_expr.type(), subtype_bits_int);
208  operands.push_back(bv_to_expr(
210  bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
211  array_type.element_type(),
212  endianness_map,
213  ns));
214  }
215  else
216  {
217  operands.push_back(bv_to_expr(
218  bitvector_expr, array_type.element_type(), endianness_map, ns));
219  }
220  }
221 
222  return array_exprt{std::move(operands), array_type};
223 }
224 
228  const exprt &bitvector_expr,
229  const vector_typet &vector_type,
230  const endianness_mapt &endianness_map,
231  const namespacet &ns)
232 {
233  const std::size_t num_elements =
234  numeric_cast_v<std::size_t>(vector_type.size());
235  auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
237  !subtype_bits.has_value() ||
238  *subtype_bits * num_elements ==
239  to_bitvector_type(bitvector_expr.type()).get_width(),
240  "subtype width times vector size should be total bitvector width");
241 
242  exprt::operandst operands;
243  operands.reserve(num_elements);
244  for(std::size_t i = 0; i < num_elements; ++i)
245  {
246  if(subtype_bits.has_value())
247  {
248  const std::size_t subtype_bits_int =
249  numeric_cast_v<std::size_t>(*subtype_bits);
250  const auto bounds = map_bounds(
251  endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
252  bitvector_typet type =
253  adjust_width(bitvector_expr.type(), subtype_bits_int);
254  operands.push_back(bv_to_expr(
256  bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
257  vector_type.element_type(),
258  endianness_map,
259  ns));
260  }
261  else
262  {
263  operands.push_back(bv_to_expr(
264  bitvector_expr, vector_type.element_type(), endianness_map, ns));
265  }
266  }
267 
268  return vector_exprt{std::move(operands), vector_type};
269 }
270 
274  const exprt &bitvector_expr,
275  const complex_typet &complex_type,
276  const endianness_mapt &endianness_map,
277  const namespacet &ns)
278 {
279  const std::size_t total_bits =
280  to_bitvector_type(bitvector_expr.type()).get_width();
281  const auto subtype_bits_opt = pointer_offset_bits(complex_type.subtype(), ns);
282  std::size_t subtype_bits;
283  if(subtype_bits_opt.has_value())
284  {
285  subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
287  subtype_bits * 2 == total_bits,
288  "subtype width should be half of the total bitvector width");
289  }
290  else
291  subtype_bits = total_bits / 2;
292 
293  const auto bounds_real = map_bounds(endianness_map, 0, subtype_bits - 1);
294  const auto bounds_imag =
295  map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
296 
297  const bitvector_typet type =
298  adjust_width(bitvector_expr.type(), subtype_bits);
299 
300  return complex_exprt{
301  bv_to_expr(
302  extractbits_exprt{bitvector_expr, bounds_real.ub, bounds_real.lb, type},
303  complex_type.subtype(),
304  endianness_map,
305  ns),
306  bv_to_expr(
307  extractbits_exprt{bitvector_expr, bounds_imag.ub, bounds_imag.lb, type},
308  complex_type.subtype(),
309  endianness_map,
310  ns),
311  complex_type};
312 }
313 
328  const exprt &bitvector_expr,
329  const typet &target_type,
330  const endianness_mapt &endianness_map,
331  const namespacet &ns)
332 {
334 
335  if(
336  can_cast_type<bitvector_typet>(target_type) ||
337  target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
338  target_type.id() == ID_string)
339  {
340  std::size_t width = to_bitvector_type(bitvector_expr.type()).get_width();
341  exprt bv_expr =
342  typecast_exprt::conditional_cast(bitvector_expr, bv_typet{width});
343  return simplify_expr(
344  typecast_exprt::conditional_cast(bv_expr, target_type), ns);
345  }
346 
347  if(target_type.id() == ID_struct)
348  {
349  return bv_to_struct_expr(
350  bitvector_expr, to_struct_type(target_type), endianness_map, ns);
351  }
352  else if(target_type.id() == ID_struct_tag)
353  {
355  bitvector_expr,
356  ns.follow_tag(to_struct_tag_type(target_type)),
357  endianness_map,
358  ns);
359  result.type() = target_type;
360  return std::move(result);
361  }
362  else if(target_type.id() == ID_union)
363  {
364  return bv_to_union_expr(
365  bitvector_expr, to_union_type(target_type), endianness_map, ns);
366  }
367  else if(target_type.id() == ID_union_tag)
368  {
369  union_exprt result = bv_to_union_expr(
370  bitvector_expr,
371  ns.follow_tag(to_union_tag_type(target_type)),
372  endianness_map,
373  ns);
374  result.type() = target_type;
375  return std::move(result);
376  }
377  else if(target_type.id() == ID_array)
378  {
379  return bv_to_array_expr(
380  bitvector_expr, to_array_type(target_type), endianness_map, ns);
381  }
382  else if(target_type.id() == ID_vector)
383  {
384  return bv_to_vector_expr(
385  bitvector_expr, to_vector_type(target_type), endianness_map, ns);
386  }
387  else if(target_type.id() == ID_complex)
388  {
389  return bv_to_complex_expr(
390  bitvector_expr, to_complex_type(target_type), endianness_map, ns);
391  }
392  else
393  {
395  false, "bv_to_expr does not yet support ", target_type.id_string());
396  }
397 }
398 
399 static exprt unpack_rec(
400  const exprt &src,
401  bool little_endian,
402  const optionalt<mp_integer> &offset_bytes,
403  const optionalt<mp_integer> &max_bytes,
404  const namespacet &ns,
405  bool unpack_byte_array = false);
406 
414  const exprt &src,
415  std::size_t lower_bound,
416  std::size_t upper_bound,
417  const namespacet &ns)
418 {
419  PRECONDITION(lower_bound <= upper_bound);
420 
421  if(src.id() == ID_array)
422  {
423  PRECONDITION(upper_bound <= src.operands().size());
424  return exprt::operandst{
425  src.operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
426  src.operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
427  }
428 
429  PRECONDITION(src.type().id() == ID_array || src.type().id() == ID_vector);
430  PRECONDITION(
432  to_type_with_subtype(src.type()).subtype()) &&
434  8);
435  exprt::operandst bytes;
436  bytes.reserve(upper_bound - lower_bound);
437  for(std::size_t i = lower_bound; i < upper_bound; ++i)
438  {
439  const index_exprt idx{src, from_integer(i, c_index_type())};
440  bytes.push_back(simplify_expr(idx, ns));
441  }
442  return bytes;
443 }
444 
453  const exprt &src,
454  std::size_t el_bytes,
455  bool little_endian,
456  const namespacet &ns)
457 {
458  // TODO we either need a symbol table here or make array comprehensions
459  // introduce a scope
460  static std::size_t array_comprehension_index_counter = 0;
461  ++array_comprehension_index_counter;
462  symbol_exprt array_comprehension_index{
463  "$array_comprehension_index_a_v" +
464  std::to_string(array_comprehension_index_counter),
465  c_index_type()};
466 
467  index_exprt element{src,
468  div_exprt{array_comprehension_index,
469  from_integer(el_bytes, c_index_type())}};
470 
471  exprt sub = unpack_rec(element, little_endian, {}, {}, ns, false);
472  exprt::operandst sub_operands = instantiate_byte_array(sub, 0, el_bytes, ns);
473 
474  exprt body = sub_operands.front();
475  const mod_exprt offset{
476  array_comprehension_index,
477  from_integer(el_bytes, array_comprehension_index.type())};
478  for(std::size_t i = 1; i < el_bytes; ++i)
479  {
480  body = if_exprt{
481  equal_exprt{offset, from_integer(i, array_comprehension_index.type())},
482  sub_operands[i],
483  body};
484  }
485 
486  const exprt array_vector_size = src.type().id() == ID_vector
487  ? to_vector_type(src.type()).size()
488  : to_array_type(src.type()).size();
489 
491  std::move(array_comprehension_index),
492  std::move(body),
494  mult_exprt{array_vector_size,
495  from_integer(el_bytes, array_vector_size.type())}}};
496 }
497 
512  const exprt &src,
513  const optionalt<mp_integer> &src_size,
514  const mp_integer &element_bits,
515  bool little_endian,
516  const optionalt<mp_integer> &offset_bytes,
517  const optionalt<mp_integer> &max_bytes,
518  const namespacet &ns)
519 {
520  const std::size_t el_bytes =
521  numeric_cast_v<std::size_t>((element_bits + 7) / 8);
522 
523  if(!src_size.has_value() && !max_bytes.has_value())
524  {
526  el_bytes > 0 && element_bits % 8 == 0,
527  "unpacking of arrays with non-byte-aligned elements is not supported");
529  src, el_bytes, little_endian, ns);
530  }
531 
532  exprt::operandst byte_operands;
533  mp_integer first_element = 0;
534 
535  // refine the number of elements to extract in case the element width is known
536  // and a multiple of bytes; otherwise we will expand the entire array/vector
537  optionalt<mp_integer> num_elements = src_size;
538  if(element_bits > 0 && element_bits % 8 == 0)
539  {
540  if(!num_elements.has_value())
541  {
542  // turn bytes into elements, rounding up
543  num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
544  }
545 
546  if(offset_bytes.has_value())
547  {
548  // compute offset as number of elements
549  first_element = *offset_bytes / el_bytes;
550  // insert offset_bytes-many nil bytes into the output array
551  byte_operands.resize(
552  numeric_cast_v<std::size_t>(*offset_bytes - (*offset_bytes % el_bytes)),
553  from_integer(0, bv_typet{8}));
554  }
555  }
556 
557  // the maximum number of bytes is an upper bound in case the size of the
558  // array/vector is unknown; if element_bits was usable above this will
559  // have been turned into a number of elements already
560  if(!num_elements)
561  num_elements = *max_bytes;
562 
563  const exprt src_simp = simplify_expr(src, ns);
564 
565  for(mp_integer i = first_element; i < *num_elements; ++i)
566  {
567  exprt element;
568 
569  if(
570  (src_simp.id() == ID_array || src_simp.id() == ID_vector) &&
571  i < src_simp.operands().size())
572  {
573  const std::size_t index_int = numeric_cast_v<std::size_t>(i);
574  element = src_simp.operands()[index_int];
575  }
576  else
577  {
578  element = index_exprt(src_simp, from_integer(i, c_index_type()));
579  }
580 
581  // recursively unpack each element so that we eventually just have an array
582  // of bytes left
583 
584  const optionalt<mp_integer> element_max_bytes =
585  max_bytes
586  ? std::min(mp_integer{el_bytes}, *max_bytes - byte_operands.size())
588  const std::size_t element_max_bytes_int =
589  element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
590  : el_bytes;
591 
592  exprt sub =
593  unpack_rec(element, little_endian, {}, element_max_bytes, ns, true);
594  exprt::operandst sub_operands =
595  instantiate_byte_array(sub, 0, element_max_bytes_int, ns);
596  byte_operands.insert(
597  byte_operands.end(), sub_operands.begin(), sub_operands.end());
598 
599  if(max_bytes && byte_operands.size() >= *max_bytes)
600  break;
601  }
602 
603  const std::size_t size = byte_operands.size();
604  return array_exprt(
605  std::move(byte_operands),
607 }
608 
619 static void process_bit_fields(
620  exprt::operandst &&bit_fields,
621  std::size_t total_bits,
622  exprt::operandst &dest,
623  bool little_endian,
624  const optionalt<mp_integer> &offset_bytes,
625  const optionalt<mp_integer> &max_bytes,
626  const namespacet &ns)
627 {
628  const concatenation_exprt concatenation{std::move(bit_fields),
629  bv_typet{total_bits}};
630 
631  exprt sub =
632  unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns, true);
633 
634  dest.insert(
635  dest.end(),
636  std::make_move_iterator(sub.operands().begin()),
637  std::make_move_iterator(sub.operands().end()));
638 }
639 
650  const exprt &src,
651  bool little_endian,
652  const optionalt<mp_integer> &offset_bytes,
653  const optionalt<mp_integer> &max_bytes,
654  const namespacet &ns)
655 {
656  const struct_typet &struct_type = to_struct_type(ns.follow(src.type()));
657  const struct_typet::componentst &components = struct_type.components();
658 
659  optionalt<mp_integer> offset_in_member;
660  optionalt<mp_integer> max_bytes_left;
662 
664  exprt::operandst byte_operands;
665  for(auto it = components.begin(); it != components.end(); ++it)
666  {
667  const auto &comp = *it;
668  auto component_bits = pointer_offset_bits(comp.type(), ns);
669 
670  // We can only handle a member of unknown width when it is the last member
671  // and is byte-aligned. Members of unknown width in the middle would leave
672  // us with unknown alignment of subsequent members, and queuing them up as
673  // bit fields is not possible either as the total width of the concatenation
674  // could not be determined.
676  component_bits.has_value() ||
677  (std::next(it) == components.end() && !bit_fields.has_value()),
678  "members of non-constant width should come last in a struct");
679 
680  member_exprt member(src, comp.get_name(), comp.type());
681  if(src.id() == ID_struct)
682  simplify(member, ns);
683 
684  // Is it a byte-aligned member?
685  if(member_offset_bits % 8 == 0)
686  {
687  if(bit_fields.has_value())
688  {
690  std::move(bit_fields->first),
691  bit_fields->second,
692  byte_operands,
693  little_endian,
694  offset_in_member,
695  max_bytes_left,
696  ns);
697  bit_fields.reset();
698  }
699 
700  if(offset_bytes.has_value())
701  {
702  offset_in_member = *offset_bytes - member_offset_bits / 8;
703  // if the offset is negative, offset_in_member remains unset, which has
704  // the same effect as setting it to zero
705  if(*offset_in_member < 0)
706  offset_in_member.reset();
707  }
708 
709  if(max_bytes.has_value())
710  {
711  max_bytes_left = *max_bytes - member_offset_bits / 8;
712  if(*max_bytes_left < 0)
713  break;
714  }
715  }
716 
717  if(
718  member_offset_bits % 8 != 0 ||
719  (component_bits.has_value() && *component_bits % 8 != 0))
720  {
721  if(!bit_fields.has_value())
722  bit_fields = std::make_pair(exprt::operandst{}, std::size_t{0});
723 
724  const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
725  bit_fields->first.insert(
726  little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
727  typecast_exprt::conditional_cast(member, bv_typet{bits_int}));
728  bit_fields->second += bits_int;
729 
730  member_offset_bits += *component_bits;
731 
732  continue;
733  }
734 
735  INVARIANT(
736  !bit_fields.has_value(),
737  "all preceding members should have been processed");
738 
739  exprt sub = unpack_rec(
740  member, little_endian, offset_in_member, max_bytes_left, ns, true);
741 
742  byte_operands.insert(
743  byte_operands.end(),
744  std::make_move_iterator(sub.operands().begin()),
745  std::make_move_iterator(sub.operands().end()));
746 
747  if(component_bits.has_value())
748  member_offset_bits += *component_bits;
749  }
750 
751  if(bit_fields.has_value())
753  std::move(bit_fields->first),
754  bit_fields->second,
755  byte_operands,
756  little_endian,
757  offset_in_member,
758  max_bytes_left,
759  ns);
760 
761  const std::size_t size = byte_operands.size();
762  return array_exprt{std::move(byte_operands),
764 }
765 
771 static array_exprt
772 unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
773 {
774  const complex_typet &complex_type = to_complex_type(src.type());
775  const typet &subtype = complex_type.subtype();
776 
777  auto subtype_bits = pointer_offset_bits(subtype, ns);
778  CHECK_RETURN(subtype_bits.has_value());
779  CHECK_RETURN(*subtype_bits % 8 == 0);
780 
781  exprt sub_real = unpack_rec(
782  complex_real_exprt{src},
783  little_endian,
784  mp_integer{0},
785  *subtype_bits / 8,
786  ns,
787  true);
788  exprt::operandst byte_operands = std::move(sub_real.operands());
789 
790  exprt sub_imag = unpack_rec(
791  complex_imag_exprt{src},
792  little_endian,
793  mp_integer{0},
794  *subtype_bits / 8,
795  ns,
796  true);
797  byte_operands.insert(
798  byte_operands.end(),
799  std::make_move_iterator(sub_imag.operands().begin()),
800  std::make_move_iterator(sub_imag.operands().end()));
801 
802  const std::size_t size = byte_operands.size();
803  return array_exprt{std::move(byte_operands),
805 }
806 
816 // array of bytes
819  const exprt &src,
820  bool little_endian,
821  const optionalt<mp_integer> &offset_bytes,
822  const optionalt<mp_integer> &max_bytes,
823  const namespacet &ns,
824  bool unpack_byte_array)
825 {
826  if(src.type().id()==ID_array)
827  {
828  const array_typet &array_type=to_array_type(src.type());
829  const typet &subtype = array_type.element_type();
830 
831  auto element_bits = pointer_offset_bits(subtype, ns);
832  CHECK_RETURN(element_bits.has_value());
833 
834  if(!unpack_byte_array && *element_bits == 8)
835  return src;
836 
837  const auto constant_size_opt = numeric_cast<mp_integer>(array_type.size());
838  return unpack_array_vector(
839  src,
840  constant_size_opt,
841  *element_bits,
842  little_endian,
843  offset_bytes,
844  max_bytes,
845  ns);
846  }
847  else if(src.type().id() == ID_vector)
848  {
849  const vector_typet &vector_type = to_vector_type(src.type());
850  const typet &subtype = vector_type.element_type();
851 
852  auto element_bits = pointer_offset_bits(subtype, ns);
853  CHECK_RETURN(element_bits.has_value());
854 
855  if(!unpack_byte_array && *element_bits == 8)
856  return src;
857 
858  return unpack_array_vector(
859  src,
860  numeric_cast_v<mp_integer>(vector_type.size()),
861  *element_bits,
862  little_endian,
863  offset_bytes,
864  max_bytes,
865  ns);
866  }
867  else if(src.type().id() == ID_complex)
868  {
869  return unpack_complex(src, little_endian, ns);
870  }
871  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
872  {
873  return unpack_struct(src, little_endian, offset_bytes, max_bytes, ns);
874  }
875  else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
876  {
877  const union_typet &union_type = to_union_type(ns.follow(src.type()));
878 
879  const auto widest_member = union_type.find_widest_union_component(ns);
880 
881  if(widest_member.has_value())
882  {
883  member_exprt member{
884  src, widest_member->first.get_name(), widest_member->first.type()};
885  return unpack_rec(
886  member, little_endian, offset_bytes, widest_member->second, ns, true);
887  }
888  }
889  else if(src.type().id() == ID_pointer)
890  {
891  return unpack_rec(
893  little_endian,
894  offset_bytes,
895  max_bytes,
896  ns,
897  unpack_byte_array);
898  }
899  else if(src.id() == ID_string_constant)
900  {
901  return unpack_rec(
903  little_endian,
904  offset_bytes,
905  max_bytes,
906  ns,
907  unpack_byte_array);
908  }
909  else if(src.id() == ID_constant && src.type().id() == ID_string)
910  {
911  return unpack_rec(
912  string_constantt(to_constant_expr(src).get_value()).to_array_expr(),
913  little_endian,
914  offset_bytes,
915  max_bytes,
916  ns,
917  unpack_byte_array);
918  }
919  else if(src.type().id()!=ID_empty)
920  {
921  // a basic type; we turn that into extractbits while considering
922  // endianness
923  auto bits_opt = pointer_offset_bits(src.type(), ns);
924  DATA_INVARIANT(bits_opt.has_value(), "basic type should have a fixed size");
925 
926  const mp_integer total_bits = *bits_opt;
927  mp_integer last_bit = total_bits;
928  mp_integer bit_offset = 0;
929 
930  if(max_bytes.has_value())
931  {
932  const auto max_bits = *max_bytes * 8;
933  if(little_endian)
934  {
935  last_bit = std::min(last_bit, max_bits);
936  }
937  else
938  {
939  bit_offset = std::max(mp_integer{0}, last_bit - max_bits);
940  }
941  }
942 
943  auto const src_as_bitvector = typecast_exprt::conditional_cast(
944  src, bv_typet{numeric_cast_v<std::size_t>(total_bits)});
945  auto const byte_type = bv_typet{8};
946  exprt::operandst byte_operands;
947  for(; bit_offset < last_bit; bit_offset += 8)
948  {
949  extractbits_exprt extractbits(
950  src_as_bitvector,
951  from_integer(bit_offset + 7, c_index_type()),
952  from_integer(bit_offset, c_index_type()),
953  byte_type);
954 
955  // endianness_mapt should be the point of reference for mapping out
956  // endianness, but we need to work on elements here instead of
957  // individual bits
958  if(little_endian)
959  byte_operands.push_back(extractbits);
960  else
961  byte_operands.insert(byte_operands.begin(), extractbits);
962  }
963 
964  const std::size_t size = byte_operands.size();
965  return array_exprt(
966  std::move(byte_operands),
968  }
969 
970  return array_exprt(
971  {}, array_typet{bv_typet{8}, from_integer(0, size_type())});
972 }
973 
985  const byte_extract_exprt &src,
986  const byte_extract_exprt &unpacked,
987  const typet &subtype,
988  const mp_integer &element_bits,
989  const namespacet &ns)
990 {
991  optionalt<std::size_t> num_elements;
992  if(src.type().id() == ID_array)
993  num_elements = numeric_cast<std::size_t>(to_array_type(src.type()).size());
994  else
995  num_elements = numeric_cast<std::size_t>(to_vector_type(src.type()).size());
996 
997  if(num_elements.has_value())
998  {
999  exprt::operandst operands;
1000  operands.reserve(*num_elements);
1001  for(std::size_t i = 0; i < *num_elements; ++i)
1002  {
1003  plus_exprt new_offset(
1004  unpacked.offset(),
1005  from_integer(i * element_bits / 8, unpacked.offset().type()));
1006 
1007  byte_extract_exprt tmp(unpacked);
1008  tmp.type() = subtype;
1009  tmp.offset() = new_offset;
1010 
1011  operands.push_back(lower_byte_extract(tmp, ns));
1012  }
1013 
1014  exprt result;
1015  if(src.type().id() == ID_array)
1016  result = array_exprt{std::move(operands), to_array_type(src.type())};
1017  else
1018  result = vector_exprt{std::move(operands), to_vector_type(src.type())};
1019 
1020  return simplify_expr(result, ns);
1021  }
1022 
1023  DATA_INVARIANT(src.type().id() == ID_array, "vectors have constant size");
1024  const array_typet &array_type = to_array_type(src.type());
1025 
1026  // TODO we either need a symbol table here or make array comprehensions
1027  // introduce a scope
1028  static std::size_t array_comprehension_index_counter = 0;
1029  ++array_comprehension_index_counter;
1030  symbol_exprt array_comprehension_index{
1031  "$array_comprehension_index_a" +
1032  std::to_string(array_comprehension_index_counter),
1033  c_index_type()};
1034 
1035  plus_exprt new_offset{
1036  unpacked.offset(),
1038  mult_exprt{
1039  array_comprehension_index,
1040  from_integer(element_bits / 8, array_comprehension_index.type())},
1041  unpacked.offset().type())};
1042 
1043  byte_extract_exprt body(unpacked);
1044  body.type() = subtype;
1045  body.offset() = std::move(new_offset);
1046 
1047  return array_comprehension_exprt{std::move(array_comprehension_index),
1048  lower_byte_extract(body, ns),
1049  array_type};
1050 }
1051 
1061  const byte_extract_exprt &src,
1062  const byte_extract_exprt &unpacked,
1063  const namespacet &ns)
1064 {
1065  const complex_typet &complex_type = to_complex_type(src.type());
1066  const typet &subtype = complex_type.subtype();
1067 
1068  auto subtype_bits = pointer_offset_bits(subtype, ns);
1069  if(!subtype_bits.has_value() || *subtype_bits % 8 != 0)
1070  return {};
1071 
1072  // offset remains unchanged
1073  byte_extract_exprt real{unpacked};
1074  real.type() = subtype;
1075 
1076  const plus_exprt new_offset{
1077  unpacked.offset(),
1078  from_integer(*subtype_bits / 8, unpacked.offset().type())};
1079  byte_extract_exprt imag{unpacked};
1080  imag.type() = subtype;
1081  imag.offset() = simplify_expr(new_offset, ns);
1082 
1083  return simplify_expr(
1084  complex_exprt{
1085  lower_byte_extract(real, ns), lower_byte_extract(imag, ns), complex_type},
1086  ns);
1087 }
1088 
1092 {
1093  // General notes about endianness and the bit-vector conversion:
1094  // A single byte with value 0b10001000 is stored (in irept) as
1095  // exactly this string literal, and its bit-vector encoding will be
1096  // bvt bv={0,0,0,1,0,0,0,1}, i.e., bv[0]==0 and bv[7]==1
1097  //
1098  // A multi-byte value like x=256 would be:
1099  // - little-endian storage: ((char*)&x)[0]==0, ((char*)&x)[1]==1
1100  // - big-endian storage: ((char*)&x)[0]==1, ((char*)&x)[1]==0
1101  // - irept representation: 0000000100000000
1102  // - bvt: {0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0}
1103  // <... 8bits ...> <... 8bits ...>
1104  //
1105  // An array {0, 1} will be encoded as bvt bv={0,1}, i.e., bv[1]==1
1106  // concatenation(0, 1) will yield a bvt bv={1,0}, i.e., bv[1]==0
1107  //
1108  // The semantics of byte_extract(endianness, op, offset, T) is:
1109  // interpret ((char*)&op)+offset as the endianness-ordered storage
1110  // of an object of type T at address ((char*)&op)+offset
1111  // For some T x, byte_extract(endianness, x, 0, T) must yield x.
1112  //
1113  // byte_extract for a composite type T or an array will interpret
1114  // the individual subtypes with suitable endianness; the overall
1115  // order of components is not affected by endianness.
1116  //
1117  // Examples:
1118  // unsigned char A[4];
1119  // byte_extract_little_endian(A, 0, unsigned short) requests that
1120  // A[0],A[1] be interpreted as the storage of an unsigned short with
1121  // A[1] being the most-significant byte; byte_extract_big_endian for
1122  // the same operands will select A[0] as the most-significant byte.
1123  //
1124  // int A[2] = {0x01020304,0xDEADBEEF}
1125  // byte_extract_big_endian(A, 0, short) should yield 0x0102
1126  // byte_extract_little_endian(A, 0, short) should yield 0x0304
1127  // To obtain this we first compute byte arrays while taking into
1128  // account endianness:
1129  // big-endian byte representation: {01,02,03,04,DE,AB,BE,EF}
1130  // little-endian byte representation: {04,03,02,01,EF,BE,AB,DE}
1131  // We extract the relevant bytes starting from ((char*)A)+0:
1132  // big-endian: {01,02}; little-endian: {04,03}
1133  // Finally we place them in the appropriate byte order as indicated
1134  // by endianness:
1135  // big-endian: (short)concatenation(01,02)=0x0102
1136  // little-endian: (short)concatenation(03,04)=0x0304
1137 
1138  PRECONDITION(
1139  src.id() == ID_byte_extract_little_endian ||
1140  src.id() == ID_byte_extract_big_endian);
1141  const bool little_endian = src.id() == ID_byte_extract_little_endian;
1142 
1143  // determine an upper bound of the last byte we might need
1144  auto upper_bound_opt = size_of_expr(src.type(), ns);
1145  if(upper_bound_opt.has_value())
1146  {
1147  upper_bound_opt = simplify_expr(
1148  plus_exprt(
1149  upper_bound_opt.value(),
1151  src.offset(), upper_bound_opt.value().type())),
1152  ns);
1153  }
1154  else if(src.type().id() == ID_empty)
1155  upper_bound_opt = from_integer(0, size_type());
1156 
1157  const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.offset());
1158  const auto upper_bound_int_opt =
1159  numeric_cast<mp_integer>(upper_bound_opt.value_or(nil_exprt()));
1160 
1161  byte_extract_exprt unpacked(src);
1162  unpacked.op() = unpack_rec(
1163  src.op(), little_endian, lower_bound_int_opt, upper_bound_int_opt, ns);
1164  CHECK_RETURN(
1166  .get_width() == 8);
1167 
1168  if(src.type().id() == ID_array || src.type().id() == ID_vector)
1169  {
1170  const typet &subtype = to_type_with_subtype(src.type()).subtype();
1171 
1172  // consider ways of dealing with arrays of unknown subtype size or with a
1173  // subtype size that does not fit byte boundaries; currently we fall back to
1174  // stitching together consecutive elements down below
1175  auto element_bits = pointer_offset_bits(subtype, ns);
1176  if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1177  {
1179  src, unpacked, subtype, *element_bits, ns);
1180  }
1181  }
1182  else if(src.type().id() == ID_complex)
1183  {
1184  auto result = lower_byte_extract_complex(src, unpacked, ns);
1185  if(result.has_value())
1186  return std::move(*result);
1187 
1188  // else fall back to generic lowering that uses bit masks, below
1189  }
1190  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
1191  {
1192  const struct_typet &struct_type=to_struct_type(ns.follow(src.type()));
1193  const struct_typet::componentst &components=struct_type.components();
1194 
1195  bool failed=false;
1196  struct_exprt s({}, src.type());
1197 
1198  for(const auto &comp : components)
1199  {
1200  auto component_bits = pointer_offset_bits(comp.type(), ns);
1201 
1202  // the next member would be misaligned, abort
1203  if(
1204  !component_bits.has_value() || *component_bits == 0 ||
1205  *component_bits % 8 != 0)
1206  {
1207  failed=true;
1208  break;
1209  }
1210 
1211  auto member_offset_opt =
1212  member_offset_expr(struct_type, comp.get_name(), ns);
1213 
1214  if(!member_offset_opt.has_value())
1215  {
1216  failed = true;
1217  break;
1218  }
1219 
1220  plus_exprt new_offset(
1221  unpacked.offset(),
1223  member_offset_opt.value(), unpacked.offset().type()));
1224 
1225  byte_extract_exprt tmp(unpacked);
1226  tmp.type()=comp.type();
1227  tmp.offset()=new_offset;
1228 
1229  s.add_to_operands(lower_byte_extract(tmp, ns));
1230  }
1231 
1232  if(!failed)
1233  return simplify_expr(std::move(s), ns);
1234  }
1235  else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
1236  {
1237  const union_typet &union_type = to_union_type(ns.follow(src.type()));
1238 
1239  const auto widest_member = union_type.find_widest_union_component(ns);
1240 
1241  if(widest_member.has_value())
1242  {
1243  byte_extract_exprt tmp(unpacked);
1244  tmp.type() = widest_member->first.type();
1245 
1246  return union_exprt(
1247  widest_member->first.get_name(),
1248  lower_byte_extract(tmp, ns),
1249  src.type());
1250  }
1251  }
1252 
1253  const exprt &root=unpacked.op();
1254  const exprt &offset=unpacked.offset();
1255 
1256  optionalt<typet> subtype;
1257  if(root.type().id() == ID_vector)
1258  subtype = to_vector_type(root.type()).element_type();
1259  else
1260  subtype = to_array_type(root.type()).element_type();
1261 
1262  auto subtype_bits = pointer_offset_bits(*subtype, ns);
1263 
1265  subtype_bits.has_value() && *subtype_bits == 8,
1266  "offset bits are byte aligned");
1267 
1268  auto size_bits = pointer_offset_bits(unpacked.type(), ns);
1269  if(!size_bits.has_value())
1270  {
1271  auto op0_bits = pointer_offset_bits(unpacked.op().type(), ns);
1272  // all cases with non-constant width should have been handled above
1274  op0_bits.has_value(),
1275  "the extracted width or the source width must be known");
1276  size_bits = op0_bits;
1277  }
1278 
1279  mp_integer num_bytes = (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
1280 
1281  // get 'width'-many bytes, and concatenate
1282  const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
1283  exprt::operandst op;
1284  op.reserve(width_bytes);
1285 
1286  for(std::size_t i=0; i<width_bytes; i++)
1287  {
1288  // the most significant byte comes first in the concatenation!
1289  std::size_t offset_int=
1290  little_endian?(width_bytes-i-1):i;
1291 
1292  plus_exprt offset_i(from_integer(offset_int, offset.type()), offset);
1293  simplify(offset_i, ns);
1294 
1295  mp_integer index = 0;
1296  if(
1297  offset_i.is_constant() &&
1298  (root.id() == ID_array || root.id() == ID_vector) &&
1299  !to_integer(to_constant_expr(offset_i), index) &&
1300  index < root.operands().size() && index >= 0)
1301  {
1302  // offset is constant and in range
1303  op.push_back(root.operands()[numeric_cast_v<std::size_t>(index)]);
1304  }
1305  else
1306  {
1307  op.push_back(index_exprt(root, offset_i));
1308  }
1309  }
1310 
1311  if(width_bytes==1)
1312  {
1313  return simplify_expr(
1314  typecast_exprt::conditional_cast(op.front(), src.type()), ns);
1315  }
1316  else // width_bytes>=2
1317  {
1318  concatenation_exprt concatenation(
1319  std::move(op), adjust_width(*subtype, width_bytes * 8));
1320 
1321  endianness_mapt map(concatenation.type(), little_endian, ns);
1322  return bv_to_expr(concatenation, src.type(), map, ns);
1323  }
1324 }
1325 
1326 static exprt lower_byte_update(
1327  const byte_update_exprt &src,
1328  const exprt &value_as_byte_array,
1329  const optionalt<exprt> &non_const_update_bound,
1330  const namespacet &ns);
1331 
1342  const byte_update_exprt &src,
1343  const typet &subtype,
1344  const exprt &value_as_byte_array,
1345  const exprt &non_const_update_bound,
1346  const namespacet &ns)
1347 {
1348  // TODO we either need a symbol table here or make array comprehensions
1349  // introduce a scope
1350  static std::size_t array_comprehension_index_counter = 0;
1351  ++array_comprehension_index_counter;
1352  symbol_exprt array_comprehension_index{
1353  "$array_comprehension_index_u_a_v" +
1354  std::to_string(array_comprehension_index_counter),
1355  c_index_type()};
1356 
1357  binary_predicate_exprt lower_bound{
1359  array_comprehension_index, src.offset().type()),
1360  ID_lt,
1361  src.offset()};
1362  binary_predicate_exprt upper_bound{
1364  array_comprehension_index, non_const_update_bound.type()),
1365  ID_ge,
1367  src.offset(), non_const_update_bound.type()),
1368  non_const_update_bound}};
1369 
1370  if_exprt array_comprehension_body{
1371  or_exprt{std::move(lower_bound), std::move(upper_bound)},
1372  index_exprt{src.op(), array_comprehension_index},
1374  index_exprt{
1375  value_as_byte_array,
1376  minus_exprt{array_comprehension_index,
1378  src.offset(), array_comprehension_index.type())}},
1379  subtype)};
1380 
1381  return simplify_expr(
1382  array_comprehension_exprt{array_comprehension_index,
1383  std::move(array_comprehension_body),
1384  to_array_type(src.type())},
1385  ns);
1386 }
1387 
1398  const byte_update_exprt &src,
1399  const typet &subtype,
1400  const array_exprt &value_as_byte_array,
1401  const optionalt<exprt> &non_const_update_bound,
1402  const namespacet &ns)
1403 {
1404  // apply 'array-update-with' num_elements times
1405  exprt result = src.op();
1406 
1407  for(std::size_t i = 0; i < value_as_byte_array.operands().size(); ++i)
1408  {
1409  const exprt &element = value_as_byte_array.operands()[i];
1410 
1411  const exprt where = simplify_expr(
1412  plus_exprt{src.offset(), from_integer(i, src.offset().type())}, ns);
1413 
1414  // skip elements that wouldn't change (skip over typecasts as we might have
1415  // some signed/unsigned char conversions)
1416  const exprt &e = skip_typecast(element);
1417  if(e.id() == ID_index)
1418  {
1419  const index_exprt &index_expr = to_index_expr(e);
1420  if(index_expr.array() == src.op() && index_expr.index() == where)
1421  continue;
1422  }
1423 
1424  exprt update_value;
1425  if(non_const_update_bound.has_value())
1426  {
1427  update_value = typecast_exprt::conditional_cast(
1429  from_integer(i, non_const_update_bound->type()),
1430  ID_lt,
1431  *non_const_update_bound},
1432  element,
1433  index_exprt{src.op(), where}},
1434  subtype);
1435  }
1436  else
1437  update_value = typecast_exprt::conditional_cast(element, subtype);
1438 
1439  if(result.id() != ID_with)
1440  result = with_exprt{result, where, update_value};
1441  else
1442  result.add_to_operands(where, update_value);
1443  }
1444 
1445  return simplify_expr(std::move(result), ns);
1446 }
1447 
1464  const byte_update_exprt &src,
1465  const typet &subtype,
1466  const exprt &subtype_size,
1467  const exprt &value_as_byte_array,
1468  const exprt &non_const_update_bound,
1469  const exprt &initial_bytes,
1470  const exprt &first_index,
1471  const exprt &first_update_value,
1472  const namespacet &ns)
1473 {
1474  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1475  ? ID_byte_extract_little_endian
1476  : ID_byte_extract_big_endian;
1477 
1478  // TODO we either need a symbol table here or make array comprehensions
1479  // introduce a scope
1480  static std::size_t array_comprehension_index_counter = 0;
1481  ++array_comprehension_index_counter;
1482  symbol_exprt array_comprehension_index{
1483  "$array_comprehension_index_u_a_v_u" +
1484  std::to_string(array_comprehension_index_counter),
1485  c_index_type()};
1486 
1487  // all arithmetic uses offset/index types
1488  PRECONDITION(subtype_size.type() == src.offset().type());
1489  PRECONDITION(initial_bytes.type() == src.offset().type());
1490  PRECONDITION(first_index.type() == src.offset().type());
1491 
1492  // the bound from where updates start
1493  binary_predicate_exprt lower_bound{
1495  array_comprehension_index, first_index.type()),
1496  ID_lt,
1497  first_index};
1498 
1499  // The actual value of updates other than at the start or end
1500  plus_exprt offset_expr{
1501  initial_bytes,
1502  mult_exprt{subtype_size,
1504  array_comprehension_index, first_index.type()),
1505  plus_exprt{first_index,
1506  from_integer(1, first_index.type())}}}};
1507  exprt update_value = lower_byte_extract(
1509  extract_opcode, value_as_byte_array, std::move(offset_expr), subtype},
1510  ns);
1511 
1512  // The number of target array/vector elements being replaced, not including
1513  // a possible partial update at the end of the updated range, which is handled
1514  // below: (non_const_update_bound + (subtype_size - 1)) / subtype_size to
1515  // round up to the nearest multiple of subtype_size.
1516  div_exprt updated_elements{
1518  non_const_update_bound, subtype_size.type()),
1519  minus_exprt{subtype_size, from_integer(1, subtype_size.type())}},
1520  subtype_size};
1521 
1522  // The last element to be updated: first_index + updated_elements - 1
1523  plus_exprt last_index{first_index,
1524  minus_exprt{std::move(updated_elements),
1525  from_integer(1, first_index.type())}};
1526 
1527  // The size of a partial update at the end of the updated range, may be zero.
1528  mod_exprt tail_size{
1530  non_const_update_bound, initial_bytes.type()),
1531  initial_bytes},
1532  subtype_size};
1533 
1534  // The bound where updates end, which is conditional on the partial update
1535  // being empty.
1536  binary_predicate_exprt upper_bound{
1538  array_comprehension_index, last_index.type()),
1539  ID_ge,
1540  if_exprt{equal_exprt{tail_size, from_integer(0, tail_size.type())},
1541  last_index,
1542  plus_exprt{last_index, from_integer(1, last_index.type())}}};
1543 
1544  // The actual value of a partial update at the end.
1545  exprt last_update_value = lower_byte_operators(
1547  src.id(),
1548  index_exprt{src.op(), last_index},
1549  from_integer(0, src.offset().type()),
1550  byte_extract_exprt{extract_opcode,
1551  value_as_byte_array,
1553  last_index, subtype_size.type()),
1554  subtype_size},
1555  array_typet{bv_typet{8}, tail_size}}},
1556  ns);
1557 
1558  if_exprt array_comprehension_body{
1559  or_exprt{std::move(lower_bound), std::move(upper_bound)},
1560  index_exprt{src.op(), array_comprehension_index},
1561  if_exprt{
1563  array_comprehension_index, first_index.type()),
1564  first_index},
1565  first_update_value,
1567  array_comprehension_index, last_index.type()),
1568  last_index},
1569  std::move(last_update_value),
1570  std::move(update_value)}}};
1571 
1572  return simplify_expr(
1573  array_comprehension_exprt{array_comprehension_index,
1574  std::move(array_comprehension_body),
1575  to_array_type(src.type())},
1576  ns);
1577 }
1578 
1590  const byte_update_exprt &src,
1591  const typet &subtype,
1592  const exprt &value_as_byte_array,
1593  const optionalt<exprt> &non_const_update_bound,
1594  const namespacet &ns)
1595 {
1596  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1597  ? ID_byte_extract_little_endian
1598  : ID_byte_extract_big_endian;
1599 
1600  // do all arithmetic below using index/offset types - the array theory
1601  // back-end is really picky about indices having the same type
1602  auto subtype_size_opt = size_of_expr(subtype, ns);
1603  CHECK_RETURN(subtype_size_opt.has_value());
1604 
1605  const exprt subtype_size = simplify_expr(
1607  subtype_size_opt.value(), src.offset().type()),
1608  ns);
1609 
1610  // compute the index of the first element of the array/vector that may be
1611  // updated
1612  exprt first_index = div_exprt{src.offset(), subtype_size};
1613  simplify(first_index, ns);
1614 
1615  // compute the offset within that first element
1616  const exprt update_offset = mod_exprt{src.offset(), subtype_size};
1617 
1618  // compute the number of bytes (from the update value) that are going to be
1619  // consumed for updating the first element
1620  exprt initial_bytes = minus_exprt{subtype_size, update_offset};
1621  exprt update_bound;
1622  if(non_const_update_bound.has_value())
1623  {
1624  update_bound = typecast_exprt::conditional_cast(
1625  *non_const_update_bound, subtype_size.type());
1626  }
1627  else
1628  {
1630  value_as_byte_array.id() == ID_array,
1631  "value should be an array expression if the update bound is constant");
1632  update_bound =
1633  from_integer(value_as_byte_array.operands().size(), initial_bytes.type());
1634  }
1635  initial_bytes =
1636  if_exprt{binary_predicate_exprt{initial_bytes, ID_lt, update_bound},
1637  initial_bytes,
1638  update_bound};
1639  simplify(initial_bytes, ns);
1640 
1641  // encode the first update: update the original element at first_index with
1642  // initial_bytes-many bytes extracted from value_as_byte_array
1643  exprt first_update_value = lower_byte_operators(
1645  src.id(),
1646  index_exprt{src.op(), first_index},
1647  update_offset,
1648  byte_extract_exprt{extract_opcode,
1649  value_as_byte_array,
1650  from_integer(0, src.offset().type()),
1651  array_typet{bv_typet{8}, initial_bytes}}},
1652  ns);
1653 
1654  if(value_as_byte_array.id() != ID_array)
1655  {
1657  src,
1658  subtype,
1659  subtype_size,
1660  value_as_byte_array,
1661  *non_const_update_bound,
1662  initial_bytes,
1663  first_index,
1664  first_update_value,
1665  ns);
1666  }
1667 
1668  // We will update one array/vector element at a time - compute the number of
1669  // update values that will be consumed in each step. If we cannot determine a
1670  // constant value at this time we assume it's at least one byte. The
1671  // byte_extract_exprt within the loop uses the symbolic value (subtype_size),
1672  // we just need to make sure we make progress for the loop to terminate.
1673  std::size_t step_size = 1;
1674  if(subtype_size.is_constant())
1675  step_size = numeric_cast_v<std::size_t>(to_constant_expr(subtype_size));
1676  // Given the first update already encoded, keep track of the offset into the
1677  // update value. Again, the expressions within the loop use the symbolic
1678  // value, this is just an optimization in case we can determine a constant
1679  // offset.
1680  std::size_t offset = 0;
1681  if(initial_bytes.is_constant())
1682  offset = numeric_cast_v<std::size_t>(to_constant_expr(initial_bytes));
1683 
1684  with_exprt result{src.op(), first_index, first_update_value};
1685 
1686  std::size_t i = 1;
1687  for(; offset + step_size <= value_as_byte_array.operands().size();
1688  offset += step_size, ++i)
1689  {
1690  exprt where = simplify_expr(
1691  plus_exprt{first_index, from_integer(i, first_index.type())}, ns);
1692 
1693  exprt offset_expr = simplify_expr(
1694  plus_exprt{
1695  initial_bytes,
1696  mult_exprt{subtype_size, from_integer(i - 1, subtype_size.type())}},
1697  ns);
1698 
1699  exprt element = lower_byte_operators(
1701  src.id(),
1702  index_exprt{src.op(), where},
1703  from_integer(0, src.offset().type()),
1704  byte_extract_exprt{extract_opcode,
1705  value_as_byte_array,
1706  std::move(offset_expr),
1707  array_typet{bv_typet{8}, subtype_size}}},
1708  ns);
1709 
1710  result.add_to_operands(std::move(where), std::move(element));
1711  }
1712 
1713  // do the tail
1714  if(offset < value_as_byte_array.operands().size())
1715  {
1716  const std::size_t tail_size =
1717  value_as_byte_array.operands().size() - offset;
1718 
1719  exprt where = simplify_expr(
1720  plus_exprt{first_index, from_integer(i, first_index.type())}, ns);
1721 
1722  exprt element = lower_byte_operators(
1724  src.id(),
1725  index_exprt{src.op(), where},
1726  from_integer(0, src.offset().type()),
1728  extract_opcode,
1729  value_as_byte_array,
1730  from_integer(offset, src.offset().type()),
1731  array_typet{bv_typet{8}, from_integer(tail_size, size_type())}}},
1732  ns);
1733 
1734  result.add_to_operands(std::move(where), std::move(element));
1735  }
1736 
1737  return simplify_expr(std::move(result), ns);
1738 }
1739 
1750  const byte_update_exprt &src,
1751  const typet &subtype,
1752  const exprt &value_as_byte_array,
1753  const optionalt<exprt> &non_const_update_bound,
1754  const namespacet &ns)
1755 {
1756  const bool is_array = src.type().id() == ID_array;
1757  exprt size;
1758  if(is_array)
1759  size = to_array_type(src.type()).size();
1760  else
1761  size = to_vector_type(src.type()).size();
1762 
1763  auto subtype_bits = pointer_offset_bits(subtype, ns);
1764 
1765  // fall back to bytewise updates in all non-constant or dubious cases
1766  if(
1767  !size.is_constant() || !src.offset().is_constant() ||
1768  !subtype_bits.has_value() || *subtype_bits == 0 || *subtype_bits % 8 != 0 ||
1769  non_const_update_bound.has_value() || value_as_byte_array.id() != ID_array)
1770  {
1772  src, subtype, value_as_byte_array, non_const_update_bound, ns);
1773  }
1774 
1775  std::size_t num_elements =
1776  numeric_cast_v<std::size_t>(to_constant_expr(size));
1777  mp_integer offset_bytes =
1778  numeric_cast_v<mp_integer>(to_constant_expr(src.offset()));
1779 
1780  exprt::operandst elements;
1781  elements.reserve(num_elements);
1782 
1783  std::size_t i = 0;
1784  // copy the prefix not affected by the update
1785  for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bytes * 8; ++i)
1786  elements.push_back(index_exprt{src.op(), from_integer(i, c_index_type())});
1787 
1788  // the modified elements
1789  for(; i < num_elements &&
1790  i * *subtype_bits <
1791  (offset_bytes + value_as_byte_array.operands().size()) * 8;
1792  ++i)
1793  {
1794  mp_integer update_offset = offset_bytes - i * (*subtype_bits / 8);
1795  mp_integer update_elements = *subtype_bits / 8;
1796  exprt::operandst::const_iterator first =
1797  value_as_byte_array.operands().begin();
1798  exprt::operandst::const_iterator end = value_as_byte_array.operands().end();
1799  if(update_offset < 0)
1800  {
1801  INVARIANT(
1802  value_as_byte_array.operands().size() > -update_offset,
1803  "indices past the update should be handled above");
1804  first += numeric_cast_v<std::ptrdiff_t>(-update_offset);
1805  }
1806  else
1807  {
1808  update_elements -= update_offset;
1809  INVARIANT(
1810  update_elements > 0,
1811  "indices before the update should be handled above");
1812  }
1813 
1814  if(std::distance(first, end) > update_elements)
1815  end = first + numeric_cast_v<std::ptrdiff_t>(update_elements);
1816  exprt::operandst update_values{first, end};
1817  const std::size_t update_size = update_values.size();
1818 
1819  const byte_update_exprt bu{
1820  src.id(),
1821  index_exprt{src.op(), from_integer(i, c_index_type())},
1822  from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
1823  array_exprt{
1824  std::move(update_values),
1825  array_typet{bv_typet{8}, from_integer(update_size, size_type())}}};
1826  elements.push_back(lower_byte_operators(bu, ns));
1827  }
1828 
1829  // copy the tail not affected by the update
1830  for(; i < num_elements; ++i)
1831  elements.push_back(index_exprt{src.op(), from_integer(i, c_index_type())});
1832 
1833  if(is_array)
1834  return simplify_expr(
1835  array_exprt{std::move(elements), to_array_type(src.type())}, ns);
1836  else
1837  return simplify_expr(
1838  vector_exprt{std::move(elements), to_vector_type(src.type())}, ns);
1839 }
1840 
1851  const byte_update_exprt &src,
1852  const struct_typet &struct_type,
1853  const exprt &value_as_byte_array,
1854  const optionalt<exprt> &non_const_update_bound,
1855  const namespacet &ns)
1856 {
1857  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1858  ? ID_byte_extract_little_endian
1859  : ID_byte_extract_big_endian;
1860 
1861  exprt::operandst elements;
1862  elements.reserve(struct_type.components().size());
1863 
1865  for(const auto &comp : struct_type.components())
1866  {
1867  auto element_width = pointer_offset_bits(comp.type(), ns);
1868 
1869  exprt member = member_exprt{src.op(), comp.get_name(), comp.type()};
1870 
1871  // compute the update offset relative to this struct member - will be
1872  // negative if we are already in the middle of the update or beyond it
1873  exprt offset = simplify_expr(
1874  minus_exprt{src.offset(),
1875  from_integer(member_offset_bits / 8, src.offset().type())},
1876  ns);
1877  auto offset_bytes = numeric_cast<mp_integer>(offset);
1878  // we don't need to update anything when
1879  // 1) the update offset is greater than the end of this member (thus the
1880  // relative offset is greater than this element) or
1881  // 2) the update offset plus the size of the update is less than the member
1882  // offset
1883  if(
1884  offset_bytes.has_value() &&
1885  (*offset_bytes * 8 >= *element_width ||
1886  (value_as_byte_array.id() == ID_array && *offset_bytes < 0 &&
1887  -*offset_bytes >= value_as_byte_array.operands().size())))
1888  {
1889  elements.push_back(std::move(member));
1890  member_offset_bits += *element_width;
1891  continue;
1892  }
1893  else if(!offset_bytes.has_value())
1894  {
1895  // The offset to update is not constant; abort the attempt to update
1896  // indiviual struct members and instead turn the operand-to-be-updated
1897  // into a byte array, which we know how to update even if the offset is
1898  // non-constant.
1899  auto src_size_opt = size_of_expr(src.type(), ns);
1900  CHECK_RETURN(src_size_opt.has_value());
1901 
1902  const byte_extract_exprt byte_extract_expr{
1903  extract_opcode,
1904  src.op(),
1905  from_integer(0, src.offset().type()),
1906  array_typet{bv_typet{8}, src_size_opt.value()}};
1907 
1908  byte_update_exprt bu = src;
1909  bu.set_op(lower_byte_extract(byte_extract_expr, ns));
1910  bu.type() = bu.op().type();
1911 
1912  return lower_byte_extract(
1914  extract_opcode,
1916  bu, value_as_byte_array, non_const_update_bound, ns),
1917  from_integer(0, src.offset().type()),
1918  src.type()},
1919  ns);
1920  }
1921 
1922  // We now need to figure out how many bytes to consume from the update
1923  // value. If the size of the update is unknown, then we need to leave some
1924  // of this work to a back-end solver via the non_const_update_bound branch
1925  // below.
1926  mp_integer update_elements = (*element_width + 7) / 8;
1927  std::size_t first = 0;
1928  if(*offset_bytes < 0)
1929  {
1930  offset = from_integer(0, src.offset().type());
1931  INVARIANT(
1932  value_as_byte_array.id() != ID_array ||
1933  value_as_byte_array.operands().size() > -*offset_bytes,
1934  "members past the update should be handled above");
1935  first = numeric_cast_v<std::size_t>(-*offset_bytes);
1936  }
1937  else
1938  {
1939  update_elements -= *offset_bytes;
1940  INVARIANT(
1941  update_elements > 0,
1942  "members before the update should be handled above");
1943  }
1944 
1945  // Now that we have an idea on how many bytes we need from the update value,
1946  // determine the exact range [first, end) in the update value, and create
1947  // that sequence of bytes (via instantiate_byte_array).
1948  std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1949  if(value_as_byte_array.id() == ID_array)
1950  end = std::min(end, value_as_byte_array.operands().size());
1951  exprt::operandst update_values =
1952  instantiate_byte_array(value_as_byte_array, first, end, ns);
1953  const std::size_t update_size = update_values.size();
1954 
1955  // With an upper bound on the size of the update established, construct the
1956  // actual update expression. If the exact size of the update is unknown,
1957  // make the size expression conditional.
1958  exprt update_size_expr = from_integer(update_size, size_type());
1959  array_exprt update_expr{std::move(update_values),
1960  array_typet{bv_typet{8}, update_size_expr}};
1961  optionalt<exprt> member_update_bound;
1962  if(non_const_update_bound.has_value())
1963  {
1964  // The size of the update is not constant, and thus is to be symbolically
1965  // bound; first see how many bytes we have left in the update:
1966  // non_const_update_bound > first ? non_const_update_bound - first: 0
1967  const exprt remaining_update_bytes = typecast_exprt::conditional_cast(
1968  if_exprt{
1970  *non_const_update_bound,
1971  ID_gt,
1972  from_integer(first, non_const_update_bound->type())},
1973  minus_exprt{*non_const_update_bound,
1974  from_integer(first, non_const_update_bound->type())},
1975  from_integer(0, non_const_update_bound->type())},
1976  size_type());
1977  // Now take the minimum of update-bytes-left and the previously computed
1978  // size of the member to be updated:
1979  update_size_expr = if_exprt{
1980  binary_predicate_exprt{update_size_expr, ID_lt, remaining_update_bytes},
1981  update_size_expr,
1982  remaining_update_bytes};
1983  simplify(update_size_expr, ns);
1984  member_update_bound = std::move(update_size_expr);
1985  }
1986 
1987  // We have established the bytes to use for the update, but now need to
1988  // account for sub-byte members.
1989  const std::size_t shift =
1990  numeric_cast_v<std::size_t>(member_offset_bits % 8);
1991  const std::size_t element_bits_int =
1992  numeric_cast_v<std::size_t>(*element_width);
1993 
1994  const bool little_endian = src.id() == ID_byte_update_little_endian;
1995  if(shift != 0)
1996  {
1997  member = concatenation_exprt{
1998  typecast_exprt::conditional_cast(member, bv_typet{element_bits_int}),
1999  from_integer(0, bv_typet{shift}),
2000  bv_typet{shift + element_bits_int}};
2001 
2002  if(!little_endian)
2003  to_concatenation_expr(member).op0().swap(
2004  to_concatenation_expr(member).op1());
2005  }
2006 
2007  // Finally construct the updated member.
2008  byte_update_exprt bu{src.id(), std::move(member), offset, update_expr};
2009  exprt updated_element =
2010  lower_byte_update(bu, update_expr, member_update_bound, ns);
2011 
2012  if(shift == 0)
2013  elements.push_back(updated_element);
2014  else
2015  {
2016  elements.push_back(typecast_exprt::conditional_cast(
2017  extractbits_exprt{updated_element,
2018  element_bits_int - 1 + (little_endian ? shift : 0),
2019  (little_endian ? shift : 0),
2020  bv_typet{element_bits_int}},
2021  comp.type()));
2022  }
2023 
2024  member_offset_bits += *element_width;
2025  }
2026 
2027  return simplify_expr(struct_exprt{std::move(elements), struct_type}, ns);
2028 }
2029 
2040  const byte_update_exprt &src,
2041  const union_typet &union_type,
2042  const exprt &value_as_byte_array,
2043  const optionalt<exprt> &non_const_update_bound,
2044  const namespacet &ns)
2045 {
2046  const auto widest_member = union_type.find_widest_union_component(ns);
2047 
2049  widest_member.has_value(),
2050  "lower_byte_update of union of unknown size is not supported");
2051 
2052  byte_update_exprt bu = src;
2053  bu.set_op(member_exprt{
2054  src.op(), widest_member->first.get_name(), widest_member->first.type()});
2055  bu.type() = widest_member->first.type();
2056 
2057  return union_exprt{
2058  widest_member->first.get_name(),
2059  lower_byte_update(bu, value_as_byte_array, non_const_update_bound, ns),
2060  src.type()};
2061 }
2062 
2072  const byte_update_exprt &src,
2073  const exprt &value_as_byte_array,
2074  const optionalt<exprt> &non_const_update_bound,
2075  const namespacet &ns)
2076 {
2077  if(src.type().id() == ID_array || src.type().id() == ID_vector)
2078  {
2079  optionalt<typet> subtype;
2080  if(src.type().id() == ID_vector)
2081  subtype = to_vector_type(src.type()).element_type();
2082  else
2083  subtype = to_array_type(src.type()).element_type();
2084 
2085  auto element_width = pointer_offset_bits(*subtype, ns);
2086  CHECK_RETURN(element_width.has_value());
2087  CHECK_RETURN(*element_width > 0);
2088  CHECK_RETURN(*element_width % 8 == 0);
2089 
2090  if(*element_width == 8)
2091  {
2092  if(value_as_byte_array.id() != ID_array)
2093  {
2095  non_const_update_bound.has_value(),
2096  "constant update bound should yield an array expression");
2098  src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2099  }
2100 
2102  src,
2103  *subtype,
2104  to_array_expr(value_as_byte_array),
2105  non_const_update_bound,
2106  ns);
2107  }
2108  else
2110  src, *subtype, value_as_byte_array, non_const_update_bound, ns);
2111  }
2112  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
2113  {
2115  src,
2116  to_struct_type(ns.follow(src.type())),
2117  value_as_byte_array,
2118  non_const_update_bound,
2119  ns);
2120  result.type() = src.type();
2121  return result;
2122  }
2123  else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
2124  {
2125  exprt result = lower_byte_update_union(
2126  src,
2127  to_union_type(ns.follow(src.type())),
2128  value_as_byte_array,
2129  non_const_update_bound,
2130  ns);
2131  result.type() = src.type();
2132  return result;
2133  }
2134  else if(
2136  src.type().id() == ID_c_enum || src.type().id() == ID_c_enum_tag)
2137  {
2138  // mask out the bits to be updated, shift the value according to the
2139  // offset and bit-or
2140  const auto type_width = pointer_offset_bits(src.type(), ns);
2141  CHECK_RETURN(type_width.has_value() && *type_width > 0);
2142  const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2143 
2144  exprt::operandst update_bytes;
2145  if(value_as_byte_array.id() == ID_array)
2146  update_bytes = value_as_byte_array.operands();
2147  else
2148  {
2149  update_bytes =
2150  instantiate_byte_array(value_as_byte_array, 0, (type_bits + 7) / 8, ns);
2151  }
2152 
2153  const std::size_t update_size_bits = update_bytes.size() * 8;
2154  const std::size_t bit_width = std::max(type_bits, update_size_bits);
2155 
2156  const bool is_little_endian = src.id() == ID_byte_update_little_endian;
2157 
2158  exprt val_before =
2159  typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits});
2160  if(bit_width > type_bits)
2161  {
2162  val_before =
2163  concatenation_exprt{from_integer(0, bv_typet{bit_width - type_bits}),
2164  val_before,
2165  bv_typet{bit_width}};
2166 
2167  if(!is_little_endian)
2168  to_concatenation_expr(val_before)
2169  .op0()
2170  .swap(to_concatenation_expr(val_before).op1());
2171  }
2172 
2173  if(non_const_update_bound.has_value())
2174  {
2175  const exprt src_as_bytes = unpack_rec(
2176  val_before,
2177  src.id() == ID_byte_update_little_endian,
2178  mp_integer{0},
2179  mp_integer{update_bytes.size()},
2180  ns);
2181  CHECK_RETURN(src_as_bytes.id() == ID_array);
2182  CHECK_RETURN(src_as_bytes.operands().size() == update_bytes.size());
2183  for(std::size_t i = 0; i < update_bytes.size(); ++i)
2184  {
2185  update_bytes[i] =
2187  from_integer(i, non_const_update_bound->type()),
2188  ID_lt,
2189  *non_const_update_bound},
2190  update_bytes[i],
2191  src_as_bytes.operands()[i]};
2192  }
2193  }
2194 
2195  // build mask
2196  exprt mask;
2197  if(is_little_endian)
2198  mask = from_integer(power(2, update_size_bits) - 1, bv_typet{bit_width});
2199  else
2200  {
2201  mask = from_integer(
2202  power(2, bit_width) - power(2, bit_width - update_size_bits),
2203  bv_typet{bit_width});
2204  }
2205 
2206  const typet &offset_type = src.offset().type();
2207  mult_exprt offset_times_eight{src.offset(), from_integer(8, offset_type)};
2208 
2209  const binary_predicate_exprt offset_ge_zero{
2210  offset_times_eight, ID_ge, from_integer(0, offset_type)};
2211 
2212  if_exprt mask_shifted{offset_ge_zero,
2213  shl_exprt{mask, offset_times_eight},
2214  lshr_exprt{mask, offset_times_eight}};
2215  if(!is_little_endian)
2216  mask_shifted.true_case().swap(mask_shifted.false_case());
2217 
2218  // original_bits &= ~mask
2219  bitand_exprt bitand_expr{val_before, bitnot_exprt{mask_shifted}};
2220 
2221  // concatenate and zero-extend the value
2222  concatenation_exprt value{update_bytes, bv_typet{update_size_bits}};
2223  if(is_little_endian)
2224  std::reverse(value.operands().begin(), value.operands().end());
2225 
2226  exprt zero_extended;
2227  if(bit_width > update_size_bits)
2228  {
2229  zero_extended = concatenation_exprt{
2230  from_integer(0, bv_typet{bit_width - update_size_bits}),
2231  value,
2232  bv_typet{bit_width}};
2233 
2234  if(!is_little_endian)
2235  to_concatenation_expr(zero_extended)
2236  .op0()
2237  .swap(to_concatenation_expr(zero_extended).op1());
2238  }
2239  else
2240  zero_extended = value;
2241 
2242  // shift the value
2243  if_exprt value_shifted{offset_ge_zero,
2244  shl_exprt{zero_extended, offset_times_eight},
2245  lshr_exprt{zero_extended, offset_times_eight}};
2246  if(!is_little_endian)
2247  value_shifted.true_case().swap(value_shifted.false_case());
2248 
2249  // original_bits |= newvalue
2250  bitor_exprt bitor_expr{bitand_expr, value_shifted};
2251 
2252  if(bit_width > type_bits)
2253  {
2254  endianness_mapt endianness_map(
2255  bitor_expr.type(), src.id() == ID_byte_update_little_endian, ns);
2256  const auto bounds = map_bounds(endianness_map, 0, type_bits - 1);
2257 
2258  return simplify_expr(
2261  bitor_expr, bounds.ub, bounds.lb, bv_typet{type_bits}},
2262  src.type()),
2263  ns);
2264  }
2265 
2266  return simplify_expr(
2267  typecast_exprt::conditional_cast(bitor_expr, src.type()), ns);
2268  }
2269  else
2270  {
2272  false, "lower_byte_update does not yet support ", src.type().id_string());
2273  }
2274 }
2275 
2277 {
2279  src.id() == ID_byte_update_little_endian ||
2280  src.id() == ID_byte_update_big_endian,
2281  "byte update expression should either be little or big endian");
2282 
2283  // An update of a void-typed object or update by a void-typed value is the
2284  // source operand (this is questionable, but may arise when dereferencing
2285  // invalid pointers).
2286  if(src.type().id() == ID_empty || src.value().type().id() == ID_empty)
2287  return src.op();
2288 
2289  // byte_update lowering proceeds as follows:
2290  // 1) Determine the size of the update, with the size of the object to be
2291  // updated as an upper bound. We fail if neither can be determined.
2292  // 2) Turn the update value into a byte array of the size determined above.
2293  // 3) If the offset is not constant, turn the object into a byte array, and
2294  // use a "with" expression to encode the update; else update the values in
2295  // place.
2296  // 4) Construct a new object.
2297  optionalt<exprt> non_const_update_bound;
2298  // update value, may require extension to full bytes
2299  exprt update_value = src.value();
2300  auto update_size_expr_opt = size_of_expr(update_value.type(), ns);
2301  CHECK_RETURN(update_size_expr_opt.has_value());
2302  simplify(update_size_expr_opt.value(), ns);
2303 
2304  if(!update_size_expr_opt.value().is_constant())
2305  non_const_update_bound = *update_size_expr_opt;
2306  else
2307  {
2308  auto update_bits = pointer_offset_bits(update_value.type(), ns);
2309  // If the following invariant fails, then the type was only found to be
2310  // constant via simplification. Such instances should be fixed at the place
2311  // introducing these constant-but-not-constant_exprt type sizes.
2313  update_bits.has_value(), "constant size-of should imply fixed bit width");
2314  const size_t update_bits_int = numeric_cast_v<size_t>(*update_bits);
2315 
2316  if(update_bits_int % 8 != 0)
2317  {
2319  can_cast_type<bitvector_typet>(update_value.type()),
2320  "non-byte aligned type expected to be a bitvector type");
2321  size_t n_extra_bits = 8 - update_bits_int % 8;
2322 
2323  endianness_mapt endianness_map(
2324  src.op().type(), src.id() == ID_byte_update_little_endian, ns);
2325  const auto bounds = map_bounds(
2326  endianness_map, update_bits_int, update_bits_int + n_extra_bits - 1);
2327  extractbits_exprt extra_bits{
2328  src.op(), bounds.ub, bounds.lb, bv_typet{n_extra_bits}};
2329 
2330  update_value = concatenation_exprt{
2332  update_value, bv_typet{update_bits_int}),
2333  extra_bits,
2334  adjust_width(update_value.type(), update_bits_int + n_extra_bits)};
2335  }
2336  else
2337  {
2338  update_size_expr_opt =
2339  from_integer(update_bits_int / 8, update_size_expr_opt->type());
2340  }
2341  }
2342 
2343  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
2344  ? ID_byte_extract_little_endian
2345  : ID_byte_extract_big_endian;
2346 
2347  const byte_extract_exprt byte_extract_expr{
2348  extract_opcode,
2349  update_value,
2350  from_integer(0, src.offset().type()),
2351  array_typet{bv_typet{8}, *update_size_expr_opt}};
2352 
2353  const exprt value_as_byte_array = lower_byte_extract(byte_extract_expr, ns);
2354 
2355  exprt result =
2356  lower_byte_update(src, value_as_byte_array, non_const_update_bound, ns);
2357  return result;
2358 }
2359 
2360 bool has_byte_operator(const exprt &src)
2361 {
2362  if(src.id()==ID_byte_update_little_endian ||
2363  src.id()==ID_byte_update_big_endian ||
2364  src.id()==ID_byte_extract_little_endian ||
2365  src.id()==ID_byte_extract_big_endian)
2366  return true;
2367 
2368  forall_operands(it, src)
2369  if(has_byte_operator(*it))
2370  return true;
2371 
2372  return false;
2373 }
2374 
2376 {
2377  exprt tmp=src;
2378 
2379  // destroys any sharing, should use hash table
2380  Forall_operands(it, tmp)
2381  {
2382  *it = lower_byte_operators(*it, ns);
2383  }
2384 
2385  if(src.id()==ID_byte_update_little_endian ||
2386  src.id()==ID_byte_update_big_endian)
2387  return lower_byte_update(to_byte_update_expr(tmp), ns);
2388  else if(src.id()==ID_byte_extract_little_endian ||
2389  src.id()==ID_byte_extract_big_endian)
2390  return lower_byte_extract(to_byte_extract_expr(tmp), ns);
2391  else
2392  return tmp;
2393 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
API to expression classes for bitvectors.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
unsignedbv_typet size_type()
Definition: c_types.cpp:68
bitvector_typet c_index_type()
Definition: c_types.cpp:16
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:58
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3182
Array constructor from list of elements.
Definition: std_expr.h:1476
Arrays with given size.
Definition: std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
const exprt & size() const
Definition: std_types.h:790
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
Bit-wise AND.
Bit-wise negation of bit-vectors.
Bit-wise OR.
Base class of fixed-width bit-vector types.
Definition: std_types.h:853
std::size_t get_width() const
Definition: std_types.h:864
Fixed-width bit-vector without numerical interpretation.
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & value() const
const exprt & op() const
const exprt & offset() const
void set_op(exprt e)
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition: c_types.h:20
Complex constructor from a pair of numbers.
Definition: std_expr.h:1761
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1874
Real part of the expression describing a complex number.
Definition: std_expr.h:1829
Complex numbers made of pair of given subtype.
Definition: std_types.h:1057
Concatenation of bit-vector operands.
A constant literal expression.
Definition: std_expr.h:2807
Division.
Definition: std_expr.h:1064
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Maps a big-endian offset to a little-endian offset.
size_t number_of_bits() const
size_t map_bit(size_t bit) const
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
Extracts a sub-range of a bit-vector operand.
The trinary if-then-else operator.
Definition: std_expr.h:2226
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1353
exprt & index()
Definition: std_expr.h:1363
const std::string & id_string() const
Definition: irep.h:399
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
Logical right shift.
Extract member of struct or union.
Definition: std_expr.h:2667
Binary minus.
Definition: std_expr.h:973
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
exprt & op0()
Definition: std_expr.h:844
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
Boolean OR.
Definition: std_expr.h:2082
The plus expression Associativity is not specified.
Definition: std_expr.h:914
Left shift.
Fixed-width bit-vector with two's complement interpretation.
Struct constructor from list of elements.
Definition: std_expr.h:1722
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const typet & subtype() const
Definition: type.h:156
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
Union constructor from single element.
Definition: std_expr.h:1611
The union type.
Definition: c_types.h:125
optionalt< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
Definition: c_types.cpp:318
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
Definition: std_expr.h:1575
The vector type.
Definition: std_types.h:996
const constant_exprt & size() const
Definition: std_types.cpp:253
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1006
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
Deprecated expression utility functions.
nonstd::optional< T > optionalt
Definition: optional.h:35
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
static exprt unpack_array_vector_no_known_bounds(const exprt &src, std::size_t el_bytes, bool little_endian, const namespacet &ns)
Rewrite an array or vector into its individual bytes when no maximum number of bytes is known.
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...
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.
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.
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.
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 ...
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...
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...
bitvector_typet adjust_width(const typet &src, std::size_t new_width)
changes the width of the given bitvector type
static array_exprt unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
Rewrite a complex_exprt into its individual bytes.
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.
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...
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.
static union_exprt bv_to_union_expr(const exprt &bitvector_expr, const union_typet &union_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a union-typed expression.
bool has_byte_operator(const exprt &src)
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.
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.
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...
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
static exprt lower_byte_extract_array_vector(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const typet &subtype, const mp_integer &element_bits, const namespacet &ns)
Rewrite a byte extraction of an array/vector-typed result to byte extraction of the individual compon...
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.
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.
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.
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...
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.
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 ...
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...
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.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1506
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1082
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:887
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::size_t lb
std::size_t ub
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177