cprover
Loading...
Searching...
No Matches
may_alias.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Solver
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#include "may_alias.h"
13
14#include <util/c_types.h>
15#include <util/namespace.h>
16#include <util/pointer_expr.h>
17#include <util/prefix.h>
18#include <util/std_expr.h>
19#include <util/symbol.h>
20
22{
23 // C99; ISO/IEC 9899:1999 6.5/7
24 if(a == b)
25 return true;
26 else if(a == signed_char_type() || a == unsigned_char_type())
27 return true; // char * can alias anyting
28 else if(b == signed_char_type() || b == unsigned_char_type())
29 return true; // char * can alias anyting
30 else if(
31 (a.id() == ID_unsignedbv || a.id() == ID_signedbv) &&
32 (b.id() == ID_unsignedbv || b.id() == ID_signedbv))
33 {
34 // signed/unsigned of same width can alias
36 }
37 else if(a.id() == ID_empty)
38 return true; // void * can alias any pointer
39 else if(b.id() == ID_empty)
40 return true; // void * can alias any pointer
41 else if(
42 a.id() == ID_pointer && to_pointer_type(a).base_type().id() == ID_empty)
43 return true; // void * can alias any pointer
44 else if(
45 b.id() == ID_pointer && to_pointer_type(b).base_type().id() == ID_empty)
46 return true; // void * can alias any pointer
47 else if(
48 a.id() == ID_pointer && to_pointer_type(a).base_type().id() == ID_pointer &&
49 to_pointer_type(to_pointer_type(a).base_type()).base_type().id() ==
50 ID_empty)
51 return true; // void * can alias any pointer
52 else if(
53 b.id() == ID_pointer && to_pointer_type(b).base_type().id() == ID_pointer &&
54 to_pointer_type(to_pointer_type(b).base_type()).base_type().id() ==
55 ID_empty)
56 return true; // void * can alias any pointer
57 else
58 {
59 return false;
60 }
61}
62
64{
65 if(expr.id() == ID_object_address)
66 return true;
67 else if(expr.id() == ID_element_address)
69 else if(expr.id() == ID_field_address)
71 else
72 return false;
73}
74
75bool prefix_of(const typet &a, const typet &b, const namespacet &ns)
76{
77 if(a == b)
78 return true;
79
80 if(a.id() == ID_struct_tag)
81 return prefix_of(ns.follow_tag(to_struct_tag_type(a)), b, ns);
82
83 if(b.id() == ID_struct_tag)
84 return prefix_of(a, ns.follow_tag(to_struct_tag_type(b)), ns);
85
86 if(a.id() != ID_struct || b.id() != ID_struct)
87 return false;
88
89 const auto &a_struct = to_struct_type(a);
90 const auto &b_struct = to_struct_type(b);
91
92 return a_struct.is_prefix_of(b_struct) || b_struct.is_prefix_of(a_struct);
93}
94
96{
97 if(expr.id() == ID_object_address)
98 return to_object_address_expr(expr);
99 else if(expr.id() == ID_field_address)
100 return find_object(to_field_address_expr(expr).base());
101 else if(expr.id() == ID_element_address)
102 return find_object(to_element_address_expr(expr).base());
103 else
104 return {};
105}
106
107// Is 'expr' on the stack and it's address is not taken?
109 const exprt &expr,
110 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
111 const namespacet &ns)
112{
113 auto object = find_object(expr);
114 if(object.has_value())
115 {
116 auto symbol_expr = object->object_expr();
117 auto identifier = symbol_expr.get_identifier();
118 if(has_prefix(id2string(identifier), "va_arg::"))
119 return true; // on the stack, and might alias
120 else if(has_prefix(id2string(identifier), "var_args::"))
121 return false; // on the stack -- can take address?
122 else if(has_prefix(id2string(identifier), "va_args::"))
123 return false; // on the stack -- can take address?
124 else if(has_prefix(id2string(identifier), "va_arg_array::"))
125 return false; // on the stack -- can take address?
126 else if(has_prefix(id2string(identifier), "old::"))
127 return true; // on the stack, but can't take address
128 else if(identifier == "return_value")
129 return true; // on the stack, but can't take address
130 const auto &symbol = ns.lookup(symbol_expr);
131 return !symbol.is_static_lifetime &&
132 address_taken.find(symbol_expr) == address_taken.end();
133 }
134 else
135 return false;
136}
137
139{
140 if(
141 src.id() == ID_typecast &&
142 to_typecast_expr(src).op().type().id() == ID_pointer)
144 else
145 return src;
146}
147
149same_address(const exprt &a, const exprt &b, const namespacet &ns)
150{
151 static const auto true_expr = true_exprt();
152 static const auto false_expr = false_exprt();
153
154 // syntactically the same?
156 return true_expr;
157
158 // a and b are both object/field/element?
160 {
161 if(a.id() == ID_object_address && b.id() == ID_object_address)
162 {
163 if(
164 to_object_address_expr(a).object_identifier() ==
165 to_object_address_expr(b).object_identifier())
166 {
167 return true_expr; // the same
168 }
169 else
170 return false_expr; // different
171 }
172 else if(a.id() == ID_element_address && b.id() == ID_element_address)
173 {
174 const auto &a_element_address = to_element_address_expr(a);
175 const auto &b_element_address = to_element_address_expr(b);
176
177 // rec. call
178 auto base_same_address =
179 same_address(a_element_address.base(), b_element_address.base(), ns);
180
181 CHECK_RETURN(base_same_address.has_value());
182
183 if(base_same_address->is_false())
184 return false_expr;
185 else
186 {
187 return and_exprt(
188 *base_same_address,
189 equal_exprt(a_element_address.index(), b_element_address.index()));
190 }
191 }
192 else if(a.id() == ID_field_address && b.id() == ID_field_address)
193 {
194 const auto &a_field_address = to_field_address_expr(a);
195 const auto &b_field_address = to_field_address_expr(b);
196
197 // structs can't alias unless one is a prefix of the other
198 if(!prefix_of(
199 a_field_address.type().base_type(),
200 b_field_address.type().base_type(),
201 ns))
202 {
203 return false_expr;
204 }
205
206 if(a_field_address.component_name() == b_field_address.component_name())
207 {
208 // rec. call
209 return same_address(a_field_address.base(), b_field_address.base(), ns);
210 }
211 else
212 return false_expr;
213 }
214 else
215 return false_expr;
216 }
217
218 // don't know
219 return {};
220}
221
223 const exprt &a,
224 const exprt &b,
225 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
226 const namespacet &ns)
227{
228 PRECONDITION(a.type().id() == ID_pointer);
229 PRECONDITION(b.type().id() == ID_pointer);
230
231 static const auto true_expr = true_exprt();
232 static const auto false_expr = false_exprt();
233
234 // syntactically the same?
236 return true_expr;
237
238 // consider the strict aliasing rule
239 const auto &a_base = to_pointer_type(a.type()).base_type();
240 const auto &b_base = to_pointer_type(b.type()).base_type();
241
242 if(!permitted_by_strict_aliasing(a_base, b_base))
243 {
244 // The object is known to be different, because of strict aliasing.
245 return false_expr;
246 }
247
248 // a and b the same addresses?
249 auto same_address_opt = same_address(a, b, ns);
250 if(same_address_opt.has_value())
251 return same_address_opt;
252
253 // is one of them stack-allocated and it's address is not taken?
255 return false_expr; // can't alias
256
258 return false_expr; // can't alias
259
260 // we don't know
261 return {};
262}
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
signedbv_typet signed_char_type()
Definition c_types.cpp:139
unsignedbv_typet unsigned_char_type()
Definition c_types.cpp:132
Boolean AND.
Definition std_expr.h:2071
std::size_t get_width() const
Definition std_types.h:876
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3017
const irep_idt & id() const
Definition irep.h:396
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const typet & base_type() const
The type of the data what we point to.
The Boolean constant true.
Definition std_expr.h:3008
The type of an expression, extends irept.
Definition type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
bool permitted_by_strict_aliasing(const typet &a, const typet &b)
Definition may_alias.cpp:21
bool prefix_of(const typet &a, const typet &b, const namespacet &ns)
Definition may_alias.cpp:75
optionalt< exprt > same_address(const exprt &a, const exprt &b, const namespacet &ns)
static optionalt< object_address_exprt > find_object(const exprt &expr)
Definition may_alias.cpp:95
static exprt drop_pointer_typecasts(exprt src)
bool is_object_field_element(const exprt &expr)
Definition may_alias.cpp:63
optionalt< exprt > may_alias(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
bool stack_and_not_dirty(const exprt &expr, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
May Alias.
nonstd::optional< T > optionalt
Definition optional.h:35
API to expression classes for Pointers.
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
Symbol table entry.