cprover
global_may_alias.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-insensitive, location-sensitive global may alias analysis
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "global_may_alias.h"
13 
15  const exprt &lhs,
16  const std::set<irep_idt> &alias_set)
17 {
18  if(lhs.id()==ID_symbol)
19  {
20  irep_idt identifier=to_symbol_expr(lhs).get_identifier();
21 
22  aliases.isolate(identifier);
23 
24  for(const auto &alias : alias_set)
25  {
26  aliases.make_union(identifier, alias);
27  }
28  }
29 }
30 
32  const exprt &rhs,
33  std::set<irep_idt> &alias_set)
34 {
35  if(rhs.id()==ID_symbol)
36  {
37  irep_idt identifier=to_symbol_expr(rhs).get_identifier();
38  alias_set.insert(identifier);
39 
40  for(const auto &alias : alias_set)
41  if(aliases.same_set(alias, identifier))
42  alias_set.insert(alias);
43  }
44  else if(rhs.id()==ID_if)
45  {
46  get_rhs_aliases(to_if_expr(rhs).true_case(), alias_set);
47  get_rhs_aliases(to_if_expr(rhs).false_case(), alias_set);
48  }
49  else if(rhs.id()==ID_typecast)
50  {
51  get_rhs_aliases(to_typecast_expr(rhs).op(), alias_set);
52  }
53  else if(rhs.id()==ID_address_of)
54  {
55  get_rhs_aliases_address_of(to_address_of_expr(rhs).op0(), alias_set);
56  }
57 }
58 
60  const exprt &rhs,
61  std::set<irep_idt> &alias_set)
62 {
63  if(rhs.id()==ID_symbol)
64  {
65  irep_idt identifier=to_symbol_expr(rhs).get_identifier();
66  alias_set.insert("&"+id2string(identifier));
67  }
68  else if(rhs.id()==ID_if)
69  {
70  get_rhs_aliases_address_of(to_if_expr(rhs).true_case(), alias_set);
71  get_rhs_aliases_address_of(to_if_expr(rhs).false_case(), alias_set);
72  }
73  else if(rhs.id()==ID_dereference)
74  {
75  }
76 }
77 
79  locationt from,
80  locationt to,
81  ai_baset &ai,
82  const namespacet &ns)
83 {
84  if(has_values.is_false())
85  return;
86 
87  const goto_programt::instructiont &instruction=*from;
88 
89  switch(instruction.type)
90  {
91  case ASSIGN:
92  {
93  const code_assignt &code_assign=to_code_assign(instruction.code);
94 
95  std::set<irep_idt> aliases;
96  get_rhs_aliases(code_assign.rhs(), aliases);
97  assign_lhs_aliases(code_assign.lhs(), aliases);
98  }
99  break;
100 
101  case DECL:
102  {
103  const code_declt &code_decl=to_code_decl(instruction.code);
104  aliases.isolate(code_decl.get_identifier());
105  }
106  break;
107 
108  case DEAD:
109  {
110  const code_deadt &code_dead=to_code_dead(instruction.code);
111  aliases.isolate(code_dead.get_identifier());
112  }
113  break;
114 
115  default:
116  {
117  }
118  }
119 }
120 
122  std::ostream &out,
123  const ai_baset &ai,
124  const namespacet &ns) const
125 {
126  if(has_values.is_known())
127  {
128  out << has_values.to_string() << '\n';
129  return;
130  }
131 
133  a_it1!=aliases.end();
134  a_it1++)
135  {
136  bool first=true;
137 
139  a_it2!=aliases.end();
140  a_it2++)
141  {
142  if(aliases.is_root(a_it1) && a_it1!=a_it2 &&
143  aliases.same_set(a_it1, a_it2))
144  {
145  if(first)
146  {
147  out << "Aliases: " << *a_it1;
148  first=false;
149  }
150  out << ' ' << *a_it2;
151  }
152  }
153 
154  if(!first)
155  out << '\n';
156  }
157 }
158 
160  const global_may_alias_domaint &b,
161  locationt from,
162  locationt to)
163 {
164  bool changed=has_values.is_false();
166 
167  // do union
169  it!=b.aliases.end(); it++)
170  {
171  irep_idt b_root=b.aliases.find(it);
172 
173  if(!aliases.same_set(*it, b_root))
174  {
175  aliases.make_union(*it, b_root);
176  changed=true;
177  }
178  }
179 
180  // isolate non-tracked ones
181  #if 0
183  it!=aliases.end(); it++)
184  {
185  if(cleanup_map.find(*it)==cleanup_map.end())
186  aliases.isolate(it);
187  }
188  #endif
189 
190  return changed;
191 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
bool is_false() const
Definition: threeval.h:26
iterator end()
Definition: union_find.h:274
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:289
bool merge(const global_may_alias_domaint &b, locationt from, locationt to)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
const irep_idt & get_identifier() const
Definition: std_code.cpp:19
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final override
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:341
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
const irep_idt & get_identifier() const
Definition: std_expr.h:128
static tvt unknown()
Definition: threeval.h:33
void isolate(typename numbering< T >::const_iterator it)
Definition: union_find.h:250
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3201
const T & find(typename numbering< T >::const_iterator it) const
Definition: union_find.h:188
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
iterator begin()
Definition: union_find.h:270
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
const char * to_string() const
Definition: threeval.cpp:13
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
bool same_set(const T &a, const T &b) const
Definition: union_find.h:169
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
A declaration of a local variable.
Definition: std_code.h:253
bool is_known() const
Definition: threeval.h:28
exprt & rhs()
Definition: std_code.h:213
const irep_idt & get_identifier() const
Definition: std_code.cpp:14
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
numbering_typet::const_iterator const_iterator
Definition: union_find.h:147
Definition: ai.h:128
Base class for all expressions.
Definition: expr.h:42
bool is_root(const T &a) const
Definition: union_find.h:218
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
A removal of a local variable.
Definition: std_code.h:305
goto_programt::const_targett locationt
Definition: ai.h:44
bool make_union(const T &a, const T &b)
Definition: union_find.h:150
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
Field-insensitive, location-sensitive, over-approximative escape analysis.
Assignment.
Definition: std_code.h:195