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