From 32ed64006cf31f867fa4e8b4ed3098091e678ab6 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 27 Jun 2024 12:22:16 -0500 Subject: [PATCH] Add loop-contract symbols into symbol table during typecheck --- src/linking/remove_internal_symbols.cpp | 8 +- src/util/find_symbols.cpp | 123 +++++++++++++++++------- src/util/find_symbols.h | 16 +-- 3 files changed, 103 insertions(+), 44 deletions(-) diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 23b24c9aee7..ce8401a0699 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -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 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)); diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index 0038d1ad337..488bad7e07f 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -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, - std::unordered_set &bindings); + std::unordered_set &bindings, + const std::vector &subs_to_find); static bool find_symbols( symbol_kindt kind, const exprt &src, std::function op, - std::unordered_set &bindings) + std::unordered_set &bindings, + const std::vector &subs_to_find) { if(kind == symbol_kindt::F_EXPR_FREE) { @@ -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) { @@ -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(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) @@ -95,12 +117,15 @@ 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(c_sizeof_type), op, bindings)) + c_sizeof_type.is_not_nil() && !find_symbols( + kind, + static_cast(c_sizeof_type), + op, + bindings, + subs_to_find)) { return false; } @@ -108,8 +133,12 @@ static bool find_symbols( const irept &va_arg_type=src.find(ID_C_va_arg_type); if( - va_arg_type.is_not_nil() && - !find_symbols(kind, static_cast(va_arg_type), op, bindings)) + va_arg_type.is_not_nil() && !find_symbols( + kind, + static_cast(va_arg_type), + op, + bindings, + subs_to_find)) { return false; } @@ -117,24 +146,29 @@ static bool find_symbols( 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 op, - std::unordered_set &bindings) + std::unordered_set &bindings, + const std::vector &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; } @@ -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( @@ -204,19 +239,21 @@ static bool find_symbols( static bool find_symbols( symbol_kindt kind, const typet &type, - std::function op) + std::function op, + const std::vector &subs_to_find = {}) { std::unordered_set 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 op) + std::function op, + const std::vector &subs_to_find = {}) { std::unordered_set 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 &dest) @@ -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 &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 &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) diff --git a/src/util/find_symbols.h b/src/util/find_symbols.h index df840001b7e..c699ebd7380 100644 --- a/src/util/find_symbols.h +++ b/src/util/find_symbols.h @@ -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 &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 &subs_to_find = {}); #endif // CPROVER_UTIL_FIND_SYMBOLS_H