CBMC: /home/runner/work/cbmc/cbmc/src/cprover/may_alias.cpp Source File

20 bool permitted_by_strict_aliasing(const typet &a, const typet &b)

21{

22 // C99; ISO/IEC 9899:1999 6.5/7

23 if(a == b)

24 return true;

25 else if(a == signed_char_type() || a == unsigned_char_type())

26 return true; // char * can alias anyting

27 else if(b == signed_char_type() || b == unsigned_char_type())

28 return true; // char * can alias anyting

29 else if(

30 (a.id() == ID_unsignedbv || a.id() == ID_signedbv) &&

31 (b.id() == ID_unsignedbv || b.id() == ID_signedbv))

32 {

33 // signed/unsigned of same width can alias

34 return to_bitvector_type(a).get_width() == to_bitvector_type(b).get_width();

35 }

36 else if(a.id() == ID_empty)

37 return true; // void * can alias any pointer

38 else if(b.id() == ID_empty)

39 return true; // void * can alias any pointer

40 else if(

41 a.id() == ID_pointer && to_pointer_type(a).base_type().id() == ID_empty)

42 return true; // void * can alias any pointer

43 else if(

44 b.id() == ID_pointer && to_pointer_type(b).base_type().id() == ID_empty)

45 return true; // void * can alias any pointer

46 else if(

47 a.id() == ID_pointer && to_pointer_type(a).base_type().id() == ID_pointer &&

48 to_pointer_type(to_pointer_type(a).base_type()).base_type().id() ==

49 ID_empty)

50 return true; // void * can alias any pointer

51 else if(

52 b.id() == ID_pointer && to_pointer_type(b).base_type().id() == ID_pointer &&

53 to_pointer_type(to_pointer_type(b).base_type()).base_type().id() ==

54 ID_empty)

55 return true; // void * can alias any pointer

56 else

57 {

58 return false;

59 }

60}

62 bool is_object_field_element(const exprt &expr)

63{

64 if(expr.id() == ID_object_address)

65 return true;

66 else if(expr.id() == ID_element_address)

67 return is_object_field_element(to_element_address_expr(expr).base());

68 else if(expr.id() == ID_field_address)

69 return is_object_field_element(to_field_address_expr(expr).base());

70 else

71 return false;

72}

74 bool prefix_of(const typet &a, const typet &b, const namespacet &ns)

75{

76 if(a == b)

77 return true;

78

79 if(a.id() == ID_struct_tag)

80 return prefix_of(ns.follow_tag(to_struct_tag_type(a)), b, ns);

81

82 if(b.id() == ID_struct_tag)

83 return prefix_of(a, ns.follow_tag(to_struct_tag_type(b)), ns);

84

85 if(a.id() != ID_struct || b.id() != ID_struct)

86 return false;

87

88 const auto &a_struct = to_struct_type(a);

89 const auto &b_struct = to_struct_type(b);

90

91 return a_struct.is_prefix_of(b_struct) || b_struct.is_prefix_of(a_struct);

92}

94 static std::optional<object_address_exprt> find_object(const exprt &expr)

95{

96 if(expr.id() == ID_object_address)

97 return to_object_address_expr(expr);

98 else if(expr.id() == ID_field_address)

99 return find_object(to_field_address_expr(expr).base());

100 else if(expr.id() == ID_element_address)

101 return find_object(to_element_address_expr(expr).base());

102 else

103 return {};

104}

107 bool stack_and_not_dirty(

108 const exprt &expr,

109 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,

110 const namespacet &ns)

111{

112 auto object = find_object(expr);

113 if(object.has_value())

114 {

115 auto symbol_expr = object->object_expr();

116 auto identifier = symbol_expr.identifier();

117 if(identifier.starts_with("va_arg::"))

118 return true; // on the stack, and might alias

119 else if(identifier.starts_with("var_args::"))

120 return false; // on the stack -- can take address?

121 else if(identifier.starts_with("va_args::"))

122 return false; // on the stack -- can take address?

123 else if(identifier.starts_with("va_arg_array::"))

124 return false; // on the stack -- can take address?

125 else if(identifier.starts_with("old::"))

126 return true; // on the stack, but can't take address

127 else if(identifier == "return_value")

128 return true; // on the stack, but can't take address

129 const auto &symbol = ns.lookup(symbol_expr);

130 return !symbol.is_static_lifetime &&

131 address_taken.find(symbol_expr) == address_taken.end();

132 }

133 else

134 return false;

135}

137 static exprt drop_pointer_typecasts(exprt src)

138{

139 if(

140 src.id() == ID_typecast &&

141 to_typecast_expr(src).op().type().id() == ID_pointer)

142 return drop_pointer_typecasts(to_typecast_expr(src).op());

143 else

144 return src;

145}

148 same_address(const exprt &a, const exprt &b, const namespacet &ns)

149{

150 static const auto true_expr = true_exprt();

151 static const auto false_expr = false_exprt();

152

153 // syntactically the same?

154 if(drop_pointer_typecasts(a) == drop_pointer_typecasts(b))

155 return true_expr;

156

157 // a and b are both object/field/element?

158 if(is_object_field_element(a) && is_object_field_element(b))

159 {

160 if(a.id() == ID_object_address && b.id() == ID_object_address)

161 {

162 if(

163 to_object_address_expr(a).object_identifier() ==

164 to_object_address_expr(b).object_identifier())

165 {

166 return true_expr; // the same

167 }

168 else

169 return false_expr; // different

170 }

171 else if(a.id() == ID_element_address && b.id() == ID_element_address)

172 {

173 const auto &a_element_address = to_element_address_expr(a);

174 const auto &b_element_address = to_element_address_expr(b);

175

176 // rec. call

177 auto base_same_address =

178 same_address(a_element_address.base(), b_element_address.base(), ns);

179

180 CHECK_RETURN(base_same_address.has_value());

181

182 if(*base_same_address == false)

183 return false_expr;

184 else

185 {

186 return and_exprt(

187 *base_same_address,

188 equal_exprt(a_element_address.index(), b_element_address.index()));

189 }

190 }

191 else if(a.id() == ID_field_address && b.id() == ID_field_address)

192 {

193 const auto &a_field_address = to_field_address_expr(a);

194 const auto &b_field_address = to_field_address_expr(b);

195

196 // structs can't alias unless one is a prefix of the other

197 if(!prefix_of(

198 a_field_address.type().base_type(),

199 b_field_address.type().base_type(),

200 ns))

201 {

202 return false_expr;

203 }

204

205 if(a_field_address.component_name() == b_field_address.component_name())

206 {

207 // rec. call

208 return same_address(a_field_address.base(), b_field_address.base(), ns);

209 }

210 else

211 return false_expr;

212 }

213 else

214 return false_expr;

215 }

216

217 // don't know

218 return {};

219}

221 std::optional<exprt> may_alias(

222 const exprt &a,

223 const exprt &b,

224 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,

225 const namespacet &ns)

226{

227 PRECONDITION(a.type().id() == ID_pointer);

228 PRECONDITION(b.type().id() == ID_pointer);

229

230 static const auto true_expr = true_exprt();

231 static const auto false_expr = false_exprt();

232

233 // syntactically the same?

234 if(drop_pointer_typecasts(a) == drop_pointer_typecasts(b))

235 return true_expr;

236

237 // consider the strict aliasing rule

238 const auto &a_base = to_pointer_type(a.type()).base_type();

239 const auto &b_base = to_pointer_type(b.type()).base_type();

240

241 if(!permitted_by_strict_aliasing(a_base, b_base))

242 {

243 // The object is known to be different, because of strict aliasing.

244 return false_expr;

245 }

246

247 // a and b the same addresses?

248 auto same_address_opt = same_address(a, b, ns);

249 if(same_address_opt.has_value())

250 return same_address_opt;

251

252 // is one of them stack-allocated and it's address is not taken?

253 if(stack_and_not_dirty(a, address_taken, ns))

254 return false_expr; // can't alias

255

256 if(stack_and_not_dirty(b, address_taken, ns))

257 return false_expr; // can't alias

258

259 // we don't know

260 return {};

261}

address_taken

std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)

Definition address_taken.cpp:51

to_bitvector_type

const bitvector_typet & to_bitvector_type(const typet &type)

Cast a typet to a bitvector_typet.

Definition bitvector_types.h:99

signed_char_type

signedbv_typet signed_char_type()

Definition c_types.cpp:134

unsigned_char_type

unsignedbv_typet unsigned_char_type()

Definition c_types.cpp:127

c_types.h

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

and_exprt

Boolean AND All operands must be boolean, and the result is always boolean.

Definition std_expr.h:2043

equal_exprt

Equality.

Definition std_expr.h:1339

exprt

Base class for all expressions.

Definition expr.h:57

false_exprt

The Boolean constant false.

Definition std_expr.h:3135

irept::id

const irep_idt & id() const

Definition irep.h:388

namespace_baset::follow_tag

const union_typet & follow_tag(const union_tag_typet &) const

Follow type tag of union type.

Definition namespace.cpp:49

namespacet

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...

Definition namespace.h:91

namespacet::lookup

bool lookup(const irep_idt &name, const symbolt *&symbol) const override

See documentation for namespace_baset::lookup().

Definition namespace.cpp:134

true_exprt

The Boolean constant true.

Definition std_expr.h:3126

typet

The type of an expression, extends irept.

Definition type.h:29

same_address

std::optional< exprt > same_address(const exprt &a, const exprt &b, const namespacet &ns)

Definition may_alias.cpp:148

find_object

static std::optional< object_address_exprt > find_object(const exprt &expr)

Definition may_alias.cpp:94

permitted_by_strict_aliasing

bool permitted_by_strict_aliasing(const typet &a, const typet &b)

Definition may_alias.cpp:20

prefix_of

bool prefix_of(const typet &a, const typet &b, const namespacet &ns)

Definition may_alias.cpp:74

may_alias

std::optional< exprt > may_alias(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)

Definition may_alias.cpp:221

drop_pointer_typecasts

static exprt drop_pointer_typecasts(exprt src)

Definition may_alias.cpp:137

is_object_field_element

bool is_object_field_element(const exprt &expr)

Definition may_alias.cpp:62

stack_and_not_dirty

bool stack_and_not_dirty(const exprt &expr, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)

Definition may_alias.cpp:107

may_alias.h

May Alias.

namespace.h

pointer_expr.h

API to expression classes for Pointers.

to_element_address_expr

const element_address_exprt & to_element_address_expr(const exprt &expr)

Cast an exprt to an element_address_exprt.

Definition pointer_expr.h:814

to_object_address_expr

const object_address_exprt & to_object_address_expr(const exprt &expr)

Cast an exprt to an object_address_exprt.

Definition pointer_expr.h:643

to_pointer_type

const pointer_typet & to_pointer_type(const typet &type)

Cast a typet to a pointer_typet.

Definition pointer_expr.h:93

to_field_address_expr

const field_address_exprt & to_field_address_expr(const exprt &expr)

Cast an exprt to an field_address_exprt.

Definition pointer_expr.h:727

CHECK_RETURN

#define CHECK_RETURN(CONDITION)

Definition invariant.h:495

PRECONDITION

#define PRECONDITION(CONDITION)

Definition invariant.h:463

std_expr.h

API to expression classes.

to_typecast_expr

const typecast_exprt & to_typecast_expr(const exprt &expr)

Cast an exprt to a typecast_exprt.

Definition std_expr.h:2024

to_struct_type

const struct_typet & to_struct_type(const typet &type)

Cast a typet to a struct_typet.

Definition std_types.h:307

to_struct_tag_type

const struct_tag_typet & to_struct_tag_type(const typet &type)

Cast a typet to a struct_tag_typet.

Definition std_types.h:517

symbol.h

Symbol table entry.