From ea472cb09d34ca2bd1111695c08ff5d7ea1ec790 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 Mar 2022 08:59:43 +0000 Subject: [PATCH] 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 6a8492275c0..5fb42d06822 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,