cprover
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 "std_types.h"
14 #include "pointer_offset_size.h"
15 #include "arith_tools.h"
16 #include "namespace.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_symbol_type)
56  else if(src.id()==ID_c_enum_tag)
58  else if(src.id()==ID_unsignedbv ||
59  src.id()==ID_signedbv ||
60  src.id()==ID_fixedbv ||
61  src.id()==ID_floatbv ||
62  src.id()==ID_c_enum ||
63  src.id()==ID_c_bit_field)
64  {
65  // these do get re-ordered!
66  auto bits = pointer_offset_bits(src, ns); // error is -1
67  CHECK_RETURN(bits.has_value());
68 
69  const std::size_t bits_int = numeric_cast_v<std::size_t>(*bits);
70  const std::size_t base = map.size();
71 
72  for(size_t bit=0; bit<bits_int; bit++)
73  {
74  map.push_back(base+bits_int-1-bit);
75  }
76  }
77  else if(src.id()==ID_struct)
78  {
79  const struct_typet &struct_type=to_struct_type(src);
80 
81  // todo: worry about padding being in wrong order
82  for(const auto &c : struct_type.components())
83  {
84  build_big_endian(c.type());
85  }
86  }
87  else if(src.id() == ID_struct_tag)
88  {
90  }
91  else if(src.id()==ID_array)
92  {
93  const array_typet &array_type=to_array_type(src);
94 
95  // array size constant?
96  auto s = numeric_cast<mp_integer>(array_type.size());
97  if(s.has_value())
98  {
99  while(*s > 0)
100  {
101  build_big_endian(array_type.subtype());
102  --(*s);
103  }
104  }
105  }
106  else if(src.id()==ID_vector)
107  {
108  const vector_typet &vector_type=to_vector_type(src);
109 
110  mp_integer s = numeric_cast_v<mp_integer>(vector_type.size());
111 
112  while(s > 0)
113  {
114  build_big_endian(vector_type.subtype());
115  --s;
116  }
117  }
118  else
119  {
120  // everything else (unions in particular)
121  // is treated like a byte-array
122  auto s = pointer_offset_bits(src, ns); // error is -1
123 
124  if(!s.has_value())
125  return;
126 
127  const std::size_t new_size = map.size() + numeric_cast_v<std::size_t>(*s);
128  map.reserve(new_size);
129 
130  for(std::size_t i=map.size(); i<new_size; ++i)
131  map.push_back(i);
132  }
133 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
pointer_offset_size.h
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: std_types.h:737
typet::subtype
const typet & subtype() const
Definition: type.h:38
endianness_mapt::build
void build(const typet &type, bool little_endian)
Definition: endianness_map.cpp:30
vector_typet::size
const exprt & size() const
Definition: std_types.h:1765
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:349
typet
The type of an expression, extends irept.
Definition: type.h:27
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
endianness_mapt::build_little_endian
virtual void build_little_endian(const typet &type)
Definition: endianness_map.cpp:38
vector_typet
The vector type.
Definition: std_types.h:1755
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:1010
endianness_mapt::map
std::vector< size_t > map
Definition: endianness_map.h:67
namespace_baset::follow_tag
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
endianness_mapt::ns
const namespacet & ns
Definition: endianness_map.h:66
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:101
std_types.h
irept::id
const irep_idt & id() const
Definition: irep.h:259
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:543
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:276
array_typet
Arrays with given size.
Definition: std_types.h:1000
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1793
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470