CBMC
Loading...
Searching...
No Matches
global_may_alias.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-insensitive, location-sensitive global may alias analysis
4
5Author: 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 {
64 }
65 else if(rhs.id()==ID_address_of)
66 {
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 {
89 }
90 else if(rhs.id()==ID_dereference)
91 {
92 }
93}
94
98 const irep_idt &function_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 std::set<irep_idt> rhs_aliases;
115 get_rhs_aliases(instruction.assign_rhs(), rhs_aliases);
117 break;
118 }
119
120 case DECL:
121 aliases.isolate(instruction.decl_symbol().get_identifier());
122 break;
123
124 case DEAD:
125 aliases.isolate(instruction.dead_symbol().get_identifier());
126 break;
127
128 case FUNCTION_CALL: // Probably safe
129 case GOTO: // Ignoring the guard is a valid over-approximation
130 break;
131 case CATCH:
132 case THROW:
133 DATA_INVARIANT(false, "Exceptions must be removed before analysis");
134 break;
135 case SET_RETURN_VALUE:
136 DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
137 break;
138 case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
139 case ATOMIC_END: // Ignoring is a valid over-approximation
140 case LOCATION: // No action required
141 case START_THREAD: // Require a concurrent analysis at higher level
142 case END_THREAD: // Require a concurrent analysis at higher level
143 case ASSERT: // No action required
144 case ASSUME: // Ignoring is a valid over-approximation
145 case SKIP: // No action required
146 case END_FUNCTION: // No action required
147 break;
148 case OTHER:
149 DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
150 break;
151 case INCOMPLETE_GOTO:
153 DATA_INVARIANT(false, "Only complete instructions can be analyzed");
154 break;
155 }
156}
157
159 std::ostream &out,
160 const ai_baset &,
161 const namespacet &) const
162{
163 if(has_values.is_known())
164 {
165 out << has_values.to_string() << '\n';
166 return;
167 }
168
170 a_it1!=aliases.end();
171 a_it1++)
172 {
173 bool first=true;
174
176 a_it2!=aliases.end();
177 a_it2++)
178 {
179 if(aliases.is_root(a_it1) && a_it1!=a_it2 &&
181 {
182 if(first)
183 {
184 out << "Aliases: " << *a_it1;
185 first=false;
186 }
187 out << ' ' << *a_it2;
188 }
189 }
190
191 if(!first)
192 out << '\n';
193 }
194}
195
200{
201 bool changed=has_values.is_false();
203
204 // do union
205 for(aliasest::const_iterator it=b.aliases.begin();
206 it!=b.aliases.end(); it++)
207 {
208 irep_idt b_root=b.aliases.find(it);
209
210 if(!aliases.same_set(*it, b_root))
211 {
213 changed=true;
214 }
215 }
216
217 // isolate non-tracked ones
218 #if 0
220 it!=aliases.end(); it++)
221 {
222 if(cleanup_map.find(*it)==cleanup_map.end())
223 aliases.isolate(it);
224 }
225 #endif
226
227 return changed;
228}
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:73
goto_programt::const_targett locationt
Definition ai_domain.h:72
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
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.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Abstract Interpretation domain output function.
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.
bool merge(const global_may_alias_domaint &b, trace_ptrt from, trace_ptrt to)
Abstract Interpretation domain merge function.
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.
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.
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
goto_program_instruction_typet type() const
What kind of instruction?
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool is_known() const
Definition threeval.h:28
const char * to_string() const
Definition threeval.cpp:13
bool is_false() const
Definition threeval.h:26
static tvt unknown()
Definition threeval.h:33
void isolate(const_iterator it)
Definition union_find.h:253
bool make_union(const T &a, const T &b)
Definition union_find.h:155
iterator begin()
Definition union_find.h:273
bool same_set(const T &a, const T &b) const
Definition union_find.h:173
typename numbering_typet::const_iterator const_iterator
Definition union_find.h:152
bool is_root(const T &a) const
Definition union_find.h:221
iterator end()
Definition union_find.h:277
Field-insensitive, location-sensitive, over-approximative escape analysis.
@ FUNCTION_CALL
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2582
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272