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 
15 #include <util/config.h>
16 #include <util/symbol_table.h>
17 
19  const symbol_tablet &symbol_table,
20  std::ostream &out)
21 {
22  forall_symbols(it, symbol_table.symbols)
23  if(it->second.is_type && it->second.type.id()==ID_struct)
24  {
25  const struct_typet &str=to_struct_type(it->second.type);
26  const struct_typet::componentst &components=str.components();
27 
28  bool first_time_seen_in_struct=true;
29 
30  for(struct_typet::componentst::const_iterator
31  it_mem=components.begin();
32  it_mem!=components.end();
33  it_mem++)
34  {
35  mp_integer cumulated_length=0;
36  bool first_time_seen_from=true;
37 
38  // if the instruction cannot be aligned to the address,
39  // try the next one
40 
41  if(it_mem->get_is_padding())
42  // || alignment(it_mem->type())%config.ansi_c.alignment!=0)
43  continue;
44 
45  for(struct_typet::componentst::const_iterator
46  it_next=it_mem;
47  it_next!=components.end();
48  it_next++)
49  {
50  const typet &it_type=it_next->type();
51  const namespacet ns(symbol_table);
52  mp_integer size=pointer_offset_size(it_type, ns);
53 
54  if(size<0)
55  throw "type of unknown size:\n"+it_type.pretty();
56 
57  cumulated_length+=size;
58  // [it_mem;it_next] cannot be covered by an instruction
59  if(cumulated_length>config.ansi_c.memory_operand_size)
60  {
61  // if interferences have been found, no need to check with
62  // starting from an already covered member
63  if(!first_time_seen_from)
64  it_mem=it_next-1;
65  break;
66  }
67 
68  if(it_mem!=it_next && !it_next->get_is_padding())
69  {
70  if(first_time_seen_in_struct)
71  {
72  first_time_seen_in_struct=false;
73  first_time_seen_from=false;
74 
75  out << "\nWARNING: "
76  << "declaration of structure "
77  << str.find_type(ID_tag).pretty()
78  << " at " << it->second.location << '\n';
79  }
80 
81  out << "members " << it_mem->get_pretty_name() << " and "
82  << it_next->get_pretty_name() << " might interfere\n";
83  }
84  }
85  }
86  }
87  else if(it->second.type.id()==ID_array)
88  {
89  // is this structure likely to introduce data races?
90  #if 0
91  const namespacet ns(symbol_table);
92  const array_typet array=to_array_type(it->second.type);
93  const mp_integer size=
94  pointer_offset_size(array.subtype(), ns);
95 
96  if(size<0)
97  throw "type of unknown size:\n"+it_type.pretty();
98 
99  if(2*integer2long(size)<=config.ansi_c.memory_operand_size)
100  {
101  out << "\nWARNING: "
102  << "declaration of an array at "
103  << it->second.location <<
104  << "\nmight be concurrently accessed\n";
105  }
106  #endif
107  }
108 }
The type of an expression.
Definition: type.h:20
struct configt::ansi_ct ansi_c
BigInt mp_integer
Definition: mp_arith.h:19
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
void print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
std::vector< componentt > componentst
Definition: std_types.h:240
const componentst & components() const
Definition: std_types.h:242
Structure type.
Definition: std_types.h:296
configt config
Definition: config.cpp:21
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
symbolst symbols
Definition: symbol_table.h:57
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
unsigned memory_operand_size
Definition: config.h:72
Symbol table.
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
Pointer Logic.
const typet & find_type(const irep_namet &name) const
Definition: type.h:110
Alignment Checks.
arrays with given size
Definition: std_types.h:901
const typet & subtype() const
Definition: type.h:31