[CONTRACTS] Add loop-contract symbols into symbol table during typecheck

[qinheping]

Currently, when type-checking functions with contracts, we only keep function contracts symbols (see https://github.com/diffblue/cbmc/blob/develop/src/linking/remove_internal_symbols.cpp#L69). It was OK as there couldn't be any new symbol declared in loop contracts. However, if we want to support statement expressions or pure functions in loop contracts, we shouldn't remove loop contract symbols during type checking.

This PR will keep symbols in loop contracts---not removing them in remove_internal_symbols. In detail, we not only find symbols in sub-expressions (find_symbols) but also find symbols in given named subs (find_symbols_in_expr_and_subs) when finding symbols to keep.

The test of #8360 covers the change of this PR.

• 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.
• 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).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Attention: Patch coverage is 56.25000% with 28 lines in your changes missing coverage. Please review.

Project coverage is 78.28%. Comparing base (582aa69) to head (32ed640).
Report is 2 commits behind head on develop.

Files	Patch %	Lines
src/util/find_symbols.cpp	54.23%	27 Missing ⚠️
src/linking/remove_internal_symbols.cpp	80.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8359      +/-   ##
===========================================
- Coverage    78.28%   78.28%   -0.01%     
===========================================
  Files         1726     1726              
  Lines       188577   188594      +17     
  Branches     18443    18230     -213     
===========================================
+ Hits        147629   147641      +12     
- Misses       40948    40953       +5     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[tautschnig]

Approving of the goal, but I think the implementation should look a little different. See detailed comments.

[tautschnig]

You could substantially reduce the churn by adding a variant of find_symbols_in_expr_and_subs that either doesn't require the "subs" argument, or uses a default value of {}. By extension of this I'd argue that you can reduce churn even further by just making find_symbols have this capability.

[qinheping]

Sounds great. I made the static find_symbols take the "subs" argument without default value and the public function find_type_and_expr_symbols take the subs argument with the default value of {}.

[tautschnig]

Hmm, I think if you did it the other way around (make the non-public function use a default value) you could substantially reduce the size of the diff in this PR. Also, I don't think the default value on the (new!) public function adds as much value for any use of that function without the third argument just amounts to using one of the other, pre-existing functions.

[qinheping]

I moved the default value to the static function and it actually reduce the diff of this PR.
The public function with the new subs_to_find argument is different from other pre-existing functions. It calls the static function find_symbols with kind symbol_kindt::F_ALL while others call find_symbols with different kind arguments.

[kroening]

I strongly disagree with this PR, and would like to see it reverted. There is a fundamental misunderstanding how bound symbols work. In particular, they should never show up in the symbol table.

[kroening]

I appreciate this is trying to fix something, but there needs to be an entirely different approach for this fix.

[qinheping]

I strongly disagree with this PR, and would like to see it reverted. There is a fundamental misunderstanding how bound symbols work. In particular, they should never show up in the symbol table.

This PR will add the symbols declared in loop contracts into the symbol table so that we can in the future allow non side_effect_exprt in loop contracts such as pure functions and side-effect free statement expression. I reused the find-symbols function that we used for function contracts and didn't realize that find_type_and_expr_symbols will add bound symbols. Isn't the issue of including bound variables in symbol table also in function contracts? I think they should both use the version of find_symbols that excluding bound variables, i.e., with kind F_EXPR_FREE. I can open a PR to fix it. @kroening What do you think?