Enum range check #4972

angelhof · 2019-08-01T14:25:52Z

Adds checks before every appearance of an enum type expression. These checks ensure that the value of the enum expression is one of the defined enum values. It doesn't insert checks for occurrences on the left hand side of assignments, as this introduces false positives (e.g when a variable is just declared but not initialized).

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.

angelhof · 2019-08-01T15:19:31Z

Why does only one build fail with error:

c_typecheck_type.cpp:1244:33: error: use of undeclared identifier 'as_string'
    auto value = string2integer(as_string(member.get_value()));
                                ^
1 error generated.

whereas all other builds succeed?

smowton · 2019-08-01T15:27:22Z

Most likely that's a build using typedef std::string irep_idt. Use id2string, which is always defined, rather than as_string, which is a dstring function only included when irep_idt == dstringt

angelhof · 2019-08-01T16:01:16Z

Most likely that's a build using typedef std::string irep_idt. Use id2string, which is always defined, rather than as_string, which is a dstring function only included when irep_idt == dstringt

@smowton Thanks, this seems to work :)

allredj

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

src/analyses/goto_check.cpp

src/ansi-c/c_typecheck_type.cpp

regression/goto-instrument/enum-range-check1/main.c

src/ansi-c/c_typecheck_type.cpp

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 66d7172).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121771820
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

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

codecov-io · 2019-08-02T15:26:19Z

Codecov Report

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

@@             Coverage Diff             @@
##           develop    #4972      +/-   ##
===========================================
+ Coverage    69.24%   69.25%   +<.01%     
===========================================
  Files         1309     1309              
  Lines       108453   108475      +22     
===========================================
+ Hits         75096    75119      +23     
+ Misses       33357    33356       -1

Impacted Files	Coverage Δ
.../goto-instrument/goto_instrument_parse_options.cpp	`56.26% <ø> (ø)`	⬆️
src/ansi-c/c_typecheck_base.h	`100% <ø> (ø)`	⬆️
src/ansi-c/c_typecheck_type.cpp	`76.12% <100%> (+0.12%)`	⬆️
src/analyses/goto_check.cpp	`79.5% <100%> (+0.54%)`	⬆️
src/ansi-c/expr2c.cpp	`67.2% <0%> (+0.07%)`	⬆️

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 cf7b9bf...9938747. Read the comment docs.

allredj

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

smowton

Couple of minor nitpicks, and you should squash the last two fixup commits into the "main" two wherever is appropriate, then LGTM

src/analyses/goto_check.cpp

This check can be enabled by using the flag --enum-range-check in goto-instrument. It inserts assertions before each use of any enum type expressions that the expression's value is one of the valid enum values. Note: It doesn't insert checks for occurrences of enum expressions on the left hand side of assignments.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 85b90f3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122303742
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.

tautschnig

Looks good, just needs a few extensions to make sure pragmas to disable the new check work fine.

src/goto-instrument/goto_instrument_parse_options.cpp

src/analyses/goto_check.cpp

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 933eb5e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122622217
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.

angelhof requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, owen-mc-diffblue, peterschrammel, smowton, tautschnig and thk123 as code owners August 1, 2019 14:25

allredj reviewed Aug 1, 2019

View reviewed changes

karkhaz reviewed Aug 1, 2019

View reviewed changes

src/analyses/goto_check.cpp Outdated Show resolved Hide resolved

smowton reviewed Aug 2, 2019

View reviewed changes

angelhof force-pushed the enum-range-check branch from ec750ef to 66d7172 Compare August 2, 2019 14:33

Fix the parsing of enums and enum constants

72aafbe

angelhof force-pushed the enum-range-check branch from 66d7172 to 9938747 Compare August 2, 2019 14:37

allredj reviewed Aug 2, 2019

View reviewed changes

allredj reviewed Aug 6, 2019

View reviewed changes

smowton approved these changes Aug 7, 2019

View reviewed changes

src/analyses/goto_check.cpp Outdated Show resolved Hide resolved

src/analyses/goto_check.cpp Outdated Show resolved Hide resolved

angelhof force-pushed the enum-range-check branch from a895b40 to 85b90f3 Compare August 7, 2019 14:20

allredj reviewed Aug 7, 2019

View reviewed changes

chrisr-diffblue assigned danpoe, chrisr-diffblue and hannes-steffenhagen-diffblue Aug 8, 2019

tautschnig requested changes Aug 8, 2019

View reviewed changes

src/goto-instrument/goto_instrument_parse_options.cpp Outdated Show resolved Hide resolved

src/analyses/goto_check.cpp Show resolved Hide resolved

Add a disable option for enum-range-check

933eb5e

allredj reviewed Aug 9, 2019

View reviewed changes

tautschnig approved these changes Aug 9, 2019

View reviewed changes

tautschnig merged commit 06ef36d into diffblue:develop Aug 9, 2019

Enum range check #4972

Enum range check #4972

Uh oh!

Conversation

angelhof commented Aug 1, 2019

Uh oh!

angelhof commented Aug 1, 2019

Uh oh!

smowton commented Aug 1, 2019

Uh oh!

angelhof commented Aug 1, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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!

codecov-io commented Aug 2, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov-io commented Aug 2, 2019 •

edited

Loading