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