Skip to content

Commit

Permalink
Merge pull request diffblue#8359 from qinheping/feature/add_loop_cont…
Browse files Browse the repository at this point in the history 
…ract_symbols_into_symbol_table

[CONTRACTS] Add loop-contract symbols into symbol table during typecheck
  • Loading branch information
@tautschnig
tautschnig authored Jul 2, 2024
2 parents 54c20cd + 32ed640 commit 66ae03f
Show file tree
Hide file tree
Showing 3 changed files with 103 additions and 44 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
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
123 changes: 87 additions & 36 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,
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);
}
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);
}
}

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
// 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;
}
}
}

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))
{
return false;
}

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,
static_cast<const typet &>(va_arg_type),
op,
bindings,
subs_to_find))
{
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.
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)
{
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 @@ -155,26 +189,27 @@ static bool find_symbols(

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)
{
const code_typet &code_type=to_code_type(src);
if(!find_symbols(kind, code_type.return_type(), op, bindings))
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)
{
// 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,19 +239,21 @@ 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 = {})
{
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)
Expand Down Expand Up @@ -278,20 +315,34 @@ void find_non_pointer_type_symbols(
});
}

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)
{
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,
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)
{
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,
src,
[&dest](const symbol_exprt &e) {
dest.insert(e.get_identifier());
return true;
},
subs_to_find);
}

void find_symbols(const exprt &src, find_symbols_sett &dest)
Expand Down
16 changes: 10 additions & 6 deletions src/util/find_symbols.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,16 +79,20 @@ void find_non_pointer_type_symbols(
const exprt &src,
find_symbols_sett &dest);

/// Find identifiers of the sub expressions with id ID_symbol, considering both
/// free and bound variables, as well as any type tags.
/// 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.
void find_type_and_expr_symbols(
const typet &src,
find_symbols_sett &dest);
find_symbols_sett &dest,
const std::vector<irep_idt> &subs_to_find = {});

/// Find identifiers of the sub expressions with id ID_symbol, considering both
/// free and bound variables, as well as any type tags.
/// 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.
void find_type_and_expr_symbols(
const exprt &src,
find_symbols_sett &dest);
find_symbols_sett &dest,
const std::vector<irep_idt> &subs_to_find = {});

#endif // CPROVER_UTIL_FIND_SYMBOLS_H

0 comments on commit 66ae03f

Please sign in to comment.