Correctly interpret underlying type specification of enums #5441

danpoe · 2020-08-03T09:37:31Z

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.
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.

chrisr-diffblue · 2020-08-04T08:39:57Z

src/ansi-c/c_typecheck_type.cpp

+    {
+      error().source_location = source_location;
+      error() << "underlying type for enum must be an integral type" << eom;
+      throw 0;


Do we not have a structured exception to throw here? (and in the other cases below)

Yes this should an invalid_source_file_exceptiont

chrisr-diffblue

Looks good, and thanks for the comprehensive test cases. A couple of minor nitpicks really:

Error handling - we put quite a big effort into cleaning up error handling, adding structured exceptions, things like that - so it would be good to avoid the throw 0 if possible.
What error messages does clang emit for the "non-integral underlying type" and "underlying type too narrow for constant" cases? It would be good to make our error messages broadly similar just for ease of users googling for help if they hit them, etc.

hannes-steffenhagen-diffblue · 2020-08-03T13:56:52Z

src/ansi-c/c_typecheck_type.cpp

  {
-    warning().source_location = source_location;
-    warning() << "ignoring specification of underlying type for enum" << eom;
+    typecheck_type(type.add_type(ID_enum_underlying_type));


Using add_something to refer to something that's already there is pretty oof.

hannes-steffenhagen-diffblue · 2020-08-03T13:59:03Z

regression/cbmc/enum_underlying_type_02/main.c

+
+enum enum1 : unsigned char
+{
+  E1 = 256


Good test case to include!

hannes-steffenhagen-diffblue · 2020-08-04T08:51:46Z

@chrisr-diffblue Current errors for these cases in clang look like this:

test.c:1:10: error: non-integral type 'float' is an invalid underlying type

and

test.c:1:24: error: enumerator value is not representable in the underlying type 'signed char'

I think the existing error messages we have here are sufficiently close to that. We could include some extra information like what we think the underlying type is and why it doesn't fit and such, but I wouldn't call this a blocker.

hannes-steffenhagen-diffblue · 2020-08-04T08:54:31Z

I'm OK with these changes though I'd also prefer if we didn't proliferate the throw 0 thing.

chrisr-diffblue · 2020-08-04T09:16:16Z

@chrisr-diffblue Current errors for these cases in clang look like this:
test.c:1:10: error: non-integral type 'float' is an invalid underlying type
and
test.c:1:24: error: enumerator value is not representable in the underlying type 'signed char'
I think the existing error messages we have here are sufficiently close to that. We could include some extra information like what we think the underlying type is and why it doesn't fit and such, but I wouldn't call this a blocker.

Thanks @hannes-steffenhagen-diffblue - @danpoe If it's not too much of a pain, could you model the error messages on the above? In particular, showing the user the type like that its quite helpful to them.

codecov · 2020-08-04T09:42:09Z

Codecov Report

Merging #5441 into develop will decrease coverage by 0.83%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #5441      +/-   ##
===========================================
- Coverage    68.21%   67.38%   -0.84%     
===========================================
  Files         1178     1178              
  Lines        97561    97580      +19     
===========================================
- Hits         66554    65750     -804     
- Misses       31007    31830     +823

Flag	Coverage Δ
#cproversmt2	`?`
#regression	`65.39% <100.00%> (+<0.01%)`	⬆️
#unit	`32.26% <25.00%> (-0.01%)`	⬇️

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

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_type.cpp	`77.08% <100.00%> (+0.56%)`	⬆️
src/ansi-c/parser.y	`78.05% <100.00%> (+0.02%)`	⬆️
src/solvers/smt2/smt2irep.cpp	`32.00% <0.00%> (-56.00%)`	⬇️
src/solvers/smt2/smt2_conv.cpp	`31.46% <0.00%> (-26.23%)`	⬇️
src/solvers/floatbv/float_bv.cpp	`55.25% <0.00%> (-18.88%)`	⬇️
src/solvers/smt2/smt2_dec.cpp	`61.53% <0.00%> (-16.93%)`	⬇️
src/solvers/smt2/smt2_tokenizer.cpp	`69.02% <0.00%> (-16.82%)`	⬇️
src/solvers/smt2/smt2_parser.cpp	`58.91% <0.00%> (-8.07%)`	⬇️
src/solvers/flattening/pointer_logic.cpp	`81.81% <0.00%> (-7.58%)`	⬇️
src/util/expr_util.cpp	`80.50% <0.00%> (-4.24%)`	⬇️
... and 13 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 eefd06f...5f3519a. Read the comment docs.

… feature

danpoe · 2020-08-05T07:52:40Z

@chrisr-diffblue Current errors for these cases in clang look like this:
test.c:1:10: error: non-integral type 'float' is an invalid underlying type
and
test.c:1:24: error: enumerator value is not representable in the underlying type 'signed char'
I think the existing error messages we have here are sufficiently close to that. We could include some extra information like what we think the underlying type is and why it doesn't fit and such, but I wouldn't call this a blocker.
Thanks @hannes-steffenhagen-diffblue - @danpoe If it's not too much of a pain, could you model the error messages on the above? In particular, showing the user the type like that its quite helpful to them.

Ok, changed the error messages to a text similar to the clang messages and including the type.

chrisr-diffblue

Thanks for addressing my nitpicks :-)

danpoe requested review from chrisr-diffblue, kroening and tautschnig as code owners August 3, 2020 09:37

danpoe changed the title ~~Correctly interpret underlying type specification of enums~~ Correctly interpret underlying type specification of enums [depends-on: #5438] Aug 3, 2020

Update grammar to provide parsed types

4ded255

danpoe force-pushed the fixes/enum-underlying-types branch from b862db3 to a64235e Compare August 3, 2020 15:47

danpoe changed the title ~~Correctly interpret underlying type specification of enums [depends-on: #5438]~~ Correctly interpret underlying type specification of enums Aug 3, 2020

danpoe force-pushed the fixes/enum-underlying-types branch from a64235e to 775a449 Compare August 4, 2020 08:33

chrisr-diffblue reviewed Aug 4, 2020

View reviewed changes

hannes-steffenhagen-diffblue reviewed Aug 4, 2020

View reviewed changes

hannes-steffenhagen-diffblue approved these changes Aug 4, 2020

View reviewed changes

danpoe force-pushed the fixes/enum-underlying-types branch from 775a449 to 875bf69 Compare August 4, 2020 09:14

danpoe added 3 commits August 4, 2020 19:46

Add regression tests for enum underlying type specification feature

d0cd064

Set enum underlying type from specified type

16b48f0

Adapt existing enum regression test for underlying type specification…

5f3519a

… feature

danpoe force-pushed the fixes/enum-underlying-types branch from 875bf69 to 5f3519a Compare August 4, 2020 18:48

chrisr-diffblue approved these changes Aug 5, 2020

View reviewed changes

danpoe merged commit b3a6cc4 into diffblue:develop Aug 5, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Correctly interpret underlying type specification of enums #5441

Correctly interpret underlying type specification of enums #5441

Uh oh!

danpoe commented Aug 3, 2020 •

edited

Loading

Uh oh!

chrisr-diffblue Aug 4, 2020

Uh oh!

hannes-steffenhagen-diffblue Aug 4, 2020

Uh oh!

danpoe Aug 5, 2020

Uh oh!

chrisr-diffblue left a comment

Uh oh!

hannes-steffenhagen-diffblue Aug 3, 2020

Uh oh!

hannes-steffenhagen-diffblue Aug 3, 2020

Uh oh!

hannes-steffenhagen-diffblue commented Aug 4, 2020 •

edited

Loading

Uh oh!

hannes-steffenhagen-diffblue commented Aug 4, 2020

Uh oh!

chrisr-diffblue commented Aug 4, 2020

Uh oh!

codecov bot commented Aug 4, 2020 •

edited

Loading

Uh oh!

danpoe commented Aug 5, 2020

Uh oh!

chrisr-diffblue left a comment

Uh oh!

Uh oh!

Correctly interpret underlying type specification of enums #5441

Correctly interpret underlying type specification of enums #5441

Uh oh!

Conversation

danpoe commented Aug 3, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chrisr-diffblue Aug 4, 2020

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Aug 4, 2020

Choose a reason for hiding this comment

Uh oh!

danpoe Aug 5, 2020

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Aug 3, 2020

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Aug 3, 2020

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Aug 4, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue commented Aug 4, 2020

Uh oh!

chrisr-diffblue commented Aug 4, 2020

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

danpoe commented Aug 5, 2020

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

danpoe commented Aug 3, 2020 •

edited

Loading

hannes-steffenhagen-diffblue commented Aug 4, 2020 •

edited

Loading

codecov bot commented Aug 4, 2020 •

edited

Loading