Remove void_typet #4102

tautschnig · 2019-02-05T21:57:30Z

I suggest reviewing commit-by-commit.

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.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 75d5d28).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99859081
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

tautschnig · 2019-02-06T00:02:00Z

I'm assuming the bot failure is genuine: @svorenova @thk123 whenever time permits, could you scan TG for occurrences of void_typet and update this as is done in the commits in this PR? That should be safe to do without depending on the changes in this PR.

kroening · 2019-02-06T09:56:17Z

You could also change typet void_type(); in c_types.h to return empty_typet.

majakusber · 2019-02-06T12:14:33Z

@tautschnig I made the companion PR here: https://github.com/diffblue/test-gen/pull/2999 Note that I would like to merge my PR before this one, to avoid clash.

tautschnig · 2019-02-06T13:09:18Z

@svorenova Thank you very much - yes, please do let me know when it's merged, I'd like to keep the bot (and thus TG) happy at all times to avoid spurious messages being posted.

tautschnig · 2019-02-06T15:29:26Z

You could also change typet void_type(); in c_types.h to return empty_typet.

Done, which made some further room for improvement apparent. I hope the additional 5 commits are ok to be in this PR.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 8a28d16).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99961187
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

majakusber · 2019-02-06T19:08:53Z

I updated the companion PR https://github.com/diffblue/test-gen/pull/2999

majakusber · 2019-02-07T10:57:16Z

@tautschnig The companion PR is merged now, you can merge this 👍

void_typet and empty_typet are effectively the same, but weren't consistently used and thus void_typet is going away.

There was a mix of empty_typet, void_typet, and actual uses of java_void_type. At the moment, they are all the same, but there is no compile-time guarantee that this remains true.

void_typet was only sometimes used.

void_typet had 25 uses across the codebase, while its equivalent empty_typet has 84 uses. Only sometimes using "void_typet" requires that empty_typet and void_typet forever stay the same.

This is consistent with what is done in the Java front-end. Also use the same trick to construct only a single, shared instance of it.

Should we ever choose to add any annotations consistent use of the generator function will ensure these are available.

Use empty_typet as done in all other places.

This has been cleaned up in f573d97 already, and future changes might see complete removal of type() from codet.

Don't do incremental updates which may result in objects that do not match what we build via constructors.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 32f4aa5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100076282

NlightNFotis · 2019-02-08T10:26:45Z

Now this has been merged, but I have a question: Wouldn't it be better instead of completely removing void_typet to instead alias it to empty_typet?

That would make the API better and the semantics of some code much closer to the semantics of the languages they supposedly model (like C code). Because as far I understand the empty type is a concept present on functional languages. C descendants use void for the the same thing?

tautschnig · 2019-02-08T10:32:36Z

I had pondered to introduce a typedef, but my main concern was that there was no consistent use of one or the other. I have tried to clean this up, and now ended up (trying to) make consistent use of java_void_type() in the Java front-end, and void_type() in the C and C++ front-ends. I think that's fairly clean within the language front-ends now. That leaves as concern that those still return an empty_typet, but I think that's actually good, because we are converting towards goto programs, not either of the languages. If anything, we've probably been too close to C in the middle-end I think.

tautschnig added the cleanup label Feb 5, 2019

tautschnig requested review from cesaro, chrisr-diffblue, cristina-david, kroening, martin-cs, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners February 5, 2019 21:57

peterschrammel approved these changes Feb 5, 2019

View reviewed changes

tautschnig assigned kroening Feb 5, 2019

allredj reviewed Feb 5, 2019

View reviewed changes

tautschnig assigned thk123 and majakusber Feb 6, 2019

majakusber assigned antlechner and unassigned thk123 and majakusber Feb 6, 2019

kroening approved these changes Feb 6, 2019

View reviewed changes

kroening removed their assignment Feb 6, 2019

majakusber assigned majakusber and unassigned antlechner Feb 6, 2019

majakusber added the do not merge label Feb 6, 2019

tautschnig force-pushed the remove-void_typet branch from 75d5d28 to 8a28d16 Compare February 6, 2019 15:27

allredj reviewed Feb 6, 2019

View reviewed changes

majakusber removed the do not merge label Feb 7, 2019

tautschnig added 9 commits February 7, 2019 11:24

java_void_type() is now empty_typet

b934052

void_typet and empty_typet are effectively the same, but weren't consistently used and thus void_typet is going away.

Consistently use java_void_type

9a61f1a

There was a mix of empty_typet, void_typet, and actual uses of java_void_type. At the moment, they are all the same, but there is no compile-time guarantee that this remains true.

Always use empty_typet instead of void_typet

e15756d

void_typet was only sometimes used.

Remove void_typet

b04bb82

void_typet had 25 uses across the codebase, while its equivalent empty_typet has 84 uses. Only sometimes using "void_typet" requires that empty_typet and void_typet forever stay the same.

Make void_type() return empty_typet()

e3232c7

This is consistent with what is done in the Java front-end. Also use the same trick to construct only a single, shared instance of it.

Consistently use void_type() in the C/C++ front-end

20c9977

Should we ever choose to add any annotations consistent use of the generator function will ensure these are available.

Don't use void_type() outside the C/C++ front-end

26ad5c9

Use empty_typet as done in all other places.

Do not mark codet objects as having typet(ID_code)

661dd88

This has been cleaned up in f573d97 already, and future changes might see complete removal of type() from codet.

Use constructors to build code(-like) objects

32f4aa5

Don't do incremental updates which may result in objects that do not match what we build via constructors.

tautschnig force-pushed the remove-void_typet branch from 8a28d16 to 32f4aa5 Compare February 7, 2019 11:24

tautschnig assigned tautschnig and unassigned majakusber Feb 7, 2019

allredj reviewed Feb 7, 2019

View reviewed changes

tautschnig merged commit 2dc0863 into diffblue:develop Feb 7, 2019

tautschnig deleted the remove-void_typet branch February 7, 2019 13:11

tautschnig mentioned this pull request Jan 16, 2021

Remove one of empty_typet or void_typet #2780

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Remove void_typet #4102

Remove void_typet #4102

Uh oh!

tautschnig commented Feb 5, 2019

Uh oh!

allredj left a comment

Uh oh!

tautschnig commented Feb 6, 2019

Uh oh!

kroening commented Feb 6, 2019

Uh oh!

majakusber commented Feb 6, 2019

Uh oh!

tautschnig commented Feb 6, 2019

Uh oh!

tautschnig commented Feb 6, 2019

Uh oh!

allredj left a comment

Uh oh!

majakusber commented Feb 6, 2019

Uh oh!

majakusber commented Feb 7, 2019

Uh oh!

allredj left a comment

Uh oh!

NlightNFotis commented Feb 8, 2019 •

edited

Loading

Uh oh!

tautschnig commented Feb 8, 2019

Uh oh!

Uh oh!

Remove void_typet #4102

Remove void_typet #4102

Uh oh!

Conversation

tautschnig commented Feb 5, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Feb 6, 2019

Uh oh!

kroening commented Feb 6, 2019

Uh oh!

majakusber commented Feb 6, 2019

Uh oh!

tautschnig commented Feb 6, 2019

Uh oh!

tautschnig commented Feb 6, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

majakusber commented Feb 6, 2019

Uh oh!

majakusber commented Feb 7, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Uh oh!

tautschnig commented Feb 8, 2019

Uh oh!

Uh oh!

NlightNFotis commented Feb 8, 2019 •

edited

Loading