CBMC
endianness_map.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 "endianness_map.h"
10 
11 #include <ostream>
12 
13 #include "arith_tools.h"
14 #include "c_types.h"
15 #include "namespace.h"
16 #include "pointer_offset_size.h"
17 
18 void endianness_mapt::output(std::ostream &out) const
19 {
20  for(std::vector<size_t>::const_iterator it=map.begin();
21  it!=map.end();
22  ++it)
23  {
24  if(it!=map.begin())
25  out << ", ";
26  out << *it;
27  }
28 }
29 
30 void endianness_mapt::build(const typet &src, bool little_endian)
31 {
32  if(little_endian)
34  else
35  build_big_endian(src);
36 }
37 
39 {
40  auto s = pointer_offset_bits(src, ns);
41 
42  if(!s.has_value())
43  return;
44 
45  const std::size_t new_size = map.size() + numeric_cast_v<std::size_t>(*s);
46  map.reserve(new_size);
47 
48  for(std::size_t i=map.size(); i<new_size; ++i)
49  map.push_back(i);
50 }
51 
53 {
54  if(src.id() == ID_c_enum_tag)
56  else if(
57  src.id() == ID_unsignedbv || src.id() == ID_signedbv ||
58  src.id() == ID_fixedbv || src.id() == ID_floatbv || src.id() == ID_c_enum ||
59  src.id() == ID_c_bit_field || src.id() == ID_bv)
60  {
61  // these do get re-ordered!
62  auto bits = pointer_offset_bits(src, ns); // error is -1
63  CHECK_RETURN(bits.has_value());
64 
65  const std::size_t bits_int = numeric_cast_v<std::size_t>(*bits);
66  const std::size_t base = map.size();
67 
68  for(size_t bit=0; bit<bits_int; bit++)
69  {
70  map.push_back(base+bits_int-1-bit);
71  }
72  }
73  else if(src.id()==ID_struct)
74  {
75  const struct_typet &struct_type=to_struct_type(src);
76 
77  // todo: worry about padding being in wrong order
78  for(const auto &c : struct_type.components())
79  {
80  build_big_endian(c.type());
81  }
82  }
83  else if(src.id() == ID_struct_tag)
84  {
86  }
87  else if(src.id()==ID_array)
88  {
89  const array_typet &array_type=to_array_type(src);
90 
91  // array size constant?
92  auto s = numeric_cast<mp_integer>(array_type.size());
93  if(s.has_value())
94  {
95  while(*s > 0)
96  {
97  build_big_endian(array_type.element_type());
98  --(*s);
99  }
100  }
101  }
102  else if(src.id()==ID_vector)
103  {
104  const vector_typet &vector_type=to_vector_type(src);
105 
106  mp_integer s = numeric_cast_v<mp_integer>(vector_type.size());
107 
108  while(s > 0)
109  {
110  build_big_endian(vector_type.element_type());
111  --s;
112  }
113  }
114  else
115  {
116  // everything else (unions in particular)
117  // is treated like a byte-array
118  auto s = pointer_offset_bits(src, ns); // error is -1
119 
120  if(!s.has_value())
121  return;
122 
123  const std::size_t new_size = map.size() + numeric_cast_v<std::size_t>(*s);
124  map.reserve(new_size);
125 
126  for(std::size_t i=map.size(); i<new_size; ++i)
127  map.push_back(i);
128  }
129 }
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:377
Arrays with given size.
Definition: std_types.h:807
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
const namespacet & ns
virtual void build_big_endian(const typet &type)
virtual void build_little_endian(const typet &type)
void build(const typet &type, bool little_endian)
std::vector< size_t > map
void output(std::ostream &) const
const irep_idt & id() const
Definition: irep.h:384
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
The type of an expression, extends irept.
Definition: type.h:29
The vector type.
Definition: std_types.h:1052
const constant_exprt & size() const
Definition: std_types.cpp:270
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1068
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
BigInt mp_integer
Definition: smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1104
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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518