CBMC
lower_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 "arith_tools.h"
10 #include "bitvector_expr.h"
11 #include "byte_operators.h"
12 #include "c_types.h"
13 #include "endianness_map.h"
14 #include "expr_util.h"
15 #include "namespace.h"
16 #include "narrow.h"
17 #include "pointer_offset_size.h"
18 #include "simplify_expr.h"
19 #include "string_constant.h"
20 
21 #include <algorithm>
22 
23 static exprt bv_to_expr(
24  const exprt &bitvector_expr,
25  const typet &target_type,
26  const endianness_mapt &endianness_map,
27  const namespacet &ns);
28 
29 struct boundst
30 {
31  std::size_t lb;
32  std::size_t ub;
33 };
34 
37  const endianness_mapt &endianness_map,
38  std::size_t lower_bound,
39  std::size_t upper_bound)
40 {
41  boundst result;
42  result.lb = lower_bound;
43  result.ub = upper_bound;
44 
45  if(result.ub < endianness_map.number_of_bits())
46  {
47  result.lb = endianness_map.map_bit(result.lb);
48  result.ub = endianness_map.map_bit(result.ub);
49 
50  // big-endian bounds need swapping
51  if(result.ub < result.lb)
52  std::swap(result.lb, result.ub);
53  }
54 
55  return result;
56 }
57 
59 bitvector_typet adjust_width(const typet &src, std::size_t new_width)
60 {
61  if(src.id() == ID_unsignedbv)
62  return unsignedbv_typet(new_width);
63  else if(src.id() == ID_signedbv)
64  return signedbv_typet(new_width);
65  else if(src.id() == ID_bv)
66  return bv_typet(new_width);
67  else if(src.id() == ID_c_enum) // we use the underlying type
68  return adjust_width(to_c_enum_type(src).underlying_type(), new_width);
69  else if(src.id() == ID_c_bit_field)
70  return c_bit_field_typet(
71  to_c_bit_field_type(src).underlying_type(), new_width);
72  else
73  PRECONDITION(false);
74 }
75 
79  const exprt &bitvector_expr,
80  const struct_typet &struct_type,
81  const endianness_mapt &endianness_map,
82  const namespacet &ns)
83 {
84  const struct_typet::componentst &components = struct_type.components();
85 
86  exprt::operandst operands;
87  operands.reserve(components.size());
88  std::size_t member_offset_bits = 0;
89  for(const auto &comp : components)
90  {
91  const auto component_bits_opt = pointer_offset_bits(comp.type(), ns);
92  std::size_t component_bits;
93  if(component_bits_opt.has_value())
94  component_bits = numeric_cast_v<std::size_t>(*component_bits_opt);
95  else
96  component_bits = to_bitvector_type(bitvector_expr.type()).get_width() -
98 
99  if(component_bits == 0)
100  {
101  operands.push_back(
102  bv_to_expr(bitvector_expr, comp.type(), endianness_map, ns));
103  continue;
104  }
105 
106  const auto bounds = map_bounds(
107  endianness_map,
109  member_offset_bits + component_bits - 1);
110  bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits);
111  PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
112  operands.push_back(bv_to_expr(
113  extractbits_exprt{bitvector_expr, bounds.lb, std::move(type)},
114  comp.type(),
115  endianness_map,
116  ns));
117 
118  if(component_bits_opt.has_value())
119  member_offset_bits += component_bits;
120  }
121 
122  return struct_exprt{std::move(operands), struct_type};
123 }
124 
128  const exprt &bitvector_expr,
129  const union_typet &union_type,
130  const endianness_mapt &endianness_map,
131  const namespacet &ns)
132 {
133  const union_typet::componentst &components = union_type.components();
134 
135  if(components.empty())
136  return empty_union_exprt{union_type};
137 
138  const auto widest_member = union_type.find_widest_union_component(ns);
139 
140  std::size_t component_bits;
141  if(widest_member.has_value())
142  component_bits = numeric_cast_v<std::size_t>(widest_member->second);
143  else
144  component_bits = to_bitvector_type(bitvector_expr.type()).get_width();
145 
146  if(component_bits == 0)
147  {
148  return union_exprt{
149  components.front().get_name(),
150  bv_to_expr(bitvector_expr, components.front().type(), endianness_map, ns),
151  union_type};
152  }
153 
154  const auto bounds = map_bounds(endianness_map, 0, component_bits - 1);
155  bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits);
156  const irep_idt &component_name = widest_member.has_value()
157  ? widest_member->first.get_name()
158  : components.front().get_name();
159  const typet &component_type = widest_member.has_value()
160  ? widest_member->first.type()
161  : components.front().type();
162  PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
163  return union_exprt{
164  component_name,
165  bv_to_expr(
166  extractbits_exprt{bitvector_expr, bounds.lb, std::move(type)},
167  component_type,
168  endianness_map,
169  ns),
170  union_type};
171 }
172 
176  const exprt &bitvector_expr,
177  const array_typet &array_type,
178  const endianness_mapt &endianness_map,
179  const namespacet &ns)
180 {
181  auto num_elements = numeric_cast<std::size_t>(array_type.size());
182  auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
183 
184  const std::size_t total_bits =
185  to_bitvector_type(bitvector_expr.type()).get_width();
186  if(!num_elements.has_value())
187  {
188  if(!subtype_bits.has_value() || *subtype_bits == 0)
189  num_elements = total_bits;
190  else
191  num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
192  }
194  !num_elements.has_value() || !subtype_bits.has_value() ||
195  *subtype_bits * *num_elements == total_bits,
196  "subtype width times array size should be total bitvector width");
197 
198  exprt::operandst operands;
199  operands.reserve(*num_elements);
200  for(std::size_t i = 0; i < *num_elements; ++i)
201  {
202  if(subtype_bits.has_value())
203  {
204  const std::size_t subtype_bits_int =
205  numeric_cast_v<std::size_t>(*subtype_bits);
206  const auto bounds = map_bounds(
207  endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
208  bitvector_typet type =
209  adjust_width(bitvector_expr.type(), subtype_bits_int);
210  PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
211  operands.push_back(bv_to_expr(
212  extractbits_exprt{bitvector_expr, bounds.lb, std::move(type)},
213  array_type.element_type(),
214  endianness_map,
215  ns));
216  }
217  else
218  {
219  operands.push_back(bv_to_expr(
220  bitvector_expr, array_type.element_type(), endianness_map, ns));
221  }
222  }
223 
224  return array_exprt{std::move(operands), array_type};
225 }
226 
230  const exprt &bitvector_expr,
231  const vector_typet &vector_type,
232  const endianness_mapt &endianness_map,
233  const namespacet &ns)
234 {
235  const std::size_t num_elements =
236  numeric_cast_v<std::size_t>(vector_type.size());
237  auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
239  !subtype_bits.has_value() ||
240  *subtype_bits * num_elements ==
241  to_bitvector_type(bitvector_expr.type()).get_width(),
242  "subtype width times vector size should be total bitvector width");
243 
244  exprt::operandst operands;
245  operands.reserve(num_elements);
246  for(std::size_t i = 0; i < num_elements; ++i)
247  {
248  if(subtype_bits.has_value())
249  {
250  const std::size_t subtype_bits_int =
251  numeric_cast_v<std::size_t>(*subtype_bits);
252  const auto bounds = map_bounds(
253  endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
254  bitvector_typet type =
255  adjust_width(bitvector_expr.type(), subtype_bits_int);
256  PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
257  operands.push_back(bv_to_expr(
258  extractbits_exprt{bitvector_expr, bounds.lb, std::move(type)},
259  vector_type.element_type(),
260  endianness_map,
261  ns));
262  }
263  else
264  {
265  operands.push_back(bv_to_expr(
266  bitvector_expr, vector_type.element_type(), endianness_map, ns));
267  }
268  }
269 
270  return vector_exprt{std::move(operands), vector_type};
271 }
272 
276  const exprt &bitvector_expr,
277  const complex_typet &complex_type,
278  const endianness_mapt &endianness_map,
279  const namespacet &ns)
280 {
281  const std::size_t total_bits =
282  to_bitvector_type(bitvector_expr.type()).get_width();
283  const auto subtype_bits_opt = pointer_offset_bits(complex_type.subtype(), ns);
284  std::size_t subtype_bits;
285  if(subtype_bits_opt.has_value())
286  {
287  subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
289  subtype_bits * 2 == total_bits,
290  "subtype width should be half of the total bitvector width");
291  }
292  else
293  subtype_bits = total_bits / 2;
294 
295  const auto bounds_real = map_bounds(endianness_map, 0, subtype_bits - 1);
296  const auto bounds_imag =
297  map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
298 
299  const bitvector_typet type =
300  adjust_width(bitvector_expr.type(), subtype_bits);
301 
302  PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
303  return complex_exprt{
304  bv_to_expr(
305  extractbits_exprt{bitvector_expr, bounds_real.lb, type},
306  complex_type.subtype(),
307  endianness_map,
308  ns),
309  bv_to_expr(
310  extractbits_exprt{bitvector_expr, bounds_imag.lb, type},
311  complex_type.subtype(),
312  endianness_map,
313  ns),
314  complex_type};
315 }
316 
331  const exprt &bitvector_expr,
332  const typet &target_type,
333  const endianness_mapt &endianness_map,
334  const namespacet &ns)
335 {
337 
338  if(target_type.id() == ID_floatbv)
339  {
340  std::size_t width = to_bitvector_type(bitvector_expr.type()).get_width();
341  exprt bv_expr =
342  typecast_exprt::conditional_cast(bitvector_expr, bv_typet{width});
343  return simplify_expr(
344  typecast_exprt::conditional_cast(bv_expr, target_type), ns);
345  }
346  else if(
347  can_cast_type<bitvector_typet>(target_type) ||
348  target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
349  target_type.id() == ID_string ||
350  (target_type.id() == ID_bool &&
351  to_bitvector_type(bitvector_expr.type()).get_width() == 1))
352  {
353  return simplify_expr(
354  typecast_exprt::conditional_cast(bitvector_expr, target_type), ns);
355  }
356  else if(target_type.id() == ID_struct)
357  {
358  return bv_to_struct_expr(
359  bitvector_expr, to_struct_type(target_type), endianness_map, ns);
360  }
361  else if(target_type.id() == ID_struct_tag)
362  {
364  bitvector_expr,
365  ns.follow_tag(to_struct_tag_type(target_type)),
366  endianness_map,
367  ns);
368  result.type() = target_type;
369  return std::move(result);
370  }
371  else if(target_type.id() == ID_union)
372  {
373  return bv_to_union_expr(
374  bitvector_expr, to_union_type(target_type), endianness_map, ns);
375  }
376  else if(target_type.id() == ID_union_tag)
377  {
378  exprt result = bv_to_union_expr(
379  bitvector_expr,
380  ns.follow_tag(to_union_tag_type(target_type)),
381  endianness_map,
382  ns);
383  result.type() = target_type;
384  return result;
385  }
386  else if(target_type.id() == ID_array)
387  {
388  return bv_to_array_expr(
389  bitvector_expr, to_array_type(target_type), endianness_map, ns);
390  }
391  else if(target_type.id() == ID_vector)
392  {
393  return bv_to_vector_expr(
394  bitvector_expr, to_vector_type(target_type), endianness_map, ns);
395  }
396  else if(target_type.id() == ID_complex)
397  {
398  return bv_to_complex_expr(
399  bitvector_expr, to_complex_type(target_type), endianness_map, ns);
400  }
401  else
402  {
404  false, "bv_to_expr does not yet support ", target_type.id_string());
405  }
406 }
407 
408 static exprt unpack_rec(
409  const exprt &src,
410  bool little_endian,
411  const std::optional<mp_integer> &offset_bytes,
412  const std::optional<mp_integer> &max_bytes,
413  const std::size_t bits_per_byte,
414  const namespacet &ns,
415  bool unpack_byte_array = false);
416 
425  const exprt &src,
426  std::size_t lower_bound,
427  std::size_t upper_bound,
428  const std::size_t bits_per_byte,
429  const namespacet &ns)
430 {
431  PRECONDITION(lower_bound <= upper_bound);
432 
433  if(src.id() == ID_array)
434  {
435  PRECONDITION(upper_bound <= src.operands().size());
436  return exprt::operandst{
437  src.operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
438  src.operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
439  }
440 
441  const typet &element_type = src.type().id() == ID_array
442  ? to_array_type(src.type()).element_type()
443  : to_vector_type(src.type()).element_type();
444  const typet index_type = src.type().id() == ID_array
445  ? to_array_type(src.type()).index_type()
446  : to_vector_type(src.type()).index_type();
447  PRECONDITION(
448  can_cast_type<bitvector_typet>(element_type) &&
449  to_bitvector_type(element_type).get_width() == bits_per_byte);
450  exprt::operandst bytes;
451  bytes.reserve(upper_bound - lower_bound);
452  for(std::size_t i = lower_bound; i < upper_bound; ++i)
453  {
454  const index_exprt idx{src, from_integer(i, index_type)};
455  bytes.push_back(simplify_expr(idx, ns));
456  }
457  return bytes;
458 }
459 
469  const exprt &src,
470  std::size_t el_bytes,
471  bool little_endian,
472  const std::size_t bits_per_byte,
473  const namespacet &ns)
474 {
475  const typet index_type = src.type().id() == ID_array
476  ? to_array_type(src.type()).index_type()
477  : to_vector_type(src.type()).index_type();
478 
479  // TODO we either need a symbol table here or make array comprehensions
480  // introduce a scope
481  static std::size_t array_comprehension_index_counter = 0;
482  ++array_comprehension_index_counter;
483  symbol_exprt array_comprehension_index{
484  "$array_comprehension_index_a_v" +
485  std::to_string(array_comprehension_index_counter),
486  index_type};
487 
488  index_exprt element{
489  src,
490  div_exprt{array_comprehension_index, from_integer(el_bytes, index_type)}};
491 
492  exprt sub =
493  unpack_rec(element, little_endian, {}, {}, bits_per_byte, ns, false);
494  exprt::operandst sub_operands =
495  instantiate_byte_array(sub, 0, el_bytes, bits_per_byte, ns);
496 
497  exprt body = sub_operands.front();
498  const mod_exprt offset{
499  array_comprehension_index,
500  from_integer(el_bytes, array_comprehension_index.type())};
501  for(std::size_t i = 1; i < el_bytes; ++i)
502  {
503  body = if_exprt{
504  equal_exprt{offset, from_integer(i, array_comprehension_index.type())},
505  sub_operands[i],
506  body};
507  }
508 
509  const exprt array_vector_size = src.type().id() == ID_vector
510  ? to_vector_type(src.type()).size()
511  : to_array_type(src.type()).size();
512 
514  std::move(array_comprehension_index),
515  std::move(body),
516  array_typet{
517  bv_typet{bits_per_byte},
518  mult_exprt{
519  array_vector_size, from_integer(el_bytes, array_vector_size.type())}}};
520 }
521 
538  const exprt &src,
539  const std::optional<mp_integer> &src_size,
540  const mp_integer &element_bits,
541  bool little_endian,
542  const std::optional<mp_integer> &offset_bytes,
543  const std::optional<mp_integer> &max_bytes,
544  const std::size_t bits_per_byte,
545  const namespacet &ns)
546 {
547  const std::size_t el_bytes = numeric_cast_v<std::size_t>(
548  (element_bits + bits_per_byte - 1) / bits_per_byte);
549 
550  if(!src_size.has_value() && !max_bytes.has_value())
551  {
553  el_bytes > 0 && element_bits % bits_per_byte == 0,
554  "unpacking of arrays with non-byte-aligned elements is not supported");
556  src, el_bytes, little_endian, bits_per_byte, ns);
557  }
558 
559  exprt::operandst byte_operands;
560  mp_integer first_element = 0;
561 
562  // refine the number of elements to extract in case the element width is known
563  // and a multiple of bytes; otherwise we will expand the entire array/vector
564  std::optional<mp_integer> num_elements = src_size;
565  if(element_bits > 0 && element_bits % bits_per_byte == 0)
566  {
567  if(!num_elements.has_value())
568  {
569  // turn bytes into elements, rounding up
570  num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
571  }
572 
573  if(offset_bytes.has_value())
574  {
575  // compute offset as number of elements
576  first_element = *offset_bytes / el_bytes;
577  // insert offset_bytes-many nil bytes into the output array
578  byte_operands.resize(
579  numeric_cast_v<std::size_t>(std::min(
580  *offset_bytes - (*offset_bytes % el_bytes),
581  *num_elements * el_bytes)),
582  bv_typet{bits_per_byte}.all_zeros_expr());
583  }
584  }
585 
586  // the maximum number of bytes is an upper bound in case the size of the
587  // array/vector is unknown; if element_bits was usable above this will
588  // have been turned into a number of elements already
589  if(!num_elements)
590  num_elements = *max_bytes;
591 
592  const exprt src_simp = simplify_expr(src, ns);
593  const typet index_type = src_simp.type().id() == ID_array
594  ? to_array_type(src_simp.type()).index_type()
595  : to_vector_type(src_simp.type()).index_type();
596 
597  for(mp_integer i = first_element; i < *num_elements; ++i)
598  {
599  exprt element;
600 
601  if(
602  (src_simp.id() == ID_array || src_simp.id() == ID_vector) &&
603  i < src_simp.operands().size())
604  {
605  const std::size_t index_int = numeric_cast_v<std::size_t>(i);
606  element = src_simp.operands()[index_int];
607  }
608  else
609  {
610  element = index_exprt(src_simp, from_integer(i, index_type));
611  }
612 
613  // recursively unpack each element so that we eventually just have an array
614  // of bytes left
615 
616  const std::optional<mp_integer> element_max_bytes =
617  max_bytes
618  ? std::min(mp_integer{el_bytes}, *max_bytes - byte_operands.size())
619  : std::optional<mp_integer>{};
620  const std::size_t element_max_bytes_int =
621  element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
622  : el_bytes;
623 
624  exprt sub = unpack_rec(
625  element, little_endian, {}, element_max_bytes, bits_per_byte, ns, true);
626  exprt::operandst sub_operands =
627  instantiate_byte_array(sub, 0, element_max_bytes_int, bits_per_byte, ns);
628  byte_operands.insert(
629  byte_operands.end(), sub_operands.begin(), sub_operands.end());
630 
631  if(max_bytes && byte_operands.size() >= *max_bytes)
632  break;
633  }
634 
635  const std::size_t size = byte_operands.size();
636  return array_exprt(
637  std::move(byte_operands),
638  array_typet{bv_typet{bits_per_byte}, from_integer(size, size_type())});
639 }
640 
652 static void process_bit_fields(
653  exprt::operandst &&bit_fields,
654  std::size_t total_bits,
655  exprt::operandst &dest,
656  bool little_endian,
657  const std::optional<mp_integer> &offset_bytes,
658  const std::optional<mp_integer> &max_bytes,
659  const std::size_t bits_per_byte,
660  const namespacet &ns)
661 {
662  const concatenation_exprt concatenation{
663  std::move(bit_fields), bv_typet{total_bits}};
664 
665  exprt sub = unpack_rec(
666  concatenation,
667  little_endian,
668  offset_bytes,
669  max_bytes,
670  bits_per_byte,
671  ns,
672  true);
673 
674  dest.insert(
675  dest.end(),
676  std::make_move_iterator(sub.operands().begin()),
677  std::make_move_iterator(sub.operands().end()));
678 }
679 
691  const exprt &src,
692  bool little_endian,
693  const std::optional<mp_integer> &offset_bytes,
694  const std::optional<mp_integer> &max_bytes,
695  const std::size_t bits_per_byte,
696  const namespacet &ns)
697 {
698  const struct_typet &struct_type =
699  src.type().id() == ID_struct_tag
700  ? ns.follow_tag(to_struct_tag_type(src.type()))
701  : to_struct_type(src.type());
702  const struct_typet::componentst &components = struct_type.components();
703 
704  std::optional<mp_integer> offset_in_member;
705  std::optional<mp_integer> max_bytes_left;
706  std::optional<std::pair<exprt::operandst, std::size_t>> bit_fields;
707 
709  exprt::operandst byte_operands;
710  for(auto it = components.begin(); it != components.end(); ++it)
711  {
712  const auto &comp = *it;
713  auto component_bits = pointer_offset_bits(comp.type(), ns);
714 
715  // We can only handle a member of unknown width when it is the last member
716  // and is byte-aligned. Members of unknown width in the middle would leave
717  // us with unknown alignment of subsequent members, and queuing them up as
718  // bit fields is not possible either as the total width of the concatenation
719  // could not be determined.
721  component_bits.has_value() ||
722  (std::next(it) == components.end() && !bit_fields.has_value()),
723  "members of non-constant width should come last in a struct");
724 
725  member_exprt member(src, comp.get_name(), comp.type());
726  if(src.id() == ID_struct)
727  simplify(member, ns);
728 
729  // Is it a byte-aligned member?
730  if(member_offset_bits % bits_per_byte == 0)
731  {
732  if(bit_fields.has_value())
733  {
735  std::move(bit_fields->first),
736  bit_fields->second,
737  byte_operands,
738  little_endian,
739  offset_in_member,
740  max_bytes_left,
741  bits_per_byte,
742  ns);
743  bit_fields.reset();
744  }
745 
746  if(offset_bytes.has_value())
747  {
748  offset_in_member = *offset_bytes - member_offset_bits / bits_per_byte;
749  // if the offset is negative, offset_in_member remains unset, which has
750  // the same effect as setting it to zero
751  if(*offset_in_member < 0)
752  offset_in_member.reset();
753  }
754 
755  if(max_bytes.has_value())
756  {
757  max_bytes_left = *max_bytes - member_offset_bits / bits_per_byte;
758  if(*max_bytes_left < 0)
759  break;
760  }
761  }
762 
763  if(
764  member_offset_bits % bits_per_byte != 0 ||
765  (component_bits.has_value() && *component_bits % bits_per_byte != 0))
766  {
767  if(!bit_fields.has_value())
768  bit_fields = std::make_pair(exprt::operandst{}, std::size_t{0});
769 
770  const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
771  bit_fields->first.insert(
772  little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
773  typecast_exprt::conditional_cast(member, bv_typet{bits_int}));
774  bit_fields->second += bits_int;
775 
776  member_offset_bits += *component_bits;
777 
778  continue;
779  }
780 
781  INVARIANT(
782  !bit_fields.has_value(),
783  "all preceding members should have been processed");
784 
785  if(
786  component_bits.has_value() && offset_in_member.has_value() &&
787  *offset_in_member * bits_per_byte >= *component_bits)
788  {
789  // we won't actually need this component, fill in zeros instead of
790  // computing an unpacking
791  byte_operands.resize(
792  byte_operands.size() +
793  numeric_cast_v<std::size_t>(*component_bits / bits_per_byte),
794  bv_typet{bits_per_byte}.all_zeros_expr());
795  }
796  else
797  {
798  exprt sub = unpack_rec(
799  member,
800  little_endian,
801  offset_in_member,
802  max_bytes_left,
803  bits_per_byte,
804  ns,
805  true);
806 
807  byte_operands.insert(
808  byte_operands.end(),
809  std::make_move_iterator(sub.operands().begin()),
810  std::make_move_iterator(sub.operands().end()));
811  }
812 
813  if(component_bits.has_value())
814  member_offset_bits += *component_bits;
815  }
816 
817  // any remaining bit fields?
818  if(bit_fields.has_value())
819  {
821  std::move(bit_fields->first),
822  bit_fields->second,
823  byte_operands,
824  little_endian,
825  offset_in_member,
826  max_bytes_left,
827  bits_per_byte,
828  ns);
829  }
830 
831  const std::size_t size = byte_operands.size();
832  return array_exprt{
833  std::move(byte_operands),
834  array_typet{bv_typet{bits_per_byte}, from_integer(size, size_type())}};
835 }
836 
844  const exprt &src,
845  bool little_endian,
846  const std::size_t bits_per_byte,
847  const namespacet &ns)
848 {
849  const complex_typet &complex_type = to_complex_type(src.type());
850  const typet &subtype = complex_type.subtype();
851 
852  auto subtype_bits = pointer_offset_bits(subtype, ns);
853  CHECK_RETURN(subtype_bits.has_value());
854  CHECK_RETURN(*subtype_bits % bits_per_byte == 0);
855 
856  exprt sub_real = unpack_rec(
857  complex_real_exprt{src},
858  little_endian,
859  mp_integer{0},
860  *subtype_bits / bits_per_byte,
861  bits_per_byte,
862  ns,
863  true);
864  exprt::operandst byte_operands = std::move(sub_real.operands());
865 
866  exprt sub_imag = unpack_rec(
867  complex_imag_exprt{src},
868  little_endian,
869  mp_integer{0},
870  *subtype_bits / bits_per_byte,
871  bits_per_byte,
872  ns,
873  true);
874  byte_operands.insert(
875  byte_operands.end(),
876  std::make_move_iterator(sub_imag.operands().begin()),
877  std::make_move_iterator(sub_imag.operands().end()));
878 
879  const std::size_t size = byte_operands.size();
880  return array_exprt{
881  std::move(byte_operands),
882  array_typet{bv_typet{bits_per_byte}, from_integer(size, size_type())}};
883 }
884 
895 // array of bytes
898  const exprt &src,
899  bool little_endian,
900  const std::optional<mp_integer> &offset_bytes,
901  const std::optional<mp_integer> &max_bytes,
902  const std::size_t bits_per_byte,
903  const namespacet &ns,
904  bool unpack_byte_array)
905 {
906  if(src.type().id() == ID_array)
907  {
908  const array_typet &array_type = to_array_type(src.type());
909  const typet &subtype = array_type.element_type();
910 
911  auto element_bits = pointer_offset_bits(subtype, ns);
912  CHECK_RETURN(element_bits.has_value());
913 
914  if(
915  !unpack_byte_array && *element_bits == bits_per_byte &&
917  {
918  return src;
919  }
920 
921  const auto constant_size_opt = numeric_cast<mp_integer>(array_type.size());
922  return unpack_array_vector(
923  src,
924  constant_size_opt,
925  *element_bits,
926  little_endian,
927  offset_bytes,
928  max_bytes,
929  bits_per_byte,
930  ns);
931  }
932  else if(src.type().id() == ID_vector)
933  {
934  const vector_typet &vector_type = to_vector_type(src.type());
935  const typet &subtype = vector_type.element_type();
936 
937  auto element_bits = pointer_offset_bits(subtype, ns);
938  CHECK_RETURN(element_bits.has_value());
939 
940  if(
941  !unpack_byte_array && *element_bits == bits_per_byte &&
943  {
944  return src;
945  }
946 
947  return unpack_array_vector(
948  src,
949  numeric_cast_v<mp_integer>(vector_type.size()),
950  *element_bits,
951  little_endian,
952  offset_bytes,
953  max_bytes,
954  bits_per_byte,
955  ns);
956  }
957  else if(src.type().id() == ID_complex)
958  {
959  return unpack_complex(src, little_endian, bits_per_byte, ns);
960  }
961  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
962  {
963  return unpack_struct(
964  src, little_endian, offset_bytes, max_bytes, bits_per_byte, ns);
965  }
966  else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
967  {
968  const union_typet &union_type =
969  src.type().id() == ID_union_tag
970  ? ns.follow_tag(to_union_tag_type(src.type()))
971  : to_union_type(src.type());
972 
973  const auto widest_member = union_type.find_widest_union_component(ns);
974 
975  if(widest_member.has_value())
976  {
977  member_exprt member{
978  src, widest_member->first.get_name(), widest_member->first.type()};
979  return unpack_rec(
980  member,
981  little_endian,
982  offset_bytes,
983  widest_member->second,
984  bits_per_byte,
985  ns,
986  true);
987  }
988  else if(!union_type.components().empty())
989  {
990  member_exprt member{src, union_type.components().front()};
991  return unpack_rec(
992  member,
993  little_endian,
994  offset_bytes,
995  max_bytes,
996  bits_per_byte,
997  ns,
998  true);
999  }
1000  }
1001  else if(src.type().id() == ID_pointer)
1002  {
1003  return unpack_rec(
1005  little_endian,
1006  offset_bytes,
1007  max_bytes,
1008  bits_per_byte,
1009  ns,
1010  unpack_byte_array);
1011  }
1012  else if(src.id() == ID_string_constant)
1013  {
1014  return unpack_rec(
1016  little_endian,
1017  offset_bytes,
1018  max_bytes,
1019  bits_per_byte,
1020  ns,
1021  unpack_byte_array);
1022  }
1023  else if(src.is_constant() && src.type().id() == ID_string)
1024  {
1025  return unpack_rec(
1026  string_constantt(to_constant_expr(src).get_value()).to_array_expr(),
1027  little_endian,
1028  offset_bytes,
1029  max_bytes,
1030  bits_per_byte,
1031  ns,
1032  unpack_byte_array);
1033  }
1034  else if(src.type().id() != ID_empty)
1035  {
1036  // a basic type; we turn that into extractbits while considering
1037  // endianness
1038  auto bits_opt = pointer_offset_bits(src.type(), ns);
1039  DATA_INVARIANT(bits_opt.has_value(), "basic type should have a fixed size");
1040 
1041  const mp_integer total_bits = *bits_opt;
1042  mp_integer last_bit = total_bits;
1043  mp_integer bit_offset = 0;
1044 
1045  if(max_bytes.has_value())
1046  {
1047  const auto max_bits = *max_bytes * bits_per_byte;
1048  if(little_endian)
1049  {
1050  last_bit = std::min(last_bit, max_bits);
1051  }
1052  else
1053  {
1054  bit_offset = std::max(mp_integer{0}, last_bit - max_bits);
1055  }
1056  }
1057 
1058  auto const src_as_bitvector = typecast_exprt::conditional_cast(
1059  src, bv_typet{numeric_cast_v<std::size_t>(total_bits)});
1060  auto const byte_type = bv_typet{bits_per_byte};
1061  exprt::operandst byte_operands;
1062  array_typet array_type{
1063  bv_typet{bits_per_byte}, from_integer(0, size_type())};
1064 
1065  for(; bit_offset < last_bit; bit_offset += bits_per_byte)
1066  {
1067  PRECONDITION(
1068  pointer_offset_bits(src_as_bitvector.type(), ns).has_value());
1069  extractbits_exprt extractbits(
1070  src_as_bitvector,
1071  from_integer(bit_offset, array_type.index_type()),
1072  byte_type);
1073 
1074  // endianness_mapt should be the point of reference for mapping out
1075  // endianness, but we need to work on elements here instead of
1076  // individual bits
1077  if(little_endian)
1078  byte_operands.push_back(extractbits);
1079  else
1080  byte_operands.insert(byte_operands.begin(), extractbits);
1081  }
1082 
1083  const std::size_t size = byte_operands.size();
1084  array_type.size() = from_integer(size, size_type());
1085  return array_exprt{std::move(byte_operands), std::move(array_type)};
1086  }
1087 
1088  return array_exprt(
1089  {}, array_typet{bv_typet{bits_per_byte}, from_integer(0, size_type())});
1090 }
1091 
1103  const byte_extract_exprt &src,
1104  const byte_extract_exprt &unpacked,
1105  const typet &subtype,
1106  const mp_integer &element_bits,
1107  const namespacet &ns)
1108 {
1109  std::optional<std::size_t> num_elements;
1110  if(src.type().id() == ID_array)
1111  num_elements = numeric_cast<std::size_t>(to_array_type(src.type()).size());
1112  else
1113  num_elements = numeric_cast<std::size_t>(to_vector_type(src.type()).size());
1114 
1115  if(num_elements.has_value())
1116  {
1117  exprt::operandst operands;
1118  operands.reserve(*num_elements);
1119  for(std::size_t i = 0; i < *num_elements; ++i)
1120  {
1121  plus_exprt new_offset(
1122  unpacked.offset(),
1123  from_integer(
1124  i * element_bits / src.get_bits_per_byte(),
1125  unpacked.offset().type()));
1126 
1127  byte_extract_exprt tmp(unpacked);
1128  tmp.type() = subtype;
1129  tmp.offset() = new_offset;
1130 
1131  operands.push_back(lower_byte_extract(tmp, ns));
1132  }
1133 
1134  exprt result;
1135  if(src.type().id() == ID_array)
1136  result = array_exprt{std::move(operands), to_array_type(src.type())};
1137  else
1138  result = vector_exprt{std::move(operands), to_vector_type(src.type())};
1139 
1140  return simplify_expr(result, ns);
1141  }
1142 
1143  DATA_INVARIANT(src.type().id() == ID_array, "vectors have constant size");
1144  const array_typet &array_type = to_array_type(src.type());
1145 
1146  // TODO we either need a symbol table here or make array comprehensions
1147  // introduce a scope
1148  static std::size_t array_comprehension_index_counter = 0;
1149  ++array_comprehension_index_counter;
1150  symbol_exprt array_comprehension_index{
1151  "$array_comprehension_index_a" +
1152  std::to_string(array_comprehension_index_counter),
1153  array_type.index_type()};
1154 
1155  plus_exprt new_offset{
1156  unpacked.offset(),
1158  mult_exprt{
1159  array_comprehension_index,
1160  from_integer(
1161  element_bits / src.get_bits_per_byte(),
1162  array_comprehension_index.type())},
1163  unpacked.offset().type())};
1164 
1165  byte_extract_exprt body(unpacked);
1166  body.type() = subtype;
1167  body.offset() = std::move(new_offset);
1168 
1170  std::move(array_comprehension_index),
1171  lower_byte_extract(body, ns),
1172  array_type};
1173 }
1174 
1183 static std::optional<exprt> lower_byte_extract_complex(
1184  const byte_extract_exprt &src,
1185  const byte_extract_exprt &unpacked,
1186  const namespacet &ns)
1187 {
1188  const complex_typet &complex_type = to_complex_type(src.type());
1189  const typet &subtype = complex_type.subtype();
1190 
1191  auto subtype_bits = pointer_offset_bits(subtype, ns);
1192  if(!subtype_bits.has_value() || *subtype_bits % src.get_bits_per_byte() != 0)
1193  return {};
1194 
1195  // offset remains unchanged
1196  byte_extract_exprt real{unpacked};
1197  real.type() = subtype;
1198 
1199  const plus_exprt new_offset{
1200  unpacked.offset(),
1201  from_integer(
1202  *subtype_bits / src.get_bits_per_byte(), unpacked.offset().type())};
1203  byte_extract_exprt imag{unpacked};
1204  imag.type() = subtype;
1205  imag.offset() = simplify_expr(new_offset, ns);
1206 
1207  return simplify_expr(
1208  complex_exprt{
1209  lower_byte_extract(real, ns), lower_byte_extract(imag, ns), complex_type},
1210  ns);
1211 }
1212 
1216 {
1217  // General notes about endianness and the bit-vector conversion:
1218  // A single byte with value 0b10001000 is stored (in irept) as
1219  // exactly this string literal, and its bit-vector encoding will be
1220  // bvt bv={0,0,0,1,0,0,0,1}, i.e., bv[0]==0 and bv[7]==1
1221  //
1222  // A multi-byte value like x=256 would be:
1223  // - little-endian storage: ((char*)&x)[0]==0, ((char*)&x)[1]==1
1224  // - big-endian storage: ((char*)&x)[0]==1, ((char*)&x)[1]==0
1225  // - irept representation: 0000000100000000
1226  // - bvt: {0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0}
1227  // <... 8bits ...> <... 8bits ...>
1228  //
1229  // An array {0, 1} will be encoded as bvt bv={0,1}, i.e., bv[1]==1
1230  // concatenation(0, 1) will yield a bvt bv={1,0}, i.e., bv[1]==0
1231  //
1232  // The semantics of byte_extract(endianness, op, offset, T) is:
1233  // interpret ((char*)&op)+offset as the endianness-ordered storage
1234  // of an object of type T at address ((char*)&op)+offset
1235  // For some T x, byte_extract(endianness, x, 0, T) must yield x.
1236  //
1237  // byte_extract for a composite type T or an array will interpret
1238  // the individual subtypes with suitable endianness; the overall
1239  // order of components is not affected by endianness.
1240  //
1241  // Examples:
1242  // unsigned char A[4];
1243  // byte_extract_little_endian(A, 0, unsigned short) requests that
1244  // A[0],A[1] be interpreted as the storage of an unsigned short with
1245  // A[1] being the most-significant byte; byte_extract_big_endian for
1246  // the same operands will select A[0] as the most-significant byte.
1247  //
1248  // int A[2] = {0x01020304,0xDEADBEEF}
1249  // byte_extract_big_endian(A, 0, short) should yield 0x0102
1250  // byte_extract_little_endian(A, 0, short) should yield 0x0304
1251  // To obtain this we first compute byte arrays while taking into
1252  // account endianness:
1253  // big-endian byte representation: {01,02,03,04,DE,AB,BE,EF}
1254  // little-endian byte representation: {04,03,02,01,EF,BE,AB,DE}
1255  // We extract the relevant bytes starting from ((char*)A)+0:
1256  // big-endian: {01,02}; little-endian: {04,03}
1257  // Finally we place them in the appropriate byte order as indicated
1258  // by endianness:
1259  // big-endian: (short)concatenation(01,02)=0x0102
1260  // little-endian: (short)concatenation(03,04)=0x0304
1261 
1262  PRECONDITION(
1263  src.id() == ID_byte_extract_little_endian ||
1264  src.id() == ID_byte_extract_big_endian);
1265  const bool little_endian = src.id() == ID_byte_extract_little_endian;
1266 
1267  // determine an upper bound of the last byte we might need
1268  auto upper_bound_opt = size_of_expr(src.type(), ns);
1269  if(upper_bound_opt.has_value())
1270  {
1271  upper_bound_opt = simplify_expr(
1272  plus_exprt(
1273  upper_bound_opt.value(),
1275  src.offset(), upper_bound_opt.value().type())),
1276  ns);
1277  }
1278  else if(src.type().id() == ID_empty)
1279  upper_bound_opt = from_integer(0, size_type());
1280 
1281  const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.offset());
1282  const auto upper_bound_int_opt =
1283  numeric_cast<mp_integer>(upper_bound_opt.value_or(nil_exprt()));
1284 
1285  byte_extract_exprt unpacked(src);
1286  unpacked.op() = unpack_rec(
1287  src.op(),
1288  little_endian,
1289  lower_bound_int_opt,
1290  upper_bound_int_opt,
1291  src.get_bits_per_byte(),
1292  ns);
1293  CHECK_RETURN(
1295  .get_width() == src.get_bits_per_byte());
1296 
1297  if(src.type().id() == ID_array || src.type().id() == ID_vector)
1298  {
1299  const typet &subtype = to_type_with_subtype(src.type()).subtype();
1300 
1301  // consider ways of dealing with arrays of unknown subtype size or with a
1302  // subtype size that does not fit byte boundaries; currently we fall back to
1303  // stitching together consecutive elements down below
1304  auto element_bits = pointer_offset_bits(subtype, ns);
1305  if(
1306  element_bits.has_value() && *element_bits >= 1 &&
1307  *element_bits % src.get_bits_per_byte() == 0)
1308  {
1310  src, unpacked, subtype, *element_bits, ns);
1311  }
1312  }
1313  else if(src.type().id() == ID_complex)
1314  {
1315  auto result = lower_byte_extract_complex(src, unpacked, ns);
1316  if(result.has_value())
1317  return std::move(*result);
1318 
1319  // else fall back to generic lowering that uses bit masks, below
1320  }
1321  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
1322  {
1323  const struct_typet &struct_type =
1324  src.type().id() == ID_struct_tag
1325  ? ns.follow_tag(to_struct_tag_type(src.type()))
1326  : to_struct_type(src.type());
1327  const struct_typet::componentst &components = struct_type.components();
1328 
1329  bool failed = false;
1330  struct_exprt s({}, src.type());
1331 
1332  for(const auto &comp : components)
1333  {
1334  auto component_bits = pointer_offset_bits(comp.type(), ns);
1335 
1336  // the next member would be misaligned, abort
1337  if(
1338  !component_bits.has_value() ||
1339  *component_bits % src.get_bits_per_byte() != 0)
1340  {
1341  failed = true;
1342  break;
1343  }
1344 
1345  auto member_offset_opt =
1346  member_offset_expr(struct_type, comp.get_name(), ns);
1347 
1348  if(!member_offset_opt.has_value())
1349  {
1350  failed = true;
1351  break;
1352  }
1353 
1354  plus_exprt new_offset(
1355  unpacked.offset(),
1357  member_offset_opt.value(), unpacked.offset().type()));
1358 
1359  byte_extract_exprt tmp(unpacked);
1360  tmp.type() = comp.type();
1361  tmp.offset() = new_offset;
1362 
1363  s.add_to_operands(lower_byte_extract(tmp, ns));
1364  }
1365 
1366  if(!failed)
1367  return simplify_expr(std::move(s), ns);
1368  }
1369  else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
1370  {
1371  const union_typet &union_type =
1372  src.type().id() == ID_union_tag
1373  ? ns.follow_tag(to_union_tag_type(src.type()))
1374  : to_union_type(src.type());
1375 
1376  const auto widest_member = union_type.find_widest_union_component(ns);
1377 
1378  if(widest_member.has_value())
1379  {
1380  byte_extract_exprt tmp(unpacked);
1381  tmp.type() = widest_member->first.type();
1382 
1383  return union_exprt(
1384  widest_member->first.get_name(),
1385  lower_byte_extract(tmp, ns),
1386  src.type());
1387  }
1388  }
1389 
1390  const exprt &root = unpacked.op();
1391  const exprt &offset = unpacked.offset();
1392 
1393  std::optional<typet> subtype;
1394  std::optional<typet> index_type;
1395  if(root.type().id() == ID_vector)
1396  {
1397  subtype = to_vector_type(root.type()).element_type();
1398  index_type = to_vector_type(root.type()).index_type();
1399  }
1400  else
1401  {
1402  subtype = to_array_type(root.type()).element_type();
1403  index_type = to_array_type(root.type()).index_type();
1404  }
1405 
1406  auto subtype_bits = pointer_offset_bits(*subtype, ns);
1407 
1409  subtype_bits.has_value() && *subtype_bits == src.get_bits_per_byte(),
1410  "offset bits are byte aligned");
1411 
1412  auto size_bits = pointer_offset_bits(unpacked.type(), ns);
1413  if(!size_bits.has_value())
1414  {
1415  auto op0_bits = pointer_offset_bits(unpacked.op().type(), ns);
1416  // all cases with non-constant width should have been handled above
1418  op0_bits.has_value(),
1419  "the extracted width or the source width must be known");
1420  size_bits = op0_bits;
1421  }
1422 
1423  mp_integer num_bytes =
1424  (*size_bits) / src.get_bits_per_byte() +
1425  (((*size_bits) % src.get_bits_per_byte() == 0) ? 0 : 1);
1426 
1427  // get 'width'-many bytes, and concatenate
1428  const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
1429  exprt::operandst op;
1430  op.reserve(width_bytes);
1431 
1432  for(std::size_t i = 0; i < width_bytes; i++)
1433  {
1434  // the most significant byte comes first in the concatenation!
1435  std::size_t offset_int = little_endian ? (width_bytes - i - 1) : i;
1436 
1437  plus_exprt offset_i{
1438  from_integer(offset_int, *index_type),
1439  typecast_exprt::conditional_cast(offset, *index_type)};
1440  simplify(offset_i, ns);
1441 
1442  mp_integer index = 0;
1443  if(
1444  offset_i.is_constant() &&
1445  (root.id() == ID_array || root.id() == ID_vector) &&
1446  !to_integer(to_constant_expr(offset_i), index) &&
1447  index < root.operands().size() && index >= 0)
1448  {
1449  // offset is constant and in range
1450  op.push_back(root.operands()[numeric_cast_v<std::size_t>(index)]);
1451  }
1452  else
1453  {
1454  op.push_back(index_exprt(root, offset_i));
1455  }
1456  }
1457 
1458  if(width_bytes == 1)
1459  {
1460  return simplify_expr(
1461  typecast_exprt::conditional_cast(op.front(), src.type()), ns);
1462  }
1463  else // width_bytes>=2
1464  {
1465  concatenation_exprt concatenation(
1466  std::move(op),
1467  adjust_width(*subtype, width_bytes * src.get_bits_per_byte()));
1468 
1469  endianness_mapt map(concatenation.type(), little_endian, ns);
1470  return bv_to_expr(concatenation, src.type(), map, ns);
1471  }
1472 }
1473 
1474 static exprt lower_byte_update(
1475  const byte_update_exprt &src,
1476  const exprt &value_as_byte_array,
1477  const std::optional<exprt> &non_const_update_bound,
1478  const namespacet &ns);
1479 
1490  const byte_update_exprt &src,
1491  const typet &subtype,
1492  const exprt &value_as_byte_array,
1493  const exprt &non_const_update_bound,
1494  const namespacet &ns)
1495 {
1496  // TODO we either need a symbol table here or make array comprehensions
1497  // introduce a scope
1498  static std::size_t array_comprehension_index_counter = 0;
1499  ++array_comprehension_index_counter;
1500  symbol_exprt array_comprehension_index{
1501  "$array_comprehension_index_u_a_v" +
1502  std::to_string(array_comprehension_index_counter),
1503  to_array_type(src.type()).index_type()};
1504 
1505  binary_predicate_exprt lower_bound{
1507  array_comprehension_index, src.offset().type()),
1508  ID_lt,
1509  src.offset()};
1510  binary_predicate_exprt upper_bound{
1512  array_comprehension_index, non_const_update_bound.type()),
1513  ID_ge,
1514  plus_exprt{
1516  src.offset(), non_const_update_bound.type()),
1517  non_const_update_bound}};
1518 
1519  PRECONDITION(
1520  src.id() == ID_byte_update_little_endian ||
1521  src.id() == ID_byte_update_big_endian);
1522  const bool little_endian = src.id() == ID_byte_update_little_endian;
1523  endianness_mapt map(
1524  to_array_type(value_as_byte_array.type()).element_type(),
1525  little_endian,
1526  ns);
1527  if_exprt array_comprehension_body{
1528  or_exprt{std::move(lower_bound), std::move(upper_bound)},
1529  index_exprt{src.op(), array_comprehension_index},
1530  bv_to_expr(
1531  index_exprt{
1532  value_as_byte_array,
1533  minus_exprt{
1534  array_comprehension_index,
1536  src.offset(), array_comprehension_index.type())}},
1537  subtype,
1538  map,
1539  ns)};
1540 
1541  return simplify_expr(
1543  array_comprehension_index,
1544  std::move(array_comprehension_body),
1545  to_array_type(src.type())},
1546  ns);
1547 }
1548 
1559  const byte_update_exprt &src,
1560  const typet &subtype,
1561  const array_exprt &value_as_byte_array,
1562  const std::optional<exprt> &non_const_update_bound,
1563  const namespacet &ns)
1564 {
1565  PRECONDITION(
1566  src.id() == ID_byte_update_little_endian ||
1567  src.id() == ID_byte_update_big_endian);
1568  const bool little_endian = src.id() == ID_byte_update_little_endian;
1569 
1570  const typet index_type = src.type().id() == ID_array
1571  ? to_array_type(src.type()).index_type()
1572  : to_vector_type(src.type()).index_type();
1573 
1574  // apply 'array-update-with' num_elements times
1575  exprt result = src.op();
1576 
1577  for(std::size_t i = 0; i < value_as_byte_array.operands().size(); ++i)
1578  {
1579  const exprt &element = value_as_byte_array.operands()[i];
1580 
1581  exprt where = simplify_expr(
1582  plus_exprt{
1583  typecast_exprt::conditional_cast(src.offset(), index_type),
1584  from_integer(i, index_type)},
1585  ns);
1586 
1587  // skip elements that wouldn't change (skip over typecasts as we might have
1588  // some signed/unsigned char conversions)
1589  const exprt &e = skip_typecast(element);
1590  if(e.id() == ID_index)
1591  {
1592  const index_exprt &index_expr = to_index_expr(e);
1593  if(index_expr.array() == src.op() && index_expr.index() == where)
1594  continue;
1595  }
1596 
1597  endianness_mapt map(element.type(), little_endian, ns);
1598  exprt update_value = bv_to_expr(element, subtype, map, ns);
1599  if(non_const_update_bound.has_value())
1600  {
1601  update_value = if_exprt{
1603  from_integer(i, non_const_update_bound->type()),
1604  ID_lt,
1605  *non_const_update_bound},
1606  update_value,
1607  index_exprt{src.op(), where}};
1608  }
1609 
1610  if(result.id() != ID_with)
1611  result = with_exprt{result, std::move(where), std::move(update_value)};
1612  else
1613  result.add_to_operands(std::move(where), std::move(update_value));
1614  }
1615 
1616  return simplify_expr(std::move(result), ns);
1617 }
1618 
1635  const byte_update_exprt &src,
1636  const typet &subtype,
1637  const exprt &subtype_size,
1638  const exprt &value_as_byte_array,
1639  const exprt &non_const_update_bound,
1640  const exprt &initial_bytes,
1641  const exprt &first_index,
1642  const exprt &first_update_value,
1643  const namespacet &ns)
1644 {
1645  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1646  ? ID_byte_extract_little_endian
1647  : ID_byte_extract_big_endian;
1648 
1649  // TODO we either need a symbol table here or make array comprehensions
1650  // introduce a scope
1651  static std::size_t array_comprehension_index_counter = 0;
1652  ++array_comprehension_index_counter;
1653  symbol_exprt array_comprehension_index{
1654  "$array_comprehension_index_u_a_v_u" +
1655  std::to_string(array_comprehension_index_counter),
1656  to_array_type(src.type()).index_type()};
1657 
1658  // all arithmetic uses offset/index types
1659  PRECONDITION(array_comprehension_index.type() == src.offset().type());
1660  PRECONDITION(subtype_size.type() == src.offset().type());
1661  PRECONDITION(initial_bytes.type() == src.offset().type());
1662  PRECONDITION(first_index.type() == src.offset().type());
1663 
1664  // the bound from where updates start
1665  binary_predicate_exprt lower_bound{
1667  array_comprehension_index, first_index.type()),
1668  ID_lt,
1669  first_index};
1670 
1671  // The actual value of updates other than at the start or end
1672  plus_exprt offset_expr{
1673  initial_bytes,
1674  mult_exprt{
1675  subtype_size,
1676  minus_exprt{
1678  array_comprehension_index, first_index.type()),
1679  plus_exprt{first_index, from_integer(1, first_index.type())}}}};
1680  exprt update_value = lower_byte_extract(
1682  extract_opcode,
1683  value_as_byte_array,
1684  std::move(offset_expr),
1685  src.get_bits_per_byte(),
1686  subtype},
1687  ns);
1688 
1689  // The number of target array/vector elements being replaced, not including
1690  // a possible partial update at the end of the updated range, which is handled
1691  // below: (non_const_update_bound + (subtype_size - 1)) / subtype_size to
1692  // round up to the nearest multiple of subtype_size.
1693  div_exprt updated_elements{
1694  plus_exprt{
1696  non_const_update_bound, subtype_size.type()),
1697  minus_exprt{subtype_size, from_integer(1, subtype_size.type())}},
1698  subtype_size};
1699 
1700  // The last element to be updated: first_index + updated_elements - 1
1701  plus_exprt last_index{
1702  first_index,
1703  minus_exprt{
1704  std::move(updated_elements), from_integer(1, first_index.type())}};
1705 
1706  // The size of a partial update at the end of the updated range, may be zero.
1707  mod_exprt tail_size{
1709  minus_exprt{
1711  non_const_update_bound, initial_bytes.type()),
1712  initial_bytes},
1713  subtype_size.type()),
1714  subtype_size};
1715 
1716  // The bound where updates end, which is conditional on the partial update
1717  // being empty.
1718  binary_predicate_exprt upper_bound{
1720  array_comprehension_index, last_index.type()),
1721  ID_ge,
1722  if_exprt{
1723  equal_exprt{tail_size, from_integer(0, tail_size.type())},
1724  last_index,
1725  plus_exprt{last_index, from_integer(1, last_index.type())}}};
1726 
1727  // The actual value of a partial update at the end.
1728  exprt last_update_value = lower_byte_update(
1730  src.id(),
1731  index_exprt{src.op(), last_index},
1733  typecast_exprt::conditional_cast(last_index, subtype_size.type()),
1734  subtype_size}},
1735  value_as_byte_array,
1736  src.get_bits_per_byte()},
1737  ns);
1738 
1739  if_exprt array_comprehension_body{
1740  or_exprt{std::move(lower_bound), std::move(upper_bound)},
1741  index_exprt{src.op(), array_comprehension_index},
1742  if_exprt{
1743  equal_exprt{
1745  array_comprehension_index, first_index.type()),
1746  first_index},
1747  first_update_value,
1748  if_exprt{
1749  equal_exprt{
1751  array_comprehension_index, last_index.type()),
1752  last_index},
1753  std::move(last_update_value),
1754  std::move(update_value)}}};
1755 
1756  return simplify_expr(
1758  array_comprehension_index,
1759  std::move(array_comprehension_body),
1760  to_array_type(src.type())},
1761  ns);
1762 }
1763 
1775  const byte_update_exprt &src,
1776  const typet &subtype,
1777  const exprt &value_as_byte_array,
1778  const std::optional<exprt> &non_const_update_bound,
1779  const namespacet &ns)
1780 {
1781  // do all arithmetic below using index/offset types - the array theory
1782  // back-end is really picky about indices having the same type
1783  auto subtype_size_opt = size_of_expr(subtype, ns);
1784  CHECK_RETURN(subtype_size_opt.has_value());
1785 
1786  const exprt subtype_size = simplify_expr(
1788  subtype_size_opt.value(), src.offset().type()),
1789  ns);
1790 
1791  // compute the index of the first element of the array/vector that may be
1792  // updated
1793  PRECONDITION(
1794  src.offset().type() == to_array_type(src.op().type()).index_type());
1795  exprt first_index = div_exprt{src.offset(), subtype_size};
1796  simplify(first_index, ns);
1797 
1798  // compute the offset within that first element
1799  const exprt update_offset = mod_exprt{src.offset(), subtype_size};
1800 
1801  // compute the number of bytes (from the update value) that are going to be
1802  // consumed for updating the first element
1803  const exprt update_size =
1804  from_integer(value_as_byte_array.operands().size(), subtype_size.type());
1805  exprt initial_bytes = minus_exprt{subtype_size, update_offset};
1806  exprt update_bound;
1807  if(non_const_update_bound.has_value())
1808  {
1809  update_bound = typecast_exprt::conditional_cast(
1810  *non_const_update_bound, subtype_size.type());
1811  }
1812  else
1813  {
1815  value_as_byte_array.id() == ID_array,
1816  "value should be an array expression if the update bound is constant");
1817  update_bound = update_size;
1818  }
1819  initial_bytes = if_exprt{
1820  binary_predicate_exprt{initial_bytes, ID_lt, update_bound},
1821  initial_bytes,
1822  update_bound};
1823  simplify(initial_bytes, ns);
1824 
1825  // encode the first update: update the original element at first_index (the
1826  // actual update will only be initial_bytes-many bytes from
1827  // value_as_byte_array)
1828  exprt first_update_value = lower_byte_update(
1830  src.id(),
1831  index_exprt{src.op(), first_index},
1832  update_offset,
1833  value_as_byte_array,
1834  src.get_bits_per_byte()},
1835  ns);
1836 
1837  if(value_as_byte_array.id() != ID_array)
1838  {
1840  src,
1841  subtype,
1842  subtype_size,
1843  value_as_byte_array,
1844  *non_const_update_bound,
1845  initial_bytes,
1846  first_index,
1847  first_update_value,
1848  ns);
1849  }
1850 
1851  // We will update one array/vector element at a time - compute the number of
1852  // update values that will be consumed in each step. If we cannot determine a
1853  // constant value at this time we assume it's at least one byte. The
1854  // byte_extract_exprt within the loop uses the symbolic value (subtype_size),
1855  // we just need to make sure we make progress for the loop to terminate.
1856  std::size_t step_size = 1;
1857  if(subtype_size.is_constant())
1858  step_size = numeric_cast_v<std::size_t>(to_constant_expr(subtype_size));
1859  // Given the first update already encoded, keep track of the offset into the
1860  // update value. Again, the expressions within the loop use the symbolic
1861  // value, this is just an optimization in case we can determine a constant
1862  // offset.
1863  std::size_t offset = 0;
1864  if(initial_bytes.is_constant())
1865  offset = numeric_cast_v<std::size_t>(to_constant_expr(initial_bytes));
1866 
1867  with_exprt result{src.op(), first_index, first_update_value};
1868 
1869  auto lower_byte_update_array_vector_non_const_one_element =
1870  [&src,
1871  &first_index,
1872  &initial_bytes,
1873  &subtype_size,
1874  &value_as_byte_array,
1875  &ns,
1876  &result](std::size_t i) -> void {
1877  exprt where = simplify_expr(
1878  plus_exprt{first_index, from_integer(i, first_index.type())}, ns);
1879 
1880  exprt neg_offset_expr = simplify_expr(
1882  initial_bytes,
1883  mult_exprt{subtype_size, from_integer(i - 1, subtype_size.type())}}},
1884  ns);
1885 
1886  exprt element = lower_byte_update(
1888  src.id(),
1889  index_exprt{src.op(), where},
1890  neg_offset_expr,
1891  value_as_byte_array,
1892  src.get_bits_per_byte()},
1893  ns);
1894 
1895  result.add_to_operands(std::move(where), std::move(element));
1896  };
1897 
1898  std::size_t i = 1;
1899  for(; offset + step_size <= value_as_byte_array.operands().size();
1900  offset += step_size, ++i)
1901  {
1902  lower_byte_update_array_vector_non_const_one_element(i);
1903  }
1904 
1905  // do the tail
1906  if(offset < value_as_byte_array.operands().size())
1907  lower_byte_update_array_vector_non_const_one_element(i);
1908 
1909  return simplify_expr(std::move(result), ns);
1910 }
1911 
1925  const byte_update_exprt &src,
1926  const mp_integer &offset_bits,
1927  const exprt &element_to_update,
1928  const mp_integer &subtype_bits,
1929  const mp_integer &bits_already_set,
1930  const exprt &value_as_byte_array,
1931  const std::optional<exprt> &non_const_update_bound,
1932  const namespacet &ns)
1933 {
1934  // We need to take one or more bytes from value_as_byte_array to modify the
1935  // target element. We need to compute:
1936  // - The position in value_as_byte_array to take bytes from: If subtype_bits
1937  // is less than the size of a byte, then multiple struct/array/vector elements
1938  // will need to be updated using the same byte.
1939  std::size_t first = 0;
1940  // - An upper bound on the number of bytes required from value_as_byte_array.
1941  mp_integer update_elements =
1942  (subtype_bits + src.get_bits_per_byte() - 1) / src.get_bits_per_byte();
1943  // - The offset into the target element: If subtype_bits is greater or equal
1944  // to the size of a byte, then there may be an offset into the target element
1945  // that needs to be taken into account, and multiple bytes will be required.
1946  mp_integer offset_bits_in_target_element = offset_bits - bits_already_set;
1947 
1948  if(offset_bits_in_target_element < 0)
1949  {
1950  INVARIANT(
1951  value_as_byte_array.id() != ID_array ||
1952  value_as_byte_array.operands().size() * src.get_bits_per_byte() >
1953  -offset_bits_in_target_element,
1954  "indices past the update should be handled below");
1955  first += numeric_cast_v<std::size_t>(
1956  -offset_bits_in_target_element / src.get_bits_per_byte());
1957  offset_bits_in_target_element +=
1958  (-offset_bits_in_target_element / src.get_bits_per_byte()) *
1959  src.get_bits_per_byte();
1960  if(offset_bits_in_target_element < 0)
1961  ++update_elements;
1962  }
1963  else
1964  {
1965  update_elements -= offset_bits_in_target_element / src.get_bits_per_byte();
1966  INVARIANT(
1967  update_elements > 0, "indices before the update should be handled above");
1968  }
1969 
1970  std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1971  if(value_as_byte_array.id() == ID_array)
1972  end = std::min(end, value_as_byte_array.operands().size());
1973  exprt::operandst update_values = instantiate_byte_array(
1974  value_as_byte_array, first, end, src.get_bits_per_byte(), ns);
1975  const std::size_t update_size = update_values.size();
1976  const exprt update_size_expr = from_integer(update_size, size_type());
1977  const array_typet update_type{
1978  bv_typet{src.get_bits_per_byte()}, update_size_expr};
1979 
1980  // each case below will set "new_value" as appropriate
1981  exprt new_value;
1982 
1983  if(
1984  offset_bits_in_target_element >= 0 &&
1985  offset_bits_in_target_element % src.get_bits_per_byte() == 0)
1986  {
1987  new_value = array_exprt{update_values, update_type};
1988  }
1989  else
1990  {
1991  if(src.id() == ID_byte_update_little_endian)
1992  std::reverse(update_values.begin(), update_values.end());
1993  if(offset_bits_in_target_element < 0)
1994  {
1995  if(src.id() == ID_byte_update_little_endian)
1996  {
1997  new_value = lshr_exprt{
1999  update_values, bv_typet{update_size * src.get_bits_per_byte()}},
2000  numeric_cast_v<std::size_t>(-offset_bits_in_target_element)};
2001  }
2002  else
2003  {
2004  new_value = shl_exprt{
2006  update_values, bv_typet{update_size * src.get_bits_per_byte()}},
2007  numeric_cast_v<std::size_t>(-offset_bits_in_target_element)};
2008  }
2009  }
2010  else
2011  {
2012  const std::size_t offset_bits_int =
2013  numeric_cast_v<std::size_t>(offset_bits_in_target_element);
2014  const std::size_t subtype_bits_int =
2015  numeric_cast_v<std::size_t>(subtype_bits);
2016 
2017  extractbits_exprt bits_to_keep{
2018  element_to_update,
2019  subtype_bits_int - offset_bits_int,
2020  bv_typet{offset_bits_int}};
2021  new_value = concatenation_exprt{
2022  bits_to_keep,
2025  update_values, bv_typet{update_size * src.get_bits_per_byte()}},
2026  offset_bits_int,
2027  bv_typet{update_size * src.get_bits_per_byte() - offset_bits_int}},
2028  bv_typet{update_size * src.get_bits_per_byte()}};
2029  }
2030 
2031  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
2032  ? ID_byte_extract_little_endian
2033  : ID_byte_extract_big_endian;
2034 
2035  const byte_extract_exprt byte_extract_expr{
2036  extract_opcode,
2037  new_value,
2038  from_integer(0, src.offset().type()),
2039  src.get_bits_per_byte(),
2040  update_type};
2041 
2042  new_value = lower_byte_extract(byte_extract_expr, ns);
2043 
2044  offset_bits_in_target_element = 0;
2045  }
2046 
2047  // With an upper bound on the size of the update established, construct the
2048  // actual update expression. If the exact size of the update is unknown,
2049  // make the size expression conditional.
2050  const byte_update_exprt bu{
2051  src.id(),
2052  element_to_update,
2053  from_integer(
2054  offset_bits_in_target_element / src.get_bits_per_byte(),
2055  src.offset().type()),
2056  new_value,
2057  src.get_bits_per_byte()};
2058 
2059  std::optional<exprt> update_bound;
2060  if(non_const_update_bound.has_value())
2061  {
2062  // The size of the update is not constant, and thus is to be symbolically
2063  // bound; first see how many bytes we have left in the update:
2064  // non_const_update_bound > first ? non_const_update_bound - first: 0
2065  const exprt remaining_update_bytes = typecast_exprt::conditional_cast(
2066  if_exprt{
2068  *non_const_update_bound,
2069  ID_gt,
2070  from_integer(first, non_const_update_bound->type())},
2071  minus_exprt{
2072  *non_const_update_bound,
2073  from_integer(first, non_const_update_bound->type())},
2074  from_integer(0, non_const_update_bound->type())},
2075  size_type());
2076  // Now take the minimum of update-bytes-left and the previously computed
2077  // size of the element to be updated:
2078  update_bound = simplify_expr(
2079  if_exprt{
2080  binary_predicate_exprt{update_size_expr, ID_lt, remaining_update_bytes},
2081  update_size_expr,
2082  remaining_update_bytes},
2083  ns);
2084  }
2085 
2086  return lower_byte_update(bu, new_value, update_bound, ns);
2087 }
2088 
2100  const byte_update_exprt &src,
2101  const typet &subtype,
2102  const std::optional<mp_integer> &subtype_bits,
2103  const exprt &value_as_byte_array,
2104  const std::optional<exprt> &non_const_update_bound,
2105  const namespacet &ns)
2106 {
2107  const bool is_array = src.type().id() == ID_array;
2108  exprt size;
2109  typet index_type;
2110  if(is_array)
2111  {
2112  size = to_array_type(src.type()).size();
2113  index_type = to_array_type(src.type()).index_type();
2114  }
2115  else
2116  {
2117  size = to_vector_type(src.type()).size();
2118  index_type = to_vector_type(src.type()).index_type();
2119  }
2120 
2121  // fall back to bytewise updates in all non-constant or dubious cases
2122  if(
2123  !size.is_constant() || !src.offset().is_constant() ||
2124  !subtype_bits.has_value() || value_as_byte_array.id() != ID_array)
2125  {
2127  src, subtype, value_as_byte_array, non_const_update_bound, ns);
2128  }
2129 
2130  std::size_t num_elements =
2131  numeric_cast_v<std::size_t>(to_constant_expr(size));
2132  mp_integer offset_bits =
2133  numeric_cast_v<mp_integer>(to_constant_expr(src.offset())) *
2134  src.get_bits_per_byte();
2135 
2136  exprt::operandst elements;
2137  elements.reserve(num_elements);
2138 
2139  std::size_t i = 0;
2140  // copy the prefix not affected by the update
2141  for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bits; ++i)
2142  elements.push_back(index_exprt{src.op(), from_integer(i, index_type)});
2143 
2144  // the modified elements
2145  for(;
2146  i < num_elements &&
2147  i * *subtype_bits < offset_bits + value_as_byte_array.operands().size() *
2148  src.get_bits_per_byte();
2149  ++i)
2150  {
2151  elements.push_back(lower_byte_update_single_element(
2152  src,
2153  offset_bits,
2154  index_exprt{src.op(), from_integer(i, index_type)},
2155  *subtype_bits,
2156  i * *subtype_bits,
2157  value_as_byte_array,
2158  non_const_update_bound,
2159  ns));
2160  }
2161 
2162  // copy the tail not affected by the update
2163  for(; i < num_elements; ++i)
2164  elements.push_back(index_exprt{src.op(), from_integer(i, index_type)});
2165 
2166  if(is_array)
2167  return simplify_expr(
2168  array_exprt{std::move(elements), to_array_type(src.type())}, ns);
2169  else
2170  return simplify_expr(
2171  vector_exprt{std::move(elements), to_vector_type(src.type())}, ns);
2172 }
2173 
2184  const byte_update_exprt &src,
2185  const struct_typet &struct_type,
2186  const exprt &value_as_byte_array,
2187  const std::optional<exprt> &non_const_update_bound,
2188  const namespacet &ns)
2189 {
2190  exprt::operandst elements;
2191  elements.reserve(struct_type.components().size());
2192 
2194  for(const auto &comp : struct_type.components())
2195  {
2196  auto element_width = pointer_offset_bits(comp.type(), ns);
2197 
2198  // compute the update offset relative to this struct member - will be
2199  // negative if we are already in the middle of the update or beyond it
2200  exprt offset = simplify_expr(
2201  minus_exprt{
2202  mult_exprt{
2203  src.offset(),
2204  from_integer(src.get_bits_per_byte(), src.offset().type())},
2206  ns);
2207  auto offset_bits = numeric_cast<mp_integer>(offset);
2208  if(!offset_bits.has_value() || !element_width.has_value())
2209  {
2210  // The offset to update is not constant, either because the original
2211  // offset in src never was, or because a struct member has an unknown
2212  // offset. Abort the attempt to update individual struct members and
2213  // instead turn the operand-to-be-updated into a byte array, which we know
2214  // how to update even if the offset is non-constant.
2215  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
2216  ? ID_byte_extract_little_endian
2217  : ID_byte_extract_big_endian;
2218 
2219  auto src_size_opt = size_of_expr(src.type(), ns);
2220  CHECK_RETURN(src_size_opt.has_value());
2221 
2222  const byte_extract_exprt byte_extract_expr{
2223  extract_opcode,
2224  src.op(),
2225  from_integer(0, src.offset().type()),
2226  src.get_bits_per_byte(),
2227  array_typet{bv_typet{src.get_bits_per_byte()}, src_size_opt.value()}};
2228 
2229  byte_update_exprt bu = src;
2230  bu.set_op(lower_byte_extract(byte_extract_expr, ns));
2231  bu.type() = bu.op().type();
2232 
2233  return lower_byte_extract(
2235  extract_opcode,
2237  bu, value_as_byte_array, non_const_update_bound, ns),
2238  from_integer(0, src.offset().type()),
2239  src.get_bits_per_byte(),
2240  src.type()},
2241  ns);
2242  }
2243 
2244  exprt member = member_exprt{src.op(), comp.get_name(), comp.type()};
2245 
2246  // we don't need to update anything when
2247  // 1) the update offset is greater than the end of this member (thus the
2248  // relative offset is greater than this element) or
2249  // 2) the update offset plus the size of the update is less than the member
2250  // offset
2251  if(
2252  *offset_bits >= *element_width ||
2253  (value_as_byte_array.id() == ID_array && *offset_bits < 0 &&
2254  -*offset_bits >=
2255  value_as_byte_array.operands().size() * src.get_bits_per_byte()))
2256  {
2257  elements.push_back(member);
2258  member_offset_bits += *element_width;
2259  continue;
2260  }
2261 
2262  elements.push_back(lower_byte_update_single_element(
2263  src,
2264  *offset_bits + member_offset_bits,
2265  member,
2266  *element_width,
2268  value_as_byte_array,
2269  non_const_update_bound,
2270  ns));
2271 
2272  member_offset_bits += *element_width;
2273  }
2274 
2275  return simplify_expr(struct_exprt{std::move(elements), struct_type}, ns);
2276 }
2277 
2288  const byte_update_exprt &src,
2289  const union_typet &union_type,
2290  const exprt &value_as_byte_array,
2291  const std::optional<exprt> &non_const_update_bound,
2292  const namespacet &ns)
2293 {
2294  const auto widest_member = union_type.find_widest_union_component(ns);
2295 
2297  widest_member.has_value(),
2298  "lower_byte_update of union of unknown size is not supported");
2299 
2300  byte_update_exprt bu = src;
2301  bu.set_op(member_exprt{
2302  src.op(), widest_member->first.get_name(), widest_member->first.type()});
2303  bu.type() = widest_member->first.type();
2304 
2305  return union_exprt{
2306  widest_member->first.get_name(),
2307  lower_byte_update(bu, value_as_byte_array, non_const_update_bound, ns),
2308  src.type()};
2309 }
2310 
2320  const byte_update_exprt &src,
2321  const exprt &value_as_byte_array,
2322  const std::optional<exprt> &non_const_update_bound,
2323  const namespacet &ns)
2324 {
2325  if(src.type().id() == ID_array || src.type().id() == ID_vector)
2326  {
2327  std::optional<typet> subtype;
2328  if(src.type().id() == ID_vector)
2329  subtype = to_vector_type(src.type()).element_type();
2330  else
2331  subtype = to_array_type(src.type()).element_type();
2332 
2333  auto element_width = pointer_offset_bits(*subtype, ns);
2334 
2335  if(element_width.has_value() && *element_width == src.get_bits_per_byte())
2336  {
2337  if(value_as_byte_array.id() != ID_array)
2338  {
2340  non_const_update_bound.has_value(),
2341  "constant update bound should yield an array expression");
2343  src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2344  }
2345 
2347  src,
2348  *subtype,
2349  to_array_expr(value_as_byte_array),
2350  non_const_update_bound,
2351  ns);
2352  }
2353  else
2354  {
2356  src,
2357  *subtype,
2358  element_width,
2359  value_as_byte_array,
2360  non_const_update_bound,
2361  ns);
2362  }
2363  }
2364  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
2365  {
2366  const struct_typet &struct_type =
2367  src.type().id() == ID_struct_tag
2368  ? ns.follow_tag(to_struct_tag_type(src.type()))
2369  : to_struct_type(src.type());
2371  src, struct_type, value_as_byte_array, non_const_update_bound, ns);
2372  result.type() = src.type();
2373  return result;
2374  }
2375  else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
2376  {
2377  const union_typet &union_type =
2378  src.type().id() == ID_union_tag
2379  ? ns.follow_tag(to_union_tag_type(src.type()))
2380  : to_union_type(src.type());
2381  exprt result = lower_byte_update_union(
2382  src, union_type, value_as_byte_array, non_const_update_bound, ns);
2383  result.type() = src.type();
2384  return result;
2385  }
2386  else if(
2388  src.type().id() == ID_c_enum || src.type().id() == ID_c_enum_tag)
2389  {
2390  // mask out the bits to be updated, shift the value according to the
2391  // offset and bit-or
2392  const auto type_width = pointer_offset_bits(src.type(), ns);
2393  CHECK_RETURN(type_width.has_value() && *type_width > 0);
2394  const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2395 
2396  exprt::operandst update_bytes;
2397  if(value_as_byte_array.id() == ID_array)
2398  update_bytes = value_as_byte_array.operands();
2399  else
2400  {
2401  update_bytes = instantiate_byte_array(
2402  value_as_byte_array,
2403  0,
2404  (type_bits + src.get_bits_per_byte() - 1) / src.get_bits_per_byte(),
2405  src.get_bits_per_byte(),
2406  ns);
2407  }
2408 
2409  const std::size_t update_size_bits =
2410  update_bytes.size() * src.get_bits_per_byte();
2411  const std::size_t bit_width = std::max(type_bits, update_size_bits);
2412 
2413  const bool is_little_endian = src.id() == ID_byte_update_little_endian;
2414 
2415  exprt val_before =
2416  typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits});
2417  if(bit_width > type_bits)
2418  {
2419  val_before = concatenation_exprt{
2420  bv_typet{bit_width - type_bits}.all_zeros_expr(),
2421  val_before,
2422  bv_typet{bit_width}};
2423 
2424  if(!is_little_endian)
2425  to_concatenation_expr(val_before)
2426  .op0()
2427  .swap(to_concatenation_expr(val_before).op1());
2428  }
2429 
2430  if(non_const_update_bound.has_value())
2431  {
2432  const exprt src_as_bytes = unpack_rec(
2433  val_before,
2434  src.id() == ID_byte_update_little_endian,
2435  mp_integer{0},
2436  mp_integer{update_bytes.size()},
2437  src.get_bits_per_byte(),
2438  ns);
2439  CHECK_RETURN(src_as_bytes.id() == ID_array);
2440  CHECK_RETURN(src_as_bytes.operands().size() == update_bytes.size());
2441  for(std::size_t i = 0; i < update_bytes.size(); ++i)
2442  {
2443  update_bytes[i] = if_exprt{
2445  from_integer(i, non_const_update_bound->type()),
2446  ID_lt,
2447  *non_const_update_bound},
2448  update_bytes[i],
2449  src_as_bytes.operands()[i]};
2450  }
2451  }
2452 
2453  // build mask
2454  exprt mask;
2455  if(is_little_endian)
2456  mask = from_integer(power(2, update_size_bits) - 1, bv_typet{bit_width});
2457  else
2458  {
2459  mask = from_integer(
2460  power(2, bit_width) - power(2, bit_width - update_size_bits),
2461  bv_typet{bit_width});
2462  }
2463 
2464  const typet &offset_type = src.offset().type();
2465  mult_exprt offset_in_bits{
2466  src.offset(), from_integer(src.get_bits_per_byte(), offset_type)};
2467 
2468  const binary_predicate_exprt offset_ge_zero{
2469  offset_in_bits, ID_ge, from_integer(0, offset_type)};
2470 
2471  if_exprt mask_shifted{
2472  offset_ge_zero,
2473  shl_exprt{mask, offset_in_bits},
2474  lshr_exprt{mask, unary_minus_exprt{offset_in_bits}}};
2475  if(!is_little_endian)
2476  {
2477  mask_shifted.true_case().swap(mask_shifted.false_case());
2478  to_shift_expr(mask_shifted.true_case())
2479  .distance()
2480  .swap(to_shift_expr(mask_shifted.false_case()).distance());
2481  }
2482 
2483  // original_bits &= ~mask
2484  bitand_exprt bitand_expr{val_before, bitnot_exprt{mask_shifted}};
2485 
2486  // concatenate and zero-extend the value
2487  concatenation_exprt value{update_bytes, bv_typet{update_size_bits}};
2488  if(is_little_endian)
2489  std::reverse(value.operands().begin(), value.operands().end());
2490 
2491  exprt zero_extended;
2492  if(bit_width > update_size_bits)
2493  {
2494  if(is_little_endian)
2495  zero_extended = zero_extend_exprt{value, bv_typet{bit_width}};
2496  else
2497  {
2498  // Big endian -- the zero is added as LSB.
2499  zero_extended = concatenation_exprt{
2500  value,
2501  bv_typet{bit_width - update_size_bits}.all_zeros_expr(),
2502  bv_typet{bit_width}};
2503  }
2504  }
2505  else
2506  zero_extended = value;
2507 
2508  // shift the value
2509  if_exprt value_shifted{
2510  offset_ge_zero,
2511  shl_exprt{zero_extended, offset_in_bits},
2512  lshr_exprt{zero_extended, unary_minus_exprt{offset_in_bits}}};
2513  if(!is_little_endian)
2514  {
2515  value_shifted.true_case().swap(value_shifted.false_case());
2516  to_shift_expr(value_shifted.true_case())
2517  .distance()
2518  .swap(to_shift_expr(value_shifted.false_case()).distance());
2519  }
2520 
2521  // original_bits |= newvalue
2522  bitor_exprt bitor_expr{bitand_expr, value_shifted};
2523 
2524  if(bit_width > type_bits)
2525  {
2526  endianness_mapt endianness_map(
2527  bitor_expr.type(), src.id() == ID_byte_update_little_endian, ns);
2528  const auto bounds = map_bounds(endianness_map, 0, type_bits - 1);
2529 
2530  PRECONDITION(pointer_offset_bits(bitor_expr.type(), ns).has_value());
2531  return simplify_expr(
2533  extractbits_exprt{bitor_expr, bounds.lb, bv_typet{type_bits}},
2534  src.type()),
2535  ns);
2536  }
2537 
2538  return simplify_expr(
2539  typecast_exprt::conditional_cast(bitor_expr, src.type()), ns);
2540  }
2541  else
2542  {
2544  false, "lower_byte_update does not yet support ", src.type().id_string());
2545  }
2546 }
2547 
2549 {
2551  src.id() == ID_byte_update_little_endian ||
2552  src.id() == ID_byte_update_big_endian,
2553  "byte update expression should either be little or big endian");
2554 
2555  // An update of a void-typed object or update by a void-typed value is the
2556  // source operand (this is questionable, but may arise when dereferencing
2557  // invalid pointers).
2558  if(src.type().id() == ID_empty || src.value().type().id() == ID_empty)
2559  return src.op();
2560 
2561  // byte_update lowering proceeds as follows:
2562  // 1) Determine the size of the update, with the size of the object to be
2563  // updated as an upper bound. We fail if neither can be determined.
2564  // 2) Turn the update value into a byte array of the size determined above.
2565  // 3) If the offset is not constant, turn the object into a byte array, and
2566  // use a "with" expression to encode the update; else update the values in
2567  // place.
2568  // 4) Construct a new object.
2569  std::optional<exprt> non_const_update_bound;
2570  // update value, may require extension to full bytes
2571  exprt update_value = src.value();
2572  auto update_size_expr_opt = size_of_expr(update_value.type(), ns);
2573  CHECK_RETURN(update_size_expr_opt.has_value());
2574  simplify(update_size_expr_opt.value(), ns);
2575 
2576  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
2577  ? ID_byte_extract_little_endian
2578  : ID_byte_extract_big_endian;
2579  const std::size_t bits_per_byte = src.get_bits_per_byte();
2580 
2581  if(!update_size_expr_opt.value().is_constant())
2582  non_const_update_bound = *update_size_expr_opt;
2583  else
2584  {
2585  auto update_bits = pointer_offset_bits(update_value.type(), ns);
2586  // If the following invariant fails, then the type was only found to be
2587  // constant via simplification. Such instances should be fixed at the place
2588  // introducing these constant-but-not-constant_exprt type sizes.
2590  update_bits.has_value(), "constant size-of should imply fixed bit width");
2591  const size_t update_bits_int = numeric_cast_v<size_t>(*update_bits);
2592 
2593  if(update_bits_int % bits_per_byte != 0)
2594  {
2596  can_cast_type<bitvector_typet>(update_value.type()),
2597  "non-byte aligned type expected to be a bitvector type");
2598  const byte_extract_exprt overlapping_byte_extract{
2599  extract_opcode,
2600  src.op(),
2601  simplify_expr(
2602  plus_exprt{
2603  src.offset(),
2604  from_integer(update_bits_int / bits_per_byte, src.offset().type())},
2605  ns),
2606  src.get_bits_per_byte(),
2607  bv_typet{bits_per_byte}};
2608  const exprt overlapping_byte =
2609  lower_byte_extract(overlapping_byte_extract, ns);
2610 
2611  size_t n_extra_bits = bits_per_byte - update_bits_int % bits_per_byte;
2612  extractbits_exprt extra_bits{overlapping_byte, 0, bv_typet{n_extra_bits}};
2613 
2614  update_value = concatenation_exprt{
2616  update_value, bv_typet{update_bits_int}),
2617  extra_bits,
2618  adjust_width(update_value.type(), update_bits_int + n_extra_bits)};
2619  }
2620  else
2621  {
2622  update_size_expr_opt = from_integer(
2623  update_bits_int / bits_per_byte, update_size_expr_opt->type());
2624  }
2625  }
2626 
2627  const byte_extract_exprt byte_extract_expr{
2628  extract_opcode,
2629  update_value,
2630  from_integer(0, src.offset().type()),
2631  src.get_bits_per_byte(),
2632  array_typet{bv_typet{bits_per_byte}, *update_size_expr_opt}};
2633 
2634  const exprt value_as_byte_array = lower_byte_extract(byte_extract_expr, ns);
2635 
2636  exprt result =
2637  lower_byte_update(src, value_as_byte_array, non_const_update_bound, ns);
2638  return result;
2639 }
2640 
2642 {
2643  exprt tmp = src;
2644 
2645  // destroys any sharing, should use hash table
2646  Forall_operands(it, tmp)
2647  {
2648  *it = lower_byte_operators(*it, ns);
2649  }
2650 
2651  if(
2652  src.id() == ID_byte_update_little_endian ||
2653  src.id() == ID_byte_update_big_endian)
2654  {
2655  return lower_byte_update(to_byte_update_expr(tmp), ns);
2656  }
2657  else if(
2658  src.id() == ID_byte_extract_little_endian ||
2659  src.id() == ID_byte_extract_big_endian)
2660  {
2661  return lower_byte_extract(to_byte_extract_expr(tmp), ns);
2662  }
2663  else
2664  return tmp;
2665 }
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:20
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 shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:335
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:224
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:80
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:184
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3423
Array constructor from list of elements.
Definition: std_expr.h:1621
Arrays with given size.
Definition: std_types.h:807
typet index_type() const
The type of the index expressions into any instance of this type.
Definition: std_types.cpp:34
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
const exprt & size() const
Definition: std_types.h:840
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:731
Bit-wise AND.
Bit-wise negation of bit-vectors.
Bit-wise OR.
Base class of fixed-width bit-vector types.
Definition: std_types.h:909
std::size_t get_width() const
Definition: std_types.h:925
Fixed-width bit-vector without numerical interpretation.
constant_exprt all_zeros_expr() const
Expression of type type extracted from some object op starting at position offset (given in number of...
std::size_t get_bits_per_byte() const
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)
std::size_t get_bits_per_byte() const
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition: c_types.h:20
Complex constructor from a pair of numbers.
Definition: std_expr.h:1916
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:2027
Real part of the expression describing a complex number.
Definition: std_expr.h:1984
Complex numbers made of pair of given subtype.
Definition: std_types.h:1130
Concatenation of bit-vector operands.
Division.
Definition: std_expr.h:1157
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Union constructor to support unions without any member (a GCC/Clang feature).
Definition: std_expr.h:1834
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:1366
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
operandst & operands()
Definition: expr.h:94
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:170
Extracts a sub-range of a bit-vector operand.
The trinary if-then-else operator.
Definition: std_expr.h:2380
Array index operator.
Definition: std_expr.h:1470
exprt & array()
Definition: std_expr.h:1500
exprt & index()
Definition: std_expr.h:1510
const std::string & id_string() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:388
void swap(irept &irep)
Definition: irep.h:434
Logical right shift.
Extract member of struct or union.
Definition: std_expr.h:2854
Binary minus.
Definition: std_expr.h:1061
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1228
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1107
exprt & op0()
Definition: std_expr.h:932
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The NIL expression.
Definition: std_expr.h:3091
Boolean OR.
Definition: std_expr.h:2233
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
exprt & distance()
Left shift.
Fixed-width bit-vector with two's complement interpretation.
Struct constructor from list of elements.
Definition: std_expr.h:1877
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const typet & subtype() const
Definition: type.h:187
Semantic type conversion.
Definition: std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2081
The type of an expression, extends irept.
Definition: type.h:29
The unary minus expression.
Definition: std_expr.h:484
Union constructor from single element.
Definition: std_expr.h:1770
The union type.
Definition: c_types.h:147
std::optional< 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:300
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
Definition: std_expr.h:1734
The vector type.
Definition: std_types.h:1061
const constant_exprt & size() const
Definition: std_types.cpp:286
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1077
typet index_type() const
The type of any index expression into an instance of this type.
Definition: std_types.cpp:274
Operator to update elements in structs and arrays.
Definition: std_expr.h:2481
zero extension The operand is converted to the given type by either a) truncating if the new type is ...
#define Forall_operands(it, expr)
Definition: expr.h:27
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:193
Deprecated expression utility functions.
static exprt lower_byte_update_union(const byte_update_exprt &src, const union_typet &union_type, const exprt &value_as_byte_array, const std::optional< 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...
static exprt lower_byte_update_byte_array_vector(const byte_update_exprt &src, const typet &subtype, const array_exprt &value_as_byte_array, const std::optional< 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 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 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.
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 array_exprt unpack_struct(const exprt &src, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite a struct-typed expression into its individual bytes.
static exprt::operandst instantiate_byte_array(const exprt &src, std::size_t lower_bound, std::size_t upper_bound, const std::size_t bits_per_byte, const namespacet &ns)
Build the individual bytes to be used in an 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...
bitvector_typet adjust_width(const typet &src, std::size_t new_width)
changes the width of the given bitvector type
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 void process_bit_fields(exprt::operandst &&bit_fields, std::size_t total_bits, exprt::operandst &dest, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Extract bytes from a sequence of bitvector-typed elements.
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 array_exprt unpack_complex(const exprt &src, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite a complex_exprt into its individual bytes.
static exprt unpack_array_vector_no_known_bounds(const exprt &src, std::size_t el_bytes, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite an array or vector into its individual bytes when no maximum number of bytes is known.
static exprt lower_byte_update_array_vector(const byte_update_exprt &src, const typet &subtype, const std::optional< mp_integer > &subtype_bits, const exprt &value_as_byte_array, const std::optional< 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_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const std::optional< 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 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.
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
static exprt lower_byte_extract_array_vector(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const typet &subtype, const mp_integer &element_bits, const namespacet &ns)
Rewrite a byte extraction of an array/vector-typed result to byte extraction of the individual compon...
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const std::optional< 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 unpack_array_vector(const exprt &src, const std::optional< mp_integer > &src_size, const mp_integer &element_bits, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite an array or vector into its individual bytes.
static exprt unpack_rec(const exprt &src, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns, bool unpack_byte_array=false)
Rewrite an object into its individual bytes.
static exprt lower_byte_update_struct(const byte_update_exprt &src, const struct_typet &struct_type, const exprt &value_as_byte_array, const std::optional< 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 ...
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_single_element(const byte_update_exprt &src, const mp_integer &offset_bits, const exprt &element_to_update, const mp_integer &subtype_bits, const mp_integer &bits_already_set, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Byte update a struct/array/vector element.
static std::optional< 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 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...
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:17
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3055
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1665
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1538
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1113
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1155
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:952
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:208
#define size_type
Definition: unistd.c:347