Skip to content

Commit 35336a4

Browse files
committed
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.
1 parent b4e8664 commit 35336a4

File tree

7 files changed

+53
-48
lines changed

7 files changed

+53
-48
lines changed

src/goto-instrument/accelerate/accelerate.cpp

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -379,21 +379,16 @@ void acceleratet::add_dirty_checks()
379379

380380
// Find which symbols are read, i.e. those appearing in a guard or on
381381
// the right hand side of an assignment. Assume each is not dirty.
382-
find_symbols_sett read;
382+
std::set<symbol_exprt> read;
383383

384384
if(it->has_condition())
385-
find_symbols_or_nexts(it->get_condition(), read);
385+
find_symbols(it->get_condition(), read);
386386

387387
if(it->is_assign())
388-
{
389-
find_symbols_or_nexts(it->assign_rhs(), read);
390-
}
388+
find_symbols(it->assign_rhs(), read);
391389

392-
for(find_symbols_sett::iterator jt=read.begin();
393-
jt!=read.end();
394-
++jt)
390+
for(const auto &var : read)
395391
{
396-
const exprt &var=ns.lookup(*jt).symbol_expr();
397392
expr_mapt::iterator dirty_var=dirty_vars_map.find(var);
398393

399394
if(dirty_var==dirty_vars_map.end())

src/goto-instrument/accelerate/acceleration_utils.cpp

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -198,18 +198,19 @@ void acceleration_utilst::stash_variables(
198198
expr_sett modified,
199199
substitutiont &substitution)
200200
{
201-
find_symbols_sett vars =
202-
find_symbols_or_nexts(modified.begin(), modified.end());
203-
const irep_idt &loop_counter_name =
204-
to_symbol_expr(loop_counter).get_identifier();
205-
vars.erase(loop_counter_name);
201+
const symbol_exprt &loop_counter_sym = to_symbol_expr(loop_counter);
206202

207-
for(const irep_idt &symbol : vars)
203+
std::set<symbol_exprt> vars;
204+
for(const exprt &expr : modified)
205+
find_symbols(expr, vars);
206+
207+
vars.erase(loop_counter_sym);
208+
209+
for(const symbol_exprt &orig : vars)
208210
{
209-
const symbolt &orig = symbol_table.lookup_ref(symbol);
210-
symbolt stashed_sym=fresh_symbol("polynomial::stash", orig.type);
211-
substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
212-
program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());
211+
symbolt stashed_sym = fresh_symbol("polynomial::stash", orig.type());
212+
substitution[orig] = stashed_sym.symbol_expr();
213+
program.assign(stashed_sym.symbol_expr(), orig);
213214
}
214215
}
215216

src/goto-instrument/dump_c.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -913,9 +913,7 @@ void dump_ct::convert_global_variable(
913913

914914
code_frontend_declt d(symbol.symbol_expr());
915915

916-
find_symbols_sett syms;
917-
if(symbol.value.is_not_nil())
918-
find_symbols_or_nexts(symbol.value, syms);
916+
find_symbols_sett syms = find_symbol_identifiers(symbol.value);
919917

920918
// add a tentative declaration to cater for symbols in the initializer
921919
// relying on it this symbol

src/goto-instrument/full_slicer.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ void full_slicert::add_decl_dead(
6262

6363
find_symbols_sett syms;
6464

65-
node.PC->apply([&syms](const exprt &e) { find_symbols_or_nexts(e, syms); });
65+
node.PC->apply([&syms](const exprt &e) { find_symbols(e, syms); });
6666

6767
for(find_symbols_sett::const_iterator
6868
it=syms.begin();

src/goto-programs/goto_program.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -760,8 +760,7 @@ void goto_programt::instructiont::validate(
760760

761761
auto expr_symbol_finder = [&](const exprt &e) {
762762
find_symbols_sett typetags;
763-
find_type_symbols(e.type(), typetags);
764-
find_symbols_or_nexts(e, typetags);
763+
find_type_and_expr_symbols(e, typetags);
765764
const symbolt *symbol;
766765
for(const auto &identifier : typetags)
767766
{
@@ -873,7 +872,7 @@ void goto_programt::instructiont::validate(
873872
"assert instruction should not have a target",
874873
source_location());
875874

876-
std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
875+
expr_symbol_finder(guard);
877876
std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
878877
break;
879878
case OTHER:
@@ -940,7 +939,7 @@ void goto_programt::instructiont::validate(
940939
"function call instruction should contain a call statement",
941940
source_location());
942941

943-
std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
942+
expr_symbol_finder(code);
944943
std::for_each(code.depth_begin(), code.depth_end(), type_finder);
945944
break;
946945
case THROW:

src/util/find_symbols.cpp

Lines changed: 22 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -13,25 +13,6 @@ Author: Daniel Kroening, [email protected]
1313
#include "range.h"
1414
#include "std_expr.h"
1515

16-
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
17-
{
18-
find_symbols(src, dest, true, true);
19-
}
20-
21-
void find_symbols(
22-
const exprt &src,
23-
find_symbols_sett &dest,
24-
bool current,
25-
bool next)
26-
{
27-
src.visit_pre([&dest, current, next](const exprt &e) {
28-
if(e.id() == ID_symbol && current)
29-
dest.insert(to_symbol_expr(e).get_identifier());
30-
else if(e.id() == ID_next_symbol && next)
31-
dest.insert(e.get(ID_identifier));
32-
});
33-
}
34-
3516
bool has_symbol(
3617
const exprt &src,
3718
const find_symbols_sett &symbols,
@@ -215,3 +196,25 @@ void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest)
215196
{
216197
find_symbols(kindt::F_ALL, src, dest);
217198
}
199+
200+
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
201+
{
202+
find_symbols(kindt::F_EXPR_BOTH, src, dest);
203+
}
204+
205+
void find_symbols(
206+
const exprt &src,
207+
find_symbols_sett &dest,
208+
bool current,
209+
bool next)
210+
{
211+
if(current)
212+
{
213+
if(next)
214+
find_symbols(kindt::F_EXPR_BOTH, src, dest);
215+
else
216+
find_symbols(kindt::F_EXPR_CURRENT, src, dest);
217+
}
218+
else if(next)
219+
find_symbols(kindt::F_EXPR_NEXT, src, dest);
220+
}

src/util/find_symbols.h

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -45,21 +45,30 @@ enum class kindt
4545
/// is of kind \p kind.
4646
bool has_symbol(const exprt &src, const irep_idt &identifier, kindt kind);
4747

48+
DEPRECATED(SINCE(2022, 3, 14, "use find_symbols"))
4849
/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol or
4950
/// ID_next_symbol
5051
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest);
5152

53+
/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol if
54+
/// \p current is true, and ID_next_symbol if \p next is true
55+
void find_symbols(
56+
const exprt &src,
57+
find_symbols_sett &dest,
58+
bool current = true,
59+
bool next = true);
60+
5261
/// \return set of sub-expressions of the expressions contained in the range
5362
/// defined by \p begin and \p end which have id ID_symbol or ID_next_symbol
5463
template <typename iteratort>
64+
DEPRECATED(SINCE(2022, 3, 14, "use find_symbols and a local iteration"))
5565
find_symbols_sett find_symbols_or_nexts(iteratort begin, iteratort end)
5666
{
5767
static_assert(
5868
std::is_base_of<exprt, typename iteratort::value_type>::value,
5969
"find_symbols takes exprt iterators as arguments");
6070
find_symbols_sett result;
61-
std::for_each(
62-
begin, end, [&](const exprt &e) { find_symbols_or_nexts(e, result); });
71+
std::for_each(begin, end, [&](const exprt &e) { find_symbols(e, result); });
6372
return result;
6473
}
6574

0 commit comments

Comments
 (0)