Cleanup find_symbols API

[tautschnig]

The various functions declared in find_symbols.h might sound alike, but actually have different semantics. I wasn't really sure what to use anymore, so I went for a cleanup instead. Requires #6725 and #6726. Please review commit-by-commit.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[kroening]

This function is trying to do too much.

1. Type-symbols and 'normal ones' are really very different, and the use-cases won't overlap. I'd make these separate functions.
2. I don't think next_symbol is used anywhere in this repo. It can go away.
3. This leaves bound vs. non-bound symbols. How about passing that as a category to a functor?

[codecov]

Codecov Report

Merging #6727 (5bf57ef) into develop (5d74a03) will decrease coverage by 0.00%.
The diff coverage is 74.24%.

@@             Coverage Diff             @@
##           develop    #6727      +/-   ##
===========================================
- Coverage    77.78%   77.78%   -0.01%     
===========================================
  Files         1567     1567              
  Lines       179701   179769      +68     
===========================================
+ Hits        139789   139840      +51     
- Misses       39912    39929      +17     

Impacted Files	Coverage Δ
src/analyses/interval_analysis.cpp	0.00% <0.00%> (ø)
src/ansi-c/expr2c.cpp	67.63% <ø> (+0.03%)	⬆️
src/goto-instrument/accelerate/accelerate.cpp	32.28% <0.00%> (+0.33%)	⬆️
.../goto-instrument/accelerate/acceleration_utils.cpp	2.23% <0.00%> (+<0.01%)	⬆️
src/goto-instrument/accelerate/trace_automaton.cpp	0.00% <ø> (ø)
src/goto-instrument/wmm/data_dp.cpp	75.71% <ø> (ø)
src/goto-programs/goto_program.h	90.70% <ø> (ø)
src/solvers/flattening/arrays.cpp	81.45% <ø> (ø)
src/util/find_symbols.cpp	65.71% <65.48%> (-18.45%)	⬇️
src/pointer-analysis/value_set_fi.cpp	69.83% <66.66%> (+0.04%)	⬆️
... and 34 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 6061711...5bf57ef. Read the comment docs.

[tautschnig]

This function is trying to do too much.

1. Type-symbols and 'normal ones' are really very different, and the use-cases won't overlap. I'd make these separate functions.

That makes a lot of sense as far as the user-facing API is concerned (which already has different functions), but I'm not sure the underlying implementation would be very different? Expressions can be contained in types and types in expressions, so the iteration will be rather similar?

2. I don't think next_symbol is used anywhere in this repo. It can go away.

The precondition and postcondition code presumably still supports it, but likely no one cares. I'll clean this up.

3. This leaves bound vs. non-bound symbols. How about passing that as a category to a functor?

With the above changes this might end up as nothing more than a Boolean? I'll give it a try.

[kroening]

That makes a lot of sense as far as the user-facing API is concerned (which already has different functions), but I'm not sure the underlying implementation would be very different? Expressions can be contained in types and types in expressions, so the iteration will be rather similar?

I can certainly see a case for offering separate, easy functions as part of the user-facing API, which then call one (complex) function internally to avoid code duplication.

The precondition and postcondition code presumably still supports it, but likely no one cares. I'll clean this up.

next_symbol is not to be confused with __CPROVER_old -- I don't believe pre/postconditions ever used next_symbol.

With the above changes this might end up as nothing more than a Boolean? I'll give it a try.

Super!

[tautschnig]

@kroening I hope that the state at the end of commit series in this PR matches your expectations. The individual commits should be meaningful, but there is some back&forth, so it's probably best to either checkout the branch or just review all code changes at once.

[kroening]

1. Comments: you may wish to call the non-bound variables the 'free variables'.
2. Can you add an explicit comment whether or not bound variables are considered?
3. Is there a use-case for finding both free and the bound variables in the codebase?

[tautschnig]

1. Comments: you may wish to call the non-bound variables the 'free variables'.

Thank you, done.

2. Can you add an explicit comment whether or not bound variables are considered?

Done.

3. Is there a use-case for finding both free and the bound variables in the codebase?

I cannot rule out that such a case exists, but I'm not currently aware of one. There may well be places that currently feature a local lookalike of find_symbols.

[kroening]

5. Is there a use-case for finding both free and the bound variables in the codebase?

I cannot rule out that such a case exists, but I'm not currently aware of one. There may well be places that currently feature a local lookalike of find_symbols.

Let's go with the PR as is for now. In the long term, it makes sense to change the default semantics of the find_symbol functions to exclude the bound symbols. I strongly suspect that this is what all users want.