Cleanup of throws and asserts of goto_convert.cpp by NlightNFotis · Pull Request #2905 · diffblue/cbmc

NlightNFotis · 2018-09-05T15:30:43Z

In the same spirit as #2904 I am taking over development of #2814 because the original repository is now defunct, and I can't go further with that PR. This PR will host further development of that line of work.

Each commit message has a non-empty body, explaining why the change was made.
My contribution is formatted in line with CODING_STANDARD.md.
[n/a] Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
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.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig

At the current state: please see #2814 for a number of blocking request.

allredj

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

Remove duplicate invariants, and change some to transfer (cast) function calls, which provide guarantees about the data types by construction. Also substitute invariants with exceptions where appropriate.

NlightNFotis · 2018-09-27T11:32:47Z

@tautschnig This should be now in a state where it's ready for a review. Just a note:

I have tried my best to make the commits as close as possible to the contribution guidelines. It's a little bit hairy, because 3 people have worked on this thus far, and one of them is no longer with us, but we have to be careful not to lose commit information and attribution information, hence why the commits are the way they are and I can not squash them better.

regression/ansi-c/goto_convert/switch_range_bounds/test.desc

tautschnig · 2018-09-27T11:39:03Z

regression/ansi-c/goto_convert/invalid_goto_label/test.desc

@@ -0,0 +1,8 @@
+CORE gcc-only


Why is this gcc-only?

You're right, this is a mistake, both clang and gcc report the same error.

tautschnig · 2018-09-27T11:39:43Z

regression/ansi-c/goto_convert/switch_range_empty/test.desc

+CORE
+main.c
+
+^EXIT=134$


Huh? That's not what should be happening...

What should be happening? I see that gcc and clang produce warnings that the range is empty, but are happy to compile nonetheless. Should I remove the invariant?

We should be able to support whatever GCC and Clang do. 134 (a failing invariant) is not an exit code we should ever be producing for a syntactically valid C program.

src/goto-programs/goto_convert.cpp

tautschnig · 2018-09-27T11:42:15Z

src/goto-programs/goto_convert.cpp

-
-    throw 0;
-  }
+  bool res = get_string_constant(expr, result);


allredj

Passed Diffblue compatibility checks (cbmc commit: 9a6e16f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86143603

NlightNFotis · 2018-09-27T15:48:29Z

@tautschnig I decided on an alternative approach to the bugged test (the one we had a divergent behaviour from gcc and clang).

Before the refactoring work, that turned a line in goto_convertt::convert_switch in line 1252 from an assert to a DATA_INVARIANT. It seems that both of these behaviours are wrong to begin with, and I consider this a bug. For this reason I added a KNOWNBUG test, that I will mark as CORE in another PR, that I will submit on top of this PR fixing this, and in which I will only have the removal of the assertion and the activation of the test. So consider this one at a reviewable state.

Refactor a function in goto_convertt so that it becomes more comprehensible.

Change some data_invariants to invariants_with_diagnostics where they are more appropriate, and remove some duplicate invariants, where they are guaranteed by construction of the types themselves.

NlightNFotis · 2018-09-27T15:58:47Z

I pushed #3055 that fixes this the issue suggested above. That PR also for now contains the changes introduced here, but once this one is merged, I will rebase that one appropriately to only mirror the change it introduces.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 5e7e55a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86177330
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: 5523818).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86177840

NlightNFotis added the do not merge label Sep 5, 2018

NlightNFotis self-assigned this Sep 5, 2018

NlightNFotis requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners September 5, 2018 15:30

NlightNFotis mentioned this pull request Sep 5, 2018

Convert throws and asserts to INVARIANTs for goto_convert.cpp #2814

Closed

tautschnig requested changes Sep 5, 2018

View reviewed changes

NlightNFotis force-pushed the 2814_takeover branch 2 times, most recently from eb1c4b9 to 7d0ba9f Compare September 25, 2018 15:24

NlightNFotis requested a review from martin-cs as a code owner September 25, 2018 15:24

NlightNFotis force-pushed the 2814_takeover branch from 7d0ba9f to a6c1699 Compare September 25, 2018 15:26

Convert throws and asserts to INVARIANTs for goto_convert.cpp

ccce5d7

NlightNFotis force-pushed the 2814_takeover branch from a6c1699 to 3e57a9c Compare September 25, 2018 15:54

allredj reviewed Sep 25, 2018

View reviewed changes

NlightNFotis added the work in progress label Sep 26, 2018

Substitute duplicate invariants with transfer function calls

40b2355

Remove duplicate invariants, and change some to transfer (cast) function calls, which provide guarantees about the data types by construction. Also substitute invariants with exceptions where appropriate.

NlightNFotis force-pushed the 2814_takeover branch from 3e57a9c to 9a6e16f Compare September 27, 2018 11:25

NlightNFotis removed do not merge work in progress labels Sep 27, 2018

tautschnig reviewed Sep 27, 2018

View reviewed changes

allredj reviewed Sep 27, 2018

View reviewed changes

NlightNFotis force-pushed the 2814_takeover branch from 9a6e16f to 5e7e55a Compare September 27, 2018 15:42

NlightNFotis and others added 3 commits September 27, 2018 16:50

Provide tests for goto_convert

e0dca08

Refactor goto_convertt::case_guard

e67b6d0

Refactor a function in goto_convertt so that it becomes more comprehensible.

Change data_invariants to invariants_with_diagnostics

5523818

Change some data_invariants to invariants_with_diagnostics where they are more appropriate, and remove some duplicate invariants, where they are guaranteed by construction of the types themselves.

NlightNFotis force-pushed the 2814_takeover branch from 5e7e55a to 5523818 Compare September 27, 2018 15:50

NlightNFotis mentioned this pull request Sep 27, 2018

Fix handling of case range statement in special case #3055

Merged

4 tasks

allredj reviewed Sep 27, 2018

View reviewed changes

tautschnig approved these changes Sep 27, 2018

View reviewed changes

tautschnig merged commit 0914275 into diffblue:develop Sep 27, 2018

NlightNFotis deleted the 2814_takeover branch February 19, 2021 10:48

Conversation

NlightNFotis commented Sep 5, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig 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!

NlightNFotis commented Sep 27, 2018

Uh oh!

Uh oh!

tautschnig Sep 27, 2018

Choose a reason for hiding this comment

Uh oh!

NlightNFotis Sep 27, 2018

Choose a reason for hiding this comment

Uh oh!

tautschnig Sep 27, 2018

Choose a reason for hiding this comment

Uh oh!

NlightNFotis Sep 27, 2018

Choose a reason for hiding this comment

Uh oh!

tautschnig Sep 27, 2018

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig Sep 27, 2018

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

NlightNFotis commented Sep 27, 2018

Uh oh!

NlightNFotis commented Sep 27, 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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

NlightNFotis commented Sep 5, 2018 •

edited

Loading