Use goto_functiont::parameter_identifiers and remove goto_functiont::type #4167

tautschnig · 2019-02-12T12:28:40Z

Having two function type definitions (one in the symbol table and one in
goto_functiont) is just prone to become inconsistent. Instead, always look at
the symbol table when we do need type information. If all we care about are the
identifiers we can still use goto_functiont::parameter_identifiers.

I'm also marking this RFC, @kroening in particular: it's quite painful to maintain consistency between parameter_identifiers and code_typet::parameters() - do we really need parameter_identifiers, or shouldn't we instead always use the information stored in the type?

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.

tautschnig · 2019-02-12T12:30:46Z

Also marking this do-not-review: I should try to break this up into a series of smaller commits that prepare the final change.

kroening · 2019-02-12T13:31:10Z

@tautschnig For a long list of reasons, it's best to get rid of the identifiers in code_typet::parameters() and only use the ones in goto_functiont.
I am happy to get rid of the signature in goto_functiont, for the reason that you are giving.

peterschrammel · 2019-02-12T13:44:10Z

On a side note: I've seen an issue with function pointer types recently: i.e. a function pointer variable has the original return type whereas the symbol table has return type void for the pointed function after the remove_return pass. Type consistency validations fail due to that.

kroening · 2019-02-12T21:54:31Z

On the side note: One cleanup item on my list is to change the way remove_returns works: the idea is to keep the return type as is. This removes the need to keep a copy of the original return type.

This is to enable a transition towards #4167.

This is to enable a transition towards diffblue#4167.

This is to enable a transition towards #4167.

Store identifiers of parameters in goto_functiont::parameter_identifiers [blocks: #4167]

kroening · 2020-11-12T07:33:55Z

I would leave the note about parameter_identifiers around for a while, say until codet::parametert::get_identifier() is gone.

tautschnig · 2020-11-12T08:14:10Z

I would leave the note about parameter_identifiers around for a while, say until codet::parametert::get_identifier() is gone.

Done, and updated - assuming that was the comment you were after.

kroening · 2020-11-12T09:41:56Z

Apologies for iterating on this PR.

The PR goes beyond the parameter identifiers, and also touches the "is hidden" feature. The question of whether or not the execution of a functions should be hidden is a property of the body (it's triggered via a label in the body), and not a property of the function signature.

It should therefore be in goto_functiont, and not the type.

codecov · 2020-11-12T10:06:37Z

Codecov Report

Merging #4167 (33d85ff) into develop (53750fa) will decrease coverage by 20.83%.
The diff coverage is 55.55%.

@@             Coverage Diff              @@
##           develop    #4167       +/-   ##
============================================
- Coverage    69.32%   48.48%   -20.84%     
============================================
  Files         1241     1005      -236     
  Lines       100406    84594    -15812     
============================================
- Hits         69604    41014    -28590     
- Misses       30802    43580    +12778

Flag	Coverage Δ
cproversmt2	`43.08% <55.55%> (+<0.01%)`	⬆️
regression	`?`
unit	`32.24% <50.00%> (-0.03%)`	⬇️

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

Impacted Files	Coverage Δ
src/assembler/remove_asm.cpp	`7.09% <0.00%> (-27.30%)`	⬇️
src/goto-programs/goto_function.cpp	`100.00% <ø> (ø)`
src/goto-programs/goto_functions.cpp	`51.16% <0.00%> (-31.77%)`	⬇️
src/goto-programs/link_goto_model.cpp	`0.00% <ø> (-80.86%)`	⬇️
src/goto-programs/read_bin_goto_object.cpp	`0.00% <0.00%> (-91.21%)`	⬇️
src/goto-programs/remove_complex.cpp	`89.18% <ø> (-0.10%)`	⬇️
src/goto-programs/remove_vector.cpp	`63.44% <ø> (-35.50%)`	⬇️
src/goto-checker/symex_coverage.cpp	`95.39% <100.00%> (ø)`
src/goto-programs/goto_convert_functions.cpp	`97.36% <100.00%> (-2.64%)`	⬇️
src/goto-programs/goto_function.h	`93.33% <100.00%> (-2.13%)`	⬇️
... and 804 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 53750fa...33d85ff. Read the comment docs.

martin-cs · 2020-11-12T12:11:42Z

@tautschnig Do you want this reviewed as is?

tautschnig · 2020-11-13T00:10:35Z

Apologies for iterating on this PR.

The PR goes beyond the parameter identifiers, and also touches the "is hidden" feature. The question of whether or not the execution of a functions should be hidden is a property of the body (it's triggered via a label in the body), and not a property of the function signature.

It should therefore be in goto_functiont, and not the type.

That all makes sense, but really means I should first revert #4312. I'll create a PR to that effect.

tautschnig · 2020-11-13T00:28:46Z

The "is hidden" PR is now posted as #5575.

tautschnig · 2020-11-13T10:58:07Z

@kroening @martin-cs This is now rebased on top of the changes implementing "is hidden" as requested.

martin-cs

Seems good.

martin-cs · 2020-11-13T15:03:02Z

src/goto-programs/goto_function.h

  /// The identifiers of the parameters of this function
  ///
  /// Note: This is now the preferred way of getting the identifiers of the
-  /// parameters. The identifiers in the type will go away.
+  /// parameters. The identifiers in the type are now gone.


I am afraid they are still there. "The type" here refers to the type in the symbol table.

Err, true. Change to the comment reverted/dropped.

Future changes will remove this member as it is redundant with the information stored in the symbol table. We keep writing to it so as not to break any users, but no longer read it.

Having two function type definitions (one in the symbol table and one in goto_functiont) is just prone to become inconsistent. Instead, always look at the symbol table when we do need type information. If all we care about are the identifiers we can still use goto_functiont::parameter_identifiers.

tautschnig added the RFC Request for comment label Feb 12, 2019

tautschnig assigned kroening Feb 12, 2019

tautschnig requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and thk123 as code owners February 12, 2019 12:28

tautschnig added the do not review label Feb 12, 2019

tautschnig self-assigned this Feb 12, 2019

kroening pushed a commit that referenced this pull request Feb 16, 2019

Store identifiers of parameters in goto_functiont::parameter_identifiers

548f19a

This is to enable a transition towards #4167.

kroening mentioned this pull request Feb 16, 2019

Store identifiers of parameters in goto_functiont::parameter_identifiers [blocks: #4167] #4207

Merged

3 tasks

tautschnig unassigned kroening Feb 19, 2019

tautschnig removed the RFC Request for comment label Feb 19, 2019

tautschnig changed the title ~~Use goto_functiont::parameter_identifiers and remove goto_functiont::type~~ Use goto_functiont::parameter_identifiers and remove goto_functiont::type [depends-on: #4207] Feb 21, 2019

tautschnig added dependent - do not merge and removed do not review labels Feb 21, 2019

tautschnig force-pushed the parameter-identifiers branch from a1631f1 to 2ec3300 Compare February 21, 2019 14:40

tautschnig pushed a commit to tautschnig/cbmc that referenced this pull request Feb 21, 2019

Store identifiers of parameters in goto_functiont::parameter_identifiers

5206e12

This is to enable a transition towards diffblue#4167.

tautschnig pushed a commit that referenced this pull request Feb 21, 2019

Store identifiers of parameters in goto_functiont::parameter_identifiers

f3774dc

This is to enable a transition towards #4167.

tautschnig pushed a commit that referenced this pull request Feb 21, 2019

Store identifiers of parameters in goto_functiont::parameter_identifiers

aa181b6

This is to enable a transition towards #4167.

tautschnig added a commit that referenced this pull request Feb 21, 2019

Merge pull request #4207 from diffblue/parameter_identifiers

88c9629

Store identifiers of parameters in goto_functiont::parameter_identifiers [blocks: #4167]

tautschnig changed the title ~~Use goto_functiont::parameter_identifiers and remove goto_functiont::type [depends-on: #4207]~~ Use goto_functiont::parameter_identifiers and remove goto_functiont::type [depends-on: #4251] Feb 21, 2019

tautschnig force-pushed the parameter-identifiers branch from 9004219 to d69301e Compare November 11, 2020 22:58

tautschnig added cleanup and removed do not merge Needs rebase labels Nov 11, 2020

tautschnig assigned kroening and unassigned tautschnig Nov 11, 2020

tautschnig changed the title ~~Use goto_functiont::parameter_identifiers and remove goto_functiont::type [do not merge before 2019-08-16]~~ Use goto_functiont::parameter_identifiers and remove goto_functiont::type Nov 11, 2020

tautschnig force-pushed the parameter-identifiers branch from d69301e to 09290cc Compare November 12, 2020 08:13

tautschnig force-pushed the parameter-identifiers branch from 09290cc to 67aa39c Compare November 12, 2020 09:27

tautschnig force-pushed the parameter-identifiers branch from 67aa39c to f3f4da1 Compare November 13, 2020 10:47

kroening approved these changes Nov 13, 2020

View reviewed changes

tautschnig assigned peterschrammel, martin-cs and hannes-steffenhagen-diffblue and unassigned kroening Nov 13, 2020

martin-cs approved these changes Nov 13, 2020

View reviewed changes

tautschnig added 2 commits November 13, 2020 20:54

Do not read from goto_functiont::type

35456a2

Future changes will remove this member as it is redundant with the information stored in the symbol table. We keep writing to it so as not to break any users, but no longer read it.

tautschnig force-pushed the parameter-identifiers branch from f3f4da1 to 33d85ff Compare November 13, 2020 20:54

tautschnig merged commit ee3b3fb into diffblue:develop Nov 13, 2020

tautschnig deleted the parameter-identifiers branch November 13, 2020 22:47

tautschnig mentioned this pull request Jan 16, 2021

Get rid of parameter_identifiers #1695

Closed

Use goto_functiont::parameter_identifiers and remove goto_functiont::type #4167

Use goto_functiont::parameter_identifiers and remove goto_functiont::type #4167

Uh oh!

Conversation

tautschnig commented Feb 12, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig commented Feb 12, 2019

Uh oh!

kroening commented Feb 12, 2019

Uh oh!

peterschrammel commented Feb 12, 2019

Uh oh!

kroening commented Feb 12, 2019

Uh oh!

kroening commented Nov 12, 2020

Uh oh!

tautschnig commented Nov 12, 2020

Uh oh!

kroening commented Nov 12, 2020

Uh oh!

codecov bot commented Nov 12, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

martin-cs commented Nov 12, 2020

Uh oh!

tautschnig commented Nov 13, 2020

Uh oh!

tautschnig commented Nov 13, 2020

Uh oh!

tautschnig commented Nov 13, 2020

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs Nov 13, 2020

Choose a reason for hiding this comment

Uh oh!

kroening Nov 13, 2020

Choose a reason for hiding this comment

Uh oh!

tautschnig Nov 13, 2020

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig commented Feb 12, 2019 •

edited

Loading

codecov bot commented Nov 12, 2020 •

edited

Loading