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