Parser support for assigns contracts on loops #6196

aalok-thakkar · 2021-06-23T18:47:02Z

Created cprover_loop_contract that has cprover_contract_assigns_opt and loop_invariant_opt.

This adds support for parsing assigns clauses for loops.

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 · 2021-06-23T21:42:12Z

Codecov Report

Merging #6196 (e190b7f) into develop (141f3ce) will increase coverage by 0.16%.
The diff coverage is 86.66%.

@@             Coverage Diff             @@
##           develop    #6196      +/-   ##
===========================================
+ Coverage    75.30%   75.47%   +0.16%     
===========================================
  Files         1458     1458              
  Lines       161436   161437       +1     
===========================================
+ Hits        121575   121838     +263     
+ Misses       39861    39599     -262

Impacted Files	Coverage Δ
src/ansi-c/parser.y	`79.24% <86.66%> (+16.85%)`	⬆️
src/util/simplify_expr.cpp	`78.53% <0.00%> (+0.07%)`	⬆️
src/ansi-c/c_typecheck_expr.cpp	`61.56% <0.00%> (+0.33%)`	⬆️
src/ansi-c/parser_static.inc	`96.58% <0.00%> (+2.56%)`	⬆️
src/util/floatbv_expr.h	`73.58% <0.00%> (+2.83%)`	⬆️

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 665abf7...e190b7f. Read the comment docs.

SaswatPadhi

Please rebase against current develop and resolve the merge conflict -- it's due to the decreases contract that Long's PR introduced. That should be added to cprover_loop_contract and should be removed from individual iteration statements.

src/ansi-c/parser.y

feliperodri

LGTM.

SaswatPadhi · 2021-06-26T04:29:25Z

Marking this as draft. There are several issues with commits, including merge conflicts.
@aalok-thakkar please fix these.

martin-cs

Please rebase as there seems to be at least one unrelated commit in this PR.

SaswatPadhi

LGTM, but one minor issue.

src/ansi-c/parser.y

martin-cs

The patch looks OK but I really don't think we should be adding syntax extensions without test cases that at least demonstrate how to use them.

regression/contracts/invar_loop_constant_pass/test.desc

regression/contracts/invar_dynamic_struct_member/main.c

regression/contracts/invar_check_multiple_loops/main.c

regression/contracts/invar_assigns_opt/test.desc

regression/contracts/invar_assigns_opt/main.c

regression/contracts/invar_assigns_alias_analysis/test.desc

feliperodri · 2021-07-08T21:07:19Z

regression/contracts/invar_assigns_alias_analysis/test.desc

+This test shows that the current implementation only supports
+parsing and still uses alias analysis. Fixing this is a part 


What do you mean by "current implementation only supports parsing and still uses alias analysis"? Could you elaborate?

This PR only adds parsing to it, and assertion statements are yet not generated. Therefore, this proof does not go through.

What Aalok is saying is that, he added this test just to check the parsing support (and address Martin's comment regarding usage of assigns clause). But it's not considered during instrumentation, so this test which he obtained from my bug report, still fails as before.

regression/contracts/invar_assigns_empty/test.desc

regression/contracts/invar_check_multiple_loops/main.c

regression/contracts/invar_dynamic_struct_member/main.c

regression/contracts/invar_loop_constant_pass/test.desc

feliperodri

LGTM.

1. Renamed cprover_contract_assigns_opt to cprover_contract_assigns. 2. Created cprover_contract_assigns_opt which has a unit production and cprover_contract_assigns. 3. Renamed cprover_decreases_opt to cprover_contract_decreases_opt. 4. Renamed loop_invariant to cprover_contract_loop_invariant. 5. Renamed loop_invariant_list to cprover_contract_loop_invariant_list. 6. Renamed loop_invariant_list_opt to cprover_contract_loop_invariant_list_opt. 7. Added cprover_contract_assigns_opt to iteration statement. 8. Created the regression test invar_assigns_alias_analysis (KNOWNBUG). 9. Created the regression test invar_assigns_opt (CORE). 10. Created the regression test invar_assigns_empty (CORE). This adds parser support for assigns contracts on loops.

feliperodri · 2021-07-12T14:35:43Z

@martin-cs could you give another review on this PR?

martin-cs

Sure @feliperodri . There are now tests so no longer blocking.

regression/contracts/invar_assigns_alias_analysis/test.desc

In this commit we implement the parsing actions, type checking and conversion routines for assigns clauses on loops. The syntax rules along with regressions tests were introduced in an earlier PR: diffblue#6196.

aalok-thakkar requested review from chrisr-diffblue, kroening and tautschnig as code owners June 23, 2021 18:47

SaswatPadhi assigned aalok-thakkar Jun 23, 2021

SaswatPadhi added aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Jun 23, 2021

SaswatPadhi requested a review from feliperodri June 23, 2021 19:04

SaswatPadhi changed the title ~~Created cprover_loop_contract~~ Parser support for assigns contracts on loops Jun 23, 2021

aalok-thakkar force-pushed the loop-contract branch 2 times, most recently from ec43ea3 to 83a39db Compare June 23, 2021 20:10

SaswatPadhi suggested changes Jun 23, 2021

View reviewed changes

src/ansi-c/parser.y Outdated Show resolved Hide resolved

src/ansi-c/parser.y Outdated Show resolved Hide resolved

aalok-thakkar force-pushed the loop-contract branch 3 times, most recently from 990341f to c50fb3a Compare June 24, 2021 21:16

feliperodri approved these changes Jun 25, 2021

View reviewed changes

aalok-thakkar force-pushed the loop-contract branch 3 times, most recently from 36419cc to c07518e Compare June 25, 2021 19:18

aalok-thakkar requested review from allredj, martin-cs, peterschrammel and romainbrenguier as code owners June 25, 2021 19:18

SaswatPadhi marked this pull request as draft June 26, 2021 04:28

martin-cs reviewed Jun 27, 2021

View reviewed changes

aalok-thakkar force-pushed the loop-contract branch from c07518e to c5e09d0 Compare June 28, 2021 16:05

SaswatPadhi suggested changes Jun 28, 2021

View reviewed changes

src/ansi-c/parser.y Outdated Show resolved Hide resolved

aalok-thakkar force-pushed the loop-contract branch from c5e09d0 to 26a3b3c Compare June 28, 2021 17:09

SaswatPadhi marked this pull request as ready for review June 28, 2021 17:36

SaswatPadhi requested a review from martin-cs June 28, 2021 17:36

SaswatPadhi approved these changes Jun 28, 2021

View reviewed changes

martin-cs requested changes Jun 29, 2021

View reviewed changes

aalok-thakkar force-pushed the loop-contract branch 4 times, most recently from e166702 to 64b5182 Compare July 1, 2021 18:38

feliperodri added the C Front End label Jul 7, 2021

feliperodri requested changes Jul 7, 2021

View reviewed changes

aalok-thakkar force-pushed the loop-contract branch from 64b5182 to df7696e Compare July 7, 2021 17:52

aalok-thakkar requested a review from a team as a code owner July 8, 2021 18:26

aalok-thakkar force-pushed the loop-contract branch 2 times, most recently from dbe9e64 to 5717865 Compare July 8, 2021 18:48

feliperodri requested changes Jul 8, 2021

View reviewed changes

aalok-thakkar force-pushed the loop-contract branch 4 times, most recently from 6d7db3d to 1868741 Compare July 9, 2021 15:17

feliperodri approved these changes Jul 10, 2021

View reviewed changes

aalok-thakkar force-pushed the loop-contract branch from 1868741 to e190b7f Compare July 12, 2021 13:59

martin-cs approved these changes Jul 12, 2021

View reviewed changes

regression/contracts/invar_assigns_alias_analysis/test.desc Show resolved Hide resolved

chrisr-diffblue approved these changes Jul 13, 2021

View reviewed changes

feliperodri merged commit 9f19902 into diffblue:develop Jul 13, 2021

SaswatPadhi mentioned this pull request Nov 19, 2021

Add support for assigns clauses on loops #6249

Merged

5 tasks

		This test shows that the current implementation only supports
		parsing and still uses alias analysis. Fixing this is a part

Parser support for assigns contracts on loops #6196

Parser support for assigns contracts on loops #6196

Uh oh!

Conversation

aalok-thakkar commented Jun 23, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Jun 23, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

SaswatPadhi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi commented Jun 26, 2021

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feliperodri Jul 8, 2021

Choose a reason for hiding this comment

Uh oh!

aalok-thakkar Jul 9, 2021

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi Jul 10, 2021

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

feliperodri commented Jul 12, 2021

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

aalok-thakkar commented Jun 23, 2021 •

edited

Loading

codecov bot commented Jun 23, 2021 •

edited

Loading