From b1179337c8fe16e1e4f9e884eed4589964990524 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 Mar 2022 08:59:43 +0000 Subject: [PATCH 1/8] Make has_symbol configurable and deprecate the existing has_symbol The existing code did not permit configuring what kinds of symbols are to be found. It had a single user within the code base, and even that one was not a good use of it for it constructed a single-element set. The new implementation does not yet make use of potential efficiency advantages of "has a symbol" over "find the existing symbols," but such improvements will be done based on further cleanup of find_symbols code. --- src/ansi-c/goto_check_c.cpp | 4 ++-- src/goto-symex/postcondition.cpp | 17 ++++++++++------- src/goto-symex/precondition.cpp | 17 +++++++++++------ src/util/find_symbols.cpp | 9 +++++++-- src/util/find_symbols.h | 24 ++++++++++++++++++++++-- 5 files changed, 52 insertions(+), 19 deletions(-) diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index d54833e869b..1fc30b64289 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -461,12 +461,12 @@ void goto_check_ct::invalidate(const exprt &lhs) else if(lhs.id() == ID_symbol) { // clear all assertions about 'symbol' - find_symbols_sett find_symbols_set{to_symbol_expr(lhs).get_identifier()}; + const irep_idt &lhs_id = to_symbol_expr(lhs).get_identifier(); for(auto it = assertions.begin(); it != assertions.end();) { if( - has_symbol(it->second, find_symbols_set) || + has_symbol(it->second, lhs_id, kindt::F_EXPR) || has_subexpr(it->second, ID_dereference)) { it = assertions.erase(it); diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp index ed115270c9b..847de15b327 100644 --- a/src/goto-symex/postcondition.cpp +++ b/src/goto-symex/postcondition.cpp @@ -164,13 +164,16 @@ bool postconditiont::is_used( else if(expr.id()==ID_dereference) { // aliasing may happen here - const std::vector expr_set = - value_set.get_value_set(to_dereference_expr(expr).pointer(), ns); - const auto original_names = make_range(expr_set).map( - [](const exprt &e) { return get_original_name(e); }); - const std::unordered_set symbols = - find_symbols_or_nexts(original_names.begin(), original_names.end()); - return symbols.find(identifier)!=symbols.end(); + for(const exprt &e : + value_set.get_value_set(to_dereference_expr(expr).pointer(), ns)) + { + if(has_symbol(get_original_name(e), identifier, kindt::F_BOTH)) + { + return true; + } + } + + return false; } else forall_operands(it, expr) diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp index 990f1a3a2b1..b89c14b6edc 100644 --- a/src/goto-symex/precondition.cpp +++ b/src/goto-symex/precondition.cpp @@ -113,14 +113,19 @@ void preconditiont::compute_rec(exprt &dest) // aliasing may happen here - const std::vector expr_set = value_sets.get_values( - SSA_step.source.function_id, target, deref_expr.pointer()); - const std::unordered_set symbols = - find_symbols_or_nexts(expr_set.begin(), expr_set.end()); + bool may_alias = false; + for(const exprt &e : value_sets.get_values( + SSA_step.source.function_id, target, deref_expr.pointer())) + { + if(has_symbol(e, lhs_identifier, kindt::F_BOTH)) + { + may_alias = true; + break; + } + } - if(symbols.find(lhs_identifier)!=symbols.end()) + if(may_alias) { - // may alias! exprt tmp; tmp.swap(deref_expr.pointer()); dereference(SSA_step.source.function_id, target, tmp, ns, value_sets); diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index b4db7d346f4..4e7ad8c6585 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "range.h" #include "std_expr.h" -enum class kindt { F_TYPE, F_TYPE_NON_PTR, F_EXPR, F_BOTH }; - void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest) { find_symbols(src, dest, true, true); @@ -173,6 +171,13 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest) } } +bool has_symbol(const exprt &src, const irep_idt &identifier, kindt kind) +{ + find_symbols_sett tmp_dest; + find_symbols(kind, src, tmp_dest); + return tmp_dest.find(identifier) != tmp_dest.end(); +} + void find_type_symbols(const exprt &src, find_symbols_sett &dest) { find_symbols(kindt::F_TYPE, src, dest); diff --git a/src/util/find_symbols.h b/src/util/find_symbols.h index 7337e8aef57..33f34e9e8f0 100644 --- a/src/util/find_symbols.h +++ b/src/util/find_symbols.h @@ -10,18 +10,37 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_FIND_SYMBOLS_H #define CPROVER_UTIL_FIND_SYMBOLS_H +#include "deprecate.h" +#include "irep.h" + #include #include #include -#include "irep.h" - class exprt; class symbol_exprt; class typet; typedef std::unordered_set find_symbols_sett; +/// Kinds of symbols to be considered by \ref has_symbol or \ref find_symbols. +enum class kindt +{ + /// Struct, union, or enum tag symbols. + F_TYPE, + /// Struct, union, or enum tag symbols when the expression using them is not a + /// pointer. + F_TYPE_NON_PTR, + /// Symbol expressions. + F_EXPR, + /// Current or next-state symbol expressions. + F_BOTH, +}; + +/// Returns true if one of the symbols in \p src with identifier \p identifier +/// is of kind \p kind. +bool has_symbol(const exprt &src, const irep_idt &identifier, kindt kind); + /// Add to the set \p dest the sub-expressions of \p src with id ID_symbol or /// ID_next_symbol void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest); @@ -59,6 +78,7 @@ std::set find_symbols(const exprt &src); /// Find identifiers of the sub expressions with id ID_symbol std::unordered_set find_symbol_identifiers(const exprt &src); +DEPRECATED(SINCE(2022, 3, 14, "use has_symbol(exprt, irep_idt, symbol_kindt)")) /// \return true if one of the symbols in \p src is present in \p symbols bool has_symbol( const exprt &src, From f0223d9d6435279d2adf036cd523ed83e69db8d7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 9 May 2022 12:31:25 +0000 Subject: [PATCH 2/8] find_symbols kindt: clarify enum entries "F_BOTH" is not a good fit when there are three (and not two) other entries. While at it, also add support to selectively choose current or next expression symbols. --- src/ansi-c/goto_check_c.cpp | 2 +- src/goto-symex/postcondition.cpp | 2 +- src/goto-symex/precondition.cpp | 2 +- src/util/find_symbols.cpp | 20 ++++++++++++-------- src/util/find_symbols.h | 8 ++++++-- 5 files changed, 21 insertions(+), 13 deletions(-) diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 1fc30b64289..83d1323aa5d 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -466,7 +466,7 @@ void goto_check_ct::invalidate(const exprt &lhs) for(auto it = assertions.begin(); it != assertions.end();) { if( - has_symbol(it->second, lhs_id, kindt::F_EXPR) || + has_symbol(it->second, lhs_id, kindt::F_EXPR_CURRENT) || has_subexpr(it->second, ID_dereference)) { it = assertions.erase(it); diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp index 847de15b327..32bc4260045 100644 --- a/src/goto-symex/postcondition.cpp +++ b/src/goto-symex/postcondition.cpp @@ -167,7 +167,7 @@ bool postconditiont::is_used( for(const exprt &e : value_set.get_value_set(to_dereference_expr(expr).pointer(), ns)) { - if(has_symbol(get_original_name(e), identifier, kindt::F_BOTH)) + if(has_symbol(get_original_name(e), identifier, kindt::F_EXPR_BOTH)) { return true; } diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp index b89c14b6edc..f618a4fe0a5 100644 --- a/src/goto-symex/precondition.cpp +++ b/src/goto-symex/precondition.cpp @@ -117,7 +117,7 @@ void preconditiont::compute_rec(exprt &dest) for(const exprt &e : value_sets.get_values( SSA_step.source.function_id, target, deref_expr.pointer())) { - if(has_symbol(e, lhs_identifier, kindt::F_BOTH)) + if(has_symbol(e, lhs_identifier, kindt::F_EXPR_BOTH)) { may_alias = true; break; diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index 4e7ad8c6585..aa9d8c32501 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -95,11 +95,19 @@ void find_symbols(kindt kind, const exprt &src, find_symbols_sett &dest) find_symbols(kind, src.type(), dest); - if(kind==kindt::F_BOTH || kind==kindt::F_EXPR) + if( + kind == kindt::F_ALL || kind == kindt::F_EXPR_CURRENT || + kind == kindt::F_EXPR_BOTH) { if(src.id() == ID_symbol) dest.insert(to_symbol_expr(src).get_identifier()); - else if(src.id() == ID_next_symbol) + } + + if( + kind == kindt::F_ALL || kind == kindt::F_EXPR_NEXT || + kind == kindt::F_EXPR_BOTH) + { + if(src.id() == ID_next_symbol) dest.insert(src.get(ID_identifier)); } @@ -146,10 +154,6 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest) for(const auto &p : code_type.parameters()) { find_symbols(kind, p, dest); - - // irep_idt identifier=it->get_identifier(); - // if(!identifier.empty() && (kind==F_TYPE || kind==F_BOTH)) - // dest.insert(identifier); } } else if(src.id()==ID_array) @@ -204,10 +208,10 @@ void find_non_pointer_type_symbols( void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest) { - find_symbols(kindt::F_BOTH, src, dest); + find_symbols(kindt::F_ALL, src, dest); } void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest) { - find_symbols(kindt::F_BOTH, src, dest); + find_symbols(kindt::F_ALL, src, dest); } diff --git a/src/util/find_symbols.h b/src/util/find_symbols.h index 33f34e9e8f0..b58add391a0 100644 --- a/src/util/find_symbols.h +++ b/src/util/find_symbols.h @@ -32,9 +32,13 @@ enum class kindt /// pointer. F_TYPE_NON_PTR, /// Symbol expressions. - F_EXPR, + F_EXPR_CURRENT, + /// Next-state symbol expressions. + F_EXPR_NEXT, /// Current or next-state symbol expressions. - F_BOTH, + F_EXPR_BOTH, + /// All of the above. + F_ALL }; /// Returns true if one of the symbols in \p src with identifier \p identifier From 7b5eec6f2f354ec585442e9dcac780f51c0dd140 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 Mar 2022 10:33:02 +0000 Subject: [PATCH 3/8] Deprecate find_symbols_or_nexts Make the two Boolean parameters of find_symbols(expr, set, bool, bool) optional so that each existing users can safely use that function (or another, even more suitable, function) instead. --- src/goto-instrument/accelerate/accelerate.cpp | 13 ++---- .../accelerate/acceleration_utils.cpp | 21 +++++----- src/goto-instrument/dump_c.cpp | 4 +- src/goto-instrument/full_slicer.cpp | 2 +- src/goto-programs/goto_program.cpp | 7 ++-- src/util/find_symbols.cpp | 41 ++++++++++--------- src/util/find_symbols.h | 13 +++++- 7 files changed, 53 insertions(+), 48 deletions(-) diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index 144aa6edbd5..fd36f38002f 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -383,21 +383,16 @@ void acceleratet::add_dirty_checks() // Find which symbols are read, i.e. those appearing in a guard or on // the right hand side of an assignment. Assume each is not dirty. - find_symbols_sett read; + std::set read; if(it->has_condition()) - find_symbols_or_nexts(it->condition(), read); + find_symbols(it->condition(), read); if(it->is_assign()) - { - find_symbols_or_nexts(it->assign_rhs(), read); - } + find_symbols(it->assign_rhs(), read); - for(find_symbols_sett::iterator jt=read.begin(); - jt!=read.end(); - ++jt) + for(const auto &var : read) { - const exprt &var=ns.lookup(*jt).symbol_expr(); expr_mapt::iterator dirty_var=dirty_vars_map.find(var); if(dirty_var==dirty_vars_map.end()) diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index 35213de9107..0cba44da764 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -198,18 +198,19 @@ void acceleration_utilst::stash_variables( expr_sett modified, substitutiont &substitution) { - find_symbols_sett vars = - find_symbols_or_nexts(modified.begin(), modified.end()); - const irep_idt &loop_counter_name = - to_symbol_expr(loop_counter).get_identifier(); - vars.erase(loop_counter_name); + const symbol_exprt &loop_counter_sym = to_symbol_expr(loop_counter); - for(const irep_idt &symbol : vars) + std::set vars; + for(const exprt &expr : modified) + find_symbols(expr, vars); + + vars.erase(loop_counter_sym); + + for(const symbol_exprt &orig : vars) { - const symbolt &orig = symbol_table.lookup_ref(symbol); - symbolt stashed_sym=fresh_symbol("polynomial::stash", orig.type); - substitution[orig.symbol_expr()]=stashed_sym.symbol_expr(); - program.assign(stashed_sym.symbol_expr(), orig.symbol_expr()); + symbolt stashed_sym = fresh_symbol("polynomial::stash", orig.type()); + substitution[orig] = stashed_sym.symbol_expr(); + program.assign(stashed_sym.symbol_expr(), orig); } } diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 3de84264a78..de60507cbe6 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -913,9 +913,7 @@ void dump_ct::convert_global_variable( code_frontend_declt d(symbol.symbol_expr()); - find_symbols_sett syms; - if(symbol.value.is_not_nil()) - find_symbols_or_nexts(symbol.value, syms); + find_symbols_sett syms = find_symbol_identifiers(symbol.value); // add a tentative declaration to cater for symbols in the initializer // relying on it this symbol diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index 12c9831c4c7..ac73581f353 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -62,7 +62,7 @@ void full_slicert::add_decl_dead( find_symbols_sett syms; - node.PC->apply([&syms](const exprt &e) { find_symbols_or_nexts(e, syms); }); + node.PC->apply([&syms](const exprt &e) { find_symbols(e, syms); }); for(find_symbols_sett::const_iterator it=syms.begin(); diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index eb47b2da203..9eb4c45a07e 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -760,8 +760,7 @@ void goto_programt::instructiont::validate( auto expr_symbol_finder = [&](const exprt &e) { find_symbols_sett typetags; - find_type_symbols(e.type(), typetags); - find_symbols_or_nexts(e, typetags); + find_type_and_expr_symbols(e, typetags); const symbolt *symbol; for(const auto &identifier : typetags) { @@ -873,7 +872,7 @@ void goto_programt::instructiont::validate( "assert instruction should not have a target", source_location()); - std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder); + expr_symbol_finder(guard); std::for_each(guard.depth_begin(), guard.depth_end(), type_finder); break; case OTHER: @@ -940,7 +939,7 @@ void goto_programt::instructiont::validate( "function call instruction should contain a call statement", source_location()); - std::for_each(_code.depth_begin(), _code.depth_end(), expr_symbol_finder); + expr_symbol_finder(_code); std::for_each(_code.depth_begin(), _code.depth_end(), type_finder); break; case THROW: diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index aa9d8c32501..13527581410 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -13,25 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "range.h" #include "std_expr.h" -void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest) -{ - find_symbols(src, dest, true, true); -} - -void find_symbols( - const exprt &src, - find_symbols_sett &dest, - bool current, - bool next) -{ - src.visit_pre([&dest, current, next](const exprt &e) { - if(e.id() == ID_symbol && current) - dest.insert(to_symbol_expr(e).get_identifier()); - else if(e.id() == ID_next_symbol && next) - dest.insert(e.get(ID_identifier)); - }); -} - bool has_symbol( const exprt &src, const find_symbols_sett &symbols, @@ -215,3 +196,25 @@ void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest) { find_symbols(kindt::F_ALL, src, dest); } + +void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest) +{ + find_symbols(kindt::F_EXPR_BOTH, src, dest); +} + +void find_symbols( + const exprt &src, + find_symbols_sett &dest, + bool current, + bool next) +{ + if(current) + { + if(next) + find_symbols(kindt::F_EXPR_BOTH, src, dest); + else + find_symbols(kindt::F_EXPR_CURRENT, src, dest); + } + else if(next) + find_symbols(kindt::F_EXPR_NEXT, src, dest); +} diff --git a/src/util/find_symbols.h b/src/util/find_symbols.h index b58add391a0..882df001636 100644 --- a/src/util/find_symbols.h +++ b/src/util/find_symbols.h @@ -45,21 +45,30 @@ enum class kindt /// is of kind \p kind. bool has_symbol(const exprt &src, const irep_idt &identifier, kindt kind); +DEPRECATED(SINCE(2022, 3, 14, "use find_symbols")) /// Add to the set \p dest the sub-expressions of \p src with id ID_symbol or /// ID_next_symbol void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest); +/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol if +/// \p current is true, and ID_next_symbol if \p next is true +void find_symbols( + const exprt &src, + find_symbols_sett &dest, + bool current = true, + bool next = true); + /// \return set of sub-expressions of the expressions contained in the range /// defined by \p begin and \p end which have id ID_symbol or ID_next_symbol template +DEPRECATED(SINCE(2022, 3, 14, "use find_symbols and a local iteration")) find_symbols_sett find_symbols_or_nexts(iteratort begin, iteratort end) { static_assert( std::is_base_of::value, "find_symbols takes exprt iterators as arguments"); find_symbols_sett result; - std::for_each( - begin, end, [&](const exprt &e) { find_symbols_or_nexts(e, result); }); + std::for_each(begin, end, [&](const exprt &e) { find_symbols(e, result); }); return result; } From 6fbe9b65dea6700295f1f8a2dfbec1640ad9e503 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 11 May 2022 10:08:41 +0000 Subject: [PATCH 4/8] Remove support for ID_next_symbol This is never used in CBMC's code base. --- src/ansi-c/expr2c.cpp | 6 --- src/ansi-c/goto_check_c.cpp | 2 +- src/goto-programs/slice_global_inits.cpp | 4 +- src/goto-symex/postcondition.cpp | 2 +- src/goto-symex/precondition.cpp | 2 +- src/util/find_macros.cpp | 13 ------- src/util/find_symbols.cpp | 49 ++++-------------------- src/util/find_symbols.h | 23 ++--------- src/util/irep_ids.def | 1 - 9 files changed, 15 insertions(+), 87 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index b776bfe6b16..7a4671c8688 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1663,9 +1663,6 @@ std::string expr2ct::convert_symbol(const exprt &src) #endif } - if(src.id()==ID_next_symbol) - dest="NEXT("+dest+")"; - return dest; } @@ -3850,9 +3847,6 @@ std::string expr2ct::convert_with_precedence( else if(src.id()==ID_symbol) return convert_symbol(src); - else if(src.id()==ID_next_symbol) - return convert_symbol(src); - else if(src.id()==ID_nondet_symbol) return convert_nondet_symbol(to_nondet_symbol_expr(src)); diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 83d1323aa5d..1fc30b64289 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -466,7 +466,7 @@ void goto_check_ct::invalidate(const exprt &lhs) for(auto it = assertions.begin(); it != assertions.end();) { if( - has_symbol(it->second, lhs_id, kindt::F_EXPR_CURRENT) || + has_symbol(it->second, lhs_id, kindt::F_EXPR) || has_subexpr(it->second, ID_dereference)) { it = assertions.erase(it); diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp index 990c22046fc..5ef08988620 100644 --- a/src/goto-programs/slice_global_inits.cpp +++ b/src/goto-programs/slice_global_inits.cpp @@ -64,7 +64,7 @@ void slice_global_inits( for(const auto &i : it->second.body.instructions) { i.apply([&symbols_to_keep](const exprt &expr) { - find_symbols(expr, symbols_to_keep, true, false); + find_symbols(expr, symbols_to_keep); }); } } @@ -103,7 +103,7 @@ void slice_global_inits( symbols_to_keep.find(id) != symbols_to_keep.end()) { fixed_point_reached = false; - find_symbols(instruction.assign_rhs(), symbols_to_keep, true, false); + find_symbols(instruction.assign_rhs(), symbols_to_keep); *seen_it = true; } } diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp index 32bc4260045..93de311c36d 100644 --- a/src/goto-symex/postcondition.cpp +++ b/src/goto-symex/postcondition.cpp @@ -167,7 +167,7 @@ bool postconditiont::is_used( for(const exprt &e : value_set.get_value_set(to_dereference_expr(expr).pointer(), ns)) { - if(has_symbol(get_original_name(e), identifier, kindt::F_EXPR_BOTH)) + if(has_symbol(get_original_name(e), identifier, kindt::F_EXPR)) { return true; } diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp index f618a4fe0a5..248382b20bd 100644 --- a/src/goto-symex/precondition.cpp +++ b/src/goto-symex/precondition.cpp @@ -117,7 +117,7 @@ void preconditiont::compute_rec(exprt &dest) for(const exprt &e : value_sets.get_values( SSA_step.source.function_id, target, deref_expr.pointer())) { - if(has_symbol(e, lhs_identifier, kindt::F_EXPR_BOTH)) + if(has_symbol(e, lhs_identifier, kindt::F_EXPR)) { may_alias = true; break; diff --git a/src/util/find_macros.cpp b/src/util/find_macros.cpp index c78f856eb7c..3b81fdbc3df 100644 --- a/src/util/find_macros.cpp +++ b/src/util/find_macros.cpp @@ -42,19 +42,6 @@ void find_macros( stack.push(&symbol.value); } } - else if(e.id() == ID_next_symbol) - { - const irep_idt &identifier=e.get(ID_identifier); - - const symbolt &symbol=ns.lookup(identifier); - - if(symbol.is_macro) - { - // inserted? - if(dest.insert(identifier).second) - stack.push(&symbol.value); - } - } else { forall_operands(it, e) diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index 13527581410..b1c6d48117b 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -13,33 +13,20 @@ Author: Daniel Kroening, kroening@kroening.com #include "range.h" #include "std_expr.h" -bool has_symbol( - const exprt &src, - const find_symbols_sett &symbols, - bool current, - bool next) +bool has_symbol(const exprt &src, const find_symbols_sett &symbols) { - if(src.id() == ID_symbol && current) + if(src.id() == ID_symbol) return symbols.count(to_symbol_expr(src).get_identifier()) != 0; - else if(src.id() == ID_next_symbol && next) - return symbols.count(src.get(ID_identifier))!=0; else { forall_operands(it, src) - if(has_symbol(*it, symbols, current, next)) + if(has_symbol(*it, symbols)) return true; } return false; } -bool has_symbol( - const exprt &src, - const find_symbols_sett &symbols) -{ - return has_symbol(src, symbols, true, true); -} - void find_symbols( const exprt &src, std::set &dest) @@ -76,22 +63,12 @@ void find_symbols(kindt kind, const exprt &src, find_symbols_sett &dest) find_symbols(kind, src.type(), dest); - if( - kind == kindt::F_ALL || kind == kindt::F_EXPR_CURRENT || - kind == kindt::F_EXPR_BOTH) + if(kind == kindt::F_ALL || kind == kindt::F_EXPR) { if(src.id() == ID_symbol) dest.insert(to_symbol_expr(src).get_identifier()); } - if( - kind == kindt::F_ALL || kind == kindt::F_EXPR_NEXT || - kind == kindt::F_EXPR_BOTH) - { - if(src.id() == ID_next_symbol) - dest.insert(src.get(ID_identifier)); - } - const irept &c_sizeof_type=src.find(ID_C_c_sizeof_type); if(c_sizeof_type.is_not_nil()) @@ -199,22 +176,10 @@ void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest) void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest) { - find_symbols(kindt::F_EXPR_BOTH, src, dest); + find_symbols(kindt::F_EXPR, src, dest); } -void find_symbols( - const exprt &src, - find_symbols_sett &dest, - bool current, - bool next) +void find_symbols(const exprt &src, find_symbols_sett &dest) { - if(current) - { - if(next) - find_symbols(kindt::F_EXPR_BOTH, src, dest); - else - find_symbols(kindt::F_EXPR_CURRENT, src, dest); - } - else if(next) - find_symbols(kindt::F_EXPR_NEXT, src, dest); + find_symbols(kindt::F_EXPR, src, dest); } diff --git a/src/util/find_symbols.h b/src/util/find_symbols.h index 882df001636..6769998a12e 100644 --- a/src/util/find_symbols.h +++ b/src/util/find_symbols.h @@ -32,11 +32,7 @@ enum class kindt /// pointer. F_TYPE_NON_PTR, /// Symbol expressions. - F_EXPR_CURRENT, - /// Next-state symbol expressions. - F_EXPR_NEXT, - /// Current or next-state symbol expressions. - F_EXPR_BOTH, + F_EXPR, /// All of the above. F_ALL }; @@ -50,13 +46,8 @@ DEPRECATED(SINCE(2022, 3, 14, "use find_symbols")) /// ID_next_symbol void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest); -/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol if -/// \p current is true, and ID_next_symbol if \p next is true -void find_symbols( - const exprt &src, - find_symbols_sett &dest, - bool current = true, - bool next = true); +/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol. +void find_symbols(const exprt &src, find_symbols_sett &dest); /// \return set of sub-expressions of the expressions contained in the range /// defined by \p begin and \p end which have id ID_symbol or ID_next_symbol @@ -72,14 +63,6 @@ find_symbols_sett find_symbols_or_nexts(iteratort begin, iteratort end) return result; } -/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol if -/// \p current is true, and ID_next_symbol if \p next is true -void find_symbols( - const exprt &src, - find_symbols_sett &dest, - bool current, - bool next); - /// Find sub expressions with id ID_symbol void find_symbols( const exprt &src, diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index ad4c7058226..31ad25ab76f 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -58,7 +58,6 @@ IREP_ID_ONE(bitxnor) IREP_ID_ONE(notequal) IREP_ID_ONE(if) IREP_ID_ONE(symbol) -IREP_ID_ONE(next_symbol) IREP_ID_ONE(nondet_symbol) IREP_ID_ONE(predicate_symbol) IREP_ID_ONE(predicate_next_symbol) From fcb6b23f9e89ac133a88164fc9113b442f6cd4f8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 11 May 2022 10:20:50 +0000 Subject: [PATCH 5/8] Make find_symbols implementations uniform Each function used a different approach, with different potential omissions of symbols. Instead, use a single way to traverse expressions (and types), and configure the operation done via a parameter. All other (non-deprecated) functions are now just thin wrappers. --- src/util/find_symbols.cpp | 194 ++++++++++++++++++++++++-------------- src/util/find_symbols.h | 14 ++- 2 files changed, 137 insertions(+), 71 deletions(-) diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index b1c6d48117b..91ea5fd5f99 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -27,73 +27,81 @@ bool has_symbol(const exprt &src, const find_symbols_sett &symbols) return false; } -void find_symbols( - const exprt &src, - std::set &dest) -{ - src.visit_pre([&dest](const exprt &e) { - if(e.id() == ID_symbol) - dest.insert(to_symbol_expr(e)); - }); -} - -std::set find_symbols(const exprt &src) -{ - return make_range(src.depth_begin(), src.depth_end()) - .filter([](const exprt &e) { return e.id() == ID_symbol; }) - .map([](const exprt &e) { return to_symbol_expr(e); }); -} +static bool find_symbols( + kindt, + const typet &, + std::function); -std::unordered_set find_symbol_identifiers(const exprt &src) -{ - std::unordered_set result; - src.visit_pre([&](const exprt &e) { - if(e.id() == ID_symbol) - result.insert(to_symbol_expr(e).get_identifier()); - }); - return result; -} - -void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest); - -void find_symbols(kindt kind, const exprt &src, find_symbols_sett &dest) +static bool find_symbols( + kindt kind, + const exprt &src, + std::function op) { forall_operands(it, src) - find_symbols(kind, *it, dest); + { + if(!find_symbols(kind, *it, op)) + return false; + } - find_symbols(kind, src.type(), dest); + if(!find_symbols(kind, src.type(), op)) + return false; if(kind == kindt::F_ALL || kind == kindt::F_EXPR) { - if(src.id() == ID_symbol) - dest.insert(to_symbol_expr(src).get_identifier()); + if(src.id() == ID_symbol && !op(to_symbol_expr(src))) + return false; } 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), dest); + if( + c_sizeof_type.is_not_nil() && + !find_symbols(kind, static_cast(c_sizeof_type), op)) + { + 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(va_arg_type), dest); + if( + va_arg_type.is_not_nil() && + !find_symbols(kind, static_cast(va_arg_type), op)) + { + return false; + } + + return true; } -void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest) +static bool find_symbols( + kindt kind, + const typet &src, + std::function op) { if(kind!=kindt::F_TYPE_NON_PTR || src.id()!=ID_pointer) { - if(src.has_subtype()) - find_symbols(kind, to_type_with_subtype(src).subtype(), dest); + if( + src.has_subtype() && + !find_symbols(kind, to_type_with_subtype(src).subtype(), op)) + { + return false; + } for(const typet &subtype : to_type_with_subtypes(src).subtypes()) - find_symbols(kind, subtype, dest); + { + if(!find_symbols(kind, subtype, op)) + return false; + } - const irep_idt &typedef_name=src.get(ID_C_typedef); - if(!typedef_name.empty()) - dest.insert(typedef_name); + if( + kind == kindt::F_TYPE || kind == kindt::F_TYPE_NON_PTR || + kind == kindt::F_ALL) + { + const irep_idt &typedef_name = src.get(ID_C_typedef); + if(!typedef_name.empty() && !op(symbol_exprt{typedef_name, typet{}})) + return false; + } } if(src.id()==ID_struct || @@ -102,84 +110,132 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest) const struct_union_typet &struct_union_type=to_struct_union_type(src); for(const auto &c : struct_union_type.components()) - find_symbols(kind, c, dest); + { + if(!find_symbols(kind, c, op)) + return false; + } } else if(src.id()==ID_code) { const code_typet &code_type=to_code_type(src); - find_symbols(kind, code_type.return_type(), dest); + if(!find_symbols(kind, code_type.return_type(), op)) + return false; for(const auto &p : code_type.parameters()) { - find_symbols(kind, p, dest); + if(!find_symbols(kind, p, op)) + return false; } } else if(src.id()==ID_array) { // do the size -- the subtype is already done - find_symbols(kind, to_array_type(src).size(), dest); - } - else if(src.id()==ID_c_enum_tag) - { - dest.insert(to_c_enum_tag_type(src).get_identifier()); + if(!find_symbols(kind, to_array_type(src).size(), op)) + return false; } - else if(src.id()==ID_struct_tag) + else if( + kind == kindt::F_TYPE || kind == kindt::F_TYPE_NON_PTR || + kind == kindt::F_ALL) { - dest.insert(to_struct_tag_type(src).get_identifier()); - } - else if(src.id()==ID_union_tag) - { - dest.insert(to_union_tag_type(src).get_identifier()); + if(src.id() == ID_c_enum_tag) + { + if(!op(symbol_exprt{to_c_enum_tag_type(src).get_identifier(), typet{}})) + return false; + } + else if(src.id() == ID_struct_tag) + { + if(!op(symbol_exprt{to_struct_tag_type(src).get_identifier(), typet{}})) + return false; + } + else if(src.id() == ID_union_tag) + { + if(!op(symbol_exprt{to_union_tag_type(src).get_identifier(), typet{}})) + return false; + } } + + return true; +} + +void find_symbols(const exprt &src, std::set &dest) +{ + find_symbols(kindt::F_EXPR, src, [&dest](const symbol_exprt &e) { + dest.insert(e); + return true; + }); } bool has_symbol(const exprt &src, const irep_idt &identifier, kindt kind) { - find_symbols_sett tmp_dest; - find_symbols(kind, src, tmp_dest); - return tmp_dest.find(identifier) != tmp_dest.end(); + return !find_symbols(kind, src, [&identifier](const symbol_exprt &e) { + return e.get_identifier() != identifier; + }); } void find_type_symbols(const exprt &src, find_symbols_sett &dest) { - find_symbols(kindt::F_TYPE, src, dest); + find_symbols(kindt::F_TYPE, src, [&dest](const symbol_exprt &e) { + dest.insert(e.get_identifier()); + return true; + }); } void find_type_symbols(const typet &src, find_symbols_sett &dest) { - find_symbols(kindt::F_TYPE, src, dest); + find_symbols(kindt::F_TYPE, src, [&dest](const symbol_exprt &e) { + dest.insert(e.get_identifier()); + return true; + }); } void find_non_pointer_type_symbols( const exprt &src, find_symbols_sett &dest) { - find_symbols(kindt::F_TYPE_NON_PTR, src, dest); + find_symbols(kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) { + dest.insert(e.get_identifier()); + return true; + }); } void find_non_pointer_type_symbols( const typet &src, find_symbols_sett &dest) { - find_symbols(kindt::F_TYPE_NON_PTR, src, dest); + find_symbols(kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) { + dest.insert(e.get_identifier()); + return true; + }); } void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest) { - find_symbols(kindt::F_ALL, src, dest); + find_symbols(kindt::F_ALL, src, [&dest](const symbol_exprt &e) { + dest.insert(e.get_identifier()); + return true; + }); } void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest) { - find_symbols(kindt::F_ALL, src, dest); + find_symbols(kindt::F_ALL, src, [&dest](const symbol_exprt &e) { + dest.insert(e.get_identifier()); + return true; + }); } void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest) { - find_symbols(kindt::F_EXPR, src, dest); + find_symbols(kindt::F_EXPR, src, [&dest](const symbol_exprt &e) { + dest.insert(e.get_identifier()); + return true; + }); } void find_symbols(const exprt &src, find_symbols_sett &dest) { - find_symbols(kindt::F_EXPR, src, dest); + find_symbols(kindt::F_EXPR, src, [&dest](const symbol_exprt &e) { + dest.insert(e.get_identifier()); + return true; + }); } diff --git a/src/util/find_symbols.h b/src/util/find_symbols.h index 6769998a12e..75741fcc533 100644 --- a/src/util/find_symbols.h +++ b/src/util/find_symbols.h @@ -69,10 +69,20 @@ void find_symbols( std::set &dest); /// Find sub expressions with id ID_symbol -std::set find_symbols(const exprt &src); +inline std::set find_symbols(const exprt &src) +{ + std::set syms; + find_symbols(src, syms); + return syms; +} /// Find identifiers of the sub expressions with id ID_symbol -std::unordered_set find_symbol_identifiers(const exprt &src); +inline find_symbols_sett find_symbol_identifiers(const exprt &src) +{ + find_symbols_sett identifiers; + find_symbols(src, identifiers); + return identifiers; +} DEPRECATED(SINCE(2022, 3, 14, "use has_symbol(exprt, irep_idt, symbol_kindt)")) /// \return true if one of the symbols in \p src is present in \p symbols From aa3d52b586a87ff6a5ae1480cf39f5f4fc02dd82 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 9 May 2022 12:24:06 +0000 Subject: [PATCH 6/8] Rename kindt to symbol_kindt for clarity This is just a change in the enum tag. --- src/ansi-c/goto_check_c.cpp | 2 +- src/goto-symex/postcondition.cpp | 2 +- src/goto-symex/precondition.cpp | 2 +- src/util/find_symbols.cpp | 53 ++++++++++++++++---------------- src/util/find_symbols.h | 7 +++-- 5 files changed, 35 insertions(+), 31 deletions(-) diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 1fc30b64289..2d299eb85af 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -466,7 +466,7 @@ void goto_check_ct::invalidate(const exprt &lhs) for(auto it = assertions.begin(); it != assertions.end();) { if( - has_symbol(it->second, lhs_id, kindt::F_EXPR) || + has_symbol(it->second, lhs_id, symbol_kindt::F_EXPR) || has_subexpr(it->second, ID_dereference)) { it = assertions.erase(it); diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp index 93de311c36d..02f8b06c4fb 100644 --- a/src/goto-symex/postcondition.cpp +++ b/src/goto-symex/postcondition.cpp @@ -167,7 +167,7 @@ bool postconditiont::is_used( for(const exprt &e : value_set.get_value_set(to_dereference_expr(expr).pointer(), ns)) { - if(has_symbol(get_original_name(e), identifier, kindt::F_EXPR)) + if(has_symbol(get_original_name(e), identifier, symbol_kindt::F_EXPR)) { return true; } diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp index 248382b20bd..2d304f79411 100644 --- a/src/goto-symex/precondition.cpp +++ b/src/goto-symex/precondition.cpp @@ -117,7 +117,7 @@ void preconditiont::compute_rec(exprt &dest) for(const exprt &e : value_sets.get_values( SSA_step.source.function_id, target, deref_expr.pointer())) { - if(has_symbol(e, lhs_identifier, kindt::F_EXPR)) + if(has_symbol(e, lhs_identifier, symbol_kindt::F_EXPR)) { may_alias = true; break; diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index 91ea5fd5f99..291b9473beb 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -28,12 +28,12 @@ bool has_symbol(const exprt &src, const find_symbols_sett &symbols) } static bool find_symbols( - kindt, + symbol_kindt, const typet &, std::function); static bool find_symbols( - kindt kind, + symbol_kindt kind, const exprt &src, std::function op) { @@ -46,7 +46,7 @@ static bool find_symbols( if(!find_symbols(kind, src.type(), op)) return false; - if(kind == kindt::F_ALL || kind == kindt::F_EXPR) + if(kind == symbol_kindt::F_ALL || kind == symbol_kindt::F_EXPR) { if(src.id() == ID_symbol && !op(to_symbol_expr(src))) return false; @@ -74,12 +74,11 @@ static bool find_symbols( } static bool find_symbols( - kindt kind, + symbol_kindt kind, const typet &src, std::function op) { - if(kind!=kindt::F_TYPE_NON_PTR || - src.id()!=ID_pointer) + if(kind != symbol_kindt::F_TYPE_NON_PTR || src.id() != ID_pointer) { if( src.has_subtype() && @@ -95,8 +94,8 @@ static bool find_symbols( } if( - kind == kindt::F_TYPE || kind == kindt::F_TYPE_NON_PTR || - kind == kindt::F_ALL) + kind == symbol_kindt::F_TYPE || kind == symbol_kindt::F_TYPE_NON_PTR || + kind == symbol_kindt::F_ALL) { const irep_idt &typedef_name = src.get(ID_C_typedef); if(!typedef_name.empty() && !op(symbol_exprt{typedef_name, typet{}})) @@ -134,8 +133,8 @@ static bool find_symbols( return false; } else if( - kind == kindt::F_TYPE || kind == kindt::F_TYPE_NON_PTR || - kind == kindt::F_ALL) + kind == symbol_kindt::F_TYPE || kind == symbol_kindt::F_TYPE_NON_PTR || + kind == symbol_kindt::F_ALL) { if(src.id() == ID_c_enum_tag) { @@ -159,13 +158,13 @@ static bool find_symbols( void find_symbols(const exprt &src, std::set &dest) { - find_symbols(kindt::F_EXPR, src, [&dest](const symbol_exprt &e) { + find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) { dest.insert(e); return true; }); } -bool has_symbol(const exprt &src, const irep_idt &identifier, kindt kind) +bool has_symbol(const exprt &src, const irep_idt &identifier, symbol_kindt kind) { return !find_symbols(kind, src, [&identifier](const symbol_exprt &e) { return e.get_identifier() != identifier; @@ -174,7 +173,7 @@ bool has_symbol(const exprt &src, const irep_idt &identifier, kindt kind) void find_type_symbols(const exprt &src, find_symbols_sett &dest) { - find_symbols(kindt::F_TYPE, src, [&dest](const symbol_exprt &e) { + find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) { dest.insert(e.get_identifier()); return true; }); @@ -182,7 +181,7 @@ void find_type_symbols(const exprt &src, find_symbols_sett &dest) void find_type_symbols(const typet &src, find_symbols_sett &dest) { - find_symbols(kindt::F_TYPE, src, [&dest](const symbol_exprt &e) { + find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) { dest.insert(e.get_identifier()); return true; }); @@ -192,25 +191,27 @@ void find_non_pointer_type_symbols( const exprt &src, find_symbols_sett &dest) { - find_symbols(kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) { - dest.insert(e.get_identifier()); - return true; - }); + find_symbols( + symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) { + dest.insert(e.get_identifier()); + return true; + }); } void find_non_pointer_type_symbols( const typet &src, find_symbols_sett &dest) { - find_symbols(kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) { - dest.insert(e.get_identifier()); - return true; - }); + find_symbols( + symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) { + dest.insert(e.get_identifier()); + return true; + }); } void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest) { - find_symbols(kindt::F_ALL, src, [&dest](const symbol_exprt &e) { + find_symbols(symbol_kindt::F_ALL, src, [&dest](const symbol_exprt &e) { dest.insert(e.get_identifier()); return true; }); @@ -218,7 +219,7 @@ void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest) void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest) { - find_symbols(kindt::F_ALL, src, [&dest](const symbol_exprt &e) { + find_symbols(symbol_kindt::F_ALL, src, [&dest](const symbol_exprt &e) { dest.insert(e.get_identifier()); return true; }); @@ -226,7 +227,7 @@ void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest) void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest) { - find_symbols(kindt::F_EXPR, src, [&dest](const symbol_exprt &e) { + find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) { dest.insert(e.get_identifier()); return true; }); @@ -234,7 +235,7 @@ void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest) void find_symbols(const exprt &src, find_symbols_sett &dest) { - find_symbols(kindt::F_EXPR, src, [&dest](const symbol_exprt &e) { + find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) { dest.insert(e.get_identifier()); return true; }); diff --git a/src/util/find_symbols.h b/src/util/find_symbols.h index 75741fcc533..46f85825be4 100644 --- a/src/util/find_symbols.h +++ b/src/util/find_symbols.h @@ -24,7 +24,7 @@ class typet; typedef std::unordered_set find_symbols_sett; /// Kinds of symbols to be considered by \ref has_symbol or \ref find_symbols. -enum class kindt +enum class symbol_kindt { /// Struct, union, or enum tag symbols. F_TYPE, @@ -39,7 +39,10 @@ enum class kindt /// Returns true if one of the symbols in \p src with identifier \p identifier /// is of kind \p kind. -bool has_symbol(const exprt &src, const irep_idt &identifier, kindt kind); +bool has_symbol( + const exprt &src, + const irep_idt &identifier, + symbol_kindt kind); DEPRECATED(SINCE(2022, 3, 14, "use find_symbols")) /// Add to the set \p dest the sub-expressions of \p src with id ID_symbol or From de7aa2514cb2d126ae4fe9315f5a5fc03a83a65b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 11 May 2022 10:40:12 +0000 Subject: [PATCH 7/8] Restrict has_symbol to symbol expressions and rename it to has_symbol_expr With the removal of support for ID_next_symbol all uses of `has_symbol` searched for symbol expressions only. --- src/ansi-c/goto_check_c.cpp | 2 +- src/goto-symex/postcondition.cpp | 4 +--- src/goto-symex/precondition.cpp | 2 +- src/util/find_symbols.cpp | 20 ++++++++++++++++++-- src/util/find_symbols.h | 25 ++++--------------------- 5 files changed, 25 insertions(+), 28 deletions(-) diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 2d299eb85af..2a2f2f1c8ab 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -466,7 +466,7 @@ void goto_check_ct::invalidate(const exprt &lhs) for(auto it = assertions.begin(); it != assertions.end();) { if( - has_symbol(it->second, lhs_id, symbol_kindt::F_EXPR) || + has_symbol_expr(it->second, lhs_id) || has_subexpr(it->second, ID_dereference)) { it = assertions.erase(it); diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp index 02f8b06c4fb..4d6e9ad7262 100644 --- a/src/goto-symex/postcondition.cpp +++ b/src/goto-symex/postcondition.cpp @@ -167,10 +167,8 @@ bool postconditiont::is_used( for(const exprt &e : value_set.get_value_set(to_dereference_expr(expr).pointer(), ns)) { - if(has_symbol(get_original_name(e), identifier, symbol_kindt::F_EXPR)) - { + if(has_symbol_expr(get_original_name(e), identifier)) return true; - } } return false; diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp index 2d304f79411..6cb9c170fed 100644 --- a/src/goto-symex/precondition.cpp +++ b/src/goto-symex/precondition.cpp @@ -117,7 +117,7 @@ void preconditiont::compute_rec(exprt &dest) for(const exprt &e : value_sets.get_values( SSA_step.source.function_id, target, deref_expr.pointer())) { - if(has_symbol(e, lhs_identifier, symbol_kindt::F_EXPR)) + if(has_symbol_expr(e, lhs_identifier)) { may_alias = true; break; diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index 291b9473beb..88cee3d0941 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -13,6 +13,22 @@ Author: Daniel Kroening, kroening@kroening.com #include "range.h" #include "std_expr.h" +/// Kinds of symbols to be considered by \ref has_symbol or \ref find_symbols. +enum class symbol_kindt +{ + /// Struct, union, or enum tag symbols. + F_TYPE, + /// Struct, union, or enum tag symbols when the expression using them is not a + /// pointer. + F_TYPE_NON_PTR, + /// Symbol expressions. + F_EXPR, + /// Symbol expressions, but excluding bindings. + F_EXPR_NOT_BOUND, + /// All of the above. + F_ALL +}; + bool has_symbol(const exprt &src, const find_symbols_sett &symbols) { if(src.id() == ID_symbol) @@ -164,9 +180,9 @@ void find_symbols(const exprt &src, std::set &dest) }); } -bool has_symbol(const exprt &src, const irep_idt &identifier, symbol_kindt kind) +bool has_symbol_expr(const exprt &src, const irep_idt &identifier) { - return !find_symbols(kind, src, [&identifier](const symbol_exprt &e) { + return !find_symbols(symbol_kindt::F_EXPR, src, [&identifier](const symbol_exprt &e) { return e.get_identifier() != identifier; }); } diff --git a/src/util/find_symbols.h b/src/util/find_symbols.h index 46f85825be4..26d5375408d 100644 --- a/src/util/find_symbols.h +++ b/src/util/find_symbols.h @@ -23,26 +23,9 @@ class typet; typedef std::unordered_set find_symbols_sett; -/// Kinds of symbols to be considered by \ref has_symbol or \ref find_symbols. -enum class symbol_kindt -{ - /// Struct, union, or enum tag symbols. - F_TYPE, - /// Struct, union, or enum tag symbols when the expression using them is not a - /// pointer. - F_TYPE_NON_PTR, - /// Symbol expressions. - F_EXPR, - /// All of the above. - F_ALL -}; - -/// Returns true if one of the symbols in \p src with identifier \p identifier -/// is of kind \p kind. -bool has_symbol( - const exprt &src, - const irep_idt &identifier, - symbol_kindt kind); +/// Returns true if one of the symbol expressions in \p src has identifier +/// \p identifier. +bool has_symbol_expr(const exprt &src, const irep_idt &identifier); DEPRECATED(SINCE(2022, 3, 14, "use find_symbols")) /// Add to the set \p dest the sub-expressions of \p src with id ID_symbol or @@ -87,7 +70,7 @@ inline find_symbols_sett find_symbol_identifiers(const exprt &src) return identifiers; } -DEPRECATED(SINCE(2022, 3, 14, "use has_symbol(exprt, irep_idt, symbol_kindt)")) +DEPRECATED(SINCE(2022, 3, 14, "use has_symbol_expr(exprt, irep_idt, bool)")) /// \return true if one of the symbols in \p src is present in \p symbols bool has_symbol( const exprt &src, From 5bf57efc6605fe519ade47b19ce80c8351b75f76 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 10 May 2022 12:08:21 +0000 Subject: [PATCH 8/8] find_symbols: support restriction to non-bound symbols Adds a new symbol kind to distinguish bound from unbound ones. Add documentation to all non-deprecated functions and clarify whether or not bound symbols are included. --- src/ansi-c/goto_check_c.cpp | 2 +- src/goto-symex/postcondition.cpp | 2 +- src/goto-symex/precondition.cpp | 2 +- src/util/find_symbols.cpp | 113 +++++++++++++++++++++++++------ src/util/find_symbols.h | 30 ++++++-- 5 files changed, 118 insertions(+), 31 deletions(-) diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 2a2f2f1c8ab..7a3762c1a04 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -466,7 +466,7 @@ void goto_check_ct::invalidate(const exprt &lhs) for(auto it = assertions.begin(); it != assertions.end();) { if( - has_symbol_expr(it->second, lhs_id) || + has_symbol_expr(it->second, lhs_id, false) || has_subexpr(it->second, ID_dereference)) { it = assertions.erase(it); diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp index 4d6e9ad7262..f262c597f2d 100644 --- a/src/goto-symex/postcondition.cpp +++ b/src/goto-symex/postcondition.cpp @@ -167,7 +167,7 @@ bool postconditiont::is_used( for(const exprt &e : value_set.get_value_set(to_dereference_expr(expr).pointer(), ns)) { - if(has_symbol_expr(get_original_name(e), identifier)) + if(has_symbol_expr(get_original_name(e), identifier, false)) return true; } diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp index 6cb9c170fed..afe0677f989 100644 --- a/src/goto-symex/precondition.cpp +++ b/src/goto-symex/precondition.cpp @@ -117,7 +117,7 @@ void preconditiont::compute_rec(exprt &dest) for(const exprt &e : value_sets.get_values( SSA_step.source.function_id, target, deref_expr.pointer())) { - if(has_symbol_expr(e, lhs_identifier)) + if(has_symbol_expr(e, lhs_identifier, false)) { may_alias = true; break; diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index 88cee3d0941..0bfaefb8ef6 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -23,8 +23,8 @@ enum class symbol_kindt F_TYPE_NON_PTR, /// Symbol expressions. F_EXPR, - /// Symbol expressions, but excluding bindings. - F_EXPR_NOT_BOUND, + /// Symbol expressions, but excluding bound variables. + F_EXPR_FREE, /// All of the above. F_ALL }; @@ -46,33 +46,77 @@ bool has_symbol(const exprt &src, const find_symbols_sett &symbols) static bool find_symbols( symbol_kindt, const typet &, - std::function); + std::function, + std::unordered_set &bindings); static bool find_symbols( symbol_kindt kind, const exprt &src, - std::function op) + std::function op, + std::unordered_set &bindings) { + if(kind == symbol_kindt::F_EXPR_FREE) + { + if(src.id() == ID_forall || src.id() == ID_exists || src.id() == ID_lambda) + { + const auto &binding_expr = to_binding_expr(src); + std::unordered_set new_bindings{bindings}; + for(const auto &v : binding_expr.variables()) + new_bindings.insert(v.get_identifier()); + + if(!find_symbols(kind, binding_expr.where(), op, new_bindings)) + return false; + + return find_symbols(kind, binding_expr.type(), op, bindings); + } + else if(src.id() == ID_let) + { + const auto &let_expr = to_let_expr(src); + std::unordered_set new_bindings{bindings}; + for(const auto &v : let_expr.variables()) + new_bindings.insert(v.get_identifier()); + + if(!find_symbols(kind, let_expr.where(), op, new_bindings)) + return false; + + if(!find_symbols(kind, let_expr.op1(), op, new_bindings)) + return false; + + return find_symbols(kind, let_expr.type(), op, bindings); + } + } + forall_operands(it, src) { - if(!find_symbols(kind, *it, op)) + if(!find_symbols(kind, *it, op, bindings)) return false; } - if(!find_symbols(kind, src.type(), op)) + if(!find_symbols(kind, src.type(), op, bindings)) return false; - if(kind == symbol_kindt::F_ALL || kind == symbol_kindt::F_EXPR) + if(src.id() == ID_symbol) { - if(src.id() == ID_symbol && !op(to_symbol_expr(src))) - return false; + const symbol_exprt &s = to_symbol_expr(src); + + if(kind == symbol_kindt::F_ALL || kind == symbol_kindt::F_EXPR) + { + if(!op(s)) + return false; + } + else if(kind == symbol_kindt::F_EXPR_FREE) + { + if(bindings.find(s.get_identifier()) == bindings.end() && !op(s)) + return false; + } } 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)) + !find_symbols( + kind, static_cast(c_sizeof_type), op, bindings)) { return false; } @@ -81,7 +125,7 @@ static bool find_symbols( if( va_arg_type.is_not_nil() && - !find_symbols(kind, static_cast(va_arg_type), op)) + !find_symbols(kind, static_cast(va_arg_type), op, bindings)) { return false; } @@ -92,20 +136,21 @@ static bool find_symbols( static bool find_symbols( symbol_kindt kind, const typet &src, - std::function op) + std::function op, + std::unordered_set &bindings) { 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)) + !find_symbols(kind, to_type_with_subtype(src).subtype(), op, bindings)) { return false; } for(const typet &subtype : to_type_with_subtypes(src).subtypes()) { - if(!find_symbols(kind, subtype, op)) + if(!find_symbols(kind, subtype, op, bindings)) return false; } @@ -126,26 +171,26 @@ static bool find_symbols( for(const auto &c : struct_union_type.components()) { - if(!find_symbols(kind, c, op)) + if(!find_symbols(kind, c, op, bindings)) 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)) + if(!find_symbols(kind, code_type.return_type(), op, bindings)) return false; for(const auto &p : code_type.parameters()) { - if(!find_symbols(kind, p, op)) + if(!find_symbols(kind, p, op, bindings)) 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)) + if(!find_symbols(kind, to_array_type(src).size(), op, bindings)) return false; } else if( @@ -172,6 +217,24 @@ static bool find_symbols( return true; } +static bool find_symbols( + symbol_kindt kind, + const typet &type, + std::function op) +{ + std::unordered_set bindings; + return find_symbols(kind, type, op, bindings); +} + +static bool find_symbols( + symbol_kindt kind, + const exprt &src, + std::function op) +{ + std::unordered_set bindings; + return find_symbols(kind, src, op, bindings); +} + void find_symbols(const exprt &src, std::set &dest) { find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) { @@ -180,11 +243,17 @@ void find_symbols(const exprt &src, std::set &dest) }); } -bool has_symbol_expr(const exprt &src, const irep_idt &identifier) +bool has_symbol_expr( + const exprt &src, + const irep_idt &identifier, + bool include_bound_symbols) { - return !find_symbols(symbol_kindt::F_EXPR, src, [&identifier](const symbol_exprt &e) { - return e.get_identifier() != identifier; - }); + return !find_symbols( + include_bound_symbols ? symbol_kindt::F_EXPR : symbol_kindt::F_EXPR_FREE, + src, + [&identifier](const symbol_exprt &e) { + return e.get_identifier() != identifier; + }); } void find_type_symbols(const exprt &src, find_symbols_sett &dest) diff --git a/src/util/find_symbols.h b/src/util/find_symbols.h index 26d5375408d..5679e24a29f 100644 --- a/src/util/find_symbols.h +++ b/src/util/find_symbols.h @@ -24,15 +24,20 @@ class typet; typedef std::unordered_set find_symbols_sett; /// Returns true if one of the symbol expressions in \p src has identifier -/// \p identifier. -bool has_symbol_expr(const exprt &src, const irep_idt &identifier); +/// \p identifier; if +/// \p include_bound_symbols is true, then bindings are included in the search. +bool has_symbol_expr( + const exprt &src, + const irep_idt &identifier, + bool include_bound_symbols); DEPRECATED(SINCE(2022, 3, 14, "use find_symbols")) /// Add to the set \p dest the sub-expressions of \p src with id ID_symbol or /// ID_next_symbol void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest); -/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol. +/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol, for +/// both free and bound variables. void find_symbols(const exprt &src, find_symbols_sett &dest); /// \return set of sub-expressions of the expressions contained in the range @@ -49,12 +54,14 @@ find_symbols_sett find_symbols_or_nexts(iteratort begin, iteratort end) return result; } -/// Find sub expressions with id ID_symbol +/// Find sub expressions with id ID_symbol, considering both free and bound +/// variables. void find_symbols( const exprt &src, std::set &dest); -/// Find sub expressions with id ID_symbol +/// Find sub expressions with id ID_symbol, considering both free and bound +/// variables. inline std::set find_symbols(const exprt &src) { std::set syms; @@ -62,7 +69,8 @@ inline std::set find_symbols(const exprt &src) return syms; } -/// Find identifiers of the sub expressions with id ID_symbol +/// Find identifiers of the sub expressions with id ID_symbol, considering both +/// free and bound variables. inline find_symbols_sett find_symbol_identifiers(const exprt &src) { find_symbols_sett identifiers; @@ -76,26 +84,36 @@ bool has_symbol( const exprt &src, const find_symbols_sett &symbols); +/// Collect all type tags contained in \p src and add them to \p dest. void find_type_symbols( const typet &src, find_symbols_sett &dest); +/// Collect all type tags contained in \p src and add them to \p dest. void find_type_symbols( const exprt &src, find_symbols_sett &dest); +/// Collect type tags contained in \p src when the expression of such a type is +/// not a pointer, and add them to \p dest. void find_non_pointer_type_symbols( const typet &src, find_symbols_sett &dest); +/// Collect type tags contained in \p src when the expression of such a type is +/// not a pointer, and add them to \p dest. 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. void find_type_and_expr_symbols( const typet &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. void find_type_and_expr_symbols( const exprt &src, find_symbols_sett &dest);