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  plus_exprt{first_index,
1481  from_integer(1, first_index.type())}}}};
1482  exprt update_value = lower_byte_extract(
1484  extract_opcode, value_as_byte_array, std::move(offset_expr), subtype},
1485  ns);
1486 
1487  // The number of target array/vector elements being replaced, not including
1488  // a possible partial update at the end of the updated range, which is handled
1489  // below: (non_const_update_bound + (subtype_size - 1)) / subtype_size to
1490  // round up to the nearest multiple of subtype_size.
1491  div_exprt updated_elements{
1493  non_const_update_bound, subtype_size.type()),
1494  minus_exprt{subtype_size, from_integer(1, subtype_size.type())}},
1495  subtype_size};
1496 
1497  // The last element to be updated: first_index + updated_elements - 1
1498  plus_exprt last_index{first_index,
1499  minus_exprt{std::move(updated_elements),
1500  from_integer(1, first_index.type())}};
1501 
1502  // The size of a partial update at the end of the updated range, may be zero.
1503  mod_exprt tail_size{
1505  non_const_update_bound, initial_bytes.type()),
1506  initial_bytes},
1507  subtype_size};
1508 
1509  // The bound where updates end, which is conditional on the partial update
1510  // being empty.
1511  binary_predicate_exprt upper_bound{
1513  array_comprehension_index, last_index.type()),
1514  ID_ge,
1515  if_exprt{equal_exprt{tail_size, from_integer(0, tail_size.type())},
1516  last_index,
1517  plus_exprt{last_index, from_integer(1, last_index.type())}}};
1518 
1519  // The actual value of a partial update at the end.
1520  exprt last_update_value = lower_byte_operators(
1522  src.id(),
1523  index_exprt{src.op(), last_index},
1524  from_integer(0, src.offset().type()),
1525  byte_extract_exprt{extract_opcode,
1526  value_as_byte_array,
1528  last_index, subtype_size.type()),
1529  subtype_size},
1530  array_typet{bv_typet{8}, tail_size}}},
1531  ns);
1532 
1533  if_exprt array_comprehension_body{
1534  or_exprt{std::move(lower_bound), std::move(upper_bound)},
1535  index_exprt{src.op(), array_comprehension_index},
1536  if_exprt{
1538  array_comprehension_index, first_index.type()),
1539  first_index},
1540  first_update_value,
1542  array_comprehension_index, last_index.type()),
1543  last_index},
1544  std::move(last_update_value),
1545  std::move(update_value)}}};
1546 
1547  return simplify_expr(
1548  array_comprehension_exprt{array_comprehension_index,
1549  std::move(array_comprehension_body),
1550  to_array_type(src.type())},
1551  ns);
1552 }
1553 
1565  const byte_update_exprt &src,
1566  const typet &subtype,
1567  const exprt &value_as_byte_array,
1568  const optionalt<exprt> &non_const_update_bound,
1569  const namespacet &ns)
1570 {
1571  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1572  ? ID_byte_extract_little_endian
1573  : ID_byte_extract_big_endian;
1574 
1575  // do all arithmetic below using index/offset types - the array theory
1576  // back-end is really picky about indices having the same type
1577  auto subtype_size_opt = size_of_expr(subtype, ns);
1578  CHECK_RETURN(subtype_size_opt.has_value());
1579 
1580  const exprt subtype_size = simplify_expr(
1582  subtype_size_opt.value(), src.offset().type()),
1583  ns);
1584 
1585  // compute the index of the first element of the array/vector that may be
1586  // updated
1587  exprt first_index = div_exprt{src.offset(), subtype_size};
1588  simplify(first_index, ns);
1589 
1590  // compute the offset within that first element
1591  const exprt update_offset = mod_exprt{src.offset(), subtype_size};
1592 
1593  // compute the number of bytes (from the update value) that are going to be
1594  // consumed for updating the first element
1595  exprt initial_bytes = minus_exprt{subtype_size, update_offset};
1596  exprt update_bound;
1597  if(non_const_update_bound.has_value())
1598  {
1599  update_bound = typecast_exprt::conditional_cast(
1600  *non_const_update_bound, subtype_size.type());
1601  }
1602  else
1603  {
1605  value_as_byte_array.id() == ID_array,
1606  "value should be an array expression if the update bound is constant");
1607  update_bound =
1608  from_integer(value_as_byte_array.operands().size(), initial_bytes.type());
1609  }
1610  initial_bytes =
1611  if_exprt{binary_predicate_exprt{initial_bytes, ID_lt, update_bound},
1612  initial_bytes,
1613  update_bound};
1614  simplify(initial_bytes, ns);
1615 
1616  // encode the first update: update the original element at first_index with
1617  // initial_bytes-many bytes extracted from value_as_byte_array
1618  exprt first_update_value = lower_byte_operators(
1620  src.id(),
1621  index_exprt{src.op(), first_index},
1622  update_offset,
1623  byte_extract_exprt{extract_opcode,
1624  value_as_byte_array,
1625  from_integer(0, src.offset().type()),
1626  array_typet{bv_typet{8}, initial_bytes}}},
1627  ns);
1628 
1629  if(value_as_byte_array.id() != ID_array)
1630  {
1632  src,
1633  subtype,
1634  subtype_size,
1635  value_as_byte_array,
1636  *non_const_update_bound,
1637  initial_bytes,
1638  first_index,
1639  first_update_value,
1640  ns);
1641  }
1642 
1643  // We will update one array/vector element at a time - compute the number of
1644  // update values that will be consumed in each step. If we cannot determine a
1645  // constant value at this time we assume it's at least one byte. The
1646  // byte_extract_exprt within the loop uses the symbolic value (subtype_size),
1647  // we just need to make sure we make progress for the loop to terminate.
1648  std::size_t step_size = 1;
1649  if(subtype_size.is_constant())
1650  step_size = numeric_cast_v<std::size_t>(to_constant_expr(subtype_size));
1651  // Given the first update already encoded, keep track of the offset into the
1652  // update value. Again, the expressions within the loop use the symbolic
1653  // value, this is just an optimization in case we can determine a constant
1654  // offset.
1655  std::size_t offset = 0;
1656  if(initial_bytes.is_constant())
1657  offset = numeric_cast_v<std::size_t>(to_constant_expr(initial_bytes));
1658 
1659  with_exprt result{src.op(), first_index, first_update_value};
1660 
1661  std::size_t i = 1;
1662  for(; offset + step_size <= value_as_byte_array.operands().size();
1663  offset += step_size, ++i)
1664  {
1665  exprt where = simplify_expr(
1666  plus_exprt{first_index, from_integer(i, first_index.type())}, ns);
1667 
1668  exprt offset_expr = simplify_expr(
1669  plus_exprt{
1670  initial_bytes,
1671  mult_exprt{subtype_size, from_integer(i - 1, subtype_size.type())}},
1672  ns);
1673 
1674  exprt element = lower_byte_operators(
1676  src.id(),
1677  index_exprt{src.op(), where},
1678  from_integer(0, src.offset().type()),
1679  byte_extract_exprt{extract_opcode,
1680  value_as_byte_array,
1681  std::move(offset_expr),
1682  array_typet{bv_typet{8}, subtype_size}}},
1683  ns);
1684 
1685  result.add_to_operands(std::move(where), std::move(element));
1686  }
1687 
1688  // do the tail
1689  if(offset < value_as_byte_array.operands().size())
1690  {
1691  const std::size_t tail_size =
1692  value_as_byte_array.operands().size() - offset;
1693 
1694  exprt where = simplify_expr(
1695  plus_exprt{first_index, from_integer(i, first_index.type())}, ns);
1696 
1697  exprt element = lower_byte_operators(
1699  src.id(),
1700  index_exprt{src.op(), where},
1701  from_integer(0, src.offset().type()),
1703  extract_opcode,
1704  value_as_byte_array,
1705  from_integer(offset, src.offset().type()),
1706  array_typet{bv_typet{8}, from_integer(tail_size, size_type())}}},
1707  ns);
1708 
1709  result.add_to_operands(std::move(where), std::move(element));
1710  }
1711 
1712  return simplify_expr(std::move(result), ns);
1713 }
1714 
1725  const byte_update_exprt &src,
1726  const typet &subtype,
1727  const exprt &value_as_byte_array,
1728  const optionalt<exprt> &non_const_update_bound,
1729  const namespacet &ns)
1730 {
1731  const bool is_array = src.type().id() == ID_array;
1732  exprt size;
1733  if(is_array)
1734  size = to_array_type(src.type()).size();
1735  else
1736  size = to_vector_type(src.type()).size();
1737 
1738  auto subtype_bits = pointer_offset_bits(subtype, ns);
1739 
1740  // fall back to bytewise updates in all non-constant or dubious cases
1741  if(
1742  !size.is_constant() || !src.offset().is_constant() ||
1743  !subtype_bits.has_value() || *subtype_bits == 0 || *subtype_bits % 8 != 0 ||
1744  non_const_update_bound.has_value() || value_as_byte_array.id() != ID_array)
1745  {
1747  src, subtype, value_as_byte_array, non_const_update_bound, ns);
1748  }
1749 
1750  std::size_t num_elements =
1751  numeric_cast_v<std::size_t>(to_constant_expr(size));
1752  mp_integer offset_bytes =
1753  numeric_cast_v<mp_integer>(to_constant_expr(src.offset()));
1754 
1755  exprt::operandst elements;
1756  elements.reserve(num_elements);
1757 
1758  std::size_t i = 0;
1759  // copy the prefix not affected by the update
1760  for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bytes * 8; ++i)
1761  elements.push_back(index_exprt{src.op(), from_integer(i, index_type())});
1762 
1763  // the modified elements
1764  for(; i < num_elements &&
1765  i * *subtype_bits <
1766  (offset_bytes + value_as_byte_array.operands().size()) * 8;
1767  ++i)
1768  {
1769  mp_integer update_offset = offset_bytes - i * (*subtype_bits / 8);
1770  mp_integer update_elements = *subtype_bits / 8;
1771  exprt::operandst::const_iterator first =
1772  value_as_byte_array.operands().begin();
1773  exprt::operandst::const_iterator end = value_as_byte_array.operands().end();
1774  if(update_offset < 0)
1775  {
1776  INVARIANT(
1777  value_as_byte_array.operands().size() > -update_offset,
1778  "indices past the update should be handled above");
1779  first += numeric_cast_v<std::ptrdiff_t>(-update_offset);
1780  }
1781  else
1782  {
1783  update_elements -= update_offset;
1784  INVARIANT(
1785  update_elements > 0,
1786  "indices before the update should be handled above");
1787  }
1788 
1789  if(std::distance(first, end) > update_elements)
1790  end = first + numeric_cast_v<std::ptrdiff_t>(update_elements);
1791  exprt::operandst update_values{first, end};
1792  const std::size_t update_size = update_values.size();
1793 
1794  const byte_update_exprt bu{
1795  src.id(),
1796  index_exprt{src.op(), from_integer(i, index_type())},
1797  from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
1798  array_exprt{
1799  std::move(update_values),
1800  array_typet{bv_typet{8}, from_integer(update_size, size_type())}}};
1801  elements.push_back(lower_byte_operators(bu, ns));
1802  }
1803 
1804  // copy the tail not affected by the update
1805  for(; i < num_elements; ++i)
1806  elements.push_back(index_exprt{src.op(), from_integer(i, index_type())});
1807 
1808  if(is_array)
1809  return simplify_expr(
1810  array_exprt{std::move(elements), to_array_type(src.type())}, ns);
1811  else
1812  return simplify_expr(
1813  vector_exprt{std::move(elements), to_vector_type(src.type())}, ns);
1814 }
1815 
1826  const byte_update_exprt &src,
1827  const struct_typet &struct_type,
1828  const exprt &value_as_byte_array,
1829  const optionalt<exprt> &non_const_update_bound,
1830  const namespacet &ns)
1831 {
1832  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1833  ? ID_byte_extract_little_endian
1834  : ID_byte_extract_big_endian;
1835 
1836  exprt::operandst elements;
1837  elements.reserve(struct_type.components().size());
1838 
1840  for(const auto &comp : struct_type.components())
1841  {
1842  auto element_width = pointer_offset_bits(comp.type(), ns);
1843 
1844  exprt member = member_exprt{src.op(), comp.get_name(), comp.type()};
1845 
1846  // compute the update offset relative to this struct member - will be
1847  // negative if we are already in the middle of the update or beyond it
1848  exprt offset = simplify_expr(
1849  minus_exprt{src.offset(),
1850  from_integer(member_offset_bits / 8, src.offset().type())},
1851  ns);
1852  auto offset_bytes = numeric_cast<mp_integer>(offset);
1853  // we don't need to update anything when
1854  // 1) the update offset is greater than the end of this member (thus the
1855  // relative offset is greater than this element) or
1856  // 2) the update offset plus the size of the update is less than the member
1857  // offset
1858  if(
1859  offset_bytes.has_value() &&
1860  (*offset_bytes * 8 >= *element_width ||
1861  (value_as_byte_array.id() == ID_array && *offset_bytes < 0 &&
1862  -*offset_bytes >= value_as_byte_array.operands().size())))
1863  {
1864  elements.push_back(std::move(member));
1865  member_offset_bits += *element_width;
1866  continue;
1867  }
1868  else if(!offset_bytes.has_value())
1869  {
1870  // The offset to update is not constant; abort the attempt to update
1871  // indiviual struct members and instead turn the operand-to-be-updated
1872  // into a byte array, which we know how to update even if the offset is
1873  // non-constant.
1874  auto src_size_opt = size_of_expr(src.type(), ns);
1875  CHECK_RETURN(src_size_opt.has_value());
1876 
1877  const byte_extract_exprt byte_extract_expr{
1878  extract_opcode,
1879  src.op(),
1880  from_integer(0, src.offset().type()),
1881  array_typet{bv_typet{8}, src_size_opt.value()}};
1882 
1883  byte_update_exprt bu = src;
1884  bu.set_op(lower_byte_extract(byte_extract_expr, ns));
1885  bu.type() = bu.op().type();
1886 
1887  return lower_byte_extract(
1889  extract_opcode,
1891  bu, value_as_byte_array, non_const_update_bound, ns),
1892  from_integer(0, src.offset().type()),
1893  src.type()},
1894  ns);
1895  }
1896 
1897  // We now need to figure out how many bytes to consume from the update
1898  // value. If the size of the update is unknown, then we need to leave some
1899  // of this work to a back-end solver via the non_const_update_bound branch
1900  // below.
1901  mp_integer update_elements = (*element_width + 7) / 8;
1902  std::size_t first = 0;
1903  if(*offset_bytes < 0)
1904  {
1905  offset = from_integer(0, src.offset().type());
1906  INVARIANT(
1907  value_as_byte_array.id() != ID_array ||
1908  value_as_byte_array.operands().size() > -*offset_bytes,
1909  "members past the update should be handled above");
1910  first = numeric_cast_v<std::size_t>(-*offset_bytes);
1911  }
1912  else
1913  {
1914  update_elements -= *offset_bytes;
1915  INVARIANT(
1916  update_elements > 0,
1917  "members before the update should be handled above");
1918  }
1919 
1920  // Now that we have an idea on how many bytes we need from the update value,
1921  // determine the exact range [first, end) in the update value, and create
1922  // that sequence of bytes (via instantiate_byte_array).
1923  std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1924  if(value_as_byte_array.id() == ID_array)
1925  end = std::min(end, value_as_byte_array.operands().size());
1926  exprt::operandst update_values =
1927  instantiate_byte_array(value_as_byte_array, first, end, ns);
1928  const std::size_t update_size = update_values.size();
1929 
1930  // With an upper bound on the size of the update established, construct the
1931  // actual update expression. If the exact size of the update is unknown,
1932  // make the size expression conditional.
1933  exprt update_size_expr = from_integer(update_size, size_type());
1934  array_exprt update_expr{std::move(update_values),
1935  array_typet{bv_typet{8}, update_size_expr}};
1936  optionalt<exprt> member_update_bound;
1937  if(non_const_update_bound.has_value())
1938  {
1939  // The size of the update is not constant, and thus is to be symbolically
1940  // bound; first see how many bytes we have left in the update:
1941  // non_const_update_bound > first ? non_const_update_bound - first: 0
1942  const exprt remaining_update_bytes = typecast_exprt::conditional_cast(
1943  if_exprt{
1945  *non_const_update_bound,
1946  ID_gt,
1947  from_integer(first, non_const_update_bound->type())},
1948  minus_exprt{*non_const_update_bound,
1949  from_integer(first, non_const_update_bound->type())},
1950  from_integer(0, non_const_update_bound->type())},
1951  size_type());
1952  // Now take the minimum of update-bytes-left and the previously computed
1953  // size of the member to be updated:
1954  update_size_expr = if_exprt{
1955  binary_predicate_exprt{update_size_expr, ID_lt, remaining_update_bytes},
1956  update_size_expr,
1957  remaining_update_bytes};
1958  simplify(update_size_expr, ns);
1959  member_update_bound = std::move(update_size_expr);
1960  }
1961 
1962  // We have established the bytes to use for the update, but now need to
1963  // account for sub-byte members.
1964  const std::size_t shift =
1965  numeric_cast_v<std::size_t>(member_offset_bits % 8);
1966  const std::size_t element_bits_int =
1967  numeric_cast_v<std::size_t>(*element_width);
1968 
1969  const bool little_endian = src.id() == ID_byte_update_little_endian;
1970  if(shift != 0)
1971  {
1972  member = concatenation_exprt{
1973  typecast_exprt::conditional_cast(member, bv_typet{element_bits_int}),
1974  from_integer(0, bv_typet{shift}),
1975  bv_typet{shift + element_bits_int}};
1976 
1977  if(!little_endian)
1978  to_concatenation_expr(member).op0().swap(
1979  to_concatenation_expr(member).op1());
1980  }
1981 
1982  // Finally construct the updated member.
1983  byte_update_exprt bu{src.id(), std::move(member), offset, update_expr};
1984  exprt updated_element =
1985  lower_byte_update(bu, update_expr, member_update_bound, ns);
1986 
1987  if(shift == 0)
1988  elements.push_back(updated_element);
1989  else
1990  {
1991  elements.push_back(typecast_exprt::conditional_cast(
1992  extractbits_exprt{updated_element,
1993  element_bits_int - 1 + (little_endian ? shift : 0),
1994  (little_endian ? shift : 0),
1995  bv_typet{element_bits_int}},
1996  comp.type()));
1997  }
1998 
1999  member_offset_bits += *element_width;
2000  }
2001 
2002  return simplify_expr(struct_exprt{std::move(elements), struct_type}, ns);
2003 }
2004 
2015  const byte_update_exprt &src,
2016  const union_typet &union_type,
2017  const exprt &value_as_byte_array,
2018  const optionalt<exprt> &non_const_update_bound,
2019  const namespacet &ns)
2020 {
2021  const auto widest_member = union_type.find_widest_union_component(ns);
2022 
2024  widest_member.has_value(),
2025  "lower_byte_update of union of unknown size is not supported");
2026 
2027  byte_update_exprt bu = src;
2028  bu.set_op(member_exprt{
2029  src.op(), widest_member->first.get_name(), widest_member->first.type()});
2030  bu.type() = widest_member->first.type();
2031 
2032  return union_exprt{
2033  widest_member->first.get_name(),
2034  lower_byte_update(bu, value_as_byte_array, non_const_update_bound, ns),
2035  src.type()};
2036 }
2037 
2047  const byte_update_exprt &src,
2048  const exprt &value_as_byte_array,
2049  const optionalt<exprt> &non_const_update_bound,
2050  const namespacet &ns)
2051 {
2052  if(src.type().id() == ID_array || src.type().id() == ID_vector)
2053  {
2054  optionalt<typet> subtype;
2055  if(src.type().id() == ID_vector)
2056  subtype = to_vector_type(src.type()).subtype();
2057  else
2058  subtype = to_array_type(src.type()).subtype();
2059 
2060  auto element_width = pointer_offset_bits(*subtype, ns);
2061  CHECK_RETURN(element_width.has_value());
2062  CHECK_RETURN(*element_width > 0);
2063  CHECK_RETURN(*element_width % 8 == 0);
2064 
2065  if(*element_width == 8)
2066  {
2067  if(value_as_byte_array.id() != ID_array)
2068  {
2070  non_const_update_bound.has_value(),
2071  "constant update bound should yield an array expression");
2073  src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2074  }
2075 
2077  src,
2078  *subtype,
2079  to_array_expr(value_as_byte_array),
2080  non_const_update_bound,
2081  ns);
2082  }
2083  else
2085  src, *subtype, value_as_byte_array, non_const_update_bound, ns);
2086  }
2087  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
2088  {
2090  src,
2091  to_struct_type(ns.follow(src.type())),
2092  value_as_byte_array,
2093  non_const_update_bound,
2094  ns);
2095  result.type() = src.type();
2096  return result;
2097  }
2098  else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
2099  {
2100  exprt result = lower_byte_update_union(
2101  src,
2102  to_union_type(ns.follow(src.type())),
2103  value_as_byte_array,
2104  non_const_update_bound,
2105  ns);
2106  result.type() = src.type();
2107  return result;
2108  }
2109  else if(
2111  src.type().id() == ID_c_enum || src.type().id() == ID_c_enum_tag)
2112  {
2113  // mask out the bits to be updated, shift the value according to the
2114  // offset and bit-or
2115  const auto type_width = pointer_offset_bits(src.type(), ns);
2116  CHECK_RETURN(type_width.has_value() && *type_width > 0);
2117  const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2118 
2119  exprt::operandst update_bytes;
2120  if(value_as_byte_array.id() == ID_array)
2121  update_bytes = value_as_byte_array.operands();
2122  else
2123  {
2124  update_bytes =
2125  instantiate_byte_array(value_as_byte_array, 0, (type_bits + 7) / 8, ns);
2126  }
2127 
2128  const std::size_t update_size_bits = update_bytes.size() * 8;
2129  const std::size_t bit_width = std::max(type_bits, update_size_bits);
2130 
2131  const bool is_little_endian = src.id() == ID_byte_update_little_endian;
2132 
2133  exprt val_before =
2134  typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits});
2135  if(bit_width > type_bits)
2136  {
2137  val_before =
2138  concatenation_exprt{from_integer(0, bv_typet{bit_width - type_bits}),
2139  val_before,
2140  bv_typet{bit_width}};
2141 
2142  if(!is_little_endian)
2143  to_concatenation_expr(val_before)
2144  .op0()
2145  .swap(to_concatenation_expr(val_before).op1());
2146  }
2147 
2148  if(non_const_update_bound.has_value())
2149  {
2150  const exprt src_as_bytes = unpack_rec(
2151  val_before,
2152  src.id() == ID_byte_update_little_endian,
2153  mp_integer{0},
2154  mp_integer{update_bytes.size()},
2155  ns);
2156  CHECK_RETURN(src_as_bytes.id() == ID_array);
2157  CHECK_RETURN(src_as_bytes.operands().size() == update_bytes.size());
2158  for(std::size_t i = 0; i < update_bytes.size(); ++i)
2159  {
2160  update_bytes[i] =
2162  from_integer(i, non_const_update_bound->type()),
2163  ID_lt,
2164  *non_const_update_bound},
2165  update_bytes[i],
2166  src_as_bytes.operands()[i]};
2167  }
2168  }
2169 
2170  // build mask
2171  exprt mask;
2172  if(is_little_endian)
2173  mask = from_integer(power(2, update_size_bits) - 1, bv_typet{bit_width});
2174  else
2175  {
2176  mask = from_integer(
2177  power(2, bit_width) - power(2, bit_width - update_size_bits),
2178  bv_typet{bit_width});
2179  }
2180 
2181  const typet &offset_type = src.offset().type();
2182  mult_exprt offset_times_eight{src.offset(), from_integer(8, offset_type)};
2183 
2184  const binary_predicate_exprt offset_ge_zero{
2185  offset_times_eight, ID_ge, from_integer(0, offset_type)};
2186 
2187  if_exprt mask_shifted{offset_ge_zero,
2188  shl_exprt{mask, offset_times_eight},
2189  lshr_exprt{mask, offset_times_eight}};
2190  if(!is_little_endian)
2191  mask_shifted.true_case().swap(mask_shifted.false_case());
2192 
2193  // original_bits &= ~mask
2194  bitand_exprt bitand_expr{val_before, bitnot_exprt{mask_shifted}};
2195 
2196  // concatenate and zero-extend the value
2197  concatenation_exprt value{update_bytes, bv_typet{update_size_bits}};
2198  if(is_little_endian)
2199  std::reverse(value.operands().begin(), value.operands().end());
2200 
2201  exprt zero_extended;
2202  if(bit_width > update_size_bits)
2203  {
2204  zero_extended = concatenation_exprt{
2205  from_integer(0, bv_typet{bit_width - update_size_bits}),
2206  value,
2207  bv_typet{bit_width}};
2208 
2209  if(!is_little_endian)
2210  to_concatenation_expr(zero_extended)
2211  .op0()
2212  .swap(to_concatenation_expr(zero_extended).op1());
2213  }
2214  else
2215  zero_extended = value;
2216 
2217  // shift the value
2218  if_exprt value_shifted{offset_ge_zero,
2219  shl_exprt{zero_extended, offset_times_eight},
2220  lshr_exprt{zero_extended, offset_times_eight}};
2221  if(!is_little_endian)
2222  value_shifted.true_case().swap(value_shifted.false_case());
2223 
2224  // original_bits |= newvalue
2225  bitor_exprt bitor_expr{bitand_expr, value_shifted};
2226 
2227  if(!is_little_endian && bit_width > type_bits)
2228  {
2229  return simplify_expr(
2231  extractbits_exprt{bitor_expr,
2232  bit_width - 1,
2233  bit_width - type_bits,
2234  bv_typet{type_bits}},
2235  src.type()),
2236  ns);
2237  }
2238  else if(bit_width > type_bits)
2239  {
2240  return simplify_expr(
2242  extractbits_exprt{bitor_expr, type_bits - 1, 0, bv_typet{type_bits}},
2243  src.type()),
2244  ns);
2245  }
2246 
2247  return simplify_expr(
2248  typecast_exprt::conditional_cast(bitor_expr, src.type()), ns);
2249  }
2250  else
2251  {
2253  false, "lower_byte_update does not yet support ", src.type().id_string());
2254  }
2255 }
2256 
2258 {
2260  src.id() == ID_byte_update_little_endian ||
2261  src.id() == ID_byte_update_big_endian,
2262  "byte update expression should either be little or big endian");
2263 
2264  // An update of a void-typed object or update by a void-typed value is the
2265  // source operand (this is questionable, but may arise when dereferencing
2266  // invalid pointers).
2267  if(src.type().id() == ID_empty || src.value().type().id() == ID_empty)
2268  return src.op();
2269 
2270  // byte_update lowering proceeds as follows:
2271  // 1) Determine the size of the update, with the size of the object to be
2272  // updated as an upper bound. We fail if neither can be determined.
2273  // 2) Turn the update value into a byte array of the size determined above.
2274  // 3) If the offset is not constant, turn the object into a byte array, and
2275  // use a "with" expression to encode the update; else update the values in
2276  // place.
2277  // 4) Construct a new object.
2278  optionalt<exprt> non_const_update_bound;
2279  auto update_size_expr_opt = size_of_expr(src.value().type(), ns);
2280  CHECK_RETURN(update_size_expr_opt.has_value());
2281  simplify(update_size_expr_opt.value(), ns);
2282 
2283  if(!update_size_expr_opt.value().is_constant())
2284  non_const_update_bound = *update_size_expr_opt;
2285 
2286  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
2287  ? ID_byte_extract_little_endian
2288  : ID_byte_extract_big_endian;
2289 
2290  const byte_extract_exprt byte_extract_expr{
2291  extract_opcode,
2292  src.value(),
2293  from_integer(0, src.offset().type()),
2294  array_typet{bv_typet{8}, *update_size_expr_opt}};
2295 
2296  const exprt value_as_byte_array = lower_byte_extract(byte_extract_expr, ns);
2297 
2298  exprt result =
2299  lower_byte_update(src, value_as_byte_array, non_const_update_bound, ns);
2300  return result;
2301 }
2302 
2303 bool has_byte_operator(const exprt &src)
2304 {
2305  if(src.id()==ID_byte_update_little_endian ||
2306  src.id()==ID_byte_update_big_endian ||
2307  src.id()==ID_byte_extract_little_endian ||
2308  src.id()==ID_byte_extract_big_endian)
2309  return true;
2310 
2311  forall_operands(it, src)
2312  if(has_byte_operator(*it))
2313  return true;
2314 
2315  return false;
2316 }
2317 
2319 {
2320  exprt tmp=src;
2321 
2322  // destroys any sharing, should use hash table
2323  Forall_operands(it, tmp)
2324  {
2325  *it = lower_byte_operators(*it, ns);
2326  }
2327 
2328  if(src.id()==ID_byte_update_little_endian ||
2329  src.id()==ID_byte_update_big_endian)
2330  return lower_byte_update(to_byte_update_expr(tmp), ns);
2331  else if(src.id()==ID_byte_extract_little_endian ||
2332  src.id()==ID_byte_extract_big_endian)
2333  return lower_byte_extract(to_byte_extract_expr(tmp), ns);
2334  else
2335  return tmp;
2336 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2172
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
bv_to_vector_expr
static vector_exprt bv_to_vector_expr(const exprt &bitvector_expr, const vector_typet &vector_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a vector-typed expression.
Definition: byte_operators.cpp:212
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
unpack_complex
static array_exprt unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
Rewrite a complex_exprt into its individual bytes.
Definition: byte_operators.cpp:732
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1788
typet::subtype
const typet & subtype() const
Definition: type.h:47
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:219
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:81
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
arith_tools.h
to_array_expr
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1411
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
member_offset_bits
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:64
typet
The type of an expression, extends irept.
Definition: type.h:28
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
union_typet::find_widest_union_component
optionalt< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
Definition: c_types.cpp:308
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
byte_update_exprt::offset
const exprt & offset() const
Definition: byte_operators.h:109
has_byte_operator
bool has_byte_operator(const exprt &src)
Definition: byte_operators.cpp:2303
replace_symbol.h
unpack_array_vector
static exprt unpack_array_vector(const exprt &src, const optionalt< mp_integer > &src_size, const mp_integer &element_bits, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
Rewrite an array or vector into its individual bytes.
Definition: byte_operators.cpp:435
lower_byte_update
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
Definition: byte_operators.cpp:2046
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1689
union_exprt
Union constructor from single element.
Definition: std_expr.h:1516
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
bv_to_expr
static exprt bv_to_expr(const exprt &bitvector_expr, const typet &target_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an expression of type target_type.
Definition: byte_operators.cpp:310
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:154
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
lower_byte_extract
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
Definition: byte_operators.cpp:987
string_constant.h
lower_byte_update_array_vector
static exprt lower_byte_update_array_vector(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand using the byte array value_as_byte_array as ...
Definition: byte_operators.cpp:1724
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:66
byte_update_exprt::set_op
void set_op(exprt e)
Definition: byte_operators.h:95
complex_typet
Complex numbers made of pair of given subtype.
Definition: std_types.h:1009
vector_typet
The vector type.
Definition: std_types.h:969
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
concatenation_exprt
Concatenation of bit-vector operands.
Definition: bitvector_expr.h:590
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1480
lshr_exprt
Logical right shift.
Definition: bitvector_expr.h:348
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1034
div_exprt
Division.
Definition: std_expr.h:980
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
namespace.h
string_constantt
Definition: string_constant.h:16
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1139
expr_lowering.h
lower_byte_update_byte_array_vector
static exprt lower_byte_update_byte_array_vector(const byte_update_exprt &src, const typet &subtype, const array_exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte array value_as_byte_array as updat...
Definition: byte_operators.cpp:1372
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1582
array_typet::size
const exprt & size() const
Definition: std_types.h:765
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
bv_to_struct_expr
static struct_exprt bv_to_struct_expr(const exprt &bitvector_expr, const struct_typet &struct_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a struct-typed expression.
Definition: byte_operators.cpp:65
byte_operators.h
Expression classes for byte-level operators.
bitor_exprt
Bit-wise OR.
Definition: bitvector_expr.h:125
endianness_mapt::number_of_bits
size_t number_of_bits() const
Definition: endianness_map.h:55
or_exprt
Boolean OR.
Definition: std_expr.h:1942
lower_byte_update_array_vector_non_const
static exprt lower_byte_update_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
Definition: byte_operators.cpp:1564
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
lower_byte_update_struct
static exprt lower_byte_update_struct(const byte_update_exprt &src, const struct_typet &struct_type, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a struct typed operand using the byte array value_as_byte_array as update ...
Definition: byte_operators.cpp:1825
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
failed
static bool failed(bool error_indicator)
Definition: symtab2gb_parse_options.cpp:36
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:120
boundst
Definition: byte_operators.cpp:32
lower_byte_update_array_vector_unbounded
static exprt lower_byte_update_array_vector_unbounded(const byte_update_exprt &src, const typet &subtype, const exprt &subtype_size, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const exprt &initial_bytes, const exprt &first_index, const exprt &first_update_value, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
Definition: byte_operators.cpp:1438
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
endianness_mapt::map_bit
size_t map_bit(size_t bit) const
Definition: endianness_map.h:47
lower_byte_operators
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
Definition: byte_operators.cpp:2318
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2552
bv_to_union_expr
static union_exprt bv_to_union_expr(const exprt &bitvector_expr, const union_typet &union_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a union-typed expression.
Definition: byte_operators.cpp:112
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:935
bv_to_complex_expr
static complex_exprt bv_to_complex_expr(const exprt &bitvector_expr, const complex_typet &complex_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a complex-typed expression.
Definition: byte_operators.cpp:257
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2557
index_exprt::index
exprt & index()
Definition: std_expr.h:1268
index_exprt::array
exprt & array()
Definition: std_expr.h:1258
irept::swap
void swap(irept &irep)
Definition: irep.h:453
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:468
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
instantiate_byte_array
static exprt::operandst instantiate_byte_array(const exprt &src, std::size_t lower_bound, std::size_t upper_bound, const namespacet &ns)
Build the individual bytes to be used in an update.
Definition: byte_operators.cpp:396
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1621
union_typet
The union type.
Definition: c_types.h:112
bitand_exprt
Bit-wise AND.
Definition: bitvector_expr.h:195
lower_byte_update_union
static exprt lower_byte_update_union(const byte_update_exprt &src, const union_typet &union_type, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a union typed operand using the byte array value_as_byte_array as update v...
Definition: byte_operators.cpp:2014
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:243
minus_exprt
Binary minus.
Definition: std_expr.h:889
lower_byte_extract_complex
static optionalt< exprt > lower_byte_extract_complex(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const namespacet &ns)
Rewrite a byte extraction of a complex-typed result to byte extraction of the individual components t...
Definition: byte_operators.cpp:956
map_bounds
static boundst map_bounds(const endianness_mapt &endianness_map, std::size_t lower_bound, std::size_t upper_bound)
Map bit boundaries according to endianness.
Definition: byte_operators.cpp:38
endianness_map.h
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: bitvector_expr.h:82
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:44
to_concatenation_expr
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: bitvector_expr.h:618
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
expr_util.h
Deprecated expression utility functions.
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
byte_update_exprt::value
const exprt & value() const
Definition: byte_operators.h:110
array_typet
Arrays with given size.
Definition: std_types.h:757
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:826
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
bv_to_array_expr
static array_exprt bv_to_array_expr(const exprt &bitvector_expr, const array_typet &array_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an array-typed expression.
Definition: byte_operators.cpp:159
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
PRECONDITION_WITH_DIAGNOSTICS
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:465
unpack_rec
static exprt unpack_rec(const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns, bool unpack_byte_array=false)
Rewrite an object into its individual bytes.
Definition: byte_operators.cpp:778
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:53
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1734
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:195
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:144
endianness_mapt
Maps a big-endian offset to a little-endian offset.
Definition: endianness_map.h:31
unpack_struct
static array_exprt unpack_struct(const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
Rewrite a struct-typed expression into its individual bytes.
Definition: byte_operators.cpp:609
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:994
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:278
boundst::ub
std::size_t ub
Definition: byte_operators.cpp:34
boundst::lb
std::size_t lb
Definition: byte_operators.cpp:33
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: bitvector_expr.h:430
exprt::operands
operandst & operands()
Definition: expr.h:96
index_exprt
Array index operator.
Definition: std_expr.h:1242
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3013
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:760
member_offset_expr
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:219
byte_update_exprt::op
const exprt & op() const
Definition: byte_operators.h:108
lower_byte_update_byte_array_vector_non_const
static exprt lower_byte_update_byte_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte-array typed expression value_as_by...
Definition: byte_operators.cpp:1316
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1381
c_types.h
process_bit_fields
static void process_bit_fields(exprt::operandst &&bit_fields, std::size_t total_bits, exprt::operandst &dest, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
Extract bytes from a sequence of bitvector-typed elements.
Definition: byte_operators.cpp:579
can_cast_type< bitvector_typet >
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:860
bitvector_expr.h
API to expression classes for bitvectors.
bv_typet
Fixed-width bit-vector without numerical interpretation.
Definition: bitvector_types.h:49
mod_exprt
Modulo.
Definition: std_expr.h:1049
shl_exprt
Left shift.
Definition: bitvector_expr.h:295
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700