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 "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(src.id()==ID_unsignedbv ||
57  src.id()==ID_signedbv ||
58  src.id()==ID_fixedbv ||
59  src.id()==ID_floatbv ||
60  src.id()==ID_c_enum ||
61  src.id()==ID_c_bit_field)
62  {
63  // these do get re-ordered!
64  auto bits = pointer_offset_bits(src, ns); // error is -1
65  CHECK_RETURN(bits.has_value());
66 
67  const std::size_t bits_int = numeric_cast_v<std::size_t>(*bits);
68  const std::size_t base = map.size();
69 
70  for(size_t bit=0; bit<bits_int; bit++)
71  {
72  map.push_back(base+bits_int-1-bit);
73  }
74  }
75  else if(src.id()==ID_struct)
76  {
77  const struct_typet &struct_type=to_struct_type(src);
78 
79  // todo: worry about padding being in wrong order
80  for(const auto &c : struct_type.components())
81  {
82  build_big_endian(c.type());
83  }
84  }
85  else if(src.id() == ID_struct_tag)
86  {
88  }
89  else if(src.id()==ID_array)
90  {
91  const array_typet &array_type=to_array_type(src);
92 
93  // array size constant?
94  auto s = numeric_cast<mp_integer>(array_type.size());
95  if(s.has_value())
96  {
97  while(*s > 0)
98  {
99  build_big_endian(array_type.subtype());
100  --(*s);
101  }
102  }
103  }
104  else if(src.id()==ID_vector)
105  {
106  const vector_typet &vector_type=to_vector_type(src);
107 
108  mp_integer s = numeric_cast_v<mp_integer>(vector_type.size());
109 
110  while(s > 0)
111  {
112  build_big_endian(vector_type.subtype());
113  --s;
114  }
115  }
116  else
117  {
118  // everything else (unions in particular)
119  // is treated like a byte-array
120  auto s = pointer_offset_bits(src, ns); // error is -1
121 
122  if(!s.has_value())
123  return;
124 
125  const std::size_t new_size = map.size() + numeric_cast_v<std::size_t>(*s);
126  map.reserve(new_size);
127 
128  for(std::size_t i=map.size(); i<new_size; ++i)
129  map.push_back(i);
130  }
131 }
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:317
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:771
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:407
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:28
const typet & subtype() const
Definition: type.h:47
The vector type.
Definition: std_types.h:975
const constant_exprt & size() const
Definition: std_types.cpp:239
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
BigInt mp_integer
Definition: smt_terms.h:12
#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:1000
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:813
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474