New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

CONTRACTS: class to instrument a single loop #7672

Merged

remi-delmas-3000 merged 1 commit into diffblue:develop from remi-delmas-3000:contracts-instrument-loop

May 5, 2023

Collaborator

remi-delmas-3000 commented Apr 18, 2023

The first commit is from #7671, do not review.

The second commit adds a class that applies loop contract transformation to a single loop in a goto program.

The PR is extracted from the larger PR #7541 and will be tested once all features have been merged.

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.

remi-delmas-3000 requested review from tautschnig, feliperodri, martin-cs, chris-ryder, peterschrammel and kroening as code owners

April 18, 2023 16:32

remi-delmas-3000 self-assigned this

remi-delmas-3000 added aws aws-high Code Contracts labels

remi-delmas-3000 force-pushed the contracts-instrument-loop branch from 73d5de2 to a9edbb0 Compare

April 18, 2023 16:37

codecov bot commented Apr 18, 2023 •

edited

Loading

Codecov Report

Patch coverage has no change and project coverage change: +0.06 🎉

Comparison is base (abad42b) 78.44% compared to head (c9f2932) 78.50%.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7672      +/-   ##
===========================================
+ Coverage    78.44%   78.50%   +0.06%     
===========================================
  Files         1674     1674              
  Lines       191946   191954       +8     
===========================================
+ Hits        150567   150698     +131     
+ Misses       41379    41256     -123

Impacted Files	Coverage Δ
...strument/contracts/dynamic-frames/dfcc_library.cpp	`91.01% <0.00%> (-2.64%)`	⬇️

... and 18 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

remi-delmas-3000 mentioned this pull request

CONTRACTS: Dynamic frames for loop contracts #7541

Merged

7 tasks

remi-delmas-3000 assigned tautschnig, feliperodri and qinheping

remi-delmas-3000 changed the title ~~Contracts instrument loop~~ CONTRACTS: class to instrument a single loop

remi-delmas-3000 force-pushed the contracts-instrument-loop branch 2 times, most recently from 08dfebc to 6143154 Compare

April 20, 2023 19:37

tautschnig mentioned this pull request

Refactor replace_history_parameter #7686

Merged

4 tasks

tautschnig reviewed

View reviewed changes

Collaborator

tautschnig left a comment

Some preliminary comments, more reviewing to be done.

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated

Comment on lines 98 to 102

+                  const auto old_decreases_var =
+                    new_tmp_symbol(clause.type(), head_location, language_mode, symbol_table)
+                      .symbol_expr();
+                  old_decreases_vars.push_back(old_decreases_var);
+                  // new
+                  const auto new_decreases_var =

Collaborator

tautschnig Apr 24, 2023

I don't think the names of those temporaries add a lot of value, could you please just do old_decreases_vars.push_back(new_tmp_symbol... and new_decreases_vars.push_back(new_tmp_symbol...

Collaborator Author

remi-delmas-3000 Apr 25, 2023

proper naming helps a lot for debugging

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

tautschnig removed their assignment

qinheping force-pushed the contracts-instrument-loop branch from 6143154 to 102584b Compare

April 26, 2023 17:52

tautschnig reviewed

View reviewed changes

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

remi-delmas-3000 force-pushed the contracts-instrument-loop branch 2 times, most recently from d08a0e7 to 9a0c7d8 Compare

May 2, 2023 16:41

qinheping force-pushed the contracts-instrument-loop branch from 9a0c7d8 to a1f4292 Compare

May 2, 2023 21:36

remi-delmas-3000 force-pushed the contracts-instrument-loop branch from a1f4292 to 78354e5 Compare

May 4, 2023 15:29

tautschnig approved these changes

View reviewed changes

Collaborator

tautschnig left a comment

Just some minor suggestions.

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp Outdated Show resolved Hide resolved


          CONTRACTS: class that applies loop contract transformations

c9f2932

Co-authored-by: Qinheping Hu <qinhh@amazon.com>"

qinheping force-pushed the contracts-instrument-loop branch from 78354e5 to c9f2932 Compare

May 5, 2023 18:32

remi-delmas-3000 enabled auto-merge

May 5, 2023 18:41

qinheping approved these changes

View reviewed changes

remi-delmas-3000 merged commit cafbcc4 into diffblue:develop

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

qinheping qinheping approved these changes

tautschnig tautschnig approved these changes

feliperodri Awaiting requested review from feliperodri feliperodri is a code owner

martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

chris-ryder Awaiting requested review from chris-ryder

peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

kroening Awaiting requested review from kroening kroening is a code owner

Labels

aws aws-high Code Contracts