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/replace_symbol.h>
22 #include <util/simplify_expr.h>
23 #include <util/string_constant.h>
24 
25 static exprt bv_to_expr(
26  const exprt &bitvector_expr,
27  const typet &target_type,
28  const endianness_mapt &endianness_map,
29  const namespacet &ns);
30 
31 struct boundst
32 {
33  std::size_t lb;
34  std::size_t ub;
35 };
36 
39  const endianness_mapt &endianness_map,
40  std::size_t lower_bound,
41  std::size_t upper_bound)
42 {
43  boundst result;
44  result.lb = lower_bound;
45  result.ub = upper_bound;
46 
47  if(result.ub < endianness_map.number_of_bits())
48  {
49  result.lb = endianness_map.map_bit(result.lb);
50  result.ub = endianness_map.map_bit(result.ub);
51 
52  // big-endian bounds need swapping
53  if(result.ub < result.lb)
54  {
55  result.lb = endianness_map.number_of_bits() - result.lb - 1;
56  result.ub = endianness_map.number_of_bits() - result.ub - 1;
57  }
58  }
59 
60  return result;
61 }
62 
66  const exprt &bitvector_expr,
67  const struct_typet &struct_type,
68  const endianness_mapt &endianness_map,
69  const namespacet &ns)
70 {
71  const struct_typet::componentst &components = struct_type.components();
72 
73  exprt::operandst operands;
74  operands.reserve(components.size());
75  std::size_t member_offset_bits = 0;
76  for(const auto &comp : components)
77  {
78  const auto component_bits_opt = pointer_offset_bits(comp.type(), ns);
79  std::size_t component_bits;
80  if(component_bits_opt.has_value())
81  component_bits = numeric_cast_v<std::size_t>(*component_bits_opt);
82  else
83  component_bits = to_bitvector_type(bitvector_expr.type()).get_width() -
85 
86  if(component_bits == 0)
87  {
88  operands.push_back(constant_exprt{irep_idt{}, comp.type()});
89  continue;
90  }
91 
92  const auto bounds = map_bounds(
93  endianness_map,
95  member_offset_bits + component_bits - 1);
96  bitvector_typet type{bitvector_expr.type().id(), component_bits};
97  operands.push_back(bv_to_expr(
98  extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
99  comp.type(),
100  endianness_map,
101  ns));
102 
103  if(component_bits_opt.has_value())
104  member_offset_bits += component_bits;
105  }
106 
107  return struct_exprt{std::move(operands), struct_type};
108 }
109 
113  const exprt &bitvector_expr,
114  const union_typet &union_type,
115  const endianness_mapt &endianness_map,
116  const namespacet &ns)
117 {
118  const union_typet::componentst &components = union_type.components();
119 
120  // empty union, handled the same way as done in expr_initializert
121  if(components.empty())
122  return union_exprt{irep_idt{}, nil_exprt{}, union_type};
123 
124  const auto widest_member = union_type.find_widest_union_component(ns);
125 
126  std::size_t component_bits;
127  if(widest_member.has_value())
128  component_bits = numeric_cast_v<std::size_t>(widest_member->second);
129  else
130  component_bits = to_bitvector_type(bitvector_expr.type()).get_width();
131 
132  if(component_bits == 0)
133  {
134  return union_exprt{components.front().get_name(),
135  constant_exprt{irep_idt{}, components.front().type()},
136  union_type};
137  }
138 
139  const auto bounds = map_bounds(endianness_map, 0, component_bits - 1);
140  bitvector_typet type{bitvector_expr.type().id(), component_bits};
141  const irep_idt &component_name = widest_member.has_value()
142  ? widest_member->first.get_name()
143  : components.front().get_name();
144  const typet &component_type = widest_member.has_value()
145  ? widest_member->first.type()
146  : components.front().type();
147  return union_exprt{
148  component_name,
149  bv_to_expr(
150  extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
151  component_type,
152  endianness_map,
153  ns),
154  union_type};
155 }
156 
160  const exprt &bitvector_expr,
161  const array_typet &array_type,
162  const endianness_mapt &endianness_map,
163  const namespacet &ns)
164 {
165  auto num_elements = numeric_cast<std::size_t>(array_type.size());
166  auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
167 
168  const std::size_t total_bits =
169  to_bitvector_type(bitvector_expr.type()).get_width();
170  if(!num_elements.has_value())
171  {
172  if(!subtype_bits.has_value() || *subtype_bits == 0)
173  num_elements = total_bits;
174  else
175  num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
176  }
178  !num_elements.has_value() || !subtype_bits.has_value() ||
179  *subtype_bits * *num_elements == total_bits,
180  "subtype width times array size should be total bitvector width");
181 
182  exprt::operandst operands;
183  operands.reserve(*num_elements);
184  for(std::size_t i = 0; i < *num_elements; ++i)
185  {
186  if(subtype_bits.has_value())
187  {
188  const std::size_t subtype_bits_int =
189  numeric_cast_v<std::size_t>(*subtype_bits);
190  const auto bounds = map_bounds(
191  endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
192  bitvector_typet type{bitvector_expr.type().id(), subtype_bits_int};
193  operands.push_back(bv_to_expr(
195  bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
196  array_type.subtype(),
197  endianness_map,
198  ns));
199  }
200  else
201  {
202  operands.push_back(
203  bv_to_expr(bitvector_expr, array_type.subtype(), endianness_map, ns));
204  }
205  }
206 
207  return array_exprt{std::move(operands), array_type};
208 }
209 
213  const exprt &bitvector_expr,
214  const vector_typet &vector_type,
215  const endianness_mapt &endianness_map,
216  const namespacet &ns)
217 {
218  const std::size_t num_elements =
219  numeric_cast_v<std::size_t>(vector_type.size());
220  auto subtype_bits = pointer_offset_bits(vector_type.subtype(), ns);
222  !subtype_bits.has_value() ||
223  *subtype_bits * num_elements ==
224  to_bitvector_type(bitvector_expr.type()).get_width(),
225  "subtype width times vector size should be total bitvector width");
226 
227  exprt::operandst operands;
228  operands.reserve(num_elements);
229  for(std::size_t i = 0; i < num_elements; ++i)
230  {
231  if(subtype_bits.has_value())
232  {
233  const std::size_t subtype_bits_int =
234  numeric_cast_v<std::size_t>(*subtype_bits);
235  const auto bounds = map_bounds(
236  endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
237  bitvector_typet type{bitvector_expr.type().id(), subtype_bits_int};
238  operands.push_back(bv_to_expr(
240  bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
241  vector_type.subtype(),
242  endianness_map,
243  ns));
244  }
245  else
246  {
247  operands.push_back(
248  bv_to_expr(bitvector_expr, vector_type.subtype(), endianness_map, ns));
249  }
250  }
251 
252  return vector_exprt{std::move(operands), vector_type};
253 }
254 
258  const exprt &bitvector_expr,
259  const complex_typet &complex_type,
260  const endianness_mapt &endianness_map,
261  const namespacet &ns)
262 {
263  const std::size_t total_bits =
264  to_bitvector_type(bitvector_expr.type()).get_width();
265  const auto subtype_bits_opt = pointer_offset_bits(complex_type.subtype(), ns);
266  std::size_t subtype_bits;
267  if(subtype_bits_opt.has_value())
268  {
269  subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
271  subtype_bits * 2 == total_bits,
272  "subtype width should be half of the total bitvector width");
273  }
274  else
275  subtype_bits = total_bits / 2;
276 
277  const auto bounds_real = map_bounds(endianness_map, 0, subtype_bits - 1);
278  const auto bounds_imag =
279  map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
280 
281  const bitvector_typet type{bitvector_expr.type().id(), subtype_bits};
282 
283  return complex_exprt{
284  bv_to_expr(
285  extractbits_exprt{bitvector_expr, bounds_real.ub, bounds_real.lb, type},
286  complex_type.subtype(),
287  endianness_map,
288  ns),
289  bv_to_expr(
290  extractbits_exprt{bitvector_expr, bounds_imag.ub, bounds_imag.lb, type},
291  complex_type.subtype(),
292  endianness_map,
293  ns),
294  complex_type};
295 }
296 
311  const exprt &bitvector_expr,
312  const typet &target_type,
313  const endianness_mapt &endianness_map,
314  const namespacet &ns)
315 {
317 
318  if(
319  can_cast_type<bitvector_typet>(target_type) ||
320  target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
321  target_type.id() == ID_string)
322  {
323  std::size_t width = to_bitvector_type(bitvector_expr.type()).get_width();
324  exprt bv_expr =
325  typecast_exprt::conditional_cast(bitvector_expr, bv_typet{width});
326  return simplify_expr(
327  typecast_exprt::conditional_cast(bv_expr, target_type), ns);
328  }
329 
330  if(target_type.id() == ID_struct)
331  {
332  return bv_to_struct_expr(
333  bitvector_expr, to_struct_type(target_type), endianness_map, ns);
334  }
335  else if(target_type.id() == ID_struct_tag)
336  {
338  bitvector_expr,
339  ns.follow_tag(to_struct_tag_type(target_type)),
340  endianness_map,
341  ns);
342  result.type() = target_type;
343  return std::move(result);
344  }
345  else if(target_type.id() == ID_union)
346  {
347  return bv_to_union_expr(
348  bitvector_expr, to_union_type(target_type), endianness_map, ns);
349  }
350  else if(target_type.id() == ID_union_tag)
351  {
352  union_exprt result = bv_to_union_expr(
353  bitvector_expr,
354  ns.follow_tag(to_union_tag_type(target_type)),
355  endianness_map,
356  ns);
357  result.type() = target_type;
358  return std::move(result);
359  }
360  else if(target_type.id() == ID_array)
361  {
362  return bv_to_array_expr(
363  bitvector_expr, to_array_type(target_type), endianness_map, ns);
364  }
365  else if(target_type.id() == ID_vector)
366  {
367  return bv_to_vector_expr(
368  bitvector_expr, to_vector_type(target_type), endianness_map, ns);
369  }
370  else if(target_type.id() == ID_complex)
371  {
372  return bv_to_complex_expr(
373  bitvector_expr, to_complex_type(target_type), endianness_map, ns);
374  }
375  else
376  {
378  false, "bv_to_expr does not yet support ", target_type.id_string());
379  }
380 }
381 
382 static exprt unpack_rec(
383  const exprt &src,
384  bool little_endian,
385  const optionalt<mp_integer> &offset_bytes,
386  const optionalt<mp_integer> &max_bytes,
387  const namespacet &ns,
388  bool unpack_byte_array = false);
389 
397  const exprt &src,
398  std::size_t lower_bound,
399  std::size_t upper_bound,
400  const namespacet &ns)
401 {
402  PRECONDITION(lower_bound <= upper_bound);
403 
404  if(src.id() == ID_array)
405  {
406  PRECONDITION(upper_bound <= src.operands().size());
407  return exprt::operandst{
408  src.operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
409  src.operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
410  }
411 
412  exprt::operandst bytes;
413  bytes.reserve(upper_bound - lower_bound);
414  for(std::size_t i = lower_bound; i < upper_bound; ++i)
415  {
416  const index_exprt idx{src, from_integer(i, index_type())};
417  bytes.push_back(simplify_expr(idx, ns));
418  }
419  return bytes;
420 }
421 
436  const exprt &src,
437  const optionalt<mp_integer> &src_size,
438  const mp_integer &element_bits,
439  bool little_endian,
440  const optionalt<mp_integer> &offset_bytes,
441  const optionalt<mp_integer> &max_bytes,
442  const namespacet &ns)
443 {
444  const std::size_t el_bytes =
445  numeric_cast_v<std::size_t>((element_bits + 7) / 8);
446 
447  if(!src_size.has_value() && !max_bytes.has_value())
448  {
449  // TODO we either need a symbol table here or make array comprehensions
450  // introduce a scope
451  static std::size_t array_comprehension_index_counter = 0;
452  ++array_comprehension_index_counter;
453  symbol_exprt array_comprehension_index{
454  "$array_comprehension_index_a_v" +
455  std::to_string(array_comprehension_index_counter),
456  index_type()};
457 
458  CHECK_RETURN(el_bytes > 0);
459  index_exprt element{src,
460  div_exprt{array_comprehension_index,
461  from_integer(el_bytes, index_type())}};
462 
463  exprt sub = unpack_rec(element, little_endian, {}, {}, ns, false);
464  exprt::operandst sub_operands =
465  instantiate_byte_array(sub, 0, el_bytes, ns);
466 
467  exprt body = sub_operands.front();
468  const mod_exprt offset{
469  array_comprehension_index,
470  from_integer(el_bytes, array_comprehension_index.type())};
471  for(std::size_t i = 1; i < el_bytes; ++i)
472  {
473  body = if_exprt{
474  equal_exprt{offset, from_integer(i, array_comprehension_index.type())},
475  sub_operands[i],
476  body};
477  }
478 
479  const exprt array_vector_size = src.type().id() == ID_vector
480  ? to_vector_type(src.type()).size()
481  : to_array_type(src.type()).size();
482 
484  std::move(array_comprehension_index),
485  std::move(body),
486  array_typet{
487  bv_typet{8},
488  mult_exprt{array_vector_size,
489  from_integer(el_bytes, array_vector_size.type())}}};
490  }
491 
492  exprt::operandst byte_operands;
493  mp_integer first_element = 0;
494 
495  // refine the number of elements to extract in case the element width is known
496  // and a multiple of bytes; otherwise we will expand the entire array/vector
497  optionalt<mp_integer> num_elements = src_size;
498  if(element_bits > 0 && element_bits % 8 == 0)
499  {
500  if(!num_elements.has_value())
501  {
502  // turn bytes into elements, rounding up
503  num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
504  }
505 
506  if(offset_bytes.has_value())
507  {
508  // compute offset as number of elements
509  first_element = *offset_bytes / el_bytes;
510  // insert offset_bytes-many nil bytes into the output array
511  byte_operands.resize(
512  numeric_cast_v<std::size_t>(*offset_bytes - (*offset_bytes % el_bytes)),
513  from_integer(0, bv_typet{8}));
514  }
515  }
516 
517  // the maximum number of bytes is an upper bound in case the size of the
518  // array/vector is unknown; if element_bits was usable above this will
519  // have been turned into a number of elements already
520  if(!num_elements)
521  num_elements = *max_bytes;
522 
523  const exprt src_simp = simplify_expr(src, ns);
524 
525  for(mp_integer i = first_element; i < *num_elements; ++i)
526  {
527  exprt element;
528 
529  if(
530  (src_simp.id() == ID_array || src_simp.id() == ID_vector) &&
531  i < src_simp.operands().size())
532  {
533  const std::size_t index_int = numeric_cast_v<std::size_t>(i);
534  element = src_simp.operands()[index_int];
535  }
536  else
537  {
538  element = index_exprt(src_simp, from_integer(i, index_type()));
539  }
540 
541  // recursively unpack each element so that we eventually just have an array
542  // of bytes left
543 
544  const optionalt<mp_integer> element_max_bytes =
545  max_bytes
546  ? std::min(mp_integer{el_bytes}, *max_bytes - byte_operands.size())
548  const std::size_t element_max_bytes_int =
549  element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
550  : el_bytes;
551 
552  exprt sub =
553  unpack_rec(element, little_endian, {}, element_max_bytes, ns, true);
554  exprt::operandst sub_operands =
555  instantiate_byte_array(sub, 0, element_max_bytes_int, ns);
556  byte_operands.insert(
557  byte_operands.end(), sub_operands.begin(), sub_operands.end());
558 
559  if(max_bytes && byte_operands.size() >= *max_bytes)
560  break;
561  }
562 
563  const std::size_t size = byte_operands.size();
564  return array_exprt(
565  std::move(byte_operands),
567 }
568 
579 static void process_bit_fields(
580  exprt::operandst &&bit_fields,
581  std::size_t total_bits,
582  exprt::operandst &dest,
583  bool little_endian,
584  const optionalt<mp_integer> &offset_bytes,
585  const optionalt<mp_integer> &max_bytes,
586  const namespacet &ns)
587 {
588  const concatenation_exprt concatenation{std::move(bit_fields),
589  bv_typet{total_bits}};
590 
591  exprt sub =
592  unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns, true);
593 
594  dest.insert(
595  dest.end(),
596  std::make_move_iterator(sub.operands().begin()),
597  std::make_move_iterator(sub.operands().end()));
598 }
599 
610  const exprt &src,
611  bool little_endian,
612  const optionalt<mp_integer> &offset_bytes,
613  const optionalt<mp_integer> &max_bytes,
614  const namespacet &ns)
615 {
616  const struct_typet &struct_type = to_struct_type(ns.follow(src.type()));
617  const struct_typet::componentst &components = struct_type.components();
618 
619  optionalt<mp_integer> offset_in_member;
620  optionalt<mp_integer> max_bytes_left;
622 
624  exprt::operandst byte_operands;
625  for(auto it = components.begin(); it != components.end(); ++it)
626  {
627  const auto &comp = *it;
628  auto component_bits = pointer_offset_bits(comp.type(), ns);
629 
630  // We can only handle a member of unknown width when it is the last member
631  // and is byte-aligned. Members of unknown width in the middle would leave
632  // us with unknown alignment of subsequent members, and queuing them up as
633  // bit fields is not possible either as the total width of the concatenation
634  // could not be determined.
636  component_bits.has_value() ||
637  (std::next(it) == components.end() && !bit_fields.has_value()),
638  "members of non-constant width should come last in a struct");
639 
640  member_exprt member(src, comp.get_name(), comp.type());
641  if(src.id() == ID_struct)
642  simplify(member, ns);
643 
644  // Is it a byte-aligned member?
645  if(member_offset_bits % 8 == 0)
646  {
647  if(bit_fields.has_value())
648  {
650  std::move(bit_fields->first),
651  bit_fields->second,
652  byte_operands,
653  little_endian,
654  offset_in_member,
655  max_bytes_left,
656  ns);
657  bit_fields.reset();
658  }
659 
660  if(offset_bytes.has_value())
661  {
662  offset_in_member = *offset_bytes - member_offset_bits / 8;
663  // if the offset is negative, offset_in_member remains unset, which has
664  // the same effect as setting it to zero
665  if(*offset_in_member < 0)
666  offset_in_member.reset();
667  }
668 
669  if(max_bytes.has_value())
670  {
671  max_bytes_left = *max_bytes - member_offset_bits / 8;
672  if(*max_bytes_left < 0)
673  break;
674  }
675  }
676 
677  if(
678  member_offset_bits % 8 != 0 ||
679  (component_bits.has_value() && *component_bits % 8 != 0))
680  {
681  if(!bit_fields.has_value())
682  bit_fields = std::make_pair(exprt::operandst{}, std::size_t{0});
683 
684  const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
685  bit_fields->first.insert(
686  little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
687  typecast_exprt::conditional_cast(member, bv_typet{bits_int}));
688  bit_fields->second += bits_int;
689 
690  member_offset_bits += *component_bits;
691 
692  continue;
693  }
694 
695  INVARIANT(
696  !bit_fields.has_value(),
697  "all preceding members should have been processed");
698 
699  exprt sub = unpack_rec(
700  member, little_endian, offset_in_member, max_bytes_left, ns, true);
701 
702  byte_operands.insert(
703  byte_operands.end(),
704  std::make_move_iterator(sub.operands().begin()),
705  std::make_move_iterator(sub.operands().end()));
706 
707  if(component_bits.has_value())
708  member_offset_bits += *component_bits;
709  }
710 
711  if(bit_fields.has_value())
713  std::move(bit_fields->first),
714  bit_fields->second,
715  byte_operands,
716  little_endian,
717  offset_in_member,
718  max_bytes_left,
719  ns);
720 
721  const std::size_t size = byte_operands.size();
722  return array_exprt{std::move(byte_operands),
724 }
725 
731 static array_exprt
732 unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
733 {
734  const complex_typet &complex_type = to_complex_type(src.type());
735  const typet &subtype = complex_type.subtype();
736 
737  auto subtype_bits = pointer_offset_bits(subtype, ns);
738  CHECK_RETURN(subtype_bits.has_value());
739  CHECK_RETURN(*subtype_bits % 8 == 0);
740 
741  exprt sub_real = unpack_rec(
742  complex_real_exprt{src},
743  little_endian,
744  mp_integer{0},
745  *subtype_bits / 8,
746  ns,
747  true);
748  exprt::operandst byte_operands = std::move(sub_real.operands());
749 
750  exprt sub_imag = unpack_rec(
751  complex_imag_exprt{src},
752  little_endian,
753  mp_integer{0},
754  *subtype_bits / 8,
755  ns,
756  true);
757  byte_operands.insert(
758  byte_operands.end(),
759  std::make_move_iterator(sub_imag.operands().begin()),
760  std::make_move_iterator(sub_imag.operands().end()));
761 
762  const std::size_t size = byte_operands.size();
763  return array_exprt{std::move(byte_operands),
765 }
766 
776 // array of bytes
779  const exprt &src,
780  bool little_endian,
781  const optionalt<mp_integer> &offset_bytes,
782  const optionalt<mp_integer> &max_bytes,
783  const namespacet &ns,
784  bool unpack_byte_array)
785 {
786  if(src.type().id()==ID_array)
787  {
788  const array_typet &array_type=to_array_type(src.type());
789  const typet &subtype=array_type.subtype();
790 
791  auto element_bits = pointer_offset_bits(subtype, ns);
792  CHECK_RETURN(element_bits.has_value());
793 
794  if(!unpack_byte_array && *element_bits == 8)
795  return src;
796 
797  const auto constant_size_opt = numeric_cast<mp_integer>(array_type.size());
798  return unpack_array_vector(
799  src,
800  constant_size_opt,
801  *element_bits,
802  little_endian,
803  offset_bytes,
804  max_bytes,
805  ns);
806  }
807  else if(src.type().id() == ID_vector)
808  {
809  const vector_typet &vector_type = to_vector_type(src.type());
810  const typet &subtype = vector_type.subtype();
811 
812  auto element_bits = pointer_offset_bits(subtype, ns);
813  CHECK_RETURN(element_bits.has_value());
814 
815  if(!unpack_byte_array && *element_bits == 8)
816  return src;
817 
818  return unpack_array_vector(
819  src,
820  numeric_cast_v<mp_integer>(vector_type.size()),
821  *element_bits,
822  little_endian,
823  offset_bytes,
824  max_bytes,
825  ns);
826  }
827  else if(src.type().id() == ID_complex)
828  {
829  return unpack_complex(src, little_endian, ns);
830  }
831  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
832  {
833  return unpack_struct(src, little_endian, offset_bytes, max_bytes, ns);
834  }
835  else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
836  {
837  const union_typet &union_type = to_union_type(ns.follow(src.type()));
838  const union_typet::componentst &components = union_type.components();
839 
840  mp_integer max_width = 0;
841  typet max_comp_type;
842  irep_idt max_comp_name;
843 
844  for(const auto &comp : components)
845  {
846  auto element_width = pointer_offset_bits(comp.type(), ns);
847 
848  if(!element_width.has_value() || *element_width <= max_width)
849  continue;
850 
851  max_width = *element_width;
852  max_comp_type = comp.type();
853  max_comp_name = comp.get_name();
854  }
855 
856  if(max_width > 0)
857  {
858  member_exprt member(src, max_comp_name, max_comp_type);
859  return unpack_rec(
860  member, little_endian, offset_bytes, max_bytes, ns, true);
861  }
862  }
863  else if(src.type().id() == ID_pointer)
864  {
865  return unpack_rec(
867  little_endian,
868  offset_bytes,
869  max_bytes,
870  ns,
871  unpack_byte_array);
872  }
873  else if(src.id() == ID_string_constant)
874  {
875  return unpack_rec(
877  little_endian,
878  offset_bytes,
879  max_bytes,
880  ns,
881  unpack_byte_array);
882  }
883  else if(src.id() == ID_constant && src.type().id() == ID_string)
884  {
885  return unpack_rec(
886  string_constantt(to_constant_expr(src).get_value()).to_array_expr(),
887  little_endian,
888  offset_bytes,
889  max_bytes,
890  ns,
891  unpack_byte_array);
892  }
893  else if(src.type().id()!=ID_empty)
894  {
895  // a basic type; we turn that into extractbits while considering
896  // endianness
897  auto bits_opt = pointer_offset_bits(src.type(), ns);
898  DATA_INVARIANT(bits_opt.has_value(), "basic type should have a fixed size");
899 
900  const mp_integer total_bits = *bits_opt;
901  mp_integer last_bit = total_bits;
902  mp_integer bit_offset = 0;
903 
904  if(max_bytes.has_value())
905  {
906  const auto max_bits = *max_bytes * 8;
907  if(little_endian)
908  {
909  last_bit = std::min(last_bit, max_bits);
910  }
911  else
912  {
913  bit_offset = std::max(mp_integer{0}, last_bit - max_bits);
914  }
915  }
916 
917  auto const src_as_bitvector = typecast_exprt::conditional_cast(
918  src, bv_typet{numeric_cast_v<std::size_t>(total_bits)});
919  auto const byte_type = bv_typet{8};
920  exprt::operandst byte_operands;
921  for(; bit_offset < last_bit; bit_offset += 8)
922  {
923  extractbits_exprt extractbits(
924  src_as_bitvector,
925  from_integer(bit_offset + 7, index_type()),
926  from_integer(bit_offset, index_type()),
927  byte_type);
928 
929  // endianness_mapt should be the point of reference for mapping out
930  // endianness, but we need to work on elements here instead of
931  // individual bits
932  if(little_endian)
933  byte_operands.push_back(extractbits);
934  else
935  byte_operands.insert(byte_operands.begin(), extractbits);
936  }
937 
938  const std::size_t size = byte_operands.size();
939  return array_exprt(
940  std::move(byte_operands),
942  }
943 
944  return array_exprt(
945  {}, array_typet{bv_typet{8}, from_integer(0, size_type())});
946 }
947 
957  const byte_extract_exprt &src,
958  const byte_extract_exprt &unpacked,
959  const namespacet &ns)
960 {
961  const complex_typet &complex_type = to_complex_type(src.type());
962  const typet &subtype = complex_type.subtype();
963 
964  auto subtype_bits = pointer_offset_bits(subtype, ns);
965  if(!subtype_bits.has_value() || *subtype_bits % 8 != 0)
966  return {};
967 
968  // offset remains unchanged
969  byte_extract_exprt real{unpacked};
970  real.type() = subtype;
971 
972  const plus_exprt new_offset{
973  unpacked.offset(),
974  from_integer(*subtype_bits / 8, unpacked.offset().type())};
975  byte_extract_exprt imag{unpacked};
976  imag.type() = subtype;
977  imag.offset() = simplify_expr(new_offset, ns);
978 
979  return simplify_expr(
981  lower_byte_extract(real, ns), lower_byte_extract(imag, ns), complex_type},
982  ns);
983 }
984 
988 {
989  // General notes about endianness and the bit-vector conversion:
990  // A single byte with value 0b10001000 is stored (in irept) as
991  // exactly this string literal, and its bit-vector encoding will be
992  // bvt bv={0,0,0,1,0,0,0,1}, i.e., bv[0]==0 and bv[7]==1
993  //
994  // A multi-byte value like x=256 would be:
995  // - little-endian storage: ((char*)&x)[0]==0, ((char*)&x)[1]==1
996  // - big-endian storage: ((char*)&x)[0]==1, ((char*)&x)[1]==0
997  // - irept representation: 0000000100000000
998  // - bvt: {0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0}
999  // <... 8bits ...> <... 8bits ...>
1000  //
1001  // An array {0, 1} will be encoded as bvt bv={0,1}, i.e., bv[1]==1
1002  // concatenation(0, 1) will yield a bvt bv={1,0}, i.e., bv[1]==0
1003  //
1004  // The semantics of byte_extract(endianness, op, offset, T) is:
1005  // interpret ((char*)&op)+offset as the endianness-ordered storage
1006  // of an object of type T at address ((char*)&op)+offset
1007  // For some T x, byte_extract(endianness, x, 0, T) must yield x.
1008  //
1009  // byte_extract for a composite type T or an array will interpret
1010  // the individual subtypes with suitable endianness; the overall
1011  // order of components is not affected by endianness.
1012  //
1013  // Examples:
1014  // unsigned char A[4];
1015  // byte_extract_little_endian(A, 0, unsigned short) requests that
1016  // A[0],A[1] be interpreted as the storage of an unsigned short with
1017  // A[1] being the most-significant byte; byte_extract_big_endian for
1018  // the same operands will select A[0] as the most-significant byte.
1019  //
1020  // int A[2] = {0x01020304,0xDEADBEEF}
1021  // byte_extract_big_endian(A, 0, short) should yield 0x0102
1022  // byte_extract_little_endian(A, 0, short) should yield 0x0304
1023  // To obtain this we first compute byte arrays while taking into
1024  // account endianness:
1025  // big-endian byte representation: {01,02,03,04,DE,AB,BE,EF}
1026  // little-endian byte representation: {04,03,02,01,EF,BE,AB,DE}
1027  // We extract the relevant bytes starting from ((char*)A)+0:
1028  // big-endian: {01,02}; little-endian: {04,03}
1029  // Finally we place them in the appropriate byte order as indicated
1030  // by endianness:
1031  // big-endian: (short)concatenation(01,02)=0x0102
1032  // little-endian: (short)concatenation(03,04)=0x0304
1033 
1034  PRECONDITION(
1035  src.id() == ID_byte_extract_little_endian ||
1036  src.id() == ID_byte_extract_big_endian);
1037  const bool little_endian = src.id() == ID_byte_extract_little_endian;
1038 
1039  // determine an upper bound of the last byte we might need
1040  auto upper_bound_opt = size_of_expr(src.type(), ns);
1041  if(upper_bound_opt.has_value())
1042  {
1043  upper_bound_opt = simplify_expr(
1044  plus_exprt(
1045  upper_bound_opt.value(),
1047  src.offset(), upper_bound_opt.value().type())),
1048  ns);
1049  }
1050  else if(src.type().id() == ID_empty)
1051  upper_bound_opt = from_integer(0, size_type());
1052 
1053  const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.offset());
1054  const auto upper_bound_int_opt =
1055  numeric_cast<mp_integer>(upper_bound_opt.value_or(nil_exprt()));
1056 
1057  byte_extract_exprt unpacked(src);
1058  unpacked.op() = unpack_rec(
1059  src.op(), little_endian, lower_bound_int_opt, upper_bound_int_opt, ns);
1060  CHECK_RETURN(
1062  .get_width() == 8);
1063 
1064  if(src.type().id()==ID_array)
1065  {
1066  const array_typet &array_type=to_array_type(src.type());
1067  const typet &subtype=array_type.subtype();
1068 
1069  // consider ways of dealing with arrays of unknown subtype size or with a
1070  // subtype size that does not fit byte boundaries; currently we fall back to
1071  // stitching together consecutive elements down below
1072  auto element_bits = pointer_offset_bits(subtype, ns);
1073  if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1074  {
1075  auto num_elements = numeric_cast<std::size_t>(array_type.size());
1076 
1077  if(num_elements.has_value())
1078  {
1079  exprt::operandst operands;
1080  operands.reserve(*num_elements);
1081  for(std::size_t i = 0; i < *num_elements; ++i)
1082  {
1083  plus_exprt new_offset(
1084  unpacked.offset(),
1085  from_integer(i * (*element_bits) / 8, unpacked.offset().type()));
1086 
1087  byte_extract_exprt tmp(unpacked);
1088  tmp.type() = subtype;
1089  tmp.offset() = new_offset;
1090 
1091  operands.push_back(lower_byte_extract(tmp, ns));
1092  }
1093 
1094  return simplify_expr(array_exprt(std::move(operands), array_type), ns);
1095  }
1096  else
1097  {
1098  // TODO we either need a symbol table here or make array comprehensions
1099  // introduce a scope
1100  static std::size_t array_comprehension_index_counter = 0;
1101  ++array_comprehension_index_counter;
1102  symbol_exprt array_comprehension_index{
1103  "$array_comprehension_index_a" +
1104  std::to_string(array_comprehension_index_counter),
1105  index_type()};
1106 
1107  plus_exprt new_offset{
1108  unpacked.offset(),
1110  mult_exprt{array_comprehension_index,
1111  from_integer(
1112  *element_bits / 8, array_comprehension_index.type())},
1113  unpacked.offset().type())};
1114 
1115  byte_extract_exprt body(unpacked);
1116  body.type() = subtype;
1117  body.offset() = std::move(new_offset);
1118 
1119  return array_comprehension_exprt{std::move(array_comprehension_index),
1120  lower_byte_extract(body, ns),
1121  array_type};
1122  }
1123  }
1124  }
1125  else if(src.type().id() == ID_vector)
1126  {
1127  const vector_typet &vector_type = to_vector_type(src.type());
1128  const typet &subtype = vector_type.subtype();
1129 
1130  // consider ways of dealing with vectors of unknown subtype size or with a
1131  // subtype size that does not fit byte boundaries; currently we fall back to
1132  // stitching together consecutive elements down below
1133  auto element_bits = pointer_offset_bits(subtype, ns);
1134  if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1135  {
1136  const std::size_t num_elements =
1137  numeric_cast_v<std::size_t>(vector_type.size());
1138 
1139  exprt::operandst operands;
1140  operands.reserve(num_elements);
1141  for(std::size_t i = 0; i < num_elements; ++i)
1142  {
1143  plus_exprt new_offset(
1144  unpacked.offset(),
1145  from_integer(i * (*element_bits) / 8, unpacked.offset().type()));
1146 
1147  byte_extract_exprt tmp(unpacked);
1148  tmp.type() = subtype;
1149  tmp.offset() = simplify_expr(new_offset, ns);
1150 
1151  operands.push_back(lower_byte_extract(tmp, ns));
1152  }
1153 
1154  return simplify_expr(vector_exprt(std::move(operands), vector_type), ns);
1155  }
1156  }
1157  else if(src.type().id() == ID_complex)
1158  {
1159  auto result = lower_byte_extract_complex(src, unpacked, ns);
1160  if(result.has_value())
1161  return std::move(*result);
1162 
1163  // else fall back to generic lowering that uses bit masks, below
1164  }
1165  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
1166  {
1167  const struct_typet &struct_type=to_struct_type(ns.follow(src.type()));
1168  const struct_typet::componentst &components=struct_type.components();
1169 
1170  bool failed=false;
1171  struct_exprt s({}, src.type());
1172 
1173  for(const auto &comp : components)
1174  {
1175  auto component_bits = pointer_offset_bits(comp.type(), ns);
1176 
1177  // the next member would be misaligned, abort
1178  if(
1179  !component_bits.has_value() || *component_bits == 0 ||
1180  *component_bits % 8 != 0)
1181  {
1182  failed=true;
1183  break;
1184  }
1185 
1186  auto member_offset_opt =
1187  member_offset_expr(struct_type, comp.get_name(), ns);
1188 
1189  if(!member_offset_opt.has_value())
1190  {
1191  failed = true;
1192  break;
1193  }
1194 
1195  plus_exprt new_offset(
1196  unpacked.offset(),
1198  member_offset_opt.value(), unpacked.offset().type()));
1199 
1200  byte_extract_exprt tmp(unpacked);
1201  tmp.type()=comp.type();
1202  tmp.offset()=new_offset;
1203 
1204  s.add_to_operands(lower_byte_extract(tmp, ns));
1205  }
1206 
1207  if(!failed)
1208  return simplify_expr(std::move(s), ns);
1209  }
1210  else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
1211  {
1212  const union_typet &union_type = to_union_type(ns.follow(src.type()));
1213 
1214  const auto widest_member = union_type.find_widest_union_component(ns);
1215 
1216  if(widest_member.has_value())
1217  {
1218  byte_extract_exprt tmp(unpacked);
1219  tmp.type() = widest_member->first.type();
1220 
1221  return union_exprt(
1222  widest_member->first.get_name(),
1223  lower_byte_extract(tmp, ns),
1224  src.type());
1225  }
1226  }
1227 
1228  const exprt &root=unpacked.op();
1229  const exprt &offset=unpacked.offset();
1230 
1231  optionalt<typet> subtype;
1232  if(root.type().id() == ID_vector)
1233  subtype = to_vector_type(root.type()).subtype();
1234  else
1235  subtype = to_array_type(root.type()).subtype();
1236 
1237  auto subtype_bits = pointer_offset_bits(*subtype, ns);
1238 
1240  subtype_bits.has_value() && *subtype_bits == 8,
1241  "offset bits are byte aligned");
1242 
1243  auto size_bits = pointer_offset_bits(unpacked.type(), ns);
1244  if(!size_bits.has_value())
1245  {
1246  auto op0_bits = pointer_offset_bits(unpacked.op().type(), ns);
1247  // all cases with non-constant width should have been handled above
1249  op0_bits.has_value(),
1250  "the extracted width or the source width must be known");
1251  size_bits = op0_bits;
1252  }
1253 
1254  mp_integer num_bytes = (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
1255 
1256  // get 'width'-many bytes, and concatenate
1257  const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
1258  exprt::operandst op;
1259  op.reserve(width_bytes);
1260 
1261  for(std::size_t i=0; i<width_bytes; i++)
1262  {
1263  // the most significant byte comes first in the concatenation!
1264  std::size_t offset_int=
1265  little_endian?(width_bytes-i-1):i;
1266 
1267  plus_exprt offset_i(from_integer(offset_int, offset.type()), offset);
1268  simplify(offset_i, ns);
1269 
1270  mp_integer index = 0;
1271  if(
1272  offset_i.is_constant() &&
1273  (root.id() == ID_array || root.id() == ID_vector) &&
1274  !to_integer(to_constant_expr(offset_i), index) &&
1275  index < root.operands().size() && index >= 0)
1276  {
1277  // offset is constant and in range
1278  op.push_back(root.operands()[numeric_cast_v<std::size_t>(index)]);
1279  }
1280  else
1281  {
1282  op.push_back(index_exprt(root, offset_i));
1283  }
1284  }
1285 
1286  if(width_bytes==1)
1287  {
1288  return simplify_expr(
1289  typecast_exprt::conditional_cast(op.front(), src.type()), ns);
1290  }
1291  else // width_bytes>=2
1292  {
1293  concatenation_exprt concatenation(
1294  std::move(op), bitvector_typet(subtype->id(), width_bytes * 8));
1295 
1296  endianness_mapt map(src.type(), little_endian, ns);
1297  return bv_to_expr(concatenation, src.type(), map, ns);
1298  }
1299 }
1300 
1301 static exprt lower_byte_update(
1302  const byte_update_exprt &src,
1303  const exprt &value_as_byte_array,
1304  const optionalt<exprt> &non_const_update_bound,
1305  const namespacet &ns);
1306 
1317  const byte_update_exprt &src,
1318  const typet &subtype,
1319  const exprt &value_as_byte_array,
1320  const exprt &non_const_update_bound,
1321  const namespacet &ns)
1322 {
1323  // TODO we either need a symbol table here or make array comprehensions
1324  // introduce a scope
1325  static std::size_t array_comprehension_index_counter = 0;
1326  ++array_comprehension_index_counter;
1327  symbol_exprt array_comprehension_index{
1328  "$array_comprehension_index_u_a_v" +
1329  std::to_string(array_comprehension_index_counter),
1330  index_type()};
1331 
1332  binary_predicate_exprt lower_bound{
1334  array_comprehension_index, src.offset().type()),
1335  ID_lt,
1336  src.offset()};
1337  binary_predicate_exprt upper_bound{
1339  array_comprehension_index, non_const_update_bound.type()),
1340  ID_ge,
1342  src.offset(), non_const_update_bound.type()),
1343  non_const_update_bound}};
1344 
1345  if_exprt array_comprehension_body{
1346  or_exprt{std::move(lower_bound), std::move(upper_bound)},
1347  index_exprt{src.op(), array_comprehension_index},
1349  index_exprt{
1350  value_as_byte_array,
1351  minus_exprt{array_comprehension_index,
1353  src.offset(), array_comprehension_index.type())}},
1354  subtype)};
1355 
1356  return simplify_expr(
1357  array_comprehension_exprt{array_comprehension_index,
1358  std::move(array_comprehension_body),
1359  to_array_type(src.type())},
1360  ns);
1361 }
1362 
1373  const byte_update_exprt &src,
1374  const typet &subtype,
1375  const array_exprt &value_as_byte_array,
1376  const optionalt<exprt> &non_const_update_bound,
1377  const namespacet &ns)
1378 {
1379  // apply 'array-update-with' num_elements times
1380  exprt result = src.op();
1381 
1382  for(std::size_t i = 0; i < value_as_byte_array.operands().size(); ++i)
1383  {
1384  const exprt &element = value_as_byte_array.operands()[i];
1385 
1386  const exprt where = simplify_expr(
1387  plus_exprt{src.offset(), from_integer(i, src.offset().type())}, ns);
1388 
1389  // skip elements that wouldn't change (skip over typecasts as we might have
1390  // some signed/unsigned char conversions)
1391  const exprt &e = skip_typecast(element);
1392  if(e.id() == ID_index)
1393  {
1394  const index_exprt &index_expr = to_index_expr(e);
1395  if(index_expr.array() == src.op() && index_expr.index() == where)
1396  continue;
1397  }
1398 
1399  exprt update_value;
1400  if(non_const_update_bound.has_value())
1401  {
1402  update_value = typecast_exprt::conditional_cast(
1404  from_integer(i, non_const_update_bound->type()),
1405  ID_lt,
1406  *non_const_update_bound},
1407  element,
1408  index_exprt{src.op(), where}},
1409  subtype);
1410  }
1411  else
1412  update_value = typecast_exprt::conditional_cast(element, subtype);
1413 
1414  if(result.id() != ID_with)
1415  result = with_exprt{result, where, update_value};
1416  else
1417  result.add_to_operands(where, update_value);
1418  }
1419 
1420  return simplify_expr(std::move(result), ns);
1421 }
1422 
1439  const byte_update_exprt &src,
1440  const typet &subtype,
1441  const exprt &subtype_size,
1442  const exprt &value_as_byte_array,
1443  const exprt &non_const_update_bound,
1444  const exprt &initial_bytes,
1445  const exprt &first_index,
1446  const exprt &first_update_value,
1447  const namespacet &ns)
1448 {
1449  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1450  ? ID_byte_extract_little_endian
1451  : ID_byte_extract_big_endian;
1452 
1453  // TODO we either need a symbol table here or make array comprehensions
1454  // introduce a scope
1455  static std::size_t array_comprehension_index_counter = 0;
1456  ++array_comprehension_index_counter;
1457  symbol_exprt array_comprehension_index{
1458  "$array_comprehension_index_u_a_v_u" +
1459  std::to_string(array_comprehension_index_counter),
1460  index_type()};
1461 
1462  // all arithmetic uses offset/index types
1463  PRECONDITION(subtype_size.type() == src.offset().type());
1464  PRECONDITION(initial_bytes.type() == src.offset().type());
1465  PRECONDITION(first_index.type() == src.offset().type());
1466 
1467  // the bound from where updates start
1468  binary_predicate_exprt lower_bound{
1470  array_comprehension_index, first_index.type()),
1471  ID_lt,
1472  first_index};
1473 
1474  // The actual value of updates other than at the start or end
1475  plus_exprt offset_expr{
1476  initial_bytes,
1477  mult_exprt{subtype_size,
1479  array_comprehension_index, first_index.type()),
1480  first_index}}};
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 a 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.
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
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3025
Array constructor from list of elements.
Definition: std_expr.h:1382
Arrays with given size.
Definition: std_types.h:968
const exprt & size() const
Definition: std_types.h:976
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:644
Bit-wise AND.
Bit-wise negation of bit-vectors.
Bit-wise OR.
Base class of fixed-width bit-vector types.
Definition: std_types.h:1037
std::size_t get_width() const
Definition: std_types.h:1048
Fixed-width bit-vector without numerical interpretation.
Definition: std_types.h:1113
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:1622
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1735
Real part of the expression describing a complex number.
Definition: std_expr.h:1690
Complex numbers made of pair of given subtype.
Definition: std_types.h:1804
Concatenation of bit-vector operands.
A constant literal expression.
Definition: std_expr.h:2668
Division.
Definition: std_expr.h:981
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:1140
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:40
operandst & operands()
Definition: expr.h:96
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:140
Extracts a sub-range of a bit-vector operand.
The trinary if-then-else operator.
Definition: std_expr.h:2087
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
exprt & index()
Definition: std_expr.h:1269
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:452
Logical right shift.
Extract member of struct or union.
Definition: std_expr.h:2528
Binary minus.
Definition: std_expr.h:890
Modulo.
Definition: std_expr.h:1050
Binary multiplication Associativity is not specified.
Definition: std_expr.h:936
exprt & op0()
Definition: std_expr.h:761
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The NIL expression.
Definition: std_expr.h:2735
Boolean OR.
Definition: std_expr.h:1943
The plus expression Associativity is not specified.
Definition: std_expr.h:831
Left shift.
Struct constructor from list of elements.
Definition: std_expr.h:1583
Structure type, corresponds to C style structs.
Definition: std_types.h:226
const componentst & components() const
Definition: std_types.h:142
std::vector< componentt > componentst
Definition: std_types.h:135
Expression to hold a symbol (variable)
Definition: std_expr.h:81
Semantic type conversion.
Definition: std_expr.h:1781
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
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:1517
The union type.
Definition: std_types.h:393
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: std_types.cpp:293
Vector constructor from list of elements.
Definition: std_expr.h:1481
The vector type.
Definition: std_types.h:1764
const constant_exprt & size() const
Definition: std_types.cpp:282
Operator to update elements in structs and arrays.
Definition: std_expr.h:2173
#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:218
Deprecated expression utility functions.
BigInt mp_integer
Definition: mp_arith.h:19
nonstd::optional< T > optionalt
Definition: optional.h:35
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)
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:465
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1412
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1789
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1096
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:563
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1829
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:430
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:523
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:1071
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