Skip to content

Commit

Permalink
Add loop-contract symbols into symbol table during typecheck
Browse files Browse the repository at this point in the history
  • Loading branch information
@qinheping
qinheping committed Jun 27, 2024
1 parent 582aa69 commit 04d6bbc
Show file tree
Hide file tree
Showing 3 changed files with 155 additions and 78 deletions.
8 changes: 6 additions & 2 deletions src/linking/remove_internal_symbols.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,12 @@ static void get_symbols(

find_symbols_sett new_symbols;

find_type_and_expr_symbols(symbol.type, new_symbols);
find_type_and_expr_symbols(symbol.value, new_symbols);
// ID of named subs of loop contracts

Check warning on line 46 in src/linking/remove_internal_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/linking/remove_internal_symbols.cpp#L46 

Added line #L46 was not covered by tests
static std::vector<irep_idt> loop_contracts_subs{
ID_C_spec_loop_invariant, ID_C_spec_decreases};

find_type_and_expr_symbols(symbol.type, new_symbols, loop_contracts_subs);
find_type_and_expr_symbols(symbol.value, new_symbols, loop_contracts_subs);

for(const auto &s : new_symbols)
working_set.push_back(&ns.lookup(s));
Expand Down
209 changes: 139 additions & 70 deletions src/util/find_symbols.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,17 +27,22 @@ enum class symbol_kindt
F_ALL
};

/// Find identifiers with id ID_symbol of the sub expressions and the subs with
/// ID in \p subs_to_find
/// considering both free and bound variables, as well as any type tags.
static bool find_symbols(
symbol_kindt,
const typet &,
std::function<bool(const symbol_exprt &)>,
std::unordered_set<irep_idt> &bindings);
std::unordered_set<irep_idt> &bindings,
const std::vector<irep_idt> &subs_to_find);

static bool find_symbols(
symbol_kindt kind,
const exprt &src,
std::function<bool(const symbol_exprt &)> op,
std::unordered_set<irep_idt> &bindings)
std::unordered_set<irep_idt> &bindings,

Check warning on line 44 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L44 

Added line #L44 was not covered by tests
const std::vector<irep_idt> &subs_to_find)
{
if(kind == symbol_kindt::F_EXPR_FREE)
{
Expand All @@ -48,10 +53,12 @@ static bool find_symbols(
for(const auto &v : binding_expr.variables())
new_bindings.insert(v.get_identifier());

if(!find_symbols(kind, binding_expr.where(), op, new_bindings))
if(!find_symbols(
kind, binding_expr.where(), op, new_bindings, subs_to_find))
return false;

return find_symbols(kind, binding_expr.type(), op, bindings);
return find_symbols(
kind, binding_expr.type(), op, bindings, subs_to_find);

Check warning on line 61 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L61 

Added line #L61 was not covered by tests
}
else if(src.id() == ID_let)
{
Expand All @@ -60,23 +67,38 @@ static bool find_symbols(
for(const auto &v : let_expr.variables())
new_bindings.insert(v.get_identifier());

if(!find_symbols(kind, let_expr.where(), op, new_bindings))
if(!find_symbols(kind, let_expr.where(), op, new_bindings, subs_to_find))
return false;

if(!find_symbols(kind, let_expr.op1(), op, new_bindings))
if(!find_symbols(kind, let_expr.op1(), op, new_bindings, subs_to_find))
return false;

return find_symbols(kind, let_expr.type(), op, bindings);
return find_symbols(kind, let_expr.type(), op, bindings, subs_to_find);

Check warning on line 76 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L76 

Added line #L76 was not covered by tests
}
}

for(const auto &src_op : src.operands())
{
if(!find_symbols(kind, src_op, op, bindings))
if(!find_symbols(kind, src_op, op, bindings, subs_to_find))
return false;
}

if(!find_symbols(kind, src.type(), op, bindings))
// Go over all named subs with id in subs_to_find

Check warning on line 86 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L86 

Added line #L86 was not covered by tests
// and find symbols recursively.
for(const auto &sub_to_find : subs_to_find)
{
auto sub_expr = static_cast<const exprt &>(src.find(sub_to_find));
if(sub_expr.is_not_nil())
{
for(const auto &sub_op : sub_expr.operands())
{
if(!find_symbols(kind, sub_op, op, bindings, subs_to_find))
return false;

Check warning on line 96 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L96 

Added line #L96 was not covered by tests
}
}
}

if(!find_symbols(kind, src.type(), op, bindings, subs_to_find))
return false;

if(src.id() == ID_symbol)
Expand All @@ -95,46 +117,58 @@ static bool find_symbols(
}
}

const irept &c_sizeof_type=src.find(ID_C_c_sizeof_type);
const irept &c_sizeof_type = src.find(ID_C_c_sizeof_type);

if(
c_sizeof_type.is_not_nil() &&
!find_symbols(
kind, static_cast<const typet &>(c_sizeof_type), op, bindings))
c_sizeof_type.is_not_nil() && !find_symbols(
kind,
static_cast<const typet &>(c_sizeof_type),
op,
bindings,
subs_to_find))

Check warning on line 128 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L126-L128 

Added lines #L126 - L128 were not covered by tests
{
return false;
}

const irept &va_arg_type=src.find(ID_C_va_arg_type);
const irept &va_arg_type = src.find(ID_C_va_arg_type);

if(
va_arg_type.is_not_nil() &&
!find_symbols(kind, static_cast<const typet &>(va_arg_type), op, bindings))
va_arg_type.is_not_nil() && !find_symbols(
kind,

Check warning on line 137 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L137 

Added line #L137 was not covered by tests
static_cast<const typet &>(va_arg_type),
op,
bindings,
subs_to_find))

Check warning on line 141 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L140-L141 

Added lines #L140 - L141 were not covered by tests
{
return false;
}

return true;
}

/// Find identifiers with id ID_symbol of the sub expressions and the subs with
/// ID in \p subs_to_find
/// considering both free and bound variables, as well as any type tags.

Check warning on line 151 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L151 

Added line #L151 was not covered by tests
static bool find_symbols(
symbol_kindt kind,
const typet &src,
std::function<bool(const symbol_exprt &)> op,
std::unordered_set<irep_idt> &bindings)
std::unordered_set<irep_idt> &bindings,
const std::vector<irep_idt> &subs_to_find)

Check warning on line 157 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L156-L157 

Added lines #L156 - L157 were not covered by tests
{
if(kind != symbol_kindt::F_TYPE_NON_PTR || src.id() != ID_pointer)
{
if(
src.has_subtype() &&
!find_symbols(kind, to_type_with_subtype(src).subtype(), op, bindings))
!find_symbols(
kind, to_type_with_subtype(src).subtype(), op, bindings, subs_to_find))
{
return false;
}

for(const typet &subtype : to_type_with_subtypes(src).subtypes())
{
if(!find_symbols(kind, subtype, op, bindings))
if(!find_symbols(kind, subtype, op, bindings, subs_to_find))
return false;
}

Expand All @@ -148,33 +182,33 @@ static bool find_symbols(
}
}

if(src.id()==ID_struct ||
src.id()==ID_union)
if(src.id() == ID_struct || src.id() == ID_union)
{
const struct_union_typet &struct_union_type=to_struct_union_type(src);
const struct_union_typet &struct_union_type = to_struct_union_type(src);

for(const auto &c : struct_union_type.components())
{
if(!find_symbols(kind, c, op, bindings))
if(!find_symbols(kind, c, op, bindings, subs_to_find))
return false;
}
}
else if(src.id()==ID_code)
else if(src.id() == ID_code)
{
const code_typet &code_type=to_code_type(src);
if(!find_symbols(kind, code_type.return_type(), op, bindings))
const code_typet &code_type = to_code_type(src);
if(!find_symbols(kind, code_type.return_type(), op, bindings, subs_to_find))
return false;

for(const auto &p : code_type.parameters())
{
if(!find_symbols(kind, p, op, bindings))
if(!find_symbols(kind, p, op, bindings, subs_to_find))
return false;
}
}
else if(src.id()==ID_array)
else if(src.id() == ID_array)
{
// do the size -- the subtype is already done
if(!find_symbols(kind, to_array_type(src).size(), op, bindings))
if(!find_symbols(
kind, to_array_type(src).size(), op, bindings, subs_to_find))
return false;
}
else if(
Expand Down Expand Up @@ -204,27 +238,33 @@ static bool find_symbols(
static bool find_symbols(
symbol_kindt kind,
const typet &type,
std::function<bool(const symbol_exprt &)> op)
std::function<bool(const symbol_exprt &)> op,
const std::vector<irep_idt> &subs_to_find)
{
std::unordered_set<irep_idt> bindings;
return find_symbols(kind, type, op, bindings);
return find_symbols(kind, type, op, bindings, subs_to_find);
}

static bool find_symbols(
symbol_kindt kind,
const exprt &src,
std::function<bool(const symbol_exprt &)> op)
std::function<bool(const symbol_exprt &)> op,
const std::vector<irep_idt> &subs_to_find)

Check warning on line 252 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L251-L252 

Added lines #L251 - L252 were not covered by tests
{
std::unordered_set<irep_idt> bindings;
return find_symbols(kind, src, op, bindings);
return find_symbols(kind, src, op, bindings, subs_to_find);
}

void find_symbols(const exprt &src, std::set<symbol_exprt> &dest)
{
find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
dest.insert(e);
return true;
});
find_symbols(
symbol_kindt::F_EXPR,
src,

Check warning on line 262 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L262 

Added line #L262 was not covered by tests
[&dest](const symbol_exprt &e) {
dest.insert(e);
return true;
},

Check warning on line 266 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L266 

Added line #L266 was not covered by tests
{});
}

bool has_symbol_expr(
Expand All @@ -237,67 +277,96 @@ bool has_symbol_expr(
src,
[&identifier](const symbol_exprt &e) {
return e.get_identifier() != identifier;
});
},
{});
}

void find_type_symbols(const exprt &src, find_symbols_sett &dest)
{
find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
dest.insert(e.get_identifier());
return true;
});
find_symbols(
symbol_kindt::F_TYPE,
src,
[&dest](const symbol_exprt &e) {
dest.insert(e.get_identifier());
return true;
},
{});

Check warning on line 293 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L286-L293 

Added lines #L286 - L293 were not covered by tests
}

void find_type_symbols(const typet &src, find_symbols_sett &dest)
{
find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
dest.insert(e.get_identifier());
return true;
});
find_symbols(
symbol_kindt::F_TYPE,
src,
[&dest](const symbol_exprt &e) {
dest.insert(e.get_identifier());
return true;
},

Check warning on line 304 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L298-L304 

Added lines #L298 - L304 were not covered by tests
{});
}

void find_non_pointer_type_symbols(
const exprt &src,
find_symbols_sett &dest)
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
{
find_symbols(
symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
symbol_kindt::F_TYPE_NON_PTR,

Check warning on line 311 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L311 

Added line #L311 was not covered by tests
src,
[&dest](const symbol_exprt &e) {

Check warning on line 313 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L313 

Added line #L313 was not covered by tests
dest.insert(e.get_identifier());
return true;
});
},

Check warning on line 316 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L316 

Added line #L316 was not covered by tests
{});
}

void find_non_pointer_type_symbols(
const typet &src,
find_symbols_sett &dest)
void find_non_pointer_type_symbols(const typet &src, find_symbols_sett &dest)

Check warning on line 320 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L320 

Added line #L320 was not covered by tests
{
find_symbols(
symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
symbol_kindt::F_TYPE_NON_PTR,

Check warning on line 323 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L323 

Added line #L323 was not covered by tests
src,
[&dest](const symbol_exprt &e) {

Check warning on line 325 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L325 

Added line #L325 was not covered by tests
dest.insert(e.get_identifier());
return true;
});
},

Check warning on line 328 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L328 

Added line #L328 was not covered by tests
{});
}

void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
void find_type_and_expr_symbols(
const exprt &src,
find_symbols_sett &dest,
const std::vector<irep_idt> &subs_to_find)

Check warning on line 335 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L333-L335 

Added lines #L333 - L335 were not covered by tests
{
find_symbols(symbol_kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
dest.insert(e.get_identifier());
return true;
});
find_symbols(
symbol_kindt::F_ALL,

Check warning on line 338 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L338 

Added line #L338 was not covered by tests
src,
[&dest](const symbol_exprt &e) {
dest.insert(e.get_identifier());
return true;
},
subs_to_find);
}

void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest)
void find_type_and_expr_symbols(
const typet &src,
find_symbols_sett &dest,
const std::vector<irep_idt> &subs_to_find)

Check warning on line 350 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L348-L350 

Added lines #L348 - L350 were not covered by tests
{
find_symbols(symbol_kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
dest.insert(e.get_identifier());
return true;
});
find_symbols(
symbol_kindt::F_ALL,

Check warning on line 353 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L353 

Added line #L353 was not covered by tests
src,
[&dest](const symbol_exprt &e) {
dest.insert(e.get_identifier());
return true;
},

Check warning on line 358 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L358 

Added line #L358 was not covered by tests
subs_to_find);
}

void find_symbols(const exprt &src, find_symbols_sett &dest)
{
find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
dest.insert(e.get_identifier());
return true;
});
find_symbols(
symbol_kindt::F_EXPR,

Check warning on line 365 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L365 

Added line #L365 was not covered by tests
src,
[&dest](const symbol_exprt &e) {
dest.insert(e.get_identifier());
return true;
},

Check warning on line 370 in src/util/find_symbols.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/find_symbols.cpp#L370 

Added line #L370 was not covered by tests
{});
}
Loading

0 comments on commit 04d6bbc

Please sign in to comment.