Cleanup types [DOC-12] #2815

majakusber · 2018-08-22T11:10:55Z

This is a follow-up PR to #2771 (it is based on top of it so please ignore the Add documentation commits until it's merged and rebased).

tautschnig · 2018-08-22T14:05:00Z

It's a bit of a daring ask, but would you mind tackling #2780, #2808, and possibly even #2810 as well? The last one is likely taking it a bit too far, but the first two might be reasonable? Thank you!!!

tautschnig

I think this is great cleanup work, though it may be better to do some of this in several small PRs for work not to be held up in case some of it turns out to be controversial.

tautschnig · 2018-08-22T14:06:58Z

src/util/type.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]

 #include "type.h"
 #include "std_types.h"
-#include "namespace.h"


I think (and this would make me rather happy) std_types.h could go as well? That finally resolves a dependency that should not have existed in the first place...

tautschnig · 2018-08-22T14:07:34Z

jbmc/src/java_bytecode/ci_lazy_methods_needed.h

@@ -16,6 +16,7 @@ Author: Chris Smowton, [email protected]
 #include <set>
 #include <unordered_set>
 #include <util/symbol_table.h>
+#include <util/namespace.h>


Nit pick: please sort lexicographically.

tautschnig · 2018-08-22T14:08:06Z

src/util/std_types.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include "string2int.h"
 #include "arith_tools.h"
 #include "std_expr.h"
+#include "namespace.h"


As above: please sort lexicographically, likely making a slightly bigger change than necessary (sort all of them).

tautschnig · 2018-08-22T14:16:26Z

src/util/std_expr.h

@@ -20,7 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include "invariant.h"
 #include "std_types.h"
 #include "expr_cast.h"
-
+#include "mathematical_types.h"


Nit pick: maintain/establish lexicographic sorting

tautschnig · 2018-08-22T14:17:28Z

src/util/c_types.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_UTIL_C_TYPES_H

 #include "std_types.h"
+#include "mathematical_types.h"


I guess that's really just for complex_typet? Maybe keep that in std_types.h?

It's a mathematical type so if we're moving some of them into a separate file, it only makes sense if we really move all of them. Is there any particular reason why this stands out for you?

I thought it was the one that's actually used by C/C++ front-ends, but maybe it's not even the only one.

You are right, there is std::complex type, moving back to std_types.

majakusber · 2018-08-22T14:44:09Z

@tautschnig We only had one day booked for doc changes and I'm already out of time :) I'll make sure those issues are put on the next doc day to-do list.

majakusber · 2018-08-22T14:55:35Z

I've split out two of the changes into separate PRs:

tautschnig · 2018-08-22T15:27:06Z

We only had one day booked for doc changes and I'm already out of time :)

I know, I'm greedy :-) Thanks a lot for all the work!

majakusber · 2018-08-22T16:18:13Z

Test-gen pointer bump: https://github.com/diffblue/test-gen/pull/2192

kroening · 2018-08-23T09:21:51Z

I find the can_cast_type<symbol_typet>(type1) idiom to be hard to read, and it doesn't add value beyond the one-off. We should not do that.

tautschnig · 2018-08-23T09:48:09Z

In response to @kroening: see ba01589 from #2595, which in turn was a side track of #2205.

majakusber · 2018-08-23T12:22:50Z

Yes, the comment in guidelines was exactly my motivation to add missing cast checks.

majakusber · 2018-08-23T12:24:17Z

There is a failing test on the test-gen pointer bump, I will investigate it later. Until then I added do not merge label.

kroening · 2018-08-24T09:03:32Z

@tautschnig Yes; I understand the motivation for can_cast. However, I'd still like to stick to the if(x.id() ==ID_Z) idiom. In particular, we can then eventually do switch(x.id()).

majakusber · 2018-09-11T13:40:11Z

@kroening Introducing can_casts does not really prevent to access id directly. On top of the motivation that was already mentioned, I recently learned that can_cast is used by type/expr_try_dynamic_cast which can be quite handy as it can be used in if conditions and directly assign the result - thus replacing two lines of can_cast+cast by one (see the third commit in this PR).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 3ced6c7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84437357
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).

allredj

Passed Diffblue compatibility checks (cbmc commit: 3ced6c7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84452470

allredj

Passed Diffblue compatibility checks (cbmc commit: 1a28613).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84984878

majakusber self-assigned this Aug 22, 2018

majakusber requested review from cesaro, cristina-david, kroening, mgudemann, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners August 22, 2018 11:10

majakusber mentioned this pull request Aug 22, 2018

Complete typet documentation [DOC-12] #2771

Merged

tautschnig reviewed Aug 22, 2018

View reviewed changes

majakusber force-pushed the cleanup_typet branch 2 times, most recently from f1a227f to 6fee370 Compare August 22, 2018 14:40

majakusber force-pushed the cleanup_typet branch from 6fee370 to 5b701e2 Compare August 22, 2018 14:51

This was referenced Aug 22, 2018

Correct incomplete_array_typet [DOC-12] #2820

Merged

Deprecate nil_typet [DOC-12] #2821

Merged

majakusber force-pushed the cleanup_typet branch 2 times, most recently from 3a53602 to 3a29698 Compare August 22, 2018 15:07

majakusber force-pushed the cleanup_typet branch from 3a29698 to 08d7b44 Compare August 22, 2018 15:30

majakusber mentioned this pull request Aug 22, 2018

Add typet and symbol_typet documentation to util README [DOC-12] #2823

Merged

peterschrammel approved these changes Aug 22, 2018

View reviewed changes

peterschrammel added the cleanup label Aug 22, 2018

majakusber added the do not merge label Aug 23, 2018

majakusber force-pushed the cleanup_typet branch from 08d7b44 to 3ced6c7 Compare September 11, 2018 13:32

allredj reviewed Sep 11, 2018

View reviewed changes

svorenova added 4 commits September 17, 2018 10:08

Move functions from type to std_types

91dc220

Add missing can_casts and casts

a449f73

Use type_try_dynamic_cast instead of direct id check and cast

2c05b3a

Move mathematical types from std_types

1a28613

majakusber force-pushed the cleanup_typet branch from 3ced6c7 to 1a28613 Compare September 17, 2018 09:08

allredj reviewed Sep 17, 2018

View reviewed changes

romainbrenguier approved these changes Sep 17, 2018

View reviewed changes

majakusber merged commit 3e9b76d into diffblue:develop Sep 17, 2018

majakusber deleted the cleanup_typet branch September 17, 2018 13:22

Cleanup types [DOC-12] #2815

Cleanup types [DOC-12] #2815

Uh oh!

Conversation

majakusber commented Aug 22, 2018

Uh oh!

tautschnig commented Aug 22, 2018

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

majakusber commented Aug 22, 2018

Uh oh!

majakusber commented Aug 22, 2018

Uh oh!

tautschnig commented Aug 22, 2018

Uh oh!

majakusber commented Aug 22, 2018

Uh oh!

kroening commented Aug 23, 2018

Uh oh!

tautschnig commented Aug 23, 2018

Uh oh!

majakusber commented Aug 23, 2018

Uh oh!

majakusber commented Aug 23, 2018

Uh oh!

kroening commented Aug 24, 2018

Uh oh!

majakusber commented Sep 11, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!