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 
14 #include <util/pointer_expr.h>
15 
22  const exprt &lhs,
23  const std::set<irep_idt> &alias_set)
24 {
25  if(lhs.id()==ID_symbol)
26  {
27  irep_idt identifier=to_symbol_expr(lhs).get_identifier();
28 
29  aliases.isolate(identifier);
30 
31  for(const auto &alias : alias_set)
32  {
33  aliases.make_union(identifier, alias);
34  }
35  }
36 }
37 
44  const exprt &rhs,
45  std::set<irep_idt> &alias_set)
46 {
47  if(rhs.id()==ID_symbol)
48  {
49  irep_idt identifier=to_symbol_expr(rhs).get_identifier();
50  alias_set.insert(identifier);
51 
52  for(const auto &alias : alias_set)
53  if(aliases.same_set(alias, identifier))
54  alias_set.insert(alias);
55  }
56  else if(rhs.id()==ID_if)
57  {
58  get_rhs_aliases(to_if_expr(rhs).true_case(), alias_set);
59  get_rhs_aliases(to_if_expr(rhs).false_case(), alias_set);
60  }
61  else if(rhs.id()==ID_typecast)
62  {
63  get_rhs_aliases(to_typecast_expr(rhs).op(), alias_set);
64  }
65  else if(rhs.id()==ID_address_of)
66  {
67  get_rhs_aliases_address_of(to_address_of_expr(rhs).object(), alias_set);
68  }
69 }
70 
77  const exprt &rhs,
78  std::set<irep_idt> &alias_set)
79 {
80  if(rhs.id()==ID_symbol)
81  {
82  irep_idt identifier=to_symbol_expr(rhs).get_identifier();
83  alias_set.insert("&"+id2string(identifier));
84  }
85  else if(rhs.id()==ID_if)
86  {
87  get_rhs_aliases_address_of(to_if_expr(rhs).true_case(), alias_set);
88  get_rhs_aliases_address_of(to_if_expr(rhs).false_case(), alias_set);
89  }
90  else if(rhs.id()==ID_dereference)
91  {
92  }
93 }
94 
96  const irep_idt &function_from,
97  trace_ptrt trace_from,
98  const irep_idt &function_to,
99  trace_ptrt trace_to,
100  ai_baset &ai,
101  const namespacet &ns)
102 {
103  locationt from{trace_from->current_location()};
104 
105  if(has_values.is_false())
106  return;
107 
108  const goto_programt::instructiont &instruction=*from;
109 
110  switch(instruction.type)
111  {
112  case ASSIGN:
113  {
114  const code_assignt &code_assign = instruction.get_assign();
115 
116  std::set<irep_idt> rhs_aliases;
117  get_rhs_aliases(code_assign.rhs(), rhs_aliases);
118  assign_lhs_aliases(code_assign.lhs(), rhs_aliases);
119  break;
120  }
121 
122  case DECL:
123  aliases.isolate(instruction.decl_symbol().get_identifier());
124  break;
125 
126  case DEAD:
127  aliases.isolate(instruction.dead_symbol().get_identifier());
128  break;
129 
130  case FUNCTION_CALL: // Probably safe
131  case GOTO: // Ignoring the guard is a valid over-approximation
132  break;
133  case CATCH:
134  case THROW:
135  DATA_INVARIANT(false, "Exceptions must be removed before analysis");
136  break;
137  case RETURN:
138  DATA_INVARIANT(false, "Returns must be removed before analysis");
139  break;
140  case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
141  case ATOMIC_END: // Ignoring is a valid over-approximation
142  case LOCATION: // No action required
143  case START_THREAD: // Require a concurrent analysis at higher level
144  case END_THREAD: // Require a concurrent analysis at higher level
145  case ASSERT: // No action required
146  case ASSUME: // Ignoring is a valid over-approximation
147  case SKIP: // No action required
148  case END_FUNCTION: // No action required
149  break;
150  case OTHER:
151  DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
152  break;
153  case INCOMPLETE_GOTO:
154  case NO_INSTRUCTION_TYPE:
155  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
156  break;
157  }
158 }
159 
161  std::ostream &out,
162  const ai_baset &,
163  const namespacet &) const
164 {
165  if(has_values.is_known())
166  {
167  out << has_values.to_string() << '\n';
168  return;
169  }
170 
172  a_it1!=aliases.end();
173  a_it1++)
174  {
175  bool first=true;
176 
178  a_it2!=aliases.end();
179  a_it2++)
180  {
181  if(aliases.is_root(a_it1) && a_it1!=a_it2 &&
182  aliases.same_set(a_it1, a_it2))
183  {
184  if(first)
185  {
186  out << "Aliases: " << *a_it1;
187  first=false;
188  }
189  out << ' ' << *a_it2;
190  }
191  }
192 
193  if(!first)
194  out << '\n';
195  }
196 }
197 
199  const global_may_alias_domaint &b,
200  trace_ptrt,
201  trace_ptrt)
202 {
203  bool changed=has_values.is_false();
205 
206  // do union
208  it!=b.aliases.end(); it++)
209  {
210  irep_idt b_root=b.aliases.find(it);
211 
212  if(!aliases.same_set(*it, b_root))
213  {
214  aliases.make_union(*it, b_root);
215  changed=true;
216  }
217  }
218 
219  // isolate non-tracked ones
220  #if 0
222  it!=aliases.end(); it++)
223  {
224  if(cleanup_map.find(*it)==cleanup_map.end())
225  aliases.isolate(it);
226  }
227  #endif
228 
229  return changed;
230 }
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:21
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
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:2151
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:350
exprt
Base class for all expressions.
Definition: expr.h:54
goto_programt::instructiont::decl_symbol
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:225
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
goto_programt::instructiont::get_assign
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:199
tvt::is_known
bool is_known() const
Definition: threeval.h:28
global_may_alias_domaint::aliases
aliasest aliases
Definition: global_may_alias.h:89
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:51
GOTO
@ GOTO
Definition: goto_program.h:35
union_find::make_union
bool make_union(const T &a, const T &b)
Definition: union_find.h:155
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
goto_programt::instructiont::dead_symbol
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:267
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
union_find::find
const T & find(const_iterator it) const
Definition: union_find.h:191
union_find< irep_idt >::const_iterator
typename numbering_typet::const_iterator const_iterator
Definition: union_find.h:152
global_may_alias_domaint::transform
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
Abstract Interpretation domain transform function.
Definition: global_may_alias.cpp:95
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:34
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
union_find::isolate
void isolate(const_iterator it)
Definition: union_find.h:253
OTHER
@ OTHER
Definition: goto_program.h:38
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:43
SKIP
@ SKIP
Definition: goto_program.h:39
tvt::is_false
bool is_false() const
Definition: threeval.h:26
global_may_alias_domaint::has_values
tvt has_values
Definition: global_may_alias.h:92
RETURN
@ RETURN
Definition: goto_program.h:46
ASSIGN
@ ASSIGN
Definition: goto_program.h:47
union_find::same_set
bool same_set(const T &a, const T &b) const
Definition: union_find.h:173
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:77
union_find::is_root
bool is_root(const T &a) const
Definition: union_find.h:221
CATCH
@ CATCH
Definition: goto_program.h:52
DECL
@ DECL
Definition: goto_program.h:48
ASSUME
@ ASSUME
Definition: goto_program.h:36
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
union_find::begin
iterator begin()
Definition: union_find.h:273
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
START_THREAD
@ START_THREAD
Definition: goto_program.h:40
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:50
global_may_alias_domaint
Definition: global_may_alias.h:25
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:45
union_find::end
iterator end()
Definition: union_find.h:277
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:367
DEAD
@ DEAD
Definition: goto_program.h:49
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:44
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:76
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
LOCATION
@ LOCATION
Definition: goto_program.h:42
global_may_alias_domaint::merge
bool merge(const global_may_alias_domaint &b, trace_ptrt from, trace_ptrt to)
Abstract Interpretation domain merge function.
Definition: global_may_alias.cpp:198
ASSERT
@ ASSERT
Definition: goto_program.h:37
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
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:160
END_THREAD
@ END_THREAD
Definition: goto_program.h:41
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:53
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:43