Improves support for assigns clauses #5538

feliperodri · 2020-10-27T04:46:07Z

Assigns clauses are now able to handle structs and arrays.

Signed-off-by: Felipe R. Monteiro [email protected]

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.

codecov · 2020-10-27T05:36:36Z

Codecov Report

Merging #5538 (85dd63b) into develop (867168c) will increase coverage by 0.77%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #5538      +/-   ##
===========================================
+ Coverage    74.24%   75.01%   +0.77%     
===========================================
  Files         1431     1431              
  Lines       155290   155609     +319     
===========================================
+ Hits        115290   116732    +1442     
+ Misses       40000    38877    -1123

Impacted Files	Coverage Δ
src/goto-instrument/code_contracts.cpp	`83.53% <0.00%> (-8.55%)`	⬇️
src/goto-instrument/code_contracts.h	`94.11% <0.00%> (-5.89%)`	⬇️
src/ansi-c/ansi_c_declaration.h	`95.06% <0.00%> (-2.72%)`	⬇️
src/goto-instrument/accelerate/scratch_program.cpp	`65.95% <0.00%> (-1.46%)`	⬇️
src/ansi-c/c_typecheck_base.cpp	`78.23% <0.00%> (-0.87%)`	⬇️
src/ansi-c/expr2c.cpp	`68.62% <0.00%> (-0.15%)`	⬇️
src/ansi-c/c_typecheck_expr.cpp	`75.29% <0.00%> (-0.15%)`	⬇️
src/ansi-c/parser.y	`77.72% <0.00%> (-0.05%)`	⬇️
src/ansi-c/c_typecheck_base.h	`100.00% <0.00%> (ø)`
src/ansi-c/ansi_c_convert_type.h	`100.00% <0.00%> (ø)`
... and 30 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 8cfcfdb...85dd63b. Read the comment docs.

martin-cs · 2020-10-27T11:15:31Z

@NlightNFotis The code coverage is still showing the same spurious decrease as other PRs. I think one of the changes to the build scripts has broken it. Please can you have a look?

martin-cs · 2020-10-27T11:43:32Z

@feliperodri Thank you for this work. Would it be possible to break it into a number of smaller commits to make it easier to review? As I understand it, this includes:

A few changes to general supporting code
A change to the parser to make assigns clauses attributes (I think)
The corresponding updates to the regression tests plus some general cleaning and improvements
Handling of structs and arrays in the assigns clauses
Documentation updates

If these could be split up a bit, that would be great.

thomasspriggs · 2020-10-27T15:00:05Z

This is not a full review. Just some initial observations. My apologies if I have jumped the gun by looking whilst it is still in draft status -

CI is failing with (core dumped) errors. These will need to be fixed.
A single large commit for an entire PR of this size is going to make it more difficult to review. It would be particularly useful if you could separate changes which are entirely stylistic, from those which make functional changes. That way reviewers can pay particular attention to the functional changes and the stylistic changes can be assessed on their own merit.
Your changes include renaming existing variables to abbreviated forms. Our coding standards explicitly states that we should "Avoid abbreviations" for naming - https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md. Therefore such renaming should be removed from this PR, as it is against our standards and it has an adverse impact on readability. An additional issue with variable renaming, even where it is desirable, is that increases the size of the diff. This has the potential to cause additional merge resolution work, either for other people whose PRs are merged after yours, or for yourself if other people merge changes to the same areas before you. For this reason any renaming which you want to keep should be in a separate commit, which only includes the renaming and includes a commit message body justifying the renaming.
irep_idt / dstringt includes an overload of operator==. This should be used in preference to converting both sides to C strings and using std::strcmp. Using the operator directly should be cleaner to read and more performant.
I think I spotted const being removed from some of the declarations. I am not sure if you have added additional mutation, without looking more closely. But const should not be removed without good reason.

Good luck with finding the cause of the failing tests.

feliperodri · 2021-02-25T06:58:04Z

@martin-cs @thomasspriggs I resolved all regression test issues and split up into a few commits, could you review it? Also, @thomasspriggs I revised the code for name abbreviations, misused of std::strcmp, and const removals.

tautschnig

Comments for most of the commits (with some blockers). I am yet to properly review the largest of the commits, "Adds arrays and structs support for assigns clauses" - will do so after a first range of fixes has been applied.

regression/contracts/assigns_enforce_01/main.c

regression/contracts/assigns_enforce_02/main.c

regression/contracts/assigns_enforce_arrays_01/test.desc

regression/contracts/assigns_enforce_arrays_02/test.desc

regression/contracts/assigns_enforce_arrays_12/test.desc

src/goto-instrument/code_contracts.cpp

martin-cs · 2021-02-25T22:21:28Z

@feliperodri thanks for this and for separating the changes as requested. I am happy to take another look but maybe it's best if I wait until you've had a chance to look at / action @tautschnig 's changes.

feliperodri · 2021-03-05T19:59:26Z

Comments for most of the commits (with some blockers). I am yet to properly review the largest of the commits, "Adds arrays and structs support for assigns clauses" - will do so after a first range of fixes has been applied.

@tautschnig thank you for all insightful comments. Could you take another review round?

feliperodri · 2021-03-05T20:00:34Z

@feliperodri thanks for this and for separating the changes as requested. I am happy to take another look but maybe it's best if I wait until you've had a chance to look at / action @tautschnig 's changes.

@martin-cs I agree. As soon as @tautschnig finish reviewing all changes, I can ping you for a final round.

feliperodri · 2021-03-17T17:42:32Z

The changes to the grammar are indeed very scary, and should likely be pulled out of this PR.

The right place to do this appears to be postfixing_abstract_declarator; I'll try.

@tautschnig @kroening I completely removed the changes in this PR related to updating the grammar to support contracts on function declarations. I'll take a look at Daniel's proposal.

tautschnig

I have not read all of the changes to code_contracts.cpp, but have provided some suggestions for improvement. Most likely that bit of code needs a complete overhaul anyway. All other parts are ok except for nit picks.

src/ansi-c/parser.y

src/goto-instrument/code_contracts.cpp

feliperodri · 2021-03-17T23:08:47Z

@martin-cs and @thomasspriggs can I get one more review on this PR?

NlightNFotis

Reasonable so far.

I only have some questions and some minor requests.

src/ansi-c/scanner.l

src/goto-instrument/code_contracts.cpp

doc/cprover-manual/assigns-clause.md

NlightNFotis · 2021-03-17T23:57:45Z

regression/contracts/assigns_enforce_arrays_06/main.c

@@ -0,0 +1,12 @@
+void assign_out_under(int a[], int len) __CPROVER_assigns(a[8])
+{
+  a[7] = 5;


Is this effectively the same test as assigns_enforce_arrays_05 or do I think so?

It's quite similar. In this case we cant to see if we report failure correctly when the specification doesn't have a range, but a single cell (i.e., a[8] instead of a[2, 5]).

regression/contracts/assigns_enforce_arrays_06/test.desc

regression/contracts/assigns_enforce_arrays_08/test.desc

NlightNFotis · 2021-03-18T00:02:08Z

regression/contracts/assigns_enforce_arrays_12/test.desc

+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when a function with an array assigns target


Is there any warning printed for this case?

If yes, does it make sense to pattern match for it?

We currently do not have any warnings related to this issue. Should I create a GitHub issue to add this in future PRs?

NlightNFotis

Sorry, some small comments and otherwise it's good to go for me.

src/ansi-c/parser.y

src/goto-instrument/code_contracts.cpp

feliperodri · 2021-03-19T03:28:10Z

@NlightNFotis could you take another look?

NlightNFotis

Looks good to me, thanks for the implementation of the comment suggestions.

hannes-steffenhagen-diffblue

Unless I'm mistaken the changes here lead to a conflict in the parser w.r.t. to the comma operator. If I'm mistaken please explain.

src/util/std_expr.h

hannes-steffenhagen-diffblue · 2021-03-19T10:40:04Z

src/ansi-c/parser.y

+        | integer
+        ;
+
+array_range:


Not a blocker, but a comment from me: I'm quite worried about the proliferation of nonstandard extensions. We're getting into a situation where we have to support gcc extensions, clang extensions, visual studio extensions on top of our own modifications to the language...

This could've been done without any parser changes at the relatively small cost of a less cute syntax, e.g. __CPROVER_array_range(array, lower, upper) or something like that. Looks bad, but less problematic syntactically.

For now, I'll keep using this annotation, but that's a valid concern. Thus, I created the issue #5966 to discuss whether we should continue to use this annotation for array ranges or only adopt annotations that do not require changes to the parser.

Based on the discussion on #5966 I reverted all the parser changes (to support array ranges) from this PR. We should have a syntax similar to ACSL, but that should be added on a separate PR. I kept the code on the assigns clause size for this future support.

src/ansi-c/parser.y

hannes-steffenhagen-diffblue

Removing my block because the specific issue I was complaining about was addressed. Larger point about syntax extensions remains, but doesn't need to be addressed at this very moment.

Assigns clauses should handle multiple targets. Previously, it only supported identifiers (e.g., variable `x`) and dereferenced pointers (e.g., *myPtr). So, we expand its support to also handle members of a struct (e.g. `myStruct.someMember` or `myStructPtr->otherMember`) and array ranges (e.g. `myArr[5, lastIdx]`). Signed-off-by: Felipe R. Monteiro <[email protected]>

Signed-off-by: Felipe R. Monteiro <[email protected]>

Code contracts now supports assigns clause with structs and array ranges. It also supports contracts specified across multiple source files. So, we added regression tests to cover these capabilites. Signed-off-by: Felipe R. Monteiro <[email protected]>

Signed-off-by: Felipe R. Monteiro <[email protected]>

feliperodri added the aws Bugs or features of importance to AWS CBMC users label Oct 27, 2020

feliperodri force-pushed the support-assigns-clause branch from 0e6ca07 to d61dd49 Compare October 27, 2020 04:58

feliperodri force-pushed the support-assigns-clause branch 2 times, most recently from 9b56c97 to f64eba0 Compare October 29, 2020 22:27

feliperodri force-pushed the support-assigns-clause branch 3 times, most recently from af4fd3a to a7b3dab Compare February 23, 2021 15:38

feliperodri self-assigned this Feb 23, 2021

feliperodri added the Code Contracts Function and loop contracts label Feb 23, 2021

feliperodri force-pushed the support-assigns-clause branch 2 times, most recently from 4310b55 to a7a7f72 Compare February 25, 2021 06:54

feliperodri marked this pull request as ready for review February 25, 2021 06:55

feliperodri requested review from chrisr-diffblue, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, smowton and tautschnig as code owners February 25, 2021 06:55

tautschnig requested changes Feb 25, 2021

View reviewed changes

feliperodri force-pushed the support-assigns-clause branch from a7a7f72 to f504152 Compare March 5, 2021 19:57

feliperodri requested a review from tautschnig March 5, 2021 19:57

tautschnig approved these changes Mar 17, 2021

View reviewed changes

feliperodri force-pushed the support-assigns-clause branch from 9cef787 to 3e529c0 Compare March 17, 2021 23:00

feliperodri force-pushed the support-assigns-clause branch from 3e529c0 to bf636db Compare March 17, 2021 23:10

NlightNFotis reviewed Mar 18, 2021

View reviewed changes

feliperodri force-pushed the support-assigns-clause branch from bf636db to 6eaed34 Compare March 18, 2021 18:20

feliperodri requested a review from NlightNFotis March 18, 2021 18:20

NlightNFotis reviewed Mar 18, 2021

View reviewed changes

feliperodri force-pushed the support-assigns-clause branch 2 times, most recently from a29f208 to 3102111 Compare March 19, 2021 03:27

feliperodri requested a review from NlightNFotis March 19, 2021 03:27

NlightNFotis approved these changes Mar 19, 2021

View reviewed changes

hannes-steffenhagen-diffblue suggested changes Mar 19, 2021

View reviewed changes

ArenBabikian mentioned this pull request Mar 19, 2021

Supports quantifiers in function contracts #5959

Merged

7 tasks

feliperodri mentioned this pull request Mar 22, 2021

What is the proper annotation for ranges in function contracts #5966

Closed

feliperodri force-pushed the support-assigns-clause branch from 3102111 to 27cfe08 Compare March 22, 2021 21:43

feliperodri requested a review from hannes-steffenhagen-diffblue March 22, 2021 21:44

hannes-steffenhagen-diffblue approved these changes Mar 23, 2021

View reviewed changes

feliperodri force-pushed the support-assigns-clause branch from 27cfe08 to 61110ac Compare March 24, 2021 02:07

feliperodri added 4 commits March 23, 2021 22:17

Updates assigns clause description in CPROVER manual

58403c2

Signed-off-by: Felipe R. Monteiro <[email protected]>

Updates list of expected Doxygen warnings

85dd63b

Signed-off-by: Felipe R. Monteiro <[email protected]>

feliperodri force-pushed the support-assigns-clause branch from 61110ac to 85dd63b Compare March 24, 2021 02:17

feliperodri merged commit ca65cf9 into diffblue:develop Mar 24, 2021

feliperodri deleted the support-assigns-clause branch March 24, 2021 03:43

This was referenced Mar 24, 2021

Adds support for range annotation in assigns clauses #5972

Closed

Simply create_alias_expression in code_contracts.cpp #5528

Closed

Improves support for assigns clauses #5538

Improves support for assigns clauses #5538

Uh oh!

Conversation

feliperodri commented Oct 27, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

martin-cs commented Oct 27, 2020

Uh oh!

martin-cs commented Oct 27, 2020

Uh oh!

thomasspriggs commented Oct 27, 2020

Uh oh!

feliperodri commented Feb 25, 2021

Uh oh!

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

Uh oh!

martin-cs commented Feb 25, 2021

Uh oh!

feliperodri commented Mar 5, 2021

Uh oh!

feliperodri commented Mar 5, 2021

Uh oh!

feliperodri commented Mar 17, 2021

Uh oh!

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

Uh oh!

feliperodri commented Mar 17, 2021

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

NlightNFotis Mar 17, 2021

Choose a reason for hiding this comment

Uh oh!

feliperodri Mar 18, 2021

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

NlightNFotis Mar 18, 2021

Choose a reason for hiding this comment

Uh oh!

feliperodri Mar 18, 2021

Choose a reason for hiding this comment

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

feliperodri commented Oct 27, 2020 •

edited

Loading

codecov bot commented Oct 27, 2020 •

edited

Loading