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> rhs_aliases;
113  get_rhs_aliases(code_assign.rhs(), rhs_aliases);
114  assign_lhs_aliases(code_assign.lhs(), rhs_aliases);
115  break;
116  }
117 
118  case DECL:
119  {
120  const code_declt &code_decl = to_code_decl(instruction.code);
121  aliases.isolate(code_decl.get_identifier());
122  break;
123  }
124 
125  case DEAD:
126  {
127  const code_deadt &code_dead = to_code_dead(instruction.code);
128  aliases.isolate(code_dead.get_identifier());
129  break;
130  }
131 
132  case FUNCTION_CALL: // Probably safe
133  case GOTO: // Ignoring the guard is a valid over-approximation
134  break;
135  case CATCH:
136  case THROW:
137  DATA_INVARIANT(false, "Exceptions must be removed before analysis");
138  break;
139  case RETURN:
140  DATA_INVARIANT(false, "Returns must be removed before analysis");
141  break;
142  case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
143  case ATOMIC_END: // Ignoring is a valid over-approximation
144  case LOCATION: // No action required
145  case START_THREAD: // Require a concurrent analysis at higher level
146  case END_THREAD: // Require a concurrent analysis at higher level
147  case ASSERT: // No action required
148  case ASSUME: // Ignoring is a valid over-approximation
149  case SKIP: // No action required
150  case END_FUNCTION: // No action required
151  break;
152  case OTHER:
153  DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
154  break;
155  case INCOMPLETE_GOTO:
156  case NO_INSTRUCTION_TYPE:
157  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
158  break;
159  }
160 }
161 
163  std::ostream &out,
164  const ai_baset &,
165  const namespacet &) const
166 {
167  if(has_values.is_known())
168  {
169  out << has_values.to_string() << '\n';
170  return;
171  }
172 
174  a_it1!=aliases.end();
175  a_it1++)
176  {
177  bool first=true;
178 
180  a_it2!=aliases.end();
181  a_it2++)
182  {
183  if(aliases.is_root(a_it1) && a_it1!=a_it2 &&
184  aliases.same_set(a_it1, a_it2))
185  {
186  if(first)
187  {
188  out << "Aliases: " << *a_it1;
189  first=false;
190  }
191  out << ' ' << *a_it2;
192  }
193  }
194 
195  if(!first)
196  out << '\n';
197  }
198 }
199 
201  const global_may_alias_domaint &b,
202  locationt,
203  locationt)
204 {
205  bool changed=has_values.is_false();
207 
208  // do union
210  it!=b.aliases.end(); it++)
211  {
212  irep_idt b_root=b.aliases.find(it);
213 
214  if(!aliases.same_set(*it, b_root))
215  {
216  aliases.make_union(*it, b_root);
217  changed=true;
218  }
219  }
220 
221  // isolate non-tracked ones
222  #if 0
224  it!=aliases.end(); it++)
225  {
226  if(cleanup_map.find(*it)==cleanup_map.end())
227  aliases.isolate(it);
228  }
229  #endif
230 
231  return changed;
232 }
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:37
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:450
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:272
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:402
exprt
Base class for all expressions.
Definition: expr.h:53
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:200
code_declt::get_identifier
const irep_idt & get_identifier() const
Definition: std_code.h:418
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:92
THROW
@ THROW
Definition: goto_program.h:50
coverage_criteriont::LOCATION
@ LOCATION
GOTO
@ GOTO
Definition: goto_program.h:34
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
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:2823
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:519
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
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:312
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
OTHER
@ OTHER
Definition: goto_program.h:37
irept::id
const irep_idt & id() const
Definition: irep.h:418
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
tvt::to_string
const char * to_string() const
Definition: threeval.cpp:13
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:42
SKIP
@ SKIP
Definition: goto_program.h:38
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:467
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
RETURN
@ RETURN
Definition: goto_program.h:45
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:76
union_find::make_union
bool make_union(const T &a, const T &b)
Definition: union_find.h:154
CATCH
@ CATCH
Definition: goto_program.h:51
DECL
@ DECL
Definition: goto_program.h:47
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
ASSUME
@ ASSUME
Definition: goto_program.h:35
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
START_THREAD
@ START_THREAD
Definition: goto_program.h:39
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
global_may_alias_domaint
Definition: global_may_alias.h:25
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:44
DEAD
@ DEAD
Definition: goto_program.h:48
code_deadt::get_identifier
const irep_idt & get_identifier() const
Definition: std_code.h:483
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:43
global_may_alias.h
Field-insensitive, location-sensitive, over-approximative escape analysis.
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:295
ASSERT
@ ASSERT
Definition: goto_program.h:36
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
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:162
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
END_THREAD
@ END_THREAD
Definition: goto_program.h:40
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
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