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 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:147
pointer_offset_size.h
mp_integer
BigInt mp_integer
Definition: smt_terms.h:17
endianness_mapt::build
void build(const typet &type, bool little_endian)
Definition: endianness_map.cpp:30
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
typet
The type of an expression, extends irept.
Definition: type.h:28
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:269
endianness_mapt::build_little_endian
virtual void build_little_endian(const typet &type)
Definition: endianness_map.cpp:38
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
vector_typet
The vector type.
Definition: std_types.h:1007
namespace.h
endianness_mapt::build_big_endian
virtual void build_big_endian(const typet &type)
Definition: endianness_map.cpp:52
array_typet::size
const exprt & size() const
Definition: std_types.h:800
vector_typet::element_type
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1026
endianness_mapt::map
std::vector< size_t > map
Definition: endianness_map.h:66
to_c_enum_tag_type
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:344
endianness_mapt::ns
const namespacet & ns
Definition: endianness_map.h:65
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:101
irept::id
const irep_idt & id() const
Definition: irep.h:396
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:474
endianness_map.h
endianness_mapt::output
void output(std::ostream &) const
Definition: endianness_map.cpp:18
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:230
array_typet
Arrays with given size.
Definition: std_types.h:762
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:844
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1060
c_types.h
array_typet::element_type
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:785