Remove base_type_eq

[kroening]

These are no longer needed, as symbol_type is no longer in use.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a 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.

[tautschnig]

I'm worried that this will break linking, where semantic equality still matters as tag names can reasonably differ.

Also, I think it is necessary to implement this change as a collection of smaller commits to aid (very likely) future debugging. With a change this size it will be very difficult to revert, and bisecting to identify which of the hunks caused trouble is difficult. Furthermore we'd in the current set-up be completely blocked on the known issues in the Java front-end, even though in theory it ought to be possible to remove any use of (base_)type_eq from C/C++ front-ends.

[kroening]

Will do C/C++ first; the rest will need to sit for a few months.

[smowton]

@kroening @tautschnig I tried to rebase #4021 yesterday, but found that it continued to stumble on cases where base_type_eq and operator== disagreed about when types matched.

I took a look at why we can't merge this yet, and found the following fixups:
#4170: simple tag-vs-followed bug in is_not_zero
#4171: string preprocessor using expanded types
#4172: generic tests rely on base_type_eq to strip generic info or array member types

I also made #4173 with a value-set fix and some cosmetic / comment improvements that I think should be picked into this PR.

[smowton]

Status with all four of those merged: Java tests all pass, C tests all pass apart from Float-div2, Float-div3, noop1, all of which fail due to a disagreement between a stub symbol being of type f(void) vs. f(), aka f(...) (manifesting as ellipsis: 1). Would appreciate someone with more familiarity with the C front-end taking a look at how that ought to work.

[smowton]

Finished testing this with test-gen, successfully. Results:

Required CBMC PRs:

• Simplify and avoid redundant typecasts in build_object_descriptor #4183
• Java object factory: pass function ID to factory routine #4184
• Symex-dereference: simplify after deref [blocks: #2574, #4056] #3725
  • byte_update against a pointer shouldn't be fatal #4185

Test-gen demonstration bump: https://github.com/diffblue/test-gen/pull/3049
Part of which can be merged without the bump: https://github.com/diffblue/test-gen/pull/3048

[codecov]

Codecov Report

Merging #4056 (7a744e6) into develop (c43385b) will decrease coverage by 0.00%.
The diff coverage is 62.96%.

@@             Coverage Diff             @@
##           develop    #4056      +/-   ##
===========================================
- Coverage    69.50%   69.50%   -0.01%     
===========================================
  Files         1243     1242       -1     
  Lines       100674   100580      -94     
===========================================
- Hits         69977    69908      -69     
+ Misses       30697    30672      -25     

Flag	Coverage Δ
cproversmt2	43.11% <38.46%> (-0.04%)	⬇️
regression	66.39% <62.96%> (-0.01%)	⬇️
unit	32.26% <7.69%> (+<0.01%)	⬆️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/goto-instrument/value_set_fi_fp_removal.cpp	86.84% <ø> (ø)
src/goto-programs/link_goto_model.cpp	79.54% <ø> (ø)
src/linking/linking.cpp	57.74% <58.33%> (+0.59%)	⬆️
src/analyses/does_remove_const.cpp	100.00% <100.00%> (ø)
src/goto-instrument/replace_calls.cpp	89.13% <100.00%> (-0.24%)	⬇️
src/goto-programs/goto_program.cpp	62.16% <100.00%> (ø)

---

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 c43385b...7a744e6. Read the comment docs.

[tautschnig]

Approving , but @kroening: please double-check as I've added two commits of my own to make yours work. (Edit: those commits were moved to PRs of there own and have since been merged.)

[tautschnig]

#6989 now takes care of most of the uses, with only three uses remaining thereafter.

[tautschnig]

Closing as this was now completed in #6989.