Skip to content

Commit 7dec291

Browse files
qinhepingqinheping
committed
Add loop-contract symbols into symbol table during typecheck
1 parent 582aa69 commit 7dec291

File tree

3 files changed

+155
-78
lines changed

3 files changed

+155
-78
lines changed

‎src/linking/remove_internal_symbols.cpp‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -43,8 +43,12 @@ static void get_symbols(
4343

4444
find_symbols_sett new_symbols;
4545

46-
find_type_and_expr_symbols(symbol.type, new_symbols);
47-
find_type_and_expr_symbols(symbol.value, new_symbols);
46+
// ID of named subs of loop contracts
47+
std::vector<irep_idt> loop_contracts_subs{
48+
ID_C_spec_loop_invariant, ID_C_spec_decreases};
49+
50+
find_type_and_expr_symbols(symbol.type, new_symbols, loop_contracts_subs);
51+
find_type_and_expr_symbols(symbol.value, new_symbols, loop_contracts_subs);
4852

4953
for(const auto &s : new_symbols)
5054
working_set.push_back(&ns.lookup(s));

‎src/util/find_symbols.cpp‎

Lines changed: 139 additions & 70 deletions
Original file line numberDiff line numberDiff line change
@@ -27,17 +27,22 @@ enum class symbol_kindt
2727
F_ALL
2828
};
2929

30+
/// Find identifiers with id ID_symbol of the sub expressions and the subs with
31+
/// ID in \p subs_to_find
32+
/// considering both free and bound variables, as well as any type tags.
3033
static bool find_symbols(
3134
symbol_kindt,
3235
const typet &,
3336
std::function<bool(const symbol_exprt &)>,
34-
std::unordered_set<irep_idt> &bindings);
37+
std::unordered_set<irep_idt> &bindings,
38+
const std::vector<irep_idt> &subs_to_find);
3539

3640
static bool find_symbols(
3741
symbol_kindt kind,
3842
const exprt &src,
3943
std::function<bool(const symbol_exprt &)> op,
40-
std::unordered_set<irep_idt> &bindings)
44+
std::unordered_set<irep_idt> &bindings,
45+
const std::vector<irep_idt> &subs_to_find)
4146
{
4247
if(kind == symbol_kindt::F_EXPR_FREE)
4348
{
@@ -48,10 +53,12 @@ static bool find_symbols(
4853
for(const auto &v : binding_expr.variables())
4954
new_bindings.insert(v.get_identifier());
5055

51-
if(!find_symbols(kind, binding_expr.where(), op, new_bindings))
56+
if(!find_symbols(
57+
kind, binding_expr.where(), op, new_bindings, subs_to_find))
5258
return false;
5359

54-
return find_symbols(kind, binding_expr.type(), op, bindings);
60+
return find_symbols(
61+
kind, binding_expr.type(), op, bindings, subs_to_find);
5562
}
5663
else if(src.id() == ID_let)
5764
{
@@ -60,23 +67,38 @@ static bool find_symbols(
6067
for(const auto &v : let_expr.variables())
6168
new_bindings.insert(v.get_identifier());
6269

63-
if(!find_symbols(kind, let_expr.where(), op, new_bindings))
70+
if(!find_symbols(kind, let_expr.where(), op, new_bindings, subs_to_find))
6471
return false;
6572

66-
if(!find_symbols(kind, let_expr.op1(), op, new_bindings))
73+
if(!find_symbols(kind, let_expr.op1(), op, new_bindings, subs_to_find))
6774
return false;
6875

69-
return find_symbols(kind, let_expr.type(), op, bindings);
76+
return find_symbols(kind, let_expr.type(), op, bindings, subs_to_find);
7077
}
7178
}
7279

7380
for(const auto &src_op : src.operands())
7481
{
75-
if(!find_symbols(kind, src_op, op, bindings))
82+
if(!find_symbols(kind, src_op, op, bindings, subs_to_find))
7683
return false;
7784
}
7885

79-
if(!find_symbols(kind, src.type(), op, bindings))
86+
// Go over all named subs with id in subs_to_find
87+
// and find symbols recursively.
88+
for(const auto &sub_to_find : subs_to_find)
89+
{
90+
auto sub_expr = static_cast<const exprt &>(src.find(sub_to_find));
91+
if(sub_expr.is_not_nil())
92+
{
93+
for(const auto &sub_op : sub_expr.operands())
94+
{
95+
if(!find_symbols(kind, sub_op, op, bindings, subs_to_find))
96+
return false;
97+
}
98+
}
99+
}
100+
101+
if(!find_symbols(kind, src.type(), op, bindings, subs_to_find))
80102
return false;
81103

82104
if(src.id() == ID_symbol)
@@ -95,46 +117,58 @@ static bool find_symbols(
95117
}
96118
}
97119

98-
const irept &c_sizeof_type=src.find(ID_C_c_sizeof_type);
120+
const irept &c_sizeof_type = src.find(ID_C_c_sizeof_type);
99121

100122
if(
101-
c_sizeof_type.is_not_nil() &&
102-
!find_symbols(
103-
kind, static_cast<const typet &>(c_sizeof_type), op, bindings))
123+
c_sizeof_type.is_not_nil() && !find_symbols(
124+
kind,
125+
static_cast<const typet &>(c_sizeof_type),
126+
op,
127+
bindings,
128+
subs_to_find))
104129
{
105130
return false;
106131
}
107132

108-
const irept &va_arg_type=src.find(ID_C_va_arg_type);
133+
const irept &va_arg_type = src.find(ID_C_va_arg_type);
109134

110135
if(
111-
va_arg_type.is_not_nil() &&
112-
!find_symbols(kind, static_cast<const typet &>(va_arg_type), op, bindings))
136+
va_arg_type.is_not_nil() && !find_symbols(
137+
kind,
138+
static_cast<const typet &>(va_arg_type),
139+
op,
140+
bindings,
141+
subs_to_find))
113142
{
114143
return false;
115144
}
116145

117146
return true;
118147
}
119148

149+
/// Find identifiers with id ID_symbol of the sub expressions and the subs with
150+
/// ID in \p subs_to_find
151+
/// considering both free and bound variables, as well as any type tags.
120152
static bool find_symbols(
121153
symbol_kindt kind,
122154
const typet &src,
123155
std::function<bool(const symbol_exprt &)> op,
124-
std::unordered_set<irep_idt> &bindings)
156+
std::unordered_set<irep_idt> &bindings,
157+
const std::vector<irep_idt> &subs_to_find)
125158
{
126159
if(kind != symbol_kindt::F_TYPE_NON_PTR || src.id() != ID_pointer)
127160
{
128161
if(
129162
src.has_subtype() &&
130-
!find_symbols(kind, to_type_with_subtype(src).subtype(), op, bindings))
163+
!find_symbols(
164+
kind, to_type_with_subtype(src).subtype(), op, bindings, subs_to_find))
131165
{
132166
return false;
133167
}
134168

135169
for(const typet &subtype : to_type_with_subtypes(src).subtypes())
136170
{
137-
if(!find_symbols(kind, subtype, op, bindings))
171+
if(!find_symbols(kind, subtype, op, bindings, subs_to_find))
138172
return false;
139173
}
140174

@@ -148,33 +182,33 @@ static bool find_symbols(
148182
}
149183
}
150184

151-
if(src.id()==ID_struct ||
152-
src.id()==ID_union)
185+
if(src.id() == ID_struct || src.id() == ID_union)
153186
{
154-
const struct_union_typet &struct_union_type=to_struct_union_type(src);
187+
const struct_union_typet &struct_union_type = to_struct_union_type(src);
155188

156189
for(const auto &c : struct_union_type.components())
157190
{
158-
if(!find_symbols(kind, c, op, bindings))
191+
if(!find_symbols(kind, c, op, bindings, subs_to_find))
159192
return false;
160193
}
161194
}
162-
else if(src.id()==ID_code)
195+
else if(src.id() == ID_code)
163196
{
164-
const code_typet &code_type=to_code_type(src);
165-
if(!find_symbols(kind, code_type.return_type(), op, bindings))
197+
const code_typet &code_type = to_code_type(src);
198+
if(!find_symbols(kind, code_type.return_type(), op, bindings, subs_to_find))
166199
return false;
167200

168201
for(const auto &p : code_type.parameters())
169202
{
170-
if(!find_symbols(kind, p, op, bindings))
203+
if(!find_symbols(kind, p, op, bindings, subs_to_find))
171204
return false;
172205
}
173206
}
174-
else if(src.id()==ID_array)
207+
else if(src.id() == ID_array)
175208
{
176209
// do the size -- the subtype is already done
177-
if(!find_symbols(kind, to_array_type(src).size(), op, bindings))
210+
if(!find_symbols(
211+
kind, to_array_type(src).size(), op, bindings, subs_to_find))
178212
return false;
179213
}
180214
else if(
@@ -204,27 +238,33 @@ static bool find_symbols(
204238
static bool find_symbols(
205239
symbol_kindt kind,
206240
const typet &type,
207-
std::function<bool(const symbol_exprt &)> op)
241+
std::function<bool(const symbol_exprt &)> op,
242+
const std::vector<irep_idt> &subs_to_find)
208243
{
209244
std::unordered_set<irep_idt> bindings;
210-
return find_symbols(kind, type, op, bindings);
245+
return find_symbols(kind, type, op, bindings, subs_to_find);
211246
}
212247

213248
static bool find_symbols(
214249
symbol_kindt kind,
215250
const exprt &src,
216-
std::function<bool(const symbol_exprt &)> op)
251+
std::function<bool(const symbol_exprt &)> op,
252+
const std::vector<irep_idt> &subs_to_find)
217253
{
218254
std::unordered_set<irep_idt> bindings;
219-
return find_symbols(kind, src, op, bindings);
255+
return find_symbols(kind, src, op, bindings, subs_to_find);
220256
}
221257

222258
void find_symbols(const exprt &src, std::set<symbol_exprt> &dest)
223259
{
224-
find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
225-
dest.insert(e);
226-
return true;
227-
});
260+
find_symbols(
261+
symbol_kindt::F_EXPR,
262+
src,
263+
[&dest](const symbol_exprt &e) {
264+
dest.insert(e);
265+
return true;
266+
},
267+
{});
228268
}
229269

230270
bool has_symbol_expr(
@@ -237,67 +277,96 @@ bool has_symbol_expr(
237277
src,
238278
[&identifier](const symbol_exprt &e) {
239279
return e.get_identifier() != identifier;
240-
});
280+
},
281+
{});
241282
}
242283

243284
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
244285
{
245-
find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
246-
dest.insert(e.get_identifier());
247-
return true;
248-
});
286+
find_symbols(
287+
symbol_kindt::F_TYPE,
288+
src,
289+
[&dest](const symbol_exprt &e) {
290+
dest.insert(e.get_identifier());
291+
return true;
292+
},
293+
{});
249294
}
250295

251296
void find_type_symbols(const typet &src, find_symbols_sett &dest)
252297
{
253-
find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
254-
dest.insert(e.get_identifier());
255-
return true;
256-
});
298+
find_symbols(
299+
symbol_kindt::F_TYPE,
300+
src,
301+
[&dest](const symbol_exprt &e) {
302+
dest.insert(e.get_identifier());
303+
return true;
304+
},
305+
{});
257306
}
258307

259-
void find_non_pointer_type_symbols(
260-
const exprt &src,
261-
find_symbols_sett &dest)
308+
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
262309
{
263310
find_symbols(
264-
symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
311+
symbol_kindt::F_TYPE_NON_PTR,
312+
src,
313+
[&dest](const symbol_exprt &e) {
265314
dest.insert(e.get_identifier());
266315
return true;
267-
});
316+
},
317+
{});
268318
}
269319

270-
void find_non_pointer_type_symbols(
271-
const typet &src,
272-
find_symbols_sett &dest)
320+
void find_non_pointer_type_symbols(const typet &src, find_symbols_sett &dest)
273321
{
274322
find_symbols(
275-
symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
323+
symbol_kindt::F_TYPE_NON_PTR,
324+
src,
325+
[&dest](const symbol_exprt &e) {
276326
dest.insert(e.get_identifier());
277327
return true;
278-
});
328+
},
329+
{});
279330
}
280331

281-
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
332+
void find_type_and_expr_symbols(
333+
const exprt &src,
334+
find_symbols_sett &dest,
335+
const std::vector<irep_idt> &subs_to_find)
282336
{
283-
find_symbols(symbol_kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
284-
dest.insert(e.get_identifier());
285-
return true;
286-
});
337+
find_symbols(
338+
symbol_kindt::F_ALL,
339+
src,
340+
[&dest](const symbol_exprt &e) {
341+
dest.insert(e.get_identifier());
342+
return true;
343+
},
344+
subs_to_find);
287345
}
288346

289-
void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest)
347+
void find_type_and_expr_symbols(
348+
const typet &src,
349+
find_symbols_sett &dest,
350+
const std::vector<irep_idt> &subs_to_find)
290351
{
291-
find_symbols(symbol_kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
292-
dest.insert(e.get_identifier());
293-
return true;
294-
});
352+
find_symbols(
353+
symbol_kindt::F_ALL,
354+
src,
355+
[&dest](const symbol_exprt &e) {
356+
dest.insert(e.get_identifier());
357+
return true;
358+
},
359+
subs_to_find);
295360
}
296361

297362
void find_symbols(const exprt &src, find_symbols_sett &dest)
298363
{
299-
find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
300-
dest.insert(e.get_identifier());
301-
return true;
302-
});
364+
find_symbols(
365+
symbol_kindt::F_EXPR,
366+
src,
367+
[&dest](const symbol_exprt &e) {
368+
dest.insert(e.get_identifier());
369+
return true;
370+
},
371+
{});
303372
}

0 commit comments

Comments
 (0)