cprover
alignment_checks.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Alignment Checks
4 
5 Author:
6 
7 \*******************************************************************/
8 
11 
12 #include "alignment_checks.h"
13 
14 #include <util/config.h>
15 #include <util/namespace.h>
17 #include <util/std_types.h>
18 
19 #include <ostream>
20 
22  const symbol_tablet &symbol_table,
23  std::ostream &out)
24 {
25  for(const auto &symbol_pair : symbol_table.symbols)
26  {
27  if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
28  {
29  const struct_typet &str = to_struct_type(symbol_pair.second.type);
30  const struct_typet::componentst &components = str.components();
31 
32  bool first_time_seen_in_struct = true;
33 
34  for(struct_typet::componentst::const_iterator it_mem = components.begin();
35  it_mem != components.end();
36  it_mem++)
37  {
38  mp_integer cumulated_length = 0;
39  bool first_time_seen_from = true;
40 
41  // if the instruction cannot be aligned to the address,
42  // try the next one
43 
44  if(it_mem->get_is_padding())
45  // || alignment(it_mem->type())%config.ansi_c.alignment!=0)
46  continue;
47 
48  for(struct_typet::componentst::const_iterator it_next = it_mem;
49  it_next != components.end();
50  it_next++)
51  {
52  const typet &it_type = it_next->type();
53  const namespacet ns(symbol_table);
54  auto size = pointer_offset_size(it_type, ns);
55 
56  if(!size.has_value())
57  throw "type of unknown size:\n" + it_type.pretty();
58 
59  cumulated_length += *size;
60  // [it_mem;it_next] cannot be covered by an instruction
61  if(cumulated_length > config.ansi_c.memory_operand_size)
62  {
63  // if interferences have been found, no need to check with
64  // starting from an already covered member
65  if(!first_time_seen_from)
66  it_mem = it_next - 1;
67  break;
68  }
69 
70  if(it_mem != it_next && !it_next->get_is_padding())
71  {
72  if(first_time_seen_in_struct)
73  {
74  first_time_seen_in_struct = false;
75  first_time_seen_from = false;
76 
77  out << "\nWARNING: "
78  << "declaration of structure "
79  << str.find_type(ID_tag).pretty() << " at "
80  << symbol_pair.second.location << '\n';
81  }
82 
83  out << "members " << it_mem->get_pretty_name() << " and "
84  << it_next->get_pretty_name() << " might interfere\n";
85  }
86  }
87  }
88  }
89  else if(symbol_pair.second.type.id() == ID_array)
90  {
91  // is this structure likely to introduce data races?
92  #if 0
93  const namespacet ns(symbol_table);
94  const array_typet array=to_array_type(symbol_pair.second.type);
95  const auto size=
96  pointer_offset_size(array.subtype(), ns);
97 
98  if(!size.has_value())
99  throw "type of unknown size:\n"+it_type.pretty();
100 
101  if(2*integer2long(*size)<=config.ansi_c.memory_operand_size)
102  {
103  out << "\nWARNING: "
104  << "declaration of an array at "
105  << symbol_pair.second.location <<
106  << "\nmight be concurrently accessed\n";
107  }
108  #endif
109  }
110  }
111 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
pointer_offset_size.h
Pointer Logic.
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
typet::subtype
const typet & subtype() const
Definition: type.h:47
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
typet
The type of an expression, extends irept.
Definition: type.h:29
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
configt::ansi_c
struct configt::ansi_ct ansi_c
namespace.h
print_struct_alignment_problems
void print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
Definition: alignment_checks.cpp:21
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
std_types.h
Pre-defined types.
configt::ansi_ct::memory_operand_size
std::size_t memory_operand_size
Definition: config.h:74
config
configt config
Definition: config.cpp:24
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
pointer_offset_size
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Definition: pointer_offset_size.cpp:89
array_typet
Arrays with given size.
Definition: std_types.h:965
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
config.h
alignment_checks.h
Alignment Checks.
typet::find_type
const typet & find_type(const irep_namet &name) const
Definition: type.h:86