Sizeof should fail on incomplete types #5211

xbauch · 2020-01-06T14:01:13Z

And so we check for it when type-checking the sizeof expression.

Note: previously, the size-of-expr function would return zero (sum of the struct components sizes).

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.
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).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

xbauch · 2020-01-06T14:12:06Z

May fix #5108.

allredj

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

codecov-io · 2020-01-06T15:12:53Z

Codecov Report

Merging #5211 into develop will increase coverage by <.01%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #5211      +/-   ##
===========================================
+ Coverage    67.37%   67.38%   +<.01%     
===========================================
  Files         1157     1157              
  Lines        95087    95092       +5     
===========================================
+ Hits         64068    64073       +5     
  Misses       31019    31019

Flag	Coverage Δ
#cproversmt2	`42.66% <100%> (ø)`	⬆️
#regression	`63.89% <100%> (ø)`	⬆️
#unit	`31.92% <20%> (-0.01%)`	⬇️

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_expr.cpp	`73.95% <100%> (+0.1%)`	⬆️

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 be84cd1...884c360. Read the comment docs.

chrisr-diffblue · 2020-01-07T10:09:44Z

src/ansi-c/c_typecheck_expr.cpp

+      to_struct_type(follow_tag(to_struct_tag_type(type))).is_incomplete())
+    {
+      error().source_location = expr.source_location();
+      error() << "calling sizeof for incomplete type: " << to_string(type)


Looks good in principal, I just have one suggestion, and one query:

I think you could pretty much copy the compiler error message from gcc for the error message here:

gcc cbmc-test.c cbmc-test.c:8:31: error: invalid application of 'sizeof' to an incomplete type 'struct foo' struct foo* thefoo = malloc(sizeof(struct foo));

This works for incomplete structs - but it won't catch other incomplete types? (e.g. unions, arrays with no dimensions, etc?)

I've change the message and extended the check to unions and enums. Arrays are weird: at the time of typechecking we already see variables of type int[] as if having type int.

Hmm, so does that mean you don't even know they are an array at that point? Also, what's the difference at that point between a variable of type int[] and a variable of type int[10] - does one have a length attribute somewhere? If you can know it's an array, and know it's length then it's a complete type. If you don't know it's length, then it's incomplete.

My bad: I was looking at a different sizeof. Now it should work for enums and arrays as well.

chrisr-diffblue

Looks good, many thanks :-)

kroening · 2020-01-07T15:59:16Z

src/ansi-c/c_typecheck_expr.cpp

@@ -951,6 +951,21 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
  }
  else
  {
+    if(
+      (type.id() == ID_struct_tag &&
+       to_struct_type(follow_tag(to_struct_tag_type(type))).is_incomplete()) ||


No need for the to_struct_type etc.

kroening · 2020-01-07T16:00:10Z

I'd stick the tests into one directory, say "incomplete-sizeof".

allredj

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

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 5564772).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/143445520
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

allredj

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

And so we check for it when type-checking the `sizeof` expression. Extends to incomplete enums, structs, unions, and arrays (zero-length). Note: previously, the `size-of-expr` function would return zero (sum of the struct components sizes).

hannes-steffenhagen-diffblue

LGTM

allredj

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

allredj reviewed Jan 6, 2020

View reviewed changes

chrisr-diffblue reviewed Jan 7, 2020

View reviewed changes

xbauch force-pushed the fix/incomplete-sizeof branch from 6684042 to a41a250 Compare January 7, 2020 15:26

chrisr-diffblue approved these changes Jan 7, 2020

View reviewed changes

kroening reviewed Jan 7, 2020

View reviewed changes

xbauch force-pushed the fix/incomplete-sizeof branch from 5564772 to 81499c5 Compare January 7, 2020 16:31

allredj reviewed Jan 7, 2020

View reviewed changes

Sizeof should fail on incomplete types

59c6d8f

And so we check for it when type-checking the `sizeof` expression. Extends to incomplete enums, structs, unions, and arrays (zero-length). Note: previously, the `size-of-expr` function would return zero (sum of the struct components sizes).

xbauch force-pushed the fix/incomplete-sizeof branch from 81499c5 to 59c6d8f Compare January 8, 2020 10:11

xbauch marked this pull request as ready for review January 8, 2020 10:12

xbauch requested a review from tautschnig as a code owner January 8, 2020 10:12

hannes-steffenhagen-diffblue approved these changes Jan 8, 2020

View reviewed changes

allredj reviewed Jan 8, 2020

View reviewed changes

chrisr-diffblue assigned kroening and tautschnig Jan 14, 2020

kroening approved these changes Jan 16, 2020

View reviewed changes

kroening merged commit 077b5ee into diffblue:develop Jan 16, 2020

xbauch mentioned this pull request Feb 7, 2020

sizeof shouldn't work for forward declared structs #5108

Closed

Sizeof should fail on incomplete types #5211

Sizeof should fail on incomplete types #5211

Uh oh!

Conversation

xbauch commented Jan 6, 2020

Uh oh!

xbauch commented Jan 6, 2020

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Jan 6, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

chrisr-diffblue Jan 7, 2020

Choose a reason for hiding this comment

Uh oh!

xbauch Jan 7, 2020

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue Jan 7, 2020

Choose a reason for hiding this comment

Uh oh!

xbauch Jan 7, 2020

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

kroening Jan 7, 2020

Choose a reason for hiding this comment

Uh oh!

xbauch Jan 8, 2020

Choose a reason for hiding this comment

Uh oh!

kroening commented Jan 7, 2020

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!

hannes-steffenhagen-diffblue 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!

codecov-io commented Jan 6, 2020 •

edited

Loading