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 }
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)
bitvector_typet index_type()
Definition: c_types.cpp:16
unsignedbv_typet size_type()
Definition: c_types.cpp:58
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3128
Array constructor from list of elements.
Definition: std_expr.h:1467
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:771
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:832
std::size_t get_width() const
Definition: std_types.h:843
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)
Complex constructor from a pair of numbers.
Definition: std_expr.h:1707
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1820
Real part of the expression describing a complex number.
Definition: std_expr.h:1775
Complex numbers made of pair of given subtype.
Definition: std_types.h:1015
Concatenation of bit-vector operands.
A constant literal expression.
Definition: std_expr.h:2753
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:2172
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1344
exprt & index()
Definition: std_expr.h:1354
const std::string & id_string() const
Definition: irep.h:410
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:453
Logical right shift.
Extract member of struct or union.
Definition: std_expr.h:2613
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:2820
Boolean OR.
Definition: std_expr.h:2028
The plus expression Associativity is not specified.
Definition: std_expr.h:914
Left shift.
Struct constructor from list of elements.
Definition: std_expr.h:1668
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
Semantic type conversion.
Definition: std_expr.h:1866
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
Union constructor from single element.
Definition: std_expr.h:1602
The union type.
Definition: c_types.h:112
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
Vector constructor from list of elements.
Definition: std_expr.h:1566
The vector type.
Definition: std_types.h:975
const constant_exprt & size() const
Definition: std_types.cpp:239
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
#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:215
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:62
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 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...
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 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:2786
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1497
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1000
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:813
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1040
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:866
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:154