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 
20  const exprt &lhs,
21  const std::set<irep_idt> &alias_set)
22 {
23  if(lhs.id()==ID_symbol)
24  {
25  irep_idt identifier=to_symbol_expr(lhs).get_identifier();
26 
27  aliases.isolate(identifier);
28 
29  for(const auto &alias : alias_set)
30  {
31  aliases.make_union(identifier, alias);
32  }
33  }
34 }
35 
42  const exprt &rhs,
43  std::set<irep_idt> &alias_set)
44 {
45  if(rhs.id()==ID_symbol)
46  {
47  irep_idt identifier=to_symbol_expr(rhs).get_identifier();
48  alias_set.insert(identifier);
49 
50  for(const auto &alias : alias_set)
51  if(aliases.same_set(alias, identifier))
52  alias_set.insert(alias);
53  }
54  else if(rhs.id()==ID_if)
55  {
56  get_rhs_aliases(to_if_expr(rhs).true_case(), alias_set);
57  get_rhs_aliases(to_if_expr(rhs).false_case(), alias_set);
58  }
59  else if(rhs.id()==ID_typecast)
60  {
61  get_rhs_aliases(to_typecast_expr(rhs).op(), alias_set);
62  }
63  else if(rhs.id()==ID_address_of)
64  {
65  get_rhs_aliases_address_of(to_address_of_expr(rhs).object(), alias_set);
66  }
67 }
68 
75  const exprt &rhs,
76  std::set<irep_idt> &alias_set)
77 {
78  if(rhs.id()==ID_symbol)
79  {
80  irep_idt identifier=to_symbol_expr(rhs).get_identifier();
81  alias_set.insert("&"+id2string(identifier));
82  }
83  else if(rhs.id()==ID_if)
84  {
85  get_rhs_aliases_address_of(to_if_expr(rhs).true_case(), alias_set);
86  get_rhs_aliases_address_of(to_if_expr(rhs).false_case(), alias_set);
87  }
88  else if(rhs.id()==ID_dereference)
89  {
90  }
91 }
92 
94  const irep_idt &,
95  locationt from,
96  const irep_idt &,
97  locationt,
98  ai_baset &,
99  const namespacet &)
100 {
101  if(has_values.is_false())
102  return;
103 
104  const goto_programt::instructiont &instruction=*from;
105 
106  switch(instruction.type)
107  {
108  case ASSIGN:
109  {
110  const code_assignt &code_assign=to_code_assign(instruction.code);
111 
112  std::set<irep_idt> aliases;
113  get_rhs_aliases(code_assign.rhs(), aliases);
114  assign_lhs_aliases(code_assign.lhs(), aliases);
115  }
116  break;
117 
118  case DECL:
119  {
120  const code_declt &code_decl=to_code_decl(instruction.code);
121  aliases.isolate(code_decl.get_identifier());
122  }
123  break;
124 
125  case DEAD:
126  {
127  const code_deadt &code_dead=to_code_dead(instruction.code);
128  aliases.isolate(code_dead.get_identifier());
129  }
130  break;
131 
132  default:
133  {
134  }
135  }
136 }
137 
139  std::ostream &out,
140  const ai_baset &,
141  const namespacet &) const
142 {
143  if(has_values.is_known())
144  {
145  out << has_values.to_string() << '\n';
146  return;
147  }
148 
150  a_it1!=aliases.end();
151  a_it1++)
152  {
153  bool first=true;
154 
156  a_it2!=aliases.end();
157  a_it2++)
158  {
159  if(aliases.is_root(a_it1) && a_it1!=a_it2 &&
160  aliases.same_set(a_it1, a_it2))
161  {
162  if(first)
163  {
164  out << "Aliases: " << *a_it1;
165  first=false;
166  }
167  out << ' ' << *a_it2;
168  }
169  }
170 
171  if(!first)
172  out << '\n';
173  }
174 }
175 
177  const global_may_alias_domaint &b,
178  locationt,
179  locationt)
180 {
181  bool changed=has_values.is_false();
183 
184  // do union
186  it!=b.aliases.end(); it++)
187  {
188  irep_idt b_root=b.aliases.find(it);
189 
190  if(!aliases.same_set(*it, b_root))
191  {
192  aliases.make_union(*it, b_root);
193  changed=true;
194  }
195  }
196 
197  // isolate non-tracked ones
198  #if 0
200  it!=aliases.end(); it++)
201  {
202  if(cleanup_map.find(*it)==cleanup_map.end())
203  aliases.isolate(it);
204  }
205  #endif
206 
207  return changed;
208 }
global_may_alias_domaint::assign_lhs_aliases
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
Populate list of aliases for a given identifier in a context in which an object is being written to.
Definition: global_may_alias.cpp:19
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
union_find::isolate
void isolate(typename numbering< T >::const_iterator it)
Definition: union_find.h:254
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:274
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:190
union_find::begin
iterator begin()
Definition: union_find.h:274
union_find::end
iterator end()
Definition: union_find.h:278
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
exprt
Base class for all expressions.
Definition: expr.h:54
global_may_alias_domaint::merge
bool merge(const global_may_alias_domaint &b, locationt from, locationt to)
Abstract Interpretation domain merge function.
Definition: global_may_alias.cpp:176
code_declt::get_identifier
const irep_idt & get_identifier() const
Definition: std_code.h:370
union_find::find
const T & find(typename numbering< T >::const_iterator it) const
Definition: union_find.h:192
tvt::is_known
bool is_known() const
Definition: threeval.h:28
global_may_alias_domaint::aliases
aliasest aliases
Definition: global_may_alias.h:92
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::instructiont::code
codet code
Definition: goto_program.h:181
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:473
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
union_find::same_set
bool same_set(const T &a, const T &b) const
Definition: union_find.h:173
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
tvt::to_string
const char * to_string() const
Definition: threeval.cpp:13
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:424
tvt::is_false
bool is_false() const
Definition: threeval.h:26
union_find::is_root
bool is_root(const T &a) const
Definition: union_find.h:222
global_may_alias_domaint::has_values
tvt has_values
Definition: global_may_alias.h:95
union_find< irep_idt >::const_iterator
numbering_typet::const_iterator const_iterator
Definition: union_find.h:151
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:40
union_find::make_union
bool make_union(const T &a, const T &b)
Definition: union_find.h:154
DECL
@ DECL
Definition: goto_program.h:47
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
ai_baset
The basic interface of an abstract interpreter.
Definition: ai.h:32
global_may_alias_domaint
Definition: global_may_alias.h:24
DEAD
@ DEAD
Definition: goto_program.h:48
code_deadt::get_identifier
const irep_idt & get_identifier() const
Definition: std_code.h:442
global_may_alias.h
global_may_alias_domaint::get_rhs_aliases_address_of
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
Specialisation of global_may_alias_domaint::get_rhs_aliases to deal with address_of expressions.
Definition: global_may_alias.cpp:74
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
global_may_alias_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Abstract Interpretation domain output function.
Definition: global_may_alias.cpp:138
global_may_alias_domaint::transform
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
Abstract Interpretation domain transform function.
Definition: global_may_alias.cpp:93
global_may_alias_domaint::get_rhs_aliases
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
Populate list of aliases for a given identifier in a context in which is an object is being read.
Definition: global_may_alias.cpp:41